Pith. sign in
module module moderate

IndisputableMonolith.Cost.Ndim.Connections

show as:
view Lean formalization →

This module defines the Kronecker delta on Fin n together with flat and pulled connection structures that extend the N-dimensional reciprocal cost. Researchers extending the scalar cost kernel to multi-index settings would cite these objects. The module contains only definitions and no proofs.

claimThe Kronecker delta $\delta_{ij}$ on the finite index set $\mathrm{Fin}\,n$, together with the flat connection on the $x$-component and the pulled connection on the $t$-component of the weighted log-aggregate cost.

background

The imported Core module defines the multi-component reciprocal cost by lifting the scalar kernel through a weighted log aggregate. The present module adds the standard basis object (Kronecker delta on Fin n) and the auxiliary connection maps needed to handle projective equivalence and diagonal/off-diagonal components in that aggregate.

The local theoretical setting is the cost domain, where these structures prepare the ground for N-dimensional extensions of the J-cost without yet invoking the phi-ladder or the forcing chain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the connection and delta objects required by any parent theorem that lifts the scalar reciprocal cost to N dimensions. It fills the geometric layer between the Core kernel and later multi-component calculations in the cost domain, even though no downstream uses are yet recorded.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)