ricciQ_eq_ricciW
plain-language theorem explainer
The theorem establishes algebraic agreement between the hyperbolic q-coordinate form of the Ricci scalar on the 2D cost Hessian metric and its rational w-coordinate form at w = exp q. Researchers modeling curvature in Recognition Science cost geometry would cite the result when switching parametrizations. The proof substitutes w = exp q, rewrites cosh and sinh via exponential identities, verifies non-vanishing conditions, then reduces both sides with field_simp and ring.
Claim. Let $a, b, q$ be real numbers with $q$ nonzero and $(a + b) cosh q - sinh q$ nonzero. The hyperbolic expression for the Ricci scalar in q-coordinates equals the rational expression in exponential coordinates evaluated at $w = e^q$.
background
The module treats the Levi-Civita connection on the Hessian manifold M_x in positive coordinates. Its Ricci scalar admits a q-form (hyperbolic in q = a s + b t) and a Z-form (rational in Z = x^{2a} y^{2b}). The substitution 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 upstream definition ricciQ is the hyperbolic expression (a + b) * ((a + b) * cosh q - 2 * sinh q) / (2 * (sinh q)^2 * ((a + b) * cosh q - sinh q)^2). The upstream definition ricciW is the rational form 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). The local setting is the 2D cost geometry derived from the J-cost structure.
proof idea
The tactic proof sets w := exp q and records that w is positive and nonzero. It derives cosh q = (w^2 + 1)/(2 w) and sinh q = (w^2 - 1)/(2 w) from the exponential definitions of sinh and cosh. Two auxiliary non-vanishing statements are proved from the input hypotheses. The definitions of ricciQ and ricciW are unfolded, the hyperbolic expressions are substituted, and field_simp followed by ring closes the equality.
why it matters
The result supplies the bridge used by the parent theorem ricci_scalar_equiv to conclude that the q-form and Z-form Ricci scalars coincide. It fills the algebraic step required for coordinate independence of the Ricci scalar in the 2D Hessian metric of multidimensional cost geometry, as stated in the module documentation referencing Sections 4.5 and 4.6.2 of the paper. Within the Recognition Science framework it confirms consistency of curvature expressions built from the phi-forcing and J-cost structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.