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

ethics_is_objective

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 201theorem ethics_is_objective (a b : EthicalAction) :
 202    -- The moral comparison is deterministic (objective)
 203    (MorallyBetter a b ∨ MorallyBetter b a) := by

proof body

Term-mode proof.

 204  unfold MorallyBetter moral_cost
 205  rcases le_or_lt (defect a.after) (defect b.after) with h | h
 206  · exact Or.inl h
 207  · exact Or.inr (le_of_lt h)
 208
 209/-- **Theorem (Cost Ordering Gives Ethics)**:
 210    Any cost model over actions directly gives an ethical ordering.
 211    Lower cost = morally preferable. -/

used by (1)

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

depends on (13)

Lean names referenced from this declaration's body.