OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSeparatedTuples.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Controlled Cartan increments from separated endpoint tuples

The actual factor action gives the small-height corrections. The resulting measurable increment set retains the separate templates, its lower volume, and the original thickened lifts of every endpoint.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_controlled_increment_volume line 36