Lipschitz constants for the CNN softmax-CE loss — descent through the pool #
SgdDescent.Mlp discharged sgd_descends' smoothness hypothesis for every
MLP weight layer; this file extends the program to the Chapter-3 MNIST CNN
(conv → relu → conv → relu → maxpool → dense → relu → dense → relu → dense). What's genuinely new versus the MLP:
The dense head is free. Below the pool the CNN is an MLP at the pooled activation: the loss-of-
W₅/W₄/W₃maps are literal instances oflinear_sgd_descends/mlp_hidden_sgd_descends/mlp_input_sgd_descendsatx := maxPoolFlat (…), and the loss-of-b₅/b₄/b₃maps oflinear_bias_sgd_descends/mlp_hidden_bias_sgd_descends/mlp_input_bias_sgd_descends(SgdDescent.MlpBias). No new theorems are needed (the MLP statements are generic in the fixed activation vector).The max-pool needs a selection margin, up to twins. At a tied window the pool has no derivative, and real MNIST ties windows in nearly every image: a constant background patch makes a window's conv outputs equal for EVERY kernel. Those cells are twins: they read identical zero-padded input patches (
ConvPatchEq, andConvPatchEq2two convs deep), so they stay equal along any step. The rungs takeMaxPool2MarginQUpTo δ Ton the conv2 pre-activation: each window is dead (all cells≤ 0, kept dead by the relu₂ margin), or the cell dominating it is more than2δabove every cell that is not its twin. Then near every point of the step segment the relu'd pool IS the gather at the base point's argmax (Conv2Slot.maxPool_relu_eventuallyEq_gather), and the gather is linear andℓ1-contractive (poolGatherFlat_l1_contract: the 2×2 stride-2 windows partition the input), so the descent argument runs on it (Conv2Slot.gather_grad_lipschitz) and transfers back (Conv2Slot.sgd_descends). The probe scripts/probes/mnist_pool_twin_probe.py evaluates the condition on the MNIST test set at the trained Chapter-3 weights.Conv layers are dense layers with weight sharing. The conv output is affine in the kernel; each output entry reads one kernel slab against bounded input values (
conv2d_flat_kernel_drift_total), and theℓ1drift picks up the spatial multiplicityh·w— each kernel entry touches every spatial position (conv2d_flat_kernel_drift_sum).
The capstone cnn_conv2_sgd_descends mirrors mlp_input_sgd_descends:
under the four margins (relu₂, pool selection up to twins, relu₃, relu₄) at the step
radius and the small-step condition, one inexact SGD step on the second
conv kernel (one example, every other parameter fixed) decreases that example's
cross-entropy loss by ≥ lr·‖∇L‖₂²/2, with the segment-Lipschitz constant
explicit.
cnn_conv1_sgd_descends extends the program one layer deeper: the step
now crosses conv2 AS A FUNCTION OF ITS INPUT. Conv is linear there, its
Jacobian entry a single kernel tap (convTap, extracted point-free from
the certified input-VJP), and its ℓ1 operator factor is LOCALITY —
(channels)·kH·kW·w₂, not a spatial count. Under FIVE margins (relu₁ +
the conv2 four, at conv1 radii) every routing decision freezes and the
loss provably drops.
cnn_conv2_bias_sgd_descends / cnn_conv1_bias_sgd_descends close the
biases: the bias-map Jacobian is a Kronecker channel indicator
(conv2d_bias_pdiv, extracted from the certified bias VJP), the
per-entry drift is exactly |e o| (no input bound a). Each conv layer's
drift chain, margins, segment-Lipschitz gradient and descent step are stated once, for any
parameter map with per-entry drift ρ·‖e‖₁ (Conv2Slot, Conv1Slot): the
kernel rungs are ρ = a, the bias rungs ρ = 1 — the bare D radii and
a² ↦ 1 in the constants. Both conv kernels, both conv biases and the
dense-head weights and biases of the Chapter-3 CNN (the latter via the MLP
rungs, SgdDescent.Mlp and SgdDescent.MlpBias) each have a single-layer, single-example descent
statement, conditional on the margins above and the oracle-accuracy,
small-step and dominance hypotheses. The rungs that replace the oracle accuracy by
the proven accuracy of the FloatModel binary32 gradient are in SgdDescent.CnnFloat.
The index plumbing, the 2×2 max-pool window facts and the twin relations (ConvPatchEq,
ConvPatchEq2) it reads tensors through are in ConvIndex; the conv's kernel, input and bias
Jacobians and drifts (conv2d_weight_pdiv, convTap, conv2d_input_l1_drift,
conv2d_bias_pdiv) in ConvGrad.
Loss input-gradient of the 3-dense head CE∘d₅∘relu∘d₄∘relu∘d₃
at the pooled vector — one pdiv_comp hop (peel dense W₃) on top of
ce_head2_input_grad, exactly as ce_head2 was one hop on
ce_head_relu. Note there is NO leading mask: the pool output feeds
dense W₃ directly.
Loss input-gradient at the conv output — the key glue of the conv
rung. The chain pdivs through the relu (mask) and the pool (frozen
selector): at a smooth point the sum over pooled coordinates collapses
to the single argmax term, so
∂(CE∘head3∘pool∘relu)/∂z₂[ci,hi,wi] = relu'(z₂[ci,hi,wi]) · 𝟙[(ci,hi,wi) is its window's argmax] · head3grad(window(ci,hi,wi)).
NB the pool acts on the POST-relu activation, so the smoothness and
argmax conditions are stated on relu z₂, not z₂.
Loss input-gradient at the conv output, through a fixed gather — the gather peer of
pool_relu_input_grad. With the pool replaced by poolGatherFlat σ, the route is σ's
selection rather than an argmax, so no pool hypothesis is needed:
∂(CE∘head3∘gather∘relu)/∂z₂[ci,hi,wi] = relu'(z₂[ci,hi,wi]) · 𝟙[(hi,wi) is σ's cell of its window] · head3grad(window(ci,hi,wi)).
Closed form of the conv2 loss gradient at any four-margin point —
the chain rule through the conv weight map (gradAt_comp_t3)
with the pool-collapsed head gradient
(pool_relu_input_grad) and the point-free conv weight Jacobian
(conv2d_weight_pdiv). The conv-layer peer of
mlp_input_loss_gradAt; the spatial triple sum (vs the MLP's
Kronecker collapse) is weight sharing.
The unmasked peer of reluMask_dense_transpose_eq: a bare Wᵀ
contraction ∑ₖ Wₗₖ·cₖ = dense (transpose W) 0 c l. The pool feeds
dense W₃ with no leading ReLU mask, so the W₃ contraction in the
certified conv-2 gradient collapses through this, where the masked W₄/W₅
contractions collapse through reluMask_dense_transpose_eq. NB this is
generic in (W, c), so fire it only where the goal has no other matrix
contraction (e.g. the spatial ∑ convPad·cot) — see head3_cot_reluMask.
The 3-dense head cotangent in dense/reluMask form. The raw nested
∑ₗ W₃·(𝟙[z₃]·∑_q W₄·(𝟙[z₄]·∑_k W₅·(softmax−onehot))) that
pool_relu_input_grad / cnn_conv2_loss_gradAt leave at the pooled vector
u equals dense W₃ᵀ 0 (mask z₃ (dense W₄ᵀ 0 (mask z₄ (dense W₅ᵀ 0 (softmax−onehot))))) — the two masked contractions via
reluMask_dense_transpose_eq, the unmasked W₃ via dense_transpose_eq.
Stated head-locally (no spatial sum) so the generic dense_transpose_eq
fires only on the W₃ row. The head peer the conv grad-close bounds against
via dense_close (W₃) and cot_step_close (W₄/W₅).
The certified conv-2 loss gradient, head restated in dense/reluMask
form — the conv peer of mlp_input_loss_gradAt_reluMask. The two head Wᵀ contractions (under the d₄/d₃ ReLU masks)
collapse via reluMask_dense_transpose_eq, the unmasked W₃ contraction via
dense_transpose_eq; the conv-output ReLU mask 𝟙[z₂>0] and the pool
argmax selector are kept explicit (their float closeness is handled by
reluMask_close and MaxPool2MarginQ.poolBack_close). The whole conv
gradient is then packaged as the spatial dot ∑ₛ convPadWin·cotWin
(convWeightGrad_eq_dot) — the exact quantity the FloatModel gradient's
conv-weight dot rounds, so the conv grad-close bounds against this.
Frozen-mask head-gradient drift: with the two head masks frozen
(0/1-valued, shared between the two points) and the softmax drifting
by at most Δ, the head3 gradient closed form drifts by at most
d₃·w₃·d₄·w₄·nC·w₅·Δ — the oneHot cancels in the difference.
The loss of a conv2-slot parameter map: a parameter map Z into conv2's pre-activation,
then relu, the 2×2 max-pool and the 3-dense head. Every CNN descent rung's loss has this
shape: the conv2 kernel and bias (Z affine in the parameter), and through Conv1Slot the
conv1 kernel and bias.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Near a point, the pooled loss is the gather loss. If at p every window of Z p is
strictly negative, or has the cell σ selects strictly above every other cell except its
T-twins (cells equal at every parameter value, hT), the strict inequalities persist on a
neighbourhood and the twins stay equal, so the relu'd pool and the relu'd gather agree near
p. This is where a tied window stops mattering: the pool has no derivative at a tie, but
a tie between twins is a tie along every parameter direction, and the gather is linear.
The margin up to twins holds along the whole step segment, in strict form, at the
selection σ = the base point's window argmax: a dead window stays strictly negative (the
relu₂ margin), and a non-twin cell stays strictly below the selected one (the 2ρD gap
against a per-entry drift of at most ρD).
Segment-Lipschitz gradient for a conv2-slot loss through a fixed gather, explicit
constant. For a parameter map Z into conv2's pre-activation with per-entry drift
ρ·‖e‖₁ (hZ) and ℓ1 drift (2h)·(2w)·ρ·‖e‖₁ (hZ1), differentiable with Jacobian
row J (row mass ≤ (2h)·(2w)·ρ, hJ) wherever Q holds (hpd): with the pool replaced by
the gather σ, under the relu₂, relu₃ and relu₄ margins at radius ρ·D every mask freezes
along [v, v+d], the route is fixed by construction, the Jacobian factors out, and the
difference collapses to the softmax drift. Q is needed only at the two ends of the
segment (hQv, hQt): the conv2 rungs take Q := True, the conv1 slot Q = relu₁'s
signs frozen. sgd_descends moves this onto the pooled loss.
One inexact SGD step through a conv2 slot decreases the loss — margin up to twins.
For a parameter map Z into conv2's pre-activation with per-entry drift ρ·‖e‖₁ and ℓ1
drift (2h)·(2w)·ρ·‖e‖₁, differentiable with Jacobian rows J (row mass ≤ (2h)·(2w)·ρ)
wherever Q holds along the step, and twins T (cells equal at every parameter value,
hT): under the relu₂ margin, the pool margin up to twins MaxPool2MarginQUpTo, the relu₃
and relu₄ margins (all at radius ρ·D, D the step radius), the small-step condition and
the two dominance conditions, one step with an η-accurate gradient oracle decreases loss
by ≥ lr·‖∇loss‖₂²/2.
The pool needs no derivative of its own. Fix σ = the base point's window argmax. Along
the segment every window is dead or has σ's cell strictly above its non-twins
(marginUpTo_seg), so near every segment point the loss IS the gather loss
(maxPool_relu_eventuallyEq_gather); the gather loss is differentiable there and its
gradient is segment-Lipschitz (gather_grad_lipschitz), and both facts transfer to loss
through the local equality. Every CNN rung is this lemma at its Z, ρ, J and Q.
The margin up to twins, strict at its own point: with every cell nonzero and δ ≥ 0, a
dead window is strictly negative and every non-twin cell is strictly below the window
argmax. marginUpTo_seg at the base point, without the drift.
The loss gradient is at most the Jacobian row mass times the head's operator norm. At a
point where the pool margin up to twins holds (at any δ ≥ 0) and every ReLU stage is off
its kink, the loss is the gather loss near the point, so its gradient is Z's Jacobian row
contracted with the gather head's gradient (gather_loss_gradAt); |softmax − onehot| ≤ 1
leaves at most d₃·w₃·d₄·w₄·nC·w₅ per cell of the row. The bound a concrete instance uses
for the step radius, which it cannot compute (the softmax is transcendental).
The loss as a function of the flattened second-conv kernel.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One inexact SGD step on the CNN's second conv kernel decreases one
example's cross-entropy loss (example (x₁, label) at the frozen conv-2
input, W₂ moving, every other parameter fixed). Conv2Slot.sgd_descends at the conv2
kernel map (ρ = a, the point-free Jacobian conv2d_weight_pdiv). The pool hypothesis is
the margin up to twins MaxPool2MarginQUpTo on the pre-activation conv2d W₂ b₂ x₁, twins
being cells whose zero-padded input patches are identical (hT, ConvPatchEq): those are
equal for every kernel, so a window of them stays tied along the step and costs nothing.
That is the condition real MNIST meets at the trained Chapter-3 weights, where a constant
background patch ties a window's cells (scripts/probes/mnist_pool_twin_probe.py). The
remaining hypotheses: the oracle accuracy η, the relu₂/relu₃/relu₄ margins at the step
radius D = lr·(‖∇L‖₁ + |kernel|·η), the small-step condition and the two dominance
conditions. Conclusion: the loss drops by ≥ lr·‖∇L‖₂²/2. The conv-layer peer of
mlp_input_sgd_descends.
The explicit ℓ1 bound on the conv2-kernel loss gradient, (c·c·kH·kW)·((2h)·(2w)·a)· (d₃·w₃·d₄·w₄·nC·w₅): Conv2Slot.gradAt_abs_le per kernel entry, times the number of
entries. Named so cnn_conv2_exact_sgd_descends can state its radius once.
Equations
Instances For
One exact-gradient SGD step on the conv2 kernel decreases the loss, every hypothesis at an
explicit radius. cnn_conv2_sgd_descends at the exact gradient (η = 0), with the step
radius lr·‖∇L‖₁ replaced by its upper bound lr·cnnConv2GradBound and the second dominance
condition by C·lr·(c·c·kH·kW) ≤ 1/4 (Cauchy–Schwarz, (Σ|g|)² ≤ (c·c·kH·kW)·Σg²). No
hypothesis mentions the gradient: each is a statement about the weights, the input and lr,
which a concrete instance checks by exact arithmetic (Trained.CnnDescent).
One inexact SGD step through a conv1 slot decreases the loss. For a parameter map Z
into conv1's pre-activation with per-entry drift ρ·‖e‖₁ and ℓ1 drift
(2h)·(2w)·ρ·‖e‖₁, differentiable everywhere with a point-free Jacobian J (row mass
≤ (2h)·(2w)·ρ): the relu₁ margin freezes relu₁'s mask along the step, so conv2's
pre-activation conv2 ∘ relu ∘ Z moves by c·kH·kW·w₂·ρ·‖e‖₁ per entry
(z2_entry_drift), and at every point of the step its Jacobian is one fixed row: J, the
base mask and conv2's taps (convTap, locality c·kH·kW·w₂). The rest is
Conv2Slot.sgd_descends at that map, radius c·kH·kW·w₂·ρ, with Q = relu₁'s signs
frozen. The conv1-kernel rung is the instance ρ = a, the conv1-bias rung ρ = 1.
The conv1-slot loss gradient is at most conv2's row mass times the head's operator norm.
Conv2Slot.gradAt_abs_le at the map conv2 ∘ relu ∘ Z: at a point where relu₁ is off its
kink, that map's Jacobian is the fixed row of z2_pdiv, of mass at most
(2h)·(2w)·c·kH·kW·w₂·ρ (z2_row_l1). The bound the conv1 exact-gradient corollaries use
for their step radius.
Loss input-gradient at the conv1 output — the conv1 peer of
pool_relu_input_grad. One more relu mask and one conv-as-input
crossing: the chain picks up relu'(z₁) and contracts the point-free
tap Jacobian of conv2 with the pool-collapsed conv2-rung gradient.
Closed form of the conv1 loss gradient at any five-margin point —
the same chain rule, contracted with the conv1 head gradient
(cnn1_pool_head_input_grad): the conv1 weight Jacobian
(convPad reads of the IMAGE) times relu₁'s mask times the
point-free conv2 tap Jacobian times the pool-collapsed head. Two
spatial triple-sums: weight sharing at conv1, locality at conv2.
The certified conv-1 loss gradient, head restated in dense/reluMask
form — the conv-1 peer of cnn_conv2_loss_gradAt_reluMask. One conv-backward deeper than conv-2: the conv-1-output
cotangent is 𝟙[z₁>0] · ∑_{co,ho,wo} convTap·(conv-2-output cotangent),
with the 3-dense head collapsed by head3_cot_reluMask exactly as in
conv-2. The conv-1 ReLU mask, the conv-2 backward tap (convTap, the
point-free conv-2 input Jacobian), the conv-2 ReLU mask and the pool
selector all stay explicit (their float closeness is mask_scalar_close /
dot_perturbed_close / poolBack_close). Packaged as the spatial dot
∑ₛ convPadWin x₀·cotWin (convWeightGrad_eq_dot) the float conv-1 weight
dot rounds.
Two-layer twins are symmetric.
Two-layer twins are transitive: the middle cell's outer reads are in bounds exactly when the
ends' are. With ConvPatchEq2.symm, the equivalence windowMarginUpTo_of_cert asks of the
twin relation.
The loss as a function of the flattened first-conv kernel.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One inexact SGD step on the CNN's FIRST conv kernel decreases one
example's cross-entropy loss (W₁ moving, every other parameter fixed).
The deepest rung: the step
crosses relu₁, conv2 (as a function of its input — the point-free
tap Jacobian with locality factor c·kH·kW·w₂), relu₂, the pool,
and the 3-dense head. Conv1Slot.sgd_descends at the conv1 kernel map (ρ = a). Under the
FIVE margins at the step radius D = lr·(‖∇L‖₁ + |kernel|·η), the pool's taken up to
two-layer twins (ConvPatchEq2: cells whose two-conv receptive fields in x₀ are
identical, equal for every W₁), every mask freezes along the step, the pool agrees with a
fixed gather near every point of it, and the loss drops by ≥ lr·‖∇L‖₂²/2.
The explicit ℓ1 bound on the conv1-kernel loss gradient, (c·ic·kH·kW)·((2h)·(2w)· (c·kH·kW·w₂·a))·(d₃·w₃·d₄·w₄·nC·w₅): Conv1Slot.gradAt_abs_le at ρ = a per kernel entry,
times the number of entries.
Equations
Instances For
One exact-gradient SGD step on the conv1 kernel decreases the loss, every hypothesis at an
explicit radius. cnn_conv1_sgd_descends at η = 0, the step radius bounded by
lr·cnnConv1GradBound and the second dominance condition by C·lr·(c·ic·kH·kW) ≤ 1/4, as in
cnn_conv2_exact_sgd_descends. The twins are two-layer (ConvPatchEq2).
Closed form of the conv2 bias loss gradient at any four-margin
point — the chain rule through the conv bias map (gradAt_comp_t3)
with the pool-collapsed head gradient (pool_relu_input_grad, reused
verbatim) and the Kronecker bias Jacobian (conv2d_bias_pdiv).
The certified conv-2 BIAS loss gradient, restated as the spatial SUM of
the reluMask-form cotangent — the bias peer of
cnn_conv2_loss_gradAt_reluMask. The 3-dense head collapses via
head3_cot_reluMask; the channel-Kronecker Jacobian if ci = o collapses
the ∑ ci to ci = o (Finset.sum_ite_eq'); the remaining spatial
∑ hi wi is packaged as ∑ s, cotWin c o s (convBiasGrad_eq_sum) — the
quantity the FloatModel gradient's bias SUM rounds.
The loss as a function of the second-conv bias.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One inexact SGD step on the CNN's second conv BIAS decreases one
example's cross-entropy loss (b₂ moving, every other parameter fixed).
Conv2Slot.sgd_descends at the conv2 bias map (ρ = 1): the four margins at the step
radius D = lr·(‖∇L‖₁ + c·η) carry no input bound a (the bias Jacobian is a Kronecker
indicator), the pool's taken up to the same twins as the kernel rung (ConvPatchEq; twin
cells are equal for every bias too), and the parameter needs no flatten/unflatten
plumbing.
The explicit ℓ1 bound on the conv2-bias loss gradient, c·((2h)·(2w)·1)· (d₃·w₃·d₄·w₄·nC·w₅): Conv2Slot.gradAt_abs_le at ρ = 1 per bias entry, times the number of
entries.
Equations
Instances For
One exact-gradient SGD step on the conv2 bias decreases the loss, every hypothesis at an
explicit radius. cnn_conv2_bias_sgd_descends at η = 0, the step radius bounded by
lr·cnnConv2BiasGradBound and the second dominance condition by C·lr·c ≤ 1/4, as in
cnn_conv2_exact_sgd_descends.
Closed form of the conv1 bias loss gradient at any five-margin
point — the chain rule through conv1's bias map, contracted with the conv1 head
gradient (cnn1_pool_head_input_grad, reused verbatim): the
Kronecker bias Jacobian times relu₁'s mask times the point-free
conv2 tap Jacobian times the pool-collapsed head.
The certified conv-1 BIAS loss gradient, restated as the spatial SUM of
the reluMask-form cotangent — the bias peer of
cnn_conv1_loss_gradAt_reluMask, one conv-backward deeper. The head
collapses via head3_cot_reluMask, the conv-2 backward stays the explicit
∑ convTap·c₂, and the channel-Kronecker conv-1 Jacobian collapses the
∑ ci (Finset.sum_ite_eq' + convBiasGrad_eq_sum) to the spatial SUM
the float bias gradient rounds.
The loss as a function of the first-conv bias.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One inexact SGD step on the CNN's FIRST conv BIAS decreases one
example's cross-entropy loss (b₁ moving, every other parameter fixed).
Conv1Slot.sgd_descends at the conv1 bias map (ρ = 1): the FIVE margins at the step
radius D = lr·(‖∇L‖₁ + c·η) carry no input bound a (the bias Jacobian is a Kronecker
indicator), the pool's taken up to two-layer twins (ConvPatchEq2), and the parameter
needs no flatten/unflatten plumbing. With this theorem both conv kernels,
both conv biases and the three dense layers' weights and biases (via the
MLP rungs, SgdDescent.Mlp and SgdDescent.MlpBias) of the Chapter-3 CNN
each have a single-layer, single-example descent statement.
The explicit ℓ1 bound on the conv1-bias loss gradient, c·((2h)·(2w)·(c·kH·kW·w₂·1))· (d₃·w₃·d₄·w₄·nC·w₅): Conv1Slot.gradAt_abs_le at ρ = 1 per bias entry, times the number of
entries.
Equations
Instances For
One exact-gradient SGD step on the conv1 bias decreases the loss, every hypothesis at an
explicit radius. cnn_conv1_bias_sgd_descends at η = 0, the step radius bounded by
lr·cnnConv1BiasGradBound and the second dominance condition by C·lr·c ≤ 1/4, as in
cnn_conv2_exact_sgd_descends.