externalization_creates_debt
plain-language theorem explainer
If a moral action externalizes sigma then the imposed J-cost on the target is strictly positive. Recognition Science ethics work would cite this to establish that sigma externalization produces measurable debt. The proof is a one-line wrapper that unfolds the two definitions and applies lt_max_of_lt_left.
Claim. Let $a$ be a moral action with source and target J-cost deltas. If the target's J-cost delta is positive, then $0 <$ max(target delta, 0).
background
MoralAction is the structure recording a source_delta_j and target_delta_j in real numbers; it models any action whose J-cost effects can be tracked. externalization(a) is defined as max(target_delta_j, 0), the non-negative portion of the target's J-cost change. externalizesSigma(a) is the proposition target_delta_j > 0, i.e., the action imposes a positive J-cost increase on the recipient. The module frames this as a physics-native ethics criterion: an action is morally wrong precisely when it externalizes sigma without the target's recognition. Upstream, sigma itself is the private-public report gap imported from the AbileneParadox development.
proof idea
Term-mode proof. simp only [externalization, externalizesSigma] at * reduces the goal to 0 < max(target_delta_j, 0) under the hypothesis target_delta_j > 0; exact lt_max_of_lt_left h discharges it directly.
why it matters
The theorem supplies the quantitative link between sigma externalization and positive J-cost debt, listed among the module's key results. It sits inside the Moral Debt development that treats injustice as measurable via J-cost; downstream siblings such as just_no_debt and injusticeCost rely on the same externalization machinery. It connects the Recognition Science J-cost formalism (T5 J-uniqueness and the RCL) to an ethics criterion without introducing new primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.