Provedalphabaguettebaguette-zsoftmax

For 0 ≤ f < 1, the mantissa 2^f lies in [1, 2)

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

1 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{2}^{\htmlData{mx=1}{f}}} \mathbin{\htmlData{mx=8}{\land}} \htmlData{mx=6}{\htmlData{mx=4}{2}^{\htmlData{mx=5}{f}}} \mathrel{\htmlData{mx=7}{<}} 2

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to f. (0 ≤ f)
<Less than: f is strictly smaller than 1. (f < 1)
∧And: Both hold: 1 ≤ 2^f, and 2^f < 2. (1 ≤ (2:ℝ) ^ f ∧ (2:ℝ) ^ f < 2)
(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 f. ((2:ℝ) ^ f)

theorem bz-exp2-fraction-bracket (f : ℝ) (h0 : 0 ≤ f) (h1 : f < 1) :
    1 ≤ (2:ℝ) ^ f ∧ (2:ℝ) ^ f < 2

The non-integer part of exp2 is confined to one binade, so it is computed once at fixed relative precision. 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: 15 lines of Lean

For 0 ≤ f < 1, the mantissa 2^f lies in [1, 2)

How it was proved

More proved statements