CartanUniformNeighborLabels.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform positive threshold for affine neighboring labels

structure OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow line 34

Source documentation

One affine supported pair together with its original sampling data. The fields record the actual maps, cells, root step and weak law; no neighbor-label conclusion is included.

structure AffineNeighborRow
    (π : G →* Multiplicative W)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (cell : Set W) (βcell : M.Bases)
    (X : I → H) {d : ℕ} (βD : WordBasisSelections X (boundedBracketWords d))
    (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
    (chartN : GroupLieAlgebra (𝓘(ℝ, F.N.modelSpace)) F.N.carrier ≃ₜ F.N.carrier)
    (hchartN : ∀ x, chartN x = F.ExpN x)
    (pivot : Fin M.letterCount → H) (shrink B δ : ℝ)
    (S : Set C((Fin (finrank ℝ H) → ℝ), W)) [MeasurableSpace S] [BorelSpace S] [BorelSpace (S × S)]
    {Λ : ℝ≥0} where
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_neighbor_label_threshold line 104
Source documentation
The shrinking-family contradiction gives a positive enlargement threshold uniform over all admissible sampling rows in the compact profile family. The reflection comparison uses the precisely stated published inputs.
```
theorem exists_uniform_neighbor_label_threshold
    (hExpG : IsGroupExponential ExpG) (hinjG : Function.Injective ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput