pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Ethics.MoralDebt

show as:
view Lean formalization →

The Ethics.MoralDebt module formalizes moral actions as operations that modify J-cost for both source and target agents, extending the Recognition Science cost model into ethics. Researchers examining physics-derived morality would cite these definitions when analyzing interpersonal recognition deficits. The module supplies a collection of definitions and predicates built directly on the imported JcostCore module.

claimLet $J$ be the cost function from JcostCore. A moral action is a relation between source agent $s$ and target agent $t$ such that the action alters $J(s)$ and $J(t)$. Related predicates include isJust, isMutuallyBeneficial, and isLovingAction, together with conservation statements such as sigma_conservation.

background

Recognition Science builds all structure from the J-cost function obeying the Recognition Composition Law. The upstream JcostCore module supplies the core J-cost definitions and the associated composition identity. This ethics module introduces MoralAction as any action that changes J-cost for both participating agents and then layers predicates for justice, mutual benefit, and love on top of that base.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the ethical interface for the J-cost formalism and directly supports sibling declarations such as externalization_creates_debt, injusticeCost, and sigma_conservation. It grounds moral concepts in the same J-function used for physical constants and the forcing chain, opening a route from recognition deficits to ethical accounting.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)