OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactPlacedGadgetProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A source-edge record contains the original integer endpoints and the nineteen calibrated lengths. The whole local coordinate list is computed by the same orientation and height routines used in the geometric proof.

  1. abbrev OAI.ContinuumCoulomb.ContactPlacedGadgetProgram.Input line 14
  2. def OAI.ContinuumCoulomb.ContactPlacedGadgetProgram.inputCode line 16
  3. def OAI.ContinuumCoulomb.ContactPlacedGadgetProgram.placement line 19
  4. def OAI.ContinuumCoulomb.ContactPlacedGadgetProgram.position line 21
  5. opaque OAI.ContinuumCoulomb.ContactPlacedGadgetProgram.placementProgram line 24
  6. opaque OAI.ContinuumCoulomb.ContactPlacedGadgetProgram.gadgetProgram line 28
  7. opaque OAI.ContinuumCoulomb.ContactPlacedGadgetProgram.positionProgram line 31
  8. def OAI.ContinuumCoulomb.ContactPlacedGadgetProgram.pointListProgram line 36
  9. def OAI.ContinuumCoulomb.ContactPlacedGadgetProgram.certificate line 44