Coding the base type

In this file, we prove a consequence of freedom of action for ⊥: a base support can support at most 2 ^ #κ-many different sets of atoms under the action of base permutations.

Main declarations

• ConNF.foo: Something new.

def ConNF.addAtom' [ConNF.Params] (S : ConNF.BaseSupport) (a : ConNF.Atom) : ConNF.BaseSupport

Equations

• ConNF.addAtom' S a = { atoms := Sᴬ + ConNF.Enumeration.singleton a, nearLitters := Sᴺ }

theorem ConNF.addAtom'_atoms [ConNF.Params] (S : ConNF.BaseSupport) (a : ConNF.Atom) : (ConNF.addAtom' S a)ᴬ = Sᴬ + ConNF.Enumeration.singleton a

theorem ConNF.addAtom'_nearLitters [ConNF.Params] (S : ConNF.BaseSupport) (a : ConNF.Atom) : (ConNF.addAtom' S a)ᴺ = Sᴺ

theorem ConNF.addAtom'_atoms_rel [ConNF.Params] (S : ConNF.BaseSupport) (a : ConNF.Atom) (i : ConNF.κ) (b : ConNF.Atom) : (ConNF.addAtom' S a)ᴬ.rel i b ↔ Sᴬ.rel i b ∨ b = a ∧ i = Sᴬ.bound

theorem ConNF.addAtom'_closed [ConNF.Params] (S : ConNF.BaseSupport) (a : ConNF.Atom) (hS : S.Closed) : (ConNF.addAtom' S a).Closed

def ConNF.Support.ofBase [ConNF.Params] (S : ConNF.BaseSupport) : ConNF.Support ⊥

Equations

• ConNF.Support.ofBase S = { atoms := Sᴬ.invImage Prod.snd ⋯, nearLitters := Sᴺ.invImage Prod.snd ⋯ }

@[simp]

theorem ConNF.Support.ofBase_derivBot [ConNF.Params] (S : ConNF.BaseSupport) (A : ⊥ ↝ ⊥) : ConNF.Support.ofBase S ⇘. A = S

theorem ConNF.InflexiblePath.elim_bot [ConNF.Params] (P : ConNF.InflexiblePath ⊥) : False

theorem ConNF.bot_preStrong [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (S : ConNF.Support ⊥) : S.PreStrong

def ConNF.addAtom [ConNF.Params] (S : ConNF.BaseSupport) (a : ConNF.Atom) : ConNF.Support ⊥

Equations

• ConNF.addAtom S a = ConNF.Support.ofBase (ConNF.addAtom' S a)

theorem ConNF.addAtom_derivBot [ConNF.Params] (S : ConNF.BaseSupport) (a : ConNF.Atom) (A : ⊥ ↝ ⊥) : ConNF.addAtom S a ⇘. A = ConNF.addAtom' S a

theorem ConNF.addAtom_strong [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (S : ConNF.BaseSupport) (a : ConNF.Atom) (hS : S.Closed) : (ConNF.addAtom S a).Strong

@[simp]

theorem ConNF.addAtom_convAtoms [ConNF.Params] (S : ConNF.BaseSupport) (a₁ a₂ : ConNF.Atom) (A : ⊥ ↝ ⊥) : ConNF.convAtoms (ConNF.addAtom S a₁) (ConNF.addAtom S a₂) A = fun (a₃ a₄ : ConNF.Atom) => a₃ = a₄ ∧ a₃ ∈ Sᴬ ∨ a₃ = a₁ ∧ a₄ = a₂

@[simp]

theorem ConNF.addAtom_convNearLitters [ConNF.Params] (S : ConNF.BaseSupport) (a₁ a₂ : ConNF.Atom) (A : ⊥ ↝ ⊥) : ConNF.convNearLitters (ConNF.addAtom S a₁) (ConNF.addAtom S a₂) A = fun (N₁ N₂ : ConNF.NearLitter) => N₁ = N₂ ∧ N₁ ∈ Sᴺ

theorem ConNF.addAtom_sameSpecLe [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {S : ConNF.BaseSupport} {a₁ a₂ : ConNF.Atom} (ha₁ : a₁ ∉ Sᴬ) (ha₂ : a₂ ∉ Sᴬ) (ha : ∀ N ∈ Sᴺ, a₁ ∈ Nᴬ ↔ a₂ ∈ Nᴬ) : ConNF.SameSpecLE (ConNF.addAtom S a₁) (ConNF.addAtom S a₂)

theorem ConNF.addAtom_spec_eq_spec [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {S : ConNF.BaseSupport} {a₁ a₂ : ConNF.Atom} (ha₁ : a₁ ∉ Sᴬ) (ha₂ : a₂ ∉ Sᴬ) (ha : ∀ N ∈ Sᴺ, a₁ ∈ Nᴬ ↔ a₂ ∈ Nᴬ) : (ConNF.addAtom S a₁).spec = (ConNF.addAtom S a₂).spec

theorem ConNF.exists_swap [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {S : ConNF.BaseSupport} (h : S.Closed) {a₁ a₂ : ConNF.Atom} (ha₁ : a₁ ∉ Sᴬ) (ha₂ : a₂ ∉ Sᴬ) (ha : ∀ N ∈ Sᴺ, a₁ ∈ Nᴬ ↔ a₂ ∈ Nᴬ) : ∃ (π : ConNF.BasePerm), π • S = S ∧ π • a₁ = a₂

theorem ConNF.mem_iff_mem_of_supports [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {S : ConNF.BaseSupport} (h : S.Closed) {s : Set ConNF.Atom} (hs : ∀ (π : ConNF.BasePerm), π • S = S → π • s = s) {a₁ a₂ : ConNF.Atom} (h₁ : a₁ ∉ Sᴬ) (h₂ : a₂ ∉ Sᴬ) (ha : ∀ N ∈ Sᴺ, a₁ ∈ Nᴬ ↔ a₂ ∈ Nᴬ) : a₁ ∈ s ↔ a₂ ∈ s

structure ConNF.Information [ConNF.Params] : Type u

• atoms : Set ConNF.κ
• nearLitters : Set ConNF.κ
• outside : Prop

def ConNF.information [ConNF.Params] (S : ConNF.BaseSupport) (s : Set ConNF.Atom) : ConNF.Information

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.subset_of_information_eq [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {S : ConNF.BaseSupport} (hS : S.Closed) {s t : Set ConNF.Atom} (hs : ∀ (π : ConNF.BasePerm), π • S = S → π • s = s) (ht : ∀ (π : ConNF.BasePerm), π • S = S → π • t = t) (h : ConNF.information S s = ConNF.information S t) : s ⊆ t

theorem ConNF.eq_of_information_eq [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {S : ConNF.BaseSupport} (hS : S.Closed) {s t : Set ConNF.Atom} (hs : ∀ (π : ConNF.BasePerm), π • S = S → π • s = s) (ht : ∀ (π : ConNF.BasePerm), π • S = S → π • t = t) (h : ConNF.information S s = ConNF.information S t) : s = t

theorem ConNF.card_supports_le_of_closed' [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {S : ConNF.BaseSupport} (hS : S.Closed) : Cardinal.mk { s : Set ConNF.Atom // ∀ (π : ConNF.BasePerm), π • S = S → π • s = s } ≤ Cardinal.mk ConNF.Information

def ConNF.informationEquiv [ConNF.Params] : ConNF.Information ≃ Set ConNF.κ × Set ConNF.κ × Prop

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.card_information_le [ConNF.Params] : Cardinal.mk ConNF.Information ≤ 2 ^ Cardinal.mk ConNF.κ

theorem ConNF.card_supports_le_of_closed [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {S : ConNF.BaseSupport} (hS : S.Closed) : Cardinal.mk { s : Set ConNF.Atom // ∀ (π : ConNF.BasePerm), π • S = S → π • s = s } ≤ 2 ^ Cardinal.mk ConNF.κ

theorem ConNF.BaseSupport.interference_small [ConNF.Params] (S : ConNF.BaseSupport) : ConNF.Small {a : ConNF.Atom | ∃ (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter), N₁ ∈ Sᴺ ∧ N₂ ∈ Sᴺ ∧ a ∈ ConNF.interference N₁ N₂}

theorem ConNF.card_supports_le [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (S : ConNF.BaseSupport) : Cardinal.mk { s : Set ConNF.Atom // ∀ (π : ConNF.BasePerm), π • S = S → π • s = s } ≤ 2 ^ Cardinal.mk ConNF.κ