OAI/NumberTheory/CubicMoment/Decomposition/StoppedCubeRoughness.lean

GitHub source file

3 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.primary_prime_factors_card_log line 14
  2. lemma OAI.CubicFirstMoment.rough_pair_prime_reciprocal_log line 22
  3. lemma OAI.CubicFirstMoment.stopped_pair_prime_reciprocal_log line 58