J_computes_P
plain-language theorem explainer
J_computes_P establishes that the Recognition cost J satisfies the multiplicative d'Alembert identity, which directly computes the composition map P(u,v) = 2uv + 2u + 2v without any polynomial hypothesis. Researchers closing the inevitability argument for physical constants cite it to show P is forced once F is fixed to J. The proof reduces the claim to the cosh-add identity via logarithmic change of variables and algebraic substitution.
Claim. For all positive reals $x,y>0$, $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, where $J(z)=(z+z^{-1})/2-1$.
background
The Unconditional module proves RCL inevitability with no assumption on P: any symmetric normalized smooth F satisfying multiplicative consistency must equal J, after which P is computed. Jcost denotes this forced function $J(z)=(z+z^{-1})/2-1$. The auxiliary G reparametrizes via $G(t)=J(e^t)$, converting the multiplicative law into an additive cosh identity. Upstream Jcost_cosh_add_identity supplies exactly that additive form $G(t+u)+G(t-u)=2G(t)G(u)+2G(t)+2G(u)$.
proof idea
The tactic proof sets $t=Real.log x$, $u=Real.log y$, recovers $x=exp t$ and $y=exp u$ by exp_log, invokes Jcost_cosh_add_identity to obtain the G-identity, substitutes the exponential expressions for $xy$ and $x/y$, then applies ring to reach the target polynomial form.
why it matters
It supplies the explicit P used in consistency_defines_composition and ultimate_inevitability to finish the unconditional forcing chain. The declaration realizes the module claim that P is computed rather than assumed once F equals J. In the Recognition framework it completes the step from J-uniqueness (T5) to the explicit RCL, supporting derivations of constants such as alpha within the observed band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.