OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRoutingFamily.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Literal enumeration of every coarse route and source center. These are the exact lists consumed by the finite crossing and permission tables.

  1. def OAI.ContinuumCoulomb.QuantumRoutingFamily.placed line 13
  2. opaque OAI.ContinuumCoulomb.QuantumRoutingFamily.placedProgram line 17
  3. def OAI.ContinuumCoulomb.QuantumRoutingFamily.positions line 25
  4. opaque OAI.ContinuumCoulomb.QuantumRoutingFamily.positionsProgram line 28
  5. def OAI.ContinuumCoulomb.QuantumRoutingFamily.coarse line 40
  6. opaque OAI.ContinuumCoulomb.QuantumRoutingFamily.coarseProgram line 44
  7. def OAI.ContinuumCoulomb.QuantumRoutingFamily.table line 57
  8. def OAI.ContinuumCoulomb.QuantumRoutingFamily.tableProgram line 60
  9. theorem OAI.ContinuumCoulomb.QuantumRoutingFamily.placed_actual line 64
  10. theorem OAI.ContinuumCoulomb.QuantumRoutingFamily.positions_actual line 71
  11. theorem OAI.ContinuumCoulomb.QuantumRoutingFamily.coarse_actual line 83
  12. theorem OAI.ContinuumCoulomb.QuantumRoutingFamily.support_range line 96
  13. theorem OAI.ContinuumCoulomb.QuantumRoutingFamily.table_actual line 107