P_diagonal
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not presuppose differentiability of F.
- Does not determine the global form of P.
- Restricts attention to strictly positive arguments.
- Does not extend to the zero or negative reals.
formal statement (Lean)
129theorem P_diagonal
130 (F : ℝ → ℝ)
131 (P : ℝ → ℝ → ℝ)
132 (hUnit : F 1 = 0)
133 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
134 ∀ x : ℝ, 0 < x → P (F x) (F x) = F (x * x) := by
proof body
Term-mode proof.
135 intro x hx
136 have h := hCons x x hx hx
137 simp only [div_self (ne_of_gt hx)] at h
138 rw [hUnit] at h
139 linarith
140
141/-! ## Part 4: Differential Constraints from Functional Equation
142
143The key insight: even without knowing P's form, we can derive that G satisfies
144the d'Alembert equation, which implies the ODE G'' = G (after shifting).
145
146This follows from the *structure* of the equation G(t+u) + G(t-u) = Q(G(t), G(u)).
147-/
148
149/-- The functional equation in log coordinates. -/