MetallicApply_square
plain-language theorem explainer
MetallicApply obeys the quadratic recurrence M(Mv) = p Mv + q v whenever mu is nonzero and p squared plus four q is nonnegative. Workers on the finite-dimensional projector algebra in Recognition Science cite this identity to confirm closure of the metallic family. The proof expands the definition, applies the companion lemma FApply_MetallicApply, and reduces the resulting scalar equations with nlinarith.
Claim. Let $M_{p,q}$ denote the metallic operator $M_{p,q} v = (p/2) v + (√(p² + 4q)/2) F v$, where $F$ is the almost-product operator induced by covector β and inverse kernel hInv. Then $M_{p,q}(M_{p,q} v) = p M_{p,q} v + q v$, provided μ(λ, hInv, β) ≠ 0 and p² + 4q ≥ 0.
background
The module develops the finite-dimensional operator algebra for cost-induced projectors. A covector β and inverse metric kernel hInv determine the sharp vector β♯, the operator A, the quadratic law A² = μ A with scalar μ = λ ⋅ (β · β♯), the normalized projector P, and the almost-product operator F = 2P − I. MetallicApply is the one-parameter family of operators built from the same F: M_{p,q} v = (p/2) v + (√(p² + 4q)/2) F v. The upstream theorem FApply_MetallicApply supplies the commutation relation F(M v) = (p/2) F v + (√(p² + 4q)/2) v that is invoked directly in the argument.
proof idea
The proof extends componentwise. It first obtains an auxiliary identity by substituting the definition of MetallicApply into FApply_MetallicApply. Two short nlinarith steps verify the square-root scaling relations (√r ⋅ √r = r and (√r/2)² = r/4). After simplification the component equality reduces to a final nlinarith application on the expanded scalar terms.
why it matters
The result shows that every metallic operator satisfies the same quadratic characteristic equation X² − p X − q = 0 as the underlying almost-product operator, thereby closing the algebra of the metallic family inside the rank-one tensor picture. It supports the construction of self-similar operators compatible with the phi-ladder and eight-tick octave in the Recognition Science framework. No downstream uses are recorded and no open questions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.