isMutuallyBeneficial
plain-language theorem explainer
The definition declares an action mutually beneficial when both source and target agents record non-positive J-cost changes. Recognition Science researchers extending the framework to ethics would cite it to formalize non-externalizing interactions. The definition is a direct conjunction on the two real fields of the MoralAction structure.
Claim. An action $a$ is mutually beneficial when its source J-cost change satisfies $a.source_delta_j ≤ 0$ and its target J-cost change satisfies $a.target_delta_j ≤ 0$.
background
MoralAction is the structure that records the J-cost change imposed on a source agent and on a target agent. J-cost is the Recognition Science functional J(x) = (x + x^{-1})/2 - 1 that quantifies deviation from self-similarity. The module treats moral debt as sigma externalization, i.e., any imposed increase in another agent's J-cost without recognition, and lists just_action_sigma_neutral as the companion result that just actions produce zero net externalization.
proof idea
This is a direct definition. It extracts the source_delta_j and target_delta_j fields from the MoralAction structure and asserts both are non-positive.
why it matters
The definition supplies the hypothesis for the theorem mutual_benefit_is_just, which concludes that such actions are just. It translates the Recognition Science prohibition on externalization into an ethics predicate, linking the J-cost formalism to the claim that just actions are sigma-neutral.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.