Pith. sign in
theorem

rankOneEnd_square

proved
show as:
module
IndisputableMonolith.Foundation.CostProjectorGolden
domain
Foundation
line
60 · github
papers citing
none yet

plain-language theorem explainer

Rank-one endomorphisms of the form A(x)=ℓ(x)v square to a scalar multiple of themselves: A²=ℓ(v)A. Anyone citing the projector-to-golden step, the normalized rank-one projector, or the multi-coordinate cost-Hessian identity needs this algebraic fact. The proof is a short pointwise simplification after extensionality on endomorphisms.

Claim. Let $V$ be a real module, $\ell:V\to\mathbb{R}$ a linear functional, and $v\in V$. Write $A$ for the rank-one endomorphism $A(x)=\ell(x)\,v$. Then $A\circ A=\ell(v)\,A$ as endomorphisms of $V$.

background

This module is the algebraic core of the paper route from Hessian cost geometry to golden operators. It deliberately stops short of a full Hessian-manifold formalization: once a normalized projector $P$ is in hand, the almost-product $F=2P-I$ satisfies $F^2=I$, and the golden operator $G=\varphi P+(1-\varphi)(I-P)$ satisfies $G^2=G+I$.

The rank-one endomorphism used here is the map $x\mapsto\ell(x),v$. That is the algebraic shape of the rank-one Hessian projector construction in the golden-structure route. Composition of endomorphisms is written multiplicatively; scalar action is the usual module smul.

The local goal is the elementary identity $A^2=\mu A$ with $\mu=\ell(v)$. Downstream, nondegeneracy $\mu\neq 0$ turns the normalized operator $\mu^{-1}A$ into a genuine projector.

proof idea

Term-mode proof by extensionality on endomorphisms: it suffices to check equality at each $x\in V$. Unfold the rank-one map, apply the scalar-associativity identity smul_smul, and commute the resulting real multiplications. Both sides evaluate to $\ell(v),\ell(x),v$. No external lemmas beyond the definition and basic scalar arithmetic are required.

why it matters

This is the algebraic projector step quoted from the Hessian-geometry paper: $A^2=\mu A$ with $\mu\neq 0$ implies $P=\mu^{-1}A$ is a projector. It is registered in the module certificate as the rank-one square field, so every golden-structure export from this file depends on it.

Direct parents: the normalized rank-one map is a projector; after normalization it obeys the golden-operator equation $G^2=G+I$; and the multi-coordinate cost-Hessian operator satisfies the same square law (paper Lemma 3.1) by specializing $\ell$ and $v$ to the cost-Hessian form. In the Recognition stack this is the pure algebra that lets reciprocal cost geometry force a golden structure without reopening the $\varphi$-forcing chain (T5–T6).

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.