additive_decomposition
plain-language theorem explainer
Researchers decomposing quadratic costs into multiplicative and residual components in the Recognition Science cost model would cite the additive decomposition identity. It states that the additive quadratic approximation of a vector ε equals the multiplicative quadratic term formed with α plus the compensatory quadratic. The proof is a direct algebraic verification obtained by unfolding the compensatory definition and simplifying.
Claim. For any natural number $n$ and vectors $α, ε ∈ ℝ^n$, let $A(ε) = ½ ∑ ε_i²$, $M(α,ε) = ½ (α · ε)²$, and $C(α,ε) = A(ε) - M(α,ε)$. Then $A(ε) = M(α,ε) + C(α,ε)$.
background
The Cost.Ndim.Bridge module addresses the additive-multiplicative quadratic bridge. Vec n is the type of maps from Fin n to the reals, representing n-component real vectors. additiveQuadratic ε is defined as ½ ∑_{i:Fin n} (ε i)², the quadratic additive approximation. multiplicativeQuadratic α ε is ½ (dot α ε)². compensatoryQuadratic α ε is introduced explicitly as additiveQuadratic ε minus multiplicativeQuadratic α ε.
proof idea
The proof is a one-line wrapper that unfolds the definition of compensatoryQuadratic and applies the ring tactic to confirm the algebraic identity.
why it matters
This identity is the core of the quadratic bridge in the cost module. It permits expressing the total quadratic cost as a sum of a multiplicative projection and a residual term. In the Recognition Science framework it supports decomposition of costs prior to applying the phi-ladder or other scaling relations. No downstream theorems are listed yet, indicating it serves as a foundational identity for subsequent cost analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.