OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPhysicalCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Every physical spin retains the coarse cell of an original route point. This transfers the original positive-coordinate and rectangle bounds.

  1. theorem OAI.ContinuumCoulomb.qmaPointCell_inner line 14
  2. theorem OAI.ContinuumCoulomb.qmaPointCell_ancilla line 17
  3. theorem OAI.ContinuumCoulomb.qmaCrossingMove_cell line 20
  4. theorem OAI.ContinuumCoulomb.QMAPortRouteData.chain_cell_property line 30
  5. theorem OAI.ContinuumCoulomb.QMAPortRouteData.finished_cell_property line 45
  6. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingPosition_cell_property line 57
  7. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingPosition_positive line 77
  8. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossingPosition_bounded line 84