just_no_debt
plain-language theorem explainer
Actions classified as just under the isJust predicate externalize zero sigma. Physicists and ethicists using Recognition Science cite it to confirm zero debt from just actions. The term-mode proof simplifies the definitions and invokes the max right equality.
Claim. If $a$ is a moral action with target J-cost delta satisfying $a.target_delta_j ≤ 0$, then $max(a.target_delta_j, 0) = 0$.
background
The Moral Debt module models actions via the MoralAction structure, which records source and target J-cost deltas. Externalization is the positive part max(target_delta_j, 0), while isJust holds precisely when target_delta_j ≤ 0. This implements the module criterion that moral wrongness equals sigma externalization without recognition by the target agent.
proof idea
The term proof simplifies externalization and isJust at the hypothesis, then applies max_eq_right directly to the inequality target_delta_j ≤ 0.
why it matters
This theorem establishes zero externalization for just actions, supporting the module key result just_action_sigma_neutral and the sigma-neutrality of justice. It aligns with Recognition Science sigma conservation from the RRF ledger and strain net without new hypotheses. No open questions or downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.