OAI/NumberTheory/CubicMoment/Decomposition/DistinguishedPrimeZero.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A distinguished prime row is empty outside its forced complementary norm range. This keeps the later mass sum linear in the output length.

  1. lemma OAI.CubicFirstMoment.stoppedDistinguished_row_eq_zero line 12