PersistentCodes.lean`

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

CodeSelection

def OAI.PartitionConsistency.ConditionCodeSelection.Selected line 21
Source documentation
A working code and the assertion that no smaller code can ever become a working representative of the same value.
```
def Selected (a : A) (p : P) : Prop :=
…
```
theorem OAI.PartitionConsistency.ConditionCodeSelection.selected_mono line 31
theorem OAI.PartitionConsistency.ConditionCodeSelection.selected_unique line 38
Source documentation
Two persistent least codes agreeing at a condition are literally equal, not merely equivalent.
```
theorem selected_unique {a b : A} {p : P}
    (ha : Selected W E a p) (hb : Selected W E b p) (hab : E p a b) : a = b := by
…
```
Mentions: OAI.PartitionConsistency.ConditionCodeSelection.Selected
theorem OAI.PartitionConsistency.ConditionCodeSelection.dense_selected line 49
Source documentation
Every working code densely admits a selected representative. The minimum is taken over the set of codes which can agree somewhere below the starting condition; minimality therefore survives every refinement.
```
theorem dense_selected (p : P) (a : A) (ha : W p a) :
    ∃ q, q ≤ p ∧ ∃ b, Selected W E b q ∧ E q a b := by
…
```
Mentions: OAI.PartitionConsistency.ConditionCodeSelection.Selected
theorem OAI.PartitionConsistency.ConditionCodeSelection.selected_covariance line 64
Source documentation
A coordinate transformation acts on conditions but leaves each ground code in place (the same-code covariance of the source). It therefore also preserves the persistent least-code predicate.
```
theorem selected_covariance (e : P ≃o P)
    (hw : ∀ p a, W (e p) a ↔ W p a)
    (he : ∀ p a b, E (e p) a b ↔ E p a b) (a : A) (p : P) :
    Selected W E a (e p) ↔ Selected W E a p := by
…
```
Mentions: OAI.PartitionConsistency.ConditionCodeSelection.Selected
theorem OAI.PartitionConsistency.ForcingQuotient.principalFilter_move line 94
def OAI.PartitionConsistency.ProductForcing.ChainCode.Works line 122
Source documentation
A code keeps representing a genuine exact-fiber value at every stronger Cohen condition. This is a predicate on the already defined name collection, not an extra mathematical hypothesis about that collection.
```
def Works (d : CohenForcing.Condition I κ) (a : ChainCode hμ c C) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode
def OAI.PartitionConsistency.ProductForcing.ChainCode.Same line 128
Source documentation
Eventual equality forced by one Cohen condition. Every comparison is of actual names at their chain diagrams.
```
def Same (d : CohenForcing.Condition I κ) (a b : ChainCode hμ c C) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.works_mono line 133
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.same_refl line 139
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.same_symm line 143
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.same_trans line 149
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.same_mono line 157
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.at_eq_iff line 164
Source documentation
At one vertex, equality of the glued points is precisely equality of the local symbolic quotient values.
```
theorem at_eq_iff {F : GenericFilter (CohenForcing.Condition I κ)} {w : Vertex q}
    {τ σ : (system (M := M) (I := I) (κ := κ) hμ).Name}
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.same_iff_represents_eq line 186
Source documentation
Eventual forced equality detects equality of genuinely represented points. This theorem applies to each principal quotient, without assuming that the filter meets ANY dense sets.
```
theorem same_iff_represents_eq {d : CohenForcing.Condition I κ} {a b : ChainCode hμ c C}
    {x y : (D[principalFilter d]).Glued hj v}
    (ha : Represents hμ c hcard hsize hmerger hj E hE C (principalFilter d) a x)
    (hb : Represents hμ c hcard hsize hmerger hj E hE C (principalFilter d) b y) :
    Same hμ c C d a b ↔ x = y := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Represents, OAI.PartitionConsistency.ProductForcing.ChainCode.Same
abbrev OAI.PartitionConsistency.ProductForcing.ChainCode.Selected line 209
Source documentation
Persistent least codes, defined over the fixed ground wellordering.
```
abbrev Selected (a : ChainCode hμ c C) (d : CohenForcing.Condition I κ) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.selected_mono line 213
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.selected_unique line 220
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.dense_selected line 228
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.works_covariance line 238
Source documentation
The working-code predicate is invariant under a tail fixer acting on the condition. The code itself, and its prescribed ground ordering, do not move.
```
theorem works_covariance (k : C.tailFixer hj) (d : CohenForcing.Condition I κ)
    (a : ChainCode hμ c C) :
    Works hμ c hcard hsize hmerger hj E hE C (d.permute k.val.val.val) a ↔
    Works hμ c hcard hsize hmerger hj E hE C d a := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Works
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.same_covariance line 270
Source documentation
Eventual equality has the same covariance, again for the unchanged codes. This uses literal fixation on a tail, not invariance of the code set's wellordering under coordinatewise transport.
```
theorem same_covariance (k : C.tailFixer hj) (d : CohenForcing.Condition I κ)
    (a b : ChainCode hμ c C) :
    Same hμ c C (d.permute k.val.val.val) a b ↔ Same hμ c C d a b := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Same
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.selected_covariance line 292
Source documentation
Condition-level covariance of least-code selection. All auxiliary wellorders remain fixed.
```
theorem selected_covariance (k : C.tailFixer hj) (d : CohenForcing.Condition I κ)
    (a : ChainCode hμ c C) :
    Selected hμ c hcard hsize hmerger hj E hE C a (d.permute k.val.val.val) ↔
      Selected hμ c hcard hsize hmerger hj E hE C a d :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Selected
theorem OAI.PartitionConsistency.ProductForcing.eligibleSystem_availability_eq line 327
Source documentation
Eligibility adds no restriction to the availability witnesses below a supporting root: a representative of an eligible class is itself eligible, by local decision.
```
theorem eligibleSystem_availability_eq (F : GenericFilter (CohenForcing.Condition I κ))
    (r : Diagram M I) (a : M) (ha : r.sub a = q) (x : (D[F]).Obj r) :
    (D[F]).availability r a x =
      (allLocalSystem (c := c) hμ hcard hsize hmerger F).availability r a x.val := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.allLocalSystem
theorem OAI.PartitionConsistency.ProductForcing.exists_fiber_principal line 351
Source documentation
For any chosen name, the actual exact-fiber predicate in a principal quotient agrees with eligibility and its computed forced availability.
```
theorem exists_fiber_principal (d : CohenForcing.Condition I κ) (v : Vertex q)
    (τ : LocalName hμ c v.diagram)
    (hel : (system hμ).Forces ![τ.name,labelSet hμ c,E]
      ((d,v.diagram) : Poset M I κ) (SetLanguage.isClass 0 1 2))
    (hU : forcedAvailability hμ c hcard hsize hmerger d v.diagram v.index τ = v.ideal) :
    ∃ x : (D[principalFilter d]).vertexFiber v,
      LocalQuotient.ofName (principalFilter d) τ = x.val.val := 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.LocalQuotient.ofName
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.exists_working_code_of_stable line 371
Source documentation
An explicit eligible name with permanently constant ideal at the root has a code which works at EVERY refinement of the condition. At each chain vertex the code's entry remains the exact same ground normalized name.
```
theorem exists_working_code_of_stable (d : CohenForcing.Condition I κ)
    (τ : LocalName hμ c v.diagram)
    (hel : (system hμ).Forces ![τ.name,labelSet hμ c,E]
      ((d,v.diagram) : Poset M I κ) (SetLanguage.isClass 0 1 2))
    (hstable : ∀ e, e ≤ d →
      forcedAvailability hμ c hcard hsize hmerger e v.diagram v.index τ = v.ideal) :
    ∃ a : ChainCode hμ c C,
      Works hμ c hcard hsize hmerger hj E hE C d a ∧
      ∀ i, (system hμ).atomic.EqF ((d,v.diagram) : Poset M I κ) (a i).name τ.name := 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
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.TransF line 439
Source documentation
The semantic transitivity clause, with unrestricted HS names.
```
def TransF (p : P) (σ : S.Name) : Prop :=
…
```
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.OrdF line 445
Source documentation
A transitive set of transitive sets; used to prove ordinal preservation, not as a replacement for the ordinal formula in the statement of ACwo.
```
def OrdF (p : P) (σ : S.Name) : Prop :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.transF_mono line 448
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.transF_congr line 451
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ordF_mono line 461
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ordF_congr line 464
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ordF_mem line 474
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_transitiveSet line 480
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ordF_of_forces_ordinal line 494
Source documentation
The literal ordinal sentence implies the semantic hereditary transitivity used in the rank induction. Internal well-foundedness is not confused with external well-foundedness of a model.
```
theorem ordF_of_forces_ordinal {n} (v : Fin n → S.Name) (p : P) (x : Fin n)
    (ho : S.Forces v p (SetLanguage.ordinal x)) : S.OrdF p (v x) := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.ordinal
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ordF_eq_check_le line 521
Source documentation
Ordinal preservation for unrestricted HS names. A condition forcing a transitive set of transitive sets has an extension deciding it to be a ground ordinal. The quantitative bound is proved by induction on literal name rank.
```
theorem ordF_eq_check_le (σ : S.Name) (p : P) (ho : S.OrdF p σ) :
    ∃ q, q ≤ p ∧ ∃ β : Ordinal.{u}, β ≤ σ.raw.rank ∧
      S.atomic.EqF q σ (Name.check β.toZFSet) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_ordinal_decide line 588
Source documentation
Dense decision of any name satisfying the actual ordinal formula. This applies at arbitrary rank, not merely to normalized subset names.
```
theorem forces_ordinal_decide {n} (v : Fin n → S.Name) (p : P) (x : Fin n)
    (ho : S.Forces v p (SetLanguage.ordinal x)) :
    ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ β : Ordinal.{u},
      S.atomic.EqF r (v x) (Name.check β.toZFSet) := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.ordinal, OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check