StableSelectors.lean`

63 declarations, 0 contain sorry, 0 declared as axioms

ConditionSelector

def OAI.PartitionConsistency.CohenForcing.Condition.rows line 21
Source documentation
A convenient total extension of a partial condition. This is auxiliary row data, NOT the generic rows; only values in the domain will be used to make a persistent decision.
```
def rows (p : Condition I κ) (i : I) (a : κ) : Bool :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.rows_of_mem line 24
theorem OAI.PartitionConsistency.CohenForcing.Condition.rows_eq_of_le line 31
theorem OAI.PartitionConsistency.CohenForcing.Condition.rows_permute line 36
theorem OAI.PartitionConsistency.CohenForcing.Condition.dom_mono line 40
def OAI.PartitionConsistency.CohenForcing.Condition.fill line 46
Source documentation
Fill only the as-yet-undefined places in a prescribed countable set.
```
def fill (p : Condition I κ) (A : Set (I × κ)) (hA : A.Countable) : Condition I κ where
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.fill_le line 59
theorem OAI.PartitionConsistency.CohenForcing.Condition.subset_dom_fill line 62
theorem OAI.PartitionConsistency.TailSelector.TailData.representative_eventually line 82
Source documentation
Eventually the canonical representative of a coset acts just like any other representative on each detector sequence.
```
theorem representative_eventually (g : G) (δ : D.Nonidentity) :
    ∃ N, ∀ n, N ≤ n → (g : D.Cosets).out • D.detector δ n = g • D.detector δ n := by
…
```
def OAI.PartitionConsistency.TailSelector.TailData.Complete line 92
Source documentation
Every bounded detector row is completely assigned after a finite initial segment. The quantifier over all representatives makes covariance literal.
```
def Complete (p : Condition I κ) (α : κ) : Prop :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.Complete.mono line 96
theorem OAI.PartitionConsistency.TailSelector.TailData.Complete.downward line 102
theorem OAI.PartitionConsistency.TailSelector.TailData.Complete.pattern_eq line 109
Source documentation
Assigned bounded patterns cannot be altered by an extension.
```
theorem Complete.pattern_eq {p q : Condition I κ} {α : κ}
    (h : D.Complete p α) (hqp : q ≤ p) : D.pattern q.rows α = D.pattern p.rows α := by
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.Complete.permute line 117
theorem OAI.PartitionConsistency.TailSelector.TailData.rows_permute line 129
def OAI.PartitionConsistency.TailSelector.TailData.Good line 137
Source documentation
A good condition actually decides a distinguishing pattern; arbitrary unassigned row values are never used for a stable selection.
```
def Good (p : Condition I κ) : Prop :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.Good.mono line 140
theorem OAI.PartitionConsistency.TailSelector.TailData.Good.permute line 145
def OAI.PartitionConsistency.TailSelector.TailData.detectorSites line 153
Source documentation
The countable coordinate family used by the fixed representatives.
```
def detectorSites : Set I :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.detectorSites_countable line 156
theorem OAI.PartitionConsistency.TailSelector.TailData.detectorSite_mem line 159
theorem OAI.PartitionConsistency.TailSelector.TailData.complete_of_covered line 162
theorem OAI.PartitionConsistency.TailSelector.TailData.bounded_countable line 170
theorem OAI.PartitionConsistency.TailSelector.TailData.good_dense line 183
Source documentation
In one countable extension all relevant unequal detector sites acquire opposite bits below a common countable bound. This argument does not assume that the ambient universe already contains distinct rows on all of I.
```
theorem good_dense [Nonempty κ] [Uncountable κ] [Countable D.Cosets]
    (hbound : ∀ f : ℕ → κ, ∃ α, ∀ n, f n < α)
    (hcount : ∀ α : κ, (Set.Iio α).Countable) (p : Condition I κ) :
    ∃ q, q ≤ p ∧ D.Good q := by
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.leastBound_le line 222
def OAI.PartitionConsistency.TailSelector.TailData.conditionSelector line 228
Source documentation
This candidate does not yet mention a generic filter.
```
def conditionSelector (p : Condition I κ) (h : D.Good p) : D.Cosets :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.Good.complete_least line 231

theorem OAI.PartitionConsistency.TailSelector.TailData.leastBound_extension line 237

Source documentation

The first distinguishing bound is persistent, not an artifact of how undefined rows were filled.

theorem leastBound_extension {p q : Condition I κ} (hp : D.Good p) (hq : D.Good q)
    (hqp : q ≤ p) :
    D.leastBound q.rows ⟨hq.choose,hq.choose_spec.2⟩ =
      D.leastBound p.rows ⟨hp.choose,hp.choose_spec.2⟩ := by
…

theorem OAI.PartitionConsistency.TailSelector.TailData.bestCoset_congr line 254

theorem OAI.PartitionConsistency.TailSelector.TailData.conditionSelector_extension line 261

Source documentation

Every stronger condition makes the same coset decision.

theorem conditionSelector_extension {p q : Condition I κ} (hp : D.Good p) (hq : D.Good q)
    (hqp : q ≤ p) : D.conditionSelector q hq = D.conditionSelector p hp := by
…

theorem OAI.PartitionConsistency.TailSelector.TailData.conditionSelector_permute line 268

Source documentation

Genuine covariance of the persistent decision made by a Cohen condition.

theorem conditionSelector_permute (p : Condition I κ) (hp : D.Good p) (σ : G)
    (hq : D.Good (p.permute (MulAction.toPerm σ))) :
    D.conditionSelector (p.permute (MulAction.toPerm σ)) hq =
      (σ : D.Cosets) * D.conditionSelector p hp := by
…

def OAI.PartitionConsistency.TailSelector.TailData.Selected line 282
Source documentation
The downward-persistent relation that can be used as a name recipe.
```
def Selected (p : Condition I κ) (c : D.Cosets) : Prop :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.Selected.mono line 285
theorem OAI.PartitionConsistency.TailSelector.TailData.selected_unique line 290
theorem OAI.PartitionConsistency.TailSelector.TailData.Selected.permute line 296
theorem OAI.PartitionConsistency.TailSelector.TailData.selected_compatible line 302
instance OAI.PartitionConsistency.CohenForcing.Condition.coordinateAction line 317
theorem OAI.PartitionConsistency.CohenForcing.Condition.smul_condition line 321
def OAI.PartitionConsistency.CosetPredicate.shift line 330
theorem OAI.PartitionConsistency.CosetPredicate.shift_one line 332
theorem OAI.PartitionConsistency.CosetPredicate.shift_mul line 336
theorem OAI.PartitionConsistency.CosetPredicate.shift_at_moved line 341
def OAI.PartitionConsistency.CosetPredicate.Invariant line 345
theorem OAI.PartitionConsistency.CosetPredicate.shift_eq line 348
abbrev OAI.PartitionConsistency.ProductForcing.ChainCode.AssignmentPoint line 387
def OAI.PartitionConsistency.ProductForcing.ChainCode.preliminaryPoint line 389
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminaryPoint_move line 392
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminaryPoint_invariant line 401
def OAI.PartitionConsistency.ProductForcing.ChainCode.Corrected line 413
Source documentation
The persistent selected-coset version of the assignment predicate.
```
def Corrected (d : CohenForcing.Condition I κ) (w : Vertex q)
    (j : labelFiberSet v) (τ : (S).Name) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_selected line 419
Source documentation
Independence of the representative of the selected coset.
```
theorem corrected_selected {d : CohenForcing.Condition I κ} {w : Vertex q}
    {j : labelFiberSet v} {τ : (S).Name} (g : G)
    (hg : (C.tailData hj).Selected d (g : G ⧸ K)) :
    Corrected hμ c hcard hsize hmerger hj E hE C d w j τ ↔
      Preliminary hμ c hcard hsize hmerger hj E hE C
        (g⁻¹ • d) (g⁻¹ • w) (g⁻¹ • j) (g⁻¹ • τ) := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.Selected, OAI.PartitionConsistency.ProductForcing.ChainCode.Corrected, OAI.PartitionConsistency.ProductForcing.ChainCode.Preliminary
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_mono line 438
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_common line 446

theorem OAI.PartitionConsistency.ProductForcing.ChainCode.root_eq_symmetry line 458

Source documentation

Equality transport at a moved vertex, with the moved Cohen coordinate.

theorem root_eq_symmetry (g : Vertex.RootGroup q) (d : CohenForcing.Condition I κ)
    (w : Vertex q) (τ σ : (S).Name) :
    (S).atomic.EqF ((g • d,(g • w).diagram) : Poset M I κ) (g • τ) (g • σ) ↔
      (S).atomic.EqF ((d,w.diagram) : Poset M I κ) τ σ := by
…

Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.Poset

theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_congr line 469

theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_eq_iff line 480

Source documentation

Both injectivity and single-valuedness survive coset correction.

theorem corrected_eq_iff {d : CohenForcing.Condition I κ} {w : Vertex q}
    {j k : labelFiberSet v} {τ σ : (S).Name}
    (h : Corrected hμ c hcard hsize hmerger hj E hE C d w j τ)
    (h' : Corrected hμ c hcard hsize hmerger hj E hE C d w k σ) :
    (S).atomic.EqF ((d,w.diagram) : Poset M I κ) τ σ ↔ j = k := by
…

Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.Corrected, OAI.PartitionConsistency.ProductForcing.Poset

theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_permute line 491

Source documentation

Covariance under every element of the entire component stabilizer.

theorem corrected_permute (g : G) (d : CohenForcing.Condition I κ) (w : Vertex q)
    (j : labelFiberSet v) (τ : (S).Name)
    (h : Corrected hμ c hcard hsize hmerger hj E hE C d w j τ) :
    Corrected hμ c hcard hsize hmerger hj E hE C
      (g • d) (g • w) (g • j) (g • τ) := by
…

Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.Corrected

theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_restrict line 511
Source documentation
Pullback along a contraction retains precisely the same representative.
```
theorem corrected_restrict {d : CohenForcing.Condition I κ} {w z : Vertex q}
    (f : w.Arrow z) {j : labelFiberSet v} {τ : (S).Name}
    (h : Corrected hμ c hcard hsize hmerger hj E hE C d z j τ) :
    Corrected hμ c hcard hsize hmerger hj E hE C d w j τ := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.Corrected
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.corrected_descend line 519
Source documentation
Reflection along a contraction for a name already supported on its target.
```
theorem corrected_descend {d : CohenForcing.Condition I κ} {w z : Vertex q}
    (f : w.Arrow z) {j : labelFiberSet v} {τ : LocalName hμ c z.diagram}
    (h : Corrected hμ c hcard hsize hmerger hj E hE C d w j τ.name) :
    Corrected hμ c hcard hsize hmerger hj E hE C d z j τ.name := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Corrected
theorem OAI.PartitionConsistency.ProductForcing.forcedAvailable_permute_iff line 550
Source documentation
Moving the entire local equality test also moves its normalized witness.
```
theorem forcedAvailable_permute_iff (π : Equiv.Perm I)
    (d : CohenForcing.Condition I κ) (r : Diagram M I) (τ : LocalName hμ c r) (n : M) :
    ForcedAvailable hμ c (d.permute π) (r.permute π) (τ.transport hμ π) n ↔
      ForcedAvailable hμ c d r τ n := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ForcedAvailable
theorem OAI.PartitionConsistency.ProductForcing.forcedAvailability_permute line 568
Source documentation
The actual ideal is preserved, not merely its cardinality.
```
theorem forcedAvailability_permute (π : Equiv.Perm I)
    (d : CohenForcing.Condition I κ) (r : Diagram M I) (a : M) (τ : LocalName hμ c r) :
    forcedAvailability hμ c hcard hsize hmerger (d.permute π) (r.permute π) a
        (τ.transport hμ π) = forcedAvailability hμ c hcard hsize hmerger d r a τ := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.forcedAvailability
def OAI.PartitionConsistency.ProductForcing.StableAt line 581
Source documentation
An actual local class whose availability has become permanent. Keeping the literal name as an argument avoids any chosen representative under transport between vertices.
```
def StableAt (E : (S).Name) (d : CohenForcing.Condition I κ) (w : Vertex q)
    (τ : (S).Name) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition

theorem OAI.PartitionConsistency.ProductForcing.stableAt_permute line 589

Source documentation

This permutation is allowed to move the component as well as its chain.

theorem stableAt_permute (E : (S).Name)
    (hE : ∀ π ∈ SupportFilter.Fix q.range, π • E = E)
    (g : Vertex.RootGroup q) (d : CohenForcing.Condition I κ) (w : Vertex q) (τ : (S).Name)
    (h : StableAt hμ c hcard hsize hmerger E d w τ) :
    StableAt hμ c hcard hsize hmerger E (g • d) (g • w) (g • τ) := by
…

Mentions: OAI.PartitionConsistency.SupportFilter.Fix, OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.StableAt

theorem OAI.PartitionConsistency.ProductForcing.stableAt_permute_iff line 619