OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPrivateProgram.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Polynomial machine instructions for rational private-pair subdivision.

  1. def OAI.ContinuumCoulomb.QuantumPrivate.scalarConstructor line 11
  2. def OAI.ContinuumCoulomb.QuantumPrivate.fieldConstructor line 17
  3. def OAI.ContinuumCoulomb.QuantumPrivate.pairConstructor line 25
  4. abbrev OAI.ContinuumCoulomb.QuantumPrivate.BlockInput line 33
  5. def OAI.ContinuumCoulomb.QuantumPrivate.blockCode line 34
  6. opaque OAI.ContinuumCoulomb.QuantumPrivate.envProgram line 37
  7. opaque OAI.ContinuumCoulomb.QuantumPrivate.indexRawProgram line 38
  8. opaque OAI.ContinuumCoulomb.QuantumPrivate.countProgram line 39
  9. opaque OAI.ContinuumCoulomb.QuantumPrivate.radiusProgram line 41
  10. opaque OAI.ContinuumCoulomb.QuantumPrivate.indexProgram line 43
  11. opaque OAI.ContinuumCoulomb.QuantumPrivate.rawProgram line 45
  12. opaque OAI.ContinuumCoulomb.QuantumPrivate.viewProgram line 47
  13. opaque OAI.ContinuumCoulomb.QuantumPrivate.freshProgram line 50
  14. opaque OAI.ContinuumCoulomb.QuantumPrivate.coefficientProgram line 52
  15. opaque OAI.ContinuumCoulomb.QuantumPrivate.pairFlagProgram line 54
  16. opaque OAI.ContinuumCoulomb.QuantumPrivate.leftFlagProgram line 56
  17. opaque OAI.ContinuumCoulomb.QuantumPrivate.oldLeftProgram line 61
  18. opaque OAI.ContinuumCoulomb.QuantumPrivate.oldRightProgram line 63
  19. opaque OAI.ContinuumCoulomb.QuantumPrivate.axisLeftProgram line 65
  20. opaque OAI.ContinuumCoulomb.QuantumPrivate.axisRightProgram line 67
  21. opaque OAI.ContinuumCoulomb.QuantumPrivate.radiusSquareProgram line 69
  22. opaque OAI.ContinuumCoulomb.QuantumPrivate.radiusHalfProgram line 72
  23. opaque OAI.ContinuumCoulomb.QuantumPrivate.coefficientHalfProgram line 74
  24. opaque OAI.ContinuumCoulomb.QuantumPrivate.coefficientSquareProgram line 76
  25. opaque OAI.ContinuumCoulomb.QuantumPrivate.zeroWeightProgram line 79
  26. opaque OAI.ContinuumCoulomb.QuantumPrivate.lastWeightProgram line 83
  27. opaque OAI.ContinuumCoulomb.QuantumPrivate.weightProgram line 87
  28. opaque OAI.ContinuumCoulomb.QuantumPrivate.termProgram line 105
  29. opaque OAI.ContinuumCoulomb.QuantumPrivate.blockProgram line 122
  30. def OAI.ContinuumCoulomb.QuantumPrivate.blockCertificate line 126