ErrCorr3DeepCert
plain-language theorem explainer
A certificate packing three analytic facts about the domain cost used for three-deep error-correction capacity: diagonal vanishing, nonnegativity off the identity, and a strictly positive canonical threshold. Anyone citing the structural Hamming-bound claim at rate J(φ) needs this bundle. It is a pure structure definition; inhabitants are assembled from sibling lemmas.
Claim. A certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module derives error-correction capacity from the Recognition Science J-cost. Module status is structural (zero sorry, zero axiom): at coding rate $R = J(\varphi) \approx 0.118$ the code supports error fraction $t/n = J(\varphi)/2 \approx 0.059$, matching a Hamming-bound reading $2^{n-k} \ge V_H(n,t)$.
Domain cost is the local cost functional on message/error pairs that the capacity argument uses; the canonical threshold is the positive cutoff separating correctable from uncorrectable regimes. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via Jcost_nonneg, which is the same positivity principle the domain-cost nonnegativity field reuses.
The structure does not itself compute rates; it packages the three inequalities the later capacity certificate must discharge.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Downstream, the definition cert fills them by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then witnesses Nonempty by packaging that inhabitant.
why it matters
This is the interface type for the module's structural error-correction theorem. Downstream cert is the concrete inhabitant and cert_inhabited proves the type is nonempty, closing the certificate side of the "Error Correction Capacity from J-Cost Deep" claim.
In the RS framework the rate is forced by the unique J-cost (T5: $J(x)=(x+x^{-1})/2-1$) evaluated at the golden self-similar point $\varphi$ (T6). The certificate isolates exactly the cost positivity and threshold facts needed before one can quote the Hamming volume bound at $R=J(\varphi)$ and $t/n=J(\varphi)/2$. It does not reopen the forcing chain; it sits in the information layer that consumes those constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.