OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryFork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual history compiler produces a bounded loop-free exchange list. Its initial subdivision and ordered fork rounds preserve the full-space ground energy with the accumulated explicit error.

  1. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelCompile.output_valid line 18
  2. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.history_valid line 40
  3. def OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.forkState line 60
  4. theorem OAI.ContinuumCoulomb.QuantumPaddedLabelProgram.fork_accuracy line 64