CartanSegmentExponent.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact source exponent of Cartan segment boxes

theorem OAI.PolycyclicRecognition.CartanWordModel.boxCost_segment line 23
Source documentation
The exponents of the actual segment construction equal the canonical height-segment support exponents.
```
theorem boxCost_segment (v : H) :
    M.boxCost T hunimod e (segment ℝ 0 (e (heightProjection T.character v))) =
      fun w : M.wordList => bracketWordExponent (M.segmentSupportExponent v) w := by
…
```
Mentions: OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.bracketWordExponent

theorem OAI.PolycyclicRecognition.CartanWordModel.maximizing_segment_exponent line 35

Source documentation

A maximizing segment box has precisely the support-profile exponent.

theorem maximizing_segment_exponent
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (v : H) (β : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (fun w : M.wordList => bracketWordExponent (M.segmentSupportExponent v) w) β.val) :
    columnBasisWeight
      (fun w : M.wordList => bracketWordExponent (M.segmentSupportExponent v) w) β.val =
      (M.supportIn T hunimod e).segmentSupport (e (heightProjection T.character v)) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.columnBasisWeight, OAI.PolycyclicRecognition.heightProjection