OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoundaryLeafComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The leaf bound from the constructed boundary volume comparisons

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.nilpotent_leaf_bound_of_boundary_comparisons line 32

    Source documentation

    The compact-shadow volume data provide all equal-set traces; there is no independent generator-action or leaf-bound premise.

    theorem nilpotent_leaf_bound_of_boundary_comparisons
    {P : Type*} [SimplyConnectedSpace G]
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput