RSFDNStructural002Cert
plain-language theorem explainer
Certificate structure that packages three structural obligations on the domain recognition cost: it vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone discharging Foundation structural module 2 (J-cost minimum near the golden ratio) cites this bundle. It is a pure structure definition; sibling lemmas fill the fields when the certificate is inhabited.
Claim. A structural certificate is a triple of facts: for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
This module is Foundation RS Structural Module 2. Its stated target is the RS J-cost minimum at the golden ratio: $J(\varphi)=\varphi-3/2\approx 0.11803$, the golden-ratio recognition cost, recorded as a structural theorem with no sorry and no axioms.
The local cost object is a real bivariate domain cost (pairs of positive scale parameters). The diagonal vanishing clause says equal arguments incur zero cost; nonnegativity restricts to the positive orthant. The canonical threshold is a fixed positive real used as a cutoff in the same module.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative, via nonnegativity of the J-cost on positive states. The present structure lifts that style of cost inequality into an explicit three-field certificate for the structural module.
proof idea
No proof body: this is a structure whose three fields are propositions. Inhabitation is deferred to the sibling definition that assigns domainCost_at_eq to the diagonal clause, domainCost_nonneg to the positivity clause, and canonicalThreshold_pos to the threshold clause. Those siblings are ordinary lemmas; the structure only names the interface they must satisfy.
why it matters
The certificate is the typed obligation that Foundation structural module 2 must discharge. Downstream, a concrete inhabitant is built by wiring the three sibling lemmas, and cert_inhabited records that the type is nonempty.
In the broader Recognition chain this sits next to T5 (J-uniqueness: $J(x)=(x+x^{-1})/2-1$) and T6 ($\varphi$ forced as the self-similar fixed point). Packaging diagonal vanishing plus nonnegativity is exactly the algebraic shape of a cost minimum; the module doc pins that minimum at $\varphi$. The structure itself does not compute $J(\varphi)$, but it is the formal hook later steps use when they quote the golden-ratio recognition cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.