Documentation

LeanMlir.Proofs.Foundation.IntervalBoundConv

IBP at conv depth — a compositional interval-bound engine #

IntervalBound.lean proves the L∞ certificate for exactly one shape: dense ∘ relu ∘ dense, dense-only, hard-wired at two layers (ibp2_certified_at_eps). That is the shape the 784→16→10 scorecards use, and it is the reason the IBP tier stops at one hidden layer.

This file removes both restrictions. The soundness argument for IBP is compositional — "the box propagates" is a property of one layer, and depth is just ∘ — so the engine here is:

InBox / InBox3 — a point lies in an axis-aligned box (flat / tensor);
BoxSound f Flo Fhi — (Flo, Fhi) is a sound interval transformer for f;
BoxSound.comp — depth: sound transformers compose exactly as the layers do, so an n-layer net's transformer is n compositions and no new proof;
per-layer instances in tensor space (BoxSound3) — relu (endpoint max), conv2d (sign-split over the padded taps), maxPool2 (max is monotone, so pool the endpoints), and the dense head denseT (sign-split);
ibp3_certified_of_boxSound — the capstone: a sound tensor body and dense head whose output boxes separate on x ∓ ε certify x at L∞ radius ε, at any depth.

The conv transformer is stated against the repo's own conv2d (CNN.lean, SAME padding, the definition the VJP suite and the codegen use) — not a re-modelled convolution. Padding contributes 0 to both endpoints, which is why the sign-split can sit outside the pad test (convTap is monotone, and constant 0 where the window falls off the image).

convLo_uniform / convHi_uniform are the conv peers of denseLo_uniform/denseHi_uniform: on the first layer's uniform box x ∓ ε the interval image collapses to conv2d W b x ∓ ε · conv2d |W| 0 𝟙, i.e. one extra convolution by the absolute kernel against the all-ones image. That keeps the generated per-image data at "one forward pass + one |W| pass" instead of two full sign-split sums — the conv analogue of the ⟨w,x⟩ ∓ ε‖w‖₁ collapse the 784-dim files already exploit.

Nonlinearity note: as in IntervalBound.lean, unstable (sign-crossing) ReLUs and tied max-pool windows are handled soundly, not assumed away — the box simply contains both branches. The certificate is sound and incomplete; counts derived from it are lower bounds only.

Everything is elementary and closes under propext / Classical.choice / Quot.sound.

def Proofs.IBP.InBox {n : ℕ} (lo hi u : Vec n) :

u lies in the axis-aligned box [lo, hi] (flat vectors).

Equations

Proofs.IBP.InBox lo hi u = ∀ (i : Fin n), lo i ≤ u i ∧ u i ≤ hi i

Instances For

def Proofs.IBP.InBox3 {c h w : ℕ} (lo hi u : Tensor3 c h w) :

u lies in the axis-aligned box [lo, hi] (rank-3 tensors).

Equations

Proofs.IBP.InBox3 lo hi u = ∀ (a : Fin c) (b : Fin h) (d : Fin w), lo a b d ≤ u a b d ∧ u a b d ≤ hi a b d

Instances For

def Proofs.IBP.BoxSound {n m : ℕ} (f : Vec n → Vec m) (Flo Fhi : Vec n → Vec n → Vec m) :

A sound interval transformer. Flo lo hi / Fhi lo hi bracket f on every point of the box [lo, hi]. This is the only property a layer needs to contribute to a certificate — it composes (BoxSound.comp) and it is what the capstone consumes.

Equations

Proofs.IBP.BoxSound f Flo Fhi = ∀ (lo hi u : Proofs.Vec n), Proofs.IBP.InBox lo hi u → Proofs.IBP.InBox (Flo lo hi) (Fhi lo hi) (f u)

Instances For

def Proofs.IBP.BoxSound3 {c h w c' h' w' : ℕ} (f : Tensor3 c h w → Tensor3 c' h' w') (Flo Fhi : Tensor3 c h w → Tensor3 c h w → Tensor3 c' h' w') :

The rank-3 peer, for the layers that live in tensor space.

Equations

Proofs.IBP.BoxSound3 f Flo Fhi = ∀ (lo hi u : Proofs.Tensor3 c h w), Proofs.IBP.InBox3 lo hi u → Proofs.IBP.InBox3 (Flo lo hi) (Fhi lo hi) (f u)

Instances For

theorem Proofs.IBP.BoxSound.comp {n m p : ℕ} {f : Vec n → Vec m} {g : Vec m → Vec p} {Flo Fhi : Vec n → Vec n → Vec m} {Glo Ghi : Vec m → Vec m → Vec p} (hg : BoxSound g Glo Ghi) (hf : BoxSound f Flo Fhi) :

BoxSound (g ∘ f) (fun (lo hi : Vec n) => Glo (Flo lo hi) (Fhi lo hi)) fun (lo hi : Vec n) => Ghi (Flo lo hi) (Fhi lo hi)

Depth, for free. Sound transformers compose exactly as their layers do: feed the first layer's output box into the second layer's transformer. An n-layer net therefore needs n per-layer soundness facts and n-1 uses of this lemma — no new argument per depth.

theorem Proofs.IBP.boxSound_id {n : ℕ} :

BoxSound id (fun (lo x : Vec n) => lo) fun (x hi : Vec n) => hi

Identity is its own transformer (the base case of a layer fold).

theorem Proofs.IBP.BoxSound3.comp {c h w c' h' w' c'' h'' w'' : ℕ} {f : Tensor3 c h w → Tensor3 c' h' w'} {g : Tensor3 c' h' w' → Tensor3 c'' h'' w''} {Flo Fhi : Tensor3 c h w → Tensor3 c h w → Tensor3 c' h' w'} {Glo Ghi : Tensor3 c' h' w' → Tensor3 c' h' w' → Tensor3 c'' h'' w''} (hg : BoxSound3 g Glo Ghi) (hf : BoxSound3 f Flo Fhi) :

BoxSound3 (g ∘ f) (fun (lo hi : Tensor3 c h w) => Glo (Flo lo hi) (Fhi lo hi)) fun (lo hi : Tensor3 c h w) => Ghi (Flo lo hi) (Fhi lo hi)

Depth in tensor space — the BoxSound3 peer of BoxSound.comp, so a conv body (maxpool ∘ relu ∘ conv ∘ …) composes without round-tripping through flatten between every layer.

noncomputable def Proofs.IBP.denseLoV {m n : ℕ} (W : Mat m n) (b : Vec n) (lo hi : Vec m) :

Sign-split LOWER image of dense W b: positive weights pull from lo, negative from hi. Biases shift both endpoints equally.

Equations

Proofs.IBP.denseLoV W b lo hi j = (∑ i : Fin m, if 0 ≤ W i j then lo i * W i j else hi i * W i j) + b j

Instances For

noncomputable def Proofs.IBP.denseHiV {m n : ℕ} (W : Mat m n) (b : Vec n) (lo hi : Vec m) :

Sign-split UPPER image of dense W b.

Equations

Proofs.IBP.denseHiV W b lo hi j = (∑ i : Fin m, if 0 ≤ W i j then hi i * W i j else lo i * W i j) + b j

Instances For

theorem Proofs.IBP.denseLoV_uniform {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (ε : ℝ) (j : Fin n) :

denseLoV W b (fun (i : Fin m) => x i - ε) (fun (i : Fin m) => x i + ε) j = ∑ i : Fin m, x i * W i j + b j - ε * ∑ i : Fin m, |W i j|

Uniform-box collapse for dense — the Vec-space peer of denseLo_uniform: on x ∓ ε the sign split evaluates to ⟨x, W⟩ + b ∓ ε·‖W_{·j}‖₁, so an instance needs one dot and one ℓ1 fact per output, not a sign-split sum.

theorem Proofs.IBP.denseHiV_uniform {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (ε : ℝ) (j : Fin n) :

denseHiV W b (fun (i : Fin m) => x i - ε) (fun (i : Fin m) => x i + ε) j = ∑ i : Fin m, x i * W i j + b j + ε * ∑ i : Fin m, |W i j|

Sibling of denseLoV_uniform for the upper endpoint.

theorem Proofs.IBP.relu_apply_eq_max {n : ℕ} (x : Vec n) (i : Fin n) :

relu n x i = max (x i) 0

Proofs.relu's if · > 0 form is the max form the box endpoints use.

noncomputable def Proofs.IBP.reluT {c h w : ℕ} (x : Tensor3 c h w) :

Coordinatewise ReLU on tensors — the form a conv body uses between conv and pool, so the body never leaves tensor space.

Equations

Proofs.IBP.reluT x o i j = max (x o i j) 0

Instances For

theorem Proofs.IBP.flatten_reluT {c h w : ℕ} (T : Tensor3 c h w) :

(reluT T).flatten = relu (c * h * w) T.flatten

reluT IS the repo's Proofs.relu, read through flatten — so the conv body's activation is the same function the VJP suite differentiates, not a second ReLU.

theorem Proofs.IBP.reluT_boxSound3 {c h w : ℕ} :

BoxSound3 reluT (fun (lo x : Tensor3 c h w) => reluT lo) fun (x hi : Tensor3 c h w) => reluT hi

theorem Proofs.IBP.unflatten_sub_const {c h w : ℕ} (T : Tensor3 c h w) (ε : ℝ) :

(Tensor3.unflatten fun (i : Fin (c * h * w)) => T.flatten i - ε) = fun (a : Fin c) (b : Fin h) (d : Fin w) => T a b d - ε

The input box of a CertifiedAtLinfV goal is stated on the FLAT vector x ∓ ε; these two put it back in tensor space so the conv transformer's uniform-collapse lemmas apply.

theorem Proofs.IBP.unflatten_add_const {c h w : ℕ} (T : Tensor3 c h w) (ε : ℝ) :

(Tensor3.unflatten fun (i : Fin (c * h * w)) => T.flatten i + ε) = fun (a : Fin c) (b : Fin h) (d : Fin w) => T a b d + ε

noncomputable def Proofs.IBP.convTap {ic h w kH kW : ℕ} (x : Tensor3 ic h w) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) (hi : Fin h) (wi : Fin w) :

The padded input lookup conv2d performs, factored out verbatim: the tap at kernel offset (kh, kw) for output position (hi, wi), or 0 where the window falls off the image.

Equations

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

Instances For

theorem Proofs.IBP.conv2d_eq_tap {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (x : Tensor3 ic h w) (o : Fin oc) (hi : Fin h) (wi : Fin w) :

conv2d W b x o hi wi = b o + ∑ c : Fin ic, ∑ kh : Fin kH, ∑ kw : Fin kW, W o c kh kw * convTap x c kh kw hi wi

conv2d in tap form — definitional, so the engine below is talking about the repo's convolution and not a re-modelled one.

theorem Proofs.IBP.convTap_mono {ic h w kH kW : ℕ} {lo hi u : Tensor3 ic h w} (hu : InBox3 lo hi u) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) (hI : Fin h) (wI : Fin w) :

convTap lo c kh kw hI wI ≤ convTap u c kh kw hI wI ∧ convTap u c kh kw hI wI ≤ convTap hi c kh kw hI wI

Taps are monotone in the input tensor (the pad branch is the constant 0, which is monotone trivially) — the only fact the conv sign-split needs.

noncomputable def Proofs.IBP.convLo {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (lo hi : Tensor3 ic h w) :

Tensor3 oc h w

Sign-split LOWER image of conv2d W b. The split sits outside the pad test because convTap is 0 on both endpoints there.

Equations

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

Instances For

noncomputable def Proofs.IBP.convHi {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (lo hi : Tensor3 ic h w) :

Tensor3 oc h w

Sign-split UPPER image of conv2d W b.

Equations

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

Instances For

theorem Proofs.IBP.conv2d_boxSound3 {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) :

BoxSound3 (conv2d W b) (convLo W b) (convHi W b)

Convolution propagates boxes soundly. The rank-3 conv peer of denseLo_le/le_denseHi.

theorem Proofs.IBP.maxPool2_boxSound3 {c h w : ℕ} :

BoxSound3 maxPool2 (fun (lo x : Tensor3 c (2 * h) (2 * w)) => maxPool2 lo) fun (x hi : Tensor3 c (2 * h) (2 * w)) => maxPool2 hi

Max-pool is monotone, so its box endpoints are the pooled endpoints. Tied windows need no special handling: max is monotone regardless of which entry attains it, so the certificate never touches the argmax.

def Proofs.IBP.CertifiedAtLinfV {n k : ℕ} (f : Vec n → Vec k) (ε : ℝ) (x : Vec n) (y : Fin k) :

f is certified at L∞ radius ε on input x with class y: every coordinatewise-bounded perturbation keeps y the strict argmax. The Vec-space peer of LipschitzCertDemo.CertifiedAtLinf.

Equations

Proofs.IBP.CertifiedAtLinfV f ε x y = ∀ (δ : Proofs.Vec n), (∀ (i : Fin n), |δ i| ≤ ε) → ∀ (j : Fin k), j ≠ y → f (x + δ) j < f (x + δ) y

Instances For

A conv classifier is Tensor3 → Vec k: a tensor body then a dense head that reads the activation directly. Stating the certificate there keeps flatten out of every per-image proof (it is an Equiv computation, and paying for it at each of the head's inputs is the difference between a cheap instance and an unaffordable one). The flat machinery above stays available for nets that need it; nothing here depends on it.

noncomputable def Proofs.IBP.denseT {c h w k : ℕ} (W : Fin c → Fin h → Fin w → Fin k → ℝ) (b : Vec k) (x : Tensor3 c h w) :

The dense head of a conv net: Fin c → Fin h → Fin w → Fin k weights read the rank-3 activation in place (this is "flatten then dense", fused).

Equations

Proofs.IBP.denseT W b x j = ∑ o : Fin c, ∑ i : Fin h, ∑ m : Fin w, x o i m * W o i m j + b j

Instances For

noncomputable def Proofs.IBP.denseTLo {c h w k : ℕ} (W : Fin c → Fin h → Fin w → Fin k → ℝ) (b : Vec k) (lo hi : Tensor3 c h w) :

Equations

Proofs.IBP.denseTLo W b lo hi j = (∑ o : Fin c, ∑ i : Fin h, ∑ m : Fin w, if 0 ≤ W o i m j then lo o i m * W o i m j else hi o i m * W o i m j) + b j

Instances For

noncomputable def Proofs.IBP.denseTHi {c h w k : ℕ} (W : Fin c → Fin h → Fin w → Fin k → ℝ) (b : Vec k) (lo hi : Tensor3 c h w) :

Equations

Proofs.IBP.denseTHi W b lo hi j = (∑ o : Fin c, ∑ i : Fin h, ∑ m : Fin w, if 0 ≤ W o i m j then hi o i m * W o i m j else lo o i m * W o i m j) + b j

Instances For

def Proofs.IBP.BoxSound3V {c h w k : ℕ} (f : Tensor3 c h w → Vec k) (Flo Fhi : Tensor3 c h w → Tensor3 c h w → Vec k) :

A sound interval transformer for a Tensor3 → Vec map (the head rung).

Equations

Proofs.IBP.BoxSound3V f Flo Fhi = ∀ (lo hi u : Proofs.Tensor3 c h w), Proofs.IBP.InBox3 lo hi u → Proofs.IBP.InBox (Flo lo hi) (Fhi lo hi) (f u)

Instances For

theorem Proofs.IBP.BoxSound3V.comp3 {c h w c' h' w' k : ℕ} {f : Tensor3 c h w → Tensor3 c' h' w'} {g : Tensor3 c' h' w' → Vec k} {Flo Fhi : Tensor3 c h w → Tensor3 c h w → Tensor3 c' h' w'} {Glo Ghi : Tensor3 c' h' w' → Tensor3 c' h' w' → Vec k} (hg : BoxSound3V g Glo Ghi) (hf : BoxSound3 f Flo Fhi) :

BoxSound3V (g ∘ f) (fun (lo hi : Tensor3 c h w) => Glo (Flo lo hi) (Fhi lo hi)) fun (lo hi : Tensor3 c h w) => Ghi (Flo lo hi) (Fhi lo hi)

Compose a tensor body into a head — the last link of a conv net's chain.

theorem Proofs.IBP.denseT_boxSound3V {c h w k : ℕ} (W : Fin c → Fin h → Fin w → Fin k → ℝ) (b : Vec k) :

BoxSound3V (denseT W b) (denseTLo W b) (denseTHi W b)

def Proofs.IBP.CertifiedAtLinf3 {c h w k : ℕ} (f : Tensor3 c h w → Vec k) (ε : ℝ) (x : Tensor3 c h w) (y : Fin k) :

f is certified at pixel L∞ radius ε on the image x with class y: every perturbation bounded by ε in EVERY pixel keeps y the strict argmax. The rank-3 (image-shaped) peer of CertifiedAtLinfV.

Equations

Proofs.IBP.CertifiedAtLinf3 f ε x y = ∀ (δ : Proofs.Tensor3 c h w), (∀ (a : Fin c) (b : Fin h) (d : Fin w), |δ a b d| ≤ ε) → ∀ (j : Fin k), j ≠ y → f (x + δ) j < f (x + δ) y

Instances For

theorem Proofs.IBP.CertifiedAtLinf3.mono {c h w k : ℕ} {f : Tensor3 c h w → Vec k} {ε ε' : ℝ} {x : Tensor3 c h w} {y : Fin k} (hc : CertifiedAtLinf3 f ε x y) (hle : ε' ≤ ε) :

CertifiedAtLinf3 f ε' x y

Certification is monotone in the radius: a certificate at ε is a certificate at every ε' ≤ ε, directly from the statement. Instances therefore only need to prove (and carry the box data for) the LARGEST radius at which an image certifies — every smaller radius on the ε-grid is a one-line corollary, not another propagated box.

theorem Proofs.IBP.CertifiedAtLinfV.mono {n k : ℕ} {f : Vec n → Vec k} {ε ε' : ℝ} {x : Vec n} {y : Fin k} (hc : CertifiedAtLinfV f ε x y) (hle : ε' ≤ ε) :

CertifiedAtLinfV f ε' x y

The flat peer of CertifiedAtLinf3.mono.

theorem Proofs.IBP.ibp3_certified_of_boxSound {c h w k : ℕ} {f : Tensor3 c h w → Vec k} {Flo Fhi : Tensor3 c h w → Tensor3 c h w → Vec k} (hs : BoxSound3V f Flo Fhi) {x : Tensor3 c h w} {ε : ℝ} {y : Fin k} (hsep : ∀ (j : Fin k), j ≠ y → Fhi (fun (a : Fin c) (b : Fin h) (d : Fin w) => x a b d - ε) (fun (a : Fin c) (b : Fin h) (d : Fin w) => x a b d + ε) j < Flo (fun (a : Fin c) (b : Fin h) (d : Fin w) => x a b d - ε) (fun (a : Fin c) (b : Fin h) (d : Fin w) => x a b d + ε) y) :

CertifiedAtLinf3 f ε x y

IBP L∞ certificate for a conv net, in the shape a convolutional classifier has: an arbitrary-depth tensor body (conv/relu/pool, composed by BoxSound3.comp) followed by a dense head. Separation of the propagated output boxes on the pixel box x ∓ ε certifies x.

noncomputable def Proofs.IBP.deepNet {ic c₁ c₂ h w k : ℕ} (W₁ : Kernel4 c₁ ic 3 3) (b₁ : Vec c₁) (W₂ : Kernel4 c₂ c₁ 3 3) (b₂ : Vec c₂) (Wh : Fin c₂ → Fin h → Fin w → Fin k → ℝ) (bh : Vec k) :

Tensor3 ic (2 * h) (2 * w) → Vec k

A deeper stack than anything the dense ibp2_certified_at_eps could state: conv → relu → conv → relu → max-pool → dense head. Weights are arbitrary — this is a statement about the ENGINE, not about one trained net.

Equations

Proofs.IBP.deepNet W₁ b₁ W₂ b₂ Wh bh = Proofs.IBP.denseT Wh bh ∘ Proofs.maxPool2 ∘ Proofs.IBP.reluT ∘ Proofs.conv2d W₂ b₂ ∘ Proofs.IBP.reluT ∘ Proofs.conv2d W₁ b₁

Instances For

theorem Proofs.IBP.deepNet_boxSound {ic c₁ c₂ h w k : ℕ} (W₁ : Kernel4 c₁ ic 3 3) (b₁ : Vec c₁) (W₂ : Kernel4 c₂ c₁ 3 3) (b₂ : Vec c₂) (Wh : Fin c₂ → Fin h → Fin w → Fin k → ℝ) (bh : Vec k) :

BoxSound3V (deepNet W₁ b₁ W₂ b₂ Wh bh) (fun (lo hi : Tensor3 ic (2 * h) (2 * w)) => denseTLo Wh bh (maxPool2 (reluT (convLo W₂ b₂ (reluT (convLo W₁ b₁ lo hi)) (reluT (convHi W₁ b₁ lo hi))))) (maxPool2 (reluT (convHi W₂ b₂ (reluT (convLo W₁ b₁ lo hi)) (reluT (convHi W₁ b₁ lo hi)))))) fun (lo hi : Tensor3 ic (2 * h) (2 * w)) => denseTHi Wh bh (maxPool2 (reluT (convLo W₂ b₂ (reluT (convLo W₁ b₁ lo hi)) (reluT (convHi W₁ b₁ lo hi))))) (maxPool2 (reluT (convHi W₂ b₂ (reluT (convLo W₁ b₁ lo hi)) (reluT (convHi W₁ b₁ lo hi)))))

Depth costs nothing. The six-layer stack's sound interval transformer is five .comps of the per-layer facts — no induction, no new lemma, and the proof term is one line. Feeding this to ibp3_certified_of_boxSound gives a pixel-L∞ certificate for the deep net exactly as for the shallow one; the only thing that grows with depth is how loose the box gets.

noncomputable def Proofs.IBP.absK {oc ic kH kW : ℕ} (W : Kernel4 oc ic kH kW) :

Kernel4 oc ic kH kW

The entrywise absolute kernel.

Equations

Proofs.IBP.absK W o c kh kw = |W o c kh kw|

Instances For

noncomputable def Proofs.IBP.onesT (ic h w : ℕ) :

Tensor3 ic h w

The all-ones input, used to read off each output position's active tap count (SAME padding drops taps at the border, so the ℓ1 weight is position-dependent — conv2d (absK W) 0 ones computes exactly that).

Equations

Proofs.IBP.onesT ic h w x✝² x✝¹ x✝ = 1

Instances For

theorem Proofs.IBP.convTap_uniform_lo {ic h w kH kW : ℕ} (x : Tensor3 ic h w) (ε : ℝ) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) (hI : Fin h) (wI : Fin w) :

convTap (fun (a : Fin ic) (b : Fin h) (d : Fin w) => x a b d - ε) c kh kw hI wI = convTap x c kh kw hI wI - ε * convTap (onesT ic h w) c kh kw hI wI

A tap of the uniform box's LOWER face splits into tap x − ε·tap 𝟙.

theorem Proofs.IBP.convTap_uniform_hi {ic h w kH kW : ℕ} (x : Tensor3 ic h w) (ε : ℝ) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) (hI : Fin h) (wI : Fin w) :

convTap (fun (a : Fin ic) (b : Fin h) (d : Fin w) => x a b d + ε) c kh kw hI wI = convTap x c kh kw hI wI + ε * convTap (onesT ic h w) c kh kw hI wI

A tap of the uniform box's UPPER face splits into tap x + ε·tap 𝟙.

theorem Proofs.IBP.convLo_uniform {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (x : Tensor3 ic h w) (ε : ℝ) (o : Fin oc) (hI : Fin h) (wI : Fin w) :

convLo W b (fun (a : Fin ic) (b' : Fin h) (d : Fin w) => x a b' d - ε) (fun (a : Fin ic) (b' : Fin h) (d : Fin w) => x a b' d + ε) o hI wI = conv2d W b x o hI wI - ε * conv2d (absK W) (fun (x : Fin oc) => 0) (onesT ic h w) o hI wI

Uniform-box collapse, LOWER. On the first layer's box x ∓ ε the conv sign split evaluates to conv2d W b x − ε · conv2d |W| 0 𝟙 — one ordinary forward pass plus one absolute-kernel pass, instead of two full sign-split sums. The conv peer of denseLo_uniform.

theorem Proofs.IBP.convHi_uniform {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (x : Tensor3 ic h w) (ε : ℝ) (o : Fin oc) (hI : Fin h) (wI : Fin w) :

convHi W b (fun (a : Fin ic) (b' : Fin h) (d : Fin w) => x a b' d - ε) (fun (a : Fin ic) (b' : Fin h) (d : Fin w) => x a b' d + ε) o hI wI = conv2d W b x o hI wI + ε * conv2d (absK W) (fun (x : Fin oc) => 0) (onesT ic h w) o hI wI

Uniform-box collapse, UPPER (sibling of convLo_uniform).