externalization_creates_debt
plain-language theorem explainer
Externalization of sigma by a moral action imposes strictly positive J-cost debt on the receiving agent. Researchers formalizing ethics within Recognition Science cite this to establish that injustice is quantitatively measurable via J-cost. The proof reduces the claim by simplification of the externalization and externalizesSigma definitions then applies the max inequality lemma.
Claim. Let $a$ be a moral action recording J-cost deltas for source and target agents. If the target's J-cost change is positive, then the externalization measure defined as the positive part of that change is strictly greater than zero.
background
The MoralDebt module treats injustice as sigma externalization: an action is wrong when it increases another agent's J-cost without recognition. MoralAction is the structure holding source_delta_j and target_delta_j. Externalization returns max(target_delta_j, 0) while externalizesSigma asserts target_delta_j > 0. Sigma itself is imported from decision theory as the gap between private preference and public report.
proof idea
Term-mode proof. Simplification rewrites externalization and externalizesSigma in place; the goal then reduces to showing that a positive target delta yields a positive max, which follows directly from the lemma lt_max_of_lt_left applied to the hypothesis.
why it matters
The result shows sigma externalization produces measurable J-cost debt, grounding the module claim that injustice has quantitative value. It anchors ethics in the same J-cost and Recognition Composition Law used for the forcing chain (T5 J-uniqueness through T8 D=3). No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.