full_inevitability_explicit
plain-language theorem explainer
Any C² function F on positive reals obeying inversion symmetry, unit normalization at 1, and a multiplicative consistency relation F(xy) + F(x/y) = P(F(x), F(y)) for some combiner P must equal the J-cost function J(x) = (x + x^{-1})/2 - 1. The associated P is forced to the bilinear form 2uv + 2u + 2v on the nonnegative quadrant. Recognition Science researchers cite this as the explicit unconditional inevitability result. The argument lifts to G(t) = F(e^t), verifies the d'Alembert equation, and invokes cosh uniqueness under the given second-der
Claim. Let $F : ℝ → ℝ$ and $P : ℝ → ℝ → ℝ$ satisfy $F(1) = 0$, $F(x) = F(x^{-1})$ for $x > 0$, $F$ twice continuously differentiable, the second derivative of $G(t) := F(e^t)$ at zero equal to 1, and $F(xy) + F(x/y) = P(F(x), F(y))$ for $x, y > 0$. Assume moreover that $P(F(x), F(y)) = 2 F(x) F(y) + 2 F(x) + 2 F(y)$ and that any $H$ obeying the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$, $H(0)=1$, twice differentiable with $H''(0)=1$ equals the hyperbolic cosine. Then $F(x) = (x + x^{-1})/2 - 1$ for $x > 0$ and $P(u, v) = 2uv + 2u + 2v$ for $u, v ≥ 0$.
background
In Recognition Science the J-cost is the function J(x) = (x + x^{-1})/2 - 1. The auxiliary map G(t) = F(exp t) converts multiplicative consistency into an additive relation on the reals. The module establishes the strongest form of RCL inevitability by assuming only the existence of some combiner P and deriving both F and P uniquely from smoothness, symmetry, normalization, and calibration of G''(0) = 1. The shifted function H = G + 1 satisfies the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0) = 1. Upstream results include the verification that G satisfies this equation under the RCL hypothesis (H_dAlembert_of_G_RCL) and the uniqueness theorem forcing H to cosh under the calibration condition.
proof idea
The proof first derives that G satisfies the RCL form of the d'Alembert equation by substituting exponential variables into the consistency relation and applying the RCL hypothesis. It then defines Hloc = G + 1, verifies Hloc(0) = 1 via G_zero_of_unit, the d'Alembert relation via H_dAlembert_of_G_RCL, smoothness by composition with exp, and the second-derivative calibration by direct differentiation. Application of the dA_cosh hypothesis yields Hloc = cosh, hence G = cosh - 1. Inversion via the logarithm recovers F = Jcost on positives using Jcost_G_eq_cosh_sub_one. The P conclusion follows by surjectivity of J onto the nonnegatives (J_surjective_nonneg) and substitution into the RCL form.
why it matters
This is the explicit form of the full unconditional inevitability theorem. It feeds the washburn_full_unconditional result that closes the forcing chain. The declaration shows that the Recognition Composition Law is the only combiner compatible with T5 J-uniqueness and the d'Alembert step under the given calibration. It removes all prior assumptions on P and thereby strengthens the link from the consistency hypothesis to the eight-tick octave and D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.