module module high

`IndisputableMonolith.Philosophy.ObjectiveMoralityStructure`

This module defines objective morality by evaluating actions according to their effect on ledger defect, extending the Law of Existence. Researchers deriving ethics from physical first principles would cite it. It consists of definitions for ethical actions and moral orderings together with basic reflexivity and transitivity properties.

claimAn ethical action is a mapping from one configuration to another evaluated by its net change in defect, where defect zero marks existence.

background

The upstream Law of Existence module states that an entity x exists if and only if defect(x) = 0. This philosophy module applies that ledger to actions by defining EthicalAction as a configuration-to-configuration map whose moral cost is measured by the resulting defect change. Sibling definitions introduce moral_cost, MorallyBetter, MorallyGood, and MorallyIdeal, plus ordering axioms and the claim that the moral ideal is unique.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the formal bridge from the Law of Existence to objective morality, directly enabling sibling results such as moral_ideal_is_unique, ideal_iff_good, and hume_guillotine_dissolved. It thereby places ethical ordering inside the Recognition framework without additional physical postulates.

scope and limits

Does not derive concrete moral prescriptions from physics.
Does not address subjective or cultural interpretations of value.
Does not quantify defect changes for specific physical systems.
Does not claim completeness of the moral ordering.

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