exp_three_mul
plain-language theorem explainer
The identity exp(3q) equals (exp q) cubed holds for every real q. Researchers converting between rational and hyperbolic expressions for Ricci curvature on the 2D cost Hessian manifold cite it when substituting w = exp q. The proof rewrites the scalar 3q as a sum of three q terms, splits the exponential twice via the addition law, and finishes by ring simplification.
Claim. For every real number $q$, $e^{3q} = (e^q)^3$.
background
The module proves algebraic equivalence between the Z-form and q-form of the Ricci scalar on the Hessian manifold M_x with positive coordinates. The Z-form is rational in Z = x^{2a} y^{2b}; the q-form is hyperbolic in q = a s + b t. The change of variables Z = e^{2q} converts one into the other once both are reduced to the common rational expression ricciW(a, b, w) with w = exp q.
proof idea
The proof is a short tactic sequence. It rewrites 3q as q + (q + q) by ring, applies Real.exp_add to obtain exp(q) * exp(q + q), applies Real.exp_add again to split the inner sum, and closes with ring to confirm the product of three factors equals the cube.
why it matters
This identity is invoked inside ricciZexp_eq_ricciW to replace ricciZexp(a, b, q) by ricciW(a, b, exp q). It therefore completes one algebraic step in the equivalence of the two Ricci expressions. Within the Recognition Science cost geometry it supplies the exponential scaling needed to relate the rational form to the hyperbolic form that appears in the Hessian metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.