OAI/MathematicalPhysics/ContinuumCoulomb/Programs/CenteredNuclearProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The complete finite rational nucleus list, generated from the actual rectangular cell bounds, numerically transported, and serialized using the continuum promise's own position codec.

  1. abbrev OAI.ContinuumCoulomb.CenteredNuclearProgram.Input line 14
  2. def OAI.ContinuumCoulomb.CenteredNuclearProgram.inputCode line 15
  3. def OAI.ContinuumCoulomb.CenteredNuclearProgram.nuclei line 18
  4. opaque OAI.ContinuumCoulomb.CenteredNuclearProgram.argumentsProgram line 22
  5. opaque OAI.ContinuumCoulomb.CenteredNuclearProgram.program line 26
  6. def OAI.ContinuumCoulomb.CenteredNuclearProgram.certificate line 31
  7. theorem OAI.ContinuumCoulomb.CenteredNuclearProgram.nuclei_length line 35
  8. theorem OAI.ContinuumCoulomb.CenteredNuclearProgram.nuclei_valid line 41
  9. theorem OAI.ContinuumCoulomb.CenteredNuclearProgram.nuclei_nonempty line 45
  10. theorem OAI.ContinuumCoulomb.CenteredNuclearProgram.nuclei_values_nodup line 49