PApply_FApply
plain-language theorem explainer
The normalized projector P satisfies P(F v) = P v where F = 2P - I is the induced almost-product operator. Researchers on the finite-dimensional cost algebra cite this when establishing involution properties of F. The proof reduces componentwise by substituting the definition of F, invoking linearity and idempotence of P, then simplifying the arithmetic expression.
Claim. Let $P = mu^{-1} A$ be the normalized projector associated to the operator $A$ determined by scalar $lam$, inverse kernel $hInv$, and covector $beta$, and let $F = 2P - I$ be the induced almost-product operator. Then $P(Fv) = Pv$ for every vector $v$, provided the scalar coefficient $mu$ is nonzero.
background
The Cost.Ndim.Projector module packages the finite-dimensional operator algebra behind the rank-one tensor picture. A covector beta and inverse metric kernel hInv determine a sharp vector beta sharp, an operator A = h inverse tilde g satisfying the quadratic law A squared equals mu A, the normalized projector P, and the almost-product operator F = 2P minus I. Vec n denotes n-component real vectors as functions from Fin n to real numbers. The scalar mu equals lam times the dot product of beta with its sharp image under hInv.
proof idea
The tactic proof applies extensionality on components. It rewrites FApply v as 2 P v minus v via the definition, invokes PApply_sub to produce an expression with P(2 P v) minus P v, uses PApply_smul to factor the scalar 2, applies PApply_idempotent to replace P(P v) by P v, and finishes with simp followed by ring to simplify the resulting arithmetic.
why it matters
This identity is invoked in the proof of FApply_square, which establishes that F is an involution satisfying F(F v) equals v. It fills an intermediate step in the operator algebra of the rank-one tensor picture. In the Recognition Science framework the projector and almost-product structures support quadratic relations and fixed-point constructions tied to the self-similar operator and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.