J
plain-language theorem explainer
The canonical cost functional J is defined on the reals by the formula (x plus the reciprocal of x) divided by two, minus one. Researchers deriving the Recognition Science framework from its primitive axioms cite this definition to invoke the explicit solution to the normalization, composition, and calibration conditions. The definition is introduced directly as the closed-form expression that satisfies the functional equation.
Claim. The cost functional is defined by $J(x) = (x + x^{-1})/2 - 1$ for real $x$.
background
The Cost Axioms module formalizes three primitive axioms: Normalization requires F(1) = 0, Recognition Composition Law states F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y), and Calibration sets the second logarithmic derivative at zero to one. J is introduced as the canonical cost functional measuring the cost of a ratio x relative to unity, with J(1) = 0 and divergence to infinity as x approaches zero. Upstream, Cost is an abbreviation for Quantity CostUnit.
proof idea
Direct definition that sets J(x) to the explicit algebraic expression (x + 1/x)/2 - 1. No lemmas are applied; the form matches the closed-form solution to the d'Alembert functional equation referenced in the module documentation.
why it matters
This definition supplies the explicit form of the cost functional that occupies the first derived level in the axiomatic hierarchy, enabling the law of existence and the meta-principle that nothing cannot recognize itself. It corresponds to the J-uniqueness step in the forcing chain, from which the framework proceeds to self-similar fixed points and derived physical structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.