CodeLinks.lean`

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

CodeOrdinal

def OAI.PartitionConsistency.ProductForcing.ChainCode.Index line 22
Source documentation
Small carrier for the prescribed ground wellordering; no rearrangement of code order occurs when conditions or components move.
```
def Index := Shrink.{u} (ChainCode hμ c C)
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode
def OAI.PartitionConsistency.ProductForcing.ChainCode.code line 24
instance OAI.PartitionConsistency.ProductForcing.ChainCode.(instance at line 26) line 26
instance OAI.PartitionConsistency.ProductForcing.ChainCode.(instance at line 30) line 30
def OAI.PartitionConsistency.ProductForcing.ChainCode.tailGroup line 45
Source documentation
The old tail fixer viewed faithfully as coordinate permutations.
```
def tailGroup : Subgroup (Equiv.Perm I) :=
…
```
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.tailGroup_mem line 49
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.root_le_tailGroup line 57
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.tailGroup_supported line 73
def OAI.PartitionConsistency.ProductForcing.ChainCode.IsSelected line 78
Source documentation
A small index is selected precisely when its actual ground name code is persistently least in its eventual-equality class.
```
def IsSelected (a : Index hμ c C) (d : CohenForcing.Condition I κ) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode.Index, OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.isSelected_mono line 81
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.isSelected_covariance line 86
def OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalRank line 95
Source documentation
The von Neumann rank of a selected code, not a check-name for its predetermined ground index.
```
def ordinalRank (a : Index hμ c C) : (system (M := M) (I := I) (κ := κ) hμ).Name :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode.Index, OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalType line 101
Source documentation
The similarly supported total order-type name.
```
def ordinalType : (system (M := M) (I := I) (κ := κ) hμ).Name :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalType_decide line 106
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalRank_eq_iff line 112
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalRank_decide line 120
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.member_ordinalRank line 130
def OAI.PartitionConsistency.ProductForcing.ChainCode.Links line 171
Source documentation
At every sufficiently late chain vertex a code entry equals the given name at w, and that vertex actually is a successor of w.
```
def Links (d : CohenForcing.Condition I κ) (w : Vertex q)
    (τ : (system (M := M) (I := I) (κ := κ) hμ).Name) (a : ChainCode hμ c C) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.ChainCode
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.links_mono line 179
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.links_common line 188
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.links_congr line 197
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.links_same line 206
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.links_eq_iff_same line 223
Source documentation
The common code comparison is exactly forced equality, at any one vertex at which both codes have linked representatives.
```
theorem links_eq_iff_same {d : CohenForcing.Condition I κ} {w : Vertex q}
    {τ σ : (system (M := M) (I := I) (κ := κ) hμ).Name} {a b : ChainCode hμ c C}
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.ChainCode
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.links_of_represents_at line 257
Source documentation
A representation in a principal quotient implies actual forced code links. There is no genericity assumption on that principal quotient.
```
theorem links_of_represents_at (d : CohenForcing.Condition I κ) (a : ChainCode hμ c C)
    (b : (D[principalFilter d]).Glued hj v)
    (ha : Represents hμ c hcard hsize hmerger hj E hE C (principalFilter d) a b)
    (w : Vertex q) (τ : LocalName hμ c w.diagram)
    (hτ : At hμ c hcard hsize hmerger hj E hE (principalFilter d) w τ.name b) :
    Links hμ c C d w τ.name a := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Represents, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.At, OAI.PartitionConsistency.ProductForcing.ChainCode.Links
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.at_of_represents_links line 289
Source documentation
A linked local name is in the exact fiber, not merely eligible. The bijective contraction maps certify the exact ideal.
```
theorem at_of_represents_links (d : CohenForcing.Condition I κ) (a : ChainCode hμ c C)
    (b : (D[principalFilter d]).Glued hj v)
    (ha : Represents hμ c hcard hsize hmerger hj E hE C (principalFilter d) a b)
    (w : Vertex q) (τ : LocalName hμ c w.diagram) (hτ : Links hμ c C d w τ.name a) :
    At hμ c hcard hsize hmerger hj E hE (principalFilter d) w τ.name b := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Represents, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Links, OAI.PartitionConsistency.ProductForcing.ChainCode.At
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.links_stable line 313
Source documentation
Extraction of the actual stable ideal from a persistent working code and a literal name linked to it at w.
```
theorem links_stable (d : CohenForcing.Condition I κ) (a : ChainCode hμ c C)
    (ha : Works hμ c hcard hsize hmerger hj E hE C d a)
    (w : Vertex q) (τ : LocalName hμ c w.diagram) (hτ : Links hμ c C d w τ.name a) :
    (system hμ).Forces ![τ.name,labelSet hμ c,E] ((d,w.diagram) : Poset M I κ)
        (SetLanguage.isClass 0 1 2) ∧
      ∀ e, e ≤ d → forcedAvailability hμ c hcard hsize hmerger e w.diagram w.index τ = w.ideal := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Works, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Links, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.labelSet, OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.SetLanguage.isClass, OAI.PartitionConsistency.ProductForcing.forcedAvailability
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.exists_linked_working_of_stable line 349
Source documentation
Stable exact membership at any vertex in the component gives a code which works at every stronger Cohen condition and remains linked there.
```
theorem exists_linked_working_of_stable (d : CohenForcing.Condition I κ)
    (w : Vertex q) (hw : Vertex.Common v w) (τ : LocalName hμ c w.diagram)
    (hel : (system hμ).Forces ![τ.name,labelSet hμ c,E]
      ((d,w.diagram) : Poset M I κ) (SetLanguage.isClass 0 1 2))
    (hstable : ∀ e, e ≤ d →
      forcedAvailability hμ c hcard hsize hmerger e w.diagram w.index τ = w.ideal) :
    ∃ a : ChainCode hμ c C, Works hμ c hcard hsize hmerger hj E hE C d a ∧
      Links hμ c C d w τ.name a := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.labelSet, OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.SetLanguage.isClass, OAI.PartitionConsistency.ProductForcing.forcedAvailability, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Works, OAI.PartitionConsistency.ProductForcing.ChainCode.Links
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.links_restrict line 391
Source documentation
Restriction along an actual contraction preserves the literal linked representative. Both the condition and the code remain unchanged.
```
theorem links_restrict (d : CohenForcing.Condition I κ) {w z : Vertex q}
    (f : w.Arrow z) (τ : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.links_descend line 405
Source documentation
Conversely a representative which is already supported on the smaller successor diagram has the same link there, by local decision.
```
theorem links_descend (d : CohenForcing.Condition I κ) {w z : Vertex q}
    (f : w.Arrow z) (τ : LocalName hμ c z.diagram)
    (a : ChainCode hμ c C) (h : Links hμ c C d w τ.name a) :
    Links hμ c C d z τ.name a := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Links
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.working_linked line 421
Source documentation
A working code has a normalized representative at EVERY vertex in its component; this is not restricted to the first vertex of the chosen chain.
```
theorem working_linked (d : CohenForcing.Condition I κ) (a : ChainCode hμ c C)
    (ha : Works hμ c hcard hsize hmerger hj E hE C d a)
    (w : Vertex q) (hw : Vertex.Common v w) :
    ∃ τ : LocalName hμ c w.diagram, Links hμ c C d w τ.name a := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Works, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Links