CartanBoundaryRayMatching.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The missing generator ray for each template symmetry

theorem OAI.PolycyclicRecognition.CartanWordModel.support_weight_comp_height line 36
Source documentation
The original Cartan generator characters are exactly the pullbacks of the chosen Euclidean height coordinates.
```
theorem support_weight_comp_height (j : Fin M.letterCount) :
    (α j).comp θ = (M.weight j : H →ₗ[ℝ] ℝ) := by
…
```

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_template_missing_generators line 46

Source documentation

The template symmetry decides which one target ray can see a given generator; every other boundary action kills that entire generator flow.

theorem exists_template_missing_generators
    (A : templateSymmetryGroup (M.supportIn T hunimod eW))
    (R : ∀ i, M.RayBoundaryModel F (((α i).comp A.val.toLinearMap).comp θ)) :
    ∃ missing : Fin M.letterCount → Fin M.letterCount,
      ∀ j i, α i ∉ positiveWeightRay (α (missing j)) →
        ∀ t : ℝ, (R i).action
          (ExpG (t • (M.letter j : GroupLieAlgebra (𝓘(ℝ, EG)) G))) = 1 := by
…

Mentions: OAI.PolycyclicRecognition.templateSymmetryGroup, OAI.PolycyclicRecognition.positiveWeightRay