OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanRootNeighborLabels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Labels agree for supported root-neighbor profiles on a closed cell

The root distortion estimate proves contact-facet agreement and supplies the pivot bridge. The actual coupled-volume theorem then rules out the reflection alternative. No neighboring-label assertion is assumed.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.supported_root_neighbor_labels_eq line 39