IndisputableMonolith.Cost.Ndim.Projector
The Projector module supplies definitions for raising a one-form β via the inverse metric kernel hInv within n-dimensional reciprocal cost models. Researchers extending the Hessian formulas to higher dimensions in the Recognition Science cost framework would cite it. The module consists of multiple definitions and algebraic lemmas for operators such as sharp and the various Apply functions, with no central theorem.
claimThe module defines the raising map $\beta^\sharp := h_{\rm Inv} \cdot \beta$ together with associated linear operators (sharp, $\mu$, AApply, PApply, FApply, GApply) and their algebraic properties (smul, add, neg, sub, dot).
background
This module sits inside the Cost.Ndim namespace of the Recognition Science framework and imports the Hessian module. The upstream Hessian documentation states that in log-coordinates the n-dimensional cost depends only on the single weighted aggregate dot α t, so its Hessian admits a closed-form expression. The Projector module therefore supplies the index-raising machinery (one-form to vector) needed to manipulate those Hessian expressions.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the raising operation required by the n-dimensional Hessian formulas referenced in Metric.lean. It therefore supports the extension of the one-dimensional cost structure to the full n-dimensional case inside the Recognition Science cost domain.
scope and limits
- Does not contain any theorems or proofs.
- Does not implement the Hessian formulas themselves.
- Does not export results outside the Cost.Ndim namespace.
- Limits scope to raising one-forms and basic linear-algebra identities on the resulting operators.
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