washburn_full_unconditional
plain-language theorem explainer
The theorem proves that any F satisfying symmetry under inversion, normalization at unity, C2 smoothness, second-derivative calibration of its log-reparametrization G at zero, and a multiplicative consistency relation with some auxiliary P must coincide with the J-cost function on the positives, forcing P to take the explicit quadratic form 2uv + 2u + 2v. Recognition Science researchers cite it as the strongest unconditional derivation of the core cost function without presupposing the shape of P. The proof is a one-line wrapper that invokes a
Claim. Let $F: (0,∞) → ℝ$ and $P: ℝ → ℝ → ℝ$ satisfy $F(x) = F(x^{-1})$ for all $x > 0$, $F(1) = 0$, $F ∈ C^2$, the calibration $(G_F)''(0) = 1$ where $G_F(t) = F(e^t)$, the consistency $F(xy) + F(x/y) = P(F(x), F(y))$ for $x,y > 0$, the assumption that $P$ is a quadratic polynomial, symmetry of $P$, existence of some $x > 0$ with $F(x) ≠ 0$, continuity of $F$ on $(0,∞)$, and $P(1,1) = 6$. Then $F(x) = J(x)$ for all $x > 0$, where $J(x) = (x + x^{-1})/2 - 1$, and $P(u,v) = 2uv + 2u + 2v$ for all $u,v ≥ 0$.
background
The module establishes the strongest form of RCL inevitability: both the cost function F and the combiner P are forced with no prior assumption on the shape of P. The key auxiliary object is the log-reparametrization $G_F(t) = F(e^t)$ whose second derivative at zero is fixed to 1 by the calibration hypothesis. Upstream, consistency_forces_RCL_form_is_theorem shows that the given normalization P(1,1)=6 together with the polynomial assumption on P already forces P into the RCL quadratic shape once F is known to be J. The d'Alembert step then converts the functional equation into an ODE whose unique solution is the hyperbolic cosine, hence F equals J.
proof idea
The proof is a one-line wrapper that applies full_inevitability_explicit to the given data. It supplies the two required sub-results by direct appeal: consistency_forces_RCL_form_is_theorem (which converts the polynomial P into RCL form under the normalization P(1,1)=6) and dAlembert_forces_cosh_is_theorem (which extracts the cosh solution from the calibrated functional equation). No further tactics are needed.
why it matters
This declaration supplies the terminal unconditional step in the forcing chain (T5 J-uniqueness) that Recognition Science uses to derive the core cost function without external assumptions. It closes the loop from the multiplicative consistency relation to the explicit J-cost and RCL polynomial, feeding directly into downstream derivations of constants and mass ladders. The module documentation notes that earlier versions either assumed F = J or presupposed the polynomial form of P; the present result removes both restrictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.