Provedalphabaguettealgorithm-ideab6

For x ≤ 0, |silu(x)| = |x·σ(x)| ≤ −x·eˣ

For all $\htmlData{mx=1}{x \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=0}{x} \mathrel{\htmlData{mx=1}{\leq}} 0$ , then

\htmlData{mx=7}{\left\lvert \htmlData{mx=6}{\htmlData{mx=0}{x} \cdot \htmlData{mx=5}{(\htmlData{mx=4}{1 + \htmlData{mx=3}{e^{\htmlData{mx=2}{-\htmlData{mx=1}{x}}}}})^{-1}}} \right\rvert} \mathrel{\htmlData{mx=13}{\leq}} \htmlData{mx=12}{\htmlData{mx=9}{-\htmlData{mx=8}{x}} \cdot \htmlData{mx=11}{e^{\htmlData{mx=10}{x}}}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: x is less than or equal to 0. (x ≤ 0)
|x|Absolute value: The size of x · (1 + exp(−x))⁻¹ without its sign. (|x * (1 + Real.exp (-x))⁻¹|)
·Multiplication: x times (1 + exp(−x))⁻¹. (x * (1 + Real.exp (-x))⁻¹)
x⁻¹Inverse: The inverse of 1 + exp(−x): what undoes it (1/x for numbers). ((1 + Real.exp (-x))⁻¹)
+Addition: 1 plus exp(−x). (1 + Real.exp (-x))
eˣExponential function: e raised to the power −x, where e ≈ 2.718. (Real.exp (-x))
−xNegation: The negative of x. (-x)

theorem silu-negative-tail-bound (x : ℝ) (hx : x ≤ 0) :
    |x * (1 + Real.exp (-x))⁻¹| ≤ -x * Real.exp x

Idea B6 (gate-first SwiGLU with certified unit skipping). Baguette's gate is silu(x) = x·(1 + e^{−x})⁻¹. For non-positive gate values its magnitude is bounded by −x·eˣ, which is tiny for strongly negative gates; this bounds a hidden unit's contribution before computing its up/down work.

How it was proved

Proved: 3 October 2026
By: Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
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: 18 lines of Lean

For x ≤ 0, |silu(x)| = |x·σ(x)| ≤ −x·eˣ

How it was proved

More proved statements