Concat occurrence accumulation in directed CROWN #
The coordinate map splits the outgoing objective by parent occurrence. The fold then adds every occurrence into the graph table, preserving repeated parents and empty slices.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.represents_fold
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{ι : Type}
(indices : List ι)
(parent : ι → ℕ)
(box : ι → FlatBox α)
(a : ι → ℕ → ℝ)
{dims : ℕ → ℕ}
{v : ℕ → ℕ → ℝ}
{input k : ℕ}
{st : Internal.DirectedBackwardState α}
{z : ℝ}
(h : Represents dims v input k st z)
(hparent : ∀ (i : ι), parent i < st.coeffs.size)
(hlive : ∀ (i : ι), parent i ∈ pending input k)
(hbox : ∀ (i : ι), RowEncloses (box i) (dims (parent i)) (a i))
:
Represents dims v input k
(List.foldl
(fun (state : Internal.DirectedBackwardState α) (i : ι) => Internal.addDirectedCoeff state (parent i) (box i)) st
indices)
(z + (List.map (fun (i : ι) => dot (dims (parent i)) (a i) (v (parent i))) indices).sum)
Folding a list of enclosed contributions adds exactly the sum of their real objectives.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.dot_concat
(layout : ConcatLayout)
(parents : Array ℕ)
(a y : ℕ → ℝ)
(v : ℕ → ℕ → ℝ)
(hy :
∀ (parent : Fin layout.lengths.length) (i : Fin (layout.parentShape parent).size),
y ↑(layout.flatEquiv ⟨parent, i⟩) = v parents[↑parent]! ↑i)
:
The concat coordinate bijection preserves the exact objective, with one term per occurrence.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.represents_concat
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{dims : ℕ → ℕ}
{v : ℕ → ℕ → ℝ}
{input k : ℕ}
{st : Internal.DirectedBackwardState α}
{z : ℝ}
(h : Represents dims v input k st z)
(layout : ConcatLayout)
(parents : Array ℕ)
(hsize : parents.size = layout.lengths.length)
(hparent : ∀ p ∈ parents, p < st.coeffs.size)
(hlive : ∀ p ∈ parents, p ∈ pending input k)
(hdim : ∀ (parent : Fin layout.lengths.length), dims parents[↑parent]! = (layout.parentShape parent).size)
{aB : FlatBox α}
{a y : ℕ → ℝ}
(ha : RowEncloses aB layout.outputShape.size a)
(hy :
∀ (parent : Fin layout.lengths.length) (i : Fin (layout.parentShape parent).size),
y ↑(layout.flatEquiv ⟨parent, i⟩) = v parents[↑parent]! ↑i)
{coefficients : Array (FlatBox α)}
(hresult : Internal.splitDirectedCoeff layout aB = some coefficients)
:
Represents dims v input k
(Array.foldl
(fun (state : Internal.DirectedBackwardState α) (entry : ℕ × FlatBox α) =>
Internal.addDirectedCoeff state entry.1 entry.2)
st (parents.zip coefficients))
(z + dot layout.outputShape.size a y)
The engine's concat split and occurrence fold enclose the exact routed objective.