CIFAR-8 last-conv SGD descent — the first non-MNIST provable descent (A2 probe) #

planning/archive/tier23_float_and_syntactic_faithfulness.md A2 asked the genuinely-uncertain question: does the segment-Lipschitz SGD-descent argument (proven for the MNIST CNN, SgdDescentCnn.lean) reach a CIFAR net? This file answers it.

The finding. CIFAR-8's tail — its last conv W₈ (c4→c4) → relu → maxpool → three denses → CE — is byte-for-byte the program cnn_conv2_sgd_descends proves descent for. So descent at the LAST conv layer reaches CIFAR-8 for free, with the SAME non-vacuous admissible lr as MNIST: it is an instance of the MNIST lemma at the frozen earlier-layer features. Made rigorous in two steps:

• cifarCnn8Forward_factor — the actual committed net factors as head ∘ (relu ∘ flatConv W₈) ∘ prefix7 (pure rfl; Function.comp is definitionally associative).
• cifar8_lastConv_sgd_descends — one SGD step on W₈ (the earlier seven conv layers held fixed, their output on image being the frozen feature map x₁) decreases the CIFAR-8 cross-entropy by ≥ lr·‖∇‖²/2. Proved by reducing the CIFAR-8 loss-as-a-function-of-W₈ to the cnn_conv2 program at x₁ (hfac, via the factor lemma + flatConv = flatten∘conv2d∘unflatten) and applying cnn_conv2_sgd_descends.

The honest stop (why this is the ceiling). Descent through the depth of all eight conv layers is NOT proved, by design: cnn_conv2_sgd_descends's admissible-lr condition hsmall is a PRODUCT of the per-layer operator-norm factors (the three dense bounds × spatial). Each additional conv layer would multiply another (spatial · weight-bound) factor into that product, so the admissible lr shrinks geometrically with depth ⇒ vacuous in any realistic regime. This is the SAME compounding mechanism that puts deep-net descent off-limits. So last-conv descent is the honest reach of provable descent for CIFAR; full-depth / end-to-end CIFAR descent stays open.