logUtilityPartial_succ
plain-language theorem explainer
The recursive relation for partial sums of the St Petersburg log-utility series states that the sum to N+1 equals the sum to N plus the next term (N+1)/2^{N+1}. Decision theorists resolving the paradox with logarithmic utility cite this step when building the closed form. The proof is a one-line wrapper that unfolds the sum definition and applies the Ico tail-recursion lemma.
Claim. For every natural number $N$, let $S_N = sum_{n=1}^N n/2^n$. Then $S_{N+1} = S_N + (N+1)/2^{N+1}$.
background
The St Petersburg module constructs the classic paradox ensemble: outcomes indexed by flip number n with probability 1/2^n and payout 2^n. Linear utility produces partial sums equal to N (unbounded). Log utility replaces the payout with its logarithm, yielding the unitless per-term contribution logTerm n := n/2^n and the partial sum logUtilityPartial N := sum_{n in Ico 1 (N+1)} logTerm n. The module proves the divergence/convergence dichotomy directly from these partial sums.
proof idea
Unfold logUtilityPartial and logTerm to expose the finite sum. Rewrite the Ico upper bound with rfl, then apply Finset.sum_Ico_succ_top. The required inequality Nat.succ_le_succ (Nat.zero_le N) is supplied by the upstream arithmetic lemmas succ_le_succ and zero_le.
why it matters
This supplies the inductive step used by the downstream theorem logUtilityPartial_closed_form, which delivers the explicit bound 2 - (N+2)/2^N. That bound shows the partial sums remain finite, so the expected log utility converges and resolves the paradox. Within Recognition Science this step belongs to the decision track that employs the J-cost (logarithmic) utility arising from T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.