qecThresholdAt_adjacent_ratio
The ratio of quantum error correction thresholds at consecutive rungs on the phi-ladder equals phi inverse. Quantum information researchers studying fault-tolerant thresholds would cite this to confirm the geometric scaling predicted by Recognition Science. The proof is a direct algebraic reduction that invokes the successor ratio identity and clears the denominator via positivity.
claimFor every natural number $k$, the ratio of the QEC threshold at rung $k+1$ to the threshold at rung $k$ equals $phi^{-1}$, where the threshold at rung $k$ is $phi^{-k}/2$.
background
The module states that the quantum error correction fault-tolerance threshold lies on the phi-ladder, with adjacent-code-family thresholds in exact ratio phi. The threshold function is defined as $phi^{-k}/2$ for rung $k$, yielding values near 0.011 at rung 9 and 0.017 at rung 8 that align with surface-code and colour-code benchmarks within empirical uncertainty.
proof idea
The proof rewrites the numerator via the successor ratio lemma qecThresholdAt_succ_ratio, which states that the threshold at $k+1$ equals the threshold at $k$ times $phi^{-1}$. It then applies field_simp, using the non-zero fact from qecThresholdAt_pos, to reduce the ratio directly to $phi^{-1}$.
why it matters in Recognition Science
This theorem supplies the adjacent ratio field of the QEC threshold certificate qecThresholdCert. It instantiates the self-similar fixed-point property of phi from the Recognition Science forcing chain at the level of error thresholds, supporting the structural prediction that QEC thresholds compound with other phi-based quantities in the Information module.
scope and limits
- Does not derive absolute threshold values from microscopic error models.
- Does not address finite-size effects or specific code constructions.
- Does not prove numerical agreement with observed thresholds beyond the ratio.
- Does not extend the relation to non-adjacent rungs.
formal statement (Lean)
49theorem qecThresholdAt_adjacent_ratio (k : ℕ) :
50 qecThresholdAt (k + 1) / qecThresholdAt k = phi⁻¹ := by
proof body
Term-mode proof.
51 rw [qecThresholdAt_succ_ratio]
52 field_simp [(qecThresholdAt_pos k).ne']
53