P_symmetric_of_F_symmetric
plain-language theorem explainer
If F on positive reals is invariant under reciprocals and satisfies the multiplicative consistency F(xy) + F(x/y) = P(F(x), F(y)), then P must be symmetric on the image of F. Workers deriving the Recognition Composition Law without prior assumptions on P cite this step when closing the unconditional inevitability argument. The proof swaps the arguments in the consistency equation, invokes F's reciprocal symmetry to equate the cross terms, 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 establishes the strongest form of RCL inevitability: both the cost function F and the pairing function P are forced from multiplicative consistency alone, with no structural hypothesis on P. F is required to obey normalization F(1)=0, reciprocal symmetry, C² smoothness, and the calibration G''(0)=1 where G(t)=F(exp(t)). The consistency relation is the only link between F and P. Upstream results supply the ledger factorization of (ℝ₊, ×) and the structure of J-cost, which later identify the unique solution F = J(x) = (x + x^{-1})/2 - 1.
proof idea
Tactic proof: introduce positive x and y; apply the consistency hypothesis once in each order to obtain the two expressions for the sum; use ring_nf to commute the products; establish positivity of the ratios and the inversion identity (x/y)^{-1} = y/x; apply the symmetry hypothesis of F to equate F(x/y) with F(y/x); rewrite both sides and finish with linarith.
why it matters
This lemma is the first of the symmetry-forcing steps that feed P_at_zero_right and P_symmetric_on_range. Together they close the unconditional derivation that P(u,v) = 2uv + 2u + 2v on the range of F, which in turn forces the ODE whose unique solution is the J-cost. It therefore occupies the position immediately after the statement of full RCL inevitability and before the identification with the eight-tick octave and D=3. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.