Dense Jacobian — ∂(W·x + b)_j/∂x_i = W_{ij}. dense W b is the linear map x ↦ (Σ_i x_i W_{ij})_j plus the constant b, so pdiv_of_affine reads the entry off the basis vector and the Kronecker sum collapses.

Jacobian of dense wrt W — ∂dense(W, b, x)_j/∂W_{i, j'} = x_i·δ(j, j'). Over the flatten bijection v ↦ dense (unflatten v) b x is linear in v plus the constant b (pdiv_of_affine). Symmetric counterpart to pdiv_dense.

denseHasVJP's correct field, restated for mnistLinear so it can be cited by name.

Dense is everywhere differentiable. dense W b is affine in x, hence smooth; this is the underlying Differentiable ℝ statement that vjpCompAt needs when composing through dense layers.

Dense weight gradient is the outer product.

Mat.outer x dy is the cotangent-contracted Jacobian of dense(W, b, x) with respect to W, at every index.

(Mat.outer x dy) i j = ∑ k, pdiv (…) (Mat.flatten W) (fPF (i, j)) k · dy k

Dense bias gradient is identity.

∂ dense(W, b, x)_j / ∂ b_{j'} = δ(j, j'), so the bias backward is just dy itself: b' ↦ dense W b' x is the identity plus a constant (pdiv_of_affine).

relu is max · 0, coordinatewise.

ReLU output is always nonnegative.

ReLU is entrywise 1-Lipschitz — what lets a drift (or a rounding error) pass through a kinked layer unamplified.

The Jacobian of a diagonal 0/1 mask. If f has, at x, the derivative that keeps coordinate k when p k and zeroes it otherwise, its pdiv is the diagonal indicator of p. relu and relu6 at a smooth point are both this.

ReLU is differentiable at smooth points. Near x every coordinate keeps its sign (finitely many strict inequalities persist, Filter.eventually_all), so relu n agrees with reluLinearPart n x on a neighbourhood. EventuallyEq promotes the CLM's HasFDerivAt to ReLU's.

ReLU is DifferentiableAt at smooth points. Corollary of relu_hasFDerivAt; lets vjpCompAt chain through ReLU.

ReLU partial derivative — proved via relu_hasFDerivAt and direct evaluation at basisVec i.

Bridge: reluHasVJP's canonical backward matches the codegen formula at smooth points.

At any point where no coordinate of x is zero, the canonical pdiv-derived backward ∑ j, pdiv (relu n) x i j * dy j collapses to the framework subgradient if x i > 0 then dy i else 0 that MlirCodegen.lean actually emits. Closes the smooth-point half of the codegen trust boundary — what's left is just the kink convention.

The softmax entries sum to one (over a nonempty class set).

Public correctness theorem for reluHasVJP: the canonical witness's backward equals the pdiv-contracted Jacobian by definition.

Public correctness theorem for mlpHasVJP: same pattern as reluHasVJP_correct, lifted to the three-layer MLP forward.

Public correctness theorem for reluHasVJPAt — the pointwise (smooth-input) variant. Unlike reluHasVJP_correct, this wrapper's underlying .correct field is a real proof (pdiv_relu + sum-collapse), not rfl; the wrapper exposes it as a top-level proposition for tests/comparator/ re-verification.

Public correctness theorem for mlpHasVJPAt — the pointwise variant composed via vjpCompAt through dense → relu_at → dense → relu_at → dense. The underlying .correct field chains real chain-rule proofs (no rfl escape at the ReLU kinks).

ReLU6 is the identity inside its window. Wherever every coordinate is strictly inside (0,6), min (max · 0) 6 does nothing — the step every structural witness takes to collapse a relu6 stage to its BatchNorm. Stated at the top level rather than inside a witness namespace: it is a fact about the op, and BatchSeal's consumers outlive any one witness.

ReLU6 is continuous — min (max · 0) 6 coordinatewise. The peer of relu_continuous (below), for the ray argument of a relu6 net's seal.

relu is continuous everywhere — it is max · 0; only its derivative has a kink.

ReLU is the identity on a strictly-positive vector. Discharges the ReLU-as-identity steps that fold the composition into a plain conv stack at a smooth (everywhere-positive) point.