OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPortRank.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The endpoint arm assigned to an incident interaction is the number of incident lane colors below it. This exposes the finite count used by the literal route evaluator.

  1. theorem OAI.ContinuumCoulomb.qmaPort_orderRank line 13
  2. theorem OAI.ContinuumCoulomb.qmaCanonicalSortedPorts_assign_rank line 32
  3. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.endpointPorts_assign_rank line 55