complete_forcing_chain
plain-language theorem explainer
The theorem asserts that Jcost equals (x + x^{-1})/2 - 1 for x > 0, satisfies the cosh-add identity under the G reparametrization, and obeys the multiplicative Recognition Composition Law, all without assuming any form for the consistency function P. Researchers deriving physical structure from symmetry and ODE uniqueness would cite this to close the forcing chain unconditionally. The proof is a term-mode refinement that splits the conjunction and discharges each conjunct by simplification or direct appeal to prior lemmas on the identities.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Then $G_J(t+u) + G_J(t-u) = 2 G_J(t) G_J(u) + 2 G_J(t) + 2 G_J(u)$ where $G_J(t) = J(e^t)$, and $J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y)$ for all $x, y > 0$.
background
The module establishes unconditional RCL inevitability: given a function F that is symmetric, normalized at 1, calibrated so that the second derivative of its log reparametrization vanishes at zero, smooth, and consistent under multiplication with some function P, both F and P are forced. Jcost denotes the explicit cost function satisfying these properties. G is the log-coordinate reparametrization defined by G(F)(t) = F(exp t). Upstream, Jcost_cosh_add_identity establishes the additive identity for this Jcost, while J_computes_P shows that the multiplicative consistency applied to J yields the specific bilinear form of P.
proof idea
The proof is a term-mode refinement of the three-way conjunction. The first conjunct is discharged by simplification against the definition of Jcost. The second conjunct is obtained by exact application of the lemma Jcost_cosh_add_identity. The third conjunct is obtained by exact application of J_computes_P.
why it matters
This theorem supplies the highest-closure form of the forcing chain in the DAlembert module, showing that P is computed from J rather than assumed and thereby ruling out all alternatives including non-polynomial ones. It feeds the uniqueness results that appear in downstream statements on P_determined_nonneg and rcl_unconditional. In the Recognition Science framework it realizes T5 J-uniqueness together with the Recognition Composition Law, confirming the self-similar fixed point and the eight-tick octave without regularity restrictions on P.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.