Directed enclosure for average pooling

The executable transfer enumerates each padded window in flat order, encloses its real sum and count, and divides the resulting intervals. The spatial proof lifts over every leading axis, including empty leading dimensions.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpAvgPool?_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] {config : IR.WindowConfig} {s t : Spec.Shape} {B box : FlatBox α} {f : ℕ → ℝ} {y : TorchLean.Tensor ℝ t} (hB : RowEncloses B s.size f) (hy : IR.Graph.evalAvgPool config { shape := s, tensor := realTensor s f } = Except.ok { shape := t, tensor := y }) (hbox : ibpAvgPool? config s t B = some box) : RowEncloses box t.size (tensorValues y)

Successful directed average pooling encloses the actual real evaluator, for every accepted window configuration and every collection of leading dimensions.