Rounded Normalization Certificates

This module bounds the shared normalization core in the rounded-real NF model. The proof is rank-generic: reductions such as a row mean or variance are certified separately and then supplied as inputs here. The resulting theorem covers the numerical part shared by LayerNorm, RMSNorm, BatchNorm, GroupNorm, and related affine normalizations.

If the exact stabilized variance is at least η > 0, the square-root stage is controlled by 1 / sqrt η. The division theorem requires square-root error strictly smaller than sqrt η, so the rounded denominator cannot cross zero. This is a conditional mathematical bound, not an executable certificate checker or a native normalization-kernel proof.

References:

• J. L. Ba, J. R. Kiros, G. E. Hinton, Layer Normalization (2016), https://arxiv.org/abs/1607.06450.
• B. Zhang, R. Sennrich, Root Mean Square Layer Normalization (2019), https://arxiv.org/abs/1910.07467.
• N. J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed. (2002), Chapters 2-3.

structure Proofs.RuntimeApprox.NFBackend.NormalizationErrorTrace : Type

Stage-by-stage infinity-norm budget for an affine normalization.

Records the errors from centering, variance stabilization, square root, division, and affine scaling. Its real-valued fields are mathematical quantities, not an executable report.

• centeredError : ℝ
• stabilizedError : ℝ
• stdError : ℝ
• normalizedError : ℝ
• scaledError : ℝ
• outputError : ℝ

noncomputable def Proofs.RuntimeApprox.NFBackend.normalizeCoreErrorTrace {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s sMean sVar sGamma sBeta : Spec.Shape} (cbMean : sMean.CanBroadcastTo s) (cbVar : sVar.CanBroadcastTo s) (cbGamma : sGamma.CanBroadcastTo s) (cbBeta : sBeta.CanBroadcastTo s) (epsilonR : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) (xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (meanR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) sMean) (varianceR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) sVar) (gammaR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) sGamma) (betaR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) sBeta) (epsX epsMean epsVariance epsGamma epsBeta epsEpsilon η : ℝ) : NormalizationErrorTrace

Compositional error trace for Spec.normalizeCore in the rounded-real model.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_normalizeCore {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s sMean sVar sGamma sBeta : Spec.Shape} (cbMean : sMean.CanBroadcastTo s) (cbVar : sVar.CanBroadcastTo s) (cbGamma : sGamma.CanBroadcastTo s) (cbBeta : sBeta.CanBroadcastTo s) (epsilonS : ℝ) (epsilonR : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) {xS : Spec.SpecTensor s} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {meanS : Spec.SpecTensor sMean} {meanR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) sMean} {varianceS : Spec.SpecTensor sVar} {varianceR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) sVar} {gammaS : Spec.SpecTensor sGamma} {gammaR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) sGamma} {betaS : Spec.SpecTensor sBeta} {betaR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) sBeta} {epsX epsMean epsVariance epsGamma epsBeta epsEpsilon η : ℝ} (hη : 0 < η) (hx : approxTensor toSpec xS xR epsX) (hmean : approxTensor toSpec meanS meanR epsMean) (hvariance : approxTensor toSpec varianceS varianceR epsVariance) (hgamma : approxTensor toSpec gammaS gammaR epsGamma) (hbeta : approxTensor toSpec betaS betaR epsBeta) (hepsilon : |toSpec epsilonR - epsilonS| ≤ epsEpsilon) (hstabilized : TorchLean.Tensor.Forall (fun (z : ℝ) => η ≤ z) ((TorchLean.Tensor.broadcastTo cbVar varianceS).addSpec (TorchLean.Tensor.full s epsilonS))) : have trace := normalizeCoreErrorTrace cbMean cbVar cbGamma cbBeta epsilonR xR meanR varianceR gammaR betaR epsX epsMean epsVariance epsGamma epsBeta epsEpsilon η; trace.stabilizedError < η → trace.stdError < √η → approxTensor toSpec (Spec.normalizeCore s sMean sVar sGamma sBeta epsilonS xS meanS varianceS gammaS betaS cbMean cbVar cbGamma cbBeta) (Spec.normalizeCore s sMean sVar sGamma sBeta epsilonR xR meanR varianceR gammaR betaR cbMean cbVar cbGamma cbBeta) trace.outputError

The rounded-real affine-normalization core approximates its exact real semantics.

The five input tensor hypotheses can themselves come from reductions or earlier graph nodes. The epsilon scalar is treated like any other rounded constant. The exact stabilized variance must have the pointwise lower bound η. The theorem retains two strict error-margin premises; its proof uses the square-root margin for division, but does not use the stabilized-variance error margin because sqrtSpec clamps its input. Both are propositions about the noncomputable error trace.