CartanSupportLegs.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Support legs in the actual Cartan subgroup

The canonical height section gives a one-parameter subgroup realizing any height displacement. Its continuity follows from the published faithful exponential representation, and its height traces the exact affine segment.

theorem OAI.PolycyclicRecognition.continuous_exp_line_of_published_realization line 31
Source documentation
Continuity of every actual exponential one-parameter subgroup.
```
theorem continuous_exp_line_of_published_realization
    [SimplyConnectedSpace G]
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
def OAI.PolycyclicRecognition.supportLegDirection line 50
Source documentation
The actual Cartan direction of a height displacement.
```
def supportLegDirection (w₀ w₁ : W) : H :=
…
```
theorem OAI.PolycyclicRecognition.supportLegDirection_height line 54

theorem OAI.PolycyclicRecognition.exists_cartan_support_leg_bound line 61

Source documentation

An actual one-parameter leg visits the requested height segment with uniform coarse speed at every scale and on every translated sheet.

theorem exists_cartan_support_leg_bound
    (π : G →* Multiplicative W)
    (hπ : ∀ x, (π (Exp x)).toAdd = eW (heightProjection T.character x))
    {E : Set W} (hE : Convex ℝ E) {w₀ w₁ : W} (hw₀ : w₀ ∈ E) (hw₁ : w₁ ∈ E) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (x : G) (r : ℝ), 0 ≤ r → (π x).toAdd = r • w₀ →
      let d := fun t : ℝ => Exp (t • (supportLegDirection T H eW w₀ w₁ :
…

Mentions: OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.supportLegDirection