OAI/MathematicalPhysics/ContinuumCoulomb/Programs/SourcePositiveProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The complete literal source-to-positive-spin program. It parses the original source, computes the fixed polynomial metadata, rounds and deletes zero coefficients, emits all three graph stages, and shifts both thresholds.

  1. structure OAI.ContinuumCoulomb.SourcePositiveProgram.Registers line 13
  2. def OAI.ContinuumCoulomb.SourcePositiveProgram.registerCode line 23
  3. def OAI.ContinuumCoulomb.SourcePositiveProgram.normalized line 29
  4. def OAI.ContinuumCoulomb.SourcePositiveProgram.offset line 32
  5. def OAI.ContinuumCoulomb.SourcePositiveProgram.error line 34
  6. def OAI.ContinuumCoulomb.SourcePositiveProgram.output line 37
  7. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.normalizedProgram line 48
  8. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.verticesProgram line 50
  9. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.boundProgram line 53
  10. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.bondsProgram line 56
  11. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.offsetProgram line 59
  12. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.gRationalProgram line 62
  13. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.denominatorProgram line 65
  14. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.errorProgram line 69
  15. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.lowerShiftProgram line 72
  16. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.upperShiftProgram line 75
  17. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.lowerProgram line 78
  18. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.upperProgram line 81
  19. opaque OAI.ContinuumCoulomb.SourcePositiveProgram.outputProgram line 85
  20. def OAI.ContinuumCoulomb.SourcePositiveProgram.certificate line 91