Provedbridge

TransformerAttention.weight1 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{weight1}}(\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_{1}} - \htmlData{mx=6}{s_{0}}})}

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₁ : ℝ))
weight1: TransformerAttention.weight1: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (TransformerAttention.weight1)
f(x)Function application: TransformerAttention.weight1 applied to s₀, s₁. Lean writes f x; papers write f(x). (TransformerAttention.weight1 s₀ s₁)
=Equality: weight1(s₀, s₁) and sigmoid(s₁ − s₀) are the same. (TransformerAttention.weight1 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-weight1-sigmoid (s₀ s₁ : ℝ) :
    TransformerAttention.weight1 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