Choice as an Act: Russell's Socks, Cardinals as Becomings, and the Productive Continuum, Machine-Checked on the Empty Axiom List

Three classical set-theoretic themes — the axiom of choice onindistinguishable pairs (Russell's socks), the comparison of infinitecardinals, and the uncountability of the continuum — are re-readoperationally: an assertion counts only as an act, performed andwitnessed, never as a completed object postulated into existence. Underthis reading each theme splits cleanly in two, and both halves becomeshort machine-checked theorems. For the socks: no selection rule exists (no swap-symmetric selectorbeyond any finite bookkeeping bound — the Fraenkel–Mostowski statementin miniature, on the empty axiom list), while selection acts form acontinuum (the selectors are exactly the branches, which are notenumerable). The deterministic half is itself a theorem — in ananonymous network of identical automata started identically theconfiguration stays constant across nodes at every round, for arbitrarywiring, so no round distinguishes a unique node (the folklore core ofAngluin 1980, machine-checked, to our knowledge for the first time). For cardinals: a comparison is an act whose witness is data — anexplicit injection from the naturals into the branches is performed; theCantor–Lawvere diagonal is proved uniformly for every floor of thepower-set ladder, on the empty axiom list; the resulting order ispartial by design, since cardinal trichotomy is equivalent to full ACand is cited as a formal-register label rather than claimed. For uncountability: the sign is flipped from prohibition toproductivity — the fugitive from any enumeration is computed by anexplicit term, so the continuum is productive in Post's sense: thecatalogue that reads itself extends itself. And dependent choice is theperformable part of choice (recursion on a history-dependent rule,choice-free); what remains of full AC above DC is the part that can onlybe written, not performed — the same remainder whose surrender dissolvesthe Banach–Tarski decomposition (Solovay's model; cited as metatheory). Nothing here is a new classical theorem; the mathematical content ofeach proof is elementary and classical. The contribution is theoperational re-reading, the split of each theme into an impossible-rulehalf and a performed-act half, the axiom pricing of every step, and themachine check. The axiom of choice is not refuted — a symmetric-selectorimpossibility is a statement about rules, while AC postulates an objectexempt from symmetry. The paper is written to be verified from zero. A single self-containedLean 4 file (`Verify_Choice_standalone.lean`, no mathlib, no imports)reproves all ten empty-axiom-list theorems in under a second — anyagent, human or machine, runs `lean Verify_Choice_standalone.lean` andreads "does not depend on any axioms" ten times. The full corpusverifies with `lake build`, and `#print axioms` lines exhibit the axiomprofile of every object. An empty axiom list is precisely a verdict twoparties who share no axioms and no trust can both confirm: the strongestform of a checkable claim. The reliability of the results does notdepend on trusting the author, the AI that helped write the paper, orthis text — only the Lean 4 kernel. AI disclosure: this work was carried out with the substantialparticipation of the AI system Claude (Anthropic; this preprint —Claude Fable 5) in a dialogue setting; all design decisions, forkchoices, and final responsibility rest with the human author.