OAI/NumberTheory/DukePrimeDegree/Geometry/AdjacentFirstRoot.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A concrete first adjacent-root product step

The first adjacent root admits a neutral contracting diagonal direction. Starting the Gaussian chain with this root gives actual local charts to which the proved conditional-product theorem applies.

  1. theorem OAI.DukePrimeDegree.exists_complete_elimination_chain_from_initial line 20
  2. lemma OAI.DukePrimeDegree.adjacent_first_initial line 52
  3. lemma OAI.DukePrimeDegree.adjacent_first_pivots line 69
  4. def OAI.DukePrimeDegree.adjacentFirstTail line 77
  5. lemma OAI.DukePrimeDegree.adjacentFirstTail_final line 83
  6. lemma OAI.DukePrimeDegree.exists_adjacent_first_weights line 88