measurement_outcome_equilibrium
plain-language theorem explainer
The declaration establishes that the recognition cost J reaches zero at the definite outcome value 1, confirming equilibrium after measurement in the cost-based model of wave function collapse. Physicists interpreting quantum measurement as minimization of recognition cost would cite this to anchor the post-collapse state. The proof is a direct one-line application of the upstream Jcost unit lemma.
Claim. After measurement the recognition cost of the definite outcome satisfies $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$.
background
The J-cost function is given by $J(x) = (x-1)^2/(2x)$, which quantifies the recognition cost of a state x relative to the unit equilibrium. The module interprets the wave function as a recognition cost distribution over possible outcomes, with collapse corresponding to selection of the minimum-cost state. This theorem rests on the upstream lemma Jcost_unit0, which proves the same equality by direct simplification of the J-cost definition.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module (and its JcostCore sibling).
why it matters
This result supplies the measurement_equilibrium field inside the WaveFunctionCollapseCert definition, which also records the five measurement bases and the positive cost of superposition. It directly supports the module claim that collapse settles the system at J = 0, consistent with the Recognition Science forcing chain step that identifies J-uniqueness at the fixed point. No open scaffolding remains for this equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.