Pith. sign in
module module moderate

IndisputableMonolith.Physics.WaveFunctionCollapseFromJCost

show as:
view Lean formalization →

Links quantum measurement to the recognition cost J: a superposition carries strictly positive J-cost, while a definite measurement outcome sits at J-equilibrium (cost zero). Physicists deriving collapse from the RS cost functional would cite this module. The argument is definitional plus elementary inequalities on J, not a deep analytic construction.

claimBefore measurement, a superposition state has strictly positive recognition cost $J>0$. A measurement basis has finite cardinality; each definite outcome is a $J$-equilibrium ($J=0$). The module packages this as a wave-function-collapse certificate: collapse is the passage from positive-cost superposition to zero-cost eigenstate under the RS cost $J(x)=(x+x^{-1})/2-1$.

background

Recognition Science treats the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) as the sole source of physical selection. The forcing chain fixes $J$ at T5; the Recognition Composition Law then governs products and ratios. In that language a pure eigenstate is an equilibrium of $J$ (cost zero), while any nontrivial superposition is a nonequilibrium configuration.

This module sits in the Physics layer and imports only the Cost core. It introduces a finite measurement basis, a count of basis elements, and the elementary claims that superposition carries positive cost and that a recorded outcome is at equilibrium. The local setting is therefore kinematic: cost comparison before and after selection, not a dynamical Schrödinger evolution.

proof idea

Definition-heavy module with short supporting lemmas. Measurement bases and their cardinalities are introduced as data. The key inequality superposition_has_cost follows from strict convexity (or the unique minimum) of $J$ at the identity: any nontrivial mixture lies off the minimum. measurement_outcome_equilibrium records that a definite basis vector saturates $J=0$. WaveFunctionCollapseCert and its witness bundle these facts into a single certificate object. No heavy analysis; the structure is definitions plus direct appeals to Cost properties of $J$.

why it matters in Recognition Science

Gives the RS reading of wave-function collapse: measurement is cost minimization under $J$, not an extra postulate. It ties the Born-rule setting to the same $J$ fixed by T5 and used for masses, $\alpha$, and the eight-tick structure elsewhere in the monolith. Downstream consumers (none linked yet in the graph) would be Born-rule or decoherence developments that need a certified positive-cost-to-equilibrium step. The module therefore closes a conceptual gap between the abstract cost functional and laboratory measurement language, while remaining elementary enough to stay fully proved.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)