Documentation

LeanMlir.Proofs.Training.TrainedCnnSeal

Level-3 seal for the trained-CNN witness #

The MLP rung's pdiv_fwd/trainedMlp_backward_nontrivial program at the CONVOLUTIONAL witness: one whole-net Jacobian entry of the trained CNN, computed in closed form by peeling mnistCnnNoBnForward with pdiv_comp from the output side. Exact backward-cotangent tables (all in-kernel rationals): dense head slices (t4V/t3V), the max-pool argmax routing (t2V, via MaxPool2IsArgmax at each of the 72 positions), the ReLU mask folds (m2V/m1V), and the conv input-VJPs (t1V and the final entry, via conv2d_input_grad_formula through HasVJPAt.correct).

The sealed entry: ∂ logit_7 / ∂ pixel (0,2) at the witness = -326103939411/34359738368 ≈ -9.4909 ≠ 0, hence trainedCnn_backward_nontrivial (the proven backward is not the zero map), trainedCnn_jacobian_nonzero (fderiv ≠ 0), and trainedCnn_not_constant. Generated by scripts/trained_cnn_seal.py; tables are DATA here.

noncomputable def Proofs.TrainedCnn.t4V :

dense-head slice pdiv (dense5 ∘ relu∘dense4) r3V · 7.

Equations

Proofs.TrainedCnn.t4V = ![-6105 / 8192, 4763 / 8192, -16753 / 16384, 3271 / 16384, -2213 / 8192, 3093 / 8192, 16479 / 16384, -6513 / 16384]

Instances For

noncomputable def Proofs.TrainedCnn.t3V :

Vec (2 * 3 * 3)

relu∘dense3: pdiv (head) p2f · 7.

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.t2V :

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

max-pool: argmax routing of t3V (zero off-argmax).

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.M2T :

relu mask₂ ⊙ t2V, tensor form (the conv2 backward cotangent).

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.m2V :

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

Equations

Proofs.TrainedCnn.m2V = Proofs.TrainedCnn.M2T.flatten

Instances For

noncomputable def Proofs.TrainedCnn.t1V :

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

conv2 input-VJP of m2V.

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.M1T :

relu mask₁ ⊙ t1V, tensor form (the conv1 backward cotangent).

Equations

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

Instances For

noncomputable def Proofs.TrainedCnn.m1V :

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

Equations

Proofs.TrainedCnn.m1V = Proofs.TrainedCnn.M1T.flatten

Instances For

theorem Proofs.TrainedCnn.diffL4_r3V :

DifferentiableAt ℝ (relu 8 ∘ dense W4 b4) r3V

theorem Proofs.TrainedCnn.diffG4_r3V :

DifferentiableAt ℝ (dense W5 b5 ∘ relu 8 ∘ dense W4 b4) r3V

theorem Proofs.TrainedCnn.diffL3_p2f :

DifferentiableAt ℝ (relu 8 ∘ dense W3 b3) p2f

theorem Proofs.TrainedCnn.r3_pt :

(relu 8 ∘ dense W3 b3) p2f = r3V

theorem Proofs.TrainedCnn.diffG3_p2f :

DifferentiableAt ℝ ((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) p2f

theorem Proofs.TrainedCnn.r2flat_eq :

relu (2 * (2 * 3) * (2 * 3)) (Tensor3.flatten c2V) = r2V.flatten

relu(conv2 table) = the max-pool input table, pointwise fold.

theorem Proofs.TrainedCnn.diffP_r2 :

DifferentiableAt ℝ (maxPoolFlat 2 3 3) r2V.flatten

theorem Proofs.TrainedCnn.diffG2_r2 :

DifferentiableAt ℝ (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten

theorem Proofs.TrainedCnn.diffG2r_c2 :

DifferentiableAt ℝ ((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) (Tensor3.flatten c2V)

theorem Proofs.TrainedCnn.c2flat_eq :

flatConv W2 b2 z1V.flatten = Tensor3.flatten c2V

conv2 at the relu(conv1) table = the conv2 table, flat form.

theorem Proofs.TrainedCnn.diffG1_z1 :

DifferentiableAt ℝ (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten

theorem Proofs.TrainedCnn.z1flat_eq :

relu (2 * (2 * 3) * (2 * 3)) (Tensor3.flatten c1V) = z1V.flatten

relu(conv1 table) = the conv2-input table, pointwise fold.

theorem Proofs.TrainedCnn.diffG1r_c1 :

DifferentiableAt ℝ ((((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) ∘ relu (2 * (2 * 3) * (2 * 3))) (Tensor3.flatten c1V)

theorem Proofs.TrainedCnn.c1flat_eq :

flatConv W1 b1 X = Tensor3.flatten c1V

conv1 at the witness input = the conv1 table, flat form.

noncomputable def Proofs.TrainedCnn.conv2wit :

HasVJPAt (flatConv W2 b2) z1V.flatten

The conv2 layer witness, type-ascribed at flatConv (defeq).

Equations

Proofs.TrainedCnn.conv2wit = (Proofs.hasVJP3_to_hasVJP (Proofs.conv2d_has_vjp3 Proofs.TrainedCnn.W2 Proofs.TrainedCnn.b2)).toHasVJPAt Proofs.TrainedCnn.z1V.flatten

Instances For

noncomputable def Proofs.TrainedCnn.conv1wit :

HasVJPAt (flatConv W1 b1) X

The conv1 layer witness, type-ascribed at flatConv (defeq).

Equations

Proofs.TrainedCnn.conv1wit = (Proofs.hasVJP3_to_hasVJP (Proofs.conv2d_has_vjp3 Proofs.TrainedCnn.W1 Proofs.TrainedCnn.b1)).toHasVJPAt Proofs.TrainedCnn.X

Instances For

theorem Proofs.TrainedCnn.d4inner (k m : Fin 8) :

pdiv (relu 8 ∘ dense W4 b4) r3V k m = W4 k m * if d4V m > 0 then 1 else 0

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

pdiv (dense W5 b5 ∘ relu 8 ∘ dense W4 b4) r3V k ⟨7, ⋯⟩ = t4V k

theorem Proofs.TrainedCnn.d3inner (k : Fin (2 * 3 * 3)) (m : Fin 8) :

pdiv (relu 8 ∘ dense W3 b3) p2f k m = W3 k m * if d3V m > 0 then 1 else 0

theorem Proofs.TrainedCnn.S3 (k : Fin (2 * 3 * 3)) :

pdiv ((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) p2f k ⟨7, ⋯⟩ = t3V k

theorem Proofs.TrainedCnn.S2_c0 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨0, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨0, ⋯⟩

theorem Proofs.TrainedCnn.S2_c1 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨1, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨1, ⋯⟩

theorem Proofs.TrainedCnn.S2_c2 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨2, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨2, ⋯⟩

theorem Proofs.TrainedCnn.S2_c3 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨3, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨3, ⋯⟩

theorem Proofs.TrainedCnn.S2_c4 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨4, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨4, ⋯⟩

theorem Proofs.TrainedCnn.S2_c5 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨5, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨5, ⋯⟩

theorem Proofs.TrainedCnn.S2_c6 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨6, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨6, ⋯⟩

theorem Proofs.TrainedCnn.S2_c7 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨7, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨7, ⋯⟩

theorem Proofs.TrainedCnn.S2_c8 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨8, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨8, ⋯⟩

theorem Proofs.TrainedCnn.S2_c9 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨9, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨9, ⋯⟩

theorem Proofs.TrainedCnn.S2_c10 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨10, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨10, ⋯⟩

theorem Proofs.TrainedCnn.S2_c11 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨11, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨11, ⋯⟩

theorem Proofs.TrainedCnn.S2_c12 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨12, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨12, ⋯⟩

theorem Proofs.TrainedCnn.S2_c13 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨13, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨13, ⋯⟩

theorem Proofs.TrainedCnn.S2_c14 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨14, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨14, ⋯⟩

theorem Proofs.TrainedCnn.S2_c15 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨15, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨15, ⋯⟩

theorem Proofs.TrainedCnn.S2_c16 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨16, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨16, ⋯⟩

theorem Proofs.TrainedCnn.S2_c17 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨17, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨17, ⋯⟩

theorem Proofs.TrainedCnn.S2_c18 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨18, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨18, ⋯⟩

theorem Proofs.TrainedCnn.S2_c19 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨19, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨19, ⋯⟩

theorem Proofs.TrainedCnn.S2_c20 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨20, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨20, ⋯⟩

theorem Proofs.TrainedCnn.S2_c21 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨21, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨21, ⋯⟩

theorem Proofs.TrainedCnn.S2_c22 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨22, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨22, ⋯⟩

theorem Proofs.TrainedCnn.S2_c23 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨23, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨23, ⋯⟩

theorem Proofs.TrainedCnn.S2_c24 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨24, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨24, ⋯⟩

theorem Proofs.TrainedCnn.S2_c25 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨25, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨25, ⋯⟩

theorem Proofs.TrainedCnn.S2_c26 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨26, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨26, ⋯⟩

theorem Proofs.TrainedCnn.S2_c27 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨27, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨27, ⋯⟩

theorem Proofs.TrainedCnn.S2_c28 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨28, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨28, ⋯⟩

theorem Proofs.TrainedCnn.S2_c29 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨29, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨29, ⋯⟩

theorem Proofs.TrainedCnn.S2_c30 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨30, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨30, ⋯⟩

theorem Proofs.TrainedCnn.S2_c31 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨31, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨31, ⋯⟩

theorem Proofs.TrainedCnn.S2_c32 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨32, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨32, ⋯⟩

theorem Proofs.TrainedCnn.S2_c33 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨33, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨33, ⋯⟩

theorem Proofs.TrainedCnn.S2_c34 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨34, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨34, ⋯⟩

theorem Proofs.TrainedCnn.S2_c35 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨35, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨35, ⋯⟩

theorem Proofs.TrainedCnn.S2_c36 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨36, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨36, ⋯⟩

theorem Proofs.TrainedCnn.S2_c37 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨37, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨37, ⋯⟩

theorem Proofs.TrainedCnn.S2_c38 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨38, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨38, ⋯⟩

theorem Proofs.TrainedCnn.S2_c39 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨39, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨39, ⋯⟩

theorem Proofs.TrainedCnn.S2_c40 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨40, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨40, ⋯⟩

theorem Proofs.TrainedCnn.S2_c41 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨41, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨41, ⋯⟩

theorem Proofs.TrainedCnn.S2_c42 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨42, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨42, ⋯⟩

theorem Proofs.TrainedCnn.S2_c43 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨43, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨43, ⋯⟩

theorem Proofs.TrainedCnn.S2_c44 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨44, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨44, ⋯⟩

theorem Proofs.TrainedCnn.S2_c45 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨45, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨45, ⋯⟩

theorem Proofs.TrainedCnn.S2_c46 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨46, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨46, ⋯⟩

theorem Proofs.TrainedCnn.S2_c47 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨47, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨47, ⋯⟩

theorem Proofs.TrainedCnn.S2_c48 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨48, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨48, ⋯⟩

theorem Proofs.TrainedCnn.S2_c49 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨49, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨49, ⋯⟩

theorem Proofs.TrainedCnn.S2_c50 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨50, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨50, ⋯⟩

theorem Proofs.TrainedCnn.S2_c51 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨51, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨51, ⋯⟩

theorem Proofs.TrainedCnn.S2_c52 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨52, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨52, ⋯⟩

theorem Proofs.TrainedCnn.S2_c53 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨53, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨53, ⋯⟩

theorem Proofs.TrainedCnn.S2_c54 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨54, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨54, ⋯⟩

theorem Proofs.TrainedCnn.S2_c55 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨55, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨55, ⋯⟩

theorem Proofs.TrainedCnn.S2_c56 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨56, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨56, ⋯⟩

theorem Proofs.TrainedCnn.S2_c57 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨57, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨57, ⋯⟩

theorem Proofs.TrainedCnn.S2_c58 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨58, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨58, ⋯⟩

theorem Proofs.TrainedCnn.S2_c59 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨59, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨59, ⋯⟩

theorem Proofs.TrainedCnn.S2_c60 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨60, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨60, ⋯⟩

theorem Proofs.TrainedCnn.S2_c61 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨61, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨61, ⋯⟩

theorem Proofs.TrainedCnn.S2_c62 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨62, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨62, ⋯⟩

theorem Proofs.TrainedCnn.S2_c63 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨63, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨63, ⋯⟩

theorem Proofs.TrainedCnn.S2_c64 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨64, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨64, ⋯⟩

theorem Proofs.TrainedCnn.S2_c65 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨65, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨65, ⋯⟩

theorem Proofs.TrainedCnn.S2_c66 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨66, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨66, ⋯⟩

theorem Proofs.TrainedCnn.S2_c67 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨67, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨67, ⋯⟩

theorem Proofs.TrainedCnn.S2_c68 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨68, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨68, ⋯⟩

theorem Proofs.TrainedCnn.S2_c69 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨69, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨69, ⋯⟩

theorem Proofs.TrainedCnn.S2_c70 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨70, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨70, ⋯⟩

theorem Proofs.TrainedCnn.S2_c71 :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten ⟨71, ⋯⟩ ⟨7, ⋯⟩ = t2V ⟨71, ⋯⟩

theorem Proofs.TrainedCnn.S2 (k : Fin (2 * (2 * 3) * (2 * 3))) :

pdiv (((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) r2V.flatten k ⟨7, ⋯⟩ = t2V k

theorem Proofs.TrainedCnn.S2r (m : Fin (2 * (2 * 3) * (2 * 3))) :

pdiv ((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) (Tensor3.flatten c2V) m ⟨7, ⋯⟩ = m2V m

theorem Proofs.TrainedCnn.S1_c0 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨0, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨0, ⋯⟩

theorem Proofs.TrainedCnn.S1_c1 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨1, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨1, ⋯⟩

theorem Proofs.TrainedCnn.S1_c2 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨2, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨2, ⋯⟩

theorem Proofs.TrainedCnn.S1_c3 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨3, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨3, ⋯⟩

theorem Proofs.TrainedCnn.S1_c4 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨4, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨4, ⋯⟩

theorem Proofs.TrainedCnn.S1_c5 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨5, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨5, ⋯⟩

theorem Proofs.TrainedCnn.S1_c6 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨6, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨6, ⋯⟩

theorem Proofs.TrainedCnn.S1_c7 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨7, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨7, ⋯⟩

theorem Proofs.TrainedCnn.S1_c8 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨8, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨8, ⋯⟩

theorem Proofs.TrainedCnn.S1_c9 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨9, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨9, ⋯⟩

theorem Proofs.TrainedCnn.S1_c10 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨10, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨10, ⋯⟩

theorem Proofs.TrainedCnn.S1_c11 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨11, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨11, ⋯⟩

theorem Proofs.TrainedCnn.S1_c12 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨12, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨12, ⋯⟩

theorem Proofs.TrainedCnn.S1_c13 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨13, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨13, ⋯⟩

theorem Proofs.TrainedCnn.S1_c14 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨14, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨14, ⋯⟩

theorem Proofs.TrainedCnn.S1_c15 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨15, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨15, ⋯⟩

theorem Proofs.TrainedCnn.S1_c16 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨16, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨16, ⋯⟩

theorem Proofs.TrainedCnn.S1_c17 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨17, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨17, ⋯⟩

theorem Proofs.TrainedCnn.S1_c18 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨18, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨18, ⋯⟩

theorem Proofs.TrainedCnn.S1_c19 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨19, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨19, ⋯⟩

theorem Proofs.TrainedCnn.S1_c20 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨20, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨20, ⋯⟩

theorem Proofs.TrainedCnn.S1_c21 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨21, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨21, ⋯⟩

theorem Proofs.TrainedCnn.S1_c22 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨22, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨22, ⋯⟩

theorem Proofs.TrainedCnn.S1_c23 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨23, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨23, ⋯⟩

theorem Proofs.TrainedCnn.S1_c24 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨24, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨24, ⋯⟩

theorem Proofs.TrainedCnn.S1_c25 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨25, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨25, ⋯⟩

theorem Proofs.TrainedCnn.S1_c26 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨26, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨26, ⋯⟩

theorem Proofs.TrainedCnn.S1_c27 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨27, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨27, ⋯⟩

theorem Proofs.TrainedCnn.S1_c28 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨28, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨28, ⋯⟩

theorem Proofs.TrainedCnn.S1_c29 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨29, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨29, ⋯⟩

theorem Proofs.TrainedCnn.S1_c30 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨30, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨30, ⋯⟩

theorem Proofs.TrainedCnn.S1_c31 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨31, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨31, ⋯⟩

theorem Proofs.TrainedCnn.S1_c32 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨32, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨32, ⋯⟩

theorem Proofs.TrainedCnn.S1_c33 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨33, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨33, ⋯⟩

theorem Proofs.TrainedCnn.S1_c34 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨34, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨34, ⋯⟩

theorem Proofs.TrainedCnn.S1_c35 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨35, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨35, ⋯⟩

theorem Proofs.TrainedCnn.S1_c36 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨36, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨36, ⋯⟩

theorem Proofs.TrainedCnn.S1_c37 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨37, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨37, ⋯⟩

theorem Proofs.TrainedCnn.S1_c38 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨38, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨38, ⋯⟩

theorem Proofs.TrainedCnn.S1_c39 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨39, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨39, ⋯⟩

theorem Proofs.TrainedCnn.S1_c40 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨40, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨40, ⋯⟩

theorem Proofs.TrainedCnn.S1_c41 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨41, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨41, ⋯⟩

theorem Proofs.TrainedCnn.S1_c42 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨42, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨42, ⋯⟩

theorem Proofs.TrainedCnn.S1_c43 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨43, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨43, ⋯⟩

theorem Proofs.TrainedCnn.S1_c44 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨44, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨44, ⋯⟩

theorem Proofs.TrainedCnn.S1_c45 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨45, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨45, ⋯⟩

theorem Proofs.TrainedCnn.S1_c46 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨46, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨46, ⋯⟩

theorem Proofs.TrainedCnn.S1_c47 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨47, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨47, ⋯⟩

theorem Proofs.TrainedCnn.S1_c48 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨48, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨48, ⋯⟩

theorem Proofs.TrainedCnn.S1_c49 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨49, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨49, ⋯⟩

theorem Proofs.TrainedCnn.S1_c50 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨50, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨50, ⋯⟩

theorem Proofs.TrainedCnn.S1_c51 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨51, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨51, ⋯⟩

theorem Proofs.TrainedCnn.S1_c52 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨52, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨52, ⋯⟩

theorem Proofs.TrainedCnn.S1_c53 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨53, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨53, ⋯⟩

theorem Proofs.TrainedCnn.S1_c54 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨54, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨54, ⋯⟩

theorem Proofs.TrainedCnn.S1_c55 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨55, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨55, ⋯⟩

theorem Proofs.TrainedCnn.S1_c56 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨56, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨56, ⋯⟩

theorem Proofs.TrainedCnn.S1_c57 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨57, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨57, ⋯⟩

theorem Proofs.TrainedCnn.S1_c58 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨58, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨58, ⋯⟩

theorem Proofs.TrainedCnn.S1_c59 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨59, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨59, ⋯⟩

theorem Proofs.TrainedCnn.S1_c60 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨60, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨60, ⋯⟩

theorem Proofs.TrainedCnn.S1_c61 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨61, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨61, ⋯⟩

theorem Proofs.TrainedCnn.S1_c62 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨62, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨62, ⋯⟩

theorem Proofs.TrainedCnn.S1_c63 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨63, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨63, ⋯⟩

theorem Proofs.TrainedCnn.S1_c64 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨64, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨64, ⋯⟩

theorem Proofs.TrainedCnn.S1_c65 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨65, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨65, ⋯⟩

theorem Proofs.TrainedCnn.S1_c66 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨66, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨66, ⋯⟩

theorem Proofs.TrainedCnn.S1_c67 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨67, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨67, ⋯⟩

theorem Proofs.TrainedCnn.S1_c68 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨68, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨68, ⋯⟩

theorem Proofs.TrainedCnn.S1_c69 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨69, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨69, ⋯⟩

theorem Proofs.TrainedCnn.S1_c70 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨70, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨70, ⋯⟩

theorem Proofs.TrainedCnn.S1_c71 :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten ⟨71, ⋯⟩ ⟨7, ⋯⟩ = t1V ⟨71, ⋯⟩

theorem Proofs.TrainedCnn.S1 (k : Fin (2 * (2 * 3) * (2 * 3))) :

pdiv (((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) z1V.flatten k ⟨7, ⋯⟩ = t1V k

theorem Proofs.TrainedCnn.S0r (m : Fin (2 * (2 * 3) * (2 * 3))) :

pdiv ((((((dense W5 b5 ∘ relu 8 ∘ dense W4 b4) ∘ relu 8 ∘ dense W3 b3) ∘ maxPoolFlat 2 3 3) ∘ relu (2 * (2 * 3) * (2 * 3))) ∘ flatConv W2 b2) ∘ relu (2 * (2 * 3) * (2 * 3))) (Tensor3.flatten c1V) m ⟨7, ⋯⟩ = m1V m

theorem Proofs.TrainedCnn.pdiv_fwd_entry :

pdiv (mnistCnnNoBnForward W1 b1 W2 b2 W3 b3 W4 b4 W5 b5) X ⟨2, ⋯⟩ ⟨7, ⋯⟩ = -326103939411 / 34359738368

The whole-net Jacobian entry, exactly: ∂ logit_7 / ∂ pixel (0,2) at the trained weights and the real witness input.

theorem Proofs.TrainedCnn.pdiv_fwd_entry_ne :

pdiv (mnistCnnNoBnForward W1 b1 W2 b2 W3 b3 W4 b4 W5 b5) X ⟨2, ⋯⟩ ⟨7, ⋯⟩ ≠ 0

theorem Proofs.TrainedCnn.trainedCnn_backward_nontrivial :

trainedCnn_has_vjp_at.backward (basisVec ⟨7, ⋯⟩) ⟨2, ⋯⟩ ≠ 0

Level 3: the trained-weight CNN backward is not the zero map — the seal the MLP rung carries, now at the convolutional witness.

theorem Proofs.TrainedCnn.trainedCnn_jacobian_nonzero :

fderiv ℝ (mnistCnnNoBnForward W1 b1 W2 b2 W3 b3 W4 b4 W5 b5) X ≠ 0

The fderiv form: the whole-net Jacobian at the trained CNN witness is nonzero.

theorem Proofs.TrainedCnn.trainedCnn_not_constant :

¬∀ (u v : Vec (1 * (2 * 3) * (2 * 3))), mnistCnnNoBnForward W1 b1 W2 b2 W3 b3 W4 b4 W5 b5 u = mnistCnnNoBnForward W1 b1 W2 b2 W3 b3 W4 b4 W5 b5 v

The trained CNN is not a constant function.