OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCommonBundlePaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common-pivot paths for the actual successful source bundles

The chart is selected before the good sets. Both endpoint bridges use the same root displacement, and their error tends to zero with that displacement.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_common_bundle_profile_paths line 28