cert
plain-language theorem explainer
Packages the three algebraic facts that certify the D=3 recognition configuration space: the domain cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Anyone citing the structural D=3 metric setup uses this certificate object. The definition is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is a D=3 configuration-space certificate: for every nonzero real $r$, the domain cost satisfies $\mathrm{cost}(r,r)=0$; for all positive $m,e$, $\mathrm{cost}(m,e)\ge 0$; and the canonical threshold is strictly positive.
background
The module fixes the Recognition Science configuration space at spatial dimension three: $C_3=\mathbb{R}^3$ equipped with the recognition metric $ds^2=J(dx/x)$ on the positive orthant, asserted positive definite for all $x>0$. Here $J$ is the unique cost functional forced by the Recognition Composition Law (T5), $J(x)=(x+x^{-1})/2-1$.
The certificate structure collects three elementary properties of the domain cost and the canonical threshold used to police that metric: diagonal vanishing (zero self-cost), nonnegativity on the positive orthant, and a strictly positive threshold scale. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J\ge 0$ for positive states.
Status of the module is structural: zero sorry, zero axioms.
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis occurs.
why it matters
Gives a single named witness that the D=3 configuration-space cost data meet the minimal certificate interface required by the foundation layer. It sits under the T8 forcing step that locks spatial dimension to three and under the Riemannian J-metric story for $C_3$. Downstream use is not yet wired in this graph (zero used-by edges), so the object presently serves as the inhabitation anchor for the certificate type and as a stable API point for later metric or observer lemmas. No open scaffold remains: the module claims a complete structural theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.