Pith. sign in
module module moderate

IndisputableMonolith.Foundation.JHessianGoldenMulti

show as:
view Lean formalization →

Defines the Hessian geometry of the recognition cost J on the multi-coordinate positive orthant: the scalar Hessian factor, the associated bilinear form, and the rank-one cost Hessian operator. Shows that operator squares to a multiple of itself and that its normalization is a projector. Cited by anyone building golden/metallic almost-product structure from reciprocal cost geometry.

claimOn the positive orthant with recognition cost $J$, introduce the inner product model, the scalar Hessian density of $J$, the bilinear cost Hessian form $H_J$, and the associated endomorphism (cost Hessian operator). Prove $H_J$ is positive on the comparison direction, the operator squares consistently with rank one, and the normalized operator is a projector $P$ with $P^2=P$.

background

Recognition Science forces the cost $J(x)=(x+x^{-1})/2-1$ (T5) and builds geometry from its Hessian on reciprocal coordinates. The companion module CostProjectorGolden records that a normalized rank-one Hessian projector $P$ yields the almost-product operator $F=2P-I$ with $F^2=I$, and thence the golden operator of the paper on Hessian manifolds.

This module supplies the multi-variable Hessian data those projectors act on: an inner-product pairing on tangent vectors, the scalar second-derivative factor of $J$, the symmetric bilinear form $H_J$, and the endomorphism obtained by raising an index. Constants (including the RS tick) are imported only for ambient units; the algebra is local to the cost Hessian.

Sibling declarations package the form evaluations, positivity on the distinguished comparison direction, non-vanishing, the square identity for the operator, and the normalized-projector theorem that hands $P$ to the golden stack.

proof idea

Definition-heavy module with short algebraic lemmas. Inner form and cost Hessian form are introduced by explicit formulae; apply lemmas are definitional unfoldings. Positivity of the scalar Hessian and of the form on the comparison direction follows from the known convexity/positivity profile of $J$ on $\mathbb{R}_{>0}$. The operator is the metric dual of the form; its square identity is rank-one linear algebra. Normalization then yields $P^2=P$ by direct expansion, the exact algebraic hypothesis CostProjectorGolden needs for $F=2P-I$.

why it matters in Recognition Science

Closes the concrete Hessian side of the golden-structure bridge: without a verified cost Hessian operator and its normalized projector, the forcing path from $J$-uniqueness (T5) to golden/metallic almost-product operators on Hessian manifolds stays formal. Upstream CostProjectorGolden states that once $P^2=P$, $F=2P-I$ satisfies $F^2=I$ and produces the golden operator; this module is the source of that $P$ from reciprocal cost geometry.

No downstream edges are recorded yet in the mirror graph, so the module presently terminates the local foundation chain rather than feeding a named parent theorem. It is the natural attachment point for multi-coordinate extensions of the eight-tick and $D=3$ forcing steps that need Hessian projectors rather than scalar $J$ alone.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)