TemplateWeightRays.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PolycyclicRecognition.templateSymmetry_weight_ray line 21
Source documentation
The cap argument from the support-symmetries lemma: pullback of every nonzero generator weight is a positive multiple of another generator weight. It uses preservation of all compact convex templates, not only segments.
```
theorem templateSymmetry_weight_ray
    (D : SupportDatum W I B) (A : templateSymmetryGroup D)
    (j : I) (hj : D.weight j ≠ 0) :
    ∃ (i : I) (r : ℝ), 0 < r ∧ (D.weight j).comp A.val.toLinearMap = r • D.weight i := by
…
```
Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.templateSymmetryGroup