OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListRouteLattice.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The final literal route tape is itself the serialized lattice source. Its coordinate and edge order are the computed orders, and its exact scalar offset is removed from both thresholds.

  1. def OAI.ContinuumCoulomb.QuantumListRouteProgram.latticePacket line 15
  2. def OAI.ContinuumCoulomb.QuantumListRouteProgram.latticeOutput line 18
  3. def OAI.ContinuumCoulomb.QuantumListRouteProgram.latticePacketProgram line 21
  4. def OAI.ContinuumCoulomb.QuantumListRouteProgram.latticeOutputProgram line 38
  5. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.get_of_eq_ofFn line 43
  6. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.represented_length line 49
  7. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.represented_nodup line 53
  8. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.represented_bounded line 59
  9. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.represented_adjacent line 65
  10. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.latticeOutput_valid line 76
  11. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.latticeOutput_yes line 87
  12. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.latticeOutput_no line 102
  13. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.latticeOutput_polynomialPromise line 117
  14. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.iterate_count_le line 146
  15. theorem OAI.ContinuumCoulomb.QuantumListRouteProgram.compiled_lattice_promise line 158