qecThresholdAt_succ_ratio
The result shows that successive quantum error correction thresholds on the phi-ladder form a geometric sequence with common ratio phi inverse. Workers on fault-tolerant quantum computation within Recognition Science cite this to establish the exact scaling between adjacent code families. The proof unfolds the explicit definition of the threshold function and reduces the exponent shift via the addition formula for integer powers of phi, using that phi is nonzero.
claimFor every natural number $k$, if the quantum error correction threshold at rung $k$ is given by $phi^{-k}/2$, then the threshold at rung $k+1$ equals that value multiplied by $phi^{-1}$.
background
The module defines the threshold function on the phi-ladder as the map sending rung $k$ to $phi^{-k}/2$, placing the fault-tolerance threshold at successive rungs. This sits inside the broader Recognition Science derivation of information quantities from the phi fixed point. Upstream, the lemma that phi is nonzero supplies the non-vanishing needed for the power identities, while the definition itself comes from the same module.
proof idea
The proof unfolds the definition of the threshold function, introduces the fact that phi is nonzero, rewrites the exponent -(k+1) as -k + (-1) by ring, applies the integer power addition identity, casts the natural number to integer, and finishes with ring simplification.
why it matters in Recognition Science
This theorem supplies the one-step ratio used to build the QEC threshold certificate and the adjacent-ratio lemma in the same module. It realizes the module claim that adjacent-code-family thresholds ration by exactly phi, consistent with the phi-ladder structure. The result closes the scaling relation needed for the empirical bench against surface and colour codes.
scope and limits
- Does not derive the absolute placement of any threshold from first principles.
- Does not address concrete error models beyond the structural phi scaling.
- Does not compute explicit code distances or logical error rates.
Lean usage
rw [qecThresholdAt_succ_ratio]formal statement (Lean)
39theorem qecThresholdAt_succ_ratio (k : ℕ) :
40 qecThresholdAt (k + 1) = qecThresholdAt k * phi⁻¹ := by
proof body
Tactic-mode proof.
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