dalembert_identity
plain-language theorem explainer
The d'Alembert identity equates J(xy) + J(x/y) to 2J(x) + 2J(y) + 2J(x)J(y) for positive reals x and y. Researchers deriving the Recognition Composition Law or hyperbolic cost bounds cite it to obtain submultiplicativity and to confirm J satisfies the required functional equation. The proof rewrites every Jcost term via its squared-ratio form then reduces the equation by field simplification and ring algebra.
Claim. For all positive real numbers $x$ and $y$, $J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y)$, where $J(z) := (z + z^{-1})/2 - 1$.
background
Jcost is defined by Jcost(z) = (z + z^{-1})/2 - 1. The upstream lemma Jcost_eq_sq rewrites it as Jcost(z) = (z-1)^2/(2z) whenever z ≠ 0. This identity sits in the Cost module, which assembles cost functions from the forcing chain that reaches J-uniqueness at T5 and the Recognition Composition Law.
proof idea
The proof first deduces nonzeroness of x, y, xy and x/y from the positivity assumptions. It applies Jcost_eq_sq to each of the four terms, then invokes field_simp followed by ring to verify the cleared algebraic identity.
why it matters
This supplies the exact Recognition Composition Law for J. It is invoked by Jcost_submult to obtain the inequality J(xy) ≤ 2J(x) + 2J(y) + 2J(x)J(y). Downstream it supports F_forced_to_Jcost by confirming the functional equation, and enters dalembert_cascade and doubling_cascade in StillnessGenerative. The result verifies that J satisfies the RCL required by the eight-tick octave and D = 3 structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.