Fault-tolerant logical qubits below threshold at useful scale

The best published demonstrations are still small. Google's Willow surface-code memory reached 0.143% error per cycle at distance 7 (101 qubits, Lambda = 2.14): one logical memory at ~1e-3, far from 1e-6 and far from 100+ logical qubits with logical gates. Neutral-atom work (Harvard/MIT/QuEra, Nature, Nov 2025) showed below-threshold suppression with up to 96 logical qubits, but at logical error rates still orders of magnitude above the utility target. DARPA's QBI is itself still asking whether a utility-scale machine can be built by 2033.

Source: arxiv.org

import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.Field.Power
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum

/-!
# Fault-tolerant logical qubits below threshold at useful scale

Concrete here: the **logical error rate as a ratio and the suppression factor**.
For a code run at distance `d`, the logical error rate per syndrome-extraction
cycle is (logical errors observed) / (cycles run), which this file defines.
"Below threshold" is the statement that growing the code distance by 2 divides
that rate by at least `Λ > 1`, written as an inequality on the measured rates
across an increasing family of distances. The scale requirement and the logical
two-qubit gate bar are plain comparisons.

Opaque oracle (`Device`): the observed logical error counts at each distance, the
logical two-qubit gate error, and the attestations that decoding was performed
within the cycle budget (real-time, not offline), that no post-selection or
leakage-discard inflated the result, and that all physical qubits reported are on
one device and calibrated under one published routine.

Who must attest: the experiment host plus an independent reviewer of the kind a
DARPA-style benchmarking programme uses, publishing per-distance raw shot data,
the decoder and its latency, the calibration protocol, and the discard policy.

Units: `errorsObserved` and `cycles` are counts; `errorPerCycle` is dimensionless
(logical errors per cycle per logical qubit); `gateError` is dimensionless
(logical two-qubit gate infidelity); distances and qubit counts are counts.

Checked with Lean 4.33.0 / Mathlib using:
  lake env lean <absolute-path-to-this-file>
-/

namespace OpenSpur.Problems.FaultTolerantQubits

/-- Measured outcome of running the code at one distance. -/
structure Run where
  distance : ℕ
  cycles : ℕ
  errorsObserved : ℝ
  logicalQubits : ℕ

/-- Logical error per syndrome cycle; meaningful when `0 < cycles`. -/
noncomputable def errorPerCycle (r : Run) : ℝ :=
  r.errorsObserved / (r.cycles : ℝ)

/-- A device report: a family of runs at distances `d₀, d₀+2, …, d₀+2*levels`,
plus the logical gate figure and the integrity attestations. -/
structure Device (levels : ℕ) where
  baseDistance : ℕ
  run : Fin (levels + 1) → Run
  /-- Distances step by 2 from `baseDistance`, matching the surface-code family. -/
  distancesStepByTwo : ∀ i : Fin (levels + 1), (run i).distance = baseDistance + 2 * i.val
  gateError : ℝ
  decodedInRealTime : Prop
  noPostSelection : Prop
  singleDeviceCalibrated : Prop

/-- Below-threshold behaviour: each distance step of 2 suppresses the logical
error rate by at least the factor `Λ`. -/
def BelowThreshold {levels : ℕ} (D : Device levels) (Λ : ℝ) : Prop :=
  ∀ i : Fin levels,
    Λ * errorPerCycle (D.run i.succ) ≤ errorPerCycle (D.run i.castSucc)

/-- Bars a board would pay against. -/
structure Thresholds where
  /-- Minimum error-suppression factor per distance step of 2, e.g. 2. -/
  minLambda : ℝ
  /-- Maximum logical error per cycle at the largest distance, e.g. 1e-6. -/
  maxErrorPerCycle : ℝ
  /-- Maximum logical two-qubit gate error, e.g. 1e-6. -/
  maxGateError : ℝ
  /-- Minimum simultaneously maintained logical qubits at that distance. -/
  minLogicalQubits : ℕ
  /-- Minimum number of distance steps demonstrated (at least 2 for a trend). -/
  minLevels : ℕ

/-- Acceptance predicate: suppression across the family, plus an absolute error
floor, a gate bar and a scale bar at the largest distance. -/
def Solved {levels : ℕ} (T : Thresholds) (D : Device levels) : Prop :=
  D.decodedInRealTime ∧
  D.noPostSelection ∧
  D.singleDeviceCalibrated ∧
  T.minLevels ≤ levels ∧
  (∀ i, 0 < (D.run i).cycles) ∧
  BelowThreshold D T.minLambda ∧
  errorPerCycle (D.run (Fin.last levels)) ≤ T.maxErrorPerCycle ∧
  D.gateError ≤ T.maxGateError ∧
  T.minLogicalQubits ≤ (D.run (Fin.last levels)).logicalQubits

/-- Rung `k` demands a logical error rate 10× smaller and one more logical qubit
decade of scale, holding the suppression factor at 2. -/
noncomputable def Rung (k : ℕ) : Thresholds where
  minLambda := 2
  maxErrorPerCycle := 1e-3 / (10 : ℝ) ^ k
  maxGateError := 1e-3 / (10 : ℝ) ^ k
  minLogicalQubits := 2 ^ k
  minLevels := 2

/-- The error-rate bar tightens monotonically along the rungs. -/
theorem rung_error_antitone {j k : ℕ} (h : j ≤ k) :
    (Rung k).maxErrorPerCycle ≤ (Rung j).maxErrorPerCycle := by
  simp only [Rung]
  have hpow : (10 : ℝ) ^ j ≤ (10 : ℝ) ^ k := pow_le_pow_right₀ (by norm_num) h
  have hj : (0 : ℝ) < (10 : ℝ) ^ j := pow_pos (by norm_num) j
  exact div_le_div_of_nonneg_left (by norm_num) hj hpow

/-- A larger suppression factor is a stronger claim, provided the measured rates
are nonnegative. -/
theorem belowThreshold_mono {levels : ℕ} (D : Device levels) {Λ₁ Λ₂ : ℝ}
    (h : Λ₁ ≤ Λ₂) (hnn : ∀ i, 0 ≤ errorPerCycle (D.run i)) :
    BelowThreshold D Λ₂ → BelowThreshold D Λ₁ := by
  intro hD i
  have hstep := hD i
  have := mul_le_mul_of_nonneg_right h (hnn i.succ)
  exact le_trans this hstep

end OpenSpur.Problems.FaultTolerantQubits

• Google Quantum AI, 'Quantum error correction below the surface code threshold' (Willow, arXiv 2408.13687 / Nature 2024)
• Harvard/MIT/QuEra below-threshold neutral-atom surface codes, up to 96 logical qubits (Nature, Nov 2025)
• DARPA Quantum Benchmarking Initiative (QBI) program page