Codes

In this file, we define codes and clouds.

Main declarations

• ConNF.foo: Something new.

class ConNF.TypedNearLitters [ConNF.Params] (α : ConNF.Λ) [ConNF.ModelData ↑α] [ConNF.Position (ConNF.Tangle ↑α)] : Type u

• typed : ConNF.NearLitter → ConNF.TSet ↑α
• typed_injective : Function.Injective ConNF.typed
• pos_le_pos_of_typed : ∀ (N : ConNF.NearLitter) (t : ConNF.Tangle ↑α), t.set = ConNF.typed N → ConNF.pos N ≤ ConNF.pos t
• smul_typed : ∀ (ρ : ConNF.AllPerm ↑α) (N : ConNF.NearLitter), ρ • ConNF.typed N = ConNF.typed (ρᵁ ↘. • N)

class ConNF.LtData [ConNF.Params] [ConNF.Level] : Type (u + 1)

• data : (β : ConNF.TypeIndex) → [inst : ConNF.LtLevel β] → ConNF.ModelData β
• positions : (β : ConNF.TypeIndex) → [inst : ConNF.LtLevel β] → ConNF.Position (ConNF.Tangle β)
• typedNearLitters : (β : ConNF.Λ) → [inst : ConNF.LtLevel ↑β] → ConNF.TypedNearLitters β

theorem ConNF.LtData.ext {inst✝ : ConNF.Params} {inst✝¹ : ConNF.Level} {x y : ConNF.LtData} (data : ConNF.LtData.data = ConNF.LtData.data) (positions : HEq ConNF.LtData.positions ConNF.LtData.positions) (typedNearLitters : HEq ConNF.LtData.typedNearLitters ConNF.LtData.typedNearLitters) : x = y

instance ConNF.instModelDataOfLtDataOfLtLevel [ConNF.Params] [ConNF.Level] [ConNF.LtData] (β : ConNF.TypeIndex) [ConNF.LtLevel β] : ConNF.ModelData β

Equations

• ConNF.instModelDataOfLtDataOfLtLevel = ConNF.LtData.data

instance ConNF.instPositionTangle_1 [ConNF.Params] [ConNF.Level] [ConNF.LtData] (β : ConNF.TypeIndex) [ConNF.LtLevel β] : ConNF.Position (ConNF.Tangle β)

Equations

• ConNF.instPositionTangle_1 = ConNF.LtData.positions

instance ConNF.instTypedNearLitters [ConNF.Params] [ConNF.Level] [ConNF.LtData] (β : ConNF.Λ) [ConNF.LtLevel ↑β] : ConNF.TypedNearLitters β

Equations

• ConNF.instTypedNearLitters = ConNF.LtData.typedNearLitters

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

• β : ConNF.TypeIndex
• hβ : ConNF.LtLevel self.β
• s : Set (ConNF.TSet self.β)
• hs : self.s.Nonempty

theorem ConNF.instLtLevelβ [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) : ConNF.LtLevel c.β

theorem ConNF.cloud_aux [ConNF.Params] [ConNF.Level] [ConNF.LtData] (β : ConNF.TypeIndex) [ConNF.LtLevel β] (γ : ConNF.Λ) [ConNF.LtLevel ↑γ] (hβγ : β ≠ ↑γ) (s : Set (ConNF.TSet β)) (hs : s.Nonempty) : (ConNF.typed '' {N : ConNF.NearLitter | ∃ (t : ConNF.Tangle β), t.set ∈ s ∧ Nᴸ = ConNF.fuzz hβγ t}).Nonempty

inductive ConNF.Cloud [ConNF.Params] [ConNF.Level] [ConNF.LtData] : Rel ConNF.Code ConNF.Code

• mk: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.LtData] (β : ConNF.TypeIndex) [inst_3 : ConNF.LtLevel β] (γ : ConNF.Λ) [inst_4 : ConNF.LtLevel ↑γ] (hβγ : β ≠ ↑γ) (s : Set (ConNF.TSet β)) (hs : s.Nonempty), ConNF.Cloud (ConNF.Code.mk β s hs) (ConNF.Code.mk (↑γ) (ConNF.typed '' {N : ConNF.NearLitter | ∃ (t : ConNF.Tangle β), t.set ∈ s ∧ Nᴸ = ConNF.fuzz hβγ t}) ⋯)

theorem ConNF.eq_coe_of_cloud [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c d : ConNF.Code} (h : ConNF.Cloud c d) : ∃ (γ : ConNF.Λ) (x : ConNF.LtLevel ↑γ) (s : Set (ConNF.TSet ↑γ)) (hs : s.Nonempty), d = ConNF.Code.mk (↑γ) s hs

theorem ConNF.cloud_mk_iff [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) (γ : ConNF.Λ) [ConNF.LtLevel ↑γ] (s : Set (ConNF.TSet ↑γ)) (hs : s.Nonempty) : ConNF.Cloud c (ConNF.Code.mk (↑γ) s hs) ↔ ∃ (hβγ : c.β ≠ ↑γ), s = ConNF.typed '' {N : ConNF.NearLitter | ∃ (t : ConNF.Tangle c.β), t.set ∈ c.s ∧ Nᴸ = ConNF.fuzz hβγ t}

theorem ConNF.subset_of_cloud [ConNF.Params] [ConNF.Level] [ConNF.LtData] {β : ConNF.TypeIndex} {γ : ConNF.Λ} [ConNF.LtLevel β] [ConNF.LtLevel ↑γ] {hβγ : β ≠ ↑γ} {s₁ s₂ : Set (ConNF.TSet β)} (h : {N : ConNF.NearLitter | ∃ (t : ConNF.Tangle β), t.set ∈ s₁ ∧ Nᴸ = ConNF.fuzz hβγ t} = {N : ConNF.NearLitter | ∃ (t : ConNF.Tangle β), t.set ∈ s₂ ∧ Nᴸ = ConNF.fuzz hβγ t}) : s₁ ⊆ s₂

theorem ConNF.cloud_injective [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.Cloud.Injective

def ConNF.Code.positions [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) : Set ConNF.μ

Equations

• c.positions = ⇑ConNF.pos '' {t : ConNF.Tangle c.β | t.set ∈ c.s}

theorem ConNF.Code.positions_nonempty [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) : c.positions.Nonempty

theorem ConNF.Code.positions_lt_of_cloud [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c d : ConNF.Code} (h : ConNF.Cloud c d) (ν₂ : ConNF.μ) : ν₂ ∈ d.positions → ∃ ν₁ ∈ c.positions, ν₁ < ν₂

def ConNF.Code.pos [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) : ConNF.μ

Equations

• c.pos = ⋯.min c.positions ⋯

theorem ConNF.Code.cloud_subrelation [ConNF.Params] [ConNF.Level] [ConNF.LtData] : Subrelation ConNF.Cloud (InvImage (fun (x1 x2 : ConNF.μ) => x1 < x2) ConNF.Code.pos)

theorem ConNF.cloud_wf [ConNF.Params] [ConNF.Level] [ConNF.LtData] : WellFounded ConNF.Cloud

theorem ConNF.eq_of_cloud [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c : ConNF.Code} {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {s t : Set (ConNF.TSet γ)} {hs : s.Nonempty} {ht : t.Nonempty} (hcs : ConNF.Cloud c (ConNF.Code.mk γ s hs)) (hct : ConNF.Cloud c (ConNF.Code.mk γ t ht)) : s = t

inductive ConNF.Code.Even [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.Code → Prop

• mk: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.LtData] (c : ConNF.Code), (∀ (d : ConNF.Code), ConNF.Cloud d c → d.Odd) → c.Even

theorem ConNF.Code.even_iff [ConNF.Params] [ConNF.Level] [ConNF.LtData] (a✝ : ConNF.Code) : a✝.Even ↔ ∀ (d : ConNF.Code), ConNF.Cloud d a✝ → d.Odd

inductive ConNF.Code.Odd [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.Code → Prop

• mk: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.LtData] (c d : ConNF.Code), ConNF.Cloud d c → d.Even → c.Odd

theorem ConNF.Code.odd_iff [ConNF.Params] [ConNF.Level] [ConNF.LtData] (a✝ : ConNF.Code) : a✝.Odd ↔ ∃ (d : ConNF.Code), ConNF.Cloud d a✝ ∧ d.Even

theorem ConNF.not_even_and_odd [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) : ¬(c.Even ∧ c.Odd)

theorem ConNF.even_or_odd [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) : c.Even ∨ c.Odd

@[simp]

theorem ConNF.not_even [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) : ¬c.Even ↔ c.Odd

@[simp]

theorem ConNF.not_odd [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) : ¬c.Odd ↔ c.Even

inductive ConNF.Represents [ConNF.Params] [ConNF.Level] [ConNF.LtData] : Rel ConNF.Code ConNF.Code

• refl: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.LtData] (c : ConNF.Code), c.Even → ConNF.Represents c c
• cloud: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.LtData] (c d : ConNF.Code), c.Even → ConNF.Cloud c d → ConNF.Represents c d

theorem ConNF.Represents.even [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c d : ConNF.Code} (h : ConNF.Represents c d) : c.Even

theorem ConNF.represents_injective [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.Represents.Injective

theorem ConNF.represents_surjective [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.Represents.Surjective

theorem ConNF.represents_cofunctional [ConNF.Params] [ConNF.Level] [ConNF.LtData] : ConNF.Represents.Cofunctional

theorem ConNF.eq_of_represents [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c : ConNF.Code} {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {s t : Set (ConNF.TSet γ)} {hs : s.Nonempty} {ht : t.Nonempty} (hcs : ConNF.Represents c (ConNF.Code.mk γ s hs)) (hct : ConNF.Represents c (ConNF.Code.mk γ t ht)) : s = t

theorem ConNF.exists_represents [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c : ConNF.Code} (hc : c.Even) (γ : ConNF.Λ) [ConNF.LtLevel ↑γ] : ∃ (s : Set (ConNF.TSet ↑γ)) (hs : s.Nonempty), ConNF.Represents c (ConNF.Code.mk (↑γ) s hs)

def ConNF.Code.members [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) (β : ConNF.TypeIndex) [ConNF.LtLevel β] : Set (ConNF.TSet β)

Equations

• c.members β = {x : ConNF.TSet β | ∃ (s : Set (ConNF.TSet β)) (hs : s.Nonempty), x ∈ s ∧ ConNF.Represents c (ConNF.Code.mk β s hs)}

theorem ConNF.Code.members_eq_of_represents [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c : ConNF.Code} {β : ConNF.TypeIndex} [ConNF.LtLevel β] {s : Set (ConNF.TSet β)} {hs : s.Nonempty} (hc : ConNF.Represents c (ConNF.Code.mk β s hs)) : c.members β = s

theorem ConNF.Code.members_nonempty [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c : ConNF.Code} (hc : c.Even) (β : ConNF.Λ) [ConNF.LtLevel ↑β] : (c.members ↑β).Nonempty

theorem ConNF.Code.ext [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c d : ConNF.Code} (hc : c.Even) (hd : d.Even) (β : ConNF.Λ) [ConNF.LtLevel ↑β] (h : c.members ↑β = d.members ↑β) : c = d

theorem ConNF.Code.eq_of_isMin [ConNF.Params] [ConNF.Level] [ConNF.LtData] (c : ConNF.Code) (hα : IsMin ConNF.α) : ∃ (s : Set (ConNF.TSet ⊥)) (hs : s.Nonempty), c = ConNF.Code.mk ⊥ s hs

theorem ConNF.Code.bot_even [ConNF.Params] [ConNF.Level] [ConNF.LtData] (s : Set (ConNF.TSet ⊥)) (hs : s.Nonempty) : (ConNF.Code.mk ⊥ s hs).Even

theorem ConNF.Code.members_bot [ConNF.Params] [ConNF.Level] [ConNF.LtData] (s : Set (ConNF.TSet ⊥)) (hs : s.Nonempty) : (ConNF.Code.mk ⊥ s hs).members ⊥ = s

theorem ConNF.Code.ext' [ConNF.Params] [ConNF.Level] [ConNF.LtData] {c d : ConNF.Code} (hc : c.Even) (hd : d.Even) (h : ∀ (β : ConNF.TypeIndex) [inst : ConNF.LtLevel β], c.members β = d.members β) : c = d