Chapter 3: MNIST 2D CNN (no BatchNorm) — whole-network VJP

The Chapter-3 demo model mnistCnnNoBn:

conv2d 1→c (relu) → conv2d c→c (relu) → maxPool 2×2 → flatten → dense (relu) → dense (relu) → dense (identity)

This file builds two things:

• mnistCnnNoBn_has_vjp_at — the structural whole-network VJP: the composed backward equals the pdiv-Jacobian VJP of the full forward pass, conditional on smoothness hypotheses (no ReLU kink / MaxPool tie at the running activations). The Chapter-3 sibling of cnn_has_vjp_at, minus BN and residual blocks.

• mnistMicroCnn_has_vjp_correct — a concrete tiny instance where every smoothness hypothesis is discharged (norm_num/explicit), so the statement is unconditional and still closes under the three-axiom kernel. The witness that the conditional machinery is instantiable.

noncomputable def Proofs.convRelu_has_vjp_at {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (v : Vec (ic * h * w)) (h_smooth : ∀ (k : Fin (oc * h * w)), flatConv W b v k ≠ 0) : HasVJPAt (relu (oc * h * w) ∘ flatConv W b) v

conv → relu block VJP at a smooth point (no BatchNorm). relu ∘ flatConv W b. The plain-conv analogue of convBnRelu_has_vjp_at — conv is linear (global VJP via the HasVJP3 bridge), relu carries the smoothness hypothesis.

Equations

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

theorem Proofs.convRelu_differentiableAt {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (v : Vec (ic * h * w)) (h_smooth : ∀ (k : Fin (oc * h * w)), flatConv W b v k ≠ 0) : DifferentiableAt ℝ (relu (oc * h * w) ∘ flatConv W b) v

relu ∘ flatConv W b is differentiable at a smooth point.

noncomputable def Proofs.denseRelu_has_vjp_at {m n : ℕ} (W : Mat m n) (b : Vec n) (v : Vec m) (h_smooth : ∀ (k : Fin n), dense W b v k ≠ 0) : HasVJPAt (relu n ∘ dense W b) v

dense → relu block VJP at a smooth point. relu ∘ dense W b.

Equations

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

theorem Proofs.denseRelu_differentiableAt {m n : ℕ} (W : Mat m n) (b : Vec n) (v : Vec m) (h_smooth : ∀ (k : Fin n), dense W b v k ≠ 0) : DifferentiableAt ℝ (relu n ∘ dense W b) v

relu ∘ dense W b is differentiable at a smooth point.

noncomputable def Proofs.mnistCnnNoBnForward {ic c h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c ic kH kW) (b₁ : Vec c) (W₂ : Kernel4 c c kH kW) (b₂ : Vec c) (W₃ : Mat (c * h * w) d1) (b₃ : Vec d1) (W₄ : Mat d1 d1) (b₄ : Vec d1) (W₅ : Mat d1 nClasses) (b₅ : Vec nClasses) : Vec (ic * (2 * h) * (2 * w)) → Vec nClasses

The Chapter-3 mnistCnnNoBn forward, in flattened Vec space. Conv stage runs at spatial (2*h, 2*w); the maxPool halves it to (h, w); then three dense layers (two with ReLU).

Equations

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

noncomputable def Proofs.mnistCnnNoBn_has_vjp_at {ic c h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c ic kH kW) (b₁ : Vec c) (W₂ : Kernel4 c c kH kW) (b₂ : Vec c) (W₃ : Mat (c * h * w) d1) (b₃ : Vec d1) (W₄ : Mat d1 d1) (b₄ : Vec d1) (W₅ : Mat d1 nClasses) (b₅ : Vec nClasses) (hc : 0 < c) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * h) * (2 * w))) (h1 : ∀ (k : Fin (c * (2 * h) * (2 * w))), flatConv W₁ b₁ x k ≠ 0) (h2 : ∀ (k : Fin (c * (2 * h) * (2 * w))), flatConv W₂ b₂ ((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x) k ≠ 0) (h_mp : MaxPool2Smooth (Tensor3.unflatten (((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₂ b₂) ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x))) (h3 : ∀ (k : Fin d1), dense W₃ b₃ (maxPoolFlat c h w (((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₂ b₂) ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x)) k ≠ 0) (h4 : ∀ (k : Fin d1), dense W₄ b₄ ((relu d1 ∘ dense W₃ b₃) (maxPoolFlat c h w (((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₂ b₂) ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x))) k ≠ 0) : HasVJPAt (mnistCnnNoBnForward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅) x

MNIST 2D CNN (no BN) whole-network VJP at a smooth point.

The composed backward of the full Chapter-3 forward equals the pdiv-contracted Jacobian (Jacobian-transpose applied to the cotangent), conditional on smoothness at the four ReLU kinks and the one MaxPool. Built by vjp_comp_at through convRelu → convRelu → maxPool → denseRelu → denseRelu → dense. The Chapter-3 sibling of cnn_has_vjp_at (BN-free, no resblocks).

Equations

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

theorem Proofs.mnistCnnNoBn_has_vjp_at_correct {ic c h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c ic kH kW) (b₁ : Vec c) (W₂ : Kernel4 c c kH kW) (b₂ : Vec c) (W₃ : Mat (c * h * w) d1) (b₃ : Vec d1) (W₄ : Mat d1 d1) (b₄ : Vec d1) (W₅ : Mat d1 nClasses) (b₅ : Vec nClasses) (hc : 0 < c) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * h) * (2 * w))) (h1 : ∀ (k : Fin (c * (2 * h) * (2 * w))), flatConv W₁ b₁ x k ≠ 0) (h2 : ∀ (k : Fin (c * (2 * h) * (2 * w))), flatConv W₂ b₂ ((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x) k ≠ 0) (h_mp : MaxPool2Smooth (Tensor3.unflatten (((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₂ b₂) ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x))) (h3 : ∀ (k : Fin d1), dense W₃ b₃ (maxPoolFlat c h w (((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₂ b₂) ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x)) k ≠ 0) (h4 : ∀ (k : Fin d1), dense W₄ b₄ ((relu d1 ∘ dense W₃ b₃) (maxPoolFlat c h w (((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₂ b₂) ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x))) k ≠ 0) (dy : Vec nClasses) (i : Fin (ic * (2 * h) * (2 * w))) : (mnistCnnNoBn_has_vjp_at W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ hc hh hw x h1 h2 h_mp h3 h4).backward dy i = ∑ j : Fin nClasses, pdiv (mnistCnnNoBnForward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅) x i j * dy j

Public correctness theorem for mnistCnnNoBn_has_vjp_at — the Chapter-3 CNN's backward equals the pdiv-contracted Jacobian.

A minimal mnistCnnNoBn at ic=c=h=w=d1=nClasses=1, 1×1 kernels, with hand-picked weights so the conv stack is the identity, every ReLU sees strictly-positive input, and the single MaxPool window has four distinct values. All five smoothness hypotheses of mnistCnnNoBn_has_vjp_at are then proved, yielding an unconditional whole-network VJP correctness theorem — the non-vacuity witness for the conditional capstone above.

noncomputable def Proofs.Micro.X0 : Vec (1 * (2 * 1) * (2 * 1))

Input Vec 4 with four distinct strictly-positive entries 1,2,3,4.

Equations

• Proofs.Micro.X0 k = ↑↑k + 1

noncomputable def Proofs.Micro.K1 : Kernel4 1 1 1 1

1×1×1×1 all-ones kernel ⇒ conv is the identity.

Equations

• Proofs.Micro.K1 x✝³ x✝² x✝¹ x✝ = 1

noncomputable def Proofs.Micro.Bz : Vec 1

Zero bias.

Equations

• Proofs.Micro.Bz x✝ = 0

noncomputable def Proofs.Micro.Wd : Mat (1 * 1 * 1) 1

All-ones dense weight (Mat 1 1).

Equations

• Proofs.Micro.Wd x✝¹ x✝ = 1

noncomputable def Proofs.Micro.B1 : Vec 1

Unit bias (keeps dense outputs strictly positive).

Equations

• Proofs.Micro.B1 x✝ = 1

theorem Proofs.Micro.conv2d_K1_id (t : Tensor3 1 (2 * 1) (2 * 1)) : conv2d K1 Bz t = t

The 1×1 ones-kernel conv2d is the identity.

theorem Proofs.Micro.flatConv_K1_id (v : Vec (1 * (2 * 1) * (2 * 1))) : flatConv K1 Bz v = v

Hence flatConv K1 Bz is the identity.

theorem Proofs.Micro.relu_pos {n : ℕ} (v : Vec n) (hv : ∀ (i : Fin n), 0 < v i) : relu n v = v

ReLU is the identity on strictly-positive vectors.

theorem Proofs.Micro.X0_pos (i : Fin (1 * (2 * 1) * (2 * 1))) : 0 < X0 i

theorem Proofs.Micro.X0_ge_one (i : Fin (1 * (2 * 1) * (2 * 1))) : 1 ≤ X0 i

theorem Proofs.Micro.CR_id (v : Vec (1 * (2 * 1) * (2 * 1))) (hv : ∀ (i : Fin (1 * (2 * 1) * (2 * 1))), 0 < v i) : (relu (1 * (2 * 1) * (2 * 1)) ∘ flatConv K1 Bz) v = v

The conv→relu block returns its (positive) input unchanged.

theorem Proofs.Micro.maxpool_input_eq : ((relu (1 * (2 * 1) * (2 * 1)) ∘ flatConv K1 Bz) ∘ relu (1 * (2 * 1) * (2 * 1)) ∘ flatConv K1 Bz) X0 = X0

Two conv→relu blocks on X0 collapse back to X0 (the MaxPool input).

theorem Proofs.Micro.mp_smooth_X0 : MaxPool2Smooth (Tensor3.unflatten X0)

The single 2×2 MaxPool window of X0 has four distinct values.

theorem Proofs.Micro.maxPoolFlat_X0_ge_one (k : Fin (1 * 1 * 1)) : 1 ≤ maxPoolFlat 1 1 1 X0 k

The pooled value is ≥ 1 (so the dense head stays nonzero).

theorem Proofs.Micro.dense_Wd_pos (u : Vec (1 * 1 * 1)) (hu : ∀ (j : Fin (1 * 1 * 1)), 0 < u j) (k : Fin 1) : 0 < dense Wd B1 u k

dense Wd B1 (ones weight, unit bias) maps a positive vector to a strictly-positive one. The dense head stays off the ReLU kink.

theorem Proofs.Micro.maxPoolFlat_X0_pos (j : Fin (1 * 1 * 1)) : 0 < maxPoolFlat 1 1 1 X0 j

The pooled vector is strictly positive (feeds the dense head).

noncomputable def Proofs.Micro.mnistMicroCnn_has_vjp_at : HasVJPAt (mnistCnnNoBnForward K1 Bz K1 Bz Wd B1 Wd B1 Wd Bz) X0

Unconditional whole-network VJP for a concrete tiny CNN. Every smoothness hypothesis of mnistCnnNoBn_has_vjp_at is discharged here, so this statement carries no side conditions.

Equations

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

theorem Proofs.Micro.mnistMicroCnn_has_vjp_correct (dy : Vec 1) (i : Fin (1 * (2 * 1) * (2 * 1))) : mnistMicroCnn_has_vjp_at.backward dy i = ∑ j : Fin 1, pdiv (mnistCnnNoBnForward K1 Bz K1 Bz Wd B1 Wd B1 Wd Bz) X0 i j * dy j

Public unconditional correctness theorem — the concrete tiny CNN's backward equals the pdiv-Jacobian VJP, no hypotheses.

theorem Proofs.maxPool2Smooth_of_injective {c h w : ℕ} (x : Tensor3 c (2 * h) (2 * w)) (hinj : ∀ (ci : Fin c) (r r' : Fin (2 * h)) (s s' : Fin (2 * w)), x ci r s = x ci r' s' → r = r' ∧ s = s') : MaxPool2Smooth x

Positional injectivity ⇒ MaxPool2Smooth. If, on each channel, the position map (r, s) ↦ x ci r s is injective, then every 2×2 window has pairwise-distinct values. One injectivity argument in place of 6·c·h·w per-window decides.

theorem Proofs.flatten_pos_of_pos {c h w : ℕ} {T : Tensor3 c h w} (hT : ∀ (ci : Fin c) (hi : Fin h) (wi : Fin w), 0 < T ci hi wi) (k : Fin (c * h * w)) : 0 < T.flatten k

A tensor that is positive everywhere flattens to a positive vector (flatten T k just reads T at the decoded index). Discharges the ReLU ∀ k, … ≠ 0 conditions once the layer is shown positive.

theorem Proofs.maxPool2_pos {c h w : ℕ} {x : Tensor3 c (2 * h) (2 * w)} (hx : ∀ (ci : Fin c) (r : Fin (2 * h)) (s : Fin (2 * w)), 0 < x ci r s) (ci : Fin c) (hi : Fin h) (wi : Fin w) : 0 < maxPool2 x ci hi wi

A 2×2 max-pool of an everywhere-positive tensor is positive (the max dominates the top-left cell).

theorem Proofs.relu_id_of_pos {n : ℕ} {v : Vec n} (hv : ∀ (i : Fin n), 0 < v i) : relu n v = v

ReLU is the identity on a strictly-positive vector. Discharges the ReLU-as-identity steps that fold the composition into a plain conv stack at a smooth (everywhere-positive) point.

theorem Proofs.dense_pos_of_nonneg {m n : ℕ} {W : Mat m n} {b : Vec n} {u : Vec m} (hW : ∀ (i : Fin m) (j : Fin n), 0 ≤ W i j) (hb : ∀ (j : Fin n), 0 < b j) (hu : ∀ (i : Fin m), 0 ≤ u i) (j : Fin n) : 0 < dense W b u j

A dense layer with nonnegative weights, a strictly-positive bias, and a nonnegative input is strictly positive — the propagating positivity invariant that discharges the dense ReLU ≠ 0 conditions without per-coordinate case analysis.

theorem Proofs.conv2d_1x1 {ic oc h w : ℕ} (W : Kernel4 oc ic 1 1) (b : Vec oc) (t : Tensor3 ic h w) (o : Fin oc) (hi : Fin h) (wi : Fin w) : conv2d W b t o hi wi = b o + ∑ c : Fin ic, W o c 0 0 * t c hi wi

1×1 conv collapses to a per-pixel channel mix. With a 1×1 kernel (SAME padding is a no-op), conv2d at each pixel is just the bias plus a channel-weighted sum of that same pixel — the closed form a center-structured instance computes its forward pass with.

theorem Proofs.conv2d_center3x3 {ic oc h w : ℕ} (W : Kernel4 oc ic 3 3) (b : Vec oc) (hW : ∀ (o : Fin oc) (c : Fin ic) (kh kw : Fin 3), ¬(kh = 1 ∧ kw = 1) → W o c kh kw = 0) (t : Tensor3 ic h w) (o : Fin oc) (hi : Fin h) (wi : Fin w) : conv2d W b t o hi wi = b o + ∑ c : Fin ic, W o c 1 1 * t c hi wi

3×3 conv with a center-only kernel collapses to a per-pixel channel mix. If W vanishes off the center tap (1,1), the full 3×3 SAME-padding sum — all nine taps and their padding branches — reduces to b o + ∑ c, W o c 1 1 · t c hi wi. The 3×3 analogue of conv2d_1x1: a center-structured instance exercises genuine spatial convolution (the padding ifs are evaluated) while keeping a closed forward form.

noncomputable def Proofs.Mini.T0 : Tensor3 1 (2 * 2) (2 * 2)

Input tensor with 16 distinct strictly-positive integer values, so (hi, wi) ↦ T0 0 hi wi is injective in position.

Equations

• Proofs.Mini.T0 x✝ hi wi = ↑(4 * ↑hi + ↑wi + 1)

noncomputable def Proofs.Mini.X : Vec (1 * (2 * 2) * (2 * 2))

Whole-network input, the flattened T0.

Equations

• Proofs.Mini.X = Proofs.Mini.T0.flatten

noncomputable def Proofs.Mini.W1 : Kernel4 2 1 1 1

conv1: 1→2 channels, 1×1, unit tap.

Equations

• Proofs.Mini.W1 x✝³ x✝² x✝¹ x✝ = 1

noncomputable def Proofs.Mini.b1 : Vec 2

conv1 bias (1, 2) — gives the two output channels distinct values.

Equations

• Proofs.Mini.b1 o = if o = 0 then 1 else 2

noncomputable def Proofs.Mini.W2 : Kernel4 2 2 1 1

conv2: 2→2 channels, 1×1. Row depends on the output channel (1 for channel 0, 2 for channel 1), so the two output channels differ and each has a strictly-positive input-pixel coefficient.

Equations

• Proofs.Mini.W2 o x✝² x✝¹ x✝ = if o = 0 then 1 else 2

noncomputable def Proofs.Mini.b2 : Vec 2

conv2 bias.

Equations

• Proofs.Mini.b2 x✝ = 1

noncomputable def Proofs.Mini.W3 : Mat (2 * 2 * 2) 3

Dense heads: nonnegative weights + strictly-positive biases keep every activation off the ReLU kink.

Equations

• Proofs.Mini.W3 x✝¹ x✝ = 1

noncomputable def Proofs.Mini.b3 : Vec 3

Equations

• Proofs.Mini.b3 x✝ = 1

noncomputable def Proofs.Mini.W4 : Mat 3 3

Equations

• Proofs.Mini.W4 x✝¹ x✝ = 1

noncomputable def Proofs.Mini.b4 : Vec 3

Equations

• Proofs.Mini.b4 x✝ = 1

noncomputable def Proofs.Mini.W5 : Mat 3 10

Equations

• Proofs.Mini.W5 x✝¹ x✝ = 1

noncomputable def Proofs.Mini.b5 : Vec 10

Equations

• Proofs.Mini.b5 x✝ = 0

theorem Proofs.Mini.conv1_eq (o : Fin 2) (hi wi : Fin (2 * 2)) : conv2d W1 b1 T0 o hi wi = b1 o + T0 0 hi wi

conv1 in closed form: bias plus the (unit-tap) input pixel.

theorem Proofs.Mini.conv1_pos (o : Fin 2) (hi wi : Fin (2 * 2)) : 0 < conv2d W1 b1 T0 o hi wi

conv1 is everywhere positive (bias ≥ 1, pixel ≥ 0).

theorem Proofs.Mini.conv2_eq (o : Fin 2) (hi wi : Fin (2 * 2)) : conv2d W2 b2 (conv2d W1 b1 T0) o hi wi = b2 o + (W2 o 0 0 0 * (b1 0 + T0 0 hi wi) + W2 o 1 0 0 * (b1 1 + T0 0 hi wi))

conv2 ∘ conv1 in closed form.

theorem Proofs.Mini.conv2_pos (o : Fin 2) (hi wi : Fin (2 * 2)) : 0 < conv2d W2 b2 (conv2d W1 b1 T0) o hi wi

conv2 ∘ conv1 is everywhere positive.

theorem Proofs.Mini.poolTensor_inj (ci : Fin 2) (r r' s s' : Fin (2 * 2)) (heq : conv2d W2 b2 (conv2d W1 b1 T0) ci r s = conv2d W2 b2 (conv2d W1 b1 T0) ci r' s') : r = r' ∧ s = s'

The max-pool input (conv2 ∘ conv1) is positionally injective on each channel: distinct positions give distinct values (the conv stack is affine with a strictly-positive coefficient on the injective input).

theorem Proofs.Mini.flatConv1_eq : flatConv W1 b1 X = (conv2d W1 b1 T0).flatten

flatConv W1 b1 X = flatten (conv2d W1 b1 T0) (the input round-trips through unflatten ∘ flatten).

theorem Proofs.Mini.convZ_eq : flatConv W2 b2 (conv2d W1 b1 T0).flatten = (conv2d W2 b2 (conv2d W1 b1 T0)).flatten

Second conv layer, post unflatten/flatten round-trip.

theorem Proofs.Mini.block1_eq : (relu (2 * (2 * 2) * (2 * 2)) ∘ flatConv W1 b1) X = (conv2d W1 b1 T0).flatten

First conv→relu block: ReLU is the identity (conv1 is positive).

theorem Proofs.Mini.blockZ_eq : ((relu (2 * (2 * 2) * (2 * 2)) ∘ flatConv W2 b2) ∘ relu (2 * (2 * 2) * (2 * 2)) ∘ flatConv W1 b1) X = (conv2d W2 b2 (conv2d W1 b1 T0)).flatten

Both conv→relu blocks fold (ReLUs are identities) to the flattened conv2 ∘ conv1 — the tensor handed to max-pool.

theorem Proofs.Mini.pooled_eq : maxPoolFlat 2 2 2 (conv2d W2 b2 (conv2d W1 b1 T0)).flatten = (maxPool2 (conv2d W2 b2 (conv2d W1 b1 T0))).flatten

The pooled vector in closed form.

theorem Proofs.Mini.pooled_pos (i : Fin (2 * 2 * 2)) : 0 < maxPoolFlat 2 2 2 (conv2d W2 b2 (conv2d W1 b1 T0)).flatten i

The pooled vector is everywhere positive.

theorem Proofs.Mini.dense3_pos (j : Fin 3) : 0 < dense W3 b3 (maxPoolFlat 2 2 2 (conv2d W2 b2 (conv2d W1 b1 T0)).flatten) j

The first dense layer's output is everywhere positive.

noncomputable def Proofs.Mini.miniCnn_has_vjp_at : HasVJPAt (mnistCnnNoBnForward W1 b1 W2 b2 W3 b3 W4 b4 W5 b5) X

Unconditional whole-network VJP for a multi-channel, multi-window, 10-class CNN. Every smoothness hypothesis of mnistCnnNoBn_has_vjp_at is discharged — the no-tie condition via maxPool2Smooth_of_injective, the ReLU conditions via positivity — so the statement carries no side conditions and stays in the three-axiom closure.

Equations

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

theorem Proofs.Mini.miniCnn_has_vjp_correct (dy : Vec 10) (i : Fin (1 * (2 * 2) * (2 * 2))) : miniCnn_has_vjp_at.backward dy i = ∑ j : Fin 10, pdiv (mnistCnnNoBnForward W1 b1 W2 b2 W3 b3 W4 b4 W5 b5) X i j * dy j

Public unconditional correctness theorem — the Tier-1 CNN's backward equals the pdiv-Jacobian VJP, no hypotheses.

noncomputable def Proofs.Spatial.T0 : Tensor3 1 (2 * 2) (2 * 2)

Input tensor, 16 distinct strictly-positive values (positionally injective).

Equations

• Proofs.Spatial.T0 x✝ hi wi = ↑(4 * ↑hi + ↑wi + 1)

noncomputable def Proofs.Spatial.X : Vec (1 * (2 * 2) * (2 * 2))

Equations

• Proofs.Spatial.X = Proofs.Spatial.T0.flatten

noncomputable def Proofs.Spatial.W1 : Kernel4 2 1 3 3

conv1: 1→2 channels, 3×3, center tap 1, zero elsewhere.

Equations

• Proofs.Spatial.W1 x✝¹ x✝ kh kw = if kh = 1 ∧ kw = 1 then 1 else 0

noncomputable def Proofs.Spatial.b1 : Vec 2

Equations

• Proofs.Spatial.b1 o = if o = 0 then 1 else 2

noncomputable def Proofs.Spatial.W2 : Kernel4 2 2 3 3

conv2: 2→2 channels, 3×3, center tap depends on the output channel (1 for channel 0, 2 for channel 1), zero elsewhere.

Equations

• Proofs.Spatial.W2 o x✝ kh kw = if kh = 1 ∧ kw = 1 then if o = 0 then 1 else 2 else 0

noncomputable def Proofs.Spatial.b2 : Vec 2

Equations

• Proofs.Spatial.b2 x✝ = 1

noncomputable def Proofs.Spatial.W3 : Mat (2 * 2 * 2) 3

Equations

• Proofs.Spatial.W3 x✝¹ x✝ = 1

noncomputable def Proofs.Spatial.b3 : Vec 3

Equations

• Proofs.Spatial.b3 x✝ = 1

noncomputable def Proofs.Spatial.W4 : Mat 3 3

Equations

• Proofs.Spatial.W4 x✝¹ x✝ = 1

noncomputable def Proofs.Spatial.b4 : Vec 3

Equations

• Proofs.Spatial.b4 x✝ = 1

noncomputable def Proofs.Spatial.W5 : Mat 3 10

Equations

• Proofs.Spatial.W5 x✝¹ x✝ = 1

noncomputable def Proofs.Spatial.b5 : Vec 10

Equations

• Proofs.Spatial.b5 x✝ = 0

theorem Proofs.Spatial.hW1 (o : Fin 2) (c : Fin 1) (kh kw : Fin 3) (hne : ¬(kh = 1 ∧ kw = 1)) : W1 o c kh kw = 0

conv1 vanishes off the center tap (the conv2d_center3x3 hypothesis).

theorem Proofs.Spatial.hW2 (o c : Fin 2) (kh kw : Fin 3) (hne : ¬(kh = 1 ∧ kw = 1)) : W2 o c kh kw = 0

theorem Proofs.Spatial.W1_center (o : Fin 2) (c : Fin 1) : W1 o c 1 1 = 1

conv1 center tap is 1.

theorem Proofs.Spatial.conv1_eq (o : Fin 2) (hi wi : Fin (2 * 2)) : conv2d W1 b1 T0 o hi wi = b1 o + T0 0 hi wi

conv1 in closed form.

theorem Proofs.Spatial.conv1_pos (o : Fin 2) (hi wi : Fin (2 * 2)) : 0 < conv2d W1 b1 T0 o hi wi

theorem Proofs.Spatial.conv2_eq (o : Fin 2) (hi wi : Fin (2 * 2)) : conv2d W2 b2 (conv2d W1 b1 T0) o hi wi = b2 o + (W2 o 0 1 1 * (b1 0 + T0 0 hi wi) + W2 o 1 1 1 * (b1 1 + T0 0 hi wi))

conv2 ∘ conv1 in closed form.

theorem Proofs.Spatial.conv2_pos (o : Fin 2) (hi wi : Fin (2 * 2)) : 0 < conv2d W2 b2 (conv2d W1 b1 T0) o hi wi

theorem Proofs.Spatial.poolTensor_inj (ci : Fin 2) (r r' s s' : Fin (2 * 2)) (heq : conv2d W2 b2 (conv2d W1 b1 T0) ci r s = conv2d W2 b2 (conv2d W1 b1 T0) ci r' s') : r = r' ∧ s = s'

The max-pool input is positionally injective on each channel.

theorem Proofs.Spatial.flatConv1_eq : flatConv W1 b1 X = (conv2d W1 b1 T0).flatten

theorem Proofs.Spatial.convZ_eq : flatConv W2 b2 (conv2d W1 b1 T0).flatten = (conv2d W2 b2 (conv2d W1 b1 T0)).flatten

theorem Proofs.Spatial.block1_eq : (relu (2 * (2 * 2) * (2 * 2)) ∘ flatConv W1 b1) X = (conv2d W1 b1 T0).flatten

theorem Proofs.Spatial.blockZ_eq : ((relu (2 * (2 * 2) * (2 * 2)) ∘ flatConv W2 b2) ∘ relu (2 * (2 * 2) * (2 * 2)) ∘ flatConv W1 b1) X = (conv2d W2 b2 (conv2d W1 b1 T0)).flatten

theorem Proofs.Spatial.pooled_eq : maxPoolFlat 2 2 2 (conv2d W2 b2 (conv2d W1 b1 T0)).flatten = (maxPool2 (conv2d W2 b2 (conv2d W1 b1 T0))).flatten

theorem Proofs.Spatial.pooled_pos (i : Fin (2 * 2 * 2)) : 0 < maxPoolFlat 2 2 2 (conv2d W2 b2 (conv2d W1 b1 T0)).flatten i

theorem Proofs.Spatial.dense3_pos (j : Fin 3) : 0 < dense W3 b3 (maxPoolFlat 2 2 2 (conv2d W2 b2 (conv2d W1 b1 T0)).flatten) j

noncomputable def Proofs.Spatial.spatialCnn_has_vjp_at : HasVJPAt (mnistCnnNoBnForward W1 b1 W2 b2 W3 b3 W4 b4 W5 b5) X

Unconditional whole-network VJP for a 3×3-convolution CNN. Same shape as Mini.miniCnn (2 channels, eight pool windows, 10 classes) but with genuine 3×3 SAME-padding convolutions, every smoothness hypothesis discharged, inside the three-axiom closure.

Equations

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

theorem Proofs.Spatial.spatialCnn_has_vjp_correct (dy : Vec 10) (i : Fin (1 * (2 * 2) * (2 * 2))) : spatialCnn_has_vjp_at.backward dy i = ∑ j : Fin 10, pdiv (mnistCnnNoBnForward W1 b1 W2 b2 W3 b3 W4 b4 W5 b5) X i j * dy j

Public unconditional correctness theorem — the 3×3-conv CNN's backward equals the pdiv-Jacobian VJP, no hypotheses.

noncomputable def Proofs.MlpConcrete.W₀ : Mat 2 2

A concrete 3-layer MLP (dense → relu → dense → relu → dense) with all-ones weights/biases and a positive input. Every ReLU pre-activation is then strictly positive (hence ≠ 0), so both smoothness hypotheses of mlp_has_vjp_at discharge. The net is non-constant, so this is a live witness (non-trivial Jacobian), not a degenerate one. The Chapter-2 analogue of the Micro/Mini/Spatial CNN instances.

Equations

• Proofs.MlpConcrete.W₀ x✝¹ x✝ = 1

noncomputable def Proofs.MlpConcrete.b₀ : Vec 2

Equations

• Proofs.MlpConcrete.b₀ x✝ = 1

noncomputable def Proofs.MlpConcrete.W₁ : Mat 2 2

Equations

• Proofs.MlpConcrete.W₁ x✝¹ x✝ = 1

noncomputable def Proofs.MlpConcrete.b₁ : Vec 2

Equations

• Proofs.MlpConcrete.b₁ x✝ = 1

noncomputable def Proofs.MlpConcrete.W₂ : Mat 2 2

Equations

• Proofs.MlpConcrete.W₂ x✝¹ x✝ = 1

noncomputable def Proofs.MlpConcrete.b₂ : Vec 2

Equations

• Proofs.MlpConcrete.b₂ x✝ = 1

noncomputable def Proofs.MlpConcrete.x : Vec 2

Equations

• Proofs.MlpConcrete.x x✝ = 1

theorem Proofs.MlpConcrete.preact0_pos (k : Fin 2) : 0 < dense W₀ b₀ x k

First-layer pre-activation is strictly positive at every coordinate.

noncomputable def Proofs.MlpConcrete.mlpConcrete_has_vjp_at : HasVJPAt (mlpForward W₀ b₀ W₁ b₁ W₂ b₂) x

Unconditional whole-network VJP for a concrete 3-layer MLP. Both ReLU ≠ 0 hypotheses are discharged via dense_pos_of_nonneg (positive bias + nonnegative weights/input propagate strict positivity), with relu_id_of_pos collapsing the inner ReLU.

Equations

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

theorem Proofs.MlpConcrete.mlpConcrete_has_vjp_correct (dy : Vec 2) (i : Fin 2) : mlpConcrete_has_vjp_at.backward dy i = ∑ j : Fin 2, pdiv (mlpForward W₀ b₀ W₁ b₁ W₂ b₂) x i j * dy j

Public unconditional correctness theorem — the concrete MLP's backward equals the pdiv-Jacobian VJP, no hypotheses.

theorem Proofs.bnForward_gamma_zero {n : ℕ} (ε β : ℝ) (v : Vec n) : bnForward n ε 0 β v = fun (x : Fin n) => β

BN with γ = 0 collapses to the constant shift β (no input constraint) — discharges the resblock smoothness conditions, whose BN inputs need not be constant.

noncomputable def Proofs.CnnConcrete.Ws : Kernel4 1 1 1 1

Equations

• Proofs.CnnConcrete.Ws x✝³ x✝² x✝¹ x✝ = 1

noncomputable def Proofs.CnnConcrete.bs : Vec 1

Equations

• Proofs.CnnConcrete.bs x✝ = 0

noncomputable def Proofs.CnnConcrete.X : Vec (1 * (2 * 1) * (2 * 1))

Equations

• Proofs.CnnConcrete.X i = ↑↑i

noncomputable def Proofs.CnnConcrete.W₁ : Kernel4 1 1 1 1

Equations

• Proofs.CnnConcrete.W₁ x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.CnnConcrete.b₁ : Vec 1

Equations

• Proofs.CnnConcrete.b₁ x✝ = 0

noncomputable def Proofs.CnnConcrete.W₂ : Kernel4 1 1 1 1

Equations

• Proofs.CnnConcrete.W₂ x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.CnnConcrete.b₂ : Vec 1

Equations

• Proofs.CnnConcrete.b₂ x✝ = 0

noncomputable def Proofs.CnnConcrete.W₁' : Kernel4 1 1 1 1

Equations

• Proofs.CnnConcrete.W₁' x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.CnnConcrete.b₁' : Vec 1

Equations

• Proofs.CnnConcrete.b₁' x✝ = 0

noncomputable def Proofs.CnnConcrete.W₂' : Kernel4 1 1 1 1

Equations

• Proofs.CnnConcrete.W₂' x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.CnnConcrete.b₂' : Vec 1

Equations

• Proofs.CnnConcrete.b₂' x✝ = 0

noncomputable def Proofs.CnnConcrete.Wp : Kernel4 1 1 1 1

Equations

• Proofs.CnnConcrete.Wp x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.CnnConcrete.bp : Vec 1

Equations

• Proofs.CnnConcrete.bp x✝ = 0

noncomputable def Proofs.CnnConcrete.Wd : Mat 1 2

Equations

• Proofs.CnnConcrete.Wd x✝¹ x✝ = 0

noncomputable def Proofs.CnnConcrete.bd : Vec 2

Equations

• Proofs.CnnConcrete.bd x✝ = 0

theorem Proofs.CnnConcrete.flatConvWs : flatConv Ws bs X = X

The 1×1 identity stem conv is the identity on the (flattened) input.

theorem Proofs.CnnConcrete.bnMeanX : bnMean (1 * (2 * 1) * (2 * 1)) X = 3 / 2

theorem Proofs.CnnConcrete.bnVarX : bnVar (1 * (2 * 1) * (2 * 1)) X = 5 / 4

theorem Proofs.CnnConcrete.bnIstdX : bnIstd (1 * (2 * 1) * (2 * 1)) X (11 / 4) = 1 / 2

theorem Proofs.CnnConcrete.bnX_eq (k : Fin (1 * (2 * 1) * (2 * 1))) : bnForward (1 * (2 * 1) * (2 * 1)) (11 / 4) 1 10 X k = (X k - 3 / 2) * (1 / 2) + 10

theorem Proofs.CnnConcrete.bnX_pos (k : Fin (1 * (2 * 1) * (2 * 1))) : 0 < bnForward (1 * (2 * 1) * (2 * 1)) (11 / 4) 1 10 X k

theorem Proofs.CnnConcrete.bnX_inj : Function.Injective (bnForward (1 * (2 * 1) * (2 * 1)) (11 / 4) 1 10 X)

theorem Proofs.CnnConcrete.cbrX : cbr Ws bs (11 / 4) 1 10 X = bnForward (1 * (2 * 1) * (2 * 1)) (11 / 4) 1 10 X

cbr X collapses to bn X (identity conv, then relu of a positive).

noncomputable def Proofs.CnnConcrete.cnnConcrete_has_vjp_at : HasVJPAt (cnnForward Ws bs (11 / 4) 1 10 W₁ b₁ W₂ b₂ 1 0 1 1 0 1 W₁' b₁' W₂' b₂' Wp bp 1 0 1 1 0 1 1 0 1 Wd bd) X

Whole-network VJP for a concrete ResNet-style CNN with BatchNorm — every smoothness hypothesis discharged: the stem produces distinct positive BN outputs (so maxpool has no ties and bn ≠ 0), and the resblock BNs use γ=0 (constant).

Equations

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

theorem Proofs.CnnConcrete.cnnConcrete_has_vjp_correct (dy : Vec 2) (i : Fin (1 * (2 * 1) * (2 * 1))) : cnnConcrete_has_vjp_at.backward dy i = ∑ j : Fin 2, pdiv (cnnForward Ws bs (11 / 4) 1 10 W₁ b₁ W₂ b₂ 1 0 1 1 0 1 W₁' b₁' W₂' b₂' Wp bp 1 0 1 1 0 1 1 0 1 Wd bd) X i j * dy j

Public unconditional correctness theorem — the concrete CNN's backward equals the pdiv-Jacobian VJP, no hypotheses.