Composable
The Composable structure equips a cost model with a binary operation on actions that obeys subadditivity of cost and monotonicity under the induced preference preorder. Researchers constructing ethical decision models or algebraic cost structures cite it when they must compose actions while keeping total cost bounded and orderings intact. The declaration is a direct structure definition that states the operation and its three axioms with no further lemmas.
claimA cost model $M$ over actions $A$ is composable when there exists an operation $comp: A×A→A$ such that $cost_M(comp(a,b))≤cost_M(a)+cost_M(b)$ for all $a,b$, the operation preserves the preorder $a≼b$ iff $cost_M(a)≤cost_M(b)$ in both arguments, and it strictly preserves the strict order $a≺b$ iff $cost_M(a)<cost_M(b)$ in the left argument.
background
CostModel is the structure that supplies a cost map from actions to nonnegative reals. Prefer is the preorder on actions defined by lower cost being better. Improves is the corresponding strict order. The module Ethics.CostModel sits alongside Algebra.CostAlgebra, whose comp composes J-automorphisms, and Aesthetics.SymmetryGroupPreference, whose preference is the negation of wallpaperJ cost. This places ethical composition inside the same algebraic setting used for J-cost throughout the framework.
proof idea
The declaration is a structure definition. It introduces the comp field and asserts subadditivity, monotonicity, and strict left monotonicity directly as the remaining fields. No lemmas are applied and no tactics are used.
why it matters in Recognition Science
The structure is invoked by prefer_comp_mono, improves_comp_left, and prefer_trans to establish that composition respects preference and strict improvement. It supplies the algebraic interface required for monotonicity results inside the ethics cost model. The construction mirrors the Recognition Science emphasis on composition laws that preserve ordering, consistent with the RCL and the composition of J-automorphisms.
scope and limits
- Does not exhibit a concrete composition function for any specific action type.
- Does not prove existence of a composable structure for a given cost model.
- Does not link the cost function to J-cost, phi-ladder, or physical constants.
- Does not impose associativity or other algebraic laws on the operation.
formal statement (Lean)
45structure Composable (M : CostModel A) where
46 comp : A → A → A
47 subadd : ∀ a b, M.cost (comp a b) ≤ M.cost a + M.cost b
48 mono : ∀ a a' b b', Prefer M a a' → Prefer M b b' → Prefer M (comp a b) (comp a' b')
49 strict_mono_left : ∀ a a' x, Improves M a a' → Improves M (comp a x) (comp a' x)
50
51/-- Monotonicity of composition w.r.t. preference. -/