logUtilityPartial_closed_form
plain-language theorem explainer
The partial sum of n over 2 to the n from 1 to N equals 2 minus (N plus 2) over 2 to the N. Decision theorists resolving the St. Petersburg paradox via logarithmic utility cite this to establish boundedness of expected value. The proof proceeds by induction on N, invoking the successor recursion for the partial sum and reducing the resulting identity with field simplification and ring arithmetic.
Claim. For every natural number $N$, the partial sum $∑_{n=1}^N n/2^n = 2 - (N+2)/2^N$.
background
The St. Petersburg module defines an ensemble with fair coin flips until first heads on flip n, payout 2^n, and probability (1/2)^n. The log-utility partial sum aggregates terms n/2^n from n=1 to N. This setup shows linear utility partial sums equal N and diverge, while logarithmic utility remains bounded.
proof idea
Induction on N. Base case N=0 applies the zero theorem directly. Successor case rewrites via the successor recursion, substitutes the inductive hypothesis, then uses push_cast, field_simp, and ring after establishing positivity of powers of 2.
why it matters
Supplies the closed form required by the St. Petersburg certificate and the one-statement theorem, which asserts linear divergence alongside logarithmic convergence to 2. This underpins the boundedness and limit statements. In Recognition Science the logarithmic resolution aligns with J-cost structures that enforce convergence, consistent with the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.