injusticeCost
plain-language theorem explainer
The definition assigns to each moral action the sum of its source and target J-cost deltas as the injustice cost. Researchers in Recognition Science ethics cite it to quantify net sigma externalization from an action. It is implemented as a direct algebraic sum of the two real fields in the MoralAction structure.
Claim. For a moral action $a$, the injustice cost equals the sum of the target's J-cost change and the source's J-cost change: $a.target_delta_j + a.source_delta_j$.
background
The Moral Debt module treats moral wrongness as sigma externalization: an action increases another agent's J-cost without recognition. MoralAction is the structure that records the two real-valued J-cost deltas for source and target. J-cost itself is supplied by upstream definitions: the cost of a recognition event equals its J-cost in ObserverForcing, and equals derivedCost of the comparator in MultiplicativeRecognizerL4.
proof idea
One-line definition that directly returns the sum of the two delta fields from the MoralAction record. No lemmas or tactics are invoked.
why it matters
It supplies the quantitative J-cost measure for injustice referenced in the module's key results on measurable injustice and zero-net-externalization for just actions. The construction rests on J-uniqueness (T5) and the Recognition Composition Law by treating net externalization as the observable debt in the phi-ladder setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.