cert
plain-language theorem explainer
Packages three structural facts about the domain J-cost into one certificate: it vanishes on the diagonal, stays non-negative for positive mass and energy, and the canonical collapse threshold is positive. Cite this when invoking the wavefunction-collapse-from-J-cost structural package. The definition is a field-by-field assembly of three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) the domain cost of equal arguments vanishes, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical collapse threshold is strictly positive.
background
This module treats objective wavefunction collapse (GRW-style) as a structural consequence of the Recognition Science J-cost. The J-cost is the unique cost functional forced by the Recognition Composition Law; here it is specialized to a two-argument domain cost on mass and energy scales. The module status is structural: zero sorry, zero axioms.
The certificate type bundles three properties needed before any collapse-rate claim: the cost is zero when the two arguments coincide (identity event at the J-minimum), the cost is non-negative off that locus, and a fixed positive threshold exists against which collapse is measured. Upstream, non-negativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: the cost of any recognition event is non-negative), via Jcost_nonneg.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields. The module notes that a naive GRW rate match is off by many orders; the present object is only the structural certificate, not a numerical fit.
proof idea
One-line structure construction. Each field of WFCollapse3Cert is filled by the corresponding sibling lemma: diagonal vanishing by domainCost_at_eq, non-negativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No additional reasoning.
why it matters
Gives a single inhabited certificate for the structural half of the wavefunction-collapse-from-J-cost story (Plan v7, 115th pass). Downstream consumers can assume diagonal vanishing, cost non-negativity, and a positive canonical threshold without re-proving them. The module frames objective collapse rate as $\lambda = J(\phi)/(m_{\mathrm{nucleon}}\phi^{20})$; this certificate does not close the numerical gap (module notes ~38 orders off at the naive GRW scale) but locks the algebraic prerequisites tied to the forced J-cost (T5) and $\phi$. No used_by edges are recorded yet; the natural consumer is any later collapse-rate or decoherence theorem that needs the bundle inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.