OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanRecurrenceBoxes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed denominator bound for the recurrence boxes

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_recurrence_box_enlargement line 33

    Source documentation

    Once the conjugated increment is in the unit normalized box, a single fixed enlargement controls every recurrence denominator. Its volume ratio is independent of the template, scale, suffix and increment law.

    theorem exists_recurrence_box_enlargement
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ R : ℝ, 1 ≤ R ∧ ∀ (E : Set W) (β : M.Bases),
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val → ∀ r : ℝ, 0 ≤ r →
      let B := M.groupBox T hunimod eW (Exp ∘ eN) E β r
…

    Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates