Provedattentionresidual-seriesexternal-review-4

Residual series: bounded scalar output on every capped path

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{h, R : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{\rho, G, d \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\rho}$ , $\htmlData{mx=0}{\rho} \mathrel{\htmlData{mx=1}{<}} 1$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{G}$ , $\htmlData{mx=6}{\forall j,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{h}(\htmlData{mx=1}{j})} \right\rvert} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{\rho}}$ , $\htmlData{mx=9}{\forall j,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{R}(\htmlData{mx=1}{j})} \right\rvert} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{(\htmlData{mx=5}{1 - \htmlData{mx=4}{\rho}}) \cdot \htmlData{mx=6}{G}}}$ and $\htmlData{mx=1}{\left\lvert \htmlData{mx=0}{d} \right\rvert} \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{G}$ , then

\begin{aligned} & \htmlData{mx=0}{\forall} \mathit{xs} : \htmlData{mx=5}{\htmlData{mx=1}{\operatorname{List}}\,\htmlData{mx=4}{\htmlData{mx=2}{J} \times \htmlData{mx=3}{\operatorname{Bool}}}}, \\ & \quad \htmlData{mx=28}{\left\lvert \htmlData{mx=27}{\htmlData{mx=9}{\operatorname{foldr}\left(\htmlData{mx=8}{\mathit{xs}}\right)}\left(\htmlData{mx=25}{z, \mathit{tail} \mapsto \htmlData{mx=24}{\begin{cases} \htmlData{mx=16}{\htmlData{mx=14}{\frac{\htmlData{mx=12}{\htmlData{mx=10}{h}(\htmlData{mx=11}{z_{1}})}}{\htmlData{mx=13}{\rho}}} \cdot \htmlData{mx=15}{\mathit{tail}}} & \text{if } \htmlData{mx=17}{z_{2}} \\ \htmlData{mx=23}{\frac{\htmlData{mx=20}{\htmlData{mx=18}{R}(\htmlData{mx=19}{z_{1}})}}{\htmlData{mx=22}{1 - \htmlData{mx=21}{\rho}}}} & \text{otherwise} \end{cases}}}, \htmlData{mx=26}{d}\right)} \right\rvert} \\ & \quad \quad \htmlData{mx=6}{\leq} \htmlData{mx=29}{G} \end{aligned}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
⟹Implies: If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
x : TVariables: h, R range over J → ℝ: the statement must hold for every choice. ((h R : J → ℝ))
x ∈ TVariables: ρ, G, d range over real numbers: the statement must hold for every choice. ((ρ G d : ℝ))
<Less than: 0 is strictly smaller than ρ. (0 < ρ)
≤At most: 0 is less than or equal to G. (0 ≤ G)
∀For all: The statement after the comma holds for every j. (∀ j, |h j| ≤ ρ)
RReal numbers: The real numbers: every point on the number line. (ℝ)
|x|Absolute value: The size of h(j) without its sign. (|h j|)
f(x)Function application: h applied to j. Lean writes f x; papers write f(x). (h j)
List: List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
·Multiplication: 1 − ρ times G. ((1-ρ)*G)
×Product: Pairs of an element of J and an element of Bool. (J × Bool)
-Subtraction: 1 minus ρ. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1-ρ)
Bool: Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Bool)
e.ffoldr: foldr of xs: Lean's dot notation e.foldr means foldr applied to e. (xs.foldr)
x ↦ f(x)Function (λ-abstraction): The function sending z, tail to h(z.1)/ρ · tail if z.2, else R(z.1)/(1 − ρ). Lean writes fun x => …; papers write x ↦ …. (fun z tail => if z.2 then (h z.1/ρ)*tai…)
{ a if c; b otherwiseCases (if … then … else): h(z.1)/ρ · tail when z.2, and R(z.1)/(1 − ρ) otherwise. (if z.2 then (h z.1/ρ)*tail else R z.1/(…)
a/bDivision: h(z.1) divided by ρ. In Lean, dividing by 0 gives 0. (h z.1/ρ)
p₁Component: The first component of the pair z. (z.1)

theorem residual-series-path-bound {J : Type} (h R : J → ℝ) (ρ G d : ℝ) (hρ : 0 < ρ) (hρ1 : ρ < 1) (hG : 0 ≤ G) (hh : ∀ j, |h j| ≤ ρ) (hR : ∀ j, |R j| ≤ (1-ρ)*G) (hd : |d| ≤ G) :
    ∀ xs : List (J × Bool), |xs.foldr (fun z tail => if z.2 then (h z.1/ρ)*tail else R z.1/(1-ρ)) d| ≤ G

For globally bounded residual factors and terminal/fallback corrections, proves every actual list-fold correction has magnitude at most G. Exact scalar arithmetic; vector convex-hull geometry and floating-point certification remain paper obligations.

How it was proved

Proved: 6 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 21 lines of Lean

Residual series: bounded scalar output on every capped path

How it was proved

More proved statements