externalization
plain-language theorem explainer
The externalization function maps a moral action to the non-negative portion of the J-cost change it imposes on the target agent. Recognition Science ethicists cite it to quantify injustice as an imposed sigma externalization without target recognition. The definition is a direct one-line application of the max operator to the target's delta J field.
Claim. For a moral action $a$ with fields source_delta_j and target_delta_j, externalization$(a) = $max$(a.target_delta_j, 0)$.
background
MoralAction is the structure recording the J-cost change imposed on a source agent and a target agent. J-cost itself is the derived cost of a multiplicative recognizer comparator (from MultiplicativeRecognizerL4.cost) or the cost of a recognition event (from ObserverForcing.cost). The module sets the local criterion that an action is morally wrong precisely when it externalizes sigma, i.e., increases another agent's J-cost without recognition.
proof idea
One-line definition that applies the max function to the target_delta_j field of the input MoralAction.
why it matters
This definition is the quantitative core of the ethics module; it is invoked directly by externalization_creates_debt (which shows externalization produces positive debt) and just_no_debt (which shows just actions produce zero externalization). It realizes the module claim that injustice is measurable via J-cost and sits inside the Recognition Science forcing chain where J-cost is generated by the T5 J-uniqueness and T6 phi fixed-point constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.