MeasurementBasis
plain-language theorem explainer
MeasurementBasis enumerates the five canonical bases for quantum measurement in the J-cost framework. Physicists modeling wave-function collapse via recognition costs would cite this when counting discrete outcomes or building collapse certificates. The declaration is an inductive type with five constructors that derives Fintype to support immediate cardinality computation.
Claim. The inductive type $MeasurementBasis$ consists of the five constructors position, momentum, spin, energy, and angularMomentum, equipped with decidable equality, representation, boolean equality, and finite-type structure.
background
In the Recognition Science account of quantum measurement the wave function is a recognition-cost distribution. Superposition carries positive J-cost while collapse reaches the equilibrium point where J-cost vanishes. The module sets configDim D = 5 by enumerating five measurement bases and imports the Jcost function from the Cost library to express the cost inequalities that precede collapse.
proof idea
The declaration is an inductive definition introducing five named constructors. The deriving clause automatically installs DecidableEq, Repr, BEq, and Fintype instances, enabling the one-line cardinality theorem that follows.
why it matters
This definition supplies the finite set required by the downstream WaveFunctionCollapseCert structure, whose five_bases field records Fintype.card MeasurementBasis = 5. It realizes the module's claim that five bases correspond to configDim D = 5 and feeds the certification that superpositions have positive J-cost while the definite outcome sits at J-cost zero. The construction closes the enumeration step before the Born-rule probability weights are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.