name
Supplies string labels for the one-box and two-box strategies in Newcomb's paradox. Researchers formalizing decision theory inside Recognition Science use these labels when stating sigma-conservation results. The definition is realized by direct pattern matching on the inductive constructors of the choice type.
claimLet $C$ be the inductive type whose constructors are the one-box choice and the two-box choice. The function $name: C → String$ is defined by $name(oneBox) = $``one-box'' and $name(twoBox) = $``two-box''.
background
NewcombChoice is the inductive type with constructors oneBox and twoBox, representing the strategies of taking only the opaque box or taking both boxes. The module situates Newcomb's paradox inside Recognition Science by treating a perfect predictor as a Z-matched copy and resolving the paradox via sigma-conservation between prediction and action. Upstream results supply the basic inductive and numeric foundations used to build the choice type and its later companions such as expectedValue and sigmaCost.
proof idea
Direct pattern match on the two constructors of NewcombChoice, returning the corresponding string literal in each case.
why it matters in Recognition Science
Provides the human-readable identifiers required by the module's theorems on expected value, sigma cost, and dominance of one-boxing under conservation. It supports the structural resolution of Newcomb's paradox as a sigma-conservation theorem. The definition sits inside the NewcombResolutionCert construction but carries no independent theorem content.
scope and limits
- Does not assign numerical values or probabilities to either choice.
- Does not encode predictor accuracy or matching conditions.
- Does not participate in sigma-cost or dominance calculations.
- Does not appear inside the master certificate NewcombResolutionCert.
formal statement (Lean)
54def name : NewcombChoice → String
55 | oneBox => "one-box"
56 | twoBox => "two-box"
57
58end NewcombChoice
59
60/-- Standard expected value: assumes the predictor is correct
61 with probability `p` and `1 − p` otherwise. At `p = 1`
62 (perfect predictor), one-box wins by `999,000`. -/