qecThresholdAt_succ_ratio
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.