prob
plain-language theorem explainer
prob supplies the geometric probability (1/2)^n for each natural number n in the St. Petersburg coin-flip game under the 1-indexed convention. Decision theorists and Recognition Science researchers resolving utility paradoxes cite this definition when establishing the linear divergence and log convergence of expected values. The definition is a direct power expression with no lemmas or reductions required.
Claim. For each natural number $n$, the probability of the corresponding outcome in the St. Petersburg ensemble is $p(n) = (1/2)^n$.
background
The module models the St. Petersburg game as a fair coin flipped until the first heads appears on flip $n$, with payout $2^n$ and probability $(1/2)^n$. This replaces earlier placeholder marginal-utility definitions and builds the ensemble explicitly from the geometric distribution to prove the linear-log dichotomy via partial sums over Finset.Ico 1 (N+1). Upstream results include the probability definition from QuantumLedger, which sets probability as the squared norm of amplitudes in a quantum state, supplying the conceptual link from quantum ledger to this classical decision setting.
proof idea
This is a direct definition that assigns the real number (1/2) raised to the power n. No tactics or lemmas are applied; the expression is the complete body of the declaration.
why it matters
This definition underpins the linear_term theorem showing each per-outcome contribution equals 1 and feeds into the StPetersburgCert structure that collects the closed forms for both utilities. It contributes to Track E6 by supplying the explicit probabilities needed to prove unbounded linear partial sums versus bounded log partial sums, consistent with the J-cost resolution. Downstream it appears in the BornRule reference within Modal.Actualization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.