Provedalphabaguettebaguette-zrange

The SwiGLU product never exceeds |gate|·|up|

For all $\htmlData{mx=1}{g, u \in \htmlData{mx=0}{\mathbb{R}}}$ :

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

What the notation means · or point at any symbol

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

theorem bz-swiglu-product-bound (g u : ℝ) :
    |g * (1 + Real.exp (-g))⁻¹ * u| ≤ |g| * |u|

|silu(g)·u| = |g·σ(g)·u| ≤ |g|·|u| because 0 < σ ≤ 1. Part of the plan 'Baguette-Z: closed-loop certified integer-state training'.

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: 17 lines of Lean