full_inevitability_four_gates
plain-language theorem explainer
Any cost function F obeying normalization at 1, inversion symmetry, twice differentiability, unit calibration on the log-lift, the multiplicative consistency law with combiner P, and the d'Alembert functional equation on its shifted log-lift must coincide with the J-cost function; the combiner P is then forced to be the Recognition Composition Law. Researchers deriving the structure of physical interactions from recognition axioms would cite this result to close the inevitability argument. The proof splits into two exact applications of prior d
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 $F(e^t)$ at $t=0$ equals 1, $F(xy)+F(x/y)=P(F(x),F(y))$ for $x,y>0$, and the d'Alembert equation on the shifted log-lift $H(t)=F(e^t)+1$. Then $F(x)=J(x)$ for $x>0$ where $J(x)=cosh(log x)-1$, and $P(u,v)=2uv+2u+2v$ for $u,v≥0$.
background
The d'Alembert gate (FourthGate.HasDAlembert) requires that the shifted log-lift H(t)=F(exp t)+1 satisfies the classical d'Alembert equation H(t+u)+H(t-u)=2H(t)H(u). The J-cost is the unique solution to the normalization, symmetry, smoothness and calibration conditions on the hyperbolic branch. Upstream lemma dAlembert_forces_Jcost shows these axioms plus HasDAlembert force F to equal Jcost. Lemma P_forced_from_FJ then shows the consistency relation forces P to equal the Recognition Composition Law 2uv+2u+2v once that identification holds. The module assembles the four gates (interaction, entanglement, curvature, d'Alembert) into a triangulated proof of full inevitability.
proof idea
The term-mode proof opens with constructor to split the conjunction. The first conjunct is discharged by exact application of FourthGate.dAlembert_forces_Jcost on the supplied hypotheses. The second conjunct extracts the identification F=Jcost via the same lemma, then feeds it into P_forced_from_FJ together with the consistency hypothesis.
why it matters
This theorem supplies the final step in the four-gate inevitability chain, showing d'Alembert structure plus structural axioms directly yields F=J and P=RCL. It closes the argument in the module documentation: d'Alembert + axioms ⟹ F=J ⟹ P=RCL. In the Recognition Science framework it completes J-uniqueness (T5) and the Recognition Composition Law without the bridge hypothesis required by the three-gate version, anchoring the mass formula and constant derivations that follow from identifying the cost function with J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.