logTerm
plain-language theorem explainer
logTerm defines the real number n divided by 2 to the power n for each natural number n. This term appears in the partial sums that establish convergence of logarithmic utility for the St. Petersburg game. Decision theorists and recognition scientists working on utility paradoxes would cite it when constructing the series for expected log payout. The definition is a direct abbreviation in real arithmetic.
Claim. For each natural number $n$, the per-outcome contribution to the log-utility expected payout is given by $n / 2^n$.
background
The St. Petersburg module models a game where a fair coin is flipped until the first heads appears on flip $n$, yielding payout $2^n$ with probability $1/2^n$. Linear utility produces an expected value that grows without bound as the number of terms, while log utility produces partial sums built from terms of the form $n/2^n$. This construction replaces earlier placeholder utilities and proves the divergence-convergence dichotomy directly from the partial sums.
proof idea
This is a one-line definition that casts the natural number $n$ to a real and divides it by the real power $2^n$.
why it matters
This definition supplies the summand for logUtilityPartial, which supports the downstream proofs of monotonicity, non-negativity, and the successor recursion. It enables the demonstration that log utility converges in the St. Petersburg setting, aligning with the J-cost resolution of infinities in the Recognition Science framework. The result sits in track E6 of the decision module and does not invoke the phi-ladder or the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.