FApply_square
plain-language theorem explainer
The almost-product operator F, defined via F(v) = 2P(v) - v with P the normalized projector from covector β and inverse kernel hInv, satisfies F(F(v)) = v for every vector v when the scalar μ is nonzero. Researchers deriving commutation rules for golden and metallic operators in the finite-dimensional cost algebra cite this result. The proof extends the claim coordinatewise, invokes the auxiliary identity P(F(v)) = P(v), and reduces via direct substitution from the definition of F.
Claim. Let $F(v) = 2P(v) - v$, where $P$ denotes the normalized projector $P(v) = μ^{-1} A(v)$ associated to covector $β$ and inverse metric kernel $h^{-1}$, and $μ$ is the scalar satisfying $A^2 = μ A$. Then $F(F(v)) = v$ for all vectors $v$, provided $μ ≠ 0$.
background
In the module on cost-induced projectors, a covector β and inverse metric kernel hInv determine an operator A satisfying the quadratic relation A² = μ A, where μ = λ ⋅ (β · β♯) and β♯ is the sharp vector. The normalized projector is P = μ⁻¹ A, and the almost-product operator is introduced as F = 2P - I. Vectors are realized as coordinate functions Fin n → ℝ. The upstream lemma PApply_FApply states that P(F(v)) = P(v) under the same nonvanishing assumption on μ.
proof idea
The proof extends the vector equality to each coordinate i. It applies the lemma PApply_FApply to obtain P(F(v)) = P(v) at that coordinate. Substituting into the definition of F then yields the expression 2P(v) - F(v), which reduces immediately to v by the definition of F.
why it matters
This theorem shows that the almost-product operator F is an involution, F² = I. It is invoked directly in the proofs of FApply_GApply and FApply_MetallicApply, which establish the algebraic relations between F and the golden and metallic operators. Within the Recognition framework the result supplies a basic composition law for the finite-dimensional projector algebra derived from the cost function, supporting the self-similar structures that appear in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.