Composition_Normalization_implies_symmetry
plain-language theorem explainer
Any cost functional obeying the Recognition Composition Law and the Normalization axiom F(1)=0 must satisfy F(x)=F(1/x) for positive x. Researchers establishing the uniqueness of the J-cost function cite this as an early derived property. The argument instantiates the d'Alembert equation at unity, collapses the right-hand side with the zero-cost condition, and rearranges algebraically to obtain symmetry.
Claim. Let $F:ℝ→ℝ$ satisfy the Recognition Composition Law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for all $x,y>0$ and the Normalization condition $F(1)=0$. Then $F(x)=F(x^{-1})$ for all $x>0$.
background
The module formalizes the three primitive axioms of Recognition Science. Normalization asserts that the cost at unity vanishes, $F(1)=0$, because perfect balance incurs no cost. Composition encodes the Recognition Composition Law (RCL), the multiplicative form of d'Alembert's equation: $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for positive arguments. These two axioms alone already force inversion symmetry. The local setting is the axiomatic hierarchy in which Normalization and Composition sit at LEVEL 0, before Calibration is introduced and before the full uniqueness result that identifies $F$ with $J$.
proof idea
The proof instantiates the dAlembert property of Composition at the pair (1,x). After rewriting with one_mul, one_div and Normalization.unit_zero, the equation simplifies to $F(x)+F(x^{-1})=2F(x)$. A ring-based subtraction then isolates $F(x^{-1})=F(x)$.
why it matters
The result feeds directly into uniqueness_specification, the statement that any function satisfying the three cost axioms with regularity equals $J$. It supplies an early step toward T5 Uniqueness in the Recognition Science framework, where the RCL plus Normalization already imply the symmetry that $J$ itself satisfies. The symmetry is therefore available before the calibration axiom fixes the second derivative at the origin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.