isJust
plain-language theorem explainer
A just action is one whose target J-cost change is non-positive. Recognition Science researchers cite this predicate to classify actions that avoid sigma externalization. The definition is a direct predicate on the target_delta_j field of the MoralAction structure.
Claim. Let $a$ be a moral action with J-cost effects $source_delta_j$ and $target_delta_j$. Then $a$ is just precisely when $target_delta_j(a) ≤ 0$.
background
The MoralDebt module treats moral wrongness as sigma externalization: an action increases another agent's J-cost without recognition. MoralAction is the structure recording the source and target J-cost deltas for any such action. The upstream MoralAction definition supplies the two real-valued fields that isJust inspects.
proof idea
This is a direct definition: isJust holds exactly when the target_delta_j component satisfies the non-positive inequality.
why it matters
The definition supplies the predicate used by just_no_debt (which shows externalization vanishes), love_is_just (which shows loving actions satisfy the predicate), and mutual_benefit_is_just (which shows mutually beneficial actions satisfy it). It thereby operationalizes the module's central claim that injustice equals measurable sigma externalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.