Information Quantum Error Correction Threshold Qec Threshold At Adjacent Ratio

The adjacent ratio

Quantum error correction is the art of protecting quantum information from noise. A quantum code stores a logical qubit across many physical qubits, and the fault-tolerance threshold is the error rate per physical operation below which the code suppresses logical errors exponentially. Below that rate, adding more physical qubits makes the logical qubit more reliable; above it, the code makes things worse. The threshold is a property of the code family and its decoder, and it is a practical engineering target for building a quantum computer.

The Recognition Science framework defines a sequence of numbers, qecThresholdAt k, as phi raised to the power minus k, divided by 2, where phi is the golden ratio, about 1.618. The declaration qecThresholdAt_adjacent_ratio proves a structural fact about this sequence: the ratio of the value at rung k plus 1 to the value at rung k equals phi to the minus 1, which is about 0.618. In other words, each step down the ladder multiplies the threshold by the reciprocal of the golden ratio. The proof is a short chain: the definition of the sequence, a theorem that the next value equals the current value times phi to the minus 1, and then division by the current value, which is positive by a separate theorem. The library also packages these facts into a certificate structure, QECThresholdCert, that bundles the positivity, the one-step ratio, and the adjacent ratio into one object.

In Recognition Science, the golden ratio is not a free parameter. It is forced by a proved theorem from five plain conditions on a cost function, and the framework models physical constants as sitting on a phi-power ladder. The QEC threshold sequence is one more rung on that ladder: the framework predicts that real code thresholds, such as the surface code at about 1 percent and the colour code at about 1.7 percent, sit at rungs 9 and 8 respectively, and that the ratio between adjacent code families is approximately phi. The empirical bench in the library lists these numbers as a check, not as a theorem.

What the declaration does not claim is equally precise. The theorem qecThresholdAt_adjacent_ratio is about the defined sequence, not about any physical code. It does not prove that the surface code threshold is exactly phi to the minus 9 over 2, nor that the colour code threshold is exactly phi to the minus 8 over 2. Those are empirical comparisons, with measured values that carry uncertainty. The theorem also does not prove that real quantum error correction thresholds form a phi-ladder; it proves that the sequence the framework defines has that property. The framework's claim that real thresholds follow this ladder is a prediction, and the named falsifier is a measured adjacent ratio that departs from phi by more than the empirical uncertainty.

theorem qecThresholdAt_adjacent_ratio (k : ℕ) :
    qecThresholdAt (k + 1) / qecThresholdAt k = phi⁻¹ := by
  rw [qecThresholdAt_succ_ratio]
  field_simp [(qecThresholdAt_pos k).ne']

theorem qecThresholdAt_succ_ratio (k : ℕ) :
    qecThresholdAt (k + 1) = qecThresholdAt k * phi⁻¹ := by
  unfold qecThresholdAt
  have hphi_ne := Constants.phi_ne_zero
  have : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
    rw [zpow_add₀ hphi_ne]; simp
  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  rw [hcast, this]; ring

theorem qecThresholdAt_pos (k : ℕ) : 0 < qecThresholdAt k := by
  unfold qecThresholdAt
  exact div_pos (zpow_pos Constants.phi_pos _) (by norm_num)

/-- QEC threshold at φ-ladder rung `k` below unity (higher rung = lower threshold). -/
def qecThresholdAt (k : ℕ) : ℝ := phi ^ (-(k : ℤ)) / 2

What this page does not claim

This theorem does not prove that any real quantum error correction code has a threshold equal to a phi-ladder value. The empirical bench values for the surface and colour codes are measurements with uncertainty, not theorem outputs. The declaration does not establish that the golden ratio itself is the correct scaling for physical thresholds outside the framework's model.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/QuantumErrorCorrectionThreshold.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: