linear_term
plain-language theorem explainer
The theorem shows that each term in the St. Petersburg linear-utility sum equals exactly 1. Decision theorists and Recognition Science modelers working on the E6 track cite it to establish the divergence of expected value under linear utility. The proof is a direct algebraic reduction that unfolds the local definitions and normalizes the resulting power product.
Claim. For every natural number $n$, the product of the outcome probability $(1/2)^n$ and the payout $2^n$ equals 1.
background
The module treats the St. Petersburg ensemble: a fair coin is flipped until the first heads appears on flip $n$, yielding payout $2^n$ with probability $(1/2)^n$. The sibling definitions payout n := 2^n and prob n := (1/2)^n supply the concrete functions whose product is shown to be identically 1. This identity is the per-term building block for the partial-sum analysis that contrasts linear divergence with log-utility convergence via J-cost.
proof idea
The term-mode proof unfolds prob and payout, rewrites the product using the inverse of the power-multiplication rule via rw [← mul_pow], and finishes with norm_num to reduce (1/2 * 2)^n to 1.
why it matters
linear_term supplies the per-outcome identity required by linearUtilityPartial_eq, which closes the partial sum to exactly N and thereby populates the master certificate stPetersburgCert. It completes the linear side of the divergence/convergence dichotomy in the Decision.StPetersburg module, setting up the contrast with log utility that aligns with the J-uniqueness fixed point from upstream PhiForcingDerived.of and the broader Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.