OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactLocalInputProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Extract the exact nineteen local lengths from the calibrated final-edge array. Runtime indices are the proved natural formulas for encodeEdge.

  1. abbrev OAI.ContinuumCoulomb.ContactLocalInputProgram.Input line 12
  2. def OAI.ContinuumCoulomb.ContactLocalInputProgram.inputCode line 14
  3. def OAI.ContinuumCoulomb.ContactLocalInputProgram.lookup line 17
  4. def OAI.ContinuumCoulomb.ContactLocalInputProgram.record line 20
  5. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.precisionProgram line 25
  6. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.tailProgram line 28
  7. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.countProgram line 32
  8. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.restProgram line 35
  9. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.indexProgram line 39
  10. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.lastProgram line 42
  11. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.signProgram line 46
  12. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.valuesProgram line 49
  13. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.lookupProgram line 52
  14. def OAI.ContinuumCoulomb.ContactLocalInputProgram.valuesListProgram line 56
  15. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.leftProgram line 62
  16. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.rightProgram line 68
  17. opaque OAI.ContinuumCoulomb.ContactLocalInputProgram.program line 74
  18. def OAI.ContinuumCoulomb.ContactLocalInputProgram.certificate line 78