OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoundedTemplatePaths.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Continuous probe paths on an entire bounded Cartan box

The local inverse scheme is repeated after dividing logarithms by one fixed integer. Both the number of switches and their amplitudes are uniform over the scale and maximizing basis. Every path sample remains continuous in the original box coordinate, which supplies the measurable choices required in the independent-probe argument.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_continuous_bounded_template_coding line 32
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.template_path_family_from_word line 72
  3. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_continuous_bounded_template_paths line 109

    Source documentation

    Whole-box endpoint selectors with continuous samples, controlled length, and the prescribed template height range.

    theorem exists_continuous_bounded_template_paths
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput