ethicsCost_symm
plain-language theorem explainer
Symmetry of the cost function on moral improvement steps is established by case analysis on equality. Researchers formalizing the ethical component of universal forcing cite this to confirm that the compare operation yields a symmetric relation. The proof splits into the equal case, where both sides reduce to zero, and the unequal case, where both sides reduce to one.
Claim. For all $a, b : Nat$, ethicsCost$(a, b) =$ ethicsCost$(b, a)$, where ethicsCost$(a, b) = 0$ if $a = b$ and $1$ otherwise.
background
MoralImprovementStep is defined as an abbreviation for the natural numbers and serves as the carrier counting morally meaningful improvement steps. The ethicsCost function returns zero on identical steps and one otherwise, supplying the minimal comparison needed for the realization. The module provides only the identity and step-comparison structure required by Universal Forcing, without reconstructing the full domain theory of ethics.
proof idea
The tactic proof opens with by_cases on whether a equals b. The equal branch substitutes and simplifies using the definition of ethicsCost. The unequal branch introduces the symmetric inequality b ≠ a and simplifies both sides of the goal with the two cases of the ethicsCost definition.
why it matters
The result feeds directly into ethicsRealization, which constructs the LogicRealization with Carrier := MoralImprovementStep, Cost := Nat, and compare := ethicsCost. It supplies the symmetry property required for the ethical realization to be admissible in the universal forcing chain. No open questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.