Rounded forward normalization steps

The node equations below describe the real tensor specifications. Stored affine parameters, running statistics, and epsilon are interpreted through LawfulBoundOps.toReal. The step theorem then proves enclosure by the actual executable transfer, using the usual parent agreement and parent enclosure hypotheses.

def NN.MLTheory.CROWN.Graph.DirectedBackward.ibpNormalizationSupportedKind : OpKind → Bool

The four normalization operations covered by this forward-step theorem.

def NN.MLTheory.CROWN.Graph.DirectedBackward.NormalizationNodeEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (nodes : Array Node) (ps : ParamStore α) (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id : ℕ) : Prop

Real tensor equations for the normalization family, independently of any interval transfer. The successful shape and payload resolutions name the same mathematical operations as IR evaluation. No equation mentions a returned box or assumes an enclosure.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpStepNodeAt?_normalization_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] (hepsilon : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon) {nodes : Array Node} {ps : ParamStore α} {boxes ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id : ℕ} (hfamily : ibpNormalizationSupportedKind nodes[id]!.kind = true) (heq : NormalizationNodeEquation nodes ps dims v id) (hagree : ∀ p ∈ nodes[id]!.parents, boxes[p]?.join = ibp[p]!) (henc : ∀ p ∈ nodes[id]!.parents, ∀ (box : FlatBox α), ibp[p]! = some box → RowEncloses box (dims p) (v p)) {box : FlatBox α} (hstep : ibpStepNodeAt? nodes ps boxes id nodes[id]! = some box) : RowEncloses box (dims id) (v id)

Successful normalization branches enclose their real node equations under the same parent agreement and parent enclosure interface as the generic forward-step theorem.