NewcombChoice
plain-language theorem explainer
The inductive type for Newcomb choices encodes the two admissible actions as one-boxing or two-boxing. Decision theorists working inside Recognition Science cite it when formalizing the predictor-chooser coupling as a sigma-conservation constraint. The declaration is a direct inductive definition that derives decidable equality and inhabited instances with no additional proof obligations.
Claim. Let $C$ be the set of choices consisting of one-boxing (selecting only the opaque box) and two-boxing (selecting both boxes).
background
The module treats Newcomb's paradox as a sigma-conservation theorem. A perfect predictor is a Z-matched copy of the chooser, so any mismatch between prediction and action creates a measurable sigma imbalance. NewcombChoice supplies the domain on which expected-value and sigma-cost functions are defined, allowing the classical causal-evidential split to be replaced by a structural constraint under R-hat action.
proof idea
The declaration is an inductive definition with two constructors, oneBox and twoBox, that automatically derives DecidableEq and Inhabited. No lemmas are applied and no tactics are invoked.
why it matters
This definition anchors the downstream results expectedValue, sigmaCost, oneBox_preserves_sigma, oneBox_dominates_under_sigma_conservation, and the master certificate NewcombResolutionCert. It supplies the choice domain required for the module's resolution of the paradox as a sigma-conservation theorem in the philosophical-paradoxes row. The construction directly supports the framework claim that one-boxing is the unique admissible action once predictor-chooser coupling is enforced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.