OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourcePositiveCorrectness.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Exact semantics of the computed positive-spin source reduction: the literal output has the full three-stage matrix and the proved rational thresholds, including the common coefficient-rounding error.

  1. abbrev OAI.ContinuumCoulomb.SourcePositiveProgram.sourceFamily line 14
  2. abbrev OAI.ContinuumCoulomb.SourcePositiveProgram.sourceBound line 17
  3. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.normalized_literal line 20
  4. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.bonds_eq line 27
  5. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.offset_eq line 34
  6. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.vertices_eq line 39
  7. def OAI.ContinuumCoulomb.SourcePositiveProgram.energy line 50
  8. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.energy_eq line 52
  9. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.lower_eq line 62
  10. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.upper_eq line 69
  11. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.output_yes line 76
  12. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.output_no line 84
  13. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.output_gap line 92