OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListRoutePreservation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Preservation of the exact finite coordinate/route representation by one round, and hence by the fixed number of rounds of the literal compiler.

  1. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.range_map_congr line 15
  2. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.tagPath_next line 20
  3. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.paths_next line 71
  4. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.value_represents line 82
  5. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.iterate_state line 87
  6. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.iterate_represents line 96
  7. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.compile_realization line 111