WaveFunctionCollapseCert
plain-language theorem explainer
The collapse certificate packages three J-cost properties for quantum measurement: the measurement basis set has five elements, the cost is positive for any superposition parameter r not equal to one, and the cost vanishes at equilibrium. A physicist working on Recognition Science models of wave function collapse would cite this to certify the minimum-cost selection of outcomes. The definition is a direct record structure with no computational content or lemmas.
Claim. A structure certifying that wave function collapse arises from J-cost minimization is given by the conjunction of: the cardinality of the measurement basis set equals five, the J-cost of any positive real number $r$ not equal to one is positive, and the J-cost at one equals zero.
background
In the module on wave function collapse from J-cost, quantum measurement is modeled as selecting the outcome that minimizes the recognition cost J. The J-cost function satisfies J(r) > 0 for r ≠ 1 (superposition carries cost) and J(1) = 0 (definite state is equilibrium). The measurement basis is formalized as an inductive type with five constructors corresponding to position, momentum, spin, energy, and angular momentum. This local setting imports the cost definitions and uses the finite type cardinality to fix the number of bases at five, matching configDim D = 5. The upstream result is the inductive definition of the measurement basis set.
proof idea
This declaration is a structure definition that directly records three properties. No lemmas are applied and no tactics are used; it serves as a packaging of the conditions stated in the module documentation.
why it matters
This structure is instantiated by the downstream definition that constructs the collapse certificate using sibling lemmas for each field. It fills the formal content for the wave function collapse model in Recognition Science, where collapse corresponds to settling at the J-cost minimum. The five bases align with the framework's recognition composition law and the five-dimensional measurement space. It touches the open question of deriving the Born rule weights from the cost distribution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.