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' [Params] (S : BaseSupport) (a : Atom) : BaseSupport

Equations

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

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

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

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

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

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

Equations

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

@[simp]

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

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

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

structure ConNF.Information [Params] : Type u

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

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

Equations

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

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

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

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

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

Equations

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

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

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

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

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