Construction of model data

In this file, we construct model data at type α, given that it is defined at all types below α.

Main declarations

• ConNF.foo: Something new.

structure ConNF.NewPerm [ConNF.Params] [ConNF.Level] [ConNF.LtData] : Type u

• sderiv : (β : ConNF.TypeIndex) → [inst : ConNF.LtLevel β] → ConNF.AllPerm β
• smul_fuzz' : ∀ {β : ConNF.TypeIndex} {γ : ConNF.Λ} [inst : ConNF.LtLevel β] [inst_1 : ConNF.LtLevel ↑γ] (hβγ : β ≠ ↑γ) (t : ConNF.Tangle β), (self.sderiv ↑γ)ᵁ ↘. • ConNF.fuzz hβγ t = ConNF.fuzz hβγ (self.sderiv β • t)

theorem ConNF.NewPerm.ext {inst✝ : ConNF.Params} {inst✝¹ : ConNF.Level} {inst✝² : ConNF.LtData} {x y : ConNF.NewPerm} (sderiv : x.sderiv = y.sderiv) : x = y

instance ConNF.instMulNewPerm [ConNF.Params] [ConNF.Level] [ConNF.LtData] : Mul ConNF.NewPerm

Equations

• ConNF.instMulNewPerm = { mul := fun (ρ₁ ρ₂ : ConNF.NewPerm) => { sderiv := fun (β : ConNF.TypeIndex) (x : ConNF.LtLevel β) => ρ₁.sderiv β * ρ₂.sderiv β, smul_fuzz' := ⋯ } }

instance ConNF.instOneNewPerm [ConNF.Params] [ConNF.Level] [ConNF.LtData] : One ConNF.NewPerm

Equations

• ConNF.instOneNewPerm = { one := { sderiv := fun (x : ConNF.TypeIndex) (x_1 : ConNF.LtLevel x) => 1, smul_fuzz' := ⋯ } }

instance ConNF.instInvNewPerm [ConNF.Params] [ConNF.Level] [ConNF.LtData] : Inv ConNF.NewPerm

Equations

• ConNF.instInvNewPerm = { inv := fun (ρ : ConNF.NewPerm) => { sderiv := fun (β : ConNF.TypeIndex) (x : ConNF.LtLevel β) => (ρ.sderiv β)⁻¹, smul_fuzz' := ⋯ } }

@[simp]

theorem ConNF.mul_sderiv [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ₁ ρ₂ : ConNF.NewPerm) (β : ConNF.TypeIndex) [ConNF.LtLevel β] : (ρ₁ * ρ₂).sderiv β = ρ₁.sderiv β * ρ₂.sderiv β

@[simp]

theorem ConNF.one_sderiv [ConNF.Params] [ConNF.Level] [ConNF.LtData] (β : ConNF.TypeIndex) [ConNF.LtLevel β] : ConNF.NewPerm.sderiv 1 β = 1

@[simp]

theorem ConNF.inv_sderiv [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.NewPerm) (β : ConNF.TypeIndex) [ConNF.LtLevel β] : ρ⁻¹.sderiv β = (ρ.sderiv β)⁻¹

instance ConNF.instGroupNewPerm [ConNF.Params] [ConNF.Level] [ConNF.LtData] : Group ConNF.NewPerm

Equations

• ConNF.instGroupNewPerm = Group.mk ⋯

instance ConNF.instSMulNewPermCode [ConNF.Params] [ConNF.Level] [ConNF.LtData] : SMul ConNF.NewPerm ConNF.Code

Equations

• ConNF.instSMulNewPermCode = { smul := fun (ρ : ConNF.NewPerm) (c : ConNF.Code) => ConNF.Code.mk c.β (ρ.sderiv c.β • c.s) ⋯ }

@[simp]

theorem ConNF.NewPerm.smul_mk [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.NewPerm) (β : ConNF.TypeIndex) [ConNF.LtLevel β] (s : Set (ConNF.TSet β)) (hs : s.Nonempty) : ρ • ConNF.Code.mk β s hs = ConNF.Code.mk β (ρ.sderiv β • s) ⋯

instance ConNF.instMulActionNewPermCode [ConNF.Params] [ConNF.Level] [ConNF.LtData] : MulAction ConNF.NewPerm ConNF.Code

Equations

• ConNF.instMulActionNewPermCode = MulAction.mk ⋯ ⋯

theorem ConNF.Cloud.smul [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c d : ConNF.Code} (h : ConNF.Cloud c d) (ρ : ConNF.NewPerm) : ConNF.Cloud (ρ • c) (ρ • d)

@[simp]

theorem ConNF.Code.smul_even [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c : ConNF.Code} (ρ : ConNF.NewPerm) : (ρ • c).Even ↔ c.Even

theorem ConNF.Represents.smul [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c d : ConNF.Code} (h : ConNF.Represents c d) (ρ : ConNF.NewPerm) : ConNF.Represents (ρ • c) (ρ • d)

@[simp]

theorem ConNF.NewPerm.smul_members [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.NewPerm) (c : ConNF.Code) (β : ConNF.TypeIndex) [ConNF.LtLevel β] : (ρ • c).members β = ρ.sderiv β • c.members β

instance ConNF.instSuperUNewPermStrPermSomeΛα [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.SuperU ConNF.NewPerm (ConNF.StrPerm ↑ConNF.α)

Equations

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

theorem ConNF.NewPerm.forget_def [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.NewPerm) (A : ↑ConNF.α ↝ ⊥) : ρᵁ A = ConNF.Path.recScoderiv (motive := fun (β : ConNF.TypeIndex) (x : β ↝ ⊥) => β ≠ ⊥ → β ≤ ↑ConNF.α → ConNF.BasePerm) (fun (h : ⊥ ≠ ⊥) => ⋯.elim) (fun (_β γ : ConNF.TypeIndex) (B : γ ↝ ⊥) (hγβ : γ < _β) (x : (fun (β : ConNF.TypeIndex) (x : β ↝ ⊥) => β ≠ ⊥ → β ≤ ↑ConNF.α → ConNF.BasePerm) γ B) (x : _β ≠ ⊥) (hβα : _β ≤ ↑ConNF.α) => (ρ.sderiv γ)ᵁ B) A ⋯ ⋯

@[simp]

theorem ConNF.NewPerm.forget_sderiv [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.NewPerm) (β : ConNF.TypeIndex) [ConNF.LtLevel β] : ρᵁ ↘ ⋯ = (ρ.sderiv β)ᵁ

theorem ConNF.NewPerm.smul_fuzz [ConNF.Params] [ConNF.Level] [ConNF.LtData] {β : ConNF.TypeIndex} {γ : ConNF.Λ} [ConNF.LtLevel β] [ConNF.LtLevel ↑γ] (ρ : ConNF.NewPerm) (hβγ : β ≠ ↑γ) (t : ConNF.Tangle β) : ρᵁ ↘ ⋯ ↘. • ConNF.fuzz hβγ t = ConNF.fuzz hβγ (ρ.sderiv β • t)

@[simp]

theorem ConNF.NewPerm.forget_mul [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ₁ ρ₂ : ConNF.NewPerm) : (ρ₁ * ρ₂)ᵁ = ρ₁ᵁ * ρ₂ᵁ

@[simp]

theorem ConNF.NewPerm.forget_one [ConNF.Params] [ConNF.Level] [ConNF.LtData] : 1ᵁ = 1

@[simp]

theorem ConNF.NewPerm.forget_inv [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.NewPerm) : ρ⁻¹ᵁ = ρᵁ⁻¹

structure ConNF.NewSet [ConNF.Params] [ConNF.Level] [ConNF.LtData] : Type u

• c : ConNF.Code
• hc : self.c.Even
• hS : ∃ (S : ConNF.Support ↑ConNF.α), ∀ (ρ : ConNF.NewPerm), ρᵁ • S = S → ρ • self.c = self.c

theorem ConNF.NewSet.ext {inst✝ : ConNF.Params} {inst✝¹ : ConNF.Level} {inst✝² : ConNF.LtData} {x y : ConNF.NewSet} (c : x.c = y.c) : x = y

instance ConNF.instSuperUNewSetStrSetSomeΛα [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.SuperU ConNF.NewSet (ConNF.StrSet ↑ConNF.α)

Equations

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

theorem ConNF.NewSet.forget_def [ConNF.Params] [ConNF.Level] [ConNF.LtData] (x : ConNF.NewSet) : xᵁ = ConNF.StrSet.coeEquiv.symm fun (β : ConNF.TypeIndex) (hβ : β < ↑ConNF.α) => (fun (x : ConNF.TSet β) => xᵁ) '' x.c.members β

theorem ConNF.NewSet.typedMem_forget [ConNF.Params] [ConNF.Level] [ConNF.LtData] (x : ConNF.NewSet) (β : ConNF.TypeIndex) (hβ : β < ↑ConNF.α) (y : ConNF.StrSet β) : y ∈[hβ] xᵁ ↔ y ∈ (fun (x : ConNF.TSet β) => xᵁ) '' x.c.members β

theorem ConNF.NewSet.mem_members [ConNF.Params] [ConNF.Level] [ConNF.LtData] (x : ConNF.NewSet) (β : ConNF.TypeIndex) [hβ : ConNF.LtLevel β] (y : ConNF.TSet β) : y ∈ x.c.members β ↔ yᵁ ∈[⋯] xᵁ

instance ConNF.instSMulNewPermNewSet [ConNF.Params] [ConNF.Level] [ConNF.LtData] : SMul ConNF.NewPerm ConNF.NewSet

Equations

• ConNF.instSMulNewPermNewSet = { smul := fun (ρ : ConNF.NewPerm) (x : ConNF.NewSet) => { c := ρ • x.c, hc := ⋯, hS := ⋯ } }

@[simp]

theorem ConNF.NewSet.smul_c [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.NewPerm) (x : ConNF.NewSet) : (ρ • x).c = ρ • x.c

instance ConNF.instMulActionNewPermNewSet [ConNF.Params] [ConNF.Level] [ConNF.LtData] : MulAction ConNF.NewPerm ConNF.NewSet

Equations

• ConNF.instMulActionNewPermNewSet = MulAction.mk ⋯ ⋯

def ConNF.newPreModelData [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.PreModelData ↑ConNF.α

Equations

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

@[simp]

theorem ConNF.newPreModelData.tSetForget_none [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.PreModelData.tSetForget none = ConNF.StrSet.coeEquiv.symm fun (x : ConNF.TypeIndex) (x_1 : x < ↑ConNF.α) => ∅

@[simp]

theorem ConNF.newPreModelData.tSetForget_some [ConNF.Params] [ConNF.Level] [ConNF.LtData] (x : ConNF.NewSet) : ConNF.PreModelData.tSetForget (some x) = xᵁ

@[simp]

theorem ConNF.newPreModelData.tSetForget_none' [ConNF.Params] [ConNF.Level] [ConNF.LtData] : (let_fun this := none; this)ᵁ = ConNF.StrSet.coeEquiv.symm fun (x : ConNF.TypeIndex) (x_1 : x < ↑ConNF.α) => ∅

@[simp]

theorem ConNF.newPreModelData.tSetForget_some' [ConNF.Params] [ConNF.Level] [ConNF.LtData] (x : ConNF.NewSet) : (let_fun this := some x; this)ᵁ = xᵁ

theorem ConNF.NewPerm.forget_injective [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ₁ ρ₂ : ConNF.NewPerm) (h : ρ₁ᵁ = ρ₂ᵁ) : ρ₁ = ρ₂

theorem ConNF.NewSet.forget_injective [ConNF.Params] [ConNF.Level] [ConNF.LtData] (x y : ConNF.NewSet) (h : xᵁ = yᵁ) : x = y

theorem ConNF.NewPerm.smul_forget [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.NewPerm) (x : ConNF.NewSet) : (ρ • x)ᵁ = ρᵁ • xᵁ

theorem ConNF.NewSet.exists_support [ConNF.Params] [ConNF.Level] [ConNF.LtData] (x : ConNF.TSet ↑ConNF.α) : ∃ (S : ConNF.Support ↑ConNF.α), S.Supports x

theorem ConNF.NewSet.coe_ne_empty [ConNF.Params] [ConNF.Level] [ConNF.LtData] (x : ConNF.NewSet) : xᵁ ≠ ConNF.StrSet.coeEquiv.symm fun (x : ConNF.TypeIndex) (x_1 : x < ↑ConNF.α) => ∅

def ConNF.newModelData [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.ModelData ↑ConNF.α

Equations

• ConNF.newModelData = ConNF.ModelData.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem ConNF.Code.hasSet [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) (hc : ∃ (S : ConNF.Support ↑ConNF.α), ∀ (ρ : ConNF.NewPerm), ρᵁ • S = S → ρ • c = c) : ∃ (x : ConNF.NewSet), ConNF.Represents x.c c

def ConNF.Code.toSet [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) (hc : ∃ (S : ConNF.Support ↑ConNF.α), ∀ (ρ : ConNF.NewPerm), ρᵁ • S = S → ρ • c = c) : ConNF.NewSet

Equations

• c.toSet hc = ⋯.choose

theorem ConNF.Code.toSet_spec [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) (hc : ∃ (S : ConNF.Support ↑ConNF.α), ∀ (ρ : ConNF.NewPerm), ρᵁ • S = S → ρ • c = c) : ConNF.Represents (c.toSet hc).c c

theorem ConNF.Code.mem_toSet' [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) {hc : ∃ (S : ConNF.Support ↑ConNF.α), ∀ (ρ : ConNF.NewPerm), ρᵁ • S = S → ρ • c = c} (y : ConNF.TSet c.β) : yᵁ ∈[⋯] (c.toSet hc)ᵁ ↔ y ∈ c.s

theorem ConNF.Code.mem_toSet [ConNF.Params] [ConNF.Level] [ConNF.LtData] {β : ConNF.TypeIndex} [ConNF.LtLevel β] {s : Set (ConNF.TSet β)} {hs : s.Nonempty} {hc : ∃ (S : ConNF.Support ↑ConNF.α), ∀ (ρ : ConNF.NewPerm), ρᵁ • S = S → ρ • ConNF.Code.mk β s hs = ConNF.Code.mk β s hs} (y : ConNF.TSet β) : yᵁ ∈[⋯] ((ConNF.Code.mk β s hs).toSet hc)ᵁ ↔ y ∈ s

theorem ConNF.NearLitter.code_aux [ConNF.Params] [ConNF.Level] [ConNF.LtData] {N : ConNF.NearLitter} : {x : ConNF.TSet ⊥ | ConNF.StrSet.botEquiv xᵁ ∈ Nᴬ}.Nonempty

def ConNF.NearLitter.code [ConNF.Params] [ConNF.Level] [ConNF.LtData] (N : ConNF.NearLitter) : ConNF.Code

Equations

• N.code = ConNF.Code.mk ⊥ {x : ConNF.TSet ⊥ | ConNF.StrSet.botEquiv xᵁ ∈ Nᴬ} ⋯

theorem ConNF.NearLitter.smul_code [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.NewPerm) (N : ConNF.NearLitter) : ρ • N.code = (ρᵁ ↘. • N).code

theorem ConNF.newTyped_aux [ConNF.Params] [ConNF.Level] [ConNF.LtData] {N : ConNF.NearLitter} : ∃ (S : ConNF.Support ↑ConNF.α), ∀ (ρ : ConNF.NewPerm), ρᵁ • S = S → ρ • N.code = N.code

def ConNF.newTyped [ConNF.Params] [ConNF.Level] [ConNF.LtData] (N : ConNF.NearLitter) : ConNF.NewSet

Equations

• ConNF.newTyped N = N.code.toSet ⋯

theorem ConNF.newTyped_c_eq [ConNF.Params] [ConNF.Level] [ConNF.LtData] (N : ConNF.NearLitter) : (ConNF.newTyped N).c = N.code

theorem ConNF.mem_newTyped_iff [ConNF.Params] [ConNF.Level] [ConNF.LtData] (a : ConNF.TSet ⊥) (N : ConNF.NearLitter) : aᵁ ∈[⋯] (ConNF.newTyped N)ᵁ ↔ ConNF.StrSet.botEquiv aᵁ ∈ Nᴬ

theorem ConNF.newTyped_injective [ConNF.Params] [ConNF.Level] [ConNF.LtData] : Function.Injective ConNF.newTyped

theorem ConNF.smul_newTyped [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.NewPerm) (N : ConNF.NearLitter) : ρ • ConNF.newTyped N = ConNF.newTyped (ρᵁ ↘. • N)

def ConNF.newSingletonCode [ConNF.Params] [ConNF.Level] [ConNF.LtData] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] (x : ConNF.TSet ↑γ) : ConNF.Code

Equations

• ConNF.newSingletonCode x = ConNF.Code.mk ↑γ {x} ⋯

theorem ConNF.newSingleton_aux [ConNF.Params] [ConNF.Level] [ConNF.LtData] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] {x : ConNF.TSet ↑γ} : ∃ (S : ConNF.Support ↑ConNF.α), ∀ (ρ : ConNF.NewPerm), ρᵁ • S = S → ρ • ConNF.newSingletonCode x = ConNF.newSingletonCode x

def ConNF.newSingleton [ConNF.Params] [ConNF.Level] [ConNF.LtData] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] (x : ConNF.TSet ↑γ) : ConNF.NewSet

Equations

• ConNF.newSingleton x = (ConNF.newSingletonCode x).toSet ⋯

def ConNF.instModelDataSomeΛα [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.ModelData ↑ConNF.α

Equations

• ConNF.instModelDataSomeΛα = ConNF.newModelData

theorem ConNF.mem_none_iff [ConNF.Params] [ConNF.Level] [ConNF.LtData] {β : ConNF.TypeIndex} [ConNF.LtLevel β] (y : ConNF.TSet β) : (y ∈[⋯] let_fun this := none; this) ↔ yᵁ ∈[⋯] ConNF.StrSet.coeEquiv.symm fun (x : ConNF.TypeIndex) (x_1 : x < ↑ConNF.α) => ∅

theorem ConNF.mem_some_iff [ConNF.Params] [ConNF.Level] [ConNF.LtData] {β : ConNF.TypeIndex} [ConNF.LtLevel β] (y : ConNF.TSet β) (x : ConNF.NewSet) : (y ∈[⋯] let_fun this := some x; this) ↔ yᵁ ∈[⋯] xᵁ

theorem ConNF.mem_newSingleton_iff [ConNF.Params] [ConNF.Level] [ConNF.LtData] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] (x y : ConNF.TSet ↑γ) : (y ∈[⋯] let_fun this := some (ConNF.newSingleton x); this) ↔ y = x

theorem ConNF.not_mem_none [ConNF.Params] [ConNF.Level] [ConNF.LtData] {β : ConNF.TypeIndex} [ConNF.LtLevel β] (z : ConNF.TSet β) : ¬z ∈[⋯] let_fun this := none; this

theorem ConNF.newModelData_ext [ConNF.Params] [ConNF.Level] [ConNF.LtData] (β : ConNF.Λ) [ConNF.LtLevel ↑β] (x y : ConNF.TSet ↑ConNF.α) (h : ∀ (z : ConNF.TSet ↑β), z ∈[⋯] x ↔ z ∈[⋯] y) : x = y

def ConNF.newPositionDeny [ConNF.Params] [ConNF.Level] [ConNF.LtData] (t : ConNF.Tangle ↑ConNF.α) : Set ConNF.μ

Equations

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

theorem ConNF.card_newPositionDeny [ConNF.Params] [ConNF.Level] [ConNF.LtData] (t : ConNF.Tangle ↑ConNF.α) : Cardinal.mk ↑(ConNF.newPositionDeny t) < (Cardinal.mk ConNF.μ).ord.cof

def ConNF.newPosition [ConNF.Params] [ConNF.Level] [ConNF.LtData] (h : Cardinal.mk (ConNF.Tangle ↑ConNF.α) ≤ Cardinal.mk ConNF.μ) : ConNF.Position (ConNF.Tangle ↑ConNF.α)

Equations

• ConNF.newPosition h = { pos := { toFun := ConNF.funOfDeny h ConNF.newPositionDeny ⋯, inj' := ⋯ } }

theorem ConNF.pos_atom_lt_newPosition [ConNF.Params] [ConNF.Level] [ConNF.LtData] (h : Cardinal.mk (ConNF.Tangle ↑ConNF.α) ≤ Cardinal.mk ConNF.μ) (t : ConNF.Tangle ↑ConNF.α) (a : ConNF.Atom) (A : ↑ConNF.α ↝ ⊥) (ha : a ∈ (t.support ⇘. A)ᴬ) : ConNF.pos a < ConNF.pos t

theorem ConNF.pos_nearLitter_lt_newPosition [ConNF.Params] [ConNF.Level] [ConNF.LtData] (h : Cardinal.mk (ConNF.Tangle ↑ConNF.α) ≤ Cardinal.mk ConNF.μ) (t : ConNF.Tangle ↑ConNF.α) (N : ConNF.NearLitter) (A : ↑ConNF.α ↝ ⊥) (hN : N ∈ (t.support ⇘. A)ᴺ) : ConNF.pos N < ConNF.pos t

theorem ConNF.pos_le_pos_of_typed [ConNF.Params] [ConNF.Level] [ConNF.LtData] (h : Cardinal.mk (ConNF.Tangle ↑ConNF.α) ≤ Cardinal.mk ConNF.μ) (N : ConNF.NearLitter) (t : ConNF.Tangle ↑ConNF.α) (ht : t.set = some (ConNF.newTyped N)) : ConNF.pos N ≤ ConNF.pos t

theorem ConNF.smul_newTyped' [ConNF.Params] [ConNF.Level] [ConNF.LtData] (ρ : ConNF.AllPerm ↑ConNF.α) (N : ConNF.NearLitter) : (ρ • let_fun this := some (ConNF.newTyped N); this) = some (ConNF.newTyped (ρᵁ ↘. • N))

def ConNF.newTypedNearLitters [ConNF.Params] [ConNF.Level] [ConNF.LtData] (h : Cardinal.mk (ConNF.Tangle ↑ConNF.α) ≤ Cardinal.mk ConNF.μ) : ConNF.TypedNearLitters ConNF.α

Equations

• ConNF.newTypedNearLitters h = { typed := some ∘ ConNF.newTyped, typed_injective := ⋯, pos_le_pos_of_typed := ⋯, smul_typed := ⋯ }