IndisputableMonolith.Cost.Ndim.Projector
The Cost.Ndim.Projector module supplies definitions to raise a one-form β using the inverse metric kernel hInv. It extends the n-dimensional reciprocal cost Hessian whose formulas depend only on the aggregate dot α t in log-coordinates. Researchers constructing dual vectors or index-raising operations in the cost framework would cite these definitions. The module is purely definitional.
claimThe module defines the raising map sending a one-form β to its raised version via the inverse metric kernel $h^{-1}$, together with auxiliary maps (sharp, AApply, PApply, FApply, GApply) and their linearity properties.
background
This module belongs to the Cost.Ndim hierarchy and imports the Hessian module. The upstream doc-comment states: 'The key point is that in log-coordinates the n-dimensional cost depends only on the single weighted aggregate dot α t, so its Hessian'. The projector layer therefore operates on the inverse kernel hInv derived from that Hessian to raise one-forms. Sibling definitions include sharp, AApply, mu, PApply, FApply, GApply, MetallicApply and the linearity lemmas AApply_smul, AApply_add, AApply_neg, AApply_sub, dot_AApply.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the raising operations required by the Metric.lean file referenced in the upstream Hessian module. It completes the public interface for handling the inverse metric kernel in the n-dimensional reciprocal cost setting. No explicit downstream declarations are listed.
scope and limits
- Does not derive or recompute the Hessian itself.
- Does not treat the one-dimensional reduction.
- Does not reference the J-function or phi-ladder.
- Does not contain numerical evaluation code.
depends on (1)
declarations in this module (28)
-
def
sharp -
def
AApply -
def
mu -
def
PApply -
def
FApply -
def
GApply -
def
MetallicApply -
theorem
AApply_smul -
theorem
AApply_add -
theorem
AApply_neg -
theorem
AApply_sub -
theorem
dot_AApply -
theorem
AApply_sq -
theorem
PApply_smul -
theorem
PApply_add -
theorem
PApply_neg -
theorem
PApply_sub -
theorem
PApply_idempotent -
theorem
PApply_FApply -
theorem
FApply_smul -
theorem
FApply_add -
theorem
FApply_neg -
theorem
FApply_sub -
theorem
FApply_square -
theorem
FApply_GApply -
theorem
FApply_MetallicApply -
theorem
GApply_square -
theorem
MetallicApply_square