Provedalphabaguettebaguette-zsoftmax
exp2 of a score splits into an exact integer shift times exp2 of the fraction
For all and :
What the notation means · or point at any symbol
- ZIntegers
- The integers …, −2, −1, 0, 1, 2, …. (
ℤ) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - (x : T)As real numbers
- 2 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(2:ℝ)) - aᵇPower
- 2 raised to the power n + f. (
(2:ℝ) ^ ((n : ℝ) + f)) - =Equality
- 2^(n + f) and 2^n · 2^f are the same. (
(2:ℝ) ^ ((n : ℝ) + f) = (2:ℝ) ^ n * (2:…) - +Addition
- n plus f. (
(n : ℝ) + f) - ·Multiplication
- 2^n times 2^f. (
(2:ℝ) ^ n * (2:ℝ) ^ f)
theorem bz-exp2-integer-split (n : ℤ) (f : ℝ) :
(2:ℝ) ^ ((n : ℝ) + f) = (2:ℝ) ^ n * (2:ℝ) ^ f2^(n+f) = 2ⁿ·2^f for integer n. In Baguette-Z, attention weights are an exact exponent shift (n) applied to a bounded mantissa 2^f. 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
- 12 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.