OAI/MathematicalPhysics/ContinuumCoulomb/Programs/SourceContactProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Literal composition from the encoded source to the calibrated contact coordinates. The signed retained bonds determine the geometric strips; the final positive bond list supplies their nineteen target weights.

  1. def OAI.ContinuumCoulomb.SourceContactProgram.size line 13
  2. def OAI.ContinuumCoulomb.SourceContactProgram.input line 15
  3. def OAI.ContinuumCoulomb.SourceContactProgram.value line 20
  4. opaque OAI.ContinuumCoulomb.SourceContactProgram.coordinateProgram line 24
  5. opaque OAI.ContinuumCoulomb.SourceContactProgram.coordinatesProgram line 32
  6. opaque OAI.ContinuumCoulomb.SourceContactProgram.sizeProgram line 37
  7. def OAI.ContinuumCoulomb.SourceContactProgram.powerProgram line 40
  8. opaque OAI.ContinuumCoulomb.SourceContactProgram.signedBondsProgram line 46
  9. opaque OAI.ContinuumCoulomb.SourceContactProgram.coefficientProgram line 50
  10. opaque OAI.ContinuumCoulomb.SourceContactProgram.coefficientsProgram line 53
  11. opaque OAI.ContinuumCoulomb.SourceContactProgram.inputProgram line 58
  12. opaque OAI.ContinuumCoulomb.SourceContactProgram.program line 63
  13. def OAI.ContinuumCoulomb.SourceContactProgram.certificate line 68
  14. theorem OAI.ContinuumCoulomb.SourceContactProgram.size_ge_two line 73