FApply_add
plain-language theorem explainer
Additivity of the induced almost-product operator F holds for vector sums in finite dimensions. Researchers developing the projector algebra in Recognition Science cite this when verifying linearity of cost-induced operators. The proof reduces componentwise via the additivity of the underlying projector P followed by ring normalization.
Claim. Let $F$ denote the operator defined by $F(v) = 2P(v) - v$, where $P$ is the projector determined by scalar parameter $λ$, inverse metric kernel $h^{-1}$, and covector $β$. Then $F(v + w) = F(v) + F(w)$ for all vectors $v, w$ in the $n$-dimensional real space.
background
The Cost.Ndim.Projector module develops the finite-dimensional operator algebra for the rank-one tensor picture. A covector $β$ and inverse metric kernel $hInv$ determine the sharp vector, the operator $A = h^{-1} g̃$, the quadratic law $A^2 = μ A$, and the normalized projector $P$. The almost-product operator $F$ is introduced as $F = 2P - I$ to capture the induced structure on vectors.
proof idea
The proof applies the extensionality tactic to equate the vectors componentwise. It then simplifies the definition of $F$ by substituting the additivity theorem for $P$, and concludes with the ring tactic to normalize the resulting scalar expressions.
why it matters
This theorem is invoked by the derivations of the interaction rules with the golden operator and the metallic operator, as well as the subtraction property for $F$. It supplies the additive structure required for the almost-product algebra in the cost domain, supporting the finite-dimensional model of the Recognition Science forcing chain and the associated operator identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.