composition_law_without_calibration_does_not_force_jcost
plain-language theorem explainer
A continuous reciprocal normalized cost on the positive reals can obey the Recognition Composition Law and still fail to equal the canonical J-cost. The explicit witness is F(x)=(x²+x⁻²)/2−1. Anyone claiming that RCL plus algebraic side conditions alone force J should cite this counterexample. The proof is a direct term construction: verify the four laws by algebra, then separate from J at x=2.
Claim. There exists $F:\mathbb{R}\to\mathbb{R}$ such that $F(x)=F(x^{-1})$ for all $x>0$, $F(1)=0$, $F$ satisfies the composition law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for $x,y>0$, and $F$ is continuous on $(0,\infty)$, yet $F$ is not the canonical cost $J(x)=(x+x^{-1})/2-1$.
background
In Recognition Science the native cost on positive ratios is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The Recognition Composition Law (RCL) is the functional equation $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Three algebraic side conditions are standard: reciprocal symmetry $F(x)=F(x^{-1})$, normalization $F(1)=0$, and continuity on $(0,\infty)$. A separate calibration condition fixes the second-derivative (curvature) scale at the unit, equivalently $\lim_{t\to 0} 2F(e^t)/t^2=1$.
The module studies which of these hypotheses are load-bearing for uniqueness of $J$ on the continuous completion. Upstream, the same algebraic package appears in the cost functional-equation layer (IsReciprocalCost, IsNormalized, SatisfiesCompositionLaw). The forcing chain's T5 step asserts J-uniqueness only after calibration is included; this theorem isolates what fails when that hypothesis is dropped.
The continuum picture parallels the rational-carrier story: there orientation is free per prime, here the scale parameter $\lambda$ in the family $F_\lambda(x)=(x^\lambda+x^{-\lambda})/2-1$ remains free.
proof idea
Term-mode existence proof. Instantiate the witness $F(x)=(x^2+x^{-2})/2-1$ (the $\lambda=2$ member of the scale family). Reciprocal symmetry: unfold, clear denominators, ring. Normalization: evaluate at $1$, reduce by norm_num to $0$. Composition law: unfold on $x,y>0$, field_simp then ring closes the RCL identity. Continuity on $(0,\infty)$: $x\mapsto x^2$ is continuous, inversion is continuous away from zero (powers of positives stay nonzero), then divide by the constant $2$ and subtract $1$. Inequality $F\neq J$: assume function extensional equality, specialize at $x=2$, unfold both formulas, and obtain a numeric contradiction by norm_num.
why it matters
Headline non-forcing result on the completion side: RCL plus reciprocal symmetry, normalization, and continuity do not select $J$. Calibration is therefore irreducible, not implied by the algebra. Downstream, the same witness seeds the full one-parameter family theorem (every $\lambda>0$ works), the single-point calibration lemma (one evaluation $x_0>1$ kills the gauge), and the joint stratification that packages form-forced / gauge-orbit / calibration-selects-$J$. The structural ledger uses the same idea to refute anchor-free uniqueness: the last field is a genuine unit choice.
In framework terms this sharpens T5. "$\delta$ forces $J$" can only mean "$\delta$ forces the family $F_\lambda$, and a separately supplied unit calibration picks $\lambda=1$." Whether the recognition defect supplies that unit calibration is the open joint (live track T1); this theorem proves the calibration step is genuinely needed. Continuum analogue of the rational underdetermination results on orientation and single-prime calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.