OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryXZPromise.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Explicit inverse-polynomial thresholds for the actual two-local X/Z history output. The precision is a fixed linear unary function of clock length.

  1. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xzPrecision line 11
  2. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xzYesThreshold line 12
  3. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xzNoThreshold line 13
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xzPrecision_positive line 15
  5. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_threshold_gap line 19
  6. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_threshold_lt line 26
  7. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.yes_budget line 31
  8. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.no_budget line 40
  9. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_accepting line 49
  10. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.xz_rejecting line 58