qecThresholdCert
plain-language theorem explainer
The definition assembles the QEC threshold certificate by packaging positivity and exact phi-inverse ratio properties of the threshold function on the phi-ladder. Researchers modeling fault-tolerant quantum computation would cite it to embed empirical thresholds (surface code near rung 9, colour code near rung 8) into the Recognition Science structure. It is a one-line wrapper that instantiates the required structure fields from three local theorems.
Claim. The QEC threshold certificate asserts that for every natural number $k$ the threshold value at rung $k$ is positive, the threshold at rung $k+1$ equals the threshold at rung $k$ multiplied by $phi^{-1}$, and the ratio of thresholds at adjacent rungs equals $phi^{-1}$.
background
The module defines the threshold function on the phi-ladder and supplies the certificate structure QECThresholdCert whose fields are positivity for all rungs, one-step multiplicative decay by $phi^{-1}$, and adjacent ratio exactly $phi^{-1}$. The local setting states that the quantum error correction fault-tolerance threshold sits on the phi-ladder with adjacent-code-family thresholds rationing by exactly phi, matching empirical values such as surface code threshold approximately 1 percent at rung 9 and colour code approximately 1.7 percent at rung 8. Upstream results supply the supporting theorems that establish positivity via zpow positivity and the two ratio identities via algebraic simplification of the exponent.
proof idea
The definition is a one-line wrapper that instantiates the QECThresholdCert structure by direct assignment of its three fields to the theorems qecThresholdAt_pos, qecThresholdAt_succ_ratio, and qecThresholdAt_adjacent_ratio.
why it matters
This certificate supplies the core positivity and ratio properties required by the downstream QECThresholdCert in QECThresholdFromPhiLadder, which augments the structure with the fixed count of five code families. It realizes the module claim that adjacent thresholds ratio by exactly phi, aligning with the phi-ladder structure forced by the T5 J-uniqueness and T6 self-similar fixed point in the unified forcing chain. The declaration closes the local information-domain scaffolding for the QEC prediction with no remaining open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.