TemplateSymmetries.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite template-preserving group from the manuscript

Preserving the support exponent of every compact convex template is stronger than preserving only its values on segments. This file keeps those groups distinct and proves the required inclusion and finiteness.

def OAI.PolycyclicRecognition.templateSymmetryGroup line 23
Source documentation
The group in equation (support-symmetry-group) of boxes.tex.
```
def templateSymmetryGroup (D : SupportDatum W I B) : Subgroup (W ≃ₗ[ℝ] W) where
…
```
Mentions: OAI.PolycyclicRecognition.SupportDatum
theorem OAI.PolycyclicRecognition.templateSymmetry_mem_linearSupportSymmetry line 44
Source documentation
Every template symmetry is an isometry of the segment norm.
```
theorem templateSymmetry_mem_linearSupportSymmetry
    (D : SupportDatum W I B) (A : templateSymmetryGroup D) :
    A.val ∈ linearSupportSymmetryGroup D := by
…
```
Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.templateSymmetryGroup, OAI.PolycyclicRecognition.linearSupportSymmetryGroup
instance OAI.PolycyclicRecognition.finite_templateSymmetryGroup line 61