Codes

In this file, we define codes and clouds.

Main declarations

• ConNF.foo: Something new.

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

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

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

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

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

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

Equations

• ConNF.instModelDataOfLtDataOfLtLevel = ConNF.LtData.data

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

Equations

• ConNF.instPositionTangle_1 = ConNF.LtData.positions

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

Equations

• ConNF.instTypedNearLitters = ConNF.LtData.typedNearLitters

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

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

Equations

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

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

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

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

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

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

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

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

• mk [Params] [Level] [LtData] (c d : Code) : Cloud d c → d.Even → c.Odd

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

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

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

@[simp]

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

@[simp]

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

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

• refl [Params] [Level] [LtData] (c : Code) : c.Even → Represents c c
• cloud [Params] [Level] [LtData] (c d : Code) : c.Even → Cloud c d → Represents c d

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

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

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

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

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

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

def ConNF.Code.members [Params] [Level] [LtData] (c : Code) (β : TypeIndex) [LtLevel β] : Set (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 [Params] [Level] [LtData] {c : Code} {β : TypeIndex} [LtLevel β] {s : Set (TSet β)} {hs : s.Nonempty} (hc : Represents c (mk β s hs)) : c.members β = s

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

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

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

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

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

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