QECThresholdCert
The QECThresholdCert structure packages positivity and exact phi-inverse scaling for the threshold function qecThresholdAt on the phi-ladder. Quantum information researchers studying fault-tolerant thresholds would cite it to link surface-code and colour-code empirical values to the Recognition Science ladder. The definition is a direct packaging of three properties taken from the explicit formula qecThresholdAt k = phi^{-k}/2.
claimLet $t(k) = phi^{-k}/2$ for $k$ a natural number. The structure asserts $t(k) > 0$ for every $k$, $t(k+1) = t(k) * phi^{-1}$, and $t(k+1)/t(k) = phi^{-1}$.
background
The module defines qecThresholdAt k := phi^{-k}/2, locating the QEC fault-tolerance threshold on the phi-ladder with higher rungs giving lower thresholds. This extends the Recognition Science treatment of information quantities already present in QuantumChannelCapacityFromPhi and PolarCodeGapFromPhi. The upstream structure QECThresholdCert in QECThresholdFromPhiLadder adds a five-family cardinality requirement and a phi-decay field; the present structure supplies the matching positivity and ratio properties for the explicit formula.
proof idea
The declaration is a structure definition whose three fields are populated directly from the lemmas qecThresholdAt_pos, qecThresholdAt_succ_ratio and qecThresholdAt_adjacent_ratio. No tactics are used; the downstream def qecThresholdCert simply supplies those lemmas to each field.
why it matters in Recognition Science
The structure supplies the local certificate required by the downstream qecThresholdCert construction in the same module and by the fuller QECThresholdCert in QECThresholdFromPhiLadder. It realises the module claim that adjacent-code-family thresholds ratio by exactly phi, consistent with the phi-ladder and the eight-tick octave in the forcing chain. No open scaffolding remains inside the module.
scope and limits
- Does not prove existence of any quantum code attaining the threshold.
- Does not derive phi or the ladder from the T0-T8 forcing chain.
- Does not treat error rates above the threshold.
- Does not connect to Berry creation or Z_cf.
formal statement (Lean)
54structure QECThresholdCert where
55 threshold_pos : ∀ k, 0 < qecThresholdAt k
56 one_step_ratio : ∀ k, qecThresholdAt (k + 1) = qecThresholdAt k * phi⁻¹
57 adjacent_ratio : ∀ k, qecThresholdAt (k + 1) / qecThresholdAt k = phi⁻¹
58
59/-- QEC threshold certificate. -/