qecCert
plain-language theorem explainer
qecCert assembles a QEC certificate asserting five code families, zero J-cost at unit rate, strictly positive J-cost for all other physical rates, and exactly eight DFT modes. Physicists modeling phi-harmonic error correction would cite it to confirm the below-threshold regime J(r) < J(φ). The definition is a direct structure instantiation that packages four sibling results without further reasoning.
Claim. The QEC certificate is the structure whose fields are: cardinality of QEC code types equals 5; J-cost at rate 1 equals 0; J-cost(r) > 0 for every real r satisfying 0 < r ≠ 1; and the number of DFT-8 modes equals 8.
background
The module implements RS patent 015 on phi-harmonic QEC scheduling. Error correction is effective precisely when the error rate r satisfies J(r) < J(φ) with J(φ) in (0.11, 0.13); above that band the errors become uncorrectable. Five code families (repetition, surface, colour, topological, flag) are required, matching configDim D = 5. The protocol employs DFT-8 harmonic pulse scheduling at 5φ Hz. Jcost is the Recognition Science cost function obeying the composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and the fixed-point relation at φ. dft8ModeCount records the eight modes arising from the eight-tick octave (period 2^3).
proof idea
The definition constructs the QECCert structure by direct field assignment: five_codes is set to qecCodeCount, threshold_zero to below_threshold_correct, error_positive to logical_error_positive, and dft8_count to dft8_eq_8. No tactics or reductions are performed; it is a pure structure builder.
why it matters
qecCert supplies the single concrete certificate demanded by the RS QEC protocol (patent 015) and packages the four supporting results into one object. It directly realises the threshold crossing condition and the DFT-8 count required by the eight-tick octave (T7). Because used_by_count is zero, the declaration serves as the terminal interface for any downstream derivation that needs a verified QEC certificate in the J-cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.