pith. sign in
module module high

IndisputableMonolith.Physics.WaveFunctionCollapseFromJCost

show as:
view Lean formalization →

The module shows that superpositions carry positive J-cost before measurement and derives wave function collapse in the Recognition Science setting. Quantum foundations researchers would cite the WaveFunctionCollapseCert to connect measurement to the cost functional. The module defines a measurement basis, proves cost positivity and outcome equilibrium, then certifies collapse.

claimDefines MeasurementBasis and certifies that $J($superposition$) > 0$ forces collapse to an equilibrium outcome minimizing recognition cost.

background

The module sits inside Recognition Science, where physics follows from the single J-functional obeying the composition law. It imports the Cost module that supplies the definition of J-cost. The module documentation states the core claim: before measurement, superposition has positive recognition cost. It introduces MeasurementBasis as the discrete set of possible outcomes together with the count function and the equilibrium property.

proof idea

This is a definition-and-theorem module. It first defines MeasurementBasis and measurementBasisCount, then proves superposition_has_cost, establishes measurement_outcome_equilibrium, and packages the results into the WaveFunctionCollapseCert.

why it matters in Recognition Science

The module supplies the WaveFunctionCollapseCert that feeds derivations of quantum measurement from J-cost. It connects directly to the J-uniqueness step in the forcing chain and supplies the cost-based mechanism for collapse. No downstream uses are listed.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)