Directed enclosure for arbitrary-axis concatenation

Concatenation transports endpoint bounds through the existing layout's coordinate equivalence. Parent occurrences remain distinct, including when a graph lists the same parent more than once.

def NN.MLTheory.CROWN.Graph.DirectedBackward.realConcat (layout : ConcatLayout) (f : Fin layout.lengths.length → ℕ → ℝ) (i : ℕ) : ℝ

Exact concat coordinates in the same layout used by the executable transfer.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.concatFlatBoxes?_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {layout : ConcatLayout} {boxes : Array (FlatBox α)} {box : FlatBox α} {f : Fin layout.lengths.length → ℕ → ℝ} (hbox : concatFlatBoxes? layout boxes = some box) (hparents : ∀ (p : Fin layout.lengths.length) (B : FlatBox α), boxes[↑p]? = some B → RowEncloses B (layout.parentShape p).size (f p)) : RowEncloses box layout.outputShape.size (realConcat layout f)

Checked concatenation encloses the exact value supplied by each parent occurrence.

def NN.MLTheory.CROWN.Graph.DirectedBackward.ConcatRealEquation (node : Node) (layout : ConcatLayout) (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id : ℕ) : Prop

The real concat equation names the source of each output scalar, independently of boxes.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.concatNodeBoxes?_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {nodes : Array Node} {boxes : Array (Option (FlatBox α))} {node : Node} {axis id : ℕ} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {box : FlatBox α} (heq : ∀ (layout : ConcatLayout), concatNodeLayout? nodes node axis = some layout → ConcatRealEquation node layout dims v id) (hparents : ∀ p ∈ node.parents, ∀ (B : FlatBox α), boxes[p]?.join = some B → RowEncloses B (dims p) (v p)) (hbox : concatNodeBoxes? nodes boxes node axis = some box) : RowEncloses box (dims id) (v id)

Node concat soundness uses the checked layout and the existing occurrence-wise array lemma.