Pith. sign in
module module moderate

IndisputableMonolith.Cost.Ndim.DAlembert

show as:
view Lean formalization →

This module extends the N-dimensional reciprocal cost framework to a d'Alembertian form. It imports the core lifting of the scalar kernel via weighted log aggregate from Cost.Ndim.Core and introduces the sibling definitions JcostN_dAlembert and JcostN_submult. The module supplies the wave-operator specialization needed for multi-component costs in the Recognition setting. It contains only definitions.

claim$J_{ m cost,N}^{d'Alembert}$ and the associated submultiplicative map, obtained by lifting the scalar kernel through a weighted log aggregate in $N$ dimensions.

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 d'Alembertian case within the Cost domain of Recognition Science. The setting uses the same J-cost kernel and phi-ladder conventions as the parent N-dimensional theory.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the d'Alembertian specialization of N-dimensional cost that feeds the broader Recognition Science cost theory and the forcing-chain constructions in IndisputableMonolith.Foundation.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (2)