NF Sum Reduction Bounds

Forward-error bounds for rounded sum reductions. The accumulator carries both the runtime value and a proof budget, so every addition contributes the incoming element error plus one rounding term.

noncomputable def Proofs.RuntimeApprox.NFBackend.sumStep {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (epsElem : ℝ) : FloatLib.Floats.Formats.Flocq.NF β fexp rnd × ℝ → FloatLib.Floats.Formats.Flocq.NF β fexp rnd → FloatLib.Floats.Formats.Flocq.NF β fexp rnd × ℝ

One fold step for sumSpec that tracks an explicit forward error budget.

State is (accR, epsAcc) where accR is the runtime accumulator and epsAcc bounds the absolute error |toSpec accR - accS| for the corresponding spec accumulator accS. Each step adds:

• the incoming per-element budget epsElem;
• one rounding-ULP term for the addition.

noncomputable def Proofs.RuntimeApprox.NFBackend.sumFoldState {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (epsElem : ℝ) (st : FloatLib.Floats.Formats.Flocq.NF β fexp rnd × ℝ) (tR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) : FloatLib.Floats.Formats.Flocq.NF β fexp rnd × ℝ

Fold sumStep over a tensor via foldlSpec.

This is the shared helper behind sumBound and approxTensor_sum_spec: it simultaneously computes the runtime sum (in .1) and the accumulated error bound (in .2).

noncomputable def Proofs.RuntimeApprox.NFBackend.sumBound {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (epsElem : ℝ) (tR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) : ℝ

Forward absolute-error bound for sumSpec.

sum_bound epsElem tR is the .2 component of sumFoldState started at 0, assuming each element is approximated within epsElem. This corresponds to naive sequential summation with a rounding term added at each step (cf. standard floating-point summation analyses).

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_sum_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {eps : ℝ} : approxTensor toSpec xS xR eps → approxTensor toSpec (TorchLean.Tensor.scalar (TorchLean.Tensor.sumSpec xS)) (TorchLean.Tensor.scalar xR.sumSpec) (sumBound eps xR)

Forward approximation bound for sumSpec over an arbitrary tensor shape.

If xR approximates xS elementwise within eps, then the scalar sums sum_spec xR and sum_spec xS differ by at most sum_bound eps xR.