aczel_theorem_3_1_3_hypothesis
plain-language theorem explainer
Names the false claim that evenness, vanishing at zero, continuity, and unit second derivative at the origin force the Cosh-Add (d'Alembert) identity on a real cost G. Kept only as the subject of the no-go certificate: the quadratic G(t)=t²/2 meets every hypothesis and fails Cosh-Add. Anyone citing the T5 ledger-cost chain or the independence of composition law C6 should reference this Prop and its refutation.
Claim. The following proposition (false): for every $G:\mathbb{R}\to\mathbb{R}$, if $G$ is even, $G(0)=0$, $G$ is continuous, and $G''(0)=1$, then $G$ satisfies the ledger Cosh-Add identity (the d'Alembert functional equation in log coordinates).
background
This module sits in the T5 verification path: ledger structure (T3) forces reciprocal symmetry $F(x)=F(1/x)$ and unit normalization $F(1)=0$, but does not force the remaining T5 constraint. Costs are often reparametrized in log coordinates by $G(t)=F(e^t)$; Cosh-Add is the d'Alembert form of the Recognition Composition Law in that chart.
The honest forcing diagram is: T3 yields symmetry and unit; composition/Cosh-Add (paper closure C6) is an independent hypothesis; with C1–C7 one recovers the unique admissible cost $J(x)=\frac12(x+1/x)-1$ (T5). Aczél's classical work classifies solutions of d'Alembert; it does not derive that equation from regularity alone.
An earlier draft misread Aczél (1966, Thm. 3.1.3) as supplying Cosh-Add from evenness, normalization, continuity, and curvature calibration. The 2026 audit (Finding 2) retracted that claim. This definition freezes the mistaken proposition so the kernel can refute it.
proof idea
No proof: this is a bare def equating a name to a Prop. The body is the universal statement that every even continuous $G$ with $G(0)=0$ and $G''(0)=1$ satisfies CoshAddFromLedger. Downstream lemmas supply the counter-model and the negation; nothing is proved at this declaration.
why it matters
This is the named subject of the module's no-go certificate. Downstream, aczel_hypothesis_refuted proves its negation by feeding the quadratic witness $G(t)=t^2/2$ (even, zero at origin, continuous, unit second derivative) into the hypothesis and invoking quadraticWitness_not_coshAdd (failure at $t=u=1$: LHS $2$, RHS $5/2$).
In the Recognition framework this pins T5 honesty: J-uniqueness (forcing chain T5) still needs the composition law / RCL as load-bearing input; ledger double-entry and identity postings only buy symmetry and unit. Without this frozen false claim, the audit trail that C6 cannot be smuggled in from regularity would be informal. Nothing downstream may assume the proposition; it exists solely to be refuted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.