OAI/NumberTheory/DukePrimeDegree/Geometry/AdjacentFirstProduct.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An unconditional adjacent-root product in actual Gaussian boxes

The neutral weights and remaining elimination chain are constructed explicitly. Every point of this chart lies in a bounded actual quotient box whose pulled-back conditional measure splits at the first root.

  1. lemma OAI.DukePrimeDegree.adjacentRootNe line 20
  2. theorem OAI.DukePrimeDegree.adjacent_first_conditional_product line 22
  3. theorem OAI.DukePrimeDegree.exists_adjacent_first_product_box line 38