name
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not define the cost functions themselves.
- Does not prove any properties of the tradeoff.
- Does not interact with physical constants or phi-ladder.
- Limited to string display for the two choices.
formal statement (Lean)
60def name : TrolleyChoice → String
61 | pull => "pull lever"
62 | doNothing => "do nothing"
63
64end TrolleyChoice
65
66/-- Lives lost as a function of choice. -/