additive_decomposition
The additive quadratic approximation decomposes exactly into the multiplicative quadratic projection plus the residual compensatory term for any vectors α and ε in dimension n. Cost analysts working with quadratic approximations in the Recognition framework cite this identity to isolate projection error from the total quadratic cost. The proof is a one-line wrapper that unfolds the residual definition and applies ring normalization.
claimFor any natural number $n$ and vectors $α, ε ∈ ℝ^n$, the additive quadratic satisfies $½ ∑_i ε_i² = ½ (α · ε)² + (½ ∑_i ε_i² − ½ (α · ε)²)$.
background
The module sets up an additive-multiplicative quadratic bridge inside the cost domain. Vec n is the type of n-component real vectors, written as functions Fin n → ℝ. additiveQuadratic ε is the standard quadratic form ½ ∑ (ε i)². multiplicativeQuadratic α ε is the squared projection ½ (dot α ε)². compensatoryQuadratic α ε is defined directly as the difference additiveQuadratic ε − multiplicativeQuadratic α ε, serving as the residual term.
proof idea
The proof unfolds compensatoryQuadratic (which expands to additiveQuadratic ε minus multiplicativeQuadratic α ε) and applies the ring tactic for algebraic simplification.
why it matters in Recognition Science
This identity supplies the exact decomposition that separates the multiplicative projection from its residual in quadratic cost models. It sits inside the Ndim cost bridge and supports consistent handling of approximation error, consistent with the framework's use of quadratic forms to approximate recognition costs before lifting to the full J-cost and phi-ladder structure.
scope and limits
- Does not assume any bound on the vectors α or ε.
- Does not extend the identity to non-quadratic or higher-order terms.
- Does not invoke the J-function, Recognition Composition Law, or phi-ladder constants.
- Does not address convergence properties or sign constraints on the residual.
formal statement (Lean)
25theorem additive_decomposition {n : ℕ} (α ε : Vec n) :
26 additiveQuadratic ε
27 = multiplicativeQuadratic α ε + compensatoryQuadratic α ε := by
proof body
Term-mode proof.
28 unfold compensatoryQuadratic
29 ring
30
31/-- Squared Cauchy-Schwarz bound in our notation. -/