OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanFacetProfileAgreement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual neighboring profiles agree on the contact facet

The source bridge is proved from the root distortion estimate, with the original deterministic generator step. No equality of affine labels or offsets is assumed here.

  1. theorem OAI.PolycyclicRecognition.affine_profiles_agree_on_contact_facet line 24