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 [Params] [Level] [LtData] : Type u

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

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ConNF.instGroupNewPerm = Group.mk ⋯

instance ConNF.instSMulNewPermCode [Params] [Level] [LtData] : SMul NewPerm 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 [Params] [Level] [LtData] (ρ : NewPerm) (β : TypeIndex) [LtLevel β] (s : Set (TSet β)) (hs : s.Nonempty) : ρ • Code.mk β s hs = Code.mk β (ρ.sderiv β • s) ⋯

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

Equations

• ConNF.instMulActionNewPermCode = MulAction.mk ⋯ ⋯

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

@[simp]

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

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

@[simp]

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

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

Equations

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

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

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

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

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

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

Equations

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

@[simp]

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

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

Equations

• ConNF.instMulActionNewPermNewSet = MulAction.mk ⋯ ⋯

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

Equations

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

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

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

Equations

• c.toSet hc = ⋯.choose

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

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

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

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

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

Equations

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

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

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

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

Equations

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

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

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

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

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

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

Equations

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

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

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

Equations

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

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

Equations

• ConNF.instModelDataSomeΛα = ConNF.newModelData

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

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

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

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

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

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

Equations

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

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

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

Equations

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

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

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

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

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

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

Equations

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