OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumComputedRoutingTable.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compute the crossing list from encoded visits, and preserve exactly the routing permissions of the geometric construction.

  1. theorem OAI.ContinuumCoulomb.QuantumRoutingTable.filter_eq_flatten line 13
  2. def OAI.ContinuumCoulomb.QuantumRoutingTable.selectCrossingProgram line 21
  3. def OAI.ContinuumCoulomb.QuantumRoutingTable.computedCrossingsProgram line 29
  4. def OAI.ContinuumCoulomb.QuantumRoutingTable.computedTable line 43
  5. def OAI.ContinuumCoulomb.QuantumRoutingTable.computedTableProgram line 45
  6. theorem OAI.ContinuumCoulomb.QuantumRoutingTable.computedTable_allowed line 50