cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single RS summary certificate: the cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the Plan-v7 structural summary will point here for the inhabited certificate object. The body is a pure structure instance, wiring three sibling lemmas into the fields.
Claim. There is a certificate object whose three fields assert: (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 is the Plan-v7 Recognition Science complete summary certificate: a structural package (zero sorry, zero axiom) that records the forced J-cost $J(x)=(x+x^{-1})/2-1$ and the consequences claimed from it (phi, gap-45, $D=3$, derived constants).
domainCost is the local real-pair cost used in this summary layer; the sibling lemmas domainCost_at_eq and domainCost_nonneg state that it vanishes when the two arguments agree (nonzero) and stays nonnegative for positive arguments. canonicalThreshold is the positive cutoff used by the same summary layer.
Upstream, ObserverForcing already has the event-level fact that every recognition-event cost is nonnegative via Cost.Jcost_nonneg. The present certificate is the summary-level packaging of the analogous domain-cost statements plus threshold positivity.
proof idea
Pure structure construction. The three fields of RSSummary3Cert are filled by the three sibling lemmas already proved in-module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No new algebra is performed.
why it matters
Gives an inhabited Plan-v7 summary certificate so downstream code can depend on one object rather than three separate lemmas. It sits in the Foundation summary layer that advertises the forced J-equation (T5 landmark), phi, gap-45, and $D=3$. No used_by edges are recorded yet; the sibling cert_inhabited is the natural consumer. It does not itself re-prove J-uniqueness or the forcing chain; it only bundles the local cost and threshold facts the summary wants on the shelf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.