Cost Ndim Ricci Scalar Ricci Scalar Equiv

The Ricci scalar equivalence

The Ricci scalar is a number that describes how much a space curves at a point, independent of how you draw coordinates on it. In the Recognition Science framework, a cost function (a rule that assigns a price to each possible state) defines a geometric space, and its curvature is measured by this scalar. The declaration ricci_scalar_equiv proves that two different ways of writing this curvature, one using coordinates (x, y) and another using a logarithmic coordinate q, actually produce the same value.

This is not a trivial check. The two formulas look completely different: one is a rational function of a variable Z, the other involves hyperbolic functions like sinh and cosh of q. The proof works by showing that both can be rewritten as the same rational expression in w = exp(q), the exponential of q. The machine-checked library of formal theorems then verifies the algebraic equivalence by reducing both sides to a common form and closing the proof with standard algebraic simplification.

In Recognition Science, this establishes that the geometric description of a cost manifold is consistent: the curvature does not depend on which coordinate chart you choose. This is a foundational property for the framework's claim that cost geometry is a well-defined object. The theorem holds under two technical conditions: q must not be zero, and a certain denominator (involving the parameters a and b) must not vanish, which are standard non-degeneracy assumptions for the coordinates to be valid.

What this does not claim is any physical measurement or empirical prediction. It is a purely mathematical statement about two formulas being equal. It does not assert that the Ricci scalar has a specific value, nor that it corresponds to any observed quantity in the physical world. It is a structural result about the internal consistency of the framework's geometry, not a statement about the universe's actual curvature.

/-- **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 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

/-- 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]

/-- **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]

What this page does not claim

This theorem does not assign a numerical value to the Ricci scalar for any specific cost function. It does not connect the Ricci scalar to any measured physical quantity. It does not claim the two coordinate systems are the only ones that work.

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: