waveFunctionCollapseCert
plain-language theorem explainer
waveFunctionCollapseCert constructs the certificate that quantum measurement arises as minimization of the J-cost function. Researchers working on recognition-based interpretations of quantum mechanics would reference it when connecting superposition costs to collapse dynamics. The definition is a direct record construction that instantiates the three fields of the WaveFunctionCollapseCert structure using previously established results on basis cardinality, positive cost away from unity, and zero cost at the unit value.
Claim. The wave function collapse certificate asserts that the measurement basis set has cardinality five, that the recognition cost satisfies $J(r) > 0$ for all real $r > 0$ with $r ≠ 1$, and that $J(1) = 0$.
background
In the Recognition Science framework the wave function is a recognition cost distribution. Collapse corresponds to the system settling to the J-cost minimum. The module states that before measurement J(r) > 0 for r ≠ 1 while after measurement J(1) = 0, with the Born rule recovered as probability weights by J-cost. Five measurement basis types (position, momentum, spin, energy, angular momentum) equal configDim D = 5.
proof idea
The definition is a one-line record constructor. It assigns the five_bases field to measurementBasisCount, which proves the cardinality equals five by decision. The superposition_cost field receives superposition_has_cost, which reduces the positivity claim to the upstream lemma Jcost_pos_of_ne_one. The measurement_equilibrium field is filled by measurement_outcome_equilibrium, which directly invokes Jcost_unit0.
why it matters
This definition supplies the top-level certificate for deriving wave function collapse from J-cost minimization. It assembles the basis count D = 5, the cost of superpositions, and the equilibrium condition J(1) = 0. The construction supports the claim that collapse selects the minimum-cost outcome, consistent with the eight-tick octave and phi-ladder structures elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.