OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedFinalBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

An integer polynomial bound for the complete six-stage ordered compiler, including the private-pair subdivision before the physical four-spin step.

  1. def OAI.ContinuumCoulomb.QuantumOrderedXZ.weightNat line 13
  2. def OAI.ContinuumCoulomb.QuantumOrderedXZ.scaleNat line 14
  3. def OAI.ContinuumCoulomb.QuantumOrderedXZ.stepNat line 15
  4. def OAI.ContinuumCoulomb.QuantumOrderedXZ.pipelineNat line 16
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.weightNat_cast line 20
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.scaleNat_cast line 24
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.stepNat_cast line 28
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.pipelineNat_cast line 31
  9. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.outputTerm_card line 36
  10. theorem OAI.ContinuumCoulomb.QuantumOrderedXZ.private_coefficient_bound line 41