Provedaitherdspexact-realb846d70

Aither: exact-real one-pole smoothing preserves intervals and reconstructs input

For all $\htmlData{mx=1}{a, \mathit{input}, \mathit{previous}, \mathit{lo}, \mathit{hi} \in \htmlData{mx=0}{\mathbb{R}}}$ :

\begin{aligned} & \left(\right. 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{a} \\ & \htmlData{mx=1}{\implies} \htmlData{mx=4}{a} \mathrel{\htmlData{mx=5}{\leq}} 1 \\ & \htmlData{mx=1}{\implies} \htmlData{mx=6}{\mathit{lo}} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{\mathit{input}} \\ & \htmlData{mx=1}{\implies} \htmlData{mx=9}{\mathit{input}} \mathrel{\htmlData{mx=11}{\leq}} \htmlData{mx=10}{\mathit{hi}} \\ & \htmlData{mx=1}{\implies} \htmlData{mx=12}{\mathit{lo}} \mathrel{\htmlData{mx=14}{\leq}} \htmlData{mx=13}{\mathit{previous}} \\ & \htmlData{mx=1}{\implies} \htmlData{mx=15}{\mathit{previous}} \mathrel{\htmlData{mx=17}{\leq}} \htmlData{mx=16}{\mathit{hi}} \\ & \htmlData{mx=1}{\implies} \htmlData{mx=19}{\mathit{lo}} \mathrel{\htmlData{mx=25}{\leq}} \htmlData{mx=24}{\htmlData{mx=20}{\operatorname{smooth}}(\htmlData{mx=21}{a}, \htmlData{mx=22}{\mathit{input}}, \htmlData{mx=23}{\mathit{previous}})} \\ & \htmlData{mx=18}{\land} \htmlData{mx=30}{\htmlData{mx=26}{\operatorname{smooth}}(\htmlData{mx=27}{a}, \htmlData{mx=28}{\mathit{input}}, \htmlData{mx=29}{\mathit{previous}})} \mathrel{\htmlData{mx=32}{\leq}} \htmlData{mx=31}{\mathit{hi}} \left.\right) \\ & \htmlData{mx=0}{\land} \htmlData{mx=40}{\htmlData{mx=38}{\htmlData{mx=34}{\operatorname{smooth}}(\htmlData{mx=35}{a}, \htmlData{mx=36}{\mathit{input}}, \htmlData{mx=37}{\mathit{previous}})} - \htmlData{mx=39}{\mathit{input}}} \\ & \quad \htmlData{mx=33}{=} \htmlData{mx=46}{(\htmlData{mx=42}{1 - \htmlData{mx=41}{a}}) \cdot (\htmlData{mx=45}{\htmlData{mx=43}{\mathit{previous}} - \htmlData{mx=44}{\mathit{input}}})} \\ & \htmlData{mx=0}{\land} \htmlData{mx=60}{\htmlData{mx=52}{\htmlData{mx=48}{\operatorname{smooth}}(\htmlData{mx=49}{a}, \htmlData{mx=50}{\mathit{input}}, \htmlData{mx=51}{\mathit{previous}})} + (\htmlData{mx=59}{\htmlData{mx=53}{\mathit{input}} - \htmlData{mx=58}{\htmlData{mx=54}{\operatorname{smooth}}(\htmlData{mx=55}{a}, \htmlData{mx=56}{\mathit{input}}, \htmlData{mx=57}{\mathit{previous}})}})} \\ & \quad \htmlData{mx=47}{=} \htmlData{mx=61}{\mathit{input}} \end{aligned}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: a, input, previous, lo, hi range over real numbers: the statement must hold for every choice. ((a input previous lo hi : ℝ))
≤At most: 0 is less than or equal to a. (0 ≤ a)
⟹Implies: If previous ≤ hi, then lo ≤ smooth(a, input, previous) ∧ smooth(a, input, previou…. (Between types, A → B is the type of functions from A to B.) (previous ≤ hi → lo ≤ smooth a input pre…)
∧And: Both hold: lo ≤ smooth(a, input, previous), and smooth(a, input, previous) ≤ hi. (lo ≤ smooth a input previous ∧ smooth a…)
smooth: smooth: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (smooth)
f(x)Function application: smooth applied to a, input, previous. Lean writes f x; papers write f(x). (smooth a input previous)
-Subtraction: smooth(a, input, previous) minus input. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (smooth a input previous - input)
=Equality: smooth(a, input, previous) − input and (1 − a) · (previous − input) are the same. (smooth a input previous - input = (1 - …)
·Multiplication: 1 − a times previous − input. ((1 - a) * (previous - input))
+Addition: smooth(a, input, previous) plus input − smooth(a, input, previous). (smooth a input previous + (input - smoo…)

theorem aither-b846-one-pole-bounds (a input previous lo hi : ℝ) :
    (0 ≤ a → a ≤ 1 → lo ≤ input → input ≤ hi → lo ≤ previous → previous ≤ hi → lo ≤ smooth a input previous ∧ smooth a input previous ≤ hi) ∧ smooth a input previous - input = (1 - a) * (previous - input) ∧ smooth a input previous + (input - smooth a input previous) = input

For coefficient 0 <= a <= 1, a smoothing step preserves any interval containing the input and previous state. Also proves the exact error recurrence and low-plus-complement reconstruction. Models nLp1/nHp1/nSlew algebra over real numbers; coefficient conversion, Float64 rounding and transients from exceptional values are excluded.

How it was proved

Proved: 1 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: 23 lines of Lean

Aither: exact-real one-pole smoothing preserves intervals and reconstructs input

How it was proved

More proved statements