prefer_comp_mono
The monotonicity theorem shows that ethical preference is preserved under binary composition of actions whenever the cost model admits a composable structure. Decision theorists modeling preferences via nonnegative costs would cite this when verifying that composed actions respect ordering. The proof is a direct one-line term application of the mono field inside the Composable structure after unfolding the preference predicate to a cost inequality.
claimLet $M$ be a cost model on type $A$ and let $C$ be a composable structure for $M$. If $a_1$ is preferred to $a_2$ and $b_1$ to $b_2$ under $M$ (i.e., $M.cost(a_1) ≤ M.cost(a_2)$ and likewise for the $b$ pair), then $C.comp(a_1,b_1)$ is preferred to $C.comp(a_2,b_2)$ under $M$.
background
In the Ethics.CostModel module a CostModel is a structure supplying a cost function $A → ℝ$ together with a nonnegativity axiom. The preference relation Prefer is defined directly as the pointwise cost inequality: $a ≼ b$ holds precisely when cost($a$) ≤ cost($b$). Composable augments this with a binary operation comp that is required to be subadditive and to satisfy the monotonicity property that is exactly the statement of the present theorem.
proof idea
The proof is a one-line term-mode wrapper. After dsimp unfolds Prefer to the underlying cost inequalities on both sides, the mono field of the supplied Composable instance $C$ is applied verbatim to the two preference hypotheses.
why it matters in Recognition Science
This result supplies the monotonicity axiom for composition inside the cost-model ethics layer, ensuring that preference orderings survive the formation of composite actions. It sits downstream of the Composition class in Foundation.CostAxioms (the Recognition Composition Law) and upstream of any further preference-transitivity or improvement lemmas in the same module. No direct used-by edges are recorded, indicating it functions as a basic building block rather than a high-level closure.
scope and limits
- Does not establish strict monotonicity for improvements.
- Does not prove subadditivity of the cost function.
- Does not extend to n-ary compositions.
- Does not apply outside models equipped with a Composable instance.
- Does not quantify over all possible action types A.
formal statement (Lean)
52theorem prefer_comp_mono (M : CostModel A) (C : Composable M)
53 {a₁ a₂ b₁ b₂ : A}
54 (ha : Prefer M a₁ a₂) (hb : Prefer M b₁ b₂) :
55 Prefer M (C.comp a₁ b₁) (C.comp a₂ b₂) := by
proof body
Term-mode proof.
56 dsimp [Prefer] at ha hb ⊢
57 exact C.mono a₁ a₂ b₁ b₂ ha hb
58
59/-- Composition preserves improvement. -/