OAI/MathematicalPhysics/ContinuumCoulomb/Programs/PhysicalNuclearProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Physical nuclear coordinates for h=1/N. The exact rational factor is 1/λ=rho/(8N^3), matching the manuscript's y=λx convention.

  1. def OAI.ContinuumCoulomb.PhysicalNuclearProgram.factor line 12
  2. def OAI.ContinuumCoulomb.PhysicalNuclearProgram.scale line 13
  3. theorem OAI.ContinuumCoulomb.PhysicalNuclearProgram.factor_positive line 15
  4. theorem OAI.ContinuumCoulomb.PhysicalNuclearProgram.factor_real line 19
  5. theorem OAI.ContinuumCoulomb.PhysicalNuclearProgram.scale_position line 22
  6. theorem OAI.ContinuumCoulomb.PhysicalNuclearProgram.scale_injective line 26
  7. theorem OAI.ContinuumCoulomb.PhysicalNuclearProgram.scale_error line 34
  8. abbrev OAI.ContinuumCoulomb.PhysicalNuclearProgram.Input line 39
  9. def OAI.ContinuumCoulomb.PhysicalNuclearProgram.inputCode line 40
  10. def OAI.ContinuumCoulomb.PhysicalNuclearProgram.triples line 42
  11. def OAI.ContinuumCoulomb.PhysicalNuclearProgram.nuclei line 45
  12. opaque OAI.ContinuumCoulomb.PhysicalNuclearProgram.meshProgram line 48
  13. opaque OAI.ContinuumCoulomb.PhysicalNuclearProgram.factorProgram line 52
  14. opaque OAI.ContinuumCoulomb.PhysicalNuclearProgram.scaleProgram line 66
  15. opaque OAI.ContinuumCoulomb.PhysicalNuclearProgram.triplesProgram line 76
  16. opaque OAI.ContinuumCoulomb.PhysicalNuclearProgram.program line 82
  17. def OAI.ContinuumCoulomb.PhysicalNuclearProgram.certificate line 86
  18. theorem OAI.ContinuumCoulomb.PhysicalNuclearProgram.nuclei_length line 90
  19. theorem OAI.ContinuumCoulomb.PhysicalNuclearProgram.nuclei_valid line 95
  20. theorem OAI.ContinuumCoulomb.PhysicalNuclearProgram.nuclei_nonempty line 98
  21. theorem OAI.ContinuumCoulomb.PhysicalNuclearProgram.nuclei_values_nodup line 102