Rounded Normalization Certificates

This module connects TorchLean's mathematical normalization core to its rounded NF execution. 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.

The conditioning assumptions are explicit. If the exact stabilized variance is at least η > 0, the square-root stage is controlled by 1 / sqrt η. Division is accepted only when the computed square-root error is strictly smaller than sqrt η, so a rounded denominator cannot cross zero.

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.

Keeping the intermediate errors is useful for auditing a failed certificate: a caller can see whether the loss of margin came from centering, variance stabilization, square root, division, or the final affine map instead of receiving only one opaque final number.

• 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

Compute the compositional error trace for Spec.normalizeCore on rounded runtime tensors.

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

Rounded execution of the shared affine-normalization core approximates its 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 two strict margin checks are directly computable from normalizeCoreErrorTrace.