OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumComputedRouteSelector.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Route selection directly from source-position and coarse-path lists. The crossing and permission tables are computed inside the polynomial program.

  1. abbrev OAI.ContinuumCoulomb.QuantumComputedRouteSelector.Input line 14
  2. def OAI.ContinuumCoulomb.QuantumComputedRouteSelector.inputCode line 15
  3. def OAI.ContinuumCoulomb.QuantumComputedRouteSelector.value line 17
  4. def OAI.ContinuumCoulomb.QuantumComputedRouteSelector.program line 20
  5. theorem OAI.ContinuumCoulomb.QuantumComputedRouteSelector.value_actual line 25
  6. theorem OAI.ContinuumCoulomb.QuantumComputedRouteSelector.value_merged line 37
  7. def OAI.ContinuumCoulomb.QuantumComputedRouteSelector.certificate line 49