OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListCellLocality.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Every new ordinary bond remains within its original coarse cell. Old ordinary bonds retain their cells, so arbitrary reflexive locality relations are preserved by the actual list transformation.

  1. def OAI.ContinuumCoulomb.QuantumForkList.BondLocal line 14
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.addedBonds_cellLocal line 17
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.next_cellLocal line 39
  4. def OAI.ContinuumCoulomb.QuantumForkList.iterateCell line 50
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.iterate_cellAligned line 54
  6. theorem OAI.ContinuumCoulomb.QuantumForkList.iterate_cellLocal line 61