OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRoutingCrossingTest.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Crossing cells are detected from the two opposite port pairs in the finite visit table. No search over a proof-level finite type is needed.

  1. theorem OAI.ContinuumCoulomb.QMAPortRouteData.crossing_iff_opposite_visits line 15
  2. def OAI.ContinuumCoulomb.QuantumRoutingTable.crossingTest line 59
  3. def OAI.ContinuumCoulomb.QuantumRoutingTable.computedCrossings line 62
  4. theorem OAI.ContinuumCoulomb.QuantumRoutingTable.mem_computedCrossings line 65
  5. theorem OAI.ContinuumCoulomb.QuantumRoutingTable.crossingTest_correct line 78
  6. theorem OAI.ContinuumCoulomb.QuantumRoutingTable.computedCrossings_correct line 83
  7. def OAI.ContinuumCoulomb.QuantumRoutingTable.crossingTestProgram line 87