CartanAlternatingSchemes.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The full limiting multiplication map is selected before any restriction to good profiles or any choice of separated target tuples.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_alternating_box_scheme line 35
Source documentation
The actual two boxes have a common subsequence and a full alternating submersion. Only their intrinsic exponential representation and Haar chart are taken from published inputs.
```
theorem exists_alternating_box_scheme
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.alternating_submersion_length_pos line 101
Source documentation
A submersion to positive-dimensional coordinates has at least one block.
```
theorem alternating_submersion_length_pos {n h c : ℕ} (hn : 0 < n)
    (a : DynkinCoefficients c 2) (p : AlternatingLawData n)
    (z : Fin h → (Fin n → ℝ) × (Fin n → ℝ))
    (hs : Function.Surjective (fderiv ℝ (alternatingCoordinateProduct a p.1 p.2.1 p.2.2) z)) :
    0 < h := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.AlternatingLawData, OAI.PolycyclicRecognition.alternatingCoordinateProduct