expectedValue
plain-language theorem explainer
expectedValue defines the classical expected payoff for one-box or two-box choices in Newcomb's paradox as a linear function of predictor accuracy p. Decision theorists in the Recognition Science setting cite it when embedding sigma-conservation constraints into payoff calculations. The definition is a direct case split on the NewcombChoice inductive type that produces explicit arithmetic expressions without invoking external lemmas.
Claim. Let $c$ be a Newcomb choice (oneBox or twoBox) and let $p$ be a real number. The expected value is $p$ times 1,000,000 if $c$ is oneBox and $p$ times 1,000 plus $(1-p)$ times 1,001,000 if $c$ is twoBox.
background
The module frames Newcomb's paradox inside Recognition Science as a sigma-conservation theorem. A perfect predictor is treated as a Z-matched copy of the agent, so two-boxing creates a sigma imbalance while one-boxing preserves it. NewcombChoice is the inductive type whose constructors are oneBox and twoBox. The module doc states that the paradox dissolves because two-boxing requires creating a sigma-imbalance equal to the prediction error. Upstream constants such as one from IntegersFromLogic and RationalsFromLogic supply the numeric literals appearing in the payoff expressions.
proof idea
The definition proceeds by pattern matching on the NewcombChoice constructor. The oneBox branch returns the expression p * 1000000 + (1 - p) * 0. The twoBox branch returns p * 1000 + (1 - p) * 1001000. No lemmas or tactics are applied; the body is a pure computational definition.
why it matters
This definition supplies the payoff map required by the dominance theorem oneBox_dominates_at_perfect_prediction and by the master certificate NewcombResolutionCert. It supplies the classical component of the sigma-conservation argument that selects one-boxing as the structural optimum. The module places the construction in §XXIII.C on philosophical paradoxes, where sigma conservation replaces the causal-evidential split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.