logUtility_converges
plain-language theorem explainer
The theorem shows that the partial sums for log utility in the St. Petersburg game converge to a finite limit. Decision theorists using Recognition Science would reference it when contrasting bounded J-cost expectations against the classical divergence. The proof proceeds by a direct term application of the already-proved limit equality to 2.
Claim. There exists a real number $L$ such that the partial sums of the logarithmic utility contributions over the St. Petersburg outcomes converge to $L$ as the truncation index tends to infinity.
background
The module treats the St. Petersburg ensemble: a fair coin flipped until the first heads on flip $n$ yields payout $2^n$ with probability $(1/2)^n$. Linear utility produces the divergent sum $N$ for the first $N$ terms, while log utility is shown to converge. Key definitions include payout returning $2^n$ and logUtilityPartial as the sum of logTerm contributions from $n=1$ to $N$, which encode the expected log payout. This setting replaces an earlier unrelated marginal-utility placeholder and works directly from the geometric distribution partial sums.
proof idea
The proof is a one-line term-mode wrapper that supplies the candidate limit 2 together with the theorem logUtility_limit_eq_two, which rewrites the partial sum explicitly as $2 - (N+2)/2^N$ and notes that the subtracted term vanishes at infinity.
why it matters
This declaration completes the convergence half of the dichotomy stated in the module documentation, confirming that log-shaped (J-cost-shaped) utility remains finite. It draws on the cost definitions from ObserverForcing and MultiplicativeRecognizerL4, where cost is the J-cost of a recognition event, and aligns with the J-uniqueness step in the forcing chain. No downstream uses are recorded yet, but the result underpins bounded expected-utility calculations in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.