Counting support orbits

In this file, we prove an upper bound on the amount of orbits of supports that can exist.

Main declarations

• ConNF.card_supportOrbit_lt: The amount of support orbits is strictly less than μ, given an inductive hypothesis about the amount of coding functions at lower levels.

structure ConNF.WeakSpec [Params] [Level] [CoherentData] (β : TypeIndex) [LeLevel β] : Type u

• atomsBound : Tree κ β
• nearLittersBound : Tree κ β
• atoms : Tree (Set κ) β
• nearLitters : Tree (Set κ) β
• spec : Spec β

instance ConNF.instSuperAWeakSpecTreeSetκ [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] : SuperA (WeakSpec β) (Tree (Set κ) β)

Equations

• ConNF.instSuperAWeakSpecTreeSetκ = { superA := ConNF.WeakSpec.atoms }

instance ConNF.instSuperNWeakSpecTreeSetκ [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] : SuperN (WeakSpec β) (Tree (Set κ) β)

Equations

• ConNF.instSuperNWeakSpecTreeSetκ = { superN := ConNF.WeakSpec.nearLitters }

def ConNF.WeakSpec.Specifies [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (σ : WeakSpec β) (S : Support β) : Prop

Equations

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

theorem ConNF.WeakSpec.exists [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) : ∃ (σ : WeakSpec β), σ.Specifies S

theorem ConNF.WeakSpec.exists_conv [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (σ : WeakSpec β) {S T : Support β} (hS : σ.Specifies S) (hT : σ.Specifies T) : ∃ (ρ : AllPerm β), ρᵁ • S = T

def ConNF.weakSpecEquiv [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] : WeakSpec β ≃ Tree κ β × Tree κ β × Tree (Set κ) β × Tree (Set κ) β × Spec β

Equations

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

theorem ConNF.card_weakSpec_of_card_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (h : Cardinal.mk (Spec β) < Cardinal.mk μ) : Cardinal.mk (WeakSpec β) < Cardinal.mk μ

def ConNF.specEquiv [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] : Spec β ≃ Tree (Enumeration AtomCond) β × Tree (Enumeration (NearLitterCond β)) β

Equations

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

def ConNF.atomCondEquiv [Params] : AtomCond ≃ Set κ × Set κ

Equations

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

def ConNF.nearLitterCondEquiv [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] : NearLitterCond β ≃ FlexCond ⊕ (P : InflexiblePath β) × InflexCond P.δ

Equations

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

def ConNF.flexCondEquiv [Params] : FlexCond ≃ Set κ

Equations

• ConNF.flexCondEquiv = { toFun := fun (x : ConNF.FlexCond) => x.nearLitters, invFun := fun (x : Set ConNF.κ) => { nearLitters := x }, left_inv := ⋯, right_inv := ⋯ }

def ConNF.inflexCondEquiv [Params] [Level] [CoherentData] (δ : TypeIndex) [LeLevel δ] : InflexCond δ ≃ CodingFunction δ × Tree (Rel κ κ) δ × Tree (Rel κ κ) δ

Equations

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

theorem ConNF.card_spec_of_card_codingFunction [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (h : ∀ δ < β, ∀ [inst : LeLevel δ], Cardinal.mk (CodingFunction δ) < Cardinal.mk μ) : Cardinal.mk (Spec β) < Cardinal.mk μ

theorem ConNF.card_supportOrbit_lt' [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] : Cardinal.mk (SupportOrbit β) ≤ Cardinal.mk (WeakSpec β)

theorem ConNF.card_supportOrbit_lt [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (h : ∀ δ < β, ∀ [inst : LeLevel δ], Cardinal.mk (CodingFunction δ) < Cardinal.mk μ) : Cardinal.mk (SupportOrbit β) < Cardinal.mk μ