Structural transfers in the directed backward sweep

Structural routing changes which node owes a coefficient. Addition and subtraction accumulate both parent occurrences, including when their graph identifiers coincide.

def NN.MLTheory.CROWN.Graph.DirectedBackward.extendFin {n : ℕ} (f : Fin n → ℝ) (i : ℕ) : ℝ

Extending a finite vector by zero avoids dependent casts in the graph's coefficient table.

@[simp]

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.extendFin_val {n : ℕ} (f : Fin n → ℝ) (i : Fin n) : extendFin f ↑i = f i

The extension agrees with the finite vector at every valid coordinate.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.represents_copy {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {input k id pid : ℕ} {st : Internal.DirectedBackwardState α} {z : ℝ} (h : Represents dims v input k st z) (hp : pid < st.coeffs.size) (hlive : pid ∈ pending input k) {aB : FlatBox α} {a : ℕ → ℝ} (ha : RowEncloses aB (dims id) a) (heq : CopyEquation dims v id pid) : Represents dims v input k (Internal.addDirectedCoeff st pid aB) (z + dot (dims id) a (v id))

Copying a coefficient to a value-preserving parent preserves its exact contribution.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.represents_addParents {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {input k id p q : ℕ} {st : Internal.DirectedBackwardState α} {z : ℝ} (h : Represents dims v input k st z) (hp : p < st.coeffs.size) (hq : q < st.coeffs.size) (hplive : p ∈ pending input k) (hqlive : q ∈ pending input k) {aB : FlatBox α} {a : ℕ → ℝ} (ha : RowEncloses aB (dims id) a) (hdp : dims p = dims id) (hdq : dims q = dims id) (hy : ∀ (i : Fin (dims id)), v id ↑i = v p ↑i + v q ↑i) : Represents dims v input k (Internal.addDirectedCoeff (Internal.addDirectedCoeff st p aB) q aB) (z + dot (dims id) a (v id))

An addition routes the same coefficient to both parents and sums both contributions.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.represents_subParents {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {input k id p q : ℕ} {st : Internal.DirectedBackwardState α} {z : ℝ} (h : Represents dims v input k st z) (hp : p < st.coeffs.size) (hq : q < st.coeffs.size) (hplive : p ∈ pending input k) (hqlive : q ∈ pending input k) {aB : FlatBox α} {a : ℕ → ℝ} (ha : RowEncloses aB (dims id) a) (hdp : dims p = dims id) (hdq : dims q = dims id) (hy : ∀ (i : Fin (dims id)), v id ↑i = v p ↑i - v q ↑i) : Represents dims v input k (Internal.addDirectedCoeff (Internal.addDirectedCoeff st p aB) q (Internal.negateDirectedCoeff aB)) (z + dot (dims id) a (v id))

Subtraction routes a directed negation to the right parent, including repeated-parent cancellation without assuming that the rounded coefficient interval is a point.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.broadcast_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} (lo hi : TorchLean.Tensor α [1]) (a : ℝ) (ha : LawfulBoundOps.toReal (lo.getScalar 0) ≤ a ∧ a ≤ LawfulBoundOps.toReal (hi.getScalar 0)) : RowEncloses { dim := n, lo := TorchLean.Tensor.full (Spec.Shape.dim n Spec.Shape.scalar) (Spec.getAtOrZero lo [0]), hi := TorchLean.Tensor.full (Spec.Shape.dim n Spec.Shape.scalar) (Spec.getAtOrZero hi [0]) } n fun (x : ℕ) => a

Broadcasting a scalar coefficient to all coordinates encloses the exact sum pullback.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.gather_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {m n : ℕ} (lo hi : TorchLean.Tensor α [m]) (a : ℕ → ℝ) (ha : RowEncloses { dim := m, lo := lo, hi := hi } m a) (index : Fin n → Fin m) : RowEncloses { dim := n, lo := TorchLean.Tensor.ofFn fun (i : Fin n) => lo.getScalar (index i), hi := TorchLean.Tensor.ofFn fun (i : Fin n) => hi.getScalar (index i) } n (extendFin fun (i : Fin n) => a ↑(index i))

A coefficient gathered along a coordinate map encloses the same gathered real vector.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.dot_permutation {n : ℕ} (perm : Fin n → Fin n) (hperm : Function.Bijective perm) (a x y : ℕ → ℝ) (hy : ∀ (i : Fin n), y ↑(perm i) = x ↑i) : dot n a y = dot n (extendFin fun (i : Fin n) => a ↑(perm i)) x

A bijective coordinate change preserves an exact real objective.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.axisPermutation_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id pid : ℕ} {aB aX : FlatBox α} {a : ℕ → ℝ} (ha : RowEncloses aB (dims id) a) (shape : Spec.Shape) (forward : Array ℕ) (heq : PermutationEquation dims v id pid shape forward) (hresult : Internal.directedAxisPermutation? shape forward aB = some aX) : ∃ (a' : ℕ → ℝ), RowEncloses aX (dims pid) a' ∧ dot (dims id) a (v id) = dot (dims pid) a' (v pid)

The actual axis-permutation pullback encloses coefficients with the same real objective.