cert
plain-language theorem explainer
Packages three structural facts about the domain cost into a single certificate for the RS Lagrangian density: diagonal vanishing, non-negativity, and a positive canonical threshold. Anyone working the J-cost action principle cites this inhabited record. The definition is a pure structure assembly wiring three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(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 builds the Recognition Science Lagrangian density from the J-cost: $L_{RS} = \int J(\varphi^r),dr - \sum_k J(\varphi^k)\delta(r-\mathrm{rung}_k)$. In RS the Lagrangian is the J-cost on field configurations, and the action principle $\delta S=0$ yields J-cost minimization equations. Status is structural (zero sorry, zero axiom).
The certificate type bundles three properties of the domain cost used by that construction: vanishing when the two arguments agree and are nonzero, non-negativity on the positive quadrant, and positivity of a fixed canonical threshold. Upstream, non-negativity of recognition-event cost is already known from ObserverForcing via $J$-cost non-negativity on positive states; the identity event sits at the $J$-minimum $x=1$.
proof idea
One-line structure inhabitant. Each field of RSLagrangian3Cert is filled by a sibling lemma already in the module: diagonal vanishing by domainCost_at_eq, non-negativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No new algebra is performed.
why it matters
This is the inhabited certificate that the module's structural theorem hangs on: once the three domain-cost facts are packaged, downstream code can treat the RS Lagrangian-from-J-cost setup as a single certified object rather than three loose lemmas. It sits in the Foundation layer that connects the forcing-chain J-uniqueness (T5: $J(x)=(x+x^{-1})/2-1$) to a concrete action density on the $\varphi$-ladder. No further used-by edges are recorded yet; the immediate consumer is the module's own cert_inhabited and any later Euler-Lagrange or minimization arguments that require a single RSLagrangian3Cert value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.