trolleyTradeoffCert
plain-language theorem explainer
The definition inhabits the TrolleyTradeoffCert structure by supplying concrete values for its five fields. Researchers formalizing ethical decision problems in Recognition Science would reference it to certify the J/σ tradeoff in the trolley scenario. The construction proceeds by reflexivity on the numerical life counts and direct invocation of the strict tradeoff and non-dominance lemmas.
Claim. The structure TrolleyTradeoffCert holds with livesLost(pull) = 1, livesLost(doNothing) = 5, jCost(pull) < jCost(doNothing) ∧ sigmaCost(pull) > sigmaCost(doNothing), ∀ c1 c2 : TrolleyChoice, c1 ≠ c2 → ¬(jCost c1 < jCost c2 ∧ sigmaCost c1 < sigmaCost c2), and pull creates an agency imbalance.
background
In the Recognition Science treatment of the trolley problem, choices are evaluated along J-cost (lives lost as proxy for the J-functional) and sigma-cost (agency imbalance from active intervention). The module defines TrolleyChoice as the inductive type with pull and doNothing, livesLost mapping pull to 1 and doNothing to 5, jCost as lives lost, and sigmaCost as 1 for pull and 0 for doNothing. This formalizes the tension where pulling reduces J but violates sigma-conservation, per the module's setup of the J/σ tradeoff.
proof idea
Direct construction of the TrolleyTradeoffCert structure: reflexivity supplies the lives-lost equalities, tradeoff_strict supplies the joint J-decrease and sigma-increase, no_strictly_dominant_choice supplies the non-dominance property, and reflexivity closes the agency-imbalance field.
why it matters
This definition supplies the inhabited master certificate for the trolley J/σ tradeoff, completing the formalization of the philosophical paradoxes row in the Recognition Science framework. It shows neither choice dominates on both axes, consistent with the requirement that virtue-aligned actions must satisfy both J-reduction and sigma-preservation. No downstream uses appear yet, leaving open integration into larger ethical procedures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.