Documentation

LeanMlir.Proofs.Training.TrainedCnnWitness

Trained-weight whole-network VJP witness — CNN rung #

The TrainedMlpWitness program extended to a CONVOLUTIONAL net (the 2026-07 audit's gap #3): the Chapter-3 mnistCnnNoBn conditional whole-net VJP (mnistCnnNoBn_has_vjp_at) instantiated at TRAINED, /128-rationalized weights and a REAL test input, with every smoothness hypothesis discharged by exact in-kernel rational arithmetic — inherited from training, not engineered:

h1/h2 — all 72+72 conv pre-activations are nonzero (conv1_eq/conv2_eq value tables + c1_ne/c2_ne);
h_mp — every 2×2 max-pool window of relu(conv2) has four pairwise-distinct values (r2_smooth). ReLU zeros collide, so this needs ≤ 1 negative conv2 pre-activation per window — trained in via a pool-tie margin regularizer (the h_mp analogue of the scorecard's spectral cap: the training method decides whether the hypotheses hold);
h3/h4 — the dense pre-activations are nonzero (d3_ne/d4_ne).

Net: 24×24-center-cropped MNIST, 4×4-average-pooled to 6×6 (exact pixel sums /4080), conv 1→2 3×3 SAME → relu → conv 2→2 3×3 SAME → relu → maxpool 2×2 → dense 18→8 → relu → dense 8→8 → relu → dense 8→10. Float test acc 0.852, /128-quantized 0.850. Witness: test digit #0 (label 7, correctly classified). Generated by scripts/trained_cnn_witness.py; weights/input are DATA here.

noncomputable def Proofs.TrainedCnn.T0 :

Test image #0, 4×4-pooled 6×6, exact pixel sums /4080.

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.X :

Vec (1 * (2 * 3) * (2 * 3))

The flattened witness input.

Equations

Proofs.TrainedCnn.X = Proofs.TrainedCnn.T0.flatten

Instances For

noncomputable def Proofs.TrainedCnn.W1 :

Kernel4 2 1 3 3

conv1 kernel (1→2, 3×3), entries k/128.

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.b1 :

Equations

Proofs.TrainedCnn.b1 = ![9 / 128, 1 / 128]

Instances For

noncomputable def Proofs.TrainedCnn.W2 :

Kernel4 2 2 3 3

conv2 kernel (2→2, 3×3), entries k/128.

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.b2 :

Equations

Proofs.TrainedCnn.b2 = ![5 / 16, 19 / 128]

Instances For

noncomputable def Proofs.TrainedCnn.W3 :

Mat (2 * 3 * 3) 8

dense3 (18→8, input×output).

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.b3 :

Equations

Proofs.TrainedCnn.b3 = ![93 / 128, -3 / 64, -53 / 64, -1 / 4, 1 / 4, 1 / 16, 91 / 128, 3 / 16]

Instances For

noncomputable def Proofs.TrainedCnn.W4 :

Mat 8 8

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.b4 :

Equations

Proofs.TrainedCnn.b4 = ![27 / 128, 31 / 64, 71 / 64, -67 / 128, 25 / 128, -49 / 128, 13 / 128, 33 / 128]

Instances For

noncomputable def Proofs.TrainedCnn.W5 :

Mat 8 10

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.b5 :

Vec 10

Equations

Proofs.TrainedCnn.b5 = ![-49 / 128, 41 / 32, -85 / 128, -81 / 128, 123 / 128, 39 / 32, 7 / 64, -31 / 128, -151 / 128, -15 / 32]

Instances For

theorem Proofs.TrainedCnn.relu_flatten {c h w : ℕ} (T : Tensor3 c h w) :

relu (c * h * w) T.flatten = Tensor3.flatten fun (ci : Fin c) (hi : Fin h) (wi : Fin w) => if T ci hi wi > 0 then T ci hi wi else 0

ReLU commutes with Tensor3.flatten (both are pointwise).

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

T.flatten k ≠ 0

A nowhere-zero tensor flattens to a nowhere-zero vector.

noncomputable def Proofs.TrainedCnn.c1V :

Fin 2 → Fin 6 → Fin 6 → ℝ

conv1 pre-activations at the witness, exact.

Equations

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

Instances For

theorem Proofs.TrainedCnn.conv1_eq_r00 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r01 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r02 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r03 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r04 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r05 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r10 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r11 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r12 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r13 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r14 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq_r15 (wi : Fin 6) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv1_eq (o : Fin 2) (hi wi : Fin 6) :

conv2d W1 b1 T0 o hi wi = c1V o hi wi

theorem Proofs.TrainedCnn.c1_ne (o : Fin 2) (hi wi : Fin 6) :

c1V o hi wi ≠ 0

noncomputable def Proofs.TrainedCnn.z1V :

relu(conv1) at the witness, exact.

Equations

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

Instances For

theorem Proofs.TrainedCnn.z1_eq :

(fun (o : Fin 2) (hi wi : Fin 6) => if c1V o hi wi > 0 then c1V o hi wi else 0) = z1V

theorem Proofs.TrainedCnn.block1_eq :

(relu (2 * (2 * 3) * (2 * 3)) ∘ flatConv W1 b1) X = z1V.flatten

First conv→relu block at the witness = the exact table.

noncomputable def Proofs.TrainedCnn.c2V :

Fin 2 → Fin 6 → Fin 6 → ℝ

conv2 pre-activations at the witness, exact.

Equations

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

Instances For

theorem Proofs.TrainedCnn.conv2_eq_r00 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r01 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r02 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r03 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r04 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r05 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r10 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r11 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r12 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r13 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r14 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq_r15 (wi : Fin 6) :

conv2d W2 b2 z1V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi

theorem Proofs.TrainedCnn.conv2_eq (o : Fin 2) (hi wi : Fin 6) :

conv2d W2 b2 z1V o hi wi = c2V o hi wi

theorem Proofs.TrainedCnn.c2_ne (o : Fin 2) (hi wi : Fin 6) :

c2V o hi wi ≠ 0

noncomputable def Proofs.TrainedCnn.r2V :

relu(conv2) at the witness (the max-pool input), exact.

Equations

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

Instances For

theorem Proofs.TrainedCnn.r2_eq :

(fun (o : Fin 2) (hi wi : Fin 6) => if c2V o hi wi > 0 then c2V o hi wi else 0) = r2V

theorem Proofs.TrainedCnn.blockZ_eq :

((relu (2 * (2 * 3) * (2 * 3)) ∘ flatConv W2 b2) ∘ relu (2 * (2 * 3) * (2 * 3)) ∘ flatConv W1 b1) X = r2V.flatten

Both conv→relu blocks fold to the exact max-pool input table.

theorem Proofs.TrainedCnn.r2sm_c0h0 (wo : Fin 3) (ab ab' : Fin 2 × Fin 2) :

ab ≠ ab' → r2V ⟨0, ⋯⟩ (winRowInv ⟨0, ⋯⟩ ab.1) (winColInv wo ab.2) ≠ r2V ⟨0, ⋯⟩ (winRowInv ⟨0, ⋯⟩ ab'.1) (winColInv wo ab'.2)

theorem Proofs.TrainedCnn.r2sm_c0h1 (wo : Fin 3) (ab ab' : Fin 2 × Fin 2) :

ab ≠ ab' → r2V ⟨0, ⋯⟩ (winRowInv ⟨1, ⋯⟩ ab.1) (winColInv wo ab.2) ≠ r2V ⟨0, ⋯⟩ (winRowInv ⟨1, ⋯⟩ ab'.1) (winColInv wo ab'.2)

theorem Proofs.TrainedCnn.r2sm_c0h2 (wo : Fin 3) (ab ab' : Fin 2 × Fin 2) :

ab ≠ ab' → r2V ⟨0, ⋯⟩ (winRowInv ⟨2, ⋯⟩ ab.1) (winColInv wo ab.2) ≠ r2V ⟨0, ⋯⟩ (winRowInv ⟨2, ⋯⟩ ab'.1) (winColInv wo ab'.2)

theorem Proofs.TrainedCnn.r2sm_c1h0 (wo : Fin 3) (ab ab' : Fin 2 × Fin 2) :

ab ≠ ab' → r2V ⟨1, ⋯⟩ (winRowInv ⟨0, ⋯⟩ ab.1) (winColInv wo ab.2) ≠ r2V ⟨1, ⋯⟩ (winRowInv ⟨0, ⋯⟩ ab'.1) (winColInv wo ab'.2)

theorem Proofs.TrainedCnn.r2sm_c1h1 (wo : Fin 3) (ab ab' : Fin 2 × Fin 2) :

ab ≠ ab' → r2V ⟨1, ⋯⟩ (winRowInv ⟨1, ⋯⟩ ab.1) (winColInv wo ab.2) ≠ r2V ⟨1, ⋯⟩ (winRowInv ⟨1, ⋯⟩ ab'.1) (winColInv wo ab'.2)

theorem Proofs.TrainedCnn.r2sm_c1h2 (wo : Fin 3) (ab ab' : Fin 2 × Fin 2) :

ab ≠ ab' → r2V ⟨1, ⋯⟩ (winRowInv ⟨2, ⋯⟩ ab.1) (winColInv wo ab.2) ≠ r2V ⟨1, ⋯⟩ (winRowInv ⟨2, ⋯⟩ ab'.1) (winColInv wo ab'.2)

theorem Proofs.TrainedCnn.r2_smooth :

MaxPool2Smooth r2V

Every 2×2 window of relu(conv2) has pairwise-distinct values — the MaxPool2Smooth hypothesis, discharged from the trained tables.

noncomputable def Proofs.TrainedCnn.p2f :

Vec (2 * 3 * 3)

The pooled feature vector (flattened maxpool output), exact.

Equations

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

Instances For

theorem Proofs.TrainedCnn.pooled_eq :

maxPoolFlat 2 3 3 r2V.flatten = p2f

noncomputable def Proofs.TrainedCnn.d3V :

Fin 8 → ℝ

dense3 pre-activations at the witness, exact.

Equations

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

Instances For

theorem Proofs.TrainedCnn.d3_eq (k : Fin 8) :

dense W3 b3 p2f k = d3V k

theorem Proofs.TrainedCnn.d3_ne (k : Fin 8) :

dense W3 b3 p2f k ≠ 0

noncomputable def Proofs.TrainedCnn.r3V :

relu(dense3) at the witness, exact.

Equations

Proofs.TrainedCnn.r3V = ![0, 3315505013 / 570425344, 663167541 / 570425344, 86836255423 / 8556380160, 0, 12288523033 / 4278190080, 4316132003 / 1069547520, 0]

Instances For

theorem Proofs.TrainedCnn.r3_eq :

relu 8 (dense W3 b3 p2f) = r3V

noncomputable def Proofs.TrainedCnn.d4V :

Fin 8 → ℝ

dense4 pre-activations at the witness, exact.

Equations

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

Instances For

theorem Proofs.TrainedCnn.d4_eq (k : Fin 8) :

dense W4 b4 r3V k = d4V k

theorem Proofs.TrainedCnn.d4_ne (k : Fin 8) :

dense W4 b4 r3V k ≠ 0

noncomputable def Proofs.TrainedCnn.trainedCnn_has_vjp_at :

HasVJPAt (mnistCnnNoBnForward W1 b1 W2 b2 W3 b3 W4 b4 W5 b5) X

Level 1: the trained-weight whole-net CNN VJP witness — HasVJPAt (mnistCnnNoBnForward …) X with every one of the five smoothness hypotheses discharged at the trained weights and the real test input. The convolutional sibling of trainedMlp_has_vjp_at.

Equations

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

Instances For

theorem Proofs.TrainedCnn.trainedCnn_has_vjp_correct (dy : Vec 10) (i : Fin (1 * (2 * 3) * (2 * 3))) :

trainedCnn_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

The witness's contract, exposed: the whole-net backward equals the pdiv-contracted Jacobian at the trained weights and real input.