Margins freeze signs. If a value drifts by at most c and sits at distance more than c from the kink, the drifted value is still off the kink with the same sign — the ReLU mask cannot flip.

A dense layer's output moves by at most w·‖Δinput‖₁ per entry — the ℓ1→ℓ∞ operator bound used at every dense crossing of the chain.

A per-entry drift inside the margin keeps a pre-activation off the kink along the whole segment — for any parameter map Z whose entries move by at most ρ·‖e‖₁, the margin ρ·D < |Z v k| at step radius D freezes every sign on [v, v+e].

The ℓ1 mass of a flattened weight perturbation, summed column by column, is the total ℓ1 mass — finProdFinEquiv partitions the flat index set into the columns.

Summed over all coordinates, the pre-activation drift is bounded by a·‖e‖₁ total — the column masses tile the flat index set.

The margin keeps the pre-activation off the kink along the whole segment. With the step's ℓ1 mass at most D and inputs bounded by a, the pre-activation drifts by at most a·D — strictly inside the margin — so every point of [v, v + e] is off the kink with the original sign.

Loss input-gradient at the logits' input: ∂(CE ∘ dense W₂)/∂yⱼ = ∑ₖ W₂ⱼₖ·(softmax − onehot)ₖ — the pdiv-level form of the backward chain's dense-back step.

Loss input-gradient through one ReLU — at an off-kink point the chain picks up the mask: ∂(CE ∘ dense W₂ ∘ relu)/∂zⱼ = relu'(zⱼ)·∑ₖ W₂ⱼₖ·(softmax − onehot)ₖ. The pdiv-level form of the cotangent mlpCotOut1 delivers (cf. mlpCotOut1_denote).

ReLU then a dense layer: an input drift of ℓ1 mass B moves each output entry by at most w·B.

Segment-Lipschitz gradient for an MLP-slot loss, explicit constant. For a map Z into a ReLU layer's pre-activation whose entries move by at most σ·‖e‖₁ (hZ) and whose ℓ1 drift is at most ρ·‖e‖₁ (hZ1), and whose loss gradient at every off-kink point is a fixed row J (row mass ≤ ρ) contracted with the mask and the W₂ head (hgrad, needed only where Q holds): the margin σ·D freezes the mask along [v, v+d], the row factors out, and the difference collapses to the softmax drift. The hidden layer is the instance σ = ρ = a; the input layer takes Z = the middle pre-activation, σ = w₁·a, ρ = d₂·w₁·a, J = xᵢ·relu₀'s frozen mask·W₁'s row, Q = relu₀'s signs frozen.

The loss-of-W₁ map is differentiable wherever the hidden pre-activation is off the kinks.

Closed form of the hidden-layer loss gradient at any off-kink parameter point: ∂L/∂W₁_{ij} = a₀ᵢ·relu'(z₁ⱼ)·∑ₖ W₂ⱼₖ·(softmax − onehot)ₖ — the suite's conditional fold (mlp_hidden_total_loss_grad) re-expressed through gradAt with both pdiv factors collapsed to their certified closed forms. The hidden-layer peer of linear_loss_gradAt.

The hidden-layer logit drift: a weight perturbation of ℓ1 mass ‖e‖₁ moves every logit by at most w₂·a·‖e‖₁ — through the frozen dense, the 1-Lipschitz ReLU, and the column-tiled ℓ1 mass. No width factor.

Segment-Lipschitz gradient for the hidden-layer loss, explicit constant. Under the margin a·D < |z₁ⱼ| (the step cannot flip a ReLU sign — the masks freeze along the whole segment) and the small-step condition 2·w₂·a·D < 1, the gradient entries drift by at most (2·d₃·w₂²·a²/(1−2·w₂·a·D))·(t·D) along [v, v+d] — the exact shape descent_segment consumes. The hidden-layer peer of linear_loss_grad_lipschitz; MlpSlot.loss_grad_lipschitz at σ = ρ = a.

One inexact SGD step on the MLP's hidden weights decreases one example's cross-entropy loss (example (a₀, label), W₁ moving, every other parameter fixed). sgd_descends' smoothness hypotheses are discharged for the loss-of-W₁ map: differentiability along the segment and the segment-Lipschitz constant C = 2·d₃·w₂²·a²/(1−2·w₂·a·D) at step radius D = lr·(‖∇L‖₁ + d₁d₂·η) both come from the margin hypothesis — the step radius is small enough that no hidden ReLU can change sign. Remaining hypotheses: the oracle accuracy η (the float budgets), the margins, the small-step condition, and the two dominance conditions. Conclusion: the loss drops by ≥ lr·‖∇L‖₂²/2. The hidden-layer peer of linear_sgd_descends.

Loss input-gradient through the relu→dense→relu chain — the two-mask closed form relu'(z₀ⱼ)·∑ₗ W₁ⱼₗ·relu'(z₁ₗ)·∑ₖ W₂ₗₖ·(softmax − onehot)ₖ at a point with both pre-activations off the kinks. The pdiv-level form of the deepest cotangent mlpCotOut0 delivers (cf. mlpCotOut0_denote).

The loss-of-W₀ map is differentiable wherever both pre-activations are off the kinks.

Closed form of the input-layer loss gradient at any two-margin point: ∂L/∂W₀_{ij} = xᵢ·relu'(z₀ⱼ)·∑ₗ W₁ⱼₗ·relu'(z₁ₗ)·∑ₖ W₂ₗₖ· (softmax − onehot)ₖ — the deepest fold (mlp_input_total_loss_grad) with both pdiv factors collapsed. The input-layer peer of linear_loss_gradAt.

The layer-1 margin keeps the middle pre-activation off the kink along the segment: the perturbation arrives through one dense + ReLU, so the drift is at most w₁·a·D — the layer-1 analogue of margin_keeps_offkink.

Segment-Lipschitz gradient for the input-layer loss, explicit constant. Under both margins (neither ReLU layer's sign pattern can change along the step) and the small-step condition, the gradient entries drift by at most (2·d₃·d₂²·w₁²·w₂²·a²/(1−2·w₂·d₂·w₁·a·D))·(t·D). The input-layer peer of mlp_hidden_loss_grad_lipschitz; the extra d₂·w₁ is the middle layer's ℓ1→ℓ1 operator factor. MlpSlot.loss_grad_lipschitz at the middle pre-activation, σ = w₁·a, ρ = d₂·w₁·a.

One inexact SGD step on the MLP's input weights decreases one example's cross-entropy loss (example (x, label), W₀ moving, every other parameter fixed). The deepest descent capstone: both ReLU layers' margins at the step radius D = lr·(‖∇L‖₁ + d₀d₁·η) freeze the masks, the segment-Lipschitz constant C = 2·d₃·d₂²·w₁²·w₂²·a²/(1−2·w₂·d₂·w₁·a·D) is proven, and the loss drops by ≥ lr·‖∇L‖₂²/2. The oracle accuracy, the margins, the small-step and the two dominance conditions remain hypotheses. The input-layer peer of linear_sgd_descends; with this each MLP weight layer has a single-layer, single-example descent statement.

One SGD step with the FloatModel binary32 output-layer gradient decreases one example's cross-entropy loss; the gradient's accuracy is proven, not assumed. The output-layer rung of the η-composition. Since the top dense layer sits directly below the softmax-CE loss with no ReLU between, the loss-of-W₂ map is the linear net's loss at the hidden activation a₁ = relu(dense W₁ b₁ (relu(dense W₀ b₀ x))) — so this is linear_float_sgd_descends instantiated there, with the same scope (one example, W₂ moving, update in ℝ). The gradient is the FloatModel binary32 output-layer gradient M.linearFloatGrad W₂ b₂ a₁ and its accuracy η = mulErr u a 1 0 (cotErr …) is proven (by linear_grad_close, inside the linear theorem), not assumed. No margin needed — the output layer never crosses a kink.

The hidden and input rungs are mlp_hidden_float_sgd_descends and mlp_input_float_sgd_descends.

The binary32 hidden-layer (W₁) gradient is within an explicit budget of the certified one, per entry — the float-backward grad-close that the hidden η-composition needs. With the layer-1 input activation a₀ frozen exact (the descent moves only W₁), the FloatModel transcription computes the W₁ gradient as fl(a₀ᵢ · c̃₁ⱼ) where the float layer-1 cotangent c̃₁ = mask(z̃₁, W₂ᵀ·c̃₂) reads the float pre-activation z̃₁ = M.dense W₁ b₁ a₀ and the float softmax−onehot head c̃₂ at the float logits. This is within mulErr M.u a … 0 (layerBudget … (cotErr …)) of the certified a₀ᵢ · mask(z₁, W₂ᵀ·(softmax−onehot))ⱼ (= mlp_hidden_loss_gradAt), built from three reusable closes: the head (softmax_ce_cot_close, accuracy cotErr), the masked W₂ᵀ contraction (cot_step_close, under the quantitative margin E₁ < |z₁ⱼ| — forward rounding must not flip the layer-1 ReLU), and the final input multiply (mul_close, with the exact a₀ operand, ea = 0, exactly as the linear grad-close).

The certified hidden-layer loss gradient, in the reluMask form that mlp_w1_grad_close bounds against. At an off-kink parameter point (hz), mlp_hidden_loss_gradAt's closed form a₀ᵢ·relu'(z₁ⱼ)·∑ₖ W₂ⱼₖ·(softmax−onehot)ₖ equals the masked-W₂ᵀ- contraction form a₀ᵢ · reluMask(z₁, dense (fun j' i' => W₂ i' j') 0 (softmax−onehot))ⱼ. The bridge that lets the float grad-close (stated with reluMask) discharge mlp_hidden_sgd_descends' abstract η (stated with gradAt).

One SGD step with the FloatModel binary32 hidden-layer gradient decreases one example's cross-entropy loss; the gradient's accuracy is proven, not assumed. The hidden-layer rung of the η-composition. The gradient is the FloatModel binary32 W₁ gradient M.mlpHiddenFloatGrad W₁ b₁ W₂ b₂ a₀ fexp label, and its accuracy η = mulErr u a (layerAct …) 0 (layerBudget … (cotErr …)) is proven by mlp_w1_grad_close (via the reluMask↔gradAt bridge mlp_hidden_loss_gradAt_reluMask), not assumed.

Two margins are carried as hypotheses: the rounding margin hmargin_round (layerBudget < |z₁|, forward rounding must not flip the layer-1 ReLU — the grad-close precondition) and the step margin hmargin_step (a·D < |z₁|, the parameter step must not flip it along the segment — the smoothness precondition). They are the same shape ("nothing flips the layer-1 ReLU") and are not collapsed into one here. This is the hidden-layer peer of linear_float_sgd_descends / mlp_output_float_sgd_descends.

Scope: one example (a₀, label), the layer's weights only (other parameters fixed), and the update taken in ℝ — only the gradient is float-modelled.

A masked Wᵀ contraction in if-then-else form equals the reluMask form. (relu'(zₗ))·∑ₖ Wₗₖ·cₖ = reluMask z (Wᵀ·c) l — the per-step identity behind the gradAt↔reluMask bridges (mlp_hidden_/ mlp_input_loss_gradAt_reluMask): one ReLU-sign case split + mul_comm (the transpose dense (fun j i' => W i' j) 0 c reads ∑ₖ cₖ·Wₗₖ).

The certified input-layer loss gradient, in the nested reluMask form that mlp_w0_grad_close bounds against. At an off-kink point (both hz0, hz1), mlp_input_loss_gradAt's two-mask if-then-else closed form equals xᵢ · reluMask(z₀, W₁ᵀ·reluMask(z₁, W₂ᵀ·(softmax−onehot)))ⱼ. Two applications of reluMask_dense_transpose_eq (inner W₂ᵀ then outer W₁ᵀ), fired by simp_rw.