OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSupportVisits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Controlled visits to actual Cartan support positions

Every letter displacement is realized by a continuous outward-switch-return path. The constants are uniform over the finite alphabet and polynomially bounded pivots. Canonical height remains exactly in the convex template.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cartan_support_visit_bound line 32

    Source documentation

    Actual single-letter visits, with no path or reachability input.

    theorem exists_cartan_support_visit_bound
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput