PApply_idempotent
plain-language theorem explainer
The normalized projector P derived from the operator A satisfies P squared equals P whenever the scaling coefficient mu is nonzero. Researchers modeling finite-dimensional cost operators in Recognition Science cite this to confirm projector behavior in the rank-one tensor setting. The proof is a direct term-mode simplification that substitutes the definition of P and invokes the quadratic law A squared equals mu A.
Claim. Let $A$ be the linear operator on vectors in $n$ dimensions induced by scalar parameter $lam$, inverse kernel $hInv$, and covector $beta$, with associated scalar $mu = lam$ times the weighted dot product of $beta$ with its sharp vector. Let $P$ denote the normalized projector $Pv = mu^{-1} Av$. Then $P(Pv) = Pv$ for every vector $v$, provided $mu neq 0$.
background
The Cost.Ndim.Projector module constructs the finite-dimensional operator algebra for the rank-one tensor picture. A covector $beta$ and inverse metric kernel $hInv$ determine a sharp vector $beta^sharp$, an operator $A$, the quadratic relation $A^2 = mu A$, and the normalized projector $P$. The abbreviation Vec $n$ stands for coordinate functions from Fin $n$ to real numbers. The scalar $mu$ is defined as $lam$ times the dot product of $beta$ with sharp $hInv$ $beta$, while $P v$ equals $mu^{-1}$ times $A v$.
proof idea
The proof is a one-line term-mode wrapper. It applies function extensionality to obtain a pointwise statement, then invokes the simplifier on the definition of PApply together with the scalar-multiplication rule AApply_smul, the quadratic law AApply_sq, the hypothesis that $mu neq 0$, and commutativity of multiplication.
why it matters
This result establishes idempotence of the normalized projector P, a basic algebraic property required for the almost-product operators in the same module. It is invoked directly by the downstream theorem PApply_FApply. In the Recognition Science setting the identity supports the finite-dimensional realization of the cost structure that underlies the forcing chain and the rank-one tensor picture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.