OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPortRankActual.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal incidence count computes the very arm assignment used by the spatial routing proof, for any explicit enumeration of the interaction labels.

  1. def OAI.ContinuumCoulomb.QuantumPortRankProgram.entries line 12
  2. theorem OAI.ContinuumCoulomb.QuantumPortRankProgram.value_actual line 17