ricci_scalar_equiv
plain-language theorem explainer
Equivalence of the q-form and Z-form of the Ricci scalar is established for the 2D cost Hessian metric under the change Z = exp(2q). Researchers modeling curvature in multidimensional cost geometry cite this result to confirm coordinate consistency. The proof is a one-line rewrite that reduces both sides to the common intermediate expression ricciW.
Claim. For real numbers $a$, $b$, $q$ with $q ≠ 0$ and $(a + b) cosh q - sinh q ≠ 0$, the Ricci scalar in q-coordinates equals the Ricci scalar in Z-exponential coordinates: $R_q(a, b, q) = R_Z(a, b, q)$.
background
The module treats the Levi-Civita connection on the Hessian manifold M_x in positive coordinates. Curvature is expressed in two ways: the Z-form (rational in Z = x^{2a} y^{2b}) from Section 4.5 and the q-form (hyperbolic in q = a s + b t, Eq. 4.26). Under Z = e^{2q} the identities coth q = (Z+1)/(Z-1) and csch q = 2 Z^{1/2}/(Z-1) convert one expression into the other. ricciQ is the q-form written with sinh and cosh to avoid coth and csch. ricciZexp is the Z-form parametrized by q via Z = exp(2q) and Z^{3/2} = exp(3q). Both prior theorems equate their respective forms to ricciW evaluated at w = exp q.
proof idea
The proof is a one-line wrapper that applies ricciQ_eq_ricciW (under the stated hypotheses on q and the linear combination) followed by ricciZexp_eq_ricciW. Each lemma reduces its side to the common ricciW expression at w = exp q, after which the two sides match directly.
why it matters
This is the main result confirming algebraic equivalence of the two Ricci scalar expressions in the 2D cost Hessian metric, as stated in the module doc-comment and referenced paper sections 4.5 and 4.6.2. It closes the coordinate transformation step required for consistent curvature calculations inside the Recognition Science cost model, where Cost is the native quantity. No downstream theorems are listed, but the equivalence supports any later use of the metric in higher-dimensional or physical applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.