ErrorCorrectionCert
plain-language theorem explainer
ErrorCorrectionCert packages the positivity of the surface code threshold with the zero-cost condition when actual and threshold rates coincide and the non-negativity of the J-derived error rate cost. Quantum information theorists applying Recognition Science to fault-tolerant thresholds would cite this when checking consistency between the predicted J(φ)/10 value and observed surface-code performance. The declaration is a direct structure definition that records the three properties from the module's auxiliary definitions without additional le
Claim. A structure certifying that the surface code threshold satisfies $0 < p_{th}$, that the J-cost of the error-rate ratio vanishes whenever the actual rate equals the threshold rate, and that the J-cost remains non-negative for all positive actual and threshold rates, where the cost is obtained by applying the J-function to the ratio of the two rates.
background
In Recognition Science the J-cost of a recognition event is given by J(x) = (x + x^{-1})/2 - 1. The present module defines surfaceCodeThreshold as recognitionQuantum/10 and errorRateCost(a,t) as Jcost(a/t). Upstream, cost_nonneg from ObserverForcing states that the cost of any recognition event is non-negative, while the surfaceCodeThreshold definition imported from QuantumErrorCorrection supplies the baseline empirical scale of approximately 1%. The module's local setting is a structural theorem with zero axioms or sorries whose MODULE_DOC states the RS prediction that the fault-tolerance threshold lies near 1.18% and is consistent with the observed 0.5-2% band.
proof idea
The declaration is a structure definition that directly records the three fields threshold_pos, cost_at_threshold and cost_nonneg. It draws threshold_pos from the positivity lemma surfaceCodeThreshold_pos, cost_at_threshold from errorRateCost_at_threshold, and cost_nonneg from errorRateCost_nonneg, all defined in the same module. No tactics or external lemmas beyond these record fields are required.
why it matters
ErrorCorrectionCert is instantiated by the downstream definition cert and shown to be inhabited by cert_inhabited. It supplies the certificate that the RS-derived surface-code threshold J(φ)/10 lies inside the empirical window, thereby linking the J-cost model to the eight-tick octave and the phi-ladder of the forcing chain. The MODULE_DOC identifies the concrete falsifier as any surface-code implementation whose measured threshold falls outside (0.1%, 2%).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.