OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLatticeSourceBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The proved physical box and coefficient estimates imply the exact binary source promise, measured against the retained input size.

  1. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.latticeSource_binary_promise line 16
  2. theorem OAI.ContinuumCoulomb.QMAPortRouteData.latticeSource_binary_promise line 47