externalizesSigma
plain-language theorem explainer
Definition externalizesSigma marks an action as externalizing sigma exactly when the target's J-cost delta is positive. Recognition Science researchers working on moral debt would cite this predicate when quantifying injustice from J-cost transfers. It is introduced as a direct predicate on the MoralAction structure with no derivation steps.
Claim. An action $a$ externalizes sigma if the target's J-cost change satisfies $a.target_delta_j > 0$.
background
The Moral Debt module frames sigma externalization as the criterion for measurable injustice in a physics-native ethics. A MoralAction is the structure recording real-valued J-cost deltas for source and target agents. The module states that an action is morally wrong when it increases another agent's J-cost without recognition, producing the rule 'do not externalize sigma' with zero sorrys across its results.
proof idea
The declaration is a direct definition that equates externalizesSigma a to the proposition a.target_delta_j > 0. No lemmas are applied; it performs a one-line predicate extraction from the MoralAction record.
why it matters
This definition supplies the predicate consumed by the theorem externalization_creates_debt, which establishes that externalization produces positive debt on the receiving agent. It fills the module's role of quantifying injustice as a J-cost increase and supports the claim that just actions remain sigma-neutral. The construction ties directly to the J-cost function imported from JcostCore.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.