Directed LayerNorm arithmetic

LayerNorm's variance stage squares a centered interval. An interval crossing zero has lower square bound zero; otherwise the smaller endpoint square is a lower bound. The upper bound is the larger endpoint square. The endpoint products must be rounded in the corresponding direction before either selection.

These facts use the existing real interpretation of directed arithmetic. They compare the computed endpoints with exact real operations, without assuming that ordinary backend addition or multiplication is exact.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.value_min2 {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (a b : α) : LawfulBoundOps.toReal (BoundOps.min2 a b) = min (LawfulBoundOps.toReal a) (LawfulBoundOps.toReal b)

Endpoint minimum selects the smaller interpreted real value.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.value_max2 {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (a b : α) : LawfulBoundOps.toReal (BoundOps.max2 a b) = max (LawfulBoundOps.toReal a) (LawfulBoundOps.toReal b)

Endpoint maximum selects the larger interpreted real value.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.square_le_max {lo x hi : ℝ} (hlo : lo ≤ x) (hhi : x ≤ hi) : x * x ≤ max (lo * lo) (hi * hi)

A scalar square lies below the larger square of any enclosing interval's endpoints.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.square_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (hzero : LawfulBoundOps.toReal 0 = 0) {lo hi : α} {x : ℝ} (hlo : LawfulBoundOps.toReal lo ≤ x) (hhi : x ≤ LawfulBoundOps.toReal hi) : LawfulBoundOps.toReal (if (!decide (0 < lo) && !decide (hi < 0)) = true then 0 else BoundOps.min2 (BoundOps.mulDown lo lo) (BoundOps.mulDown hi hi)) ≤ x * x ∧ x * x ≤ LawfulBoundOps.toReal (BoundOps.max2 (BoundOps.mulUp lo lo) (BoundOps.mulUp hi hi))

The directed square interval used by the LayerNorm variance stage encloses every input square.

The zero interpretation is stated explicitly because the base directed-arithmetic class contains order and operation laws, but does not specify the interpretation of scalar literals.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.scale_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {lo hi scale : α} {x : ℝ} (hlo : LawfulBoundOps.toReal lo ≤ x) (hhi : x ≤ LawfulBoundOps.toReal hi) : LawfulBoundOps.toReal (BoundOps.min2 (BoundOps.mulDown lo scale) (BoundOps.mulDown hi scale)) ≤ x * LawfulBoundOps.toReal scale ∧ x * LawfulBoundOps.toReal scale ≤ LawfulBoundOps.toReal (BoundOps.max2 (BoundOps.mulUp lo scale) (BoundOps.mulUp hi scale))

Multiplication by an exact stored scale respects both endpoint orders, including negative scales. The scale itself is interpreted exactly; only endpoint products are directed.

theorem NN.MLTheory.CROWN.Graph.LayerNormDirected.shift_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {lo hi bias : α} {x : ℝ} (hlo : LawfulBoundOps.toReal lo ≤ x) (hhi : x ≤ LawfulBoundOps.toReal hi) : LawfulBoundOps.toReal (BoundOps.addDown lo bias) ≤ x + LawfulBoundOps.toReal bias ∧ x + LawfulBoundOps.toReal bias ≤ LawfulBoundOps.toReal (BoundOps.addUp hi bias)

Directed endpoint addition encloses the affine bias shift.