The cloud map

The cloud map from γ to β ≠ γ sends a set of t-sets of type γ to a set of t-sets of type β. Each t-set of type γ in the domain is sent to a "cloud" of β-typed near-litters, representing "junk" at level β. This map will used to identify codes that represent the same TTT object.

An important property for intuition is that the cloud maps have disjoint ranges (except on empty codes) and are each injective, so if we connect each code to its images under the cloud maps, we get a tree (except for empty codes, which form a complete graph).

Main declarations

• ConNF.cloud: The cloud map from γ-tangles to β-tangles, assuming γ ≠ β.
• ConNF.extension: The cloud map if γ ≠ β, otherwise the identity map.
• ConNF.cloudCode: The cloud map as a map from codes with any extension to codes of extension β.
• ConNF.CloudRel: The relation on codes generated by cloudCode. It relates c to d iff d is an image of c under the cloudCode map. This relation is well-founded on nonempty codes. See ConNF.cloudRel'_wellFounded.

Notation

• c ↝₀ d: d is the image of c under the cloudCode map.
• c ↝ d: d is the image of the nonempty code c under the cloudCode map.

def ConNF.cloud [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] (hγβ : γ ≠ ↑β) (s : Set (ConNF.TSet γ)) : Set (ConNF.TSet ↑β)

The cloud map. We map each t-set to all typed near-litters near any fuzzed tangle with this t-set, and take the union over all t-sets in the input.

Equations

• ConNF.cloud hγβ s = {u : ConNF.TSet ↑β | ∃ (t : ConNF.Tangle γ), t.set_lt ∈ s ∧ ∃ (N : ConNF.NearLitter), N.fst = ConNF.fuzz hγβ t ∧ u = ConNF.typedNearLitter N}

@[simp]

theorem ConNF.cloud_empty [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {hγβ : γ ≠ ↑β} : ConNF.cloud hγβ ∅ = ∅

@[simp]

theorem ConNF.cloud_singleton [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {hγβ : γ ≠ ↑β} (t : ConNF.TSet γ) : ConNF.cloud hγβ {t} = {u : ConNF.TSet ↑β | ∃ (t' : ConNF.Tangle γ), t'.set_lt = t ∧ ∃ (N : ConNF.NearLitter), N.fst = ConNF.fuzz hγβ t' ∧ u = ConNF.typedNearLitter N}

theorem Set.Nonempty.cloud [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {hγβ : γ ≠ ↑β} {s : Set (ConNF.TSet γ)} (h : s.Nonempty) : (ConNF.cloud hγβ s).Nonempty

@[simp]

theorem ConNF.cloud_eq_empty [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {s : Set (ConNF.TSet γ)} (hγβ : γ ≠ ↑β) : ConNF.cloud hγβ s = ∅ ↔ s = ∅

@[simp]

theorem ConNF.cloud_nonempty [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {s : Set (ConNF.TSet γ)} (hγβ : γ ≠ ↑β) : (ConNF.cloud hγβ s).Nonempty ↔ s.Nonempty

theorem ConNF.subset_cloud [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {hγβ : γ ≠ ↑β} {s : Set (ConNF.TSet γ)} (t : ConNF.Tangle γ) (ht : t.set_lt ∈ s) : ⇑ConNF.typedNearLitter '' {N : ConNF.NearLitter | N.fst = ConNF.fuzz hγβ t} ⊆ ConNF.cloud hγβ s

theorem ConNF.μ_le_mk_cloud [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {hγβ : γ ≠ ↑β} {s : Set (ConNF.TSet γ)} : s.Nonempty → Cardinal.mk ConNF.μ ≤ Cardinal.mk ↑(ConNF.cloud hγβ s)

theorem ConNF.subset_of_cloud_subset [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {hγβ : γ ≠ ↑β} (s₁ : Set (ConNF.TSet γ)) (s₂ : Set (ConNF.TSet γ)) (h : ConNF.cloud hγβ s₁ ⊆ ConNF.cloud hγβ s₂) : s₁ ⊆ s₂

theorem ConNF.cloud_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {hγβ : γ ≠ ↑β} : Function.Injective (ConNF.cloud hγβ)

theorem ConNF.cloud_disjoint_range [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {hγβ : γ ≠ ↑β} {δ : ConNF.TypeIndex} [ConNF.LtLevel δ] {hδβ : δ ≠ ↑β} (c : Set (ConNF.TSet γ)) (d : Set (ConNF.TSet δ)) (hc : c.Nonempty) (h : ConNF.cloud hγβ c = ConNF.cloud hδβ d) : γ = δ

We don't need to prove that the ranges of the cloud maps are disjoint for different β, since this holds at the type level.

We now show that there are only finitely many iterated images under any inverse cloud map, in the case of nonempty sets.

theorem ConNF.wellFounded_pos [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] : WellFounded fun (a b : ConNF.Tangle γ) => ConNF.pos a < ConNF.pos b

noncomputable def ConNF.minTangle [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] (s : Set (ConNF.Tangle γ)) (hs : s.Nonempty) : ConNF.Tangle γ

The minimum tangle of a nonempty set of tangles.

Equations

• ConNF.minTangle s hs = ⋯.min s hs

theorem ConNF.minTangle_mem [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] (s : Set (ConNF.Tangle γ)) (hs : s.Nonempty) : ConNF.minTangle s hs ∈ s

theorem ConNF.minTangle_le [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] (s : Set (ConNF.Tangle γ)) (hs : s.Nonempty) {t : ConNF.Tangle γ} (ht : t ∈ s) : ConNF.pos (ConNF.minTangle s hs) ≤ ConNF.pos t

theorem ConNF.set_invImage_nonempty [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] (s : Set (ConNF.TSet γ)) (hs : s.Nonempty) : (ConNF.Tangle.set_lt ⁻¹' s).Nonempty

noncomputable def ConNF.minTSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] (s : Set (ConNF.TSet γ)) (hs : s.Nonempty) : ConNF.Tangle γ

The minimum tangle with a t-set in s.

Equations

• ConNF.minTSet s hs = ConNF.minTangle (ConNF.Tangle.set_lt ⁻¹' s) ⋯

theorem ConNF.minTSet_lt_minTSet_cloud [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {γ : ConNF.TypeIndex} [ConNF.LtLevel γ] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {hγβ : γ ≠ ↑β} (s : Set (ConNF.TSet γ)) (hs : s.Nonempty) : ConNF.pos (ConNF.minTSet s hs) < ConNF.pos (ConNF.minTSet (ConNF.cloud hγβ s) ⋯)

noncomputable def ConNF.codeMinMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] (c : ConNF.NonemptyCode) : ConNF.μ

Tool that lets us use well-founded recursion on codes via μ. This maps a nonempty code to the least pos of a tangle in the extension of the code.

Equations

• ConNF.codeMinMap c = ConNF.pos (ConNF.minTSet (↑c).members ⋯)

theorem ConNF.invImage_codeMinMap_wf [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] : WellFounded (InvImage (fun (x x_1 : ConNF.μ) => x < x_1) ConNF.codeMinMap)

The pullback < relation on codes is well-founded.

def ConNF.extension [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {β : ConNF.TypeIndex} [ConNF.LtLevel β] (s : Set (ConNF.TSet β)) (γ : ConNF.Λ) [ConNF.LtLevel ↑γ] : Set (ConNF.TSet ↑γ)

The cloud map, phrased as a function on sets of γ-tangles, but if γ = β, this is the identity function.

Equations

• ConNF.extension s γ = if hβγ : β = ↑γ then cast ⋯ s else ConNF.cloud hβγ s

@[simp]

theorem ConNF.extension_self [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] (s : Set (ConNF.TSet ↑γ)) : ConNF.extension s γ = s

@[simp]

theorem ConNF.extension_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {β : ConNF.TypeIndex} [ConNF.LtLevel β] (s : Set (ConNF.TSet β)) (γ : ConNF.Λ) [ConNF.LtLevel ↑γ] (hβγ : β = ↑γ) : ConNF.extension s γ = cast ⋯ s

@[simp]

theorem ConNF.extension_ne [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {β : ConNF.TypeIndex} [ConNF.LtLevel β] (s : Set (ConNF.TSet β)) (γ : ConNF.Λ) [ConNF.LtLevel ↑γ] (hβγ : β ≠ ↑γ) : ConNF.extension s γ = ConNF.cloud hβγ s

def ConNF.cloudCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (β : ConNF.Λ) [ConNF.LtLevel ↑β] (c : ConNF.Code) : ConNF.Code

The cloud map, phrased as a function on α-codes, but if the code's level matches β, this is the identity function. This is written in a weird way in order to make (cloudCode β c).1 defeq to β.

Equations

• ConNF.cloudCode β c = ConNF.Code.mk (↑β) (ConNF.extension c.members β)

theorem ConNF.cloudCode_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (β : ConNF.Λ) [ConNF.LtLevel ↑β] (c : ConNF.Code) (hcβ : c.β = ↑β) : ConNF.cloudCode β c = c

theorem ConNF.cloudCode_ne [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (β : ConNF.Λ) [ConNF.LtLevel ↑β] (c : ConNF.Code) (hcβ : c.β ≠ ↑β) : ConNF.cloudCode β c = ConNF.Code.mk (↑β) (ConNF.cloud hcβ c.members)

@[simp]

theorem ConNF.fst_cloudCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (β : ConNF.Λ) [ConNF.LtLevel ↑β] (c : ConNF.Code) : (ConNF.cloudCode β c).β = ↑β

@[simp]

theorem ConNF.snd_cloudCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (β : ConNF.Λ) [ConNF.LtLevel ↑β] (c : ConNF.Code) (hcβ : c.β ≠ ↑β) : (ConNF.cloudCode β c).members = ConNF.cloud hcβ c.members

@[simp]

theorem ConNF.cloudCode_mk_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (β : ConNF.Λ) [ConNF.LtLevel ↑β] (s : Set (ConNF.TSet ↑β)) : ConNF.cloudCode β (ConNF.Code.mk (↑β) s) = ConNF.Code.mk (↑β) s

@[simp]

theorem ConNF.cloudCode_mk_ne [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (γ : ConNF.TypeIndex) [ConNF.LtLevel γ] (β : ConNF.Λ) [ConNF.LtLevel ↑β] (hγβ : γ ≠ ↑β) (s : Set (ConNF.TSet γ)) : ConNF.cloudCode β (ConNF.Code.mk γ s) = ConNF.Code.mk (↑β) (ConNF.cloud hγβ s)

@[simp]

theorem ConNF.cloudCode_isEmpty [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {c : ConNF.Code} : (ConNF.cloudCode β c).IsEmpty ↔ c.IsEmpty

@[simp]

theorem ConNF.cloudCode_nonempty [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {c : ConNF.Code} : (ConNF.cloudCode β c).members.Nonempty ↔ c.members.Nonempty

theorem ConNF.Code.IsEmpty.cloudCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {c : ConNF.Code} : c.IsEmpty → (ConNF.cloudCode β c).IsEmpty

Alias of the reverse direction of ConNF.cloudCode_isEmpty.

theorem ConNF.cloudCode_injOn [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {β : ConNF.Λ} [ConNF.LtLevel ↑β] : Set.InjOn (ConNF.cloudCode β) {c : ConNF.Code | c.β ≠ ↑β ∧ c.members.Nonempty}

theorem ConNF.μ_le_mk_cloudCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {β : ConNF.Λ} [ConNF.LtLevel ↑β] (c : ConNF.Code) (hcβ : c.β ≠ ↑β) : c.members.Nonempty → Cardinal.mk ConNF.μ ≤ Cardinal.mk ↑(ConNF.cloudCode β c).members

theorem ConNF.codeMinMap_lt_codeMinMap_cloudCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (β : ConNF.Λ) [ConNF.LtLevel ↑β] (c : ConNF.NonemptyCode) (hcβ : (↑c).β ≠ ↑β) : ConNF.codeMinMap c < ConNF.codeMinMap ⟨ConNF.cloudCode β ↑c, ⋯⟩

theorem ConNF.cloudRel_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (c : ConNF.Code) : ∀ (a : ConNF.Code), c ↝₀ a ↔ ∃ (β : ConNF.Λ) (inst : ConNF.LtLevel ↑β), c.β ≠ ↑β ∧ a = ConNF.cloudCode β c

inductive ConNF.CloudRel [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (c : ConNF.Code) : ConNF.Code → Prop

This relation on α-codes allows us to state that there are only finitely many iterated images under the inverse cloud map. Note that we require the map to actually change the data, by stipulating that c.1 ≠ β.

• intro: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.ModelDataLt] [inst_4 : ConNF.PositionedTanglesLt] [inst_5 : ConNF.TypedObjectsLt] {c : ConNF.Code} (β : ConNF.Λ) [inst_6 : ConNF.LtLevel ↑β], c.β ≠ ↑β → c ↝₀ ConNF.cloudCode β c

def ConNF.«term_↝₀_» : Lean.TrailingParserDescr

Equations

• ConNF.«term_↝₀_» = Lean.ParserDescr.trailingNode `ConNF.term_↝₀_ 62 62 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↝₀ ") (Lean.ParserDescr.cat `term 63))

theorem ConNF.cloudRel_subsingleton [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {c : ConNF.Code} (hc : c.members.Nonempty) : {d : ConNF.Code | d ↝₀ c}.Subsingleton

theorem ConNF.cloudRel_cloudCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (β : ConNF.Λ) [ConNF.LtLevel ↑β] {c : ConNF.Code} {d : ConNF.Code} (hd : d.members.Nonempty) (hdβ : d.β ≠ ↑β) : c ↝₀ ConNF.cloudCode β d ↔ c = d

theorem ConNF.CloudRel.nonempty_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {c : ConNF.Code} {d : ConNF.Code} : c ↝₀ d → (c.members.Nonempty ↔ d.members.Nonempty)

theorem ConNF.cloudRelEmptyEmpty [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (γ : ConNF.TypeIndex) [ConNF.LtLevel γ] (β : ConNF.Λ) [ConNF.LtLevel ↑β] (hγβ : γ ≠ ↑β) : ConNF.Code.mk γ ∅ ↝₀ ConNF.Code.mk ↑β ∅

theorem ConNF.eq_of_cloudCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {c : ConNF.Code} {d : ConNF.Code} {β : ConNF.Λ} {γ : ConNF.Λ} [ConNF.LtLevel ↑β] [ConNF.LtLevel ↑γ] (hc : c.members.Nonempty) (hcβ : c.β ≠ ↑β) (hdγ : d.β ≠ ↑γ) (h : ConNF.cloudCode β c = ConNF.cloudCode γ d) : c = d

theorem ConNF.cloudRel'_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (c : ConNF.NonemptyCode) : ∀ (a : ConNF.NonemptyCode), c ↝ a ↔ ∃ (β : ConNF.Λ) (inst : ConNF.LtLevel ↑β), (↑c).β ≠ ↑β ∧ a = ⟨ConNF.cloudCode β ↑c, ⋯⟩

inductive ConNF.CloudRel' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (c : ConNF.NonemptyCode) : ConNF.NonemptyCode → Prop

This relation on α-codes allows us to state that there are only finitely many iterated images under the inverse cloud map.

• intro: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.ModelDataLt] [inst_4 : ConNF.PositionedTanglesLt] [inst_5 : ConNF.TypedObjectsLt] {c : ConNF.NonemptyCode} (β : ConNF.Λ) [inst_6 : ConNF.LtLevel ↑β], (↑c).β ≠ ↑β → c ↝ ⟨ConNF.cloudCode β ↑c, ⋯⟩

def ConNF.«term_↝_» : Lean.TrailingParserDescr

Equations

• ConNF.«term_↝_» = Lean.ParserDescr.trailingNode `ConNF.term_↝_ 62 62 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↝ ") (Lean.ParserDescr.cat `term 63))

@[simp]

theorem ConNF.cloudRel_coe_coe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {c : ConNF.NonemptyCode} {d : ConNF.NonemptyCode} : ↑c ↝₀ ↑d ↔ c ↝ d

theorem ConNF.cloud_subrelation [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : Subrelation (fun (x x_1 : ConNF.NonemptyCode) => x ↝ x_1) (InvImage (fun (x x_1 : ConNF.μ) => x < x_1) ConNF.codeMinMap)

theorem ConNF.cloudRel'_wellFounded [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : WellFounded fun (x x_1 : ConNF.NonemptyCode) => x ↝ x_1

There are only finitely many iterated images under any inverse cloud map.

instance ConNF.instWellFoundedRelationNonemptyCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : WellFoundedRelation ConNF.NonemptyCode

Equations

• ConNF.instWellFoundedRelationNonemptyCode = { rel := fun (x x_1 : ConNF.NonemptyCode) => x ↝ x_1, wf := ⋯ }

theorem ConNF.cloudRel'_subsingleton [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (c : ConNF.NonemptyCode) : {d : ConNF.NonemptyCode | d ↝ c}.Subsingleton

There is at most one inverse under an cloud map. This corresponds to the fact that there is only one code which is related (on the left) to any given code under the cloud map relation.