OrdinalCodes.lean`

54 declarations, 0 contain sorry, 0 declared as axioms

OrdinalSelection

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.FixedName line 23
Source documentation
Names literally fixed by one specified subgroup.
```
def FixedName (H : Subgroup Γ) := {σ : S.Name // ∀ g ∈ H, g • σ = σ}
…
```
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.FixedName.collect line 28
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.FixedName.mem_collect line 37
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectedRankFixed line 49
Source documentation
Rank in the selected suborder: recurse only along the fixed ground wellordering. The predecessor set is small, with no bound on name ranks.
```
def selectedRankFixed (a : X) : S.FixedName H :=
…
```
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectedRank line 54
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectionType line 57
Source documentation
The ordinal consisting of the ranks of all selected elements.
```
def selectionType : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectedRank_fixed line 61
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectionType_fixed line 66
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectedRankFixed_eq line 71

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_selectedRank line 79

Source documentation

Membership is densely witnessed by a selected smaller ground code.

theorem mem_selectedRank (a : X) (ν : S.Name) (p : P) :
    S.atomic.MemF p ν (S.selectedRank R H hH hR a) ↔
      ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ b, b < a ∧ ∃ c,
        R b c ∧ r ≤ c ∧ S.atomic.EqF r ν (S.selectedRank R H hH hR b) := by
…

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_selectionType line 94
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectedRank_mem_selectionType line 102
Source documentation
Ranks of selected elements belong to the selected order type.
```
theorem selectedRank_mem_selectionType (a : X) (p : P) (ha : R a p) :
    S.atomic.MemF p (S.selectedRank R H hH hR a) (S.selectionType R H hH hR) := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectedRank_mem_selectedRank line 108
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectedRank_subset line 115
Source documentation
Taking a longer initial segment can only add members.
```
theorem selectedRank_subset {a b : X} (hab : a ≤ b) (p : P) :
    S.SubsetF p (S.selectedRank R H hH hR a) (S.selectedRank R H hH hR b) := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectedRank_subset_selectionType line 124
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.transF_selectedRank line 134
Source documentation
The recursively defined ranks really are transitive sets.
```
theorem transF_selectedRank (a : X) (p : P) :
    S.TransF p (S.selectedRank R H hH hR a) := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.transF_selectionType line 145
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ordF_selectedRank line 156
Source documentation
A member of any selected rank is itself transitive.
```
theorem ordF_selectedRank (a : X) (p : P) :
    S.OrdF p (S.selectedRank R H hH hR a) := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ordF_selectionType line 168
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectionType_decide line 180
Source documentation
Ordinary ordinal decision applies to this actual, literally invariant name; no cardinal assertion about an external-filter quotient is used.
```
theorem selectionType_decide (p : P) :
    ∃ q, q ≤ p ∧ ∃ θ : Ordinal.{u}, θ ≤ (S.selectionType R H hH hR).raw.rank ∧
      S.atomic.EqF q (S.selectionType R H hH hR) (Name.check θ.toZFSet) :=
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ordF_not_mem_self line 202
Source documentation
No ordinal name can be forced to belong to itself. Ordinal decision reduces this to irreflexivity in the genuine von Neumann ordinals.
```
theorem ordF_not_mem_self (σ : S.Name) (p : P) (ho : S.OrdF p σ) :
    ¬ S.atomic.MemF p σ σ := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectedRank_eq_iff line 212
Source documentation
Distinct selected codes have distinct ordinal ranks, at every condition where both are selected. This is an internal forcing assertion about the actual ordinal names, not an assertion about an evaluated proxy order.
```
theorem selectedRank_eq_iff (a b : X) (p : P) (ha : R a p) (hb : R b p) :
    S.atomic.EqF p (S.selectedRank R H hH hR a) (S.selectedRank R H hH hR b) ↔ a = b := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.selectedRank_decide line 229
Source documentation
Deciding a selected rank under a decision of the total order type gives an actual member of that ordinal.
```
theorem selectedRank_decide (a : X) (p : P) (ha : R a p) (θ : Ordinal.{u})
    (hθ : S.atomic.EqF p (S.selectionType R H hH hR) (Name.check θ.toZFSet)) :
    ∃ q, q ≤ p ∧ ∃ β : Set.Iio θ,
      S.atomic.EqF q (S.selectedRank R H hH hR a) (Name.check β.val.toZFSet) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check
theorem OAI.PartitionConsistency.ProductForcing.forces_at_root line 260
Source documentation
Reflection to the root, retaining the full Cohen condition.
```
theorem forces_at_root {n} (φ : Formula n)
    (v : Fin n → (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.eq_at_root line 271
theorem OAI.PartitionConsistency.ProductForcing.ordinal_decide_at_root line 287
Source documentation
Every supported ordinal name can be decided by the Cohen coordinate alone while the supporting root stays fixed.
```
theorem ordinal_decide_at_root (τ : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.ProductForcing.CohenSelection.lift line 310
Source documentation
Only the Cohen coordinate is examined. No diagram-generic or ambient fully generic filter occurs in this predicate.
```
def lift (a : X) (p : Poset M I κ) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.CohenSelection.lift_coe line 315
theorem OAI.PartitionConsistency.ProductForcing.CohenSelection.lift_covariance line 326
def OAI.PartitionConsistency.ProductForcing.CohenSelection.rank line 333
Source documentation
The literal names used for the ordinal ranks and order type.
```
def rank (a : X) : (system (M := M) (I := I) (κ := κ) hμ).Name :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.ProductForcing.CohenSelection.orderType line 336
theorem OAI.PartitionConsistency.ProductForcing.CohenSelection.rank_fixed line 340
theorem OAI.PartitionConsistency.ProductForcing.CohenSelection.orderType_fixed line 345
theorem OAI.PartitionConsistency.ProductForcing.CohenSelection.orderType_decide line 352
theorem OAI.PartitionConsistency.ProductForcing.CohenSelection.rank_eq_iff line 360
theorem OAI.PartitionConsistency.ProductForcing.CohenSelection.rank_mem line 367
theorem OAI.PartitionConsistency.ProductForcing.CohenSelection.rank_decide line 374
Source documentation
Ranks are decided without changing the chosen root diagram.
```
theorem rank_decide (a : X) (d : CohenForcing.Condition I κ) (ha : R a d) (θ : Ordinal.{u})
    (hθ : (system (M := M) (I := I) (κ := κ) hμ).atomic.EqF ((d,r) : Poset M I κ)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.CohenSelection.member_rank line 391
Source documentation
Every member of a decided order type is densely the rank of a selected code. Extraction uses actual collection-name entries.
```
theorem member_rank (hmono : ∀ {a d e}, e ≤ d → R a d → R a e)
    (d : CohenForcing.Condition I κ) (θ : Ordinal.{u})
    (hθ : (system (M := M) (I := I) (κ := κ) hμ).atomic.EqF ((d,r) : Poset M I κ)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset
def OAI.PartitionConsistency.ProductForcing.ChainCode.Rooted line 442
Source documentation
A code represents a particular root name from some index onward.
```
def Rooted (a : ChainCode hμ c C) (d : CohenForcing.Condition I κ)
    (τ : LocalName hμ c v.diagram) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.rooted_mono line 449
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.rooted_eq_iff_same line 458
Source documentation
All root representatives induce exactly the same code equivalence.
```
theorem rooted_eq_iff_same {a b : ChainCode hμ c C} {d : CohenForcing.Condition I κ}
    {τ σ : LocalName hμ c v.diagram} (ha : Rooted hμ c C a d τ) (hb : Rooted hμ c C b d σ) :
    (system hμ).atomic.EqF ((d,v.diagram) : Poset M I κ) τ.name σ.name ↔ Same hμ c C d a b := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Rooted, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.ChainCode.Same
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.working_rooted line 493
Source documentation
Every persistent code has an eligible normalized name at its root. The proof uses the genuine bijective local restriction maps.
```
theorem working_rooted (d : CohenForcing.Condition I κ) (a : ChainCode hμ c C)
    (ha : Works hμ c hcard hsize hmerger hj E hE C d a) :
    ∃ τ : LocalName hμ c v.diagram,
      (system hμ).Forces ![τ.name,labelSet hμ c,E]
        ((d,v.diagram) : Poset M I κ) (SetLanguage.isClass 0 1 2) ∧
      Rooted hμ c C a d τ := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Works, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.labelSet, OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.SetLanguage.isClass, OAI.PartitionConsistency.ProductForcing.ChainCode.Rooted
def OAI.PartitionConsistency.OrderAssignment.Table line 548
Source documentation
A set-indexed table, bounded by the order type of the ground code set.
```
def Table (L : Type u) (Λ : Ordinal.{u}) :=
…
```
def OAI.PartitionConsistency.OrderAssignment.chooseTable line 551
def OAI.PartitionConsistency.OrderAssignment.indices line 557
Source documentation
Transfer the fixed table's indices to ordinal initial segments.
```
def indices (e : Table L Λ) (θ : Ordinal.{u}) (hb : θ ≤ Λ)
    (hc : θ.card = Cardinal.mk L) : L ≃ Set.Iio θ :=
…
```
Mentions: OAI.PartitionConsistency.OrderAssignment.Table
theorem OAI.PartitionConsistency.OrderAssignment.indices_val_congr line 561
def OAI.PartitionConsistency.OrderAssignment.assignment line 570
Source documentation
Unique enumeration of a wellordered set after the single fixed choice of its ordinal indexing bijection.
```
def assignment (e : Table L Λ) (r : A → A → Prop) [IsWellOrder A r]
    (hb : Ordinal.type r ≤ Λ) (hc : Cardinal.mk A = Cardinal.mk L) : L ≃ A :=
…
```
Mentions: OAI.PartitionConsistency.OrderAssignment.Table

theorem OAI.PartitionConsistency.OrderAssignment.assignment_natural line 577

Source documentation

The same ordinal table entry is used under an arbitrary wellorder isomorphism. This is the naturality needed for tail-fixed codes.

theorem assignment_natural (e : Table L Λ) {r : A → A → Prop} {s : B → B → Prop}
    [IsWellOrder A r] [IsWellOrder B s]
    (hb : Ordinal.type r ≤ Λ) (hc : Cardinal.mk A = Cardinal.mk L)
    (hb' : Ordinal.type s ≤ Λ) (hc' : Cardinal.mk B = Cardinal.mk L)
    (f : r ≃r s) (j : L) :
    f (assignment e r hb hc j) = assignment e s hb' hc' j := by
…

Mentions: OAI.PartitionConsistency.OrderAssignment.Table, OAI.PartitionConsistency.OrderAssignment.assignment

def OAI.PartitionConsistency.OrderAssignment.smallRel line 597
Source documentation
Shrinking only changes the carrier; the selected relation is retained.
```
def smallRel (r : X → X → Prop) : Shrink.{u} X → Shrink.{u} X → Prop :=
…
```
instance OAI.PartitionConsistency.OrderAssignment.smallRel_isWellOrder line 600
def OAI.PartitionConsistency.OrderAssignment.smallIso line 608
Source documentation
The shrinking isomorphism of wellorders uses no new ordering choice.
```
def smallIso {r : X → X → Prop} {s : Y → Y → Prop} (f : r ≃r s) :
    smallRel.{u} r ≃r smallRel.{u} s where
…
```
def OAI.PartitionConsistency.OrderAssignment.smallAssignment line 618
Source documentation
Only the small ordinal of the shrunk relation indexes the table.
```
def smallAssignment (e : Table L Λ) (r : X → X → Prop) [IsWellOrder X r]
    (hb : Ordinal.type (smallRel.{u} r) ≤ Λ)
    (hc : Cardinal.mk (Shrink.{u} X) = Cardinal.mk L) : L ≃ X :=
…
```
Mentions: OAI.PartitionConsistency.OrderAssignment.Table
theorem OAI.PartitionConsistency.OrderAssignment.smallAssignment_natural line 623
theorem OAI.PartitionConsistency.OrderAssignment.type_smallRel_le line 636
Source documentation
An injection into the code set gives the stated ordinal bound when the wellorder of objects is the pullback of the code wellorder.
```
theorem type_smallRel_le {r : X → X → Prop} {s : Y → Y → Prop}
    [IsWellOrder X r] [IsWellOrder Y s] (f : r ↪r s) :
    Ordinal.type (smallRel.{u} r) ≤ Ordinal.type (smallRel.{u} s) := by
…
```