ethicsCost_symm
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assign semantic content to individual moral improvement steps.
- Does not extend the cost function beyond the natural-number carrier.
- Does not establish transitivity or triangle inequality.
- Does not derive substantive ethical principles from the forcing axioms.
formal statement (Lean)
28theorem ethicsCost_symm (a b : MoralImprovementStep) : ethicsCost a b = ethicsCost b a := by
proof body
Tactic-mode proof.
29 by_cases h : a = b
30 · subst h; simp [ethicsCost]
31 · have h' : b ≠ a := by intro hb; exact h hb.symm
32 simp [ethicsCost, h, h']
33