isLovingAction
plain-language theorem explainer
isLovingAction defines a MoralAction as loving exactly when the action decreases the target's J-cost. Recognition Science ethicists cite it to formalize love as measurable sigma reduction. The definition is a direct one-line predicate on the target_delta_j field of the MoralAction structure.
Claim. A moral action $a$ is loving when its effect on the target satisfies $a.target_delta_j < 0$.
background
The Moral Debt module models actions via the MoralAction structure, which records source_delta_j and target_delta_j as real-valued changes in J-cost. Sigma externalization is defined as any increase in a target's J-cost imposed without recognition, creating quantifiable debt. This definition imports the J-cost primitives from JcostCore and rests on the upstream MoralAction structure that supplies the two delta fields.
proof idea
One-line definition that directly sets isLovingAction a to the proposition a.target_delta_j < 0.
why it matters
The definition is invoked by the downstream theorem love_is_just, which concludes isJust a from the strict inequality via le_of_lt. It operationalizes the module's core rule that just actions produce zero net externalization and aligns with the Recognition Science claim that total sigma is conserved in closed systems. The doc-comment links it to the equilibration property proved elsewhere as only_love_changes_sigma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.