OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListPathInput.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The subdivision guarantee for arbitrary valid input tapes, with no assumption that their bond lists came from a chosen abstract edge enumeration.

  1. theorem OAI.ContinuumCoulomb.QuantumListPathStep.bonds_list line 12
  2. theorem OAI.ContinuumCoulomb.QuantumListPathStep.input_of_bonds line 18
  3. theorem OAI.ContinuumCoulomb.QuantumListPathStep.energy_error_input line 30
  4. theorem OAI.ContinuumCoulomb.QuantumListPathStep.graph_energy_error line 50