OAI/NumberTheory/CubicMoment/Decomposition/StoppedPrimeBox.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cancellation of the actual free selected-bin prime with the complete two-stage stopping predicate. Only the cited Kummer prime input is used; the stopping restriction is removed by proved bin invariance.

  1. theorem OAI.CubicFirstMoment.long_stopped_selected_interval_saving line 14