InteractionForcesHyperbolicODE
plain-language theorem explainer
InteractionForcesHyperbolicODE defines the proposition that any F satisfying F(1)=0, inversion symmetry for positive arguments, C^2 smoothness, normalized second derivative of its log-lift at zero, the functional relation with some P, and HasInteraction must have its log-lift G(t)=F(e^t) obey the hyperbolic ODE G''=G+1. Recognition Science researchers working on the inevitability theorem cite it as the explicit bridge between the interaction gate and the curvature gate. The declaration is introduced as a direct definition packaging the combined
Claim. Let $F:ℝ→ℝ$ and $P:ℝ→ℝ→ℝ$. If $F(1)=0$, $F(x)=F(x^{-1})$ for all $x>0$, $F$ is twice continuously differentiable, the second derivative at $t=0$ of $t↦F(e^t)$ equals 1, $F(xy)+F(x/y)=P(F(x),F(y))$ for all $x,y>0$, and $F$ has interaction (i.e., $F(xy)+F(x/y)≠2F(x)+2F(y)$ for some $x,y>0$), then $G(t):=F(e^t)$ satisfies $G''(t)=G(t)+1$ for all real $t$.
background
This definition sits in the TriangulatedProof module, which assembles the four gates toward full inevitability. HasInteraction F (from NecessityGates) means there exist x,y>0 with F(xy)+F(x/y)≠2F(x)+2F(y). SatisfiesHyperbolicODE G (from CurvatureGate) means ∀t, the second derivative of G equals G plus one. The module document describes the quadrilateral structure in which interaction excludes the flat branch, forcing the hyperbolic solution G=cosh−1 once the other gates are applied.
proof idea
The declaration is a definition that directly encodes the bridge hypothesis as a universal statement over F and P. It combines the listed structural premises with HasInteraction to conclude SatisfiesHyperbolicODE on the log-lift. No lemmas are invoked and no tactics are used; the body is the explicit packaging of the hypothesis.
why it matters
This supplies the central hypothesis consumed by full_inevitability_triangulated, which concludes that both F and P are uniquely forced. It corresponds to the bridge step in the paper's Option A formulation of the inevitability theorem, where interaction plus axioms force the hyperbolic branch and thereby F=J. It leaves open the unconditional derivation of the ODE from the Recognition Composition Law and self-reference axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.