CommittedLedger
plain-language theorem explainer
A structure modeling a committed ledger in the Recognition Science account of quantum measurement, consisting of one selected outcome from n branches, its complex amplitude, and the unit-norm condition. Researchers formalizing wavefunction collapse as ledger commitment would cite this definition when deriving the measurement postulate. It is introduced directly as a structure declaration with three fields and no proof obligations.
Claim. A committed ledger of dimension $n$ is a structure containing an outcome $i$ in the finite set of size $n$, a complex amplitude $a$, and the normalization condition that the norm of $a$ equals 1.
background
The module derives the measurement postulate from Recognition Science ledger structure. Superposition corresponds to an uncommitted ledger with multiple branches coexisting; measurement forces commitment to one branch, with the others cancelled rather than destroyed. Amplitude is defined as the complex numbers, and the unit-norm field encodes normalization after selection. The local setting imports EightTick phases to handle periodic amplitude factors and relies on upstream ledger concepts from RSNative.Core.Measurement.
proof idea
Structure definition with no proof body; the three fields are declared directly with their types and the single proposition unit_norm.
why it matters
This structure is the codomain of the commit definition that models wavefunction collapse and the domain of the measurement_irreversible theorem. It realizes the RS resolution of the measurement problem by encoding ledger commitment and supplies the target type for deriving Born-rule probabilities from J-cost weights. It sits inside the eight-tick octave framework via the imported phase definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.