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 [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : Type u

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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