Documentation

LeanMlir.Proofs.Training.JacobianSeal

Nonzero-Jacobian seal — the generic "the backward is non-trivial here" bridge #

The whole-network capstones prove HasVJP.backward = pdiv-Jacobian-transpose. A degenerate witness (zero weights / constant output) satisfies that contract vacuously: its Jacobian is identically zero, so the backward map is the zero map and says nothing about a real gradient. A non-vacuity fact of the weaker kind (Mnv2FullBSeal.sealX_nonconstant) only rules out a constant forward — strictly weaker than a non-trivial backward at the witness.

This file supplies the missing level-3 seal (see planning/archive/whole_network_backward.md, Item B): the reusable bridge from a single nonzero Jacobian entry to a provably non-trivial backward, and the equivalence with fderiv ℝ f x ≠ 0. A witness then upgrades from "forward ≠ const" to "the rendered backward at this point is not the zero map" by exhibiting one pdiv f x i j ≠ 0 — which is what a genuine (non-degenerate) gradient requires.

The bridge is stated for the pointwise HasVJPAt the kinked witnesses are built as. The per-net seals discharge its pdiv ≠ 0 premise on the full-width batched nets themselves (ResNet34FullBSeal, ResNet50FullBSeal, MobileNetV2FullBSeal, MobileNetV4FullBSeal).

source
theorem Proofs.sum_smul_basisVec {m : ℕ} (v : Vec m) :
∑ i : Fin m, v i • basisVec i = v

The standard basis decomposition ∑ᵢ vᵢ · eᵢ = v on Vec m.

source
theorem Proofs.fderiv_eq_zero_of_pdiv_all_zero {m n : ℕ} (f : Vec m → Vec n) (x : Vec m) (hall : ∀ (i : Fin m) (j : Fin n), pdiv f x i j = 0) :
fderiv ℝ f x = 0

All Jacobian entries zero ⇒ the Fréchet derivative is the zero map. fderiv ℝ f x is ℝ-linear, so it is determined by its values on the standard basis; if those all vanish it vanishes everywhere (v = ∑ᵢ vᵢ·eᵢ). No differentiability hypothesis — at a non-smooth point fderiv is its junk-0 default and the entries are 0 too.

source
theorem Proofs.exists_pdiv_ne_of_fderiv_ne {m n : ℕ} (f : Vec m → Vec n) (x : Vec m) (hfd : fderiv ℝ f x ≠ 0) :
∃ (i : Fin m) (j : Fin n), pdiv f x i j ≠ 0

The seal in fderiv form. A nonzero Fréchet derivative at the witness yields a nonzero Jacobian entry — the clean analytic hypothesis behind HasVJPAt.backward_ne_zero_of_pdiv_ne. (Contrapositive of the all-zero lemma.)

source
theorem Proofs.HasVJPAt.backward_ne_zero_of_pdiv_ne {m n : ℕ} {f : Vec m → Vec n} {x : Vec m} (h : HasVJPAt f x) {i₀ : Fin m} {j₀ : Fin n} (hpd : pdiv f x i₀ j₀ ≠ 0) :
h.backward (basisVec j₀) i₀ ≠ 0

The nonzero-Jacobian seal. If the Jacobian of f at the witness x has a nonzero entry pdiv f x i₀ j₀ ≠ 0, then the proven backward there is not the zero map: probing it with the basis cotangent e_{j₀} returns the nonzero pdiv f x i₀ j₀ at row i₀. The cotangent collapses HasVJPAt.correct's sum to its single diagonal term.

source
theorem Proofs.HasVJPAt.backward_nontrivial_of_fderiv_ne {m n : ℕ} {f : Vec m → Vec n} {x : Vec m} (h : HasVJPAt f x) (hfd : fderiv ℝ f x ≠ 0) :
∃ (j₀ : Fin n) (i₀ : Fin m), h.backward (basisVec j₀) i₀ ≠ 0

The seal in fderiv form. A nonzero Fréchet derivative at the witness x ⇒ the proven backward there is non-trivial (some basis-cotangent probe returns a nonzero row). The form a whole-net witness uses: establish fderiv ℝ forward x ≠ 0 once, get a non-trivial backward for free.

source
theorem Proofs.fderiv_ne_zero_of_ray {m n : ℕ} {f : Vec m → Vec n} {x : Vec m} (v : Vec m) (hf : DifferentiableAt ℝ f x) (ℓ : Vec n → ℝ) (hℓ : DifferentiableAt ℝ ℓ (f x)) {c : ℝ} (hc : c ≠ 0) (hg : HasDerivAt (fun (t : ℝ) => ℓ (f (x + t • v))) c 0) :
fderiv ℝ f x ≠ 0

A nonzero directional derivative seals fderiv ≠ 0. If a readout ℓ of f (differentiable at f x) has derivative c ≠ 0 along the ray t ↦ x + t • v at t = 0, the Fréchet derivative of f at x is not the zero map (a zero one would give the readout derivative 0).

source
theorem Proofs.hasDerivAt_mul_self_zero {Q : ℝ → ℝ} (hQ : ContinuousAt Q 0) :
HasDerivAt (fun (t : ℝ) => t * Q t) (Q 0) 0

t · Q t has derivative Q 0 at 0 for any Q continuous there — the product-rule cross-term carries the factor t, so no derivative of Q is needed (its slope at 0 is Q itself).

source
theorem Proofs.hasDerivAt_mul_of_zero {S Q : ℝ → ℝ} {c : ℝ} (hS : HasDerivAt S c 0) (hS0 : S 0 = 0) (hQ : ContinuousAt Q 0) :
HasDerivAt (fun (t : ℝ) => S t * Q t) (c * Q 0) 0

⭐ S · Q at a zero of S — hasDerivAt_mul_self_zero where the carrier reaches the readout through a smooth but NON-AFFINE stage, so it is not t itself that factors out.

MobileNetV4's fused stage is swish: its two examples' outputs differ by swishGap β u, which vanishes at u = 0 and is differentiable there but is not a multiple of u. S is that gap along the ray and Q the BatchNorm factors below it; as before no derivative of Q is needed, only its continuity at 0.