qecThresholdCert
plain-language theorem explainer
qecThresholdCert constructs a certificate asserting exactly five QEC code families whose thresholds are positive and decay geometrically by the factor phi inverse between adjacent families. Researchers modeling quantum error correction thresholds under Recognition Science would cite it to confirm the phi-ladder prediction for code-family ratios. The definition is a direct record construction that supplies the three required fields from the lemmas on family count, threshold positivity, and decay ratio.
Claim. Let $QECThresholdCert$ be the structure whose fields require $|QECCodeFamily|=5$, $0< codeThreshold(k)$ for all $k$, and $codeThreshold(k+1)/codeThreshold(k)=phi^{-1}$ for all $k$. Then $qecThresholdCert$ is the term in this structure obtained by supplying the cardinality theorem for five families, the positivity theorem for each threshold, and the geometric decay theorem.
background
The module Quantum Error Correction Threshold from Phi-Ladder treats QEC code families (repetition, surface, colour, topological, concatenated) as having thresholds that decay by the factor $phi^{-1}$ between successive families, matching the Recognition Science prediction that adjacent ratios equal $1/phi$. The structure $QECThresholdCert$ packages three properties: the count of families equals five (identified with configDim $D=5$), every threshold is positive, and the decay ratio holds. Upstream results supply the ingredients: qecCodeFamilyCount proves the cardinality by decision, codeThreshold_pos derives positivity from $phi>0$, and codeThreshold_decay unfolds the power-law definition of codeThreshold to obtain the exact ratio $phi^{-1}$.
proof idea
The definition is a one-line wrapper that constructs the $QECThresholdCert$ record by assigning the five_families field to qecCodeFamilyCount, the threshold_pos field to codeThreshold_pos, and the phi_decay field to codeThreshold_decay. No additional tactics or reductions are performed.
why it matters
This definition supplies the concrete phi-ladder witness for QEC thresholds and is invoked by the general qecThresholdCert in QuantumErrorCorrectionThreshold. It realizes the framework claim that code-family thresholds ratio by $1/phi$, consistent with the surface-code value near $phi^{-9}$. The construction closes the five-family scaffolding in the Information domain while inheriting the forcing-chain landmarks T5 (J-uniqueness), T6 (phi fixed point), and T7 (eight-tick octave) from the parent UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.