def ConNF.MainInduction.instLevel [ConNF.Params] : ConNF.Level

Equations

• ConNF.MainInduction.instLevel = { α := 0 }

theorem ConNF.MainInduction.zeroModelData_subsingleton [ConNF.Params] [ConNF.BasePositions] (i₁ : ConNF.ModelDataLt) (j₁ : ConNF.ModelDataLt) (i₂ : ConNF.PositionedTanglesLt) (j₂ : ConNF.PositionedTanglesLt) (i₃ : ConNF.TypedObjectsLt) (j₃ : ConNF.TypedObjectsLt) (i₄ : ConNF.PositionedObjectsLt) (j₄ : ConNF.PositionedObjectsLt) : ConNF.ModelData.mk ConNF.NewTSet ConNF.NewAllowable ConNF.NewAllowable.toStructPerm ⋯ ⋯ { toFun := ConNF.NewTSet.toStructSet, inj' := ⋯ } ⋯ = ConNF.ModelData.mk ConNF.NewTSet ConNF.NewAllowable ConNF.NewAllowable.toStructPerm ⋯ ⋯ { toFun := ConNF.NewTSet.toStructSet, inj' := ⋯ } ⋯

def ConNF.MainInduction.instModelDataLt [ConNF.Params] : ConNF.ModelDataLt

Equations

• ConNF.MainInduction.instModelDataLt = { data := fun (β : ConNF.Λ) (i : ConNF.LtLevel ↑β) => ⋯.elim }

def ConNF.MainInduction.instPositionedTanglesLt [ConNF.Params] : ConNF.PositionedTanglesLt

Equations

• ConNF.MainInduction.instPositionedTanglesLt = { data := fun (β : ConNF.Λ) (i : ConNF.LtLevel ↑β) => ⋯.elim }

def ConNF.MainInduction.instTypedObjectsLt [ConNF.Params] : ConNF.TypedObjectsLt

Equations

• ConNF.MainInduction.instTypedObjectsLt β = ⋯.elim

def ConNF.MainInduction.instPositionedObjectsLt [ConNF.Params] [ConNF.BasePositions] : ConNF.PositionedObjectsLt

Equations

• ⋯ = ⋯

def ConNF.MainInduction.zeroModelData [ConNF.Params] [ConNF.BasePositions] : ConNF.ModelData ↑0

Equations

• ConNF.MainInduction.zeroModelData = ConNF.ModelData.mk ConNF.NewTSet ConNF.NewAllowable ConNF.NewAllowable.toStructPerm ⋯ ⋯ { toFun := ConNF.NewTSet.toStructSet, inj' := ⋯ } ⋯

def ConNF.MainInduction.zeroTypedObjects [ConNF.Params] [ConNF.BasePositions] : ConNF.TypedObjects 0

Equations

• ConNF.MainInduction.zeroTypedObjects = { typedNearLitter := { toFun := ConNF.newTypedNearLitter, inj' := ⋯ }, smul_typedNearLitter := ⋯ }

def ConNF.MainInduction.zeroPath [ConNF.Params] : ConNF.ExtendedIndex 0

Equations

• ConNF.MainInduction.zeroPath = Quiver.Hom.toPath ⋯

theorem ConNF.MainInduction.path_eq_zeroPath [ConNF.Params] (A : ConNF.ExtendedIndex 0) : A = ConNF.MainInduction.zeroPath

theorem ConNF.MainInduction.not_ltLevel [ConNF.Params] (β : ConNF.Λ) [i : ConNF.LtLevel ↑β] : False

theorem ConNF.MainInduction.eq_bot_of_ltLevel [ConNF.Params] (β : ConNF.TypeIndex) [ConNF.LtLevel β] : β = ⊥

theorem ConNF.MainInduction.eq_zero_of_leLevel [ConNF.Params] (β : ConNF.Λ) [i : ConNF.LeLevel ↑β] : β = 0

theorem ConNF.MainInduction.eq_bot_zero_of_lt [ConNF.Params] (γ : ConNF.TypeIndex) (β : ConNF.TypeIndex) [iβ : ConNF.LeLevel β] [iγ : ConNF.LeLevel γ] (h : γ < β) : γ = ⊥ ∧ β = 0

def ConNF.MainInduction.toSemiallowable [ConNF.Params] (π : ConNF.BasePerm) : ConNF.Derivatives

Equations

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

theorem ConNF.MainInduction.toSemiallowable_allowable [ConNF.Params] [ConNF.BasePositions] (π : ConNF.BasePerm) : (ConNF.MainInduction.toSemiallowable π).IsAllowable

def ConNF.MainInduction.toAllowable [ConNF.Params] [ConNF.BasePositions] (π : ConNF.BasePerm) : ConNF.NewAllowable

Equations

• ConNF.MainInduction.toAllowable π = ⟨ConNF.MainInduction.toSemiallowable π, ⋯⟩

def ConNF.MainInduction.zeroDerivative [ConNF.Params] [ConNF.BasePositions] : ConNF.NewAllowable →* ConNF.BasePerm

Equations

• ConNF.MainInduction.zeroDerivative = { toFun := fun (ρ : ConNF.NewAllowable) => ↑ρ ⊥, map_one' := ⋯, map_mul' := ⋯ }

instance ConNF.MainInduction.instMulActionAllowableSomeΛOfNatOfBasePerm [ConNF.Params] [ConNF.BasePositions] {X : Type u_1} [MulAction ConNF.BasePerm X] : MulAction (ConNF.Allowable ↑0) X

Equations

• ConNF.MainInduction.instMulActionAllowableSomeΛOfNatOfBasePerm = MulAction.compHom X ConNF.MainInduction.zeroDerivative

instance ConNF.MainInduction.instMulActionAllowableSomeΛOfNatOfNewAllowable [ConNF.Params] [ConNF.BasePositions] {X : Type u_1} [i : MulAction ConNF.NewAllowable X] : MulAction (ConNF.Allowable ↑0) X

Equations

• ConNF.MainInduction.instMulActionAllowableSomeΛOfNatOfNewAllowable = i

def ConNF.MainInduction.instFOAData [ConNF.Params] [ConNF.BasePositions] : ConNF.FOAData

Equations

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

def ConNF.MainInduction.instFOAAssumptions [ConNF.Params] [ConNF.BasePositions] : ConNF.FOAAssumptions

Equations

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

theorem ConNF.MainInduction.zero_flexible [ConNF.Params] [ConNF.BasePositions] {A : ConNF.ExtendedIndex 0} {L : ConNF.Litter} : ConNF.Flexible A L

def ConNF.MainInduction.toStructNLAction [ConNF.Params] (ξ : ConNF.BaseNLAction) : ConNF.StructNLAction 0

Equations

• ConNF.MainInduction.toStructNLAction ξ x = ξ

theorem ConNF.MainInduction.toStructNLAction_coherentDom [ConNF.Params] [ConNF.BasePositions] (ξ : ConNF.BaseNLAction) : (ConNF.MainInduction.toStructNLAction ξ).CoherentDom

theorem ConNF.MainInduction.toStructNLAction_coherent [ConNF.Params] [ConNF.BasePositions] (ξ : ConNF.BaseNLAction) : (ConNF.MainInduction.toStructNLAction ξ).Coherent

theorem ConNF.MainInduction.zero_foa [ConNF.Params] [ConNF.BasePositions] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) : ∃ (π : ConNF.BasePerm), ξ.Approximates π

An instance of the freedom of action theorem for type zero.

def ConNF.MainInduction.ZeroStrong [ConNF.Params] (S : ConNF.Support 0) : Prop

Equations

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

theorem ConNF.MainInduction.ZeroSpec.ext : ∀ {inst : ConNF.Params} (x y : ConNF.MainInduction.ZeroSpec), x.max = y.max → x.nearLitters = y.nearLitters → x.atoms = y.atoms → x.nearLitterSame = y.nearLitterSame → x.symmDiff = y.symmDiff → x.atomSame = y.atomSame → x.atomMem = y.atomMem → x = y

theorem ConNF.MainInduction.ZeroSpec.ext_iff : ∀ {inst : ConNF.Params} (x y : ConNF.MainInduction.ZeroSpec), x = y ↔ x.max = y.max ∧ x.nearLitters = y.nearLitters ∧ x.atoms = y.atoms ∧ x.nearLitterSame = y.nearLitterSame ∧ x.symmDiff = y.symmDiff ∧ x.atomSame = y.atomSame ∧ x.atomMem = y.atomMem

structure ConNF.MainInduction.ZeroSpec [ConNF.Params] : Type u

• max : ConNF.κ

  The length of the support.

• nearLitters : Set ConNF.κ

  Positions in a support containing a near-litter.

• atoms : Set ConNF.κ

  Positions in a support containing an atom.

• nearLitterSame : ConNF.κ → Set ConNF.κ

  For each position in a support containing a near-litter, the set of all positions at which another close near-litter occurs.

• symmDiff : ConNF.κ → ConNF.κ → Set ConNF.κ

  For each pair of near-litter positions, the set of all positions at which an atom in their symmetric difference occurs.

• atomSame : ConNF.κ → Set ConNF.κ

  For each position in a support containing an atom, the set of all positions this atom occurs at.

• atomMem : ConNF.κ → Set ConNF.κ

  For each position in a support containing an atom, the positions of near-litters that contain this atom.

instance ConNF.MainInduction.instLEZeroSpec [ConNF.Params] : LE ConNF.MainInduction.ZeroSpec

Equations

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

instance ConNF.MainInduction.instPartialOrderZeroSpec [ConNF.Params] : PartialOrder ConNF.MainInduction.ZeroSpec

Equations

• ConNF.MainInduction.instPartialOrderZeroSpec = PartialOrder.mk ⋯

def ConNF.MainInduction.ZeroSpec.decompose [ConNF.Params] (σ : ConNF.MainInduction.ZeroSpec) : ConNF.κ × Set ConNF.κ × Set ConNF.κ × (ConNF.κ → Set ConNF.κ) × (ConNF.κ → ConNF.κ → Set ConNF.κ) × (ConNF.κ → Set ConNF.κ) × (ConNF.κ → Set ConNF.κ)

Equations

• σ.decompose = (σ.max, σ.nearLitters, σ.atoms, σ.nearLitterSame, σ.symmDiff, σ.atomSame, σ.atomMem)

theorem ConNF.MainInduction.ZeroSpec.decompose_injective [ConNF.Params] : Function.Injective ConNF.MainInduction.ZeroSpec.decompose

theorem ConNF.MainInduction.mk_zeroSpec [ConNF.Params] : Cardinal.mk ConNF.MainInduction.ZeroSpec < Cardinal.mk ConNF.μ

def ConNF.MainInduction.zeroSpec [ConNF.Params] (S : ConNF.Support 0) : ConNF.MainInduction.ZeroSpec

Equations

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

def ConNF.MainInduction.ConvertAtom [ConNF.Params] (S : ConNF.Support 0) (T : ConNF.Support 0) (aS : ConNF.Atom) (aT : ConNF.Atom) : Prop

Equations

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

def ConNF.MainInduction.ConvertNearLitter [ConNF.Params] (S : ConNF.Support 0) (T : ConNF.Support 0) (NS : ConNF.NearLitter) (NT : ConNF.NearLitter) : Prop

Equations

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

theorem ConNF.MainInduction.convertAtom_subsingleton [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) (aS : ConNF.Atom) (aT : ConNF.Atom) (aT' : ConNF.Atom) (h : ConNF.MainInduction.ConvertAtom S T aS aT) (h' : ConNF.MainInduction.ConvertAtom S T aS aT') : aT = aT'

theorem ConNF.MainInduction.convertNearLitter_fst [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) (NS : ConNF.NearLitter) (NS' : ConNF.NearLitter) (NT : ConNF.NearLitter) (NT' : ConNF.NearLitter) (hN : NS.fst = NS'.fst) (h : ConNF.MainInduction.ConvertNearLitter S T NS NT) (h' : ConNF.MainInduction.ConvertNearLitter S T NS' NT') : NT.fst = NT'.fst

theorem ConNF.MainInduction.convertNearLitter_fst' [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) (NS : ConNF.NearLitter) (NS' : ConNF.NearLitter) (NT : ConNF.NearLitter) (NT' : ConNF.NearLitter) (hN : NT.fst = NT'.fst) (h : ConNF.MainInduction.ConvertNearLitter S T NS NT) (h' : ConNF.MainInduction.ConvertNearLitter S T NS' NT') : NS.fst = NS'.fst

theorem ConNF.MainInduction.convertNearLitter_subsingleton [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hT : ConNF.MainInduction.ZeroStrong T) (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) (NS : ConNF.NearLitter) (NT : ConNF.NearLitter) (NT' : ConNF.NearLitter) (h : ConNF.MainInduction.ConvertNearLitter S T NS NT) (h' : ConNF.MainInduction.ConvertNearLitter S T NS NT') : NT = NT'

theorem ConNF.MainInduction.convertAtom_dom_small [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} : ConNF.Small {a : ConNF.Atom | ∃ (a' : ConNF.Atom), ConNF.MainInduction.ConvertAtom S T a a'}

theorem ConNF.MainInduction.convertNearLitter_dom_small [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} : ConNF.Small {N : ConNF.NearLitter | ∃ (N' : ConNF.NearLitter), ConNF.MainInduction.ConvertNearLitter S T N N'}

noncomputable def ConNF.MainInduction.convert [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hT : ConNF.MainInduction.ZeroStrong T) (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) : ConNF.BaseNLAction

Equations

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

theorem ConNF.MainInduction.convert_atomMap_eq [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hT : ConNF.MainInduction.ZeroStrong T) (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) {a : ConNF.Atom} {b : ConNF.Atom} (h : ConNF.MainInduction.ConvertAtom S T a b) : ((ConNF.MainInduction.convert hT hST).atomMap a).get ⋯ = b

theorem ConNF.MainInduction.convert_nearLitterMap_eq [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hT : ConNF.MainInduction.ZeroStrong T) (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : ConNF.MainInduction.ConvertNearLitter S T N₁ N₂) : ((ConNF.MainInduction.convert hT hST).nearLitterMap N₁).get ⋯ = N₂

theorem ConNF.MainInduction.convertAtom_injective [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) {a : ConNF.Atom} {b : ConNF.Atom} {c : ConNF.Atom} (ha : ConNF.MainInduction.ConvertAtom S T a c) (hb : ConNF.MainInduction.ConvertAtom S T b c) : a = b

theorem ConNF.MainInduction.convertAtom_eq [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) {a : ConNF.Atom} {a' : ConNF.Atom} {N : ConNF.NearLitter} {N' : ConNF.NearLitter} (ha : ConNF.MainInduction.ConvertAtom S T a a') (hN : ConNF.MainInduction.ConvertNearLitter S T N N') : a' ∈ N' ↔ a ∈ N

theorem ConNF.MainInduction.dom_of_interferes [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hS : ConNF.MainInduction.ZeroStrong S) (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) {a : ConNF.Atom} {N₁ : ConNF.NearLitter} {N₁' : ConNF.NearLitter} {N₂ : ConNF.NearLitter} {N₂' : ConNF.NearLitter} (h : ConNF.Support.Interferes a N₁ N₂) (hN₁ : ConNF.MainInduction.ConvertNearLitter S T N₁ N₁') (hN₂ : ConNF.MainInduction.ConvertNearLitter S T N₂ N₂') : ∃ (a' : ConNF.Atom), ConNF.MainInduction.ConvertAtom S T a a'

theorem ConNF.MainInduction.ran_of_interferes [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hT : ConNF.MainInduction.ZeroStrong T) (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) {a' : ConNF.Atom} {N₁ : ConNF.NearLitter} {N₁' : ConNF.NearLitter} {N₂ : ConNF.NearLitter} {N₂' : ConNF.NearLitter} (h : ConNF.Support.Interferes a' N₁' N₂') (hN₁ : ConNF.MainInduction.ConvertNearLitter S T N₁ N₁') (hN₂ : ConNF.MainInduction.ConvertNearLitter S T N₂ N₂') : ∃ (a : ConNF.Atom), ConNF.MainInduction.ConvertAtom S T a a'

theorem ConNF.MainInduction.convert_lawful [ConNF.Params] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hS : ConNF.MainInduction.ZeroStrong S) (hT : ConNF.MainInduction.ZeroStrong T) (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) : (ConNF.MainInduction.convert hT hST).Lawful

theorem ConNF.MainInduction.exists_convertAllowable [ConNF.Params] [ConNF.BasePositions] {S : ConNF.Support ↑0} {T : ConNF.Support ↑0} (hS : ConNF.MainInduction.ZeroStrong S) (hT : ConNF.MainInduction.ZeroStrong T) (hST : ConNF.MainInduction.zeroSpec S = ConNF.MainInduction.zeroSpec T) : ∃ (ρ : ConNF.Allowable ↑0), ρ • S = T

def ConNF.MainInduction.interference [ConNF.Params] (S : Set (ConNF.Address 0)) : Set ConNF.Atom

Equations

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

def ConNF.MainInduction.interference' [ConNF.Params] (S : Set (ConNF.Address 0)) : Set ConNF.Atom

Equations

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

theorem ConNF.MainInduction.interference_eq_interference' [ConNF.Params] (S : Set (ConNF.Address 0)) : ConNF.MainInduction.interference S = ConNF.MainInduction.interference' S

theorem ConNF.MainInduction.interference_small [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) : ConNF.Small (ConNF.MainInduction.interference S)

def ConNF.MainInduction.disjointNL' [ConNF.Params] (S : Set (ConNF.Address 0)) (N : ConNF.NearLitter) : Set ConNF.Atom

Equations

• ConNF.MainInduction.disjointNL' S N = ↑N \ ConNF.MainInduction.interference S

theorem ConNF.MainInduction.disjointNL'_isNear [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) (N : ConNF.NearLitter) : ConNF.IsNearLitter N.fst (ConNF.MainInduction.disjointNL' S N)

theorem ConNF.MainInduction.disjointNL'_eq [ConNF.Params] (S : Set (ConNF.Address 0)) (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter) (hN₁ : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N₁ } ∈ S) (hN₂ : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N₂ } ∈ S) (h : N₁.fst = N₂.fst) : ConNF.MainInduction.disjointNL' S N₁ = ConNF.MainInduction.disjointNL' S N₂

def ConNF.MainInduction.disjointNL [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) (N : ConNF.NearLitter) : ConNF.NearLitter

Equations

• ConNF.MainInduction.disjointNL S hS N = ⟨N.fst, ⟨ConNF.MainInduction.disjointNL' S N, ⋯⟩⟩

theorem ConNF.MainInduction.disjointNL_eq [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter) (hN₁ : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N₁ } ∈ S) (hN₂ : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N₂ } ∈ S) (h : N₁.fst = N₂.fst) : ConNF.MainInduction.disjointNL S hS N₁ = ConNF.MainInduction.disjointNL S hS N₂

def ConNF.MainInduction.disjointNLs [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) : Set ConNF.NearLitter

Equations

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

def ConNF.MainInduction.disjointNLs' [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) : Set ConNF.NearLitter

Equations

• ConNF.MainInduction.disjointNLs' S hS = ⋃ N ∈ {N : ConNF.NearLitter | { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S}, {ConNF.MainInduction.disjointNL S hS N}

theorem ConNF.MainInduction.disjointNLs_eq_disjointNLs' [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) : ConNF.MainInduction.disjointNLs S hS = ConNF.MainInduction.disjointNLs' S hS

theorem ConNF.MainInduction.disjointNLs_small [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) : ConNF.Small (ConNF.MainInduction.disjointNLs S hS)

def ConNF.MainInduction.disjointSupport [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) : Set (ConNF.Address 0)

Equations

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

theorem ConNF.MainInduction.disjointSupport_small [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) : ConNF.Small (ConNF.MainInduction.disjointSupport S hS)

@[simp]

theorem ConNF.MainInduction.atom_mem_disjointSupport [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) (a : ConNF.Atom) : { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } ∈ ConNF.MainInduction.disjointSupport S hS ↔ a ∈ ConNF.MainInduction.interference S

@[simp]

theorem ConNF.MainInduction.nearLitter_mem_disjointSupport [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) (N : ConNF.NearLitter) : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ ConNF.MainInduction.disjointSupport S hS ↔ N ∈ ConNF.MainInduction.disjointNLs S hS

theorem ConNF.MainInduction.disjointSupport_supports [ConNF.Params] [ConNF.BasePositions] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) (c : ConNF.Address ↑0) (hc : c ∈ S) : MulAction.Supports (ConNF.Allowable ↑0) (let_fun this := ConNF.MainInduction.disjointSupport S hS; this) c

structure ConNF.MainInduction.DisjointSupport [ConNF.Params] (S : Set (ConNF.Address 0)) : Prop

• nearLitter : ∀ (N₁ N₂ : ConNF.NearLitter), { path := ConNF.MainInduction.zeroPath, value := Sum.inr N₁ } ∈ S → { path := ConNF.MainInduction.zeroPath, value := Sum.inr N₂ } ∈ S → N₁ = N₂ ∨ ↑N₁ ∩ ↑N₂ = ∅
• atom : ∀ (a : ConNF.Atom) (N : ConNF.NearLitter), { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } ∈ S → { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S → a ∉ N

theorem ConNF.MainInduction.DisjointSupport.nearLitter [ConNF.Params] {S : Set (ConNF.Address 0)} (self : ConNF.MainInduction.DisjointSupport S) (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter) (hN₁ : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N₁ } ∈ S) (hN₂ : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N₂ } ∈ S) : N₁ = N₂ ∨ ↑N₁ ∩ ↑N₂ = ∅

theorem ConNF.MainInduction.DisjointSupport.atom [ConNF.Params] {S : Set (ConNF.Address 0)} (self : ConNF.MainInduction.DisjointSupport S) (a : ConNF.Atom) (N : ConNF.NearLitter) (ha : { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } ∈ S) (hN : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S) : a ∉ N

theorem ConNF.MainInduction.disjointSupport_disjointSupport [ConNF.Params] (S : Set (ConNF.Address 0)) (hS : ConNF.Small S) : ConNF.MainInduction.DisjointSupport (ConNF.MainInduction.disjointSupport S hS)

theorem ConNF.MainInduction.disjointSupport_zeroStrong [ConNF.Params] (S : ConNF.Support 0) (hS : ConNF.MainInduction.DisjointSupport (ConNF.Enumeration.carrier S)) : ConNF.MainInduction.ZeroStrong S

theorem ConNF.MainInduction.zeroStrong_add [ConNF.Params] (S : ConNF.Support 0) (hS : ConNF.MainInduction.DisjointSupport (ConNF.Enumeration.carrier S)) (a : ConNF.Atom) : ConNF.MainInduction.ZeroStrong (S + ConNF.Enumeration.singleton { path := ConNF.MainInduction.zeroPath, value := Sum.inl a })

theorem ConNF.MainInduction.nearLitter_le_max_add [ConNF.Params] {S : ConNF.Support 0} {a : ConNF.Atom} {N : ConNF.NearLitter} {i : ConNF.κ} {hi : i < (S + ConNF.Enumeration.singleton { path := ConNF.MainInduction.zeroPath, value := Sum.inl a }).max} : (S + ConNF.Enumeration.singleton { path := ConNF.MainInduction.zeroPath, value := Sum.inl a }).f i hi = { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } → i < S.max

theorem ConNF.MainInduction.zeroStrong_spec_le [ConNF.Params] (S : ConNF.Support 0) (hS : ConNF.MainInduction.DisjointSupport (ConNF.Enumeration.carrier S)) (a : ConNF.Atom) (b : ConNF.Atom) (ha : { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } ∉ S) (hab : ∀ (N : ConNF.NearLitter), { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S → (a ∈ N ↔ b ∈ N)) : ConNF.MainInduction.zeroSpec (S + ConNF.Enumeration.singleton { path := ConNF.MainInduction.zeroPath, value := Sum.inl a }) ≤ ConNF.MainInduction.zeroSpec (S + ConNF.Enumeration.singleton { path := ConNF.MainInduction.zeroPath, value := Sum.inl b })

theorem ConNF.MainInduction.zeroStrong_spec_eq [ConNF.Params] (S : ConNF.Support 0) (hS : ConNF.MainInduction.DisjointSupport (ConNF.Enumeration.carrier S)) (a : ConNF.Atom) (b : ConNF.Atom) (ha : { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } ∉ S) (hb : { path := ConNF.MainInduction.zeroPath, value := Sum.inl b } ∉ S) (hab : ∀ (N : ConNF.NearLitter), { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S → (a ∈ N ↔ b ∈ N)) : ConNF.MainInduction.zeroSpec (S + ConNF.Enumeration.singleton { path := ConNF.MainInduction.zeroPath, value := Sum.inl a }) = ConNF.MainInduction.zeroSpec (S + ConNF.Enumeration.singleton { path := ConNF.MainInduction.zeroPath, value := Sum.inl b })

theorem ConNF.MainInduction.exists_swap [ConNF.Params] [ConNF.BasePositions] (S : Set (ConNF.Address ↑0)) (hS₁ : ConNF.Small S) (hS₂ : ConNF.MainInduction.DisjointSupport S) (a : ConNF.Atom) (b : ConNF.Atom) (ha : { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } ∉ S) (hb : { path := ConNF.MainInduction.zeroPath, value := Sum.inl b } ∉ S) (hab : ∀ (N : ConNF.NearLitter), { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S → (a ∈ N ↔ b ∈ N)) : ∃ (ρ : ConNF.Allowable ↑0), (∀ c ∈ S, ρ • c = c) ∧ ρ • a = b

In the following lemmas, e is the ⊥-extension of a 0-set.

theorem ConNF.MainInduction.mem_iff_mem_of_nearLitter_mem_disjointSupport [ConNF.Params] [ConNF.BasePositions] (S : Set (ConNF.Address ↑0)) (hS₁ : ConNF.Small S) (hS₂ : ConNF.MainInduction.DisjointSupport S) (e : Set ConNF.Atom) (heS : MulAction.Supports (ConNF.Allowable ↑0) S e) (N : ConNF.NearLitter) (hN : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S) (a : ConNF.Atom) (b : ConNF.Atom) (ha : a ∈ N) (hb : b ∈ N) : a ∈ e ↔ b ∈ e

theorem ConNF.MainInduction.mem_iff_mem_of_not_nearLitter_mem_disjointSupport [ConNF.Params] [ConNF.BasePositions] (S : Set (ConNF.Address ↑0)) (hS₁ : ConNF.Small S) (hS₂ : ConNF.MainInduction.DisjointSupport S) (e : Set ConNF.Atom) (heS : MulAction.Supports (ConNF.Allowable ↑0) S e) (a : ConNF.Atom) (b : ConNF.Atom) (haS : { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } ∉ S) (hbS : { path := ConNF.MainInduction.zeroPath, value := Sum.inl b } ∉ S) (ha : ∀ (N : ConNF.NearLitter), { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S → a ∉ N) (hb : ∀ (N : ConNF.NearLitter), { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S → b ∉ N) : a ∈ e ↔ b ∈ e

def ConNF.MainInduction.infoIn [ConNF.Params] (S : ConNF.Support 0) (e : Set ConNF.Atom) : Set ConNF.κ

Equations

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

def ConNF.MainInduction.infoOut [ConNF.Params] (S : ConNF.Support 0) (e : Set ConNF.Atom) : Prop

Equations

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

theorem ConNF.MainInduction.atom_mem_infoIn_iff [ConNF.Params] {S : ConNF.Support 0} {e : Set ConNF.Atom} {i : ConNF.κ} {hi : i < S.max} {a : ConNF.Atom} (ha : { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } = S.f i hi) : i ∈ ConNF.MainInduction.infoIn S e ↔ a ∈ e

theorem ConNF.MainInduction.nearLitter_mem_infoIn_iff [ConNF.Params] {S : ConNF.Support 0} {e : Set ConNF.Atom} {i : ConNF.κ} {hi : i < S.max} {N : ConNF.NearLitter} (hN : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } = S.f i hi) : i ∈ ConNF.MainInduction.infoIn S e ↔ ↑N ⊆ e

theorem ConNF.MainInduction.nearLitter_mem_infoIn_iff' [ConNF.Params] [ConNF.BasePositions] {S : ConNF.Support ↑0} (hS : ConNF.MainInduction.DisjointSupport (ConNF.Enumeration.carrier S)) {e : Set ConNF.Atom} (he : MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier S) e) {i : ConNF.κ} {hi : i < S.max} {N : ConNF.NearLitter} (hN : { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } = S.f i hi) : i ∈ ConNF.MainInduction.infoIn S e ↔ ∃ a ∈ N, a ∈ e

theorem ConNF.MainInduction.mk_outside [ConNF.Params] (S : ConNF.Support ↑0) : Cardinal.mk ↑({a : ConNF.Atom | { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } ∈ S} ∪ ⋃ N ∈ {N : ConNF.NearLitter | { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S}, ↑N) < Cardinal.mk ConNF.μ

theorem ConNF.MainInduction.exists_atom_outside [ConNF.Params] (S : ConNF.Support ↑0) : ∃ (a : ConNF.Atom), { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } ∉ S ∧ ∀ (N : ConNF.NearLitter), { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S → a ∉ N

theorem ConNF.MainInduction.infoOut_iff [ConNF.Params] [ConNF.BasePositions] {S : ConNF.Support ↑0} (hS : ConNF.MainInduction.DisjointSupport (ConNF.Enumeration.carrier S)) {e : Set ConNF.Atom} (he : MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier S) e) : ConNF.MainInduction.infoOut S e ↔ ∃ (a : ConNF.Atom), { path := ConNF.MainInduction.zeroPath, value := Sum.inl a } ∉ S ∧ (∀ (N : ConNF.NearLitter), { path := ConNF.MainInduction.zeroPath, value := Sum.inr N } ∈ S → a ∉ N) ∧ a ∈ e

theorem ConNF.MainInduction.info_injective' [ConNF.Params] [ConNF.BasePositions] (S : ConNF.Support ↑0) (hS : ConNF.MainInduction.DisjointSupport (ConNF.Enumeration.carrier S)) (e₁ : Set ConNF.Atom) (e₂ : Set ConNF.Atom) (h₁ : MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier S) e₁) (h₂ : MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier S) e₂) (hei : ConNF.MainInduction.infoIn S e₁ = ConNF.MainInduction.infoIn S e₂) (heo : ConNF.MainInduction.infoOut S e₁ ↔ ConNF.MainInduction.infoOut S e₂) : e₁ = e₂

def ConNF.MainInduction.info [ConNF.Params] [ConNF.BasePositions] (S : ConNF.Support ↑0) (e : { e : Set ConNF.Atom // MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier S) e }) : Set ConNF.κ × Prop

Equations

• ConNF.MainInduction.info S e = (ConNF.MainInduction.infoIn S ↑e, ConNF.MainInduction.infoOut S ↑e)

theorem ConNF.MainInduction.info_injective [ConNF.Params] [ConNF.BasePositions] (S : ConNF.Support ↑0) (hS : ConNF.MainInduction.DisjointSupport (ConNF.Enumeration.carrier S)) : Function.Injective (ConNF.MainInduction.info S)

def ConNF.MainInduction.zeroStrong [ConNF.Params] (S : Set (ConNF.Address 0)) : Set (ConNF.Address 0)

Equations

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

theorem ConNF.MainInduction.zeroStrong_small [ConNF.Params] {S : Set (ConNF.Address 0)} (hS : ConNF.Small S) : ConNF.Small (ConNF.MainInduction.zeroStrong S)

theorem ConNF.MainInduction.zeroStrong_zeroStrong [ConNF.Params] (S : ConNF.Support 0) : ConNF.MainInduction.ZeroStrong (ConNF.Enumeration.ofSet (ConNF.MainInduction.zeroStrong (ConNF.Enumeration.carrier S)) ⋯)

theorem ConNF.MainInduction.subset_zeroStrong [ConNF.Params] (S : ConNF.Support 0) : ConNF.Enumeration.carrier S ⊆ (ConNF.Enumeration.ofSet (ConNF.MainInduction.zeroStrong (ConNF.Enumeration.carrier S)) ⋯).carrier

theorem ConNF.MainInduction.exists_hom_zeroStrong [ConNF.Params] (S : ConNF.Support 0) : Nonempty (ConNF.SupportHom S (ConNF.Enumeration.ofSet (ConNF.MainInduction.zeroStrong (ConNF.Enumeration.carrier S)) ⋯))

structure ConNF.MainInduction.WeakZeroSpec [ConNF.Params] : Type u

• max : ConNF.κ
• f : ConNF.κ → ConNF.κ
• σ : ConNF.MainInduction.ZeroSpec

def ConNF.MainInduction.WeakZeroSpec.Specifies [ConNF.Params] (W : ConNF.MainInduction.WeakZeroSpec) (S : ConNF.Support 0) : Prop

Equations

• W.Specifies S = ∃ (T : ConNF.Support 0) (F : ConNF.SupportHom S T), ConNF.MainInduction.ZeroStrong T ∧ W.max = S.max ∧ W.f = F.f ∧ W.σ = ConNF.MainInduction.zeroSpec T

theorem ConNF.MainInduction.hasWeakZeroSpec [ConNF.Params] (S : ConNF.Support 0) : ∃ (W : ConNF.MainInduction.WeakZeroSpec), W.Specifies S

theorem ConNF.MainInduction.orbit_eq_of_weakSpec_eq [ConNF.Params] [ConNF.BasePositions] (S : ConNF.Support ↑0) (T : ConNF.Support ↑0) (W : ConNF.MainInduction.WeakZeroSpec) (hS : W.Specifies S) (hT : W.Specifies T) : ConNF.SupportOrbit.mk S = ConNF.SupportOrbit.mk T

noncomputable def ConNF.MainInduction.weakZeroSpec [ConNF.Params] [ConNF.BasePositions] (o : ConNF.SupportOrbit 0) : ConNF.MainInduction.WeakZeroSpec

Equations

• ConNF.MainInduction.weakZeroSpec o = ⋯.choose

noncomputable def ConNF.MainInduction.weakZeroSpec_specifies [ConNF.Params] [ConNF.BasePositions] (o : ConNF.SupportOrbit 0) : (ConNF.MainInduction.weakZeroSpec o).Specifies o.out

Equations

• ⋯ = ⋯

theorem ConNF.MainInduction.weakZeroSpec_injective [ConNF.Params] [ConNF.BasePositions] : Function.Injective ConNF.MainInduction.weakZeroSpec

theorem ConNF.MainInduction.mk_supportOrbit_zero_le' [ConNF.Params] [ConNF.BasePositions] : Cardinal.mk (ConNF.SupportOrbit 0) ≤ Cardinal.mk ConNF.MainInduction.WeakZeroSpec

def ConNF.MainInduction.WeakZeroSpec.decompose [ConNF.Params] (W : ConNF.MainInduction.WeakZeroSpec) : ConNF.κ × (ConNF.κ → ConNF.κ) × ConNF.MainInduction.ZeroSpec

Equations

• W.decompose = (W.max, W.f, W.σ)

theorem ConNF.MainInduction.WeakZeroSpec.decompose_injective [ConNF.Params] : Function.Injective ConNF.MainInduction.WeakZeroSpec.decompose

theorem ConNF.MainInduction.mk_supportOrbit_zero_le [ConNF.Params] [ConNF.BasePositions] : Cardinal.mk (ConNF.SupportOrbit 0) < Cardinal.mk ConNF.μ

def ConNF.MainInduction.zeroExtension' [ConNF.Params] [ConNF.BasePositions] {members : ConNF.Extensions} : ConNF.ExtensionalSet.Preference members → Set ConNF.Atom

Equations

• ConNF.MainInduction.zeroExtension' x = match x with | ConNF.ExtensionalSet.Preference.base atoms a => atoms | ConNF.ExtensionalSet.Preference.proper γ a a_1 => ⋯.elim

def ConNF.MainInduction.zeroExtension [ConNF.Params] [ConNF.BasePositions] (t : ConNF.NewTSet) : Set ConNF.Atom

Equations

• ConNF.MainInduction.zeroExtension t = ConNF.MainInduction.zeroExtension' (↑t).pref

theorem ConNF.MainInduction.zeroExtension_injective [ConNF.Params] [ConNF.BasePositions] : Function.Injective ConNF.MainInduction.zeroExtension

theorem ConNF.MainInduction.zeroExtension_smul [ConNF.Params] [ConNF.BasePositions] (t : ConNF.NewTSet) (ρ : ConNF.Allowable ↑0) : ConNF.MainInduction.zeroExtension (ρ • t) = ρ • ConNF.MainInduction.zeroExtension t

theorem ConNF.MainInduction.supports_zeroExtension [ConNF.Params] [ConNF.BasePositions] (S : ConNF.Support ↑0) (t : ConNF.NewTSet) (h : MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier S) t) : MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier S) (ConNF.MainInduction.zeroExtension t)

theorem ConNF.MainInduction.mk_supports_disjoint [ConNF.Params] [ConNF.BasePositions] (S : ConNF.Support ↑0) (hS : ConNF.MainInduction.DisjointSupport (ConNF.Enumeration.carrier S)) : Cardinal.mk ↑{e : Set ConNF.Atom | MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier S) e} ≤ 2 ^ Cardinal.mk ConNF.κ

theorem ConNF.MainInduction.mk_supports' [ConNF.Params] [ConNF.BasePositions] (S : ConNF.Support ↑0) : Cardinal.mk ↑{e : Set ConNF.Atom | MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier S) e} ≤ 2 ^ Cardinal.mk ConNF.κ

theorem ConNF.MainInduction.mk_supports [ConNF.Params] [ConNF.BasePositions] (S : ConNF.Support ↑0) : Cardinal.mk ↑{t : ConNF.NewTSet | MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier S) t} ≤ 2 ^ Cardinal.mk ConNF.κ

noncomputable def ConNF.MainInduction.codeSurjection [ConNF.Params] [ConNF.BasePositions] (x : (o : ConNF.SupportOrbit 0) × ↑{t : ConNF.NewTSet | MulAction.Supports (ConNF.Allowable ↑0) (ConNF.Enumeration.carrier o.out) t}) : ConNF.CodingFunction 0

Equations

• ConNF.MainInduction.codeSurjection x = ConNF.CodingFunction.code x.fst.out ↑x.snd ⋯

theorem ConNF.MainInduction.codeSurjection_surjective [ConNF.Params] [ConNF.BasePositions] : Function.Surjective ConNF.MainInduction.codeSurjection

theorem ConNF.MainInduction.mk_codingFunction_zero_le [ConNF.Params] [ConNF.BasePositions] : Cardinal.mk (ConNF.CodingFunction 0) < Cardinal.mk ConNF.μ