ideal_iff_good
plain-language theorem explainer
An action reaches the unique J-minimum configuration if and only if its resulting state has zero defect. Researchers deriving objective ethics from Recognition Science cite this to equate moral goodness with stability under the J-cost. The proof unfolds the two predicates then applies the zero-defect characterization at unity in both directions.
Claim. For any ethical action $a$ with positive initial and final configurations, $a$ reaches the configuration $1$ if and only if the defect of its final configuration is zero.
background
An ethical action is a structure carrying a pair of positive real numbers that represent the initial and final states of a configuration under the ledger. The J-cost is given by $J(x) = (x + x^{-1})/2 - 1$, and defect is this value; moral cost of an action is the defect of its final state. Morally ideal means the final state equals 1; morally good means that defect vanishes.
proof idea
The proof unfolds the definitions of the two predicates and the moral cost function. It splits into both directions with constructor. The forward direction rewrites the equality to 1 and applies the theorem that defect at 1 is zero. The reverse direction applies the biconditional that defect vanishes exactly at 1, using positivity of the final state.
why it matters
This equivalence anchors the objective morality structure by identifying the unique J-minimum with zero cost, supporting the module's claim that ought follows from is via defect minimization. It fills the step that good configurations are exactly the stable ones under the Recognition Composition Law and feeds the dissolution of Hume's guillotine in the philosophy module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.