canonicalRecognitionCostSystem
plain-language theorem explainer
This definition assembles the canonical recognition cost system as the RecognitionCostSystem record on positive reals with cost function J, the RCL satisfaction theorem, the sum-of-logs conservation map, and positive window W. Recognition Science algebraists cite it as the standard concrete model realizing the J-cost. The construction is a direct record instantiation that bundles J, RCL_holds, canonicalSigma, and the supplied window parameters.
Claim. The canonical recognition cost system on dimension $n$ is the structure with cost function $J(x) = ½(x + x^{-1}) - 1$, conservation functional $σ(x) = ∑ log(x_i)$, window length $W > 0$, and the fact that $J$ satisfies the Recognition Composition Law.
background
RecognitionCostSystem packages a ratio cost function, a proof that the cost satisfies the Recognition Composition Law, a conservation functional sigma, and a positive window length W. J is the cost J(x) = ½(x + x^{-1}) - 1 that satisfies the RCL by the upstream theorem RCL_holds. canonicalSigma supplies the conservation map as the sum of logarithms on positive coordinates. The module CostAlgebra constructs algebraic models for recognition costs from the functional equation axioms and the J-cost definition.
proof idea
This is a direct record definition that instantiates RecognitionCostSystem with cost := J, rcl := RCL_holds, sigma := canonicalSigma, W := W, and W_pos := hW. It applies the theorem RCL_holds that J satisfies the RCL and the definition canonicalSigma.
why it matters
This supplies the standard model for the recognition cost system. It is referenced by the downstream theorems canonicalRecognitionCostSystem_cost_inv and canonicalRecognitionCostSystem_cost_one that establish reciprocal symmetry and zero cost at unity. It realizes the J-uniqueness (T5) and RCL from the Recognition Science chain as the concrete instance used for further cost-algebra derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.