OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactRationalGlobal.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The rational local gadgets are glued through the exact final-graph permutation. All old lattice sites remain fixed; all nineteen edges per source edge retain a controlled error and all nonedges retain the margin.

  1. def OAI.ContinuumCoulomb.ContactRationalGlobal.localPoints line 14
  2. def OAI.ContinuumCoulomb.ContactRationalGlobal.point line 18
  3. theorem OAI.ContinuumCoulomb.ContactRationalGlobal.local_start line 21
  4. theorem OAI.ContinuumCoulomb.ContactRationalGlobal.local_end line 27
  5. theorem OAI.ContinuumCoulomb.ContactRationalGlobal.edge_error line 33
  6. theorem OAI.ContinuumCoulomb.ContactRationalGlobal.nonedge_separation line 60
  7. theorem OAI.ContinuumCoulomb.ContactRationalGlobal.separation line 75
  8. theorem OAI.ContinuumCoulomb.ContactRationalGlobal.coordinate_bound line 97
  9. def OAI.ContinuumCoulomb.ContactRationalGlobal.rationalPlace line 106
  10. theorem OAI.ContinuumCoulomb.ContactRationalGlobal.rationalPlace_cast line 111
  11. def OAI.ContinuumCoulomb.ContactRationalGlobal.position line 118
  12. theorem OAI.ContinuumCoulomb.ContactRationalGlobal.position_cast line 126