OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListRouteOutputBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual serialized output satisfies the source coefficient, coordinate and inverse-gap promise using the fixed-round compiler's proved estimates.

  1. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.compiled_polynomialPromise line 13