full_inevitability_triangulated
plain-language theorem explainer
The triangulated inevitability result shows that interaction on F together with normalization, symmetry, smoothness, calibration and the consistency relation force the combiner P to be entangling while the log-lift of F obeys the hyperbolic ODE G'' = G + 1. Researchers closing the Recognition Science forcing chain from the interaction gate to the curvature gate would cite this when isolating the remaining bridge step. The proof splits the conjunction and delegates each conjunct to a prior lemma or the supplied bridge hypothesis.
Claim. Assume $F:ℝ→ℝ$ obeys $F(1)=0$, $F(x)=F(x^{-1})$ for all $x>0$, is twice continuously differentiable, the second derivative of $t↦F(e^t)$ at zero equals 1, and $F(xy)+F(x/y)=P(F(x),F(y))$ for $x,y>0$. If $F$ has interaction and the bridge hypothesis holds, then $P$ is entangling and the log-lift $G(t)=F(e^t)$ satisfies $G''=G+1$.
background
The module assembles four gates that together force the hyperbolic branch. The interaction gate requires the consistency relation for P to deviate from additivity at some point. The entanglement gate requires nonzero mixed second difference for P. The curvature gate requires the log-lift G to satisfy the ODE G''=G+1. The d'Alembert gate requires the shifted function H=G+1 to obey the wave identity H(t+u)+H(t-u)=2H(t)H(u). InteractionForcesHyperbolicODE is the packaged claim that interaction plus the structural axioms on F imply the curvature gate. SatisfiesHyperbolicODE is the pointwise statement that the second derivative equals G plus one. IsEntangling asserts existence of points where the mixed difference of P is nonzero. Upstream, the interaction-implies-entanglement lemma shows that HasInteraction F plus consistency and symmetry already force IsEntangling P.
proof idea
The term proof begins with constructor to split the target conjunction. The first conjunct is discharged by direct application of the interaction-implies-entanglement lemma to the consistency, normalization, symmetry and interaction hypotheses. The second conjunct is discharged by direct application of the supplied bridge hypothesis to the complete list of structural assumptions on F and P.
why it matters
This declaration isolates the bridge hypothesis as the exact remaining step toward unconditional inevitability of J and the RCL combiner. It sits between the interaction and entanglement gates on one side and the curvature gate on the other. In the Recognition Science framework it advances the T5 J-uniqueness step by making explicit what must still be shown to exclude the flat branch. The module documentation notes that once interaction excludes the flat solution, the remaining calibration forces G=cosh-1 and therefore F=J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.