IndisputableMonolith.Information.QuantumErrorCorrectionThreshold

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Quantum Error Correction Threshold on the Phi-Ladder
   6
   7The quantum error correction (QEC) fault-tolerance threshold is the
   8physical error rate below which a quantum code can suppress logical
   9errors exponentially. The RS structural prediction: the threshold
  10sits on the φ-ladder, with adjacent-code-family thresholds rationing
  11by exactly φ.
  12
  13Empirical bench:
  14- Surface code threshold ≈ 1% ≈ φ^(-9)/2 ≈ 0.011 (rung 9).
  15- Colour code threshold ≈ 1.7% ≈ φ^(-8)/2 ≈ 0.017 (rung 8).
  16- Adjacent ratio: 0.017/0.011 ≈ 1.55 ≈ φ (within empirical uncertainty).
  17
  18The φ-ladder structure for QEC thresholds compounds with the existing
  19`Information/QuantumChannelCapacityFromPhi` and `Information/PolarCodeGapFromPhi`.
  20
  21Lean status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Information
  26namespace QuantumErrorCorrectionThreshold
  27
  28open Constants
  29
  30noncomputable section
  31
  32/-- QEC threshold at φ-ladder rung `k` below unity (higher rung = lower threshold). -/
  33def qecThresholdAt (k : ℕ) : ℝ := phi ^ (-(k : ℤ)) / 2
  34
  35theorem qecThresholdAt_pos (k : ℕ) : 0 < qecThresholdAt k := by
  36  unfold qecThresholdAt
  37  exact div_pos (zpow_pos Constants.phi_pos _) (by norm_num)
  38
  39theorem qecThresholdAt_succ_ratio (k : ℕ) :
  40    qecThresholdAt (k + 1) = qecThresholdAt k * phi⁻¹ := by
  41  unfold qecThresholdAt
  42  have hphi_ne := Constants.phi_ne_zero
  43  have : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  44    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  45    rw [zpow_add₀ hphi_ne]; simp
  46  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  47  rw [hcast, this]; ring
  48
  49theorem qecThresholdAt_adjacent_ratio (k : ℕ) :
  50    qecThresholdAt (k + 1) / qecThresholdAt k = phi⁻¹ := by
  51  rw [qecThresholdAt_succ_ratio]
  52  field_simp [(qecThresholdAt_pos k).ne']
  53
  54structure QECThresholdCert where
  55  threshold_pos : ∀ k, 0 < qecThresholdAt k
  56  one_step_ratio : ∀ k, qecThresholdAt (k + 1) = qecThresholdAt k * phi⁻¹
  57  adjacent_ratio : ∀ k, qecThresholdAt (k + 1) / qecThresholdAt k = phi⁻¹
  58
  59/-- QEC threshold certificate. -/
  60def qecThresholdCert : QECThresholdCert where
  61  threshold_pos := qecThresholdAt_pos
  62  one_step_ratio := qecThresholdAt_succ_ratio
  63  adjacent_ratio := qecThresholdAt_adjacent_ratio
  64
  65end
  66end QuantumErrorCorrectionThreshold
  67end Information
  68end IndisputableMonolith
  69