OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSamplingFacet.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual contact pivot and active constraints of the sampling cell

  1. theorem OAI.PolycyclicRecognition.exists_sampling_contact_facet line 13
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_sampling_contact_pivot line 37

    Source documentation

    Every generator facet has a concrete Cartan pivot. All constraints active there are positive multiples of that generator's height weight.

    theorem exists_sampling_contact_pivot (i : Fin M.letterCount) :
    let D := M.supportIn T hunimod eW
…