ricciQ
plain-language theorem explainer
The declaration supplies the explicit algebraic form of the Ricci scalar for the 2D Hessian cost metric expressed in hyperbolic q-coordinates with Z = exp(2q). Workers on multidimensional cost geometry cite it when converting between rational Z-forms and hyperbolic expressions to compare curvature invariants. It is introduced as a direct definition that rewrites the curvature using sinh and cosh to sidestep coth and csch singularities.
Claim. The Ricci scalar in (q,r)-coordinates is $R(a,b,q) = (a+b) [(a+b) cosh q - 2 sinh q] / [2 (sinh q)^2 ((a+b) cosh q - sinh q)^2]$, where a,b parametrize the underlying Hessian metric and q satisfies Z = exp(2q).
background
The module treats the Levi-Civita connection on the Hessian manifold M_x in positive coordinates. Its Ricci scalar admits two equivalent expressions: a rational Z-form in Z = x^{2a} y^{2b} and a hyperbolic q-form in q = a s + b t. The change of variables Z = e^{2q} converts one into the other via the identities coth q = (Z+1)/(Z-1) and csch q = 2 Z^{1/2}/(Z-1). The present definition encodes the q-form directly in sinh and cosh, as stated in the module doc-comment: 'The Ricci scalar in (q,r)-coordinates, Eq. (4.26). Written with sinh/cosh to avoid coth/csch.' Upstream anchor-Z definitions supply the integer sector map that fixes the parameters a,b in the physical cost model.
proof idea
This is a definition that directly encodes the closed-form expression for the q-coordinate Ricci scalar. No tactics or lemmas are applied; the body is the explicit rational function in a,b,q obtained by substituting the hyperbolic identities into the curvature formula.
why it matters
The definition supplies the q-form (Eq. 4.26) that downstream theorems ricciQ_eq_ricciW and ricci_scalar_equiv equate to the Z-form, thereby closing the coordinate equivalence for the 2D cost Hessian metric. It fills the Section 4.5 slot in the Recognition framework's curvature analysis and connects to the Recognition Composition Law through the underlying phi-ladder mass formulas. It touches the open question of extending the equivalence to D>2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.