compensatoryQuadratic
compensatoryQuadratic α ε defines the residual quadratic term obtained by subtracting the multiplicative quadratic approximation from the additive quadratic approximation. Researchers decomposing quadratic costs in the Ndim bridge would cite this definition to isolate the compensatory remainder. It is realized as a direct algebraic subtraction of the two upstream quadratic expressions.
claimFor vectors $α, ε ∈ ℝ^n$, the compensatory quadratic term is defined by $Q_{add}(ε) - Q_{mult}(α, ε)$, where $Q_{add}(ε) = ½ ∑_i ε_i²$ and $Q_{mult}(α, ε) = ½ (α · ε)²$.
background
The module develops an additive-multiplicative quadratic bridge for cost approximations. Vec n abbreviates the type of n-component real vectors, represented as functions Fin n → ℝ. Upstream, additiveQuadratic ε supplies the quadratic additive approximation ½ Σ ε_i², while multiplicativeQuadratic α ε supplies the quadratic multiplicative approximation ½ (dot α ε)².
proof idea
This is a one-line definition that subtracts multiplicativeQuadratic α ε from additiveQuadratic ε.
why it matters in Recognition Science
This definition supplies the residual term required by the additive_decomposition theorem, which equates additiveQuadratic ε to the sum of multiplicativeQuadratic α ε and compensatoryQuadratic α ε. It is also invoked to prove nonnegativity of the compensatory term when the squared norm of α is at most one. In the Recognition Science setting the quadratic bridge supports cost structures appearing in the forcing chain.
scope and limits
- Does not restrict the dimension n.
- Does not impose bounds on the vectors α or ε.
- Does not establish inequalities or other properties by itself.
Lean usage
theorem additive_decomposition {n : ℕ} (α ε : Vec n) : additiveQuadratic ε = multiplicativeQuadratic α ε + compensatoryQuadratic α ε := by unfold compensatoryQuadratic; ringformal statement (Lean)
22noncomputable def compensatoryQuadratic {n : ℕ} (α ε : Vec n) : ℝ :=
proof body
Definition body.
23 additiveQuadratic ε - multiplicativeQuadratic α ε
24