OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSegmentSupportTimes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The prescribed segment endpoints are actual root support positions

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.segment_visit_direction_support line 23

    Source documentation

    The support time is chosen on the original horizontal line. Its scaled Cartan direction has the exact root height required by the switch estimate.

    theorem segment_visit_direction_support
    (v : H) (w₀ : W) {T₀ : ℝ} (hT₀ : 0 ≤ T₀) (i : Fin M.letterCount) :
    let u := eW (heightProjection T.character (v : L))
…

    Mentions: OAI.PolycyclicRecognition.heightProjection