pith. machine review for the scientific record. sign in
theorem proved term proof high

pull_lowers_J

show as:
view Lean formalization →

The declaration establishes that the J-cost of pulling the lever is strictly smaller than the J-cost of inaction, with J-cost defined directly as the number of lives lost. Decision theorists working in the Recognition Science framework would cite it to quantify the utilitarian side of the trolley dilemma. The proof is a term-mode reduction that unfolds the cost definitions and normalizes the resulting numerical inequality.

claimLet $jCost(c)$ be the J-cost of choice $c$, defined as the real number of lives lost under $c$. Then $jCost(pull) < jCost(doNothing)$, which evaluates to $1 < 5$.

background

The Trolley module recasts the classic dilemma as a J/σ tradeoff. The inductive type TrolleyChoice has constructors pull and doNothing. livesLost maps pull to 1 and doNothing to 5; jCost is the real-valued lift of livesLost. sigmaCost assigns 1 to pull (agency imbalance) and 0 to doNothing, following the template from NewcombParadox.sigmaCost where one-boxing carries zero σ-cost.

proof idea

The proof is a one-line wrapper that unfolds jCost and livesLost, then applies norm_num to compare the constants 1 and 5.

why it matters in Recognition Science

This supplies the J-decrease half of tradeoff_strict, which pairs it with the σ-increase to feed no_strictly_dominant_choice. The module documentation positions the result as realizing the strict J/σ tension in the trolley problem, where pulling lowers J but creates an agency imbalance. It illustrates cost computation on the lives manifold inside the Recognition Science decision layer.

scope and limits

Lean usage

theorem example : jCost TrolleyChoice.pull < jCost TrolleyChoice.doNothing := pull_lowers_J

formal statement (Lean)

  82theorem pull_lowers_J : jCost TrolleyChoice.pull < jCost TrolleyChoice.doNothing := by

proof body

Term-mode proof.

  83  unfold jCost livesLost
  84  norm_num
  85
  86/-- Pulling raises σ: `sigmaCost(pull) > sigmaCost(doNothing)`. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.