PApply
plain-language theorem explainer
The normalized projector P = A/μ associated to the rank-one operator A in the finite-dimensional cost algebra. Researchers deriving almost-product operators or idempotence properties in the rank-one tensor model would cite this definition. It is a direct one-line scaling of AApply by the reciprocal of mu.
Claim. The normalized projector associated to the rank-one operator is the linear map $P v = μ^{-1} A v$, where $A v_i = λ (β^♯)_i (β · v)$ with $β^♯ = h^{-1} β$ and $μ = λ β · β^♯$.
background
Vec n denotes n-component real vectors as maps Fin n → ℝ. AApply builds the rank-one operator A = λ β^♯ ⊗ β in coordinates. mu extracts the scalar coefficient satisfying A² = μ A. The module packages the finite-dimensional operator algebra behind the rank-one tensor picture of cost, with a covector β and inverse metric kernel hInv determining the sharp vector, the operator A, and the normalized projector P.
proof idea
One-line definition that scales the output of AApply by the reciprocal of mu.
why it matters
P supplies the normalized projector that induces FApply = 2P - I and supports the idempotence, linearity, and quadratic-law theorems downstream. It fills the rank-one tensor construction in the cost-induced projector algebra, consistent with the Recognition Science finite-dimensional model prior to lifting to the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.