probability
This definition supplies the Born-rule probability for a ledger configuration inside a normalized quantum superposition. Researchers deriving measurement statistics from Recognition Science ledgers cite it when extracting outcome probabilities from ledger costs. It is realized as a direct one-line extraction of the squared complex norm of the selected amplitude.
claimLet $n$ be a natural number and let $ψ$ be a quantum state over $n$ ledger configurations with complex amplitudes $ψ_i$. The probability of configuration $i$ is $|ψ_i|^2$.
background
QuantumState structures a superposition over ledger configurations, each assigned a complex amplitude, subject to the normalization condition that the sum of squared norms equals one. The QuantumLedger module treats quantum states as ledger superpositions and derives the Born rule from J-cost minimization rather than postulating it. Upstream results in NoCloning and Unitary modules supply analogous structures of unit vectors in Hilbert space whose squared amplitudes likewise yield probabilities.
proof idea
This is a one-line definition that applies Complex.normSq directly to the amplitude component of the quantum state at the given index.
why it matters in Recognition Science
It supplies the operational definition of probability that feeds into audit summaries, coincidence bounds, and resolution-time structures downstream. The definition realizes the Born-rule step listed in the module plan, connecting ledger J-costs to quantum measurement outcomes inside the forcing chain. It closes one link between the ledger formalism and the emergence of quantum statistics without additional postulates.
scope and limits
- Does not prove that the extracted probabilities sum to one over all configurations.
- Does not derive the value from explicit J-cost minimization on ledger entries.
- Does not address continuous spectra or infinite-dimensional Hilbert spaces.
- Does not implement wavefunction collapse or measurement dynamics.
formal statement (Lean)
154noncomputable def probability {n : ℕ} (ψ : QuantumState n) (i : Fin n) : ℝ :=
proof body
Definition body.
155 Complex.normSq (ψ.amplitudes i)
156
157/-- Probabilities are non-negative. -/
used by (40)
-
ResolutionTime -
printConsistency -
printProbability -
printSummary -
AuditSummary -
CoincidenceBound -
coincidence_negligible -
cpmCoincidenceBound -
eight_tick_cmin_numerical -
generateAuditSummary -
p_stay -
p_stay_real -
switch_eq_two_stay -
switch_strictly_better_real -
switchWinningSet_card -
total_probability -
name -
payout -
prob -
stPetersburgCert -
anita_inconclusive -
systematic_dominant -
born_rule_jcost_connection -
expectedCost -
prob_nonneg -
prob_sum_one -
QuantumState -
born_weight_is_sin_sq -
C_equals_2A -
ErrorModel