The objective remaining at a backward-sweep frontier

Processed rows remain in the executable coefficient array. The invariant sums only unprocessed nodes and the designated input, so those stale rows are never counted twice.

def NN.MLTheory.CROWN.Graph.DirectedBackward.dot (n : ℕ) (a x : ℕ → ℝ) : ℝ

A finite real inner product, indexed by natural-number coordinates.

def NN.MLTheory.CROWN.Graph.DirectedBackward.pending (input k : ℕ) : Finset ℕ

The designated input remains live after its position has passed in the reverse sweep.

def NN.MLTheory.CROWN.Graph.DirectedBackward.frontierValue (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (input k : ℕ) (f : ℕ → ℕ → ℝ) (c : ℝ) : ℝ

The exact objective represented by the rows that have not yet been discharged.

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

The executable state encloses coefficients of one exact remaining objective.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.frontier_add {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {input k pid : ℕ} (hp : pid ∈ pending input k) (f : ℕ → ℕ → ℝ) (a : ℕ → ℝ) (c : ℝ) : frontierValue dims v input k (fun (id i : ℕ) => if id = pid then f id i + a i else f id i) c = frontierValue dims v input k f c + dot (dims pid) a (v pid)

Updating a live parent adds exactly its contribution to the pending objective.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.frontier_succ {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {input k : ℕ} (hk : k ≠ input) (f : ℕ → ℕ → ℝ) (c : ℝ) : frontierValue dims v input (k + 1) f c = frontierValue dims v input k f c + dot (dims k) (f k) (v k)

Dropping a non-input frontier row subtracts precisely that row's objective.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.frontier_input {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} (input : ℕ) (f : ℕ → ℕ → ℝ) (c : ℝ) : frontierValue dims v input (input + 1) f c = frontierValue dims v input input f c

Passing the designated input does not remove its objective from the invariant.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.frontier_zero (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (input : ℕ) (f : ℕ → ℕ → ℝ) (c : ℝ) : frontierValue dims v input 0 f c = dot (dims input) (f input) (v input) + c

The final frontier contains only the designated input and the accumulated constant.

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

Adding an enclosed coefficient contribution preserves the exact objective relation.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.represents_addConstant {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {input k : ℕ} {st : Internal.DirectedBackwardState α} {z : ℝ} (h : Represents dims v input k st z) (lo hi : α) (d : ℝ) (hd : LawfulBoundOps.toReal lo ≤ d ∧ d ≤ LawfulBoundOps.toReal hi) : Represents dims v input k (Internal.addDirectedConstant st lo hi) (z + d)

Adding an enclosed constant changes the represented objective by its exact real value.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.represents_drop_none {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {input k : ℕ} {st : Internal.DirectedBackwardState α} {z : ℝ} (h : Represents dims v input (k + 1) st z) (hk : k ≠ input) (hsize : k < st.coeffs.size) (hnone : st.coeffs[k]! = none) : Represents dims v input k st z

An absent non-input row contributes zero when its position passes the frontier.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.represents_drop_some {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {input k : ℕ} {st : Internal.DirectedBackwardState α} {z : ℝ} (h : Represents dims v input (k + 1) st z) (hk : k ≠ input) (hsize : k < st.coeffs.size) {box : FlatBox α} (hsome : st.coeffs[k]! = some box) : ∃ (a : ℕ → ℝ), RowEncloses box (dims k) a ∧ Represents dims v input k st (z - dot (dims k) a (v k))

A present row supplies the exact coefficient consumed by the next backward step.