IndisputableMonolith.Cost.Ndim.Projector
This module supplies the sharp raising map and related application operators that convert one-forms to vectors via the inverse metric kernel hInv extracted from the n-dimensional Hessian. Researchers constructing the geometry of the reciprocal cost function in log-coordinates cite these definitions when building the metric structure for the phi-ladder and forcing chain. The module is organized as a set of targeted definitions and algebraic lemmas implementing index raising and linear applications without a single overarching theorem.
claimThe module defines the raising operation $β^♯ = hInv(β)$ together with the associated maps AApply, PApply, FApply, GApply and MetallicApply that apply the inverse kernel to one-forms and vectors in the n-dimensional cost geometry.
background
The module imports the Hessian formulas for the n-dimensional reciprocal cost, which in log-coordinates depends only on the single weighted aggregate dot α t. This supplies the metric kernel whose inverse hInv is used to raise one-forms. The local setting is the n-dimensional extension of the J-cost function, where the Hessian furnishes the inner product structure needed for the Recognition Composition Law and the eight-tick octave.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The definitions supply the geometric raising and application operators required by the n-dimensional cost constructions that feed the unified forcing chain (T0-T8) and the mass formula on the phi-ladder. They close the interface between the Hessian module and downstream metric-dependent lemmas in the Cost.Ndim hierarchy.
scope and limits
- Does not derive the explicit form of the Hessian eigenvalues.
- Does not address coordinate changes outside log-coordinates.
- Does not treat the Berry creation threshold or Z_cf directly.
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