cert_inhabited
plain-language theorem explainer
The declaration establishes existence of an ErrorCorrectionCert by exhibiting the concrete term cert. Quantum-computing theorists modeling surface-code thresholds inside the Recognition Science framework would cite it to confirm that the J-cost-derived threshold satisfies the packaged positivity and non-negativity axioms. The proof is a one-line term-mode construction that feeds the prior cert definition directly into the structure constructor.
Claim. There exists a structure ErrorCorrectionCert whose fields assert that the surface-code threshold is positive, that the error-rate cost vanishes whenever its two arguments are equal and nonzero, and that the cost function is nonnegative for all positive arguments.
background
The module derives a structural theorem for the surface-code fault-tolerance threshold from the J-cost function of Recognition Science. ErrorCorrectionCert is the structure that packages three concrete properties: positivity of surfaceCodeThreshold, the identity errorRateCost r r = 0 for r ≠ 0, and nonnegativity of errorRateCost a t whenever a > 0 and t > 0. These rest on the constants and cost primitives imported from IndisputableMonolith.Constants and IndisputableMonolith.Cost.
proof idea
The proof is a one-line term that constructs an inhabitant of ErrorCorrectionCert by applying the structure constructor to the preceding cert definition, which already supplies the three required fields.
why it matters
The theorem supplies the existence half of the structural theorem for the J-cost-derived surface-code threshold. It supports the Recognition Science prediction that the threshold lies near J(φ)/10 ≈ 1.18 % and remains consistent with the empirical band 0.5–2 %. The module falsifier is any engineered surface-code implementation whose observed threshold falls outside (0.1 %, 2 %).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.