OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CalibrationCoulombBrackets.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Explicit rational search intervals for the actual Coulomb-calibrated hopping target. The fixed exponent simultaneously enforces the separated two-site denominator and both endpoint signs.

  1. theorem OAI.ContinuumCoulomb.CalibrationRationalBracket.exists_coulomb_brackets line 13