Jcost_cosh_add_identity
plain-language theorem explainer
The J-cost function satisfies the cosh-add identity under logarithmic reparametrization. Researchers proving the Recognition Composition Law or the T5 uniqueness result cite this lemma. The proof is a direct algebraic verification that substitutes the exponential definitions of G and Jcost then reduces via exp-add and ring tactics.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Define $G(t) := J(e^t)$. Then $G(t+u) + G(t-u) = 2G(t)G(u) + 2G(t) + 2G(u)$ for all real $t, u$.
background
The module supplies helper lemmas for the T5 cost uniqueness argument. The reparametrization $G_F(t) = F(e^t)$ converts the multiplicative Recognition Composition Law into additive form. CoshAddIdentity asserts that a function satisfies the d'Alembert-type relation $G(t+u) + G(t-u) = 2G(t)G(u) + 2G(t) + 2G(u)$. Upstream, Jcost is defined via the yardstick formula on the phi-ladder and the log-coordinate G is shown to equal cosh(t) - 1.
proof idea
The tactic proof introduces t and u, simplifies with the definitions of G and Jcost, invokes Real.exp_add to obtain product and quotient forms of the exponentials, records positivity to clear denominators, then applies field_simp followed by ring to close the identity.
why it matters
This lemma is invoked by Jcost_satisfies_composition_law to confirm Jcost obeys the Recognition Composition Law and by unique_cost_on_pos_from_rcl for the unconditional T5 statement. It also feeds dAlembert_cosh_sum and complete_forcing_chain. The result verifies that the cost function forced by T5 satisfies the required functional equation, linking to the eight-tick octave and the emergence of D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Quantum-well microcavities can squeeze light across tens of GHz
"G_F t = F (exp t); cosh-add identity G_F(t+u)+G_F(t−u) = 2 G_F t G_F u + 2(G_F t + G_F u)"