logUtilityPartial_lt_two
plain-language theorem explainer
The boundedness result for the log-utility partial sum states that the finite sum remains strictly below 2 for every natural number N. Decision theorists resolving the St. Petersburg paradox via logarithmic utility cite this bound to establish convergence of the expectation. The proof rewrites the sum to its closed form and confirms the subtracted remainder is positive via real-number positivity and linear arithmetic.
Claim. For every natural number $N$, the partial sum satisfies $2 - ((N : ℝ) + 2) / 2^N < 2$, or equivalently $∑_{n=1}^N n / 2^n < 2$.
background
In the St. Petersburg module the ensemble consists of outcomes indexed by n with probability (1/2)^n and payout 2^n. logUtilityPartial is the unitless partial sum from n=1 to N of the log-utility terms, defined as the sum of logTerm n over the initial segment of natural numbers. The upstream theorem logUtilityPartial_closed_form supplies the explicit identity logUtilityPartial N = 2 - ((N : ℝ) + 2) / (2 : ℝ)^N, quoted as 'The unitless partial sum equals 2 - (N + 2) / 2^N for every N : ℕ.' This local setting contrasts the divergent linear partial sums with the convergent log-shaped sums, placing the result inside the decision-theory track of Recognition Science.
proof idea
The tactic proof first rewrites the target via logUtilityPartial_closed_form. It then builds positivity of the power 2^N using pow_pos, positivity of the numerator N+2 using Nat.cast_nonneg and linarith, and positivity of the quotient using div_pos. The final linarith step closes the strict inequality.
why it matters
The declaration supplies the strict upper bound required by stPetersburg_dichotomy and st_petersburg_one_statement; both are assembled into the master certificate stPetersburgCert. It demonstrates that the log utility (J-cost analogue) yields a finite expectation, supporting the Recognition Science resolution of the paradox via the Recognition Composition Law and the phi-ladder structures. No open scaffolding questions are directly touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.