Structural real semantics and the backward interface

The checked backward concat layout preserves the forward layout. Transpose and permutation use the coordinate bijection of the exact tensor evaluator. These facts derive the legacy backward equations from the actual real semantics, without a second semantic assumption.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.concatBackwardLayout?_forward {α : Type} [TorchLean.Storage α] [Context α] {nodes : Array Node} {ibp : Array (Option (FlatBox α))} {node : Node} {axis : ℕ} {layout : ConcatLayout} (h : Internal.concatBackwardLayout? nodes ibp node axis = some layout) : concatNodeLayout? nodes node axis = some layout ∧ node.parents.size = layout.lengths.length

A successful backward concat check preserves the forward layout and occurrence count.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.permutationEquation_of_eval {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id p : ℕ} {s t : Spec.Shape} {forward : Array ℕ} (hdp : dims p = s.size) (hd : dims id = t.size) (heval : IR.Graph.permuteSomeTensor { shape := s, tensor := realTensor s (v p) } forward = Except.ok { shape := t, tensor := realTensor t (v id) }) : PermutationEquation dims v id p t forward

A successful exact permutation of the real parent tensor yields the backward flat-index permutation equation.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.StructuralRealNodeEquation.concat_nodeEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {nodes : Array Node} {ps : ParamStore α} {ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id axis : ℕ} (h : StructuralRealNodeEquation nodes dims v id) (hkind : nodes[id]!.kind = IR.OpKind.concat axis) : NodeEquation nodes ps ibp dims v id

The exact forward concat equation supplies the backward concat node equation.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.StructuralRealNodeEquation.permute_nodeEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {nodes : Array Node} {ps : ParamStore α} {ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id : ℕ} {forward : Array ℕ} (h : StructuralRealNodeEquation nodes dims v id) (hkind : nodes[id]!.kind = IR.OpKind.permute forward) (hparents : ∀ p ∈ nodes[id]!.parents, p < nodes.size) : NodeEquation nodes ps ibp dims v id

Exact real permutation semantics supplies the backward permutation equation.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.StructuralRealNodeEquation.transpose_nodeEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {nodes : Array Node} {ps : ParamStore α} {ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id a b : ℕ} (h : StructuralRealNodeEquation nodes dims v id) (hkind : nodes[id]!.kind = IR.OpKind.transpose a b) (hparents : ∀ p ∈ nodes[id]!.parents, p < nodes.size) : NodeEquation nodes ps ibp dims v id

Exact real transpose semantics uses the same checked axis permutation as the backward pass.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.StructuralRealNodeEquation.nodeEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {nodes : Array Node} {ps : ParamStore α} {ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id : ℕ} (hsupported : ibpStructuralSupportedNode nodes[id]! = true) (heq : StructuralRealNodeEquation nodes dims v id) (hparents : ∀ p ∈ nodes[id]!.parents, p < nodes.size) : NodeEquation nodes ps ibp dims v id

One real structural semantics supplies the backward node equations. Valid parent indices are ordinary graph topology evidence; no interval enclosure or redundant value equation is assumed.