WFCollapse3Cert
plain-language theorem explainer
Certificate packing three structural properties for J-cost wavefunction collapse: domain cost vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is positive. Downstream code builds a concrete inhabited instance from sibling lemmas. Pure structure definition with no proof obligations of its own.
Claim. A certificate consists of three facts: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive mass $m$ and energy $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical collapse threshold is strictly positive.
background
The module derives a structural GRW-style objective collapse threshold from the Recognition Science J-cost. In RS, the cost functional is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law and the T5 step of the forcing chain. Collapse rate is written schematically as $\lambda=J(\varphi)/(m_{\mathrm{nucleon}}\varphi^{20})$; the module flags that the naive numerical match is off by many orders and treats the claim as structural only.
Domain cost is the local cost assigned to a mass-energy pair in this collapse setting; the diagonal identity $C(r,r)=0$ encodes zero cost for matched recognition. The canonical threshold is the positive cutoff against which that cost is compared. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J$-cost nonnegativity on positive states.
proof idea
No proof body: this is a structure declaration. It packages three proposition-valued fields (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert instance, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named bundle for the three algebraic facts the collapse-from-J-cost story needs before any rate formula is stated. Downstream, cert assembles a concrete value and cert_inhabited records Nonempty of the certificate type, closing the module's structural theorem (0 sorry, 0 axiom).
In the broader RS picture this sits under physics derived from J-uniqueness (T5) and the golden ratio fixed point $\varphi$ (T6), not under the eight-tick or $D=3$ forcing steps. The module doc is explicit that the GRW numerical target ($\sim 10^{-16},\mathrm{s}^{-1}$) is not recovered: the structural skeleton is certified, the absolute scale remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.