Directed enclosure for max pooling

The window fold skips padded cells and uses zero only when the entire fold is empty. Its comparison selects an endpoint exactly; the proof needs the scalar order law, not rounded addition or an assumption that pooling windows contain positive values.

inductive NN.MLTheory.CROWN.Graph.DirectedBackward.OptionEncloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] : Option α → Option α → Option ℝ → Prop

Three optional window values have matching presence and enclosing scalar values.

• none {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] : OptionEncloses Option.none Option.none Option.none
• some {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {lo hi : α} {x : ℝ} (bounds : LawfulBoundOps.toReal lo ≤ x ∧ x ≤ LawfulBoundOps.toReal hi) : OptionEncloses (Option.some lo) (Option.some hi) (Option.some x)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.OptionEncloses.getD_zero {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {lo hi : Option α} {x : Option ℝ} (h : OptionEncloses lo hi x) : LawfulBoundOps.toReal (lo.getD 0) ≤ x.getD 0 ∧ x.getD 0 ≤ LawfulBoundOps.toReal (hi.getD 0)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.value_selectedMax {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (a b : α) : LawfulBoundOps.toReal (if (decide (b > a) || !decide (a > b) && !b == b) = true then b else a) = max (LawfulBoundOps.toReal a) (LawfulBoundOps.toReal b)

The unordered-value branch does not require reflexive scalar equality. Under the order law, two mutually non-greater values denote the same real number.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.selectedMax_real (a b : ℝ) : (if (decide (b > a) || !decide (a > b) && !b == b) = true then b else a) = max a b

def NN.MLTheory.CROWN.Graph.DirectedBackward.poolMaxStep {β : Type} [Context β] (best candidate : Option β) : Option β

The max-pool fold step, with absent padded candidates skipped.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.OptionEncloses.poolMaxStep {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {lo hi clo chi : Option α} {x cx : Option ℝ} (h : OptionEncloses lo hi x) (hc : OptionEncloses clo chi cx) : OptionEncloses (DirectedBackward.poolMaxStep lo clo) (DirectedBackward.poolMaxStep hi chi) (DirectedBackward.poolMaxStep x cx)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.foldl_rel₃ {ι β γ δ : Type} (R : β → γ → δ → Prop) (indices : List ι) {fl : β → ι → β} {fu : γ → ι → γ} {fx : δ → ι → δ} (hstep : ∀ (l : β) (u : γ) (x : δ) (i : ι), R l u x → R (fl l i) (fu u i) (fx x i)) {l : β} {u : γ} {x : δ} (h : R l u x) : R (List.foldl fl l indices) (List.foldl fu u indices) (List.foldl fx x indices)

A ternary relation preserved by each list step is preserved by the complete fold.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.foldlIndices_rel₃ {β γ δ : Type} (R : β → γ → δ → Prop) (dims : List ℕ) {fl : β → List ℕ → β} {fu : γ → List ℕ → γ} {fx : δ → List ℕ → δ} (hstep : ∀ (l : β) (u : γ) (x : δ) (i : List ℕ), R l u x → R (fl l i) (fu u i) (fx x i)) {l : β} {u : γ} {x : δ} (h : R l u x) : R (Spec.Conv.Internal.foldlIndices dims l fl) (Spec.Conv.Internal.foldlIndices dims u fu) (Spec.Conv.Internal.foldlIndices dims x fx)

The spatial iterator preserves a relation independently of rank and empty extents.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.paddedAverage {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {d : ℕ} {spatial : TorchLean.Tensor ℕ [d]} {lo hi : TorchLean.Tensor α (Spec.Shape.ofList (TorchLean.Tensor.Internal.Rep.data spatial).toList)} {x : TorchLean.Tensor ℝ (Spec.Shape.ofList (TorchLean.Tensor.Internal.Rep.data spatial).toList)} (h : TensorEncloses lo hi x) (out window stride padding : List ℕ) : LawfulBoundOps.toReal (Spec.Pooling.Internal.getPaddedAverageInputVal lo out window stride padding) ≤ Spec.Pooling.Internal.getPaddedAverageInputVal x out window stride padding ∧ Spec.Pooling.Internal.getPaddedAverageInputVal x out window stride padding ≤ LawfulBoundOps.toReal (Spec.Pooling.Internal.getPaddedAverageInputVal hi out window stride padding)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.paddedMax {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {d : ℕ} {spatial : TorchLean.Tensor ℕ [d]} {lo hi : TorchLean.Tensor α (Spec.Shape.ofList (TorchLean.Tensor.Internal.Rep.data spatial).toList)} {x : TorchLean.Tensor ℝ (Spec.Shape.ofList (TorchLean.Tensor.Internal.Rep.data spatial).toList)} (h : TensorEncloses lo hi x) (out window stride padding : List ℕ) : OptionEncloses (Spec.Pooling.Internal.getPaddedMaxInputVal? lo out window stride padding) (Spec.Pooling.Internal.getPaddedMaxInputVal? hi out window stride padding) (Spec.Pooling.Internal.getPaddedMaxInputVal? x out window stride padding)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.maxPoolValue {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {d : ℕ} {spatial : TorchLean.Tensor ℕ [d]} {lo hi : TorchLean.Tensor α (Spec.Shape.ofList (TorchLean.Tensor.Internal.Rep.data spatial).toList)} {x : TorchLean.Tensor ℝ (Spec.Shape.ofList (TorchLean.Tensor.Internal.Rep.data spatial).toList)} (h : TensorEncloses lo hi x) (out kernel stride padding : List ℕ) : LawfulBoundOps.toReal (Spec.Pooling.Internal.maxPoolValue lo out kernel stride padding) ≤ Spec.Pooling.Internal.maxPoolValue x out kernel stride padding ∧ Spec.Pooling.Internal.maxPoolValue x out kernel stride padding ≤ LawfulBoundOps.toReal (Spec.Pooling.Internal.maxPoolValue hi out kernel stride padding)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.maxPoolSpatial {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {d : ℕ} {kernel stride padding spatial : TorchLean.Tensor ℕ [d]} {hk : ∀ (i : Fin d), kernel.getScalar i ≠ 0} {hs : ∀ (i : Fin d), stride.getScalar i ≠ 0} (layer : Spec.MaxPoolSpec d kernel stride padding hk hs) {lo hi : TorchLean.Tensor α (Spec.Shape.ofList (TorchLean.Tensor.Internal.Rep.data spatial).toList)} {x : TorchLean.Tensor ℝ (Spec.Shape.ofList (TorchLean.Tensor.Internal.Rep.data spatial).toList)} (h : TensorEncloses lo hi x) : TensorEncloses (Spec.maxPoolSpatialSpec layer lo) (Spec.maxPoolSpatialSpec layer hi) (Spec.maxPoolSpatialSpec layer x)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.mapLeading {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (leading : Spec.Shape) {s t : Spec.Shape} {fl fu : TorchLean.Tensor α s → TorchLean.Tensor α t} {fx : TorchLean.Tensor ℝ s → TorchLean.Tensor ℝ t} (hstep : ∀ {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s}, TensorEncloses lo hi x → TensorEncloses (fl lo) (fu hi) (fx x)) {lo hi : TorchLean.Tensor α (leading.concat s)} {x : TorchLean.Tensor ℝ (leading.concat s)} (h : TensorEncloses lo hi x) : TensorEncloses (TorchLean.Tensor.mapLeading leading fl lo) (TorchLean.Tensor.mapLeading leading fu hi) (TorchLean.Tensor.mapLeading leading fx x)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.evalMaxPool_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (config : IR.WindowConfig) : TensorTransferEncloses (IR.Graph.evalMaxPool config) (IR.Graph.evalMaxPool config)

The arbitrary-rank real max-pool evaluator is enclosed by the two endpoint evaluations.