RSWFCollapseCert
plain-language theorem explainer
A certificate packing the three analytic conditions that underwrite Recognition-Science wave-function collapse: the domain cost vanishes on the diagonal, is nonnegative off it for positive arguments, and the canonical collapse threshold is strictly positive. Anyone citing the structural collapse theorem (measurement as ledger posting / J-cost minimization to the nearest rung) depends on this bundle. It is a pure structure definition; inhabitance is discharged separately by the concrete certificate.
Claim. A collapse certificate is a triple of properties: (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 collapse threshold is strictly positive.
background
The module treats wave-function collapse as a recognition event: measurement equals ledger posting. Collapse is J-cost minimization onto the nearest rung of the phi-ladder; the eight-tick octave fixes the minimal recognition time. No hidden-variable layer is introduced.
Domain cost is the RS cost assigned to a measured-versus-expected pair of positive reals. The diagonal identity (cost zero when the two arguments agree) and nonnegativity are the analytic content of a genuine cost. The canonical threshold is the positive cutoff that decides when a recognition event posts a collapse.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via the standard J-cost nonnegativity lemma. The present structure lifts that idea to the domain-cost interface used by the collapse story.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Concrete discharge is deferred to the sibling definitions that build an inhabitant and prove Nonempty.
why it matters
This certificate is the interface that the module's structural collapse claim rests on. Downstream, the concrete certificate wires in the three sibling lemmas (diagonal identity, domain-cost nonnegativity, threshold positivity), and the inhabitance theorem records that the type is nonempty. Together they close the structural half of "measurement = ledger posting / J-cost minimization to the nearest rung" with zero sorry and zero axiom.
In the broader forcing chain the story sits next to T5 (J-uniqueness) and T7 (eight-tick octave): collapse time is gated by the octave, and the cost being minimized is the unique J. The certificate does not itself derive the mass ladder or the alpha band; it only packages the cost-and-threshold hypotheses the collapse narrative needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.