Enclosure by the directed LayerNorm sequence

The successful executable row transfer encloses the corresponding row of Spec.layerNorm. The proof follows its directed sum and count folds, both centering stages, variance, square root, division, and stored affine parameters. It uses the scalar operation contracts and the existing entrywise formula for the real specification.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.checkedFiniteBounds?_eq_of_eq_some {α : Type} [Context α] {input output : α × α} (h : checkedFiniteBounds? input = some output) : input = output

A successful finite-bounds check returns its input endpoints unchanged.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.checkedFiniteBounds?_bind_eq_some {α : Type} [Context α] {action : Option (α × α)} {output : α × α} (h : action >>= checkedFiniteBounds? = some output) : action = some output

Validation after a scalar transfer preserves the successful transfer result.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.sum_count_fold_encloses {α : Type} [Context α] [TorchLean.Storage α] [BoundOps α] [LawfulBoundOps α] {ι : Type} (bounds : ι → α × α) (f : ι → ℝ) (hb : ∀ (i : ι), LawfulBoundOps.toReal (bounds i).1 ≤ f i ∧ f i ≤ LawfulBoundOps.toReal (bounds i).2) (indices : List ι) (acc : α × α × α × α) (sum count : ℝ) (hacc : LawfulBoundOps.toReal acc.1 ≤ sum ∧ sum ≤ LawfulBoundOps.toReal acc.2.1 ∧ LawfulBoundOps.toReal acc.2.2.1 ≤ count ∧ count ≤ LawfulBoundOps.toReal acc.2.2.2) : have result := List.foldl (fun (x : α × α × α × α) (i : ι) => match x with | (lo, hi, countLo, countHi) => (BoundOps.addDown lo (bounds i).1, BoundOps.addUp hi (bounds i).2, BoundOps.addDown countLo 1, BoundOps.addUp countHi 1)) acc indices; LawfulBoundOps.toReal result.1 ≤ List.foldl (fun (s : ℝ) (i : ι) => s + f i) sum indices ∧ List.foldl (fun (s : ℝ) (i : ι) => s + f i) sum indices ≤ LawfulBoundOps.toReal result.2.1 ∧ LawfulBoundOps.toReal result.2.2.1 ≤ List.foldl (fun (c : ℝ) (x : ι) => c + 1) count indices ∧ List.foldl (fun (c : ℝ) (x : ι) => c + 1) count indices ≤ LawfulBoundOps.toReal result.2.2.2

The executable four-accumulator fold encloses both the sum and the exact count.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.directedRowMean?_encloses {α : Type} [Context α] [TorchLean.Storage α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] {n : ℕ} (hn : 0 < n) (bounds : Fin n → α × α) (f : Fin n → ℝ) (hb : ∀ (i : Fin n), LawfulBoundOps.toReal (bounds i).1 ≤ f i ∧ f i ≤ LawfulBoundOps.toReal (bounds i).2) {outLo outHi : α} (hout : directedRowMean? bounds = some (outLo, outHi)) : LawfulBoundOps.toReal outLo ≤ (∑ i : Fin n, f i) / ↑n ∧ (∑ i : Fin n, f i) / ↑n ≤ LawfulBoundOps.toReal outHi

The denominator is the exact natural count, enclosed by the directed fold of ones.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.sub_encloses {α : Type} [Context α] [TorchLean.Storage α] [BoundOps α] [LawfulBoundOps α] {aLo aHi bLo bHi : α} {a b : ℝ} (ha : LawfulBoundOps.toReal aLo ≤ a ∧ a ≤ LawfulBoundOps.toReal aHi) (hb : LawfulBoundOps.toReal bLo ≤ b ∧ b ≤ LawfulBoundOps.toReal bHi) : LawfulBoundOps.toReal (BoundOps.subDown aLo bHi) ≤ a - b ∧ a - b ≤ LawfulBoundOps.toReal (BoundOps.subUp aHi bLo)

Subtracting two enclosing intervals uses opposite endpoints for the subtrahend.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.max_zero_encloses {α : Type} [Context α] [TorchLean.Storage α] [BoundOps α] [LawfulBoundOps α] {lo hi : α} {x : ℝ} (h : LawfulBoundOps.toReal lo ≤ x ∧ x ≤ LawfulBoundOps.toReal hi) : LawfulBoundOps.toReal (BoundOps.max2 lo 0) ≤ max x 0 ∧ max x 0 ≤ LawfulBoundOps.toReal (BoundOps.max2 hi 0)

Clamping both endpoints at zero encloses the clamped real value.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.directedLayerNormRow?_encloses {α : Type} [Context α] [TorchLean.Storage α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (lo hi gamma beta : TorchLean.Tensor α [n]) (epsilon : α) (x : TorchLean.Tensor ℝ [m, n]) (row : Fin m) (hx : ∀ (j : Fin n), LawfulBoundOps.toReal (lo.getScalar j) ≤ Spec.get2 x row j ∧ Spec.get2 x row j ≤ LawfulBoundOps.toReal (hi.getScalar j)) {outLo outHi : TorchLean.Tensor α [n]} (hout : directedLayerNormRow? lo hi gamma beta epsilon = some (outLo, outHi)) (j : Fin n) : have y := Spec.get2 (Spec.layerNorm x (TorchLean.Tensor.ofFn fun (k : Fin n) => LawfulBoundOps.toReal (gamma.getScalar k)) (TorchLean.Tensor.ofFn fun (k : Fin n) => LawfulBoundOps.toReal (beta.getScalar k)) hm hn (LawfulBoundOps.toReal epsilon)) row j; LawfulBoundOps.toReal (outLo.getScalar j) ≤ y ∧ y ≤ LawfulBoundOps.toReal (outHi.getScalar j)

Every successful directed row transfer encloses its row of the real LayerNorm specification.

The LawfulBoundOps laws supply the exact interpretation of zero and one. Gamma, beta, and epsilon are interpreted stored values. The statement assumes only the input enclosure and the existing scalar operation laws.