codeThreshold_decay
plain-language theorem explainer
The declaration proves that successive QEC code thresholds on the phi-ladder satisfy the constant ratio phi inverse. Researchers modeling quantum error correction from Recognition Science would cite the result when confirming geometric decay across the five canonical families. The proof is a short algebraic reduction that unfolds the explicit definition of codeThreshold and cancels using the non-vanishing of phi.
Claim. For every natural number $k$, the ratio of successive code thresholds satisfies $codeThreshold(k+1)/codeThreshold(k)=phi^{-1}$, where $codeThreshold(k)$ denotes $phi^{-k}$.
background
The module derives QEC code thresholds from the phi-ladder. The definition codeThreshold(k) equals the reciprocal of phi to the power k, assigning each rung a predicted error threshold that decreases geometrically. Upstream results supply phi positive and nonzero, which license the field operations. The module setting states that the five canonical families (repetition, surface, colour, topological, concatenated) exhibit adjacent thresholds in the ratio 1/phi, with the surface-code value near phi to the minus nine.
proof idea
The proof unfolds codeThreshold to expose the ratio of consecutive inverse powers. It obtains a non-zero witness from positivity of phi to the k, rewrites the successor power via the exponent rule, and finishes by field simplification that cancels the common phi factors using the non-vanishing lemma.
why it matters
The result supplies the phi-decay field of the QECThresholdCert certificate, which also records the five-family count and threshold positivity. It realizes the Recognition Science claim that code-family thresholds form a geometric sequence with common ratio phi inverse, consistent with the phi-ladder and the predicted surface-code scale near 1.3 percent. The certificate closes the information module by delivering a single verified object for downstream reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.