GermSelectors.lean`

63 declarations, 0 contain sorry, 0 declared as axioms

PreAssignment

def OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalTable line 33
Source documentation
The bounded ground table depends on the component's fixed coding data, never on a condition or a moved generic computation.
```
def ordinalTable : OrderAssignment.Table (labelFiberSet v) (ordT).raw.rank :=
…
```
Mentions: OAI.PartitionConsistency.OrderAssignment.Table
def OAI.PartitionConsistency.ProductForcing.ChainCode.Preliminary line 38
Source documentation
j is assigned to the class named by τ at the local vertex w. Both ordinal values in this definition are forced values of actual names.
```
def Preliminary (d : CohenForcing.Condition I κ) (w : Vertex q)
    (j : labelFiberSet v) (τ : (S).Name) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_mono line 49
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_common line 59
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_congr line 65
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.ordinal_value_unique line 76
Source documentation
This equality concerns actual forced ordinal values. It is independent of the enumeration's arbitrary but once-for-all ground choices.
```
private theorem ordinal_value_unique (d : CohenForcing.Condition I κ) (τ : (S).Name)
    {θ ψ : Ordinal.{u}}
    (hθ : (S).atomic.EqF ((d,v.diagram) : Poset M I κ) τ (Name.check θ.toZFSet))
    (hψ : (S).atomic.EqF ((d,v.diagram) : Poset M I κ) τ (Name.check ψ.toZFSet)) : θ = ψ := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_eq_iff line 86
Source documentation
Injectivity and single-valuedness together: two assigned values are forced equal at the local vertex if and only if their ground labels agree.
```
theorem preliminary_eq_iff {d : CohenForcing.Condition I κ} {w : Vertex q}
    {j k : labelFiberSet v} {τ σ : (S).Name}
    (h : Preliminary hμ c hcard hsize hmerger hj E hE C d w j τ)
    (h' : Preliminary 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.Preliminary, OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_stable line 115
Source documentation
Every assigned local representative is eligible and keeps exactly the vertex's availability ideal at every stronger Cohen condition.
```
theorem preliminary_stable {d : CohenForcing.Condition I κ} {w : Vertex q}
    {j : labelFiberSet v} {τ : LocalName hμ c w.diagram}
    (h : Preliminary hμ c hcard hsize hmerger hj E hE C d w j τ.name) :
    (S).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.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Preliminary, OAI.PartitionConsistency.ProductForcing.labelSet, OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.SetLanguage.isClass, OAI.PartitionConsistency.ProductForcing.forcedAvailability
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_restrict line 125
Source documentation
Restrictions are the canonical identifications in the component.
```
theorem preliminary_restrict {d : CohenForcing.Condition I κ} {w z : Vertex q}
    (f : w.Arrow z) {j : labelFiberSet v} {τ : (S).Name}
    (h : Preliminary hμ c hcard hsize hmerger hj E hE C d z j τ) :
    Preliminary hμ c hcard hsize hmerger hj E hE C d w j τ := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.Preliminary
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_descend line 134
Source documentation
Local decision gives the converse when the representative is supported on the successor diagram.
```
theorem preliminary_descend {d : CohenForcing.Condition I κ} {w z : Vertex q}
    (f : w.Arrow z) {j : labelFiberSet v} {τ : LocalName hμ c z.diagram}
    (h : Preliminary hμ c hcard hsize hmerger hj E hE C d w j τ.name) :
    Preliminary 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.Preliminary
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_permute line 143
Source documentation
The equation for every member of the tail group, including its moved Cohen condition and moved vertex. Ground code order is unchanged.
```
theorem preliminary_permute (g : C.tailFixer hj) (d : CohenForcing.Condition I κ)
    (w : Vertex q) (j : labelFiberSet v) (τ : (S).Name)
    (h : Preliminary hμ c hcard hsize hmerger hj E hE C d w j τ) :
    Preliminary hμ c hcard hsize hmerger hj E hE C (d.permute g.val.val.val)
      (g.val.val • w) j (g.val.val.val • τ) := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.Preliminary
def OAI.PartitionConsistency.ProductForcing.ChainCode.OrdinalCount line 161
Source documentation
The exact cardinal-count hypothesis used by the two density proofs. It is a theorem for the concrete system (not a construction premise).
```
def OrdinalCount (d : CohenForcing.Condition I κ) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_total line 167
Source documentation
Dense totality at an arbitrary vertex of the component.
```
theorem preliminary_total (d : CohenForcing.Condition I κ)
    (hcount : OrdinalCount hμ c hcard hsize hmerger hj E hE C d)
    (w : Vertex q) (hw : Vertex.Common v w) (j : labelFiberSet v) :
    ∃ e, e ≤ d ∧ ∃ τ : LocalName hμ c w.diagram,
      Preliminary hμ c hcard hsize hmerger hj E hE C e w j τ.name := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.OrdinalCount, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Preliminary
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.preliminary_onto line 183
Source documentation
Dense surjectivity onto every persistent linked class, before any selector or coset representative is chosen.
```
theorem preliminary_onto (d : CohenForcing.Condition I κ)
    (hcount : OrdinalCount hμ c hcard hsize hmerger hj E hE C d)
    (w : Vertex q) (τ : (S).Name) (a : ChainCode hμ c C)
    (ha : Works hμ c hcard hsize hmerger hj E hE C d a)
    (hl : Links hμ c C d w τ a) :
    ∃ e, e ≤ d ∧ ∃ j : labelFiberSet v,
      Preliminary hμ c hcard hsize hmerger hj E hE C e w j τ := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.OrdinalCount, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Works, OAI.PartitionConsistency.ProductForcing.ChainCode.Links, OAI.PartitionConsistency.ProductForcing.ChainCode.Preliminary
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.fromRoot line 222
Source documentation
The unique contraction from the initial vertex to a chain vertex.
```
def fromRoot (i : ℕ) : Arrow v (C.vertex i) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Arrow
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.index line 225
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.fromRoot_index line 227
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.index_diagram line 229
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.index_transition line 232
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.index_zero line 236
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.Alignments line 242
Source documentation
These are the literal alignments of the moved chain with contractions of its initial vertex. There is no replacement relation assumed here.
```
def Alignments (hj : HasConditionalJoins (LeftDivOrder M))
    (π : componentStabilizer hj v) : Set (ℕ × M) :=
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.alignments_nonempty line 246
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.alignment_bounded line 255
Source documentation
Each alignment index is bounded by an original chain index.
```
theorem alignment_bounded (hj : HasConditionalJoins (LeftDivOrder M))
    (π : componentStabilizer hj v) {p : ℕ × M} (hp : p ∈ C.Alignments hj π) :
    ∃ N, p.2 ∣ C.index N := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.alignment_replacement line 265
Source documentation
Arbitrary cofinal advances are admissible replacements in the precise sense required by finite old-gate descent.
```
theorem alignment_replacement (hj : HasConditionalJoins (LeftDivOrder M))
    (π : componentStabilizer hj v) {p : ℕ × M} (hp : p ∈ C.Alignments hj π) (N : ℕ) :
    ∃ l' d, (l',p.2*d) ∈ C.Alignments hj π ∧ p.1 ≤ l' ∧
      C.index p.1*d = C.index l' ∧ C.index N ∣ p.2*d := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.coset_eq_of_alignment line 286
Source documentation
Having the same alignment identifies the two actual quotient cosets. This is independent of any choice of a descent path.
```
theorem coset_eq_of_alignment (hj : HasConditionalJoins (LeftDivOrder M))
    (π σ : componentStabilizer hj v) {p : ℕ × M}
    (hπ : p ∈ C.Alignments hj π) (hσ : p ∈ C.Alignments hj σ) :
    (QuotientGroup.mk' (C.tailFixer hj) π) = QuotientGroup.mk' (C.tailFixer hj) σ := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer
theorem OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.countable_quotient_of_gateTower line 307
Source documentation
Conditional use of the already proved finite gate descent. This is NOT an existence theorem for the countable-base rearrangement: the tower T and its base/terminal assertions are still explicit hypotheses. It shows exactly how such a rearrangement would finish the countable-germs argument.
```
theorem countable_quotient_of_gateTower
    (hj : HasConditionalJoins (LeftDivOrder M)) (T : GateTower.{u,t} M)
    (hbase : (T.stage 0 : Set M).Countable)
    (hn : ∀ i, C.index i ∈ T.stage 0)
    (hq : ∀ i j d, C.index i*d = C.index j → d ∈ T.stage 0)
    (ω : Ordinal.{t}) (hω : T.stage ω = ⊤) :
    Countable (componentStabilizer hj v ⧸ C.tailFixer hj) := by
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer
def OAI.PartitionConsistency.TailSelector.eventualSetoid line 351
Source documentation
Equality after discarding a finite initial segment of a sequence.
```
def eventualSetoid (A : Type*) : Setoid (ℕ → A) where
…
```
abbrev OAI.PartitionConsistency.TailSelector.Eventual line 359
def OAI.PartitionConsistency.TailSelector.eventualMk line 361
theorem OAI.PartitionConsistency.TailSelector.eventualMk_eq_iff line 363
structure OAI.PartitionConsistency.TailSelector.TailData line 370
Source documentation
The tails and the actual normal subgroup of eventual pointwise fixers. For components, these data are supplied by Chain.tailFixer_normal. No bijections or selector are included among the data.
```
structure TailData (G : Type u) (I : Type v) [Group G] [MulAction G I] where
…
```
instance OAI.PartitionConsistency.TailSelector.TailData.(instance at line 379) line 379
abbrev OAI.PartitionConsistency.TailSelector.TailData.Cosets line 381
abbrev OAI.PartitionConsistency.TailSelector.TailData.Nonidentity line 382
theorem OAI.PartitionConsistency.TailSelector.TailData.detector_exists line 386
Source documentation
The fixed representative of a nonidentity coset cannot fix any entire chain tail.
```
theorem detector_exists (δ : D.Nonidentity) (n : ℕ) :
    ∃ i ∈ D.tail n, δ.val.out • i ≠ i := by
…
```
def OAI.PartitionConsistency.TailSelector.TailData.detector line 393
theorem OAI.PartitionConsistency.TailSelector.TailData.detector_mem line 395
theorem OAI.PartitionConsistency.TailSelector.TailData.detector_moved line 398
theorem OAI.PartitionConsistency.TailSelector.TailData.detector_fixed_eventually line 402
abbrev OAI.PartitionConsistency.TailSelector.TailData.Pattern line 411
Source documentation
A pattern is a tuple of sequences of bounded binary rows, modulo eventual equality. The order later used on this type is fixed, not recomputed from rows.
```
abbrev Pattern (α : κ) := D.Nonidentity → Eventual (Set.Iio α → Bool)
```
Mentions: OAI.PartitionConsistency.TailSelector.Eventual
def OAI.PartitionConsistency.TailSelector.TailData.rawPattern line 413
theorem OAI.PartitionConsistency.TailSelector.TailData.rawPattern_congr line 416
def OAI.PartitionConsistency.TailSelector.TailData.pattern line 430
Source documentation
Evaluating at the standard representative is harmless: the preceding lemma proves independence of the representative.
```
def pattern (R : I → κ → Bool) (α : κ) (c : D.Cosets) : D.Pattern α :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.pattern_mk line 433
def OAI.PartitionConsistency.TailSelector.TailData.moveRows line 439
Source documentation
This is transport of the row data, not an automorphism of one fixed universe of evaluated symmetric names.
```
def moveRows (σ : G) (R : I → κ → Bool) : I → κ → Bool :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.rawPattern_moveRows line 442
theorem OAI.PartitionConsistency.TailSelector.TailData.pattern_covariance line 452
Source documentation
The actual pattern objects, not just their cardinalities, are identical under left multiplication in the quotient and transport of rows.
```
theorem pattern_covariance (σ : G) (R : I → κ → Bool) (α : κ) (c : D.Cosets) :
    D.pattern (moveRows σ R) α ((σ : D.Cosets) * c) = D.pattern R α c := by
…
```
Mentions: OAI.PartitionConsistency.TailSelector.TailData.moveRows
theorem OAI.PartitionConsistency.TailSelector.TailData.detector_separates line 459
Source documentation
Distinct cosets are detected at every sufficiently late position of one of the fixed detector sequences.
```
theorem detector_separates (g h : G) (hne : (g : D.Cosets) ≠ (h : D.Cosets)) :
    ∃ δ : D.Nonidentity, ∃ N, ∀ n, N ≤ n →
      g • D.detector δ n ≠ h • D.detector δ n := by
…
```

theorem OAI.PartitionConsistency.TailSelector.TailData.pair_separated line 478

Source documentation

Each pair is separated by every bound above one common countable bound. Only injectivity of the rows and countable boundedness of κ are used.

theorem pair_separated [Nonempty κ]
    (hbound : ∀ f : ℕ → κ, ∃ α, ∀ n, f n < α)
    (R : I → κ → Bool) (hR : Function.Injective R) (c e : D.Cosets) (hne : c ≠ e) :
    ∃ α : κ, ∀ β, α ≤ β → D.pattern R β c ≠ D.pattern R β e := by
…

theorem OAI.PartitionConsistency.TailSelector.TailData.distinguished_bound line 501
Source documentation
Countably many germs require only one strictly bounded collection of bits. No closure of the diagram forcing, or choice inside a symmetric model, is being assumed in this statement.
```
theorem distinguished_bound [Nonempty κ] [Countable D.Cosets]
    (hbound : ∀ f : ℕ → κ, ∃ α, ∀ n, f n < α)
    (R : I → κ → Bool) (hR : Function.Injective R) :
    ∃ α : κ, Function.Injective (D.pattern R α) := by
…
```
def OAI.PartitionConsistency.TailSelector.TailData.leastBound line 524
Source documentation
The first distinguishing bound in the fixed ordinal ordering. The proof of existence is an input only to this definition, not to its application to countable germs in distinguished_bound.
```
def leastBound (R : I → κ → Bool) (h : ∃ α, Function.Injective (D.pattern R α)) : κ :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.leastBound_distinguishes line 527
theorem OAI.PartitionConsistency.TailSelector.TailData.distinguishes_moveRows_iff line 533
theorem OAI.PartitionConsistency.TailSelector.TailData.leastBound_covariance line 547
def OAI.PartitionConsistency.TailSelector.TailData.bestCoset line 560
Source documentation
Minimization is on pattern objects with their fixed wellordering, not on an arbitrary ordering of the cosets.
```
def bestCoset (R : I → κ → Bool) (α : κ) : D.Cosets :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.bestCoset_minimal line 565
theorem OAI.PartitionConsistency.TailSelector.TailData.bestCoset_covariance line 571
def OAI.PartitionConsistency.TailSelector.TailData.selector line 592
Source documentation
The coset selected at the least distinguishing bound.
```
def selector (R : I → κ → Bool) (h : ∃ α, Function.Injective (D.pattern R α)) : D.Cosets :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.selector_covariance line 597
Source documentation
Source equation (coset-selector-covariance), proved with the actual row objects on both sides, including invariance of the least distinguishing bound.
```
theorem selector_covariance (σ : G) (R : I → κ → Bool)
    (h : ∃ α, Function.Injective (D.pattern R α))
    (h' : ∃ α, Function.Injective (D.pattern (moveRows σ R) α)) :
    D.selector (moveRows σ R) h' = (σ : D.Cosets) * D.selector R h := by
…
```
Mentions: OAI.PartitionConsistency.TailSelector.TailData.moveRows
theorem OAI.PartitionConsistency.TailSelector.TailData.moveRows_injective line 607
Source documentation
Transport preserves the distinguishing property of complete rows.
```
theorem moveRows_injective (σ : G) (R : I → κ → Bool) (hR : Function.Injective R) :
    Function.Injective (moveRows σ R) := by
…
```
Mentions: OAI.PartitionConsistency.TailSelector.TailData.moveRows
def OAI.PartitionConsistency.TailSelector.TailData.countableSelector line 615
Source documentation
With countability and regularity in hand the defining existence proof is provided by distinguished_bound, rather than assumed of the chosen patterns.
```
def countableSelector [Nonempty κ] [Countable D.Cosets]
    (hbound : ∀ f : ℕ → κ, ∃ α, ∀ n, f n < α)
    (R : I → κ → Bool) (hR : Function.Injective R) : D.Cosets :=
…
```
theorem OAI.PartitionConsistency.TailSelector.TailData.countableSelector_covariance line 620
def OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain.tailData line 640
Source documentation
The abstract tail data are supplied by the actual component stabilizer and the union of its pointwise tail fixers previously constructed.
```
def tailData (C : Chain v) (hj : HasConditionalJoins (LeftDivOrder M)) :
    TailData (componentStabilizer hj v) I where
…
```
Mentions: OAI.PartitionConsistency.LocalDiagramSystem.Vertex.Chain, OAI.PartitionConsistency.LocalDiagramSystem.Vertex.componentStabilizer