Rounded LayerNorm transfers

The checked matrix view normalizes the complete suffix beginning at the requested axis. Stored gamma, beta, and epsilon are interpreted as real scalars before applying the real specification. Both the directed row path and the uniform default-parameter path are covered.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.layerNormMatrixDims_properties {s : Spec.Shape} {axis rows width : ℕ} (h : (IR.OpContracts.layerNormMatrixDims axis s).toOption = some (rows, width)) : 0 < width ∧ width = (List.drop axis s.toList).prod ∧ s.size = Spec.Shape.size [rows, width]

A successful matrix-layout check has positive width and preserves the element count.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.layerNorm_normalized_abs_le_sqrt {m n : ℕ} (hn : 0 < n) (x : TorchLean.Tensor ℝ [m, n]) (epsilon : ℝ) (hepsilon : 0 ≤ epsilon) (i : Fin m) (j : Fin n) : |(Spec.get2 x i j - Proofs.Autograd.Norm.rowMeanE x i) / √(max (Proofs.Autograd.Norm.rowVarE x i + epsilon) 0)| ≤ √↑n

Dividing a centered row entry by its stabilized standard deviation bounds its magnitude by the square root of the row width. Zero denominators follow Lean's real division convention.

def NN.MLTheory.CROWN.Graph.DirectedBackward.normalizationAffine? {α : Type} [TorchLean.Storage α] [Context α] (s : Spec.Shape) (axis width : ℕ) (parameters : Option (IR.LayerNormParams α)) : Option (IR.Graph.LayerNormAffine α width)

Resolve the optional stored payload using the same suffix validation as IR evaluation.

def NN.MLTheory.CROWN.Graph.DirectedBackward.defaultNormalizationAffine {α : Type} [TorchLean.Storage α] [Context α] (width : ℕ) : IR.Graph.LayerNormAffine α width

The unit scale, zero bias, and stored-format default epsilon used by IR evaluation.

def NN.MLTheory.CROWN.Graph.DirectedBackward.defaultLayerNormParams {α : Type} [TorchLean.Storage α] [Context α] (s : Spec.Shape) (axis : ℕ) : IR.LayerNormParams α

The payload synthesized by the executable default-parameter fallback.

@[simp]

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.normalizationAffine?_none {α : Type} [TorchLean.Storage α] [Context α] (s : Spec.Shape) (axis width : ℕ) : normalizationAffine? s axis width none = some (defaultNormalizationAffine width)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.normalizationAffine?_defaultLayerNormParams {α : Type} [TorchLean.Storage α] [Context α] (s : Spec.Shape) (axis width : ℕ) (hwidth : width = (List.drop axis s.toList).prod) : normalizationAffine? s axis width (some (defaultLayerNormParams s axis)) = some (defaultNormalizationAffine width)

Resolving the synthesized default payload gives exactly the absent-payload affine data.

noncomputable def NN.MLTheory.CROWN.Graph.DirectedBackward.layerNormRealValue {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (rows width : ℕ) (f : ℕ → ℝ) (affine : IR.Graph.LayerNormAffine α width) (hwidth : 0 < width) : TorchLean.Tensor ℝ [rows, width]

The actual real matrix LayerNorm, with every affine parameter and epsilon interpreted from its stored scalar. Empty leading batches retain the IR's empty-tensor convention.

def NN.MLTheory.CROWN.Graph.DirectedBackward.LayerNormRealEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (s : Spec.Shape) (axis : ℕ) (parameters : Option (IR.LayerNormParams α)) (f g : ℕ → ℝ) : Prop

Coordinate equation for suffix LayerNorm. Its premises are successful layout and payload resolution, independently of any interval box or interval transfer.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.LayerNormRealEquation.defaultPayload {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {axis : ℕ} {f g : ℕ → ℝ} (heq : LayerNormRealEquation s axis none f g) : LayerNormRealEquation s axis (some (defaultLayerNormParams s axis)) f g

The real coordinate equation is unchanged by materializing the default affine payload.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.layerNormRealValue_default_abs_le {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {rows width : ℕ} (hwidth : 0 < width) (f : ℕ → ℝ) (hepsilon : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon) (i : Fin rows) (j : Fin width) : |Spec.get2 (layerNormRealValue rows width f (defaultNormalizationAffine width) hwidth) i j| ≤ √↑width

The default matrix specification has the uniform square-root width bound.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.layerNormRealValue_default_singleton {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {rows : ℕ} (f : ℕ → ℝ) (i : Fin rows) (j : Fin 1) : Spec.get2 (layerNormRealValue rows 1 f (defaultNormalizationAffine 1) layerNormRealValue_default_singleton._proof_2) i j = 0

Default LayerNorm on a singleton suffix is exactly zero, even if epsilon rounds to zero.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpLayerNormPayloadBox?_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] {s : Spec.Shape} {axis : ℕ} {parameters : IR.LayerNormParams α} {input output : FlatBox α} {f g : ℕ → ℝ} (hx : RowEncloses input s.size f) (heq : LayerNormRealEquation s axis (some parameters) f g) (hout : ibpLayerNormPayloadBox? s axis parameters input = some output) : RowEncloses output s.size g

A successful stored-parameter transfer encloses the IR matrix specification, including its resolved scale, bias, and epsilon, for every accepted normalized suffix.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpLayerNormRange?_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] (hepsilon : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon) {s : Spec.Shape} {axis rows width : ℕ} {output : FlatBox α} {f g : ℕ → ℝ} (hlayout : (IR.OpContracts.layerNormMatrixDims axis s).toOption = some (rows, width)) (heq : LayerNormRealEquation s axis none f g) (hout : ibpLayerNormRange? s s.size axis = some output) : RowEncloses output s.size g

The backend's uniform default-parameter box encloses the actual real normalization. The lower radius is rounded downward; nonnegativity of the stored default epsilon is the only additional scalar fact.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpLayerNormBox?_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] (hepsilon : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon) {s : Spec.Shape} {axis : ℕ} {input output : FlatBox α} {f g : ℕ → ℝ} (hx : RowEncloses input s.size f) (heq : LayerNormRealEquation s axis none f g) (hout : ibpLayerNormBox? s input axis = some output) : RowEncloses output s.size g

Both successful default-parameter execution paths enclose the actual real LayerNorm.