name
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.