module module high

`IndisputableMonolith.Philosophy.ObjectiveMoralityStructure`

The module grounds objective morality in Recognition Science by defining ethical actions as configuration mappings whose value is measured by ledger defect change. It introduces predicates for morally better, good, and ideal actions together with their ordering properties. Researchers working on foundations of ethics or is-ought problems would cite the module to link the Law of Existence directly to moral evaluation. The module consists of definitions plus short proofs establishing reflexivity, transitivity, and existence of better actions.

claimAn ethical action is a map $a : C_1, C_2$ between configurations such that its moral cost equals the change in defect; $a$ is morally better than $b$ when moral_cost$(a) < $ moral_cost$(b)$, morally good when no better action exists, and morally ideal when it is the unique minimum-cost action.

background

The module imports the Law of Existence, which states that an entity $x$ exists if and only if defect$(x) = 0$. Configurations are the objects whose defects are tracked; an action is any map sending one configuration to another. Moral evaluation is defined by comparing the defect of the image configuration against the defect of the source, yielding a numerical cost that induces a preorder on actions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the formal bridge from the defect-based Law of Existence to moral philosophy, enabling downstream results such as uniqueness of the moral ideal and dissolution of Hume's guillotine. It shows that the ought of ethical action is reducible to the is of defect minimization without additional normative axioms.

scope and limits

Does not enumerate concrete physical actions.
Does not assign numerical values to specific defects.
Does not address non-configurational or non-defect ethics.
Does not prove that every action has a morally ideal successor.

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