OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/AffinePhysicalOutput.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A canonical unit-charge instance with the complete physical scalar offset. The coordinate and threshold metadata remain explicit until the source program supplies the same fixed polynomial scales to both components.

  1. abbrev OAI.ContinuumCoulomb.AffinePhysicalOutput.Input line 13
  2. def OAI.ContinuumCoulomb.AffinePhysicalOutput.inputCode line 15
  3. def OAI.ContinuumCoulomb.AffinePhysicalOutput.argument line 18
  4. def OAI.ContinuumCoulomb.AffinePhysicalOutput.value line 21
  5. opaque OAI.ContinuumCoulomb.AffinePhysicalOutput.argumentProgram line 24
  6. opaque OAI.ContinuumCoulomb.AffinePhysicalOutput.program line 32
  7. def OAI.ContinuumCoulomb.AffinePhysicalOutput.certificate line 36
  8. theorem OAI.ContinuumCoulomb.AffinePhysicalOutput.nuclei line 40
  9. theorem OAI.ContinuumCoulomb.AffinePhysicalOutput.electrons line 43
  10. theorem OAI.ContinuumCoulomb.AffinePhysicalOutput.lower line 46
  11. theorem OAI.ContinuumCoulomb.AffinePhysicalOutput.upper line 50
  12. theorem OAI.ContinuumCoulomb.AffinePhysicalOutput.actual_error line 54
  13. theorem OAI.ContinuumCoulomb.AffinePhysicalOutput.valid line 67