OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumStagePath.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Row-labelled stages form bounded-step spatial paths with explicit endpoints.

  1. def OAI.ContinuumCoulomb.qmaRowLift line 12
  2. def OAI.ContinuumCoulomb.QMAGridTagNear line 15
  3. theorem OAI.ContinuumCoulomb.qmaRowLift_chain line 19
  4. def OAI.ContinuumCoulomb.qmaGridStageTags line 27
  5. theorem OAI.ContinuumCoulomb.qmaGridStageTags_nonempty line 32
  6. theorem OAI.ContinuumCoulomb.qmaGridStageTags_head line 39
  7. theorem OAI.ContinuumCoulomb.qmaGridStageTags_last line 51
  8. theorem OAI.ContinuumCoulomb.qmaGridStageTags_chain line 65