Affine Arithmetic

This file implements Affine Arithmetic (AA), which tracks linear dependencies between variables to avoid the "dependency problem" in interval arithmetic.

The Dependency Problem

Standard interval arithmetic treats each occurrence of a variable independently:

• x - x with x ∈ [-1, 1] gives [-2, 2] instead of [0, 0]

Affine arithmetic solves this by representing values as: x̂ = c₀ + Σᵢ cᵢ·εᵢ + [-r, r]

where εᵢ ∈ [-1, 1] are noise symbols tracking input correlations.

Main definitions

• AffineForm - Affine representation: central value + linear terms + error
• AffineForm.add, sub, neg, scale - Linear operations (exact)
• AffineForm.mul - Multiplication (introduces error)
• AffineForm.toInterval - Convert back to interval bounds

Key Properties

• sub_self_c0 - x - x has central value 0
• sub_self_radius_zero - For input forms (r=0), x - x has radius 0

References

• Stolfi & de Figueiredo, "Self-Validated Numerical Methods and Applications"

Helper Lemmas

The Affine Form Data Structure

structure LeanCert.Engine.Affine.AffineForm : Type

Affine Form: c₀ + Σᵢ (coeffs[i] * εᵢ) + [-r, r]

where εᵢ ∈ [-1, 1] are independent noise symbols.

• c0 : ℚ
• coeffs : List ℚ
• r : ℚ
• r_nonneg : 0 ≤ self.r

@[instance_reducible]

instance LeanCert.Engine.Affine.instReprAffineForm : Repr AffineForm

Equations

• LeanCert.Engine.Affine.instReprAffineForm = { reprPrec := LeanCert.Engine.Affine.instReprAffineForm.repr }

def LeanCert.Engine.Affine.instReprAffineForm.repr : AffineForm → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineForm.const (q : ℚ) : AffineForm

Equations

• LeanCert.Engine.Affine.AffineForm.const q = { c0 := q, coeffs := [], r := 0, r_nonneg := LeanCert.Engine.Affine.AffineForm.const._proof_1 }

def LeanCert.Engine.Affine.AffineForm.zero : AffineForm

Equations

• LeanCert.Engine.Affine.AffineForm.zero = LeanCert.Engine.Affine.AffineForm.const 0

@[instance_reducible]

instance LeanCert.Engine.Affine.AffineForm.instInhabited : Inhabited AffineForm

Equations

• LeanCert.Engine.Affine.AffineForm.instInhabited = { default := LeanCert.Engine.Affine.AffineForm.zero }

Helper Functions

def LeanCert.Engine.Affine.AffineForm.sumAbs (l : List ℚ) : ℚ

Equations

• LeanCert.Engine.Affine.AffineForm.sumAbs l = List.foldl (fun (acc c : ℚ) => acc + |c|) 0 l

theorem LeanCert.Engine.Affine.AffineForm.sumAbs_nonneg (l : List ℚ) : 0 ≤ sumAbs l

def LeanCert.Engine.Affine.AffineForm.deviationBound (af : AffineForm) : ℚ

Equations

• af.deviationBound = af.r + LeanCert.Engine.Affine.AffineForm.sumAbs af.coeffs

theorem LeanCert.Engine.Affine.AffineForm.deviationBound_nonneg (af : AffineForm) : 0 ≤ af.deviationBound

@[irreducible]

def LeanCert.Engine.Affine.AffineForm.zipWithPad (f : ℚ → ℚ → ℚ) (l1 l2 : List ℚ) : List ℚ

Equations

• LeanCert.Engine.Affine.AffineForm.zipWithPad f [] [] = []
• LeanCert.Engine.Affine.AffineForm.zipWithPad f [] (h :: t) = f 0 h :: LeanCert.Engine.Affine.AffineForm.zipWithPad f [] t
• LeanCert.Engine.Affine.AffineForm.zipWithPad f (h :: t) [] = f h 0 :: LeanCert.Engine.Affine.AffineForm.zipWithPad f t []
• LeanCert.Engine.Affine.AffineForm.zipWithPad f (h1 :: t1) (h2 :: t2) = f h1 h2 :: LeanCert.Engine.Affine.AffineForm.zipWithPad f t1 t2

Linear Operations (Exact)

def LeanCert.Engine.Affine.AffineForm.add (a b : AffineForm) : AffineForm

Equations

• a.add b = { c0 := a.c0 + b.c0, coeffs := LeanCert.Engine.Affine.AffineForm.zipWithPad (fun (x1 x2 : ℚ) => x1 + x2) a.coeffs b.coeffs, r := a.r + b.r, r_nonneg := ⋯ }

def LeanCert.Engine.Affine.AffineForm.neg (a : AffineForm) : AffineForm

Equations

• a.neg = { c0 := -a.c0, coeffs := List.map (fun (x : ℚ) => x.neg) a.coeffs, r := a.r, r_nonneg := ⋯ }

def LeanCert.Engine.Affine.AffineForm.sub (a b : AffineForm) : AffineForm

Equations

• a.sub b = a.add b.neg

def LeanCert.Engine.Affine.AffineForm.scale (q : ℚ) (a : AffineForm) : AffineForm

Equations

• LeanCert.Engine.Affine.AffineForm.scale q a = { c0 := q * a.c0, coeffs := List.map (fun (x : ℚ) => q * x) a.coeffs, r := |q| * a.r, r_nonneg := ⋯ }

Non-Linear Operations

def LeanCert.Engine.Affine.AffineForm.mul (a b : AffineForm) : AffineForm

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineForm.sq (a : AffineForm) : AffineForm

Equations

• a.sq = { c0 := a.c0 * a.c0, coeffs := List.map (fun (x : ℚ) => 2 * a.c0 * x) a.coeffs, r := 2 * |a.c0| * a.r + a.deviationBound * a.deviationBound, r_nonneg := ⋯ }

Interval Conversion

def LeanCert.Engine.Affine.AffineForm.ofInterval (I : Core.IntervalRat) (idx totalVars : ℕ) : AffineForm

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineForm.ofIntervalFallback (I : Core.IntervalRat) : AffineForm

Embed an interval as an affine form without introducing a noise symbol.

This is the canonical sound fallback for nonlinear operations without a dedicated affine linearization. It intentionally loses correlation while preserving the full interval enclosure.

Equations

• LeanCert.Engine.Affine.AffineForm.ofIntervalFallback I = { c0 := (I.lo + I.hi) / 2, coeffs := [], r := |(I.hi - I.lo) / 2|, r_nonneg := ⋯ }

def LeanCert.Engine.Affine.AffineForm.toInterval (af : AffineForm) : Core.IntervalRat

Equations

• af.toInterval = { lo := af.c0 - af.deviationBound, hi := af.c0 + af.deviationBound, le := ⋯ }

The Key Property: x - x = 0

theorem LeanCert.Engine.Affine.AffineForm.sub_self_c0 (a : AffineForm) : (a.sub a).c0 = 0

The central value of x - x is exactly 0

theorem LeanCert.Engine.Affine.AffineForm.sub_self_radius_zero (a : AffineForm) (h : a.r = 0) : (a.sub a).r = 0

For an input affine form (r = 0), x - x has zero radius

theorem LeanCert.Engine.Affine.AffineForm.sub_self_coeffs_allzero (a : AffineForm) (c : ℚ) : c ∈ (a.sub a).coeffs → c = 0

Subtraction of the same form gives all-zero coefficients

Soundness Infrastructure

@[reducible, inline]

abbrev LeanCert.Engine.Affine.AffineForm.NoiseAssignment : Type

Equations

• LeanCert.Engine.Affine.AffineForm.NoiseAssignment = List ℝ

def LeanCert.Engine.Affine.AffineForm.validNoise (eps : NoiseAssignment) : Prop

Equations

• LeanCert.Engine.Affine.AffineForm.validNoise eps = ∀ e ∈ eps, -1 ≤ e ∧ e ≤ 1

def LeanCert.Engine.Affine.AffineForm.linearSum (coeffs : List ℚ) (eps : NoiseAssignment) : ℝ

The linear functional Σ cᵢ * εᵢ

Equations

• LeanCert.Engine.Affine.AffineForm.linearSum coeffs eps = (List.zipWith (fun (c : ℚ) (e : ℝ) => ↑c * e) coeffs eps).sum

def LeanCert.Engine.Affine.AffineForm.evalLinear (af : AffineForm) (eps : NoiseAssignment) : ℝ

Equations

• af.evalLinear eps = ↑af.c0 + LeanCert.Engine.Affine.AffineForm.linearSum af.coeffs eps

def LeanCert.Engine.Affine.AffineForm.mem_affine (af : AffineForm) (eps : NoiseAssignment) (v : ℝ) : Prop

Equations

• af.mem_affine eps v = ∃ (err : ℝ), |err| ≤ ↑af.r ∧ v = af.evalLinear eps + err

Helper lemmas for soundness

Soundness Proofs

theorem LeanCert.Engine.Affine.AffineForm.mem_const (q : ℚ) (eps : NoiseAssignment) : (const q).mem_affine eps ↑q

Constants are sound: const q represents q

theorem LeanCert.Engine.Affine.AffineForm.mem_scale (q : ℚ) {a : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hmem : a.mem_affine eps v) : (scale q a).mem_affine eps (↑q * v)

Scalar multiplication is sound

theorem LeanCert.Engine.Affine.AffineForm.mem_add {a b : AffineForm} {eps : NoiseAssignment} {va vb : ℝ} (ha : a.mem_affine eps va) (hb : b.mem_affine eps vb) : (a.add b).mem_affine eps (va + vb)

Addition is sound

theorem LeanCert.Engine.Affine.AffineForm.mem_neg {a : AffineForm} {eps : NoiseAssignment} {va : ℝ} (ha : a.mem_affine eps va) : a.neg.mem_affine eps (-va)

Negation is sound

theorem LeanCert.Engine.Affine.AffineForm.mem_sub {a b : AffineForm} {eps : NoiseAssignment} {va vb : ℝ} (ha : a.mem_affine eps va) (hb : b.mem_affine eps vb) : (a.sub b).mem_affine eps (va - vb)

Subtraction is sound

Bounding the linear sum

Multiplication Soundness Infrastructure

theorem LeanCert.Engine.Affine.AffineForm.mem_mul {a b : AffineForm} {eps : NoiseAssignment} {va vb : ℝ} (hvalid : validNoise eps) (ha : a.mem_affine eps va) (hb : b.mem_affine eps vb) : (a.mul b).mem_affine eps (va * vb)

Multiplication is sound

theorem LeanCert.Engine.Affine.AffineForm.mem_sq {a : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hmem : a.mem_affine eps v) : a.sq.mem_affine eps (v * v)

Squaring is sound: if v is represented by a, then v*v is represented by sq a

theorem LeanCert.Engine.Affine.AffineForm.mem_toInterval {af : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hlen : List.length eps = af.coeffs.length) (hmem : af.mem_affine eps v) : v ∈ af.toInterval

If v is represented by af, then v ∈ toInterval af

theorem LeanCert.Engine.Affine.AffineForm.mem_toInterval_weak {af : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hmem : af.mem_affine eps v) : v ∈ af.toInterval

If v is represented by af, then v ∈ toInterval af (no length assumption).

theorem LeanCert.Engine.Affine.AffineForm.mem_affine_of_interval {I : Core.IntervalRat} {eps : NoiseAssignment} {x : ℝ} (hx : x ∈ I) : { c0 := (I.lo + I.hi) / 2, coeffs := [], r := |(I.hi - I.lo) / 2|, r_nonneg := ⋯ }.mem_affine eps x

If x is inside an interval, the midpoint/radius affine form contains x.

theorem LeanCert.Engine.Affine.AffineForm.mem_ofIntervalFallback {I : Core.IntervalRat} {eps : NoiseAssignment} {x : ℝ} (hx : x ∈ I) : (ofIntervalFallback I).mem_affine eps x

ofIntervalFallback represents every point of its source interval.