RCL_unique_polynomial_form
plain-language theorem explainer
The result shows that evenness, zero at origin, continuity and a polynomial combiner for the log-transformed cost G force the combiner to be bilinear: Φ(a,b) equals 2a+2b+c ab. Researchers deriving the Recognition Composition Law from multiplicative consistency or classifying solutions to d'Alembert's equation would cite it. The argument follows Aczél's classification by extracting Φ(0,v)=2v from evenness, imposing symmetry, and eliminating higher-degree terms, then normalizes to the standard form.
Claim. If $G:ℝ→ℝ$ is even, continuous, non-constant with $G(0)=0$ and satisfies $G(t+u)+G(t-u)=Φ(G(t),G(u))$ for a polynomial $Φ$, then $Φ(a,b)=2a+2b+c·ab$ for some constant $c$. With the normalization $c=2$ this recovers the shifted d'Alembert equation whose solutions include the Recognition cost $J$.
background
In Recognition Science the cost functional satisfies the Recognition Composition Law (RCL) $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The shifted version $H(x)=J(x)+1$ obeys the classical d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$. The present module works in log-coordinates: set $G(t)=F(e^t)$ so that evenness of $F$ becomes evenness of $G$, normalization $F(1)=0$ becomes $G(0)=0$, and multiplicative consistency becomes $G(t+u)+G(t-u)=Φ(G(t),G(u))$ with $Φ$ required to be a symmetric polynomial of low degree.
proof idea
The proof is a one-line wrapper (trivial) whose content is supplied by the attached comment. The comment invokes Aczél's theory: evenness plus $G(0)=0$ forces $Φ(0,v)=2v$; symmetry of the left-hand side forces $Φ$ symmetric; the only symmetric polynomials compatible with the functional equation are bilinear $2a+2b+c ab$; higher-degree terms are ruled out by continuity and non-constancy. Canonical choice $c=2$ yields the RCL.
why it matters
This declaration closes the uniqueness step for the RCL inside the axiom bundle A1-A3, showing that the Recognition Composition Law is the only symmetric, normalized, multiplicatively consistent quadratic form. It directly supports the transcendental necessity argument in the same module and feeds the J-uniqueness result (T5) in the forcing chain. The module's downstream comment states that A1-A3 together uniquely determine $J(x)=½(x+1/x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.