ConcreteQuotients.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

CellDescent

theorem OAI.PartitionConsistency.ConservativeMonoids.Cell.descent_gate line 20

Source documentation

The old-input gate rule for the literal cells. A merger has no new old divisors; a probe's first-letter gate consumes all letters on an old input.

theorem descent_gate (w : d.extension) (hw : ∀ x, d.inclusion x ≠ w)
    (hb : ∃ y, w ∣ d.inclusion y) :
    ∃ g : M, w ∣ d.inclusion g ∧ (∀ y, w ∣ d.inclusion y → g ∣ y) ∧
      ∀ x, d.inclusion g ∣ w * d.inclusion x → ∃ y, w * d.inclusion x = d.inclusion y := by
…

theorem OAI.PartitionConsistency.ConservativeMonoids.Attachment.gateStep line 57
Source documentation
The same gate statement holds in the final monoid, by conservation of divisibility, including for final right factors not yet present at this cut.
```
theorem gateStep : OldGateStep S.submonoid R.submonoid := by
…
```

theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.finite_descent line 99

Source documentation

Finite old-gate descent in a rearranged literal cell tower. Right factors between base indices belong to the base by its conservative closure.

theorem finite_descent
    (hn : ∀ i, n i ∈ (D.stage ⊥).submonoid)
    (hbound : ∀ p ∈ A, ∃ N, p.2 ∣ n N)
    (hreplace : ∀ p ∈ A, ∀ N, ∃ l' d,
      (l',p.2*d) ∈ A ∧ p.1 ≤ l' ∧ n p.1*d = n l' ∧ n N ∣ p.2*d)
    (α : J) (p : ℕ × T) (hp : p ∈ A) (hα : p.2 ∈ (D.stage α).submonoid) :
    ∃ q ∈ A, q.2 ∈ (D.stage ⊥).submonoid ∧ Relation.ReflTransGen (Replaces n A) p q := by
…

theorem OAI.PartitionConsistency.ConservativeMonoids.CellTower.finite_descent_terminal line 128
theorem OAI.PartitionConsistency.MonoidConstruction.Saturation.cells_bottom_countable line 154
Source documentation
The fully executed construction still begins with the given countable base; flattening only inserts identity cuts between rounds.
```
theorem cells_bottom_countable [Countable M] :
    (((cells M K).stage ⊥).submonoid : Set (forgetMargins.obj (target M K))).Countable := by
…
```
Mentions: OAI.PartitionConsistency.MonoidConstruction.Saturation.cells, OAI.PartitionConsistency.MonoidConstruction.Saturation.target
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.countable_quotient_of_cells line 174
Source documentation
Finite gate descent, now applied in a literal rearrangement of the constructed monoid, bounds the actual germs by countably many alignments.
```
theorem countable_quotient_of_cells (D : CellTower M J)
    (hbot : ((D.stage ⊥).submonoid : Set M).Countable) :
    Countable (componentStabilizer M.joins v ⧸ C.tailFixer M.joins) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer
theorem OAI.PartitionConsistency.ConcreteSystem.countable_germs line 210
Source documentation
Countable germs for every local component in the actual final monoid; no rearrangement, countable-base, or gate assumptions remain.
```
theorem countable_germs {q : DiagramForcing.Diagram T I} {v : Vertex q}
    (C : Vertex.Chain v) :
    Countable (Vertex.componentStabilizer T.joins v ⧸ C.tailFixer T.joins) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram, OAI.PartitionConsistency.ConcreteSystem.T, OAI.PartitionConsistency.ConcreteSystem.I
instance OAI.PartitionConsistency.ConcreteSystem.(instance at line 231) line 231
theorem OAI.PartitionConsistency.ConcreteSystem.κ_countable_bound line 234
theorem OAI.PartitionConsistency.ConcreteSystem.κ_initial_countable line 238
theorem OAI.PartitionConsistency.ConcreteSystem.component_selector_dense line 249
Source documentation
Each actual component chain has a dense set of conditions at which the least distinguishing-bound construction selects one of its countably many residual symmetries.
```
theorem component_selector_dense (p : CohenForcing.Condition I κ) :
    ∃ r, r ≤ p ∧ (C.tailData T.joins).Good r := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ConcreteSystem.I, OAI.PartitionConsistency.ConcreteSystem.κ
theorem OAI.PartitionConsistency.ConcreteSystem.component_selected_covariant line 256
Source documentation
The selected coset is unique on compatible conditions and transforms by left multiplication when the Cohen condition is moved.
```
theorem component_selected_covariant (p : CohenForcing.Condition I κ)
    (c : (C.tailData T.joins).Cosets)
    (hp : (C.tailData T.joins).Selected p c)
    (σ : Vertex.componentStabilizer T.joins v) :
    (C.tailData T.joins).Selected (p.permute σ.val.val)
      ((σ : (C.tailData T.joins).Cosets) * c) :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ConcreteSystem.I, OAI.PartitionConsistency.ConcreteSystem.κ

theorem OAI.PartitionConsistency.ConcreteSystem.code_ordinalType_cardinal line 281

Source documentation

Every possible order type has cardinality exactly the label-fiber cardinal. The hypotheses are just the outside-list condition at which the quotient construction is made, and a stronger initial Cohen condition.

theorem code_ordinalType_cardinal {q : Diagram T I} {v : Vertex q} (C : Vertex.Chain v)
    (b : T) (hb : b ≠ 1) (E : S.Name)
    (hE : ∀ π ∈ SupportFilter.Fix (q.sub T.e).range, π • E = E)
    (t : Diagram T I) (ht : t.sub b = q.sub T.e)
    (d₀ : CohenForcing.Condition I κ) (hd₀ : d₀.support ⊆ t.range)
    (j : I) (hj : j ∈ t.range)
    (hout : ∀ z : P, z ≤ (d₀,t) →
      ¬ S.atomic.MemF z (labelClass aleph0_le_μ (posetCode κ) E j)
        (localList aleph0_le_μ (posetCode κ) cardinal_T.le (q.sub T.e)))
    (d : CohenForcing.Condition I κ) (hd : d ≤ d₀.restrict (q.sub T.e).range)
    (θ : Ordinal)
    (hθ : S.atomic.EqF ((d,v.diagram) : P)
…

Mentions: OAI.PartitionConsistency.ConcreteSystem.T, OAI.PartitionConsistency.ConcreteSystem.I, OAI.PartitionConsistency.SupportFilter.Fix, OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ConcreteSystem.κ, OAI.PartitionConsistency.ConcreteSystem.P

theorem OAI.PartitionConsistency.ConcreteSystem.labelFiberSet_cardinal line 325
Source documentation
The literal common label subset has the advertised cardinality, not merely an abstract isomorphic fiber.
```
theorem labelFiberSet_cardinal {q : Diagram T I} (v : Vertex q) :
    Cardinal.mk (labelFiberSet v) = μ := by
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.T, OAI.PartitionConsistency.ConcreteSystem.I

theorem OAI.PartitionConsistency.ConcreteSystem.preliminary_ordinalCount line 339

Source documentation

The count needed for assigning the preliminary ranks is supplied by the executed construction and the outside-list condition.

theorem preliminary_ordinalCount {q : Diagram T I} {v : Vertex q} (C : Vertex.Chain v)
    (b : T) (hb : b ≠ 1) (E : S.Name)
    (hE : ∀ π ∈ SupportFilter.Fix (q.sub T.e).range, π • E = E)
    (t : Diagram T I) (ht : t.sub b = q.sub T.e)
    (d₀ : CohenForcing.Condition I κ) (hd₀ : d₀.support ⊆ t.range)
    (j : I) (hj : j ∈ t.range)
    (hout : ∀ z : P, z ≤ (d₀,t) →
      ¬ S.atomic.MemF z (labelClass aleph0_le_μ (posetCode κ) E j)
        (localList aleph0_le_μ (posetCode κ) cardinal_T.le (q.sub T.e)))
    (d : CohenForcing.Condition I κ) (hd : d ≤ d₀.restrict (q.sub T.e).range) :
    ChainCode.OrdinalCount aleph0_le_μ (posetCode κ) cardinal_T.le size_lt finiteMergers
      T.joins E (supported_mono aleph0_le_μ (q.self_le_sub T.e) E hE) C d := by
…

theorem OAI.PartitionConsistency.ConcreteSystem.quotient_bijection_above line 369

Source documentation

All count and selector hypotheses of the equivariant assignment are satisfied by the executed construction. The condition used for the graph retains exactly the Cohen information in the smaller root.

theorem quotient_bijection_above (q : Diagram T I) (b : T) (hb : b ≠ 1) (E : S.Name)
    (hE : ∀ π ∈ SupportFilter.Fix (q.sub T.e).range, π • E = E)
    (t : Diagram T I) (ht : t.sub b = q.sub T.e)
    (d₀ : CohenForcing.Condition I κ) (hd₀ : d₀.support ⊆ t.range)
    (j : I) (hj : j ∈ t.range)
    (hout : ∀ z : P, z ≤ (d₀,t) →
      ¬ S.atomic.MemF z (labelClass aleph0_le_μ (posetCode κ) E j)
        (localList aleph0_le_μ (posetCode κ) cardinal_T.le (q.sub T.e))) :
    ∃ f : S.Name, S.Forces ![f,labelSet aleph0_le_μ (posetCode κ),
      quotientName aleph0_le_μ (posetCode κ) E] ((d₀.restrict (q.sub T.e).range,q) : P)
      ((SetLanguage.surjection 0 1 2).conj (SetLanguage.injection 0 1 2)) := by
…

theorem OAI.PartitionConsistency.ConcreteSystem.nonwellorderable_quotient_bijection line 401
Source documentation
Densely below every condition which forces a quotient to be nonwellorderable, there is an actual supported graph bijecting the label set with that quotient. There is no inaccessible-cardinal or quotient-classification premise.
```
theorem nonwellorderable_quotient_bijection (E : S.Name) (s : P)
    (hno : S.Forces ![quotientName aleph0_le_μ (posetCode κ) E] s
      (SetLanguage.wellorderable 0).neg) :
    ∃ r, r ≤ s ∧ ∃ f : S.Name,
      S.Forces ![f,labelSet aleph0_le_μ (posetCode κ),
        quotientName aleph0_le_μ (posetCode κ) E] r
        ((SetLanguage.surjection 0 1 2).conj (SetLanguage.injection 0 1 2)) := by
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.ConcreteSystem.κ, OAI.PartitionConsistency.SetLanguage.wellorderable, OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.injection