P_symmetric_from_F_symmetric
plain-language theorem explainer
A symmetric cost functional F forces the combiner P in its multiplicative consistency relation to be symmetric in its arguments. Researchers establishing uniqueness of the d'Alembert form in Recognition Science cost functionals would cite this result. The proof applies the consistency equation in both argument orders, uses commutativity of multiplication together with F symmetry on reciprocals, and concludes equality by linear arithmetic.
Claim. Let $F : (0,∞) → ℝ$ satisfy $F(x) = F(x^{-1})$ for all $x > 0$, and let $P : ℝ → ℝ → ℝ$ satisfy $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x,y > 0$. Then $P(F(x), F(y)) = P(F(y), F(x))$ for all $x,y > 0$.
background
The module proves that the d'Alembert functional equation is the unique form compatible with multiplicative consistency for symmetric cost functionals. IsSymmetric F encodes the requirement that F(x) = F(1/x) for positive x, expressing invariance under inversion. HasMultiplicativeConsistency F P encodes the relation F(xy) + F(x/y) = P(F(x), F(y)) for positive x and y, which is the definition of multiplicative consistency used throughout the inevitability argument.
proof idea
The proof instantiates the consistency relation once for the ordered pair (x,y) and once for (y,x). It records that xy equals yx by commutativity. Symmetry of F is applied to the reciprocal to obtain F(x/y) = F(y/x). These substitutions make the left-hand sides identical, so the right-hand sides must coincide; linear arithmetic finishes the equality.
why it matters
This result shows that symmetry of F propagates directly to symmetry of P, a required intermediate step before the bilinear family P(u,v) = 2u + 2v + 2uv can be forced. It forms part of the chain that renders the Recognition Composition Law inevitable rather than postulated, supporting the later steps that recover the eight-tick octave and three spatial dimensions. The module doc-comment identifies this symmetry propagation as closing one gap in the transcendental argument for the full axiom bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.