OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListInitialCells.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The initial subdivision assigns its two new spins to the original endpoints. Its singlet bonds therefore have exactly the original cell locality.

  1. def OAI.ContinuumCoulomb.QuantumForkList.initialCell line 13
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.initialCell_old line 16
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.initialCell_new line 20
  4. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_cellAligned line 25
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.initial_cellLocal line 42