OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactCanonicalEdge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The canonical strip record has an explicit finite computation from its two lattice endpoints. This identifies the selected record with the record used by rational coordinate programs.

  1. def OAI.ContinuumCoulomb.canonicalContactEdge line 11
  2. theorem OAI.ContinuumCoulomb.canonicalContactEdge_endpoints line 16
  3. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.contactEdge_computation line 23