module module high

`IndisputableMonolith.Decision.StPetersburg`

This module sets up the St. Petersburg paradox in Recognition Science decision theory by defining payout 2^n on the nth heads outcome together with probabilities and partial utility sums. It would be cited by researchers examining infinite-expectation paradoxes under RS cost functions. The module contains only definitions and elementary properties of linear and logarithmic partial utilities with no theorem proofs.

claimPayout on outcome $n$ is $p(n)=2^n$ for $ngeq0$. Probability is $q(n)=2^{-n}$. Linear partial utility up to $N$ is the sum of $p(k)q(k)$ terms; logarithmic partial utility is the corresponding sum of $log(p(k))q(k)$ terms. The $n=0$ term contributes zero to both sums.

background

The module imports Constants, whose fundamental object is the RS time quantum $tau_0=1$ tick, and the Cost module that supplies the J-cost function obeying the Recognition Composition Law. It introduces the classic St. Petersburg game: a fair coin is flipped until the first heads appears on flip $n$, at which point the payout is $2^n$. Sibling definitions include prob_zero, prob_pos, linearUtilityPartial, logUtilityPartial, and the auxiliary linear_term and logTerm objects that isolate the divergent and convergent behaviors.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete decision-theoretic example needed to test how RS-native utilities (linear versus logarithmic) behave on an infinite-expectation problem. It feeds parent results in the broader Decision domain that connect payout and probability structures to the J-uniqueness and phi fixed-point steps of the forcing chain, although the current dependency graph lists no direct used_by edges.

scope and limits

Does not prove convergence or divergence of any utility sum.
Does not invoke the Recognition Composition Law or J-cost explicitly.
Does not reference the phi-ladder, mass formula, or eight-tick octave.
Does not connect payouts to spatial dimension D=3 or the alpha band.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (24)

def payout L108
def prob L111
theorem prob_zero L116
theorem prob_pos L120
theorem linear_term L127
def linearUtilityPartial L134
theorem linearUtilityPartial_eq L138
theorem linearUtility_diverges L150
theorem linearUtilityPartial_mono L157
def logTerm L178
def logUtilityPartial L181
theorem logUtilityPartial_zero L185
theorem logUtilityPartial_succ L191
theorem logUtilityPartial_closed_form L201
theorem logUtilityPartial_lt_two L218
theorem logUtilityPartial_nonneg L229
theorem logUtilityPartial_mono L239
theorem aux_limit_N_plus_two_div_pow L257
theorem logUtility_limit_eq_two L297
theorem logUtility_converges L314
theorem stPetersburg_dichotomy L324
structure StPetersburgCert L352
def stPetersburgCert L364
theorem st_petersburg_one_statement L387