OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourcePromiseBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed exponent choices absorb all three physical simulation errors inside the margin retained by the positive-spin source program.

  1. theorem OAI.ContinuumCoulomb.physical_promise_error_budget line 11