cert
plain-language theorem explainer
Packages three structural properties of the domain cost on the recognition manifold into one certificate: diagonal vanishing, non-negativity off the axes, and a strictly positive canonical threshold. Gravity and geodesic analyses in Recognition Science cite this bundle when they need the cost landscape ready as a single object. The construction is a structure instance that wires three local lemmas.
Claim. There is a certificate asserting that the domain cost $C$ on the recognition manifold satisfies $C(r,r)=0$ for every $r\neq 0$, that $C(m,e)\geq 0$ whenever $m>0$ and $e>0$, and that the canonical threshold is strictly positive.
background
The module treats geodesics on the recognition manifold as curves that minimize the action $\int J(r(t)),dt$, where $J$ is the unique cost forced by the Recognition Composition Law (the T5 fixed point $J(x)=(x+x^{-1})/2-1$). At $J=0$ the geodesic is a recognition ground-state orbit; the first departure from a straight trajectory occurs at the cost level $J(\varphi)$.
The domain cost is the concrete bivariate cost used on this manifold. The certificate structure packages three elementary properties of that cost: it vanishes on the diagonal away from zero, it is non-negative for positive arguments, and a fixed positive threshold (the canonical threshold) sits above the ground state. Upstream, non-negativity of recognition-event cost is already known from the observer-forcing layer via non-negativity of $J$ on positive reals.
proof idea
One-line structure instance. The three fields of the certificate are filled by the local lemmas that the domain cost vanishes on the diagonal, that it is non-negative for positive mass and energy arguments, and that the canonical threshold is positive. No further rewriting is required.
why it matters
Gives gravity and geodesic code a single inhabited certificate that the cost landscape is a genuine non-negative action with a positive first-departure scale. That is the structural prerequisite for reading recognition geodesics as minimizers of $\int J$ and for locating the $J(\varphi)$ threshold as the first bend away from the ground-state orbit (module status: structural theorem, zero sorry). It sits on the gravity side of the forcing chain after T5 $J$-uniqueness and the $\varphi$ fixed point, and it makes the deep geodesic certificate available without re-proving the three cost facts at each use site. No downstream consumers are recorded yet; the immediate role is to close the certificate interface for this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.