linearUtility_diverges
plain-language theorem explainer
Linear utility in the St. Petersburg ensemble diverges: for every real M there exists N such that the partial sum exceeds M. Decision theorists resolving the paradox cite this to separate the classical infinite expectation from the log-shaped resolution. The term proof obtains N via exists_nat_gt and reduces the inequality through the closed-form identity that the partial sum equals N.
Claim. For every real number $M$, there exists a natural number $N$ such that $M < S_N$, where $S_N = sum_{n=1}^N (1/2)^n · 2^n$ denotes the partial expected payout under linear utility.
background
The module constructs the St. Petersburg ensemble: a geometric distribution with P(n) = (1/2)^n and payout 2^n for n = 1,2,…. linearUtilityPartial N is the truncated sum of prob n · payout n from n=1 to N. The upstream theorem linearUtilityPartial_eq states that this sum equals N exactly, because each term simplifies to 1 and the sum counts the index set cardinality.
proof idea
The term proof introduces M, obtains N > M from exists_nat_gt, then rewrites the target inequality by linearUtilityPartial_eq to reduce it to M < N, which holds by the choice of N.
why it matters
This result supplies the linear_unbounded conjunct for stPetersburgCert and the first clause of stPetersburg_dichotomy. It completes the divergence half of the linear-versus-log dichotomy that the module uses to contrast classical utility with the J-cost (log) resolution in the Recognition Science decision track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.