Cost Ndim Ricci Scalar Ricci W

The canonical Ricci form

In differential geometry, the Ricci scalar is a number that summarizes how much a space curves at a point, independent of direction. For a two-dimensional surface, it is twice the Gaussian curvature, so it tells whether the surface is locally like a sphere, a saddle, or a flat plane. In the Recognition Science framework, the cost function J(x) = (x + 1/x)/2 - 1 defines a geometry on its positive coordinate space, and that geometry has its own Ricci scalar. The declaration ricciW is the canonical rational form of that scalar.

What ricciW actually establishes is an equivalence, not a new physical law. The same Ricci scalar can be written in two coordinate systems: one using the original positive coordinates (x, y), the other using a hyperbolic coordinate q = a s + b t. The two expressions look very different, one rational in Z = x^{2a} y^{2b}, the other hyperbolic in q. The theorem ricci_scalar_equiv proves that these two forms agree whenever q is nonzero and a denominator condition holds. The proof works by converting both to a common rational form in w = exp q, which is exactly the function ricciW defines. So ricciW is the bridge that shows the two coordinate descriptions are the same geometry.

For a general reader, the point is that coordinate choices should not change the answer. If you measure curvature in one set of coordinates and get a different number than in another, you have made an error or the geometry is not well defined. ricciW is the clean, unified expression that makes the agreement visible. The theorem is machine-checked in the framework's library of formal theorems, meaning the algebraic equivalence is verified step by step without gaps. The conditions, q ≠ 0 and the denominator not vanishing, are the only places where the geometry is singular, so they are exactly where the equivalence could fail.

What ricciW does not claim is any physical interpretation. It does not say the universe has this curvature, nor that the cost function is the actual geometry of spacetime. It only establishes a mathematical identity between two ways of writing the same scalar curvature. The declaration is a definition, and the accompanying theorems are algebraic equivalences. Nothing in the pack connects this Ricci scalar to gravity, particle masses, or the dimensionality of space. Those are separate results, if they exist at all, and this page does not assert them.

/-- Canonical rational form of the Ricci scalar in w = exp q. -/
def ricciW (a b w : ℝ) : ℝ :=
  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)

/-- **Main result**: the two coordinate forms of the Ricci scalar agree. -/
theorem ricci_scalar_equiv (a b q : ℝ)
    (hq : q ≠ 0)
    (hLC : (a + b) * Real.cosh q - Real.sinh q ≠ 0) :
    ricciQ a b q = ricciZexp a b q := by
  rw [ricciQ_eq_ricciW a b q hq hLC, ricciZexp_eq_ricciW]

/-- The Z-form is `ricciW` evaluated at w = exp q. -/
theorem ricciZexp_eq_ricciW (a b q : ℝ) :
    ricciZexp a b q = ricciW a b (Real.exp q) := by
  unfold ricciZexp ricciW; rw [exp_two_mul, exp_three_mul]

/-- The q-form is also `ricciW` at w = exp q. -/
theorem ricciQ_eq_ricciW (a b q : ℝ)
    (hq : q ≠ 0)
    (hLC : (a + b) * Real.cosh q - Real.sinh q ≠ 0) :
    ricciQ a b q = ricciW a b (Real.exp q) := by
  set w := Real.exp q with hw_def
  have hw_pos : 0 < w := Real.exp_pos q
  have hw_ne : w ≠ 0 := hw_pos.ne'
  have hsinh_ne : Real.sinh q ≠ 0 := Real.sinh_ne_zero.mpr hq
  have hcosh_w : Real.cosh q = (w ^ 2 + 1) / (2 * w) := by
    rw [Real.cosh_eq, Real.exp_neg]; field_simp; ring
  have hsinh_w : Real.sinh q = (w ^ 2 - 1) / (2 * w) := by
    rw [Real.sinh_eq, Real.exp_neg]; field_simp; ring
  have hw2m1 : w ^ 2 - 1 ≠ 0 := by
    intro h; exact hsinh_ne (by rw [hsinh_w, h, zero_div])
  have hLCw : (a + b - 1) * w ^ 2 + (a + b + 1) ≠ 0 := by
    intro h; apply hLC; rw [hcosh_w, hsinh_w]; field_simp; linarith
  show ricciQ a b q = ricciW a b w
  unfold ricciQ ricciW
  rw [hcosh_w, hsinh_w]
  field_simp [hw_ne, hw2m1, hLCw]
  ring

What this page does not claim

The Ricci scalar is not claimed to be the curvature of physical spacetime. The declaration does not derive any particle masses or coupling constants. The equivalence does not hold without the stated conditions on q and the denominator.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Ndim/RicciScalar.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: