The reverse sweep and its boundary conditions

The loop visits every graph position exactly once in reverse order. Failure is absorbing. The frontier starts at the output objective and ends at the designated input affine form.

@[simp]

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.addParents_size {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (parents : Array (ℕ × FlatBox α)) (st : Internal.DirectedBackwardState α) : (Array.foldl (fun (state : Internal.DirectedBackwardState α) (entry : ℕ × FlatBox α) => Internal.addDirectedCoeff state entry.1 entry.2) st parents).coeffs.size = st.coeffs.size

Folding coefficient contributions preserves the size of the graph table.

@[simp]

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.backwardNode_size {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (nodes : Array Node) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (ctx : AffineCtx) (st : Internal.DirectedBackwardState α) (id : ℕ) : (Internal.directedBackwardNode nodes ps ibp ctx st id).coeffs.size = st.coeffs.size

A backward node preserves the graph table size on every execution path.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.backwardNode_failed {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (nodes : Array Node) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (ctx : AffineCtx) (st : Internal.DirectedBackwardState α) (id : ℕ) (h : st.failed = true) : (Internal.directedBackwardNode nodes ps ibp ctx st id).failed = true

Once a directed sweep fails, later graph nodes leave it failed.

def NN.MLTheory.CROWN.Graph.DirectedBackward.SweepInvariant {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (input size k : ℕ) (z : ℝ) (st : Internal.DirectedBackwardState α) : Prop

The sweep either has failed or encloses an exact pending objective in a table of fixed size.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.reverseSweep_preserves {β : Type} (step : β → ℕ → β) (P : ℕ → β → Prop) (size : ℕ) (hstep : ∀ k < size, ∀ (st : β), P (k + 1) st → P k (step st k)) (n : ℕ) : n ≤ size → ∀ (st : β), P n st → P 0 (List.foldl (fun (state : β) (i : Fin n) => step state ↑i) st (List.finRange n).reverse)

An invariant preserved at each position is preserved by the engine's reverse finRange fold.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.initial_represents {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (input size output : ℕ) (houtput : output < size) (obj : FlatTensor α) (hdim : obj.n = dims output) : SweepInvariant dims v input size size (dot (dims output) (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) (v output)) { coeffs := (Array.replicate size none).set! output (some (FlatBox.ofTensor obj.v)), cstLo := 0, cstHi := 0 }

A single output row represents exactly the requested output objective.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.inputAffines_row_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} {xB aB : FlatBox α} {x a : ℕ → ℝ} {c : ℝ} {lo hi : α} (hx : RowEncloses xB n x) (ha : RowEncloses aB n a) (hc : LawfulBoundOps.toReal lo ≤ c ∧ c ≤ LawfulBoundOps.toReal hi) {lower upper : AffineVec α n 1} (hresult : Internal.directedInputAffines n xB aB lo hi = some (lower, upper)) : (affineValue lower fun (i : Fin n) => x ↑i) ≤ dot n a x + c ∧ dot n a x + c ≤ affineValue upper fun (i : Fin n) => x ↑i

The dimension-checked affine conversion encloses an arbitrary enclosed input objective.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.inputRow_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {st : Internal.DirectedBackwardState α} {f : ℕ → ℕ → ℝ} {c : ℝ} (h : StateEncloses dims st f c) (input n : ℕ) (hinput : input < st.coeffs.size) (hdim : dims input = n) : RowEncloses (st.coeffs[input]!.getD { dim := n, lo := TorchLean.Tensor.full (Spec.Shape.dim n Spec.Shape.scalar) 0, hi := TorchLean.Tensor.full (Spec.Shape.dim n Spec.Shape.scalar) 0 }) n (f input)

The default zero input row encloses any coefficient represented by an absent array entry.