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 {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (epsElem : ℝ) : TorchLean.Floats.NF β fexp rnd × ℝ → TorchLean.Floats.NF β fexp rnd → TorchLean.Floats.NF β fexp rnd × ℝ

One fold step for sum_spec 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 {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (epsElem : ℝ) (st : TorchLean.Floats.NF β fexp rnd × ℝ) (tR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s) : TorchLean.Floats.NF β fexp rnd × ℝ

Fold sum_step over a tensor via tensor_foldl_spec.

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

noncomputable def Proofs.RuntimeApprox.NFBackend.sumBound {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (epsElem : ℝ) (tR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s) : ℝ

Forward absolute-error bound for sum_spec.

sum_bound epsElem tR is the .2 component of sum_fold_state 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.approxT_sum_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} : approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.scalar (Spec.Tensor.sumSpec xS)) (Spec.Tensor.scalar xR.sumSpec) (sumBound eps xR)

Forward approximation bound for sum_spec 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.