OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSourceBundleTerminals.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Source terminal paths from the actual successful coupled states

The source identity profile removes every source good-profile hypothesis. Only successful recurrence parameters and the proved pivot bridge rate remain.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_source_bundle_terminal_bounds line 31