Lipschitz constants for the CNN softmax-CE loss — descent through the pool #
SgdDescentMlp 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 (…). No new theorems are needed (the MLP statements are generic in the fixed activation vector).The max-pool needs a quantitative SELECTION margin.
MaxPool2Smooth(pairwise-distinct window cells) is the qualitative off-the-kink condition; descent needs its quantitative formMaxPool2MarginQ δ(pairwise window gaps exceed2δ): a perturbation of at mostδper entry then cannot reorder any window, so the argmax — hence the pool's routing pattern — FREEZES along the step segment (MaxPool2MarginQ.isArgmax_iff), exactly as the ReLU margins freeze the masks. The pool is also 1-Lipschitz per entry (maxPoolFlat_entry_lipschitz) andℓ1-contractive across entries (maxPoolFlat_l1_contract— the 2×2 stride-2 windows partition the input), so drift passes through it unamplified.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 (
flatConv_kernel_drift), and theℓ1drift picks up the spatial multiplicityh·w— each kernel entry touches every spatial position (flatConv_kernel_drift_sum).
The capstone cnn_conv2_sgd_descends mirrors mlp_input_sgd_descends:
under the four margins (relu₂, pool selection, relu₃, relu₄) at the step
radius and the small-step condition, one inexact SGD step on the second
conv kernel provably decreases the 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), and the rungs
are the kernel arguments verbatim with the conv stage's a·D radii
replaced by the bare D and a² ↦ 1 in the constants. EVERY parameter
of the Chapter-3 CNN — both conv kernels, both conv biases, and the
dense head — now has a proven descent statement.
Flat index of a Tensor3 coordinate (the suite's row-major layout).
⚠ @[reducible] is load-bearing on Lean ≥ 4.33 (see planning/archive/lean_434_and_cleanup.md):
t3Idx_def folds the raw encoding into the ite CONDITION below, but simp does not rewrite
inside the Decidable INSTANCE argument, so the goal carries a folded condition over an
unfolded instance and every if_pos/if_neg here fails to match. basisVec, which produces
that ite, is @[reducible] for the same reason.
Equations
- Proofs.t3Idx ci hi wi = finProdFinEquiv (finProdFinEquiv (ci, hi), wi)
Instances For
Column version of winRowEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ℓ1 contraction: the pooled drift, summed over all pooled entries, is
at most the input drift summed over all input entries (windows are
disjoint, max is 1-Lipschitz). The pool passes ℓ1 budgets through
unamplified.
Quantitative pool-selection margin: every two cells of every 2×2
window differ by more than 2δ. The quantitative form of
MaxPool2Smooth — a perturbation of at most δ per entry can neither
create a tie nor reorder a window, so the pool's argmax routing
freezes. The pool peer of the ReLU margin a·D < |zⱼ|.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A margined point is itself smooth.
The argmax freezes: within δ of a margined point, every window's
argmax cell is the same as at the margined point.
The padded input read that multiplies kernel entry (·, c, kh, kw) at
output position (hi, wi) — names the dite inside conv2d so the
affine-in-the-kernel structure can be stated. Depends on the input
only, never the kernel.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Flat index of a Kernel4 entry (the suite's row-major layout).
Equations
- Proofs.k4Idx o c kh kw = finProdFinEquiv (finProdFinEquiv (finProdFinEquiv (o, c), kh), kw)
Instances For
Kernel4.flatten reads off at a k4Idx — the forward peer of
unflatten_k4Idx, lifting a per-entry kernel bound to the flattened vector.
Flat index of a conv window slot (c, kh, kw) — k4Idx without the
output channel (row-major, fan-in ic·kH·kW).
Equations
- Proofs.w3Idx c kh kw = finProdFinEquiv (finProdFinEquiv (c, kh), kw)
Instances For
The triple conv-window sum collapses to one flat sum over the fan-in —
the conv analogue of dot being a single-index sum (mirrors sum_abs_k4,
one fewer axis).
The per-output-coordinate conv window as a flat Vec over the fan-in:
the (padded) input reads that the kernel slab dots against.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The kernel as a Mat (ic·kH·kW) oc — column o is the flattened slab.
Equations
- Proofs.convKernelMat W idx o = W o (finProdFinEquiv.symm (finProdFinEquiv.symm idx).1).1 (finProdFinEquiv.symm (finProdFinEquiv.symm idx).1).2 (finProdFinEquiv.symm idx).2
Instances For
conv2d is a dense layer at the conv fan-in — conv = dense-with-sharing
made exact: each output coordinate is Proofs.dense of the kernel slab
against the flattened window. The structural fact that lets the float conv
budget reuse dense_close.
Padded reads of inputs within e stay within e (the read is either a
coordinate, diff ≤ e, or 0, diff 0).
The float conv layer — M.dense of the kernel slab against the
flattened window, per output coordinate. The float peer of conv2d
(every product/accumulate/bias-add rounded), in the dense form.
Equations
- M.convF W b x o hi wi = M.dense (Proofs.convKernelMat W) b (Proofs.convWindow kH kW x hi wi) o
Instances For
Conv forward rounding budget (Item A). The rounded conv at a float input
within e of the real activation is within the conv-fan-in denseErr of the
real conv — dense_close at the flattened window. The compounded Higham
factor rides the fan-in ic·kH·kW (the dense column length here), exactly as
the planning doc calls for.
Conv output magnitude bound = dense_abs_le at the fan-in: conv is a
dense layer, so |conv2dⱼ| ≤ layerAct (ic·kH·kW) w β a.
Vec-space float conv — the float peer of flatConv
(flatten ∘ conv2d ∘ unflatten), with the rounded convF inside.
Equations
- M.flatConvF W b v = (M.convF W b (Proofs.Tensor3.unflatten v)).flatten
Instances For
Vec-space conv forward budget, uniform. The rounded flatConvF at a
float input within e of the real activation is within the conv-fan-in
layerBudget of the real flatConv — every output coordinate, one closed
form. The conv layer threads exactly like a dense layer at fan-in
ic·kH·kW.
Vec-space conv magnitude bound (the activation-norm pass-through).
The float MNIST-CNN (no BN) forward — the float peer of
mnistCnnNoBnForward: rounded conv (flatConvF) and rounded dense
(M.dense); relu and maxPoolFlat appear bare (exact in float).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whole-net MNIST-CNN forward rounding budget (Item A capstone). The
rounded forward is within an explicit closed-form layerBudget of the real
conv→relu→conv→relu→maxpool→dense→relu→dense→relu→dense forward, per
output logit — the binary32 forward-error bound for the Chapter-3 CNN.
Each weight layer threads identically: conv layers as dense at their
fan-in (ic·kH·kW, then c·kH·kW), the dense head at c·h·w / d1; relu
and maxpool pass error through exactly (no rounding, no amplification). The
budget is the mlp_float_close_uniform nest extended to the CNN's six
layers — norm_num-evaluable at a concrete net and magnitude profile.
Per-entry conv drift, slab-refined: a kernel perturbation moves the
output entry (o, hi, wi) by at most a times the ℓ1 mass of the
channel-o slab (each output reads only its own slab).
Per-entry conv drift against the TOTAL ℓ1 mass — the form the relu
margins consume.
ℓ1 conv drift: summed over all output entries, the drift is at
most (h·w)·a·‖e‖₁ — the spatial multiplicity h·w is the price of
weight sharing (each kernel entry touches every spatial position).
The pool's routing pattern is frozen: under the margin, the
pdiv3 Jacobian of the pool is entry-for-entry IDENTICAL at the
margined point and at any δ-close point. This is what lets the pool
behave as a fixed linear selector along the whole step segment.
Float pool-backward closeness (Increment 1 keystone). Under the pool
margin the float post-relu argmax matches the real one
(isArgmax_iff), so the pool's backward selector
𝟙[(ci,hi,wi) is its window's argmax]·(pooled cotangent) differs from the
certified one only through the pooled cotangent value — an indicator
pass-through (indicator ∈ {0,1}), the pool peer of reluMask_close.
The two cotangent values ay (float) / ax (real) enter only via their
closeness |ay − ax| ≤ e.
Folds the raw finProdFinEquiv encoding back into t3Idx.
The 3-dense head CE ∘ d₅ ∘ relu ∘ d₄ ∘ relu ∘ d₃ is differentiable
at any point whose two ReLU pre-activations are off the kinks.
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.
The whole head above the conv output — CE∘head3∘maxPoolFlat∘relu —
is differentiable at any point with the relu₂ pre-activation off the
kinks, no pool ties (POST-relu), and the two head masks off the
kinks.
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₂.
Closed form of the conv weight-map pdiv — extracted from the
certified VJP (conv2d_weight_grad_has_vjp) by contracting its
.correct field against a basis vector. Kernel entry (o,cc,kh,kw)
touches output (co,hi,wi) iff co = o, with coefficient the padded
input read convPad. NB the right-hand side does not mention v:
the weight map is affine, so its Jacobian is point-free — this is
what lets the gradient difference along a step segment collapse to
the head drift alone.
The ℓ1 mass of one Jacobian row of the conv weight map: kernel
entry (o,cc,kh,kw) touches the (h·w) outputs of its slab, each
with a padded read bounded by a — the quantitative form of "weight
sharing costs a spatial multiplicity".
The padded-input window for a fixed kernel slot, flattened over the
(hi, wi) spatial grid — the left operand of the conv weight-grad dot.
Equations
- Proofs.convPadWin kH kW x cc kh kw s = Proofs.convPad kH kW x cc kh kw (finProdFinEquiv.symm s).1 (finProdFinEquiv.symm s).2
Instances For
The cotangent slab for a fixed output channel, flattened over (hi, wi).
Equations
- Proofs.cotWin cot o s = cot o (finProdFinEquiv.symm s).1 (finProdFinEquiv.symm s).2
Instances For
The conv weight gradient is the spatial dot Σ_{hi,wi} convPad · cot
(the contraction conv2d_weight_pdiv certifies as ∂L/∂W_{o,cc,kh,kw}),
re-expressed as a flat Fin (h·w) dot of the padded-input window against
the cotangent slab — the form the float dot rounds.
Rounded conv weight update (Item B). The float update
fl(Wₒ,cc,kh,kw − fl(lr·fl(convPadWin · cotWin))) — the conv weight
gradient is a correlation, a dot over the h·w spatial positions — is
within sgdErr of the real step W − lr·(Σ_{hi,wi} convPad·cot), the
dot's Higham γ (fan-in h·w) as the gradient-error slot. Reuses the
generic dotSgd_step_close; the cotangent is supplied (the loss-head
exp accuracy lives in cotErr).
Rounded conv bias update (Item B) — the bias gradient is the spatial
sum Σ cot, so the rounded update reduces to sumSgd_step_close.
Numeric conv-weight-step capstone at the committed MNIST-CNN dims (Item
C). The Chapter-3 conv2 is 32→32, 3×3, at 28×28 (the conv output
grid, before maxpool), so the weight gradient is a dot over 28·28 = 784
spatial positions. At binary32 (u ≤ 2⁻²⁴), lr = 1/10, kernel |W| ≤ 3/5
(the trained-magnitude bound, matching the MLP capstone), every rounded
conv2 weight SGD entry is within (a·g)/250 + 10⁻⁷ of the certified
real step — where a bounds the conv2-input activation and g the conv2
cotangent magnitude.
Both a and g are a-posteriori / measured quantities (the conv input
and back-propagated cotangent are not intrinsically ≤ 1, unlike the
softmax−onehot loss head), supplied as hypotheses — the same worst-case→
measured hand-off as the forward δ. The decimal rate 1/250 ≈ 0.4% is
dominated by lr·γ₇₈₅ (the gradient's Higham error at learning-rate scale):
the conv weight step is as accurate as the gradient itself, no worse.
Numeric conv-BIAS-step capstone at the committed MNIST-CNN dims — the
bias peer of mnist_cnn_convW_step_float_budget. The conv2 bias gradient is
the spatial SUM ∑ₛ cotWin cot o over the 28·28 = 784 conv-output
positions (no input window, so no a factor — the bias Jacobian is the bare
channel indicator). At binary32 (u ≤ 2⁻²⁴), lr = 1/10, |b| ≤ 3/5, every
rounded conv2 bias SGD entry is within g/250 + 10⁻⁷ of the certified
real step — where g bounds the conv2 cotangent magnitude. The same 1/250
rate as the weight step (it is lr·γ₇₈₅, the gradient's Higham error at
learning-rate scale), with a·g ↦ g — the bias step is as accurate as the
gradient, no worse.
The loss-of-conv2-kernel map is differentiable wherever the relu₂ pre-activation is off the kinks, no pool window ties (POST-relu), and the two head pre-activations are off the kinks.
Closed form of the conv2 loss gradient at any four-margin point —
the EXISTING fold conv_total_loss_grad_fold (generic in the
downstream G) contracted 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 (Increment 1
keystone). 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 rendered trainer's float
conv-weight dot rounds, so the conv grad-close bounds against this.
Scalar ReLU-mask freeze — the (if z>0 then 1 else 0)·x peer of
reluMask_close. Under the sign margin ez < |z| the float and real masks
agree, so the masked value is 1-Lipschitz in x. The conv-output ReLU mask
𝟙[z₂>0] in the conv-2 grad-close sits on a scalar cell (not a Vec), so
it needs this rather than the vector reluMask_close.
Float dot against a perturbed cotangent — the conv-2 grad-close's final
contraction (the conv peer of the MLP's scalar mul_close: a dot, because
of weight sharing). M.dot A B̃ (exact left operand A, float cotangent
B̃) vs the certified ∑ Aᵢ·Bᵢ splits into the Higham dot rounding on A·B̃
(dot_close, fan-in n) plus the per-entry cotangent drift
|B̃ᵢ − Bᵢ| ≤ eB. With |Aᵢ| ≤ a and |B̃ᵢ| ≤ Ct, the bound is closed-form
and norm_num-evaluable.
The binary32 conv-2 weight gradient the rendered trainer computes — the
conv peer of mlpInputFloatGrad. At kernel entry (o,cc,kh,kw) it is the
float dot of the (exact) padded-input window convPadWin against the float
conv-output cotangent slab cotWin c̃Conv o, where the float cotangent
c̃Conv rounds every step of the backward — conv-output ReLU mask 𝟙[z̃₂>0],
pool argmax selector (read on the FLOAT post-relu), and the head
W₃ᵀ·mask(z̃₃)·W₄ᵀ·mask(z̃₄)·W₅ᵀ·(float softmax−onehot) at the float
pre-activations. The M-free reluMask/maxPoolFlat/relu are exact in
float; M.convF/M.dense/M.softmaxCECotF carry the rounding.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conv-2 float-backward grad-close budget — the closed-form η the
rounded W₂ gradient stays within of the certified one. Bottom-up: the
forward rounding nest (Econv → E₃ → E₄ → δlogit, conv at fan-in
c·kH·kW, the dense head at c·h·w / d₃) feeds the head cotErr; the
backward then rides two cot_step layerBudgets (W₅/W₄) and the unmasked
W₃ layerBudget to econv; finally the spatial dot (fan-in (2h)·(2w))
contributes its Higham γ on the float-cotangent magnitude Ctilde plus the
per-entry cotangent drift econv. The conv peer of the MLP's
mulErr/layerBudget/cotErr nest, deeper by the pool + the dot.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The binary32 conv-2 weight gradient is within an explicit budget of the
certified one (Increment 2 capstone) — the conv-layer peer of
mlp_w0_grad_close, the project's deepest float-backward grad-close. With
the conv-2 input x₁ exact, the rendered trainer's W₂ gradient
M.cnnConv2FloatGrad … stays within cnnConv2GradBudget of the certified
gradAt. The chain: float forward (convF_close → dense_close×3, relu
and pool error-transparent) ⟶ head (softmax_ce_cot_close) ⟶ two masked
Wᵀ cot_step_close (W₅ under z̃₄, W₄ under z̃₃) ⟶ unmasked W₃ dense_close
⟶ pool-backward freeze (poolBack_close) ⟶ conv-output ReLU mask freeze
(mask_scalar_close) ⟶ the spatial dot (dot_perturbed_close). Four
quantitative margins are carried (conv-output Econv, pool Econv POST-relu,
z̃₃ E₃, z̃₄ E₄); the bridge cnn_conv2_loss_gradAt_reluMask turns the
gradAt into the dot the float gradient rounds.
Per-entry conv drift, flat-index form of conv2d_kernel_drift_total.
Pooled ℓ1 drift: kernel perturbation → conv (ℓ1, spatial
multiplicity) → relu (contraction) → pool (contraction).
Per-entry POST-relu tensor drift — the form the pool margin
(MaxPool2MarginQ) consumes.
Per-entry drift of the relu₃ pre-activation.
Per-entry drift of the relu₄ pre-activation.
Logit drift through the whole conv2 chain: kernel perturbation →
conv → relu → pool → d₃ → relu → d₄ → relu → d₅. Each dense crossing
contributes its ℓ1→ℓ1 operator factor dᵢ·wᵢ; the conv contributes
the weight-sharing multiplicity (2h)·(2w).
The relu₂ margin keeps the conv pre-activation off the kink, same sign, along the whole step segment.
The POST-relu tensor stays within the pool margin radius a·D along
the whole step segment — what MaxPool2MarginQ.{smooth_of_close, isArgmax_iff, pdiv3_eq} consume.
The relu₃ margin keeps the first head pre-activation off the kink, same sign, along the whole step segment.
The relu₄ margin keeps the second head pre-activation off the kink, same sign, along the whole step segment.
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.
Segment-Lipschitz gradient for the conv2-kernel loss, explicit
constant. Under the four margins at step radius D — relu₂
(a·D), pool selection (MaxPool2MarginQ (a·D) of the POST-relu
tensor), relu₃ (w₃·4hw·a·D), relu₄ (w₄·d₃·w₃·4hw·a·D) — every
routing decision (masks AND pool argmaxes) freezes along [v, v+d],
the point-free conv Jacobian factors out, and the difference
collapses to the softmax drift exactly as in
mlp_input_loss_grad_lipschitz. The conv-layer peer of that
theorem; the constant picks up the weight-sharing multiplicity
((2h)·(2w))².
One inexact SGD step on the CNN's second conv kernel provably
decreases the cross-entropy loss. All of sgd_descends'
hypotheses discharged for the loss-of-conv2-kernel map:
differentiability along the segment and the segment-Lipschitz
constant both come from the FOUR margin hypotheses at the step
radius D = lr·(‖∇L‖₁ + |kernel|·η) — relu₂, the pool-selection
margin (POST-relu), relu₃, relu₄ — which freeze every mask and the
pool's entire routing pattern along the step. Remaining hypotheses
are checkable arithmetic: the oracle accuracy η, the margins, 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 descent program now reaches through
weight sharing and max-pooling.
One binary32 SGD step on the CNN's second conv kernel provably decreases
the cross-entropy loss — with NO abstract gradient-accuracy parameter
(Increment 3, the conv-2 rung capstone). The conv peer of
mlp_input_float_sgd_descends: the gradient is the actual binary32 W₂
gradient M.cnnConv2FloatGrad …, and its accuracy is proven by
cnn_conv2_grad_close (η := cnnConv2GradBudget, discharged per kernel
entry via k4Idx_surj), not assumed. The two rounding-margin families are
carried as hypotheses (the honest first cut): the per-layer ROUND margins
(hmarginConv/Pool/3/4, feeding the grad-close) and the gradient-radius
STEP margins + hsmall/h1/h2 (feeding cnn_conv2_sgd_descends's
drift-freeze and the descent geometry). The conv-2 input x₁ is exact.
The kernel tap that multiplies input entry (ci,hi,wi) in output
entry (co,ho,wo) — the input-side Jacobian entry of conv2d.
Depends on the kernel only, never the input (conv is linear in its
input). Deliberately let-free, like convPad.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A single conv tap is bounded by the kernel magnitude (out-of-pad taps are
zero) — the per-entry bound the conv-2 backward dot_perturbed_close uses.
The tap as a kernel-offset indicator sum: |convTap| is the sum
over kernel offsets (kh,kw) of |W co ci kh kw| pinned to the
unique offset aligning input (hi,wi) with output (ho,wo). The
workhorse for both mass bounds: summing it over OUTPUTS pins
(ho,wo) per offset, summing it over INPUTS pins (hi,wi).
Output-side tap mass: one input entry feeds at most oc·kH·kW
outputs, each through a tap bounded by wK — the ℓ1→ℓ1 operator
factor of a conv crossing as a function of its input.
Input-side tap mass: one output entry reads at most ic·kH·kW
inputs, each through a tap bounded by wK.
Closed form of the conv input-map pdiv3 — extracted from the
certified input-VJP (conv2d_has_vjp3) by contracting its
.correct field against a basis cotangent. Point-free in x:
conv is linear in its input.
Flat-coordinate form of conv2d_input_pdiv3 — the shape the chain
rule through flatConv W₂ b₂ consumes.
Per-entry conv input drift: each output reads ic·kH·kW padded
inputs through taps bounded by wK.
The padded-read drift as a position-pinned indicator sum — the
input-side peer of abs_convTap_expand, for the ℓ1 bound.
ℓ1 conv input drift: each input entry feeds at most oc·kH·kW
outputs, so the total output drift is at most oc·kH·kW·wK times
the total input drift — locality, not a spatial count.
POST-relu₁ tensor drift under a conv1 kernel perturbation.
Per-entry conv2-preactivation drift under a conv1 kernel
perturbation: the perturbation crosses conv2 as a function of its
INPUT, picking up the locality factor c·kH·kW·w₂.
POST-relu₂ tensor drift under a conv1 kernel perturbation — what the pool margin consumes on the conv1 rung.
Pooled ℓ1 drift under a conv1 kernel perturbation: conv1 (ℓ1,
spatial multiplicity) → relu → conv2-as-input (ℓ1, LOCALITY
multiplicity c·kH·kW) → relu → pool.
Per-entry drift of the relu₃ pre-activation, conv1 rung.
Per-entry drift of the relu₄ pre-activation, conv1 rung.
Logit drift through the whole conv1 chain.
The relu₁ margin keeps the conv1 pre-activation off the kink.
The relu₂ margin (at the conv1 radius) keeps the conv2 pre-activation off the kink.
The POST-relu₂ tensor stays within the conv1-rung pool margin radius along the whole step segment.
The relu₃ margin (at the conv1 radius) keeps the first head pre-activation off the kink.
The relu₄ margin (at the conv1 radius) keeps the second head pre-activation off the kink.
The whole head above the conv1 output — CE∘head3∘pool∘relu∘ (flatConv W₂ b₂)∘relu — is differentiable at any five-condition
point.
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.
The loss-of-conv1-kernel map is differentiable at any five-condition point.
Closed form of the conv1 loss gradient at any five-margin point —
the same fold, 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 (Increment 4
keystone). 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.
The binary32 conv-1 weight gradient the rendered trainer computes — the
conv-1 peer of cnnConv2FloatGrad, one conv-backward deeper. At kernel
entry (o,cc,kh,kw) it is the float dot of the (exact) padded-input window
convPadWin x₀ against the float conv-1-output cotangent slab; that
cotangent is the conv-1 ReLU mask 𝟙[z̃₁>0] times the float conv-2 backward
M.dot (convTap W₂ slab) (float conv-2-output cotangent slab), where the
conv-2 cotangent is exactly cnnConv2FloatGrad's, but at the FLOAT conv-2
input relu(z̃₁) (a function of the conv-1 kernel u). All M-ops carry
the rounding; reluMask/maxPoolFlat/relu/convTap are exact.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conv-1 float-backward grad-close budget — the conv-2 budget
(cnnConv2GradBudget-shaped) deepened by one conv layer at the bottom (the
forward nest now starts at conv-1 fan-in ic·kH·kW, the conv-2 input
carries the conv-1 rounding E₁) and one conv-backward at the top: the
conv-2 backward Higham γ over the slab c·(2h)·(2w) against the
float-cotangent magnitude C2t plus the per-entry conv-2-cotangent drift
e₂ gives eback; the conv-1 spatial dot (fan-in (2h)·(2w)) then rides
eback and the float conv-1-cotangent magnitude C1t.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conv-2-output cotangent error budget, as a function of the conv-2
input magnitude aX2 and rounding eX2 — the e₂ of cnnConv2GradBudget
(where aX2 = a, eX2 = 0) and the e₂ inside cnnConv1GradBudget (where
aX2 = A₁, eX2 = E₁). Factored so the conv-1 rung reuses the conv-2
cotangent chain at a FLOAT conv-2 input.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The real conv-2-output cotangent magnitude bound — aX2/eX2-independent
(the head cotangent and the two masked Wᵀ steps are magnitude-frozen).
Equations
- Proofs.FloatModel.cnnConv2CotMag d₃ d₄ nC w₃ w₄ w₅ = Proofs.FloatModel.layerAct d₃ w₃ 0 (Proofs.FloatModel.layerAct d₄ w₄ 0 (Proofs.FloatModel.layerAct nC w₅ 0 1))
Instances For
The conv-2-output cotangent is float-close at a float conv-2 input
(Increment 4 keystone) — Increment 2's conv-2 cotangent chain, factored to
take the conv-2 input (X2, X2F) with |X2F − X2| ≤ eX2, |X2| ≤ aX2. The
conv-1 rung instantiates X2 = relu(z₁), X2F = relu(z̃₁), eX2 = E₁. The
chain: float forward from X2 (convF_close → dense_close×3) → head
(softmax_ce_cot_close) → cot_step_close×2 → unmasked W₃ dense_close →
pool-back (poolBack_close) → conv-2 ReLU mask (mask_scalar_close).
The real conv-2-output cotangent is magnitude-bounded by cnnConv2CotMag
— the aX2/eX2-independent ℓ∞ bound (the conv-2 ReLU mask and pool
selector only shrink, the head cotangent is in [−1,1], the two masked Wᵀ
steps and the unmasked W₃ ride layerAct). Used to bound the real conv-1
cotangent ∑ convTap·c₂ in the conv-1 rung.
The float conv-2 backward (transpose conv) against a perturbed
cotangent. The rounded M.dot of the exact convTap slab against the
float conv-2-output cotangent c2F, vs the certified ∑ convTap·c2R — the
convTap-flattening (sum_t3) plus dot_perturbed_close (fan-in
c·(2h)·(2w), per-entry tap bound w₂, float-cotangent magnitude C2t,
drift e₂). Generic in (c2F, c2R) so the conv-1 rung passes the conv-2
cotangent tensors abstractly.
The real conv-2 backward ∑ convTap·c2R is magnitude-bounded by the tap
ℓ∞-mass (c·(2h)·(2w))·w₂ times the cotangent bound CP — the (loose,
uniform) bound on the real conv-1 cotangent.
The binary32 conv-1 weight gradient is within an explicit budget of the
certified one (Increment 4 capstone) — the conv-1 peer of
cnn_conv2_grad_close, one conv-backward deeper. With x₀ exact, the
rendered trainer's W₁ gradient M.cnnConv1FloatGrad … stays within
cnnConv1GradBudget. The conv-2 cotangent chain is reused at a FLOAT conv-2
input relu(z̃₁) (cnn_conv2_cot_close); the conv-2 backward is a rounded
dot of the (exact) convTap slab against the float conv-2 cotangent slab
(dot_perturbed_close over c·(2h)·(2w)); the conv-1 ReLU mask freezes
(mask_scalar_close); the conv-1 weight dot rounds it
(dot_perturbed_close over (2h)·(2w)). Five quantitative margins are
carried; the bridge cnn_conv1_loss_gradAt_reluMask turns the gradAt
into the dot.
Segment-Lipschitz gradient for the conv1-kernel loss, explicit
constant. Under the FIVE margins at step radius D — relu₁
(a·D), relu₂ (c·kH·kW·w₂·a·D), pool selection (same radius,
POST-relu₂), relu₃, relu₄ — every routing decision freezes along
[u, u+d], BOTH conv Jacobians factor out point-free, and the
difference collapses to the softmax drift. The constant picks up the
conv1 weight-sharing multiplicity ((2h)·(2w))² AND the conv2
locality multiplicity (c·kH·kW)²·w₂².
One inexact SGD step on the CNN's FIRST conv kernel provably
decreases the cross-entropy loss. 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. Under the FIVE margins at the step radius
D = lr·(‖∇L‖₁ + |kernel|·η), every mask and the pool's routing
pattern freeze along the step, and the loss drops by
≥ lr·‖∇L‖₂²/2. With this, every conv kernel of the Chapter-3 CNN
has a proven descent statement.
One binary32 SGD step on the CNN's FIRST conv kernel provably decreases
the cross-entropy loss — with NO abstract gradient-accuracy parameter
(Increment 4 capstone, the deepest descent statement). The conv-1 peer of
cnn_conv2_float_sgd_descends: the gradient is the actual binary32 W₁
gradient M.cnnConv1FloatGrad …, accuracy proven by cnn_conv1_grad_close
(η := cnnConv1GradBudget, discharged per kernel entry via k4Idx_surj),
wired into the abstract cnn_conv1_sgd_descends. Five per-layer ROUND
margins feed the grad-close; the gradient-radius STEP margins +
hsmall/h1/h2 feed the drift-freeze and descent geometry. Every conv
kernel of the Chapter-3 CNN now has a float-faithful descent statement.
ℓ1 conv bias drift: summed over all output entries, at most
(h·w)·‖e‖₁ — one bias entry feeds every spatial position of its
channel.
Closed form of the conv bias-map pdiv — extracted from the
certified VJP (conv2d_bias_grad_has_vjp) by contracting its
.correct field against a basis vector, exactly as
conv2d_weight_pdiv. Bias entry o touches output (co,hi,wi)
iff co = o, with coefficient 1 — the Kronecker channel indicator.
Point-free (the bias map is affine), so along a step segment only
the head gradient moves.
Per-entry drift of the relu₃ pre-activation, conv2-bias rung.
Per-entry drift of the relu₄ pre-activation, conv2-bias rung.
Logit drift through the whole conv2-bias chain.
The relu₂ margin (at the bias radius D) keeps the conv
pre-activation off the kink along the whole step segment.
The POST-relu tensor stays within the bias-rung pool margin radius
D along the whole step segment.
The relu₃ margin (at the bias radius) keeps the first head pre-activation off the kink along the whole step segment.
The relu₄ margin (at the bias radius) keeps the second head pre-activation off the kink along the whole step segment.
The loss-of-conv2-bias map is differentiable at any four-condition point.
Closed form of the conv2 bias loss gradient at any four-margin
point — the EXISTING fold conv_bias_total_loss_grad_fold contracted
with the pool-collapsed head gradient (pool_relu_input_grad, reused
verbatim) and the Kronecker bias Jacobian (conv2d_bias_pdiv).
Segment-Lipschitz gradient for the conv2-bias loss, explicit
constant. The kernel-rung argument with the conv stage's a·D
radius replaced by the bare D — the bias Jacobian is a Kronecker
indicator with row mass (2h)·(2w), no input bound. Constant:
the kernel constant with a² ↦ 1.
One inexact SGD step on the CNN's second conv BIAS provably
decreases the cross-entropy loss. The conv2-kernel capstone with
the bias-rung radii: the four margins at the step radius
D = lr·(‖∇L‖₁ + c·η) carry no input bound a (the bias Jacobian
is a Kronecker indicator), and the parameter needs no
flatten/unflatten plumbing — the bias IS a vector.
Per-entry conv2-preactivation drift under a conv1 bias
perturbation: the perturbation crosses conv2 as a function of its
INPUT, picking up the locality factor c·kH·kW·w₂.
POST-relu₂ tensor drift under a conv1 bias perturbation — what the pool margin consumes on the conv1-bias rung.
Pooled ℓ1 drift under a conv1 bias perturbation: conv1 (ℓ1,
spatial multiplicity, no a) → relu → conv2-as-input (ℓ1,
LOCALITY multiplicity c·kH·kW) → relu → pool.
Per-entry drift of the relu₃ pre-activation, conv1-bias rung.
Per-entry drift of the relu₄ pre-activation, conv1-bias rung.
Logit drift through the whole conv1-bias chain.
The relu₁ margin (at the bias radius D) keeps the conv1
pre-activation off the kink.
The relu₂ margin (at the conv1-bias radius) keeps the conv2 pre-activation off the kink.
The POST-relu₂ tensor stays within the conv1-bias pool margin radius along the whole step segment.
The relu₃ margin (at the conv1-bias radius) keeps the first head pre-activation off the kink.
The relu₄ margin (at the conv1-bias radius) keeps the second head pre-activation off the kink.
The loss-of-conv1-bias map is differentiable at any five-condition point.
Closed form of the conv1 bias loss gradient at any five-margin
point — the bias fold at conv1, 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.
Segment-Lipschitz gradient for the conv1-bias loss, explicit
constant. The conv1-kernel argument with the conv1 stage's a·D
radii replaced by the bare D — the bias Jacobian is a Kronecker
indicator with row mass (2h)·(2w). Constant: the conv1-kernel
constant with a² ↦ 1.
One inexact SGD step on the CNN's FIRST conv BIAS provably
decreases the cross-entropy loss. The conv1-kernel capstone with
the bias-rung radii: the FIVE margins at the step radius
D = lr·(‖∇L‖₁ + c·η) carry no input bound a (the bias Jacobian
is a Kronecker indicator) and the parameter needs no
flatten/unflatten plumbing. With this theorem every parameter of
the Chapter-3 CNN — both conv kernels, both conv biases, and the
three dense layers (weights and biases via the MLP rungs) — has a
proven descent statement.
Float sum against a perturbed summand — the conv-BIAS grad-close's
final reduction, the M.sum peer of dot_perturbed_close (no left
operand A: the bias Jacobian is the bare channel indicator, so the
contraction is a plain reduction, not a dot). M.sum B̃ vs the certified
∑ Bᵢ splits into the Higham sum rounding on B̃ (sum_close, fan-in n)
plus the per-entry drift |B̃ᵢ − Bᵢ| ≤ eB. With |B̃ᵢ| ≤ Ct the bound is
closed-form.
The binary32 conv-2 bias gradient the rendered trainer computes — the
bias peer of cnnConv2FloatGrad: at output channel o it is the float SUM
M.sum (cotWin c̃Conv o) of the same float conv-2-output cotangent slab
(the bias Jacobian is the channel indicator, so there is no convPadWin
left operand and no per-slot kernel index — one entry per channel).
Equations
- One or more equations did not get rendered due to their size.
Instances For
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_eq_single); the remaining spatial
∑ hi wi is packaged as ∑ s, cotWin c o s (convBiasGrad_eq_sum) — the
quantity the rendered trainer's float bias SUM rounds.
The conv-2 bias-gradient grad-close budget — cnnConv2GradBudget with
the a· input factor stripped (the bias Jacobian carries no input window):
the spatial sum's Higham γ over (2h)·(2w) against the float-cotangent
magnitude (cnnConv2CotMag + cnnConv2CotBudget) plus the per-entry
cotangent drift cnnConv2CotBudget. The cotangent chain is the exact
conv-2-input (aX2 = a, eX2 = 0) instance of the factored
cnnConv2CotBudget / cnnConv2CotMag.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The binary32 conv-2 BIAS gradient is within an explicit budget of the
certified one — the bias peer of cnn_conv2_grad_close, built on the
factored conv-2 cotangent chain at the exact conv-2 input x₁
(cnn_conv2_cot_close with aX2 = a, eX2 = 0) and the spatial-SUM core
sum_perturbed_close. The bridge cnn_conv2_bias_loss_gradAt_reluMask
turns the gradAt into the sum the float bias gradient rounds. Four
quantitative margins (conv-output, pool POST-relu, z̃₃, z̃₄) freeze the
routing.
One inexact SGD step on the CNN's second conv BIAS provably decreases the
cross-entropy loss — the bias peer of cnn_conv2_float_sgd_descends: the
gradient is the actual binary32 bias gradient M.cnnConv2BiasFloatGrad …,
and its accuracy is proven by cnn_conv2_bias_grad_close
(η := cnnConv2BiasGradBudget, discharged per output channel — the bias IS
a vector, so no flatten/unflatten plumbing), not assumed. The two
rounding-margin families are carried as the honest first cut, exactly as the
weight rungs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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_eq_single + convBiasGrad_eq_sum) to the spatial SUM
the float bias gradient rounds.
The conv-1 bias-gradient grad-close budget — cnnConv1GradBudget with
the a· input factors stripped (the bias Jacobian carries no input window):
the spatial sum's Higham γ over (2h)·(2w) against the float conv-1
cotangent magnitude C1t = c(2h)(2w)·w₂·CP + eback plus the per-entry drift
eback (the conv-2 backward budget). Reuses the factored cnnConv2CotMag
/cnnConv2CotBudget at the FLOAT conv-2 input (aX2 = A₁, eX2 = E₁).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The binary32 conv-1 BIAS gradient is within an explicit budget of the
certified one — the bias peer of cnn_conv1_grad_close, built on the
factored conv-2 cotangent chain at the FLOAT conv-2 input relu(z̃₁)
(cnn_conv2_cot_close), the conv-2 backward convTap_back_close, the
conv-1 ReLU-mask freeze (mask_scalar_close), and the spatial-SUM core
sum_perturbed_close. Five quantitative margins freeze the routing; the
bridge cnn_conv1_bias_loss_gradAt_reluMask turns the gradAt into the
sum.
One inexact SGD step on the CNN's first conv BIAS provably decreases the
cross-entropy loss — the bias peer of cnn_conv1_float_sgd_descends, the
deepest descent rung: the gradient is the actual binary32 bias gradient
M.cnnConv1BiasFloatGrad …, accuracy proven by cnn_conv1_bias_grad_close
(η := cnnConv1BiasGradBudget, discharged per output channel — the bias IS a
vector), not assumed. With this, every conv weight AND bias of the
Chapter-3 CNN is a float-faithful descent step.