OAI/NumberTheory/CubicMoment/Angular/AngularStoppedCubeRoughness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual early-stopped row has a logarithmic reciprocal-prime exclusion bound. Zero coefficients are kept explicit rather than requiring roughness of an artificial ambient support.

  1. lemma OAI.CubicFirstMoment.angular_stopped_pair_prime_reciprocal_log line 17