F_symmetric_of_P_symmetric
plain-language theorem explainer
Symmetry of the combiner P together with multiplicative consistency of F forces F to be reciprocal symmetric. Researchers deriving the d'Alembert equation from first principles cite this to obtain symmetry without separate assumption. The proof specializes the prior division-swap lemma at the unit value and simplifies the resulting equality.
Claim. Let $F : (0,∞) → ℝ$ and $P : ℝ → ℝ → ℝ$. If $F(xy) + F(x/y) = P(F(x), F(y))$ holds for all $x,y > 0$ and $P(u,v) = P(v,u)$ for all $u,v$, then $F(x) = F(1/x)$ for all $x > 0$.
background
The module proves that the d'Alembert functional equation is the unique form compatible with multiplicative consistency of a cost functional. HasMultiplicativeConsistency requires $F(xy) + F(x/y) = P(F(x), F(y))$ for positive $x,y$. IsSymmetric requires $F(x) = F(1/x)$ for positive $x$. Normalization states that the cost at unity vanishes: $F(1) = 0$. The division-swap lemma shows that symmetry of P implies $F(x/y) = F(y/x)$.
proof idea
This is a one-line wrapper that applies the division-swap theorem F_div_swap_of_P_symmetric at y=1 and simplifies using div_one.
why it matters
This result feeds bilinear_family_forced, which shows consistency forces the unique bilinear family. It advances the chain toward proving the Recognition Composition Law is the only possible form. The module doc states that this closes the gap showing A2 is transcendentally necessary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.