CostAlgebraData
plain-language theorem explainer
CostAlgebraData packages a cost function on positive reals together with the Recognition Composition Law, normalization at unity, reciprocal symmetry, and non-negativity. Algebraic work on the foundations of Recognition Science cites this structure when defining morphisms or proving uniqueness of the J-cost. The declaration is a pure structure definition that bundles the four properties with no proof obligations or computational content.
Claim. A CostAlgebraData consists of a function $c : (0,∞) → ℝ$ such that $c(xy) + c(x/y) = 2c(x)c(y) + 2c(x) + 2c(y)$ for all $x,y > 0$, $c(1) = 0$, $c(x) = c(x^{-1})$ for $x > 0$, and $c(x) ≥ 0$ for $x > 0$.
background
The Recognition Composition Law (SatisfiesRCL) is the single primitive of Recognition Science: for a function F, F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y) whenever x,y > 0. This is the multiplicative form of d'Alembert's functional equation. The J-cost is the explicit function J(x) = ½(x + x^{-1}) - 1 that satisfies the law together with normalization at 1, symmetry under inversion, and non-negativity on the positive reals.
proof idea
This declaration is a structure definition that directly bundles the cost function with the four required properties: satisfaction of the Recognition Composition Law via SatisfiesRCL, normalization at unity, reciprocal symmetry, and non-negativity. No lemmas or tactics are applied; the definition is a pure packaging of the data.
why it matters
CostAlgebraData is the fundamental algebraic object of Recognition Science from which all further structure is derived. It is instantiated by canonicalCostAlgebra using the J function and supplies the carrier for the uniqueness theorems cost_algebra_unique and cost_algebra_unique_aczel (T5 in the forcing chain). The same structure supports the definition of CostMorphism between cost algebras.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.