FApply
plain-language theorem explainer
FApply defines the almost-product operator F = 2P - I induced by a covector β and inverse metric kernel hInv in n dimensions. Researchers modeling rank-one updates or golden-ratio operators in the Recognition Science cost framework cite it when deriving algebraic properties of the induced operators. The definition is a direct one-line construction from the normalized projector PApply.
Claim. The almost-product operator $F(λ, h^{-1}, β) : ℝ^n → ℝ^n$ is defined by $Fv = 2Pv - v$, where $P$ is the normalized projector associated to the almost-product operator determined by the inverse metric kernel $h^{-1}$ and covector $β$.
background
The Cost.Ndim.Projector module develops the finite-dimensional operator algebra behind the rank-one tensor picture. A covector β and inverse metric kernel hInv determine a sharp vector β♯, an operator A = h^{-1} g̃ obeying the quadratic law A² = μ A, and the normalized projector P. Vec n denotes the space of n-component real vectors as functions from Fin n to ℝ. PApply constructs the normalized projector explicitly as the scalar multiple of AApply by the inverse of mu. This rests on the vector space definitions supplied in Cost.Ndim.Core.
proof idea
The definition is a one-line wrapper that applies the normalized projector PApply and subtracts the input vector after scaling by 2. The body is the explicit term 2 • PApply lam hInv β v - v. No lemmas are invoked.
why it matters
FApply supplies the almost-product operator that feeds into twelve downstream theorems, including FApply_square establishing F² = I and FApply_GApply connecting F to the golden operator G. It completes the operator algebra package in the module, linking the projector P to the metallic means and quadratic relations. The construction supports derivations involving the golden-ratio fixed point and the eight-tick octave structure in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.