cert
plain-language theorem explainer
Packages three elementary properties of the domain cost and canonical threshold into a single vacuum-field certificate. Anyone citing the recognition-field vacuum energy density construction uses this bundle as the standing hypothesis pack. The definition is a pure structure instance that wires three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ vanishes; (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 treats vacuum energy density in Recognition Science units as $\rho_{\mathrm{vac}} = J(\varphi)/\varphi^5$, with the RS vacuum identified as the ground state of the recognition field (all $J$-costs zero). The cost functional is the standard RS $J$-cost $J(x) = (x+x^{-1})/2-1$, nonnegative and minimized at the identity $x=1$.
Domain cost is the local cost assigned to a mass/energy pair in the recognition field; the certificate demands it vanish on the diagonal (equal arguments) and stay nonnegative off it. The canonical threshold is the positive cutoff used to separate vacuum from excited recognition events.
Upstream, nonnegativity of recognition-event cost is already recorded as $0 \le e.\mathrm{cost}$ via $J$-cost nonnegativity on positive states.
proof idea
One-line structure instance. The three fields of RecogFieldVac3Cert are filled by the sibling lemmas that domain cost vanishes on equal nonzero arguments, that domain cost is nonnegative for positive mass and energy, and that the canonical threshold is positive. No further rewriting or case analysis.
why it matters
Gives a single named inhabitant of the vacuum-field certificate used throughout the Plan v7 vacuum-energy density development. The module status is structural theorem (zero sorry, zero axiom): this definition is the packaging step that makes the three local facts available as one object for any later argument that the RS vacuum is the $J=0$ ground state and that $\rho_{\mathrm{vac}} = J(\varphi)/\varphi^5$ is well-posed.
It sits under the Foundation forcing chain landmarks that fix $J$ (T5) and $\varphi$ (T6), and under the global cost nonnegativity fact from observer forcing. No downstream consumers are recorded yet; the immediate sibling is the inhabitedness wrapper that exposes this certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.