OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/NuclearCoordinateOutput.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Serialization of computed rational triples into the actual nuclear position codec. The canonical numerator and positive denominator are kept exactly; no real-coordinate oracle is used.

  1. def OAI.ContinuumCoulomb.NuclearCoordinateOutput.rational line 14
  2. def OAI.ContinuumCoulomb.NuclearCoordinateOutput.position line 15
  3. theorem OAI.ContinuumCoulomb.NuclearCoordinateOutput.rational_value line 18
  4. theorem OAI.ContinuumCoulomb.NuclearCoordinateOutput.position_value line 19
  5. theorem OAI.ContinuumCoulomb.NuclearCoordinateOutput.position_valid line 21
  6. theorem OAI.ContinuumCoulomb.NuclearCoordinateOutput.position_value_injective line 23
  7. theorem OAI.ContinuumCoulomb.NuclearCoordinateOutput.position_injective line 32
  8. theorem OAI.ContinuumCoulomb.NuclearCoordinateOutput.real_position line 35
  9. opaque OAI.ContinuumCoulomb.NuclearCoordinateOutput.rationalProgram line 40
  10. opaque OAI.ContinuumCoulomb.NuclearCoordinateOutput.positionProgram line 46
  11. def OAI.ContinuumCoulomb.NuclearCoordinateOutput.positions line 55
  12. opaque OAI.ContinuumCoulomb.NuclearCoordinateOutput.positionsProgram line 57
  13. theorem OAI.ContinuumCoulomb.NuclearCoordinateOutput.positions_length line 62
  14. theorem OAI.ContinuumCoulomb.NuclearCoordinateOutput.positions_valid line 64
  15. theorem OAI.ContinuumCoulomb.NuclearCoordinateOutput.positions_nodup line 67
  16. def OAI.ContinuumCoulomb.NuclearCoordinateOutput.certificate line 70