exp_two_mul
plain-language theorem explainer
The algebraic identity exp(2q) = (exp q)^2 for real q is invoked when converting the Ricci scalar between its rational Z-form and hyperbolic q-form on the Hessian manifold. Researchers reducing curvature expressions in the two-dimensional cost geometry cite this step to equate the parametrizations under Z = e^{2q}. The proof is a one-line wrapper that rewrites the coefficient via ring, applies the exponential addition formula, and normalizes.
Claim. For every real number $q$, $e^{2q} = (e^q)^2$.
background
The module proves algebraic equivalence of two Ricci scalar expressions on the Hessian manifold M_x in positive coordinates. The Z-form is rational in Z = x^{2a} y^{2b} while the q-form is hyperbolic in q = a s + b t, related by the substitution Z = e^{2q}. This yields the conversion identities coth q = (Z+1)/(Z-1) and csch q = 2 Z^{1/2}/(Z-1). The upstream theorem from PrimitiveDistinction supplies the seven-axiom foundation that yields the four structural conditions plus three definitional facts used to construct the cost geometry.
proof idea
One-line wrapper that first rewrites 2q as q + q by ring, then applies Real.exp_add to obtain the product of exponentials, and finishes with ring normalization.
why it matters
The lemma is applied inside ricciZexp_eq_ricciW to show that the Z-exponential form of the Ricci scalar equals ricciW evaluated at w = exp q. It thereby closes the reduction between the two curvature parametrizations referenced in Washburn–Zlatanović–Beltracchi, Sections 4.5 and 4.6.2. In the Recognition framework this algebraic step supports the cost-based derivation of geometric structures that later force D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.