OAI/NumberTheory/CubicMoment/Angular/AngularScaleFirstStopping.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual low scale-first rows satisfy the two-stage stopping identity. The no-stop prefix test and both independent stopped matrices are retained exactly.

  1. theorem OAI.CubicFirstMoment.angular_distinguishedScaleRow_two_stage line 18
  2. theorem OAI.CubicFirstMoment.angular_distinguishedLowScaleRows_two_stage line 69