OAI/MathematicalPhysics/ContinuumCoulomb/Programs/UnitCoulombProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The literal output codec for a complete unit-charge Coulomb instance. The electron count is unary, and both rational thresholds are emitted in canonical numerator/positive-denominator form.

  1. abbrev OAI.ContinuumCoulomb.UnitCoulombProgram.Input line 12
  2. def OAI.ContinuumCoulomb.UnitCoulombProgram.metadataCode line 13
  3. def OAI.ContinuumCoulomb.UnitCoulombProgram.inputCode line 14
  4. def OAI.ContinuumCoulomb.UnitCoulombProgram.value line 16
  5. opaque OAI.ContinuumCoulomb.UnitCoulombProgram.unaryOutput line 22
  6. opaque OAI.ContinuumCoulomb.UnitCoulombProgram.geometryProgram line 29
  7. opaque OAI.ContinuumCoulomb.UnitCoulombProgram.metadataProgram line 31
  8. opaque OAI.ContinuumCoulomb.UnitCoulombProgram.electronsProgram line 32
  9. opaque OAI.ContinuumCoulomb.UnitCoulombProgram.thresholdsInputProgram line 34
  10. opaque OAI.ContinuumCoulomb.UnitCoulombProgram.thresholdsProgram line 37
  11. opaque OAI.ContinuumCoulomb.UnitCoulombProgram.tailProgram line 43
  12. opaque OAI.ContinuumCoulomb.UnitCoulombProgram.program line 48
  13. def OAI.ContinuumCoulomb.UnitCoulombProgram.certificate line 53
  14. theorem OAI.ContinuumCoulomb.UnitCoulombProgram.positions_injective line 56
  15. theorem OAI.ContinuumCoulomb.UnitCoulombProgram.valid line 64
  16. theorem OAI.ContinuumCoulomb.UnitCoulombProgram.valid_of_nodes line 75