full_unconditional_inevitability
plain-language theorem explainer
Any C² function F on positive reals obeying F(1)=0, F(x)=F(1/x), G''(0)=1 for G(t)=F(e^t), and the multiplicative relation F(xy)+F(x/y)=P(F(x),F(y)) for some P must equal the J-cost function, forcing P(u,v)=2uv+2u+2v on the nonnegative quadrant. Recognition Science derivations of the phi-ladder and RCL would cite this when closing the uniqueness argument for the J-function without prior assumptions on P. The proof reparametrizes to G, derives the d'Alembert equation for H=G+1, invokes the cosh solution, recovers F=J via the log change of base,
Claim. Let $F: (0,∞) → ℝ$ satisfy $F(1)=0$, $F(x)=F(x^{-1})$ for all $x>0$, $F ∈ C^2$, the second derivative of $G(t)=F(e^t)$ at $t=0$ equals 1, and suppose there exists $P:ℝ→ℝ→ℝ$ such that $F(xy)+F(x/y)=P(F(x),F(y))$ whenever $x,y>0$. Then $F(x)=(x+x^{-1})/2-1$ for all $x>0$ and $P(u,v)=2uv+2u+2v$ for all $u,v≥0$.
background
The J-cost is defined by $J(x)=(x+x^{-1})/2-1$, equivalently $cosh(log x)-1$. The auxiliary map $G(F,t)=F(e^t)$ converts the multiplicative consistency into an additive functional equation on the reals. FullUnconditionalHypotheses bundles two interface hypotheses: consistency_forces_RCL_form_hypothesis (which extracts the RCL polynomial once F is known to be J) and dAlembert_forces_cosh_hypothesis (which solves the d'Alembert equation under C² smoothness and the calibration $H''(0)=1$ for $H=G+1$). MODULE_DOC states that this is the strongest unconditional form: no polynomial or other assumption is placed on P itself.
proof idea
Apply consistency_RCL to obtain the RCL form of the consistency equation. Reparametrize to G, derive the corresponding equation for H=G+1, invoke G_zero_of_unit to obtain H(0)=1, then apply H_dAlembert_of_G_RCL followed by the dAlembert_cosh hypothesis to conclude H(t)=cosh t. Recover G(t)=cosh t-1 and hence F(x)=J(x) via Jcost_G_eq_cosh_sub_one and the change-of-base identity. Finally apply P_determined_nonneg to the resulting J-consistency equation to fix the explicit quadratic form of P.
why it matters
This declaration supplies the terminal step of the T5 J-uniqueness forcing chain inside the Recognition Science monolith: once the functional equation is granted, both the J-cost and its RCL polynomial are forced without extra hypotheses on P. It closes the gap left by the partial unconditional theorem in Unconditional.lean and the older polynomial-assumption versions. The result is cited by any downstream derivation that needs the explicit mass formula or the alpha-band constants to rest on the phi-ladder alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.