OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactEdgeNumberProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Each fixed local edge has an explicit polynomial-time global lookup index, with the original source edge index retained.

  1. abbrev OAI.ContinuumCoulomb.ContactEdgeNumberProgram.Input line 12
  2. def OAI.ContinuumCoulomb.ContactEdgeNumberProgram.inputCode line 14
  3. opaque OAI.ContinuumCoulomb.ContactEdgeNumberProgram.rProgram line 16
  4. opaque OAI.ContinuumCoulomb.ContactEdgeNumberProgram.eProgram line 19
  5. opaque OAI.ContinuumCoulomb.ContactEdgeNumberProgram.twiceRProgram line 22
  6. opaque OAI.ContinuumCoulomb.ContactEdgeNumberProgram.twiceEProgram line 25
  7. def OAI.ContinuumCoulomb.ContactEdgeNumberProgram.pathProgram line 28
  8. opaque OAI.ContinuumCoulomb.ContactEdgeNumberProgram.pathCountProgram line 39
  9. def OAI.ContinuumCoulomb.ContactEdgeNumberProgram.edgeProgram line 44
  10. def OAI.ContinuumCoulomb.ContactEdgeNumberProgram.certificate line 55