P_forced_to_RCL
plain-language theorem explainer
The theorem establishes that any combiner P satisfying the consistency equation with a cost function F obeying normalization, symmetry, twice continuous differentiability, calibration of the log-lift second derivative at zero, and the interaction condition must equal the Recognition Composition Law on the non-negative reals. Researchers deriving composition laws from symmetry in self-similar physical models would cite this to confirm uniqueness of the interaction term. The argument first invokes the companion uniqueness result identifying F asJ
Claim. Let $F: (0,∞) → ℝ$ and $P: ℝ → ℝ → ℝ$ satisfy $F(1)=0$, $F(x)=F(x^{-1})$ for $x>0$, $F$ twice continuously differentiable, the second derivative of the log-lift $G(t)=F(e^t)$ equal to 1 at $t=0$, the consistency relation $F(xy)+F(x/y)=P(F(x),F(y))$ for $x,y>0$, and the interaction condition on $F$. Then $P(u,v)=2uv+2u+2v$ for all $u,v≥0$.
background
The Analytic Bridge module proves that structural axioms on a cost function together with interaction force the combiner to satisfy the d'Alembert equation. The log-lift is defined by $G_of F t := F(exp t)$. Jcost is the function $J(x)=(x+x^{-1})/2-1$ for $x>0$, which satisfies the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
proof idea
The proof applies F_forced_to_Jcost to conclude F equals Jcost on positives. It invokes Jcost_surjective_on_nonneg to select preimages x,y ≥1 with Jcost(x)=u and Jcost(y)=v. Substituting into the consistency hypothesis and equating to the identity from Jcost_has_RCL_combiner yields the required form after rewriting.
why it matters
This result completes the analytic bridge by forcing P to the RCL form once F is identified with Jcost. It is invoked directly by the parent theorem full_inevitability, the main result of the module asserting uniqueness of both F and P under the axioms plus interaction. The declaration fills the J-uniqueness step (T5) in the forcing chain and confirms interaction selects the d'Alembert structure, consistent with the eight-tick octave and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.