OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactVertexProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial-time rational coordinates for a fixed nine-link contact path. The height program is followed by four dyadic root evaluations and the fixed finite prefix sums.

  1. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.stepXProgram line 15
  2. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.stepYProgram line 21
  3. def OAI.ContinuumCoulomb.ContactHeightEvaluation.prefixXProgram line 33
  4. def OAI.ContinuumCoulomb.ContactHeightEvaluation.prefixYProgram line 39
  5. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.coordinateInputProgram line 45
  6. opaque OAI.ContinuumCoulomb.ContactHeightEvaluation.vertexProgram line 49
  7. def OAI.ContinuumCoulomb.ContactHeightEvaluation.vertexListProgram line 54
  8. def OAI.ContinuumCoulomb.ContactHeightEvaluation.vertexListCertificate line 68