ZeroWidthQuotientBoxes.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual quotient images of zero-width Cartan boxes

Mixed words vanish in the cone quotient. Every remaining word has exponent zero, so projection of a full box has a radius independent of the scale.

theorem OAI.PolycyclicRecognition.exists_zero_width_word_projection_bound line 25

Source documentation

A linear projection annihilating all words with nonzero cost has a uniform norm bound on every rescaled word basis.

theorem exists_zero_width_word_projection_bound
    (X : I → L) (S : Finset (FreeMagma I)) (q : L →ₗ[ℝ] V) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (β : WordBasisSelections X S) (cost : S → ℝ),
      (∀ w : S, q (evalBracketWord X w) ≠ 0 → cost w = 0) →
      ∀ (r : ℝ) (v : L), ‖q v‖ ≤ C *
        ‖(exponentialRescaleBasis (WordBasisSelections.basis X S β)
          (fun j => cost (β.val j)) r).equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis

theorem OAI.PolycyclicRecognition.CartanWordModel.coneProjection_word_cost_eq_zero line 77
Source documentation
A word survives the cone projection only when all its letters are inside the cone, hence has cost zero under the stated letter costs.
```
theorem coneProjection_word_cost_eq_zero
    (s : Fin M.letterCount → ℝ)
    (hzero : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C → s i = 0)
    (w : FreeMagma (Fin M.letterCount))
    (hw : M.coneProjection C (evalBracketWord M.letter w) ≠ 0) :
    bracketWordExponent s w = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.bracketWordExponent

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cone_quotient_box_bound line 94

Source documentation

The true group quotient sends every zero-width full box into a fixed multiple of the quotient logarithmic box. Neither the radius nor the constant contains an exponential scale factor.

theorem exists_cone_quotient_box_bound {N Q : Type*} [Group N] [Group Q]
    (ExpN : cartanRootIdeal H → N)
    (ExpQ : ((cartanRootIdeal H) ⧸ M.coneWordIdeal C) → Q)
    (π : N →* Q) (hπ : ∀ v, π (ExpN v) = ExpQ (M.coneProjection C v))
    {n : ℕ} (bQ : Basis (Fin n) ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal C)) :
    ∃ A : ℝ, 0 ≤ A ∧ ∀ (β : M.Bases) (s : Fin M.letterCount → ℝ),
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C → s i = 0) →
      ∀ r R : ℝ, π '' exponentialCoordinateBox ExpN
        (exponentialRescaleBasis (WordBasisSelections.basis M.letter M.wordList β)
          (fun j => bracketWordExponent s (β.val j)) r) R ⊆
        exponentialCoordinateBox ExpQ bQ (A * R) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.bracketWordExponent