module module high

`IndisputableMonolith.Philosophy.ObjectiveMoralityStructure`

This module defines ethical actions as maps between configurations whose value is measured by induced change in ledger defect, extending the Law of Existence directly into moral evaluation. It introduces predicates for morally better actions, good actions, and the ideal action together with basic ordering properties. Formal ethicists or physicists seeking a defect-based foundation for morality would cite these definitions. The module consists entirely of definitions and elementary lemmas with no complex proofs.

claimAn ethical action is a map $f$ from one configuration to another whose moral cost equals the change in ledger defect it produces.

background

The upstream Law of Existence module states that an entity $x$ exists if and only if defect$(x)=0$. This philosophy module applies the same defect criterion to actions by treating moral evaluation as a comparison of defect before and after the action. The supplied doc-comment identifies EthicalAction precisely as a transformation between configurations that is assessed by its effect on ledger defect; sibling definitions then build moral_cost, MorallyBetter, MorallyGood, and MorallyIdeal on that base.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the vocabulary that connects the Law of Existence to objective morality, directly supporting the sibling results on uniqueness of the moral ideal and dissolution of the is-ought distinction. It places moral ordering inside the same defect framework used for physical existence throughout the Recognition Science chain.

scope and limits

Does not derive concrete moral rules from physical constants.
Does not address subjective or cultural variation in ethics.
Does not claim completeness for all possible ethical scenarios.
Does not provide a decision procedure for conflicting actions.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LawOfExistence module_import

declarations in this module (16)

structure EthicalAction L67
def moral_cost L77
def MorallyBetter L80
def MorallyGood L83
def MorallyIdeal L86
theorem moral_ideal_is_unique L93
theorem ideal_iff_good L100
theorem moral_ordering_refl L109
theorem moral_ordering_trans L112
theorem better_action_exists L120
theorem is_implies_ought L147
theorem hume_guillotine_dissolved L176
theorem moral_progress_is_defect_decrease L194
theorem ethics_is_objective L201
theorem cost_ordering_gives_ethics L212
theorem ph004_objective_morality_certificate L230