canonicalCostAlgebra
plain-language theorem explainer
J supplies the canonical CostAlgebraData by setting the cost function to the J-cost on positive reals. Algebraists tracing the forcing chain from the recognition composition law would reference this as the initial object in the category of cost algebras. The definition is a direct packaging of the four verified properties of J into the required structure record.
Claim. The structure on positive reals whose cost function is $J(x) = ½(x + x^{-1}) - 1$, satisfying the recognition composition law, with $J(1) = 0$, $J(x) = J(x^{-1})$ for $x > 0$, and non-negativity.
background
CostAlgebraData is the structure that packages the complete algebraic data for a cost function on positive reals: a map cost : ℝ → ℝ, a proof that it satisfies the Recognition Composition Law, normalization cost(1) = 0, symmetry cost(x) = cost(x^{-1}) for x > 0, and non-negativity. J is the explicit function J(x) = ½(x + x^{-1}) - 1. Upstream results establish that J meets each axiom: RCL_holds shows the composition law, J_at_one gives normalization at the identity, J_reciprocal gives the inversion symmetry, and J_nonneg supplies non-negativity.
proof idea
The definition is a direct record construction that sets the cost field to J and populates the remaining fields with the theorems RCL_holds, J_at_one, J_reciprocal, and J_nonneg.
why it matters
This supplies the initial object in the RecognitionCategory, from which morphisms exist to any other calibrated cost algebra. It realizes T5 (J-uniqueness) in the forcing chain and is used to construct the canonical layered system in RecognitionCategory.canonicalLayerSysPlus. The construction closes the algebraic calibration step before introducing phi and the octave layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.