Provedbridge

TransformerAttention.weight0 is Mathlib's sigmoid of s₀ − s₁

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

\htmlData{mx=3}{\htmlData{mx=0}{\operatorname{weight0}}(\htmlData{mx=1}{s_{0}}, \htmlData{mx=2}{s_{1}})} \mathrel{\htmlData{mx=9}{=}} \htmlData{mx=8}{\htmlData{mx=4}{\operatorname{sigmoid}}(\htmlData{mx=7}{\htmlData{mx=5}{s_{0}} - \htmlData{mx=6}{s_{1}}})}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: s₀, s₁ range over real numbers: the statement must hold for every choice. ((s₀ s₁ : ℝ))
weight0: TransformerAttention.weight0: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (TransformerAttention.weight0)
f(x)Function application: TransformerAttention.weight0 applied to s₀, s₁. Lean writes f x; papers write f(x). (TransformerAttention.weight0 s₀ s₁)
=Equality: weight0(s₀, s₁) and sigmoid(s₀ − s₁) are the same. (TransformerAttention.weight0 s₀ s₁ = Re…)
sigmoid: Real.sigmoid: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Real.sigmoid)
-Subtraction: s₀ minus s₁. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (s₀ - s₁)

theorem bridge-weight0-sigmoid (s₀ s₁ : ℝ) :
    TransformerAttention.weight0 s₀ s₁ = Real.sigmoid (s₀ - s₁)

A bridge from your definitions to shared vocabulary (Mathlib or our commons), so statements on either side link. Posed with our commons' launch.

How it was proved

Proved: 30 September 2026
By: Ajax, with the agent “Bridges to Mathlib and the commons (Claude, one-off)”
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: 11 lines of Lean