OAI/MathematicalPhysics/ContinuumCoulomb/Programs/AffinePhysicalThresholdProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial-time evaluation of the complete affine threshold shift. Every precision and loop bound is computed in unary from polynomial metadata.

  1. def OAI.ContinuumCoulomb.AffinePhysicalThreshold.dataCode line 11
  2. def OAI.ContinuumCoulomb.AffinePhysicalThreshold.inputCode line 13
  3. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.numbersProgram line 15
  4. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.dataProgram line 17
  5. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.tauProgram line 18
  6. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.listsProgram line 20
  7. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.sitesProgram line 23
  8. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.weightsProgram line 25
  9. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.errorProgram line 27
  10. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.geometryProgram line 29
  11. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.electronsProgram line 31
  12. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.precisionProgram line 33
  13. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.pairPrecisionProgram line 39
  14. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.pairProgram line 46
  15. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.finiteProgram line 49
  16. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.argumentProgram line 64
  17. opaque OAI.ContinuumCoulomb.AffinePhysicalThreshold.program line 68
  18. def OAI.ContinuumCoulomb.AffinePhysicalThreshold.certificate line 71