logUtilityPartial_nonneg
plain-language theorem explainer
The partial sum of terms n/2^n from n=1 to N is non-negative for every natural number N. Decision theorists resolving the St. Petersburg paradox via logarithmic utility cite this to confirm the expected utility starts from a valid non-negative base. The proof reduces the claim to non-negativity of each summand by unfolding the definitions and invoking standard facts about sums and divisions in the reals.
Claim. For every natural number $N$, the partial sum $0 ≤ ∑_{n=1}^N n/2^n$.
background
In the St. Petersburg module the game flips a fair coin until the first heads on flip n, paying 2^n with probability 1/2^n. The per-outcome log-utility term is defined as logTerm n := n / 2^n. The partial sum logUtilityPartial N aggregates these contributions from n=1 to N. This construction contrasts the diverging linear-utility case with the converging log-utility case, presented as a J-cost-shaped resolution.
proof idea
The term-mode proof unfolds logUtilityPartial and logTerm to expose the finite sum of n/2^n terms. It applies Finset.sum_nonneg to reduce the claim to non-negativity of each summand. For each n the proof invokes div_nonneg, supplying Nat.cast_nonneg n for the numerator and le_of_lt (pow_pos (by norm_num) _) for the positive denominator.
why it matters
This result supplies the non-negativity fact required by the master certificate stPetersburgCert, which assembles the full divergence/convergence dichotomy. It completes the log-utility side of the St. Petersburg analysis in the Decision domain and aligns with the Recognition Science use of log utility as a proxy for J-cost within the eight-tick octave framework. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.