OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PrefactorSpacing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A nominal test at unit weight bounds the shared rational spacing even when the particular source has no edges. No approximation certificate for logarithm evaluation needs to be added to the construction interface.

  1. theorem OAI.ContinuumCoulomb.PrefactorCalibration.spacing_bounds line 13