name
plain-language theorem explainer
The definition supplies display names for the two options in the trolley problem modeled as a J-cost versus sigma-cost tradeoff. Decision theorists applying Recognition Science to ethical paradoxes would cite this when formalizing choice labels. It is realized as a direct pattern-matching definition on the inductive trolley choice type.
Claim. The function maps the pull-lever choice to the string ``pull lever'' and the do-nothing choice to the string ``do nothing''.
background
The module frames the trolley problem as a J/σ tradeoff in Recognition Science: pulling the lever reduces lives lost (J-cost) from 5 to 1 but introduces an agency imbalance (σ-cost), while doing nothing preserves σ-equilibrium at higher J-cost. TrolleyChoice is the inductive type with constructors pull and doNothing. The name function provides human-readable labels for these constructors. Upstream structures calibrate the underlying J-cost via PhiForcingDerived and ledger factorization via DAlembert, which supply the cost manifolds used in the tradeoff proofs.
proof idea
The definition is a direct case analysis on the inductive type TrolleyChoice, assigning the corresponding string literal to each constructor.
why it matters
This definition supports the presentation of the trolley tradeoff certificate by providing readable names for the choices. It completes the interface for the TrolleyTradeoffCert in the decision module, which demonstrates that neither choice dominates on both J and sigma axes. It touches the philosophical paradoxes row in the Recognition Science framework, linking to the J-uniqueness and forcing chain landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.