AApply_sq
plain-language theorem explainer
The rank-one operator A defined by Av_i = λ β♯_i (β · v) satisfies A(Av) = μ Av for every vector v. Researchers on the finite-dimensional projector algebra inside Recognition Science cite this identity when constructing the normalized projector P. The short tactic proof reduces the claim via functional extensionality and the dot_AApply lemma, then finishes with unfolding, rewriting, and ring arithmetic.
Claim. Let $A$ be the operator given by $(Av)_i = λ β^♯_i (β · v)$ and let $μ = λ β · β^♯$. Then $A(Av) = μ Av$ holds for every vector $v$.
background
The Cost.Ndim.Projector module assembles the finite-dimensional operator algebra for the rank-one tensor picture. The operator A is defined coordinatewise as A v i = lam * sharp hInv β i * dot β v, where sharp raises the covector β using the inverse metric kernel hInv and dot is the weighted inner product from Core. The scalar μ is defined as lam * dot β (sharp hInv β) and appears in the quadratic relation A² = μ A highlighted in the module documentation.
proof idea
The proof begins with funext i, obtains the inner-product identity dot β (AApply lam hInv β v) = mu lam hInv β * dot β v by simpa using dot_AApply, unfolds AApply, rewrites with the obtained equality, simplifies the definition of mu, and closes with ring.
why it matters
This identity supplies the quadratic law A² = μ A required by the module documentation for the rank-one tensor picture. It is invoked directly inside the proof of PApply_idempotent to establish idempotence of the normalized projector P once μ is nonzero. The step closes the finite-dimensional operator relations before any lift to the continuous Recognition Science setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.