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