cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical threshold into a single certificate for three-deep error-correction capacity derived from J-cost. Anyone citing the structural Hamming-bound claim in this module will point at this bundle. The definition is a pure structure instance: each field is filled by a named sibling lemma.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $\tau$ is strictly positive.
background
The module treats error-correction capacity as a structural consequence of the Recognition Science J-cost. The Hamming bound $2^{n-k}\ge V_H(n,t)$ is read at the RS rate $R=J(\varphi)\approx 0.118$, which supports an error fraction $t/n=J(\varphi)/2\approx 0.059$. Status is structural: zero sorry, zero axiom.
Domain cost is the local cost functional on message/error pairs used to state the capacity claim; the certificate demands it vanish on the diagonal and stay nonnegative off it. The canonical threshold is the positive cutoff against which that cost is compared. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J$-cost nonnegativity on positive states.
proof idea
One-line structure instance. The three fields of ErrCorr3DeepCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No further tactic work; the certificate is just the packaging of those three facts.
why it matters
Gives a single named inhabitant of the error-correction certificate so downstream arguments can assume diagonal vanishing, nonnegativity, and a positive threshold without reopening the cost lemmas. The module frames this as the final-session structural theorem linking J-cost to Hamming capacity at the golden-ratio rate $J(\varphi)$. No further used-by edges are recorded yet; the immediate consumer is the inhabitedness witness in the same file. Framework landmarks in play are the unique J-cost (T5) and the forced self-similar scale $\varphi$ (T6), which fix the numerical rate and error fraction quoted in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.