linearUtilityPartial
The linearUtilityPartial definition computes the finite partial sum of expected payout under linear utility for the St. Petersburg game truncated at N outcomes. Decision theorists and economists working on the paradox cite it to establish the classical divergence before introducing logarithmic resolution. It is realized as a direct summation of the per-outcome products over the initial segment of natural numbers.
claimLet $U(N) := ∑_{n=1}^N p(n) · x(n)$ where $p(n) = 2^{-n}$ is the probability of first heads on flip $n$ and $x(n) = 2^n$ is the corresponding payout.
background
The St. Petersburg module constructs the ensemble with payout(n) defined as 2^n and prob(n) defined as (1/2)^n for n ≥ 1. linearUtilityPartial aggregates these into the partial expected value under linear utility by summing the products over Finset.Ico 1 (N+1). The module documentation replaces prior marginal-utility placeholders and directly encodes the geometric distribution and exponential payoffs of the classical paradox.
proof idea
The definition is a one-line wrapper that applies the Finset sum over the half-open interval from 1 to N+1 of the product prob n * payout n.
why it matters in Recognition Science
This supplies the partial sum that linearUtilityPartial_eq proves equals N exactly, which feeds linearUtility_diverges, the master certificate StPetersburgCert, and the dichotomy theorem stPetersburg_dichotomy. It anchors the linear half of the divergence-versus-convergence contrast, where the log utility (J-cost-shaped) remains bounded by 2 while linear utility is unbounded, consistent with the Recognition framework's use of log-shaped costs to resolve the paradox.
scope and limits
- Does not prove the infinite-sum divergence (handled separately by linearUtility_diverges).
- Does not compute or bound any logarithmic-utility partial sums.
- Does not invoke Recognition Science constants such as phi or the eight-tick octave.
- Does not address risk aversion, other utility shapes, or empirical calibration.
Lean usage
example (N : ℕ) : linearUtilityPartial N = N := by rw [linearUtilityPartial_eq]formal statement (Lean)
134def linearUtilityPartial (N : ℕ) : ℝ :=
proof body
Definition body.
135 ∑ n ∈ Finset.Ico 1 (N + 1), prob n * payout n
136
137/-- **CLOSED FORM (linear utility).** The partial sum is exactly `N`. -/