OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCoefficientHeight.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform rational-register bounds for the actual fixed-arity Pauli trace. These supply an explicit precision budget before scalar sampling.

  1. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.height_finiteSum line 14
  2. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.height_finiteProduct line 23
  3. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.height_pauli line 32
  4. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.height_word line 36
  5. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.height_coefficient line 42
  6. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.realHeight_coefficient line 72