ricciZexp
plain-language theorem explainer
This definition supplies the explicit rational expression for the Ricci scalar of the 2D cost Hessian metric when written in the exponential coordinate q with the auxiliary variable Z set to exp(2q). Analysts establishing coordinate equivalence for curvature scalars in J-cost manifolds cite it when matching the rational Z-form against the hyperbolic q-form. The definition is obtained by direct algebraic substitution of the exponential relations Z = exp(2q) and the cubic scaling exp(3q) into the base rational curvature formula.
Claim. The Ricci scalar in the (x, y)-coordinates parametrized by q via Z = exp(2q) equals $4(a + b) e^{3q} ((a + b - 2)Z + (a + b + 2)) / ((Z - 1)^2 ((a + b - 1)Z + (a + b + 1))^2)$ where $Z = e^{2q}$.
background
The module treats algebraic equivalence of the two coordinate expressions for the Ricci scalar of the Levi-Civita connection on the Hessian manifold M_x in positive coordinates. One expression is rational in Z = x^{2a} y^{2b}; the other is hyperbolic in q = a s + b t. The substitution Z = e^{2q} together with the elementary identities coth q = (Z + 1)/(Z - 1) and csch q = 2 sqrt(Z)/(Z - 1) converts one form into the other.
proof idea
The definition directly transcribes the rational form obtained after substituting Z = exp(2q) and collecting the factor exp(3q) for the cubic term. It applies the elementary identities exp(2q) for Z and exp(3q) for the numerator scaling, with no further simplification required at this stage.
why it matters
This definition supplies the Z-exp form required by the main equivalence theorem that asserts the q-form and Z-form of the Ricci scalar coincide under the stated non-degeneracy conditions. It thereby closes the algebraic step in the multidimensional cost geometry development. The construction is consistent with the J-cost convexity and the local eight-tick dynamics developed in the upstream structure of J-cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.