OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactRationalGadgetProgram.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial-time computation of the twenty rational gadget positions, including the two exact outer endpoints.

  1. def OAI.ContinuumCoulomb.ContactRationalGadget.inputCode line 11
  2. def OAI.ContinuumCoulomb.ContactRationalGadget.pointCode line 15
  3. opaque OAI.ContinuumCoulomb.ContactRationalGadget.precisionProgram line 17
  4. opaque OAI.ContinuumCoulomb.ContactRationalGadget.restProgram line 20
  5. opaque OAI.ContinuumCoulomb.ContactRationalGadget.signProgram line 24
  6. opaque OAI.ContinuumCoulomb.ContactRationalGadget.dataProgram line 27
  7. opaque OAI.ContinuumCoulomb.ContactRationalGadget.centralProgram line 31
  8. opaque OAI.ContinuumCoulomb.ContactRationalGadget.listsProgram line 34
  9. opaque OAI.ContinuumCoulomb.ContactRationalGadget.leftListProgram line 38
  10. opaque OAI.ContinuumCoulomb.ContactRationalGadget.rightListProgram line 41
  11. opaque OAI.ContinuumCoulomb.ContactRationalGadget.positiveSpanProgram line 44
  12. opaque OAI.ContinuumCoulomb.ContactRationalGadget.positiveOriginProgram line 51
  13. opaque OAI.ContinuumCoulomb.ContactRationalGadget.spanProgram line 58
  14. opaque OAI.ContinuumCoulomb.ContactRationalGadget.originProgram line 62
  15. opaque OAI.ContinuumCoulomb.ContactRationalGadget.leftEnvironmentProgram line 66
  16. opaque OAI.ContinuumCoulomb.ContactRationalGadget.rightEnvironmentProgram line 69
  17. opaque OAI.ContinuumCoulomb.ContactRationalGadget.leftVertexProgram line 72
  18. opaque OAI.ContinuumCoulomb.ContactRationalGadget.rightVertexProgram line 76
  19. opaque OAI.ContinuumCoulomb.ContactRationalGadget.rightShiftProgram line 80
  20. opaque OAI.ContinuumCoulomb.ContactRationalGadget.sideProgram line 88
  21. def OAI.ContinuumCoulomb.ContactRationalGadget.positionProgram line 94
  22. def OAI.ContinuumCoulomb.ContactRationalGadget.pointListProgram line 100
  23. def OAI.ContinuumCoulomb.ContactRationalGadget.sites line 106
  24. def OAI.ContinuumCoulomb.ContactRationalGadget.certificate line 110