improves_comp_left
plain-language theorem explainer
If action a strictly improves on b under cost model M, then left-composing both with any x preserves the strict cost reduction. Researchers modeling ethical preferences or decision costs under composition would cite this monotonicity result. The proof is a direct one-line application of the strict left monotonicity axiom supplied inside the Composable structure.
Claim. Let $M$ be a cost model on actions of type $A$ and let $C$ be a composable structure for $M$. For actions $a,b,x$ in $A$, if the cost of $a$ is strictly less than the cost of $b$, then the cost of the composition of $a$ with $x$ is strictly less than the cost of the composition of $b$ with $x$.
background
CostModel is a structure supplying a cost function from actions to nonnegative reals together with a nonnegativity axiom. Composable augments CostModel with a binary composition operation, subadditivity of costs, a monotonicity property for the induced preference relation, and a strict left monotonicity axiom for the strict improvement predicate. Improves is defined directly as the strict inequality of costs under the model.
proof idea
The proof is a one-line term wrapper that applies the strict_mono_left field of the supplied Composable instance C to the hypothesis h.
why it matters
The result guarantees that strict improvements propagate through left composition, supporting consistent ordering in composed actions within the Ethics.CostModel module. It rests on the strict_mono_left axiom of Composable and interfaces with composition notions from Algebra.CostAlgebra. No downstream uses are recorded, indicating a foundational role for later preference or decision constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.