cert
plain-language theorem explainer
Packages three structural facts into the RS path-integral certificate: domain cost vanishes on equal arguments, stays nonnegative for positive inputs, and the canonical threshold is positive. Anyone citing the Recognition selection of stationary (J=0) paths would reach for this witness. Construction is a pure structure fill from three sibling lemmas.
Claim. There is an RS path-integral 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
The module treats the Recognition Science reading of the path integral $Z = \int \mathcal{D}[\phi],\exp(iS[\phi]/\hbar)$. On a J-cost minimum path ($J=0$), the phase factor is stationary and $\exp(iS)=1$; off that locus the factor is damped by $\exp(-J(\phi^k))<1$, so Recognition selects the zero-cost paths.
Domain cost is the local cost functional on pairs of positive reals used in that selection story. The certificate structure bundles three elementary properties of that cost and of a fixed positive threshold. Upstream, nonnegativity of recognition-event cost is already known from the observer-forcing layer via $J$-cost nonnegativity.
proof idea
One-line structure inhabitant. The three fields of the certificate 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 reasoning.
why it matters
Gives a single named witness that the cost and threshold ingredients of the RS path-integral story are in place. The module is marked structural (zero sorry, zero axiom): this definition is the concrete certificate object that status refers to. It sits under the broader forcing picture in which $J$ is the unique cost (T5) and Recognition selects stationary paths. No downstream consumers are wired yet in the graph; the immediate sibling is the inhabitedness fact for the same certificate type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.