OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListInitialBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal odd subdivision satisfies all hypotheses needed to iterate the full-space fork estimate. Its fresh singlets have distinct endpoints.

  1. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_background_valid line 12
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_iterate_accuracy line 26