OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialInputBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Size and coefficient bounds for the same full spatial graph that is routed to the lattice. Active-star bonds and the scalar offset are included.

  1. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.model_size line 16
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.model_coefficientBound line 27
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.SpatialInput.model_nat_coefficientBound line 38