def definition def or abbrev

`jCost`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  79def jCost (c : TrolleyChoice) : ℝ := (livesLost c : ℝ)

Definition body.

  80
  81/-- Pulling lowers J: `jCost(pull) < jCost(doNothing)`. -/

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

no_strictly_dominant_choice in IndisputableMonolith.Decision.Trolley decl_use
pull_lowers_J in IndisputableMonolith.Decision.Trolley decl_use
tradeoff_strict in IndisputableMonolith.Decision.Trolley decl_use
TrolleyTradeoffCert in IndisputableMonolith.Decision.Trolley decl_use
jCost_before_arithmetic in IndisputableMonolith.Foundation.PreTemporalForcingOrder decl_use
rank in IndisputableMonolith.Foundation.PreTemporalForcingOrder decl_use
rcl_before_jCost in IndisputableMonolith.Foundation.PreTemporalForcingOrder decl_use
Stage in IndisputableMonolith.Foundation.PreTemporalForcingOrder decl_use
RSPrimitive in IndisputableMonolith.Foundation.RSCoupledAxis decl_use
earthAxis in IndisputableMonolith.Physics.PlanetStrataC2 decl_use

Lean names referenced from this declaration's body.