OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactSourceInputCorrectness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The raw-list program uses exactly the original source endpoints and exactly the calibrated lengths of the final mediator edges.

  1. theorem OAI.ContinuumCoulomb.ContactSourceInputProgram.lookup_ofFn line 15
  2. def OAI.ContinuumCoulomb.ContactSourceInputProgram.literalInput line 20
  3. theorem OAI.ContinuumCoulomb.ContactSourceInputProgram.local_lookup line 23
  4. theorem OAI.ContinuumCoulomb.ContactSourceInputProgram.local_record line 31
  5. theorem OAI.ContinuumCoulomb.ContactSourceInputProgram.literal_bond line 37
  6. theorem OAI.ContinuumCoulomb.ContactSourceInputProgram.literal_edge line 44
  7. theorem OAI.ContinuumCoulomb.ContactSourceInputProgram.literal_edges line 59
  8. theorem OAI.ContinuumCoulomb.ContactSourceInputProgram.literal_positions line 69