BugZoo: autograd domains before masks

PyTorch's own autograd notes document a sharp footgun: if a program computes $x/0$ and only masks the bad value afterward, the forward loss can look masked while the backward graph still contains the undefined division. The documented example gives a nan gradient for the masked-out entry:

https://docs.pytorch.org/docs/main/notes/autograd.html#division-by-zero-in-autograd

TorchLean's useful claim here is the graph-level contract. The safe-domain choice is an explicit spec node: use safedivSpec in the computation that is recorded, then mask or weight the resulting tensor. Downstream proofs and importers can then see the protected division directly in the graph shape.

Here safedivSpec means division by denominator + epsilon; it does not clamp the denominator away from zero. A denominator equal to -epsilon still makes that sum zero. The unfolding theorem below identifies the formula, but does not establish finite forward values or correct gradients for arbitrary inputs or scalar instances. Those require domain and backend-conformance evidence.

def NN.Examples.BugZoo.AutogradDomain.maskAfterSafeDiv {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (mask numerator denominator : TorchLean.Tensor α s) : TorchLean.Tensor α s

Shift the denominator by epsilon before applying the numeric contribution mask. The shifted denominator must still be nonzero.

def NN.Examples.BugZoo.AutogradDomain.unsafeDivThenMask {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (mask numerator denominator : TorchLean.Tensor α s) : TorchLean.Tensor α s

Raw division followed by a numeric mask. A zero mask does not remove an undefined division.

theorem NN.Examples.BugZoo.AutogradDomain.maskAfterSafeDiv_uses_epsilon_denominator {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (mask numerator denominator : TorchLean.Tensor α s) : maskAfterSafeDiv mask numerator denominator = mask.mulSpec (TorchLean.Tensor.map2Spec (fun (a b : α) => a / (b + Context.defaultEpsilon)) numerator denominator)

The shifted denominator is visible in the specification before masking.

theorem NN.Examples.BugZoo.AutogradDomain.unsafeDivThenMask_unfold {s : Spec.Shape} {α : Type} [TorchLean.Storage α] [Context α] (mask numerator denominator : TorchLean.Tensor α s) : unsafeDivThenMask mask numerator denominator = mask.mulSpec (numerator.divSpec denominator)

The contrast graph really is a raw division followed by masking.