Rounded softmax range transfers

Softmax probabilities are bounded using the real, max-shifted specifications. Axis permutations preserve these coordinate bounds. The hard-mask transfer additionally detects blocked entries and rows with exactly one allowed entry.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.softmax_moved_rowWidth (s : Spec.Shape) (axis : ℕ) (haxis : axis < s.rank) : Proofs.Autograd.SoftmaxAxis.rowWidth (s.applyAdjacentSwaps (Spec.Shape.moveAxisToInnermostSwaps s.rank axis)) = s.toList[axis]?.getD 0

Moving a valid softmax axis to the end preserves its extent as the row width.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.softmaxInnermostSpec_mem_Icc {s : Spec.Shape} (x : TorchLean.Tensor ℝ s) (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (Activation.Internal.softmaxInnermostSpec x) c ∈ Set.Icc 0 1

Every coordinate of the actual innermost softmax lies in the closed unit interval.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.softmaxInnermostSpec_eq_one {s : Spec.Shape} (x : TorchLean.Tensor ℝ s) (hwidth : Proofs.Autograd.SoftmaxAxis.rowWidth s = 1) (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (Activation.Internal.softmaxInnermostSpec x) c = 1

A singleton innermost row has probability one, independently of its logit.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.softmaxSpec_mem_Icc {s : Spec.Shape} (axis : ℕ) [Spec.Shape.AxisInBounds axis s] (x : TorchLean.Tensor ℝ s) (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (Activation.softmaxSpec axis x) c ∈ Set.Icc 0 1

The actual real softmax along any valid axis has probability-valued coordinates.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.softmaxSpec_eq_one {s : Spec.Shape} (axis : ℕ) [Spec.Shape.AxisInBounds axis s] (x : TorchLean.Tensor ℝ s) (hwidth : s.toList[axis]?.getD 0 = 1) (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (Activation.softmaxSpec axis x) c = 1

Softmax on a singleton selected axis is exactly one at every coordinate.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.hardMaskedSoftmaxVecSpec_eq_zero {n : ℕ} (x : TorchLean.Tensor ℝ [n]) (allowed : TorchLean.Tensor Bool [n]) (i : Fin n) (hi : allowed.getScalar i = false) : (Spec.hardMaskedSoftmaxVecSpec x allowed).getScalar i = 0

A blocked logit has exactly zero probability in the real hard-mask specification.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.hardMaskedSoftmaxVecSpec_mem_Icc {n : ℕ} (x : TorchLean.Tensor ℝ [n]) (allowed : TorchLean.Tensor Bool [n]) (i : Fin n) : (Spec.hardMaskedSoftmaxVecSpec x allowed).getScalar i ∈ Set.Icc 0 1

Hard-masked probabilities lie in the unit interval, including an entirely blocked row.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.hardMaskedSoftmaxVecSpec_eq_one {n : ℕ} (x : TorchLean.Tensor ℝ [n]) (allowed : TorchLean.Tensor Bool [n]) (i : Fin n) (hi : allowed.getScalar i = true) (hunique : ∀ (j : Fin n), allowed.getScalar j = true → j = i) : (Spec.hardMaskedSoftmaxVecSpec x allowed).getScalar i = 1

The only allowed entry in a hard-mask row has probability one.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpSoftmaxRange_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} (axis : ℕ) [Spec.Shape.AxisInBounds axis s] (x : TorchLean.Tensor ℝ s) {g : ℕ → ℝ} (hg : ∀ (c : s.Coord), g ↑c.linearize = TorchLean.Tensor.Internal.Rep.get (Activation.softmaxSpec axis x) c) : RowEncloses (ibpSoftmaxRange s axis s.size) s.size g

The executable range box encloses the actual real softmax of any input tensor.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpHardMaskedSoftmaxLastTensor_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} (lo hi : TorchLean.Tensor α s) (x : TorchLean.Tensor ℝ s) (allowed : TorchLean.Tensor Bool s) (c : s.Coord) : LawfulBoundOps.toReal (TorchLean.Tensor.Internal.Rep.get (ibpHardMaskedSoftmaxLastTensor lo hi allowed).1 c) ≤ TorchLean.Tensor.Internal.Rep.get (Spec.hardMaskedSoftmaxSpec x allowed) c ∧ TorchLean.Tensor.Internal.Rep.get (Spec.hardMaskedSoftmaxSpec x allowed) c ≤ LawfulBoundOps.toReal (TorchLean.Tensor.Internal.Rep.get (ibpHardMaskedSoftmaxLastTensor lo hi allowed).2 c)

The actual recursive hard-mask transfer encloses its real specification at every rank.