qecThresholdAt
qecThresholdAt defines the quantum error correction threshold at rung k on the phi-ladder as phi to the power minus k divided by two. Researchers modeling fault-tolerant quantum computing in the Recognition Science framework cite this when aligning predicted thresholds with surface code and colour code benchmarks. The declaration is a direct equational definition that immediately enables the positivity and ratio theorems in the same module.
claimDefine the function $T:ℕ→ℝ$ by $T(k):=φ^{-k}/2$, giving the predicted fault-tolerance threshold for quantum error correction at the $k$-th rung of the phi-ladder.
background
The module sets the quantum error correction threshold on the phi-ladder, where the threshold is the physical error rate below which a quantum code suppresses logical errors exponentially. The Recognition Science structural prediction places these thresholds at values $φ^{-k}/2$ for rung $k$, with adjacent families differing by exactly $φ^{-1}$. The module documentation states: 'The RS structural prediction: the threshold sits on the φ-ladder, with adjacent-code-family thresholds rationing by exactly φ.' Empirical checks include the surface code threshold near $φ^{-9}/2$ and the colour code near $φ^{-8}/2$. Phi is the golden ratio, the self-similar fixed point from the forcing chain.
proof idea
The declaration is introduced by a direct equational definition with no lemmas or tactics applied.
why it matters in Recognition Science
This definition supplies the base function for the QECThresholdCert structure and the theorems qecThresholdAt_pos, qecThresholdAt_succ_ratio, and qecThresholdAt_adjacent_ratio. It fills the module's RS structural prediction for QEC thresholds on the phi-ladder. The construction aligns with the phi-ladder structure in related information modules and supports comparisons to empirical thresholds.
scope and limits
- Does not derive the phi-ladder placement from the J-cost or Recognition Composition Law.
- Does not prove numerical agreement with measured thresholds.
- Does not specify any concrete quantum code or error model.
- Does not connect to the eight-tick octave or spatial dimension steps.
Lean usage
example : qecThresholdAt 8 = phi ^ (-8 : ℤ) / 2 := rflformal statement (Lean)
33def qecThresholdAt (k : ℕ) : ℝ := phi ^ (-(k : ℤ)) / 2
proof body
Definition body.
34