Kernel-fast ℤ-list dot products for certificate data #

The pooled 49-dim scorecard (LipschitzCertScorecard.lean) evaluates its rational dot products by simp [Fin.sum_univ_succ] <;> norm_num — fine at 49 terms, but quadratic in the sum length and ~15–20 s per 784-term dot, which priced a FULL-INPUT (un-pooled, 784-dim) scorecard out of CI.

This file is the fix, in three parts:

certificate data lives in List ℤ (weights k/2⁸, pixels k/255 — store the integer numerators; negatives as Int.negSucc literals, which dodges a ~15 ms/element Neg-elaboration tax);
the 784-term arithmetic is ONE kernel evaluation per dot: dotZ xs ys = v := by decide +kernel — the kernel folds zipWith (·*·) with GMP integer ops, ~0.1 s per dot, propext-only (no ofReduceBool: +kernel is the kernel evaluator, NOT native_decide);
sum_getD_div (proved once, by induction) transports the integer fact to the ∑ j : Fin n, (xs.getD j 0 : ℝ)/c * ((ys.getD j 0 : ℝ)/d) sums that denseE-level certificate statements actually quantify over.

Used by LipschitzCertScorecardFull*.lean (generated by scripts/lipschitz_cert_scorecard_full.py). All 3-axiom clean.

source

def Proofs.dotZ (xs ys : List ℤ) :

ℤ

Integer dot product of two lists — the shape the kernel evaluates fast (decide +kernel: pointer-shared tails, GMP mul/add, no Fin indexing).

Equations

Proofs.dotZ xs ys = (List.zipWith (fun (x1 x2 : ℤ) => x1 * x2) xs ys).sum

Instances For

source

theorem Proofs.dotZ_comm (xs ys : List ℤ) :

dotZ xs ys = dotZ ys xs

source

theorem Proofs.sum_getD_mul (n : ℕ) (xs ys : List ℤ) :

xs.length = n → ys.length = n → ∑ j : Fin n, ↑(xs.getD (↑j) 0) * ↑(ys.getD (↑j) 0) = ↑(dotZ xs ys)

getD-dot over Fin n = list dot, generically (proved once, by induction on n so Fin.sum_univ_succ applies syntactically).

source

theorem Proofs.sum_getD_div {xs ys : List ℤ} {n : ℕ} (hx : xs.length = n) (hy : ys.length = n) {v : ℤ} (h : dotZ xs ys = v) (c d : ℝ) :

∑ j : Fin n, ↑(xs.getD (↑j) 0) / c * (↑(ys.getD (↑j) 0) / d) = ↑v / (c * d)

The scaled form the certificate files instantiate: rows stored as ℤ-lists of numerators over denominators c, d; once dotZ xs ys = v is checked in the kernel, the ℝ-level dense-layer dot is v/(c·d).

source

def Proofs.absSumZ (xs : List ℤ) :

ℤ

Integer absolute row sum — the ℓ1 weight of a row, kernel-evaluable (decide +kernel). Feeds the IBP uniform-radius layer bound denseLo/Hi (x ∓ ε) = ⟨w,x⟩ ∓ ε·Σ|w| (IntervalBound.lean).

Equations

Proofs.absSumZ xs = (List.map (fun (x : ℤ) => |x|) xs).sum

Instances For

source

theorem Proofs.sum_getD_abs (n : ℕ) (xs : List ℤ) :

xs.length = n → ∑ j : Fin n, |↑(xs.getD (↑j) 0)| = ↑(absSumZ xs)

getD abs-sum over Fin n = list abs-sum (the sum_getD_mul sibling).

source

theorem Proofs.sum_getD_abs_div {xs : List ℤ} {n : ℕ} (hx : xs.length = n) {v : ℤ} (h : absSumZ xs = v) {c : ℝ} (hc : 0 ≤ c) :

∑ j : Fin n, |↑(xs.getD (↑j) 0) / c| = ↑v / c

Scaled form: a k/c-grid row's ℓ1 norm from one kernel fact.

Documentation

LeanMlir.Proofs.Foundation.ListDot

Kernel-fast ℤ-list dot products for certificate data #