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. These bounds follow sumSpec's left-to-right tensor traversal, starting at rounded zero. They do not cover a different reduction tree or establish a native kernel's accumulation order.

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.

Assumes each element is approximated within epsElem. The budget starts with a conservative half ULP at zero and adds one rounding term per sequential addition; it is not a tight bound for an empty tensor, whose sum is exactly zero.

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 sumSpec xR and sumSpec xS differ by at most sumBound eps xR.