FApply_sub
plain-language theorem explainer
The almost-product operator F = 2P - I induced by covector β and inverse kernel hInv satisfies F(v - w) = F(v) - F(w) for vectors in R^n. Researchers building the finite-dimensional operator algebra for Recognition Science cost models cite this when verifying linearity of the golden operator. The proof reduces subtraction to addition plus negation via extensionality and the corresponding sibling lemmas.
Claim. Let $F = 2P - I$ be the almost-product operator induced by inverse metric kernel $h^{-1}$ and covector $β$. Then $F(v - w) = F(v) - F(w)$ for all $v, w$ in the space of $n$-component real vectors.
background
The Cost.Ndim.Projector module develops the finite-dimensional operator algebra for the rank-one tensor picture. A covector β together with inverse metric kernel hInv determines the sharp vector, the operator A = h^{-1} g̃, its quadratic law, and the normalized projector P. The induced almost-product operator is defined by F = 2P - I. Vectors are coordinate functions Vec n := Fin n → ℝ.
proof idea
The term proof applies function extensionality to obtain pointwise equality. It rewrites the left-hand side via sub_eq_add_neg and invokes the additivity lemma FApply_add together with the negation lemma FApply_neg to match the right-hand side.
why it matters
This lemma verifies linearity of the almost-product operator F, completing the basic algebraic properties needed for the golden and metallic operators in the rank-one tensor picture. It supports the projector algebra described in the module documentation and feeds into quadratic relations and normalized projectors used downstream in the cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.