pith. sign in
module module moderate

IndisputableMonolith.Ethics.MoralDebt

show as:
view Lean formalization →

The module defines moral actions as interactions that change J-cost for source and target agents, extending Recognition Science into ethics. Researchers working on ethical implications of the J-cost framework would cite these definitions. The module consists entirely of definitions and basic lemmas with no complex proofs.

claimA moral action from source agent $a$ to target agent $b$ is an interaction that alters the J-cost of both agents; derived predicates include isJust (zero net J-cost change), isMutuallyBeneficial, and isLovingAction, together with externalization and sigma conservation.

background

The module imports JcostCore, which supplies the J-cost function based on the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). It introduces MoralAction as the central object: an action affecting J-cost of source and target agents. Sibling definitions then build predicates such as externalization, isJust, injusticeCost, isMutuallyBeneficial, and isLovingAction, plus the lemma sigma_conservation.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the basic objects for ethical analysis inside the Recognition Science framework, feeding MoralAction, isJust, and sigma_conservation into any later ethical theorems. It directly applies the J-cost machinery to moral philosophy without yet linking to specific upstream chain steps T0-T8.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)