pith. machine review for the scientific record. sign in
inductive definition def or abbrev high

MeasurementBasis

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  25inductive MeasurementBasis where
  26  | position | momentum | spin | energy | angularMomentum
  27  deriving DecidableEq, Repr, BEq, Fintype
  28

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.