measurementProbability
plain-language theorem explainer
The definition sets the Born rule probability of outcome i for normalized state ψ to the squared modulus of its i-th amplitude. Researchers deriving quantum measurement from ledger commitment in Recognition Science would cite it. It is a direct one-line assignment from the amplitude field of the state structure.
Claim. For a normalized quantum state ψ with amplitudes ψ_i, the probability of measuring basis outcome i is |ψ_i|^2.
background
QuantumState is the structure with amplitudes : Fin n → Amplitude and the normalization axiom that the sum over i of ‖amplitudes i‖² equals 1. The module derives the measurement postulate from ledger commitment: superposition is an uncommitted ledger entry, measurement forces commitment to one branch, and probabilities follow from relative J-cost of branches. Upstream QuantumState in QuantumLedger is defined as superpositions over ledger configurations with complex amplitudes and normalization |ψ|² = 1; the same structure appears in NoCloning and Unitarity as unit vectors in Hilbert space.
proof idea
Direct definition that equates measurementProbability ψ i to the squared norm of the selected amplitude component.
why it matters
This definition supplies the probability map used by born_rule_nonneg, born_rule_normalized, cost_probability_relation and probability_equals_weight in the same module. It fills the Born rule step in the module's derivation of collapse from ledger balancing, connecting to J-uniqueness (T5) and the Recognition Composition Law via the cost-probability link. It touches the open question of whether ledger commitment yields the full measurement postulate without additional postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.