OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRoutingTable.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite source cells, internal visits and crossing cells determine every routing permission. These tests inspect finite encoded lists, including both orientations of each internal port pair.

  1. abbrev OAI.ContinuumCoulomb.QuantumRoutingTable.Visit line 15
  2. abbrev OAI.ContinuumCoulomb.QuantumRoutingTable.Table line 16
  3. def OAI.ContinuumCoulomb.QuantumRoutingTable.visitCode line 17
  4. def OAI.ContinuumCoulomb.QuantumRoutingTable.tableCode line 18
  5. def OAI.ContinuumCoulomb.QuantumRoutingTable.inputCode line 20
  6. def OAI.ContinuumCoulomb.QuantumRoutingTable.allowed line 22
  7. opaque OAI.ContinuumCoulomb.QuantumRoutingTable.cellProgram line 30
  8. opaque OAI.ContinuumCoulomb.QuantumRoutingTable.tableProgram line 31
  9. opaque OAI.ContinuumCoulomb.QuantumRoutingTable.sourcesProgram line 32
  10. opaque OAI.ContinuumCoulomb.QuantumRoutingTable.visitsProgram line 34
  11. opaque OAI.ContinuumCoulomb.QuantumRoutingTable.crossingsProgram line 36
  12. opaque OAI.ContinuumCoulomb.QuantumRoutingTable.crossingProgram line 38
  13. opaque OAI.ContinuumCoulomb.QuantumRoutingTable.rayAllowedProgram line 41
  14. opaque OAI.ContinuumCoulomb.QuantumRoutingTable.pairAllowedProgram line 46
  15. opaque OAI.ContinuumCoulomb.QuantumRoutingTable.patchAllowedProgram line 54
  16. opaque OAI.ContinuumCoulomb.QuantumRoutingTable.corridorAllowedProgram line 57