OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ProgramGroundIdentity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The serialized unit-Coulomb instance has exactly the ground energy of the rational array generated by the numerical node program.

  1. theorem OAI.ContinuumCoulomb.unitData_attraction_list line 14
  2. theorem OAI.ContinuumCoulomb.program_ground_identity line 21