Pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.RicciScalar

show as:
view Lean formalization →

This module defines the Ricci scalar in (q, r)-coordinates for the N-dimensional reciprocal cost, using sinh and cosh forms to match Eq. (4.26). Researchers extending scalar cost kernels to curvature expressions in higher dimensions would cite these objects. The module consists of coordinated definitions and equivalence statements built on the Core import.

claimRicci scalar in (q, r)-coordinates, written with $\sinh$ and $\cosh$ to avoid $\coth$ and $\csch$, as in Eq. (4.26).

background

The upstream Core module defines the multi-component reciprocal cost by lifting the scalar kernel through a weighted log aggregate. This module specializes that construction to the Ricci scalar in (q, r)-coordinates within the cost domain. The local theoretical setting is the N-dimensional extension of the Recognition Science cost framework, where hyperbolic rewriting supports clean algebraic handling of the scalar expression.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the N-dimensional Ricci scalar objects that feed the cost hierarchy and support curvature-related derivations in the Recognition framework. It fills the coordinate-specific form required by Eq. (4.26) and connects to the broader forcing chain through the Core definitions, even though the current graph shows no direct used_by edges.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)