ethicalZero
plain-language theorem explainer
ethicalZero supplies the base action state with agent and improvement-rank coordinates both set to zero. Researchers formalizing admissible ethical realizations cite it as the identity element under preference composition. The definition is a direct constructor application to the zero pair with no lemmas or computation.
Claim. Let $ActionState$ be the structure with coordinates $(agent, improvementRank) in Nat times Nat. Define $ethicalZero := (0, 0)$.
background
The module Strict/Ethics.lean develops domain-rich ethical realizations over action states with agent and improvement-rank coordinates. The generator is the smallest recognized improvement step. ActionState is the structure with fields agent : Nat and improvementRank : Nat, deriving decidable equality and representation. This zero element anchors the base case for the strict ethical model.
proof idea
Direct definition via the ActionState constructor applied to the pair of zeros.
why it matters
ethicalZero supplies the zero element for strictEthicsRealization, which is then used to establish ethics_admissible as an admissible realization. It also serves as the left identity in preferenceCompose_left_id. In the Recognition framework it instantiates the minimal improvement generator for ethical action states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.