mutual_benefit_is_just
plain-language theorem explainer
Mutually beneficial actions reduce J-cost for both source and target agents and therefore satisfy the zero-externalization criterion for justice. Decision theorists and ethicists working in the Recognition Science sigma model would cite this to confirm that mutual benefit implies no debt creation. The proof is a direct projection of the second conjunct from the mutual-benefit definition.
Claim. For any moral action $a$ with source J-cost change $a.source_delta_j$ and target J-cost change $a.target_delta_j$, if $a.source_delta_j ≤ 0$ and $a.target_delta_j ≤ 0$, then $a.target_delta_j ≤ 0$.
background
The Moral Debt module defines ethics via sigma externalization: an action is unjust when it increases another agent's J-cost without recognition. Sigma itself is the gap between private preference and public report, taken from the Abilene Paradox definition where truthful agents have sigma = 0. A MoralAction records the pair of real-valued J-cost deltas for source and target agents. isJust holds precisely when the target delta is non-positive. isMutuallyBeneficial is the conjunction requiring both deltas non-positive.
proof idea
The proof is a one-line term that extracts the second conjunct of the isMutuallyBeneficial hypothesis, which is exactly the target_delta_j ≤ 0 condition demanded by isJust.
why it matters
The result directly supports the module's key claim that just actions have zero net externalization. It closes the basic implication between mutual benefit and justice within the sigma-externalization framework, consistent with the Recognition Science emphasis on measurable J-cost and avoidance of externalized debt. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.