cert
plain-language theorem explainer
Packages three structural facts about the domain cost into a single certificate: it vanishes on the diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Anyone citing the golden-ratio J-cost minimum module uses this bundle. The definition is a pure structure inhabitant that wires 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
This module records the structural claim that the Recognition Science J-cost attains its golden-ratio minimum $J(\varphi)=\varphi-3/2\approx 0.11803$. The J-cost is the unique nonnegative cost functional forced by the Recognition Composition Law; on the positive reals it is $J(x)=(x+x^{-1})/2-1$.
Domain cost is the two-argument cost used for mass-energy pairs in this physics layer. The certificate structure demands three properties: vanishing when the two arguments coincide (and are nonzero), nonnegativity for positive arguments, and positivity of a fixed canonical threshold. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J$-cost nonnegativity on positive states.
proof idea
One-line structure inhabitant. Each field of the certificate is filled by a named sibling lemma already proved in the same module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No extra tactics or algebraic work occur at this site.
why it matters
Gives a single named witness that the structural hypotheses of RS Physics Structural Module 2 hold, so downstream physics arguments can assume diagonal vanishing, cost nonnegativity, and a positive threshold without reopening those lemmas. The module frames this as the golden-ratio recognition-cost fact $J(\varphi)=\varphi-3/2$, tying into the forcing chain (T5 J-uniqueness, T6 $\varphi$ as self-similar fixed point). No used_by edges are recorded yet; the companion cert_inhabited sibling is the natural next consumer. Status is fully closed (zero sorry, zero axiom).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.