PathIntegral_RS_v3Cert
plain-language theorem explainer
Certificate structure packaging three analytic facts used by the RS path-integral story: diagonal domain cost vanishes, domain cost is nonnegative on positive arguments, and the canonical threshold is positive. Downstream code cites it via a concrete inhabited instance. Pure definitional packaging of field obligations; no proof body.
Claim. A certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the RS reading of the path integral $Z=\int\mathcal{D}[\phi],e^{iS[\phi]/\hbar}$. Recognition Science selects stationary paths at the $J$-cost minimum ($J=0$), where the phase factor is $1$; off those paths the weight is suppressed by a factor $e^{-J(\phi^k)}<1$.
Domain cost is the local cost functional on pairs of positive reals that appears in that selection rule; the diagonal identity $r\mapsto(r,r)$ is the zero-cost locus. The canonical threshold is the positive cutoff used to separate on-path from off-path contributions.
Upstream, nonnegativity of recognition-event cost is already forced by $J$-cost nonnegativity on positive states (cost_nonneg in ObserverForcing). The present structure lifts that style of bound into the path-integral certificate interface.
proof idea
No proof: the declaration is a structure whose three fields are Prop-valued obligations. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The companion theorem cert_inhabited then wraps that instance as Nonempty.
why it matters
Gives a single named bundle for the structural hypotheses of Path Integral RS v3 (module status: structural theorem, zero sorry/axiom). Downstream cert is the concrete witness and cert_inhabited records that the certificate type is nonempty, so later physics lemmas can assume the package rather than restate the three inequalities.
In the RS forcing picture this sits under the $J$-cost story (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) and the stationary-phase claim that recognition selects $J=0$ paths. It does not yet evaluate the full integral or derive particle spectra; it only freezes the cost and threshold axioms the v3 path-integral narrative needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.