pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.RicciScalar

show as:
view Lean formalization →

This module defines the Ricci scalar for the N-dimensional reciprocal cost in (q,r)-coordinates using sinh and cosh. It would be cited by researchers extending the geometric cost model beyond scalar cases. The module supplies component definitions and equivalence lemmas that keep expressions regular.

claimThe Ricci scalar in (q,r)-coordinates is given by an expression using sinh and cosh that equals the form in Eq. (4.26) and avoids coth/csch singularities.

background

The module imports IndisputableMonolith.Cost.Ndim.Core, whose doc states it defines the multi-component reciprocal cost by lifting the scalar kernel through a weighted log aggregate. It introduces auxiliary objects ricciQ, ricciZexp, ricciW and proves relations such as ricciZexp_eq_ricciW and ricci_scalar_equiv. The local setting is the N-dimensional extension of the reciprocal cost kernel in Recognition Science.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the explicit Ricci scalar form required by the N-dimensional cost geometry. It feeds constructions that appear in higher-level statements on dimensional forcing and cost minimization within the Recognition Science framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)