pith. sign in
module module moderate

IndisputableMonolith.Ethics.MoralDebt

show as:
view Lean formalization →

MoralDebt module defines moral actions as those altering J-cost between source and target agents. Researchers extending Recognition Science to ethics would cite it to ground moral concepts in the J-cost formalism. It is a definition module containing no proofs.

claimMoralAction$(s,t)$ holds when an action from source agent $s$ to target $t$ changes the J-cost of both agents.

background

The module imports JcostCore, which supplies the J-cost definitions built from the J function and Recognition Composition Law. J-cost quantifies deviation under the forcing chain T5 J-uniqueness. The module introduces predicates on pairs of agents including externalization, isJust, isMutuallyBeneficial, isLovingAction, and sigma_conservation that track debt creation or cancellation.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

It supplies the base interface linking J-cost to moral debt, feeding the ethics domain though no used_by theorems are listed. It applies the T5 J-uniqueness and RCL landmarks to agent interactions.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)