OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactPositionArray.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The literal coordinate list has the exact final mediator enumeration, including the original vertices. This identifies the machine output with the geometric realization without an unproved permutation.

  1. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.siteCount line 13
  2. theorem OAI.ContinuumCoulomb.ContactGeometryBlockProgram.literal_array line 17
  3. theorem OAI.ContinuumCoulomb.ContactSourceInputProgram.literal_array line 63
  4. theorem OAI.ContinuumCoulomb.ContactSourceInputProgram.scaled_literal_array line 67