Reduction-tree error enclosure

A binary tree records the parenthesization of a rounded sum. Under the explicit local RelativeLocalAddBound hypothesis, every such tree satisfies the same leaf-count and absolute-leaf-scale error enclosure. The argument is independent of a floating-point format. We retain the array-facing schedule API and use FloatLib's generic reduction-tree error bound.

Binary32 does not satisfy the usual relative bound globally: gradual underflow needs an absolute-error term. The executable specializations retain the local-bound hypothesis and check finite intermediates. No unconditional unit-roundoff claim is made here.

Generic reduction trees over $\mathbb{R}$

inductive TorchLean.Floats.IEEE754.SumTree (α : Type u) : Type u

A binary reduction schedule.

Leaves contain inputs of type α; internal nodes indicate “evaluate left and right subtrees, then combine”. Different trees represent different valid parenthesizations for a parallel reduction.

• leaf {α : Type u} : α → SumTree α
• node {α : Type u} : SumTree α → SumTree α → SumTree α

def TorchLean.Floats.IEEE754.instReprSumTree.repr {α✝ : Type u_1} [Repr α✝] : SumTree α✝ → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.Floats.IEEE754.instReprSumTree {α✝ : Type u_1} [Repr α✝] : Repr (SumTree α✝)

def TorchLean.Floats.IEEE754.SumTree.leaves {α : Type u} : SumTree α → Array α

The leaves of the reduction tree, read left-to-right.

The numerical collection is an Array. The schedule relation below converts arrays to lists only inside List.Perm, reusing mathlib's established permutation theory without exposing list-backed numerical data in the API.

def TorchLean.Floats.IEEE754.SumTree.leafCount {α : Type u} : SumTree α → ℕ

Number of leaves in the tree (the “reduction length”).

theorem TorchLean.Floats.IEEE754.SumTree.leafCount_pos {α : Type u} (t : SumTree α) : 0 < t.leafCount

A reduction tree always has at least one leaf.

noncomputable def TorchLean.Floats.IEEE754.ReductionBound.growth (u : ℝ) (n : ℕ) : ℝ

Growth factor (1+u)^(n-1) for a reduction with n leaves.

def TorchLean.Floats.IEEE754.evalRound {α : Type u} (roundAdd : ℝ → ℝ → ℝ) (leafVal : α → ℝ) : SumTree α → ℝ

Evaluate a reduction tree using a given “rounded add” at internal nodes.

evalRound roundAdd leafVal t maps leaves via leafVal, and combines subresults using roundAdd. This abstracts the idea of evaluating a parallel sum with a fixed local rounding model.

def TorchLean.Floats.IEEE754.exactSum {α : Type u} (leafVal : α → ℝ) : SumTree α → ℝ

Exact real evaluation of the tree (just + at internal nodes).

def TorchLean.Floats.IEEE754.sumAbs {α : Type u} (leafVal : α → ℝ) : SumTree α → ℝ

Sum of absolute values of leaf contributions.

This is the standard “scale” that appears in forward-error bounds for floating-point reductions.

def TorchLean.Floats.IEEE754.RelativeLocalAddBound (roundAdd : ℝ → ℝ → ℝ) (u : ℝ) : Prop

Relative local rounded-addition assumption for reductions.

This is the usual normal-range unit-roundoff envelope: $$ \operatorname{roundAdd}(a,b)=(a+b)+e, \qquad |e|\le u(|a|+|b|). $$ Binary32 does not satisfy it globally with $u=2^{-24}$: subnormal results require an absolute-error term. Consequently the executable theorems below take this predicate as an explicit hypothesis; it must be established from normal-range intermediate sums or replaced by an absolute/mixed analysis.

theorem TorchLean.Floats.IEEE754.evalRound_enclosure_of_relativeLocalAddBound {α : Type u} (roundAdd : ℝ → ℝ → ℝ) (leafVal : α → ℝ) (u : ℝ) (H : RelativeLocalAddBound roundAdd u) (hu : 0 ≤ u) (t : SumTree α) : |evalRound roundAdd leafVal t - exactSum leafVal t| ≤ (ReductionBound.growth u t.leafCount - 1) * sumAbs leafVal t

Order-independent enclosure for any reduction tree evaluated with roundAdd.

Let $A=\sum_i|\mathtt{leaf}_i|$ be the sum of absolute values of leaves. For $n$ leaves, the rounded evaluation is within $(\operatorname{growth}(u,n)-1)A$ of the exact real sum.