ricciW
plain-language theorem explainer
The definition ricciW supplies the canonical rational expression for the Ricci scalar of the 2D cost Hessian metric when written in the variable w = exp q. Researchers working on multidimensional cost geometry cite it as the common target that equates the Z-form and q-form curvature expressions. The definition is obtained by direct algebraic substitution of the identities coth q = (Z+1)/(Z-1) and csch q = 2 Z^{1/2}/(Z-1) into the curvature formula, producing a single rational function in w.
Claim. The canonical rational form of the Ricci scalar is given by $4(a+b)w^3 ((a+b-2)w^2 + (a+b+2)) / ((w^2-1)^2 ((a+b-1)w^2 + (a+b+1))^2)$ where $w = e^q > 0$.
background
The module treats the Ricci scalar equivalence for the 2D cost Hessian metric on the manifold M_x in positive coordinates. The Levi-Civita connection produces a Ricci scalar that admits a Z-form, rational in Z = x^{2a} y^{2b}, and a q-form, hyperbolic in q = a s + b t. 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, allowing both to be reduced to a common rational function in w = exp q.
proof idea
This declaration is a direct definition that encodes the rationalized expression obtained after the hyperbolic substitutions. No lemmas are applied inside the definition itself. The downstream theorems unfold ricciW and close the equalities with field_simp and ring.
why it matters
ricciW serves as the common target for the theorems ricciZexp_eq_ricciW and ricciQ_eq_ricciW, which establish that both the Z-form and q-form equal this expression at w = exp q. It thereby completes the algebraic equivalence between the two representations of the Ricci scalar, as described in the module documentation referencing Sections 4.5 and 4.6.2 of Multidimensional Cost Geometry. In the Recognition Science framework this supports curvature calculations underlying the forcing chain and the emergence of D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.