RayIdealTemplates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

+# Negative-height templates for the actual ray ideal

The halfspace construction is applied to the actual Cartan weights on canonical height. Every word in the finite mixed-word spanning pool then has positive width. Consequently a fixed ideal displacement shrinks in every maximizing full word box, even after a polynomial loss.+

theorem OAI.PolycyclicRecognition.isMixedWord_mono line 22
theorem OAI.PolycyclicRecognition.CartanWordModel.exists_negative_ray_ideal_template line 43
Source documentation
The switch template stays in a fixed strictly negative halfspace and gives positive width to every word in the actual ray-ideal spanning pool.
```
theorem exists_negative_ray_ideal_template
    (α : W →L[ℝ] ℝ) (v₀ : W) (hα : α v₀ < 0) :
    let αH := α.toLinearMap.comp
…
```

theorem OAI.PolycyclicRecognition.CartanWordModel.fixed_ideal_polynomial_box_norm_tendsto_zero line 90

Source documentation

A fixed element of the actual ideal becomes arbitrarily small in the full maximizing boxes, including after any fixed polynomial loss.

theorem fixed_ideal_polynomial_box_norm_tendsto_zero
    (C : Set (H →ₗ[ℝ] ℝ)) (E : Set W)
    (hpos : ∀ w : M.coneMixedWords C, 0 < M.boxCost T hunimod eW E w.val)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (β : ℕ → M.Bases)
    (hβ : ∀ n, IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW E) (β n).val)
    (x : M.coneWordIdeal C) (A : ℝ) (hA : 0 ≤ A) (p : ℕ) :
    Tendsto (fun n : ℕ => A * (1 + (n : ℝ)) ^ p *
      ‖(M.boxBasis T hunimod eW E (β n) n).equivFun (x : cartanRootIdeal H)‖)
      atTop (𝓝 0) := by
…

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