CostModel
plain-language theorem explainer
CostModel equips any type A with a nonnegative real-valued cost function on its elements. Researchers formalizing ethical preferences or mechanism design within Recognition Science cite this structure to anchor preference relations. The entry is a direct structure definition with no lemmas or computational reduction.
Claim. A cost model on a set $A$ consists of a function $c: A → ℝ$ together with a proof that $c(a) ≥ 0$ for every $a ∈ A$.
background
Cost functions in Recognition Science descend from J-cost on recognition events and from derived costs on multiplicative recognizers. Upstream, the cost of a recognition event equals the J-cost of its state and is provably nonnegative; aesthetic preference is defined as the negation of J-cost on wallpaper groups. The present module imports IntegrationGap.A and MultiplicativeRecognizerL4.cost to supply concrete instances while keeping the interface minimal.
proof idea
The declaration is a structure definition that directly introduces the two fields cost and nonneg. No tactics or upstream lemmas are invoked; it functions as a type constructor for later predicates such as Prefer and Composable.
why it matters
CostModel supplies the common interface used by Prefer, Improves, Composable, prefer_comp_mono, and improves_comp_left inside the same module. It thereby links ethical ordering to the J-cost machinery of ObserverForcing and the multiplicative cost of MultiplicativeRecognizerL4, supporting the recognition composition law and the forcing chain steps that fix D = 3 and the phi-ladder. It leaves open the specialization of CQ alignment thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.