payout
plain-language theorem explainer
The payout function assigns 2^n to each natural-number outcome n in the St. Petersburg game. Decision theorists examining the linear-log utility split would cite this as the payoff structure. It is introduced by a direct definition with no lemmas or tactics.
Claim. Define the payout function by $p(n) = 2^n$ for each natural number $n$, where $p(n)$ is the winnings received when the first heads occurs on the $n$th flip of a fair coin.
background
The St. Petersburg module constructs a geometric ensemble: a fair coin is flipped until the first heads appears on flip $n$, with probability $(1/2)^n$ and payout $2^n$. This replaces an earlier placeholder and proves the classical divergence of linear expected value against convergence under logarithmic utility. The payout definition supplies the basic payoff term used in all subsequent partial-sum constructions.
proof idea
Direct definition: payout n is set equal to the real power 2^n. No lemmas are invoked and no tactics are applied beyond the built-in exponentiation.
why it matters
This definition supplies the payoff term for every linear-utility partial sum in the module, which downstream theorems show equals N and therefore diverges. It feeds linearUtilityPartial_eq, linearUtilityPartial_mono, and logUtility_converges, establishing the divergence-convergence dichotomy. In the Recognition framework the construction aligns with J-cost minimization (T5 J-uniqueness) because logarithmic utility is the convex function whose global minimum occurs at unit ratio; the same structure appears in the Recognition Composition Law and the eight-tick octave. It touches the open question of how utility functions are forced by the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.