CostAlgebraData
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not specify the explicit closed form of the cost function.
- Does not impose the second-derivative calibration condition at unity.
- Does not address continuity or smoothness of the cost function.
- Does not include any realization or interpretation in a physical model.
formal statement (Lean)
589structure CostAlgebraData where
590 /-- The cost function -/
591 cost : ℝ → ℝ
592 /-- Satisfies the Recognition Composition Law -/
593 rcl : SatisfiesRCL cost
594 /-- Normalization: cost at identity is zero -/
595 normalized : cost 1 = 0
596 /-- Reciprocal symmetry -/
597 symmetric : ∀ x : ℝ, 0 < x → cost x = cost x⁻¹
598 /-- Non-negativity on ℝ₊ -/
599 nonneg : ∀ x : ℝ, 0 < x → 0 ≤ cost x
600
601/-- **THEOREM: J provides the canonical CostAlgebraData.** -/