additiveQuadratic
plain-language theorem explainer
additiveQuadratic supplies the quadratic additive cost approximation as half the sum of squared components of an n-dimensional vector ε. Cost analysts working on decompositions in the Recognition Science framework cite this definition when separating additive and multiplicative contributions to total cost. It is realized as a direct one-line summation formula over the finite index set Fin n.
Claim. For a vector ε ∈ ℝⁿ, the additive quadratic approximation is defined by ½ ∑_{i=1}^n ε_i².
background
The module Cost.Ndim.Bridge develops relations between additive and multiplicative quadratic approximations in n dimensions. Vec n is the type of functions from Fin n to the reals, serving as n-component real vectors. The upstream multiplicative theorem from CostAlgebra states that a J-automorphism f satisfies f(posMul x y) = posMul (f x) (f y), establishing multiplicativity on positive reals.
proof idea
The definition is a direct one-line expression that computes half the sum of squares of the vector components indexed by Fin n.
why it matters
This definition anchors the additive-multiplicative quadratic bridge and feeds directly into the decomposition theorem additive_decomposition, which writes additiveQuadratic ε as multiplicativeQuadratic α ε plus compensatoryQuadratic α ε. It also supports the bound multiplicative_le_additive_of_sqNorm_le_one when the squared norm of α is at most one. In the Recognition framework the quadratic forms arise when analyzing cost preservation under J-automorphisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.