OAI/NumberTheory/DukePrimeDegree/Geometry/BilateralNeutralLifts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bilateral observation fibers have neutral relative displacement

The same small radial cells are used in both time directions. Uniqueness of the small lift identifies the two triangular lifts; their common lift commutes with the diagonal flow. This supplies the geometry needed to bound the entropy left over after the complete observation itinerary.

  1. lemma OAI.DukePrimeDegree.commute_diagonalOneParameter_of_weight_support line 20
  2. theorem OAI.DukePrimeDegree.exists_radial_radius_bilateral_neutral_lifts line 35