IndisputableMonolith.Cost.Ndim.Connections
The Connections module supplies the Kronecker delta on Fin n together with flat and pulled connection predicates for N-dimensional reciprocal cost. Researchers extending the scalar J-cost to vector or matrix settings cite these definitions when building dimension-dependent cost functions. The module proceeds entirely by direct definitions and immediate properties imported from the Core module.
claimThe Kronecker delta function $delta : Fin n to Fin n to R$ is supplied, along with the predicates xFlatConnection and tPulledConnection on cost maps, and the relation ProjectivelyEquivalentToZeroAt.
background
The module imports IndisputableMonolith.Cost.Ndim.Core, whose doc-comment states that it defines the multi-component reciprocal cost by lifting the scalar kernel through a weighted log aggregate. Within this setting the Kronecker delta on Fin n serves as the standard projection operator for the N-dimensional cost components. The additional declarations introduce xFlatConnection, tPulledConnection, and the projective-equivalence relation that compare cost maps at specific points or along diagonals.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the basic connection vocabulary required by any N-dimensional extension of the reciprocal cost, thereby supporting later results that recover the three-dimensional case (D = 3) from the forcing chain. No direct downstream theorems are listed, indicating that the definitions remain available for use in higher-level Cost.Ndim constructions.
scope and limits
- Does not prove any non-trivial identities beyond the definitions themselves.
- Does not address convergence or boundedness of the lifted cost functions.
- Does not connect to the phi-ladder or mass formula.