BugZoo: ignored labels are a reduction contract

PyTorch issue #75181 reported CrossEntropyLoss(ignore_index=...) returning nan for an all- ignored target case:

https://github.com/pytorch/pytorch/issues/75181

Represent ignored labels by explicit zero contributions and choose the empty-reduction policy.

def NN.Examples.BugZoo.IgnoredLabelLoss.labelContribution {α : Type} [Zero α] (active : Bool) (loss : α) : α

A per-example loss contributes exactly when its label is active.

@[simp]

theorem NN.Examples.BugZoo.IgnoredLabelLoss.ignored_label_contributes_zero {α : Type} [Zero α] (loss : α) : labelContribution false loss = 0

Ignored labels contribute no scalar loss.

@[simp]

theorem NN.Examples.BugZoo.IgnoredLabelLoss.active_label_contributes_loss {α : Type} [Zero α] (loss : α) : labelContribution true loss = loss

Active labels contribute their ordinary scalar loss.

def NN.Examples.BugZoo.IgnoredLabelLoss.safeMaskedMean {α : Type} [TorchLean.Storage α] [Context α] (total activeCount : α) : α

One explicit empty-reduction policy: divide by an epsilon-shifted active count.

The type of activeCount does not enforce a nonnegative integer count, and Context alone gives no positivity law for epsilon. Finiteness therefore depends on the chosen scalar instance and valid inputs; the theorem below only unfolds the chosen formula.

theorem NN.Examples.BugZoo.IgnoredLabelLoss.safeMaskedMean_uses_epsilon_denominator {α : Type} [TorchLean.Storage α] [Context α] (total activeCount : α) : safeMaskedMean total activeCount = total / (activeCount + Context.defaultEpsilon)

The denominator policy for safeMaskedMean is visible in the definition.