OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanContactProbeBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The bridge at the prescribed inward contact pivot

  1. theorem OAI.PolycyclicRecognition.exists_contact_pivot_probe_bridge line 25

    Source documentation

    The scalar action is constructed, and the pivot is explicitly r (1-cδ) h₀. Its logarithm has a uniform linear bound for cδ ≤ 1. Only the cited exponential, Dynkin and representation inputs remain.

    theorem exists_contact_pivot_probe_bridge
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput