aczel_hypothesis_refuted
plain-language theorem explainer
Symmetry, unit normalization, continuity, and unit log-curvature calibration do not force the Cosh-Add (d'Alembert) identity. Anyone citing T5 uniqueness or the ledger-to-cost chain needs this no-go: the composition law C6 is an independent load-bearing hypothesis. The proof applies the quadratic witness G(t)=t²/2 to the refuted Aczél-style claim and obtains a contradiction with the known failure of Cosh-Add for that witness.
Claim. It is false that every even real function $G$ with $G(0)=0$, continuous, and unit second derivative at the origin must satisfy the Cosh-Add identity $G(t+u)+G(t-u)=2G(t)G(u)+2G(t)+2G(u)$ for all real $t,u$. The quadratic $G(t)=t^2/2$ is a counterexample.
background
This module sits in the T5 verification layer of Recognition Science. From the ledger (T3) one derives only two cost constraints: reciprocal symmetry $F(x)=F(1/x)$ from double-entry bookkeeping, and unit normalization $F(1)=0$ from the identity posting. Those two facts are packaged as ledger compatibility of a cost functional.
The remaining T5 ingredient is the Cosh-Add identity on the log axis, $G(t+u)+G(t-u)=2G(t)G(u)+2G(t)+2G(u)$. That identity is the log-form of the Recognition Composition Law (paper closure hypothesis C6) and is equivalent, under the usual calibration, to uniqueness of the J-cost $J(x)=\frac12(x+x^{-1})-1$. An earlier draft claimed Cosh-Add followed from symmetry, unit, continuity, and curvature calibration by citing Aczél (1966, Thm. 3.1.3). That claim is the proposition refuted here.
The quadratic witness $G(t)=t^2/2$ is even, vanishes at zero, is smooth, and can be calibrated to unit second derivative, yet fails Cosh-Add. So C6 cannot be discharged from T1–T4 alone.
proof idea
Term-mode reductio. Assume the Aczél-style hypothesis. Instantiate it at the quadratic witness $G(t)=t^2/2$, feeding the already-proved facts that the witness is even, vanishes at the origin, is continuous, and has the required second-derivative calibration. The hypothesis then asserts that this $G$ satisfies Cosh-Add. That assertion is discharged by the prior lemma that the quadratic witness does not satisfy Cosh-Add, yielding falsehood. No classification theorem is invoked; the argument is pure counterexample application.
why it matters
This is the kernel-checked resolution of internal audit Finding 2. It forces the honest forcing chain: T3 yields only symmetry and unit; C6 (Cosh-Add / composition law) and C7 (calibration) remain independent inputs to the T5 characterization. Downstream, CoshAddFromLedger is explicitly documented as an independent hypothesis, and ledger_forces_t5_constraints claims only the two ledger-derived constraints, not uniqueness of $J$. Constraint-forcing aliases that re-export reciprocal symmetry and unit normalization inherit the same scope.
In the primer landmarks, T5 J-uniqueness is therefore conditional on C1–C7, not an unconditional consequence of T0–T4. The RCL stays load-bearing. Without this no-go, the framework would overclaim that the ledger alone selects $J(x)=\cosh(\log x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.