OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceHubbardPromise.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

End-to-end promise accounting from a Hubbard interval for the literal source output. All errors use the actual fixed-power precision schedules.

  1. theorem OAI.ContinuumCoulomb.SourceUnitCoulomb.promise_of_hubbard_interval line 13