OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingSiteRelabel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The terminal scan is independent of the finite vertex enumeration. It returns the actual terminal in the emitted position tape.

  1. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.relabeled_injective line 19
  2. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.terminal_relabeled line 28
  3. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.sites_relabeled line 40
  4. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.allSites_relabeled line 48
  5. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.relabeled_sites_global line 54
  6. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.allSites_reordered line 60
  7. theorem OAI.ContinuumCoulomb.QuantumCrossingSiteProgram.reordered_sites_global line 69