cert
plain-language theorem explainer
Packages three elementary properties of the domain cost and the canonical collapse threshold into a single RS wave-function collapse certificate. Anyone citing the structural collapse theorem (measurement as ledger posting / J-cost minimization to the nearest rung) uses this bundle. The definition is a pure structure inhabitant: it wires three already-proved lemmas into the certificate fields.
Claim. There is a collapse certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for every $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
In this module, wave-function collapse is identified with a recognition event: a ledger posting whose timing is constrained by the eight-tick cycle, and whose outcome is J-cost minimization onto the nearest rung of the $\varphi$-ladder. No hidden variables are introduced; the status line marks the development as a structural theorem (zero sorry, zero axiom).
The certificate structure collects the minimal analytic facts needed for that story. Domain cost is the cost functional on measurement/eigenvalue pairs; it must vanish when the two arguments agree (identity recognition) and stay non-negative off the diagonal for positive inputs. The canonical threshold is the positive cutoff that separates a genuine collapse posting from sub-threshold noise.
Upstream, non-negativity of recognition-event cost is already available from ObserverForcing via $J$-cost non-negativity on positive states. The three field lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the structure obligations locally.
proof idea
One-line structure inhabitant. The three fields of RSWFCollapseCert are filled by direct assignment: diagonal vanishing from domainCost_at_eq, non-negativity from domainCost_nonneg, and positivity of the threshold from canonicalThreshold_pos. No further rewriting or case analysis.
why it matters
Gives a single named witness that the cost/threshold side conditions of RS collapse are inhabited, so downstream arguments can quote one object rather than three separate lemmas. Fits the module claim that collapse is J-cost minimization to the nearest rung under the eight-tick minimal recognition time (T7 in the forcing chain). Used_by is currently empty; the sibling cert_inhabited is the natural next consumer. Does not itself derive Born weights or decoherence rates; it only certifies the cost geometry the collapse story rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.