gates_connected
plain-language theorem explainer
The theorem asserts that J-cost satisfies interaction, the RCL combiner Prcl is entangling, and Gcosh satisfies the hyperbolic ODE G'' = G + 1. Researchers tracing the d'Alembert bridge in Recognition Science cite it to show interaction as the root gate that forces entanglement then hyperbolic curvature. The proof is a direct term-mode conjunction of three upstream lemmas.
Claim. The J-cost function satisfies the interaction property, the RCL combiner $P(u,v) = 2uv + 2u + 2v$ is entangling (mixed second difference nonzero), and $G(t) = 2^{-1}(e^t + e^{-t}) - 1$ satisfies the ODE $G''(t) = G(t) + 1$.
background
The Analytic Bridge module derives the d'Alembert functional equation from structural consistency when interaction is present. HasInteraction asserts that the combiner for J-cost is non-separable. IsEntangling requires that the mixed second difference of a combiner P is nonzero at some point, equivalently that P is not of the form alpha(u) + beta(v). SatisfiesHyperbolicODE requires G''(t) = G(t) + 1 for all t, which selects hyperbolic solutions over flat ones.
proof idea
The proof is a one-line term wrapper that applies the three lemmas Jcost_hasInteraction, Prcl_entangling, and Gcosh_satisfies_hyperbolic to discharge the conjunction.
why it matters
This declaration completes the gate chain in the Analytic Bridge: interaction implies entanglement, entanglement implies the hyperbolic ODE, and the ODE plus d'Alembert uniqueness recovers F = J. It therefore supports the module's Bridge Theorem that consistency plus interaction forces the d'Alembert structure with no third option. In the Recognition framework it reinforces T5 J-uniqueness and the RCL as the mechanism that selects the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.