OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEndpointPorts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The at-most-three incident edges are assigned distinct, ordered buffered ports.

  1. structure OAI.ContinuumCoulomb.QMASortedPorts line 14
  2. theorem OAI.ContinuumCoulomb.qmaSortedPorts_exists line 20
  3. def OAI.ContinuumCoulomb.qmaPaddedPortSlot line 34
  4. theorem OAI.ContinuumCoulomb.qmaPaddedPortSlot_increasing line 38
  5. def OAI.ContinuumCoulomb.qmaCanonicalSortedPorts line 55
  6. abbrev OAI.ContinuumCoulomb.QMASpatialExchangeModel.Incident line 73
  7. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.incident_card line 75
  8. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.incident_lane_support line 81
  9. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.incident_color_injective line 94
  10. def OAI.ContinuumCoulomb.QMASpatialExchangeModel.endpointPorts line 105
  11. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.endpointPorts_assign_injective line 109