OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRoutingInputActual.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The encoded cell/edge arrays evaluate to the actual buffered path of the ordinal-slot spatial model. No arbitrary finite-fiber choice remains in this part of the routing compiler.

  1. def OAI.ContinuumCoulomb.QuantumRoutingInputProgram.actualData line 13
  2. theorem OAI.ContinuumCoulomb.QuantumRoutingInputProgram.edge_actual line 19
  3. theorem OAI.ContinuumCoulomb.QuantumRoutingInputProgram.fine_actual line 26
  4. theorem OAI.ContinuumCoulomb.QuantumRoutingInputProgram.lane_actual line 33
  5. theorem OAI.ContinuumCoulomb.QuantumRoutingInputProgram.entry_actual line 38
  6. theorem OAI.ContinuumCoulomb.QuantumRoutingInputProgram.entries_ofFn line 47
  7. theorem OAI.ContinuumCoulomb.QuantumRoutingInputProgram.entries_actual line 56
  8. theorem OAI.ContinuumCoulomb.QuantumRoutingInputProgram.value_actual line 74
  9. theorem OAI.ContinuumCoulomb.QuantumRoutingInputProgram.path_actual line 91