OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRoutingSize.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Linear graph-size growth and an explicit polynomial routing penalty bound.

  1. abbrev OAI.ContinuumCoulomb.QMAForkGraphEdge line 11
  2. abbrev OAI.ContinuumCoulomb.QMACrossingsGraphEdge line 13
  3. abbrev OAI.ContinuumCoulomb.QMAPathsGraphEdge line 15
  4. theorem OAI.ContinuumCoulomb.qmaForkGraphEdge_card line 18
  5. theorem OAI.ContinuumCoulomb.qmaCrossingsGraphEdge_card line 23
  6. theorem OAI.ContinuumCoulomb.qmaPathsGraphEdge_card line 28
  7. theorem OAI.ContinuumCoulomb.qmaRoutingScale_polynomial line 33