OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPlanarTapeGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The emitted planar tape is the exact coordinate and path array of a bounded planar family, in its literal merged-edge order.

  1. theorem OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.value_eq_of_allowed line 16
  2. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.map_eq_ofFn line 29
  3. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.graph_packed line 35
  4. def OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.route line 55
  5. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.route_length line 59
  6. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.route_bounded line 64
  7. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.lookup_position line 77
  8. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.selected_path line 85
  9. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.path_eq line 101
  10. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.positions_eq line 110
  11. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.paths_eq line 115
  12. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.value_eq line 126
  13. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.even_input_eq line 140