P_diagonal
plain-language theorem explainer
The declaration shows that any consistency map P obeying the multiplicative relation with a normalized F must satisfy the diagonal identity P(F(x),F(x)) = F(x²) for positive x. Workers on the Recognition Science forcing chain cite this step when deriving the explicit form of the composition law from the functional equation alone. The argument is a direct substitution of equal arguments into the hypothesis, followed by cancellation of the unit term.
Claim. Let $F : ℝ → ℝ$ and $P : ℝ → ℝ → ℝ$ be functions such that $F(1) = 0$ and $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x, y > 0$. Then $P(F(x), F(x)) = F(x^2)$ for all $x > 0$.
background
This result sits inside the module establishing the full unconditional inevitability of the Recognition Composition Law. The setting assumes only normalization at unity and the existence of some P making the multiplicative consistency hold; no form is presupposed for P. The upstream reparametrization G(t) = F(exp t) converts the equation into d'Alembert form, but the present lemma operates directly in the original variables.
proof idea
Substitute y = x into the consistency hypothesis to obtain F(x * x) + F(1) = P(F(x), F(x)). The unit condition then forces the left side to equal F(x²) after cancellation, yielding the diagonal identity. The argument uses only the hypothesis and basic arithmetic simplification.
why it matters
This lemma supplies the diagonal case required for the subsequent derivation of the d'Alembert equation in the full unconditional theorem. It advances the chain from the general RCL hypothesis toward the explicit identification of F with the J-cost function J(x) = (x + x^{-1})/2 - 1. The result is invoked in the proof that P takes the form 2uv + 2u + 2v on the non-negative quadrant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.