Provedbaguettealphagpu-kernelsfloating-point

A row's maximum is the maximum of its tiles' maxima

For all $\htmlData{mx=1}{\alpha \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=5}{L \in \htmlData{mx=4}{\htmlData{mx=0}{\operatorname{List}}\,\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{List}}\,\htmlData{mx=2}{\alpha}}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{LinearOrder}}\,\htmlData{mx=1}{\alpha}}$ ):

\begin{aligned} & \htmlData{mx=10}{\htmlData{mx=3}{\operatorname{foldr}\left(\htmlData{mx=2}{\operatorname{flatten}}\right)}(\htmlData{mx=8}{a, m \mapsto \htmlData{mx=7}{\max(\htmlData{mx=5}{\htmlData{mx=4}{a}}, \htmlData{mx=6}{m})}}, \htmlData{mx=9}{\bot})} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=40}{\htmlData{mx=37}{\operatorname{foldr}\left(\htmlData{mx=36}{\htmlData{mx=24}{\operatorname{map}}(\htmlData{mx=35}{r \mapsto \htmlData{mx=34}{\htmlData{mx=27}{\operatorname{foldr}\left(\htmlData{mx=26}{r}\right)}(\htmlData{mx=32}{a, m \mapsto \htmlData{mx=31}{\max(\htmlData{mx=29}{\htmlData{mx=28}{a}}, \htmlData{mx=30}{m})}}, \htmlData{mx=33}{\bot})}})}\right)}(\htmlData{mx=38}{\operatorname{max}}, \htmlData{mx=39}{\bot})} \end{aligned}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
LinearOrder: LinearOrder: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (LinearOrder)
f(x)Function application: LinearOrder applied to α. Lean writes f x; papers write f(x). (LinearOrder α)
List: List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
e.ffoldr: foldr of flatten: Lean's dot notation e.foldr means foldr applied to e. ((L.flatten).foldr)
=Equality: foldr(flatten)(a, m ↦ max(a, m), ⊥) and foldr(map(r ↦ foldr(a, m ↦ max(a, m), ⊥)))(max, ⊥) are the same. ((L.flatten).foldr (fun a m => max (a : …)
flatten: L.flatten: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (L.flatten)
x ↦ f(x)Function (λ-abstraction): The function sending a, m to max(a, m). Lean writes fun x => …; papers write x ↦ …. (fun a m => max (a : WithBot α) m)
maxMaximum: The larger of a and m. (max (a : WithBot α) m)
(x : T)Type ascription: a read as a WithBot(α). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((a : WithBot α))
⊥Bottom: The smallest element (or “false”). (⊥)
map: L.map: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (L.map)
max: max: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (max)

theorem row-maximum-of-tile-maxima {α : Type} [LinearOrder α] (L : List (List α)) :
    (L.flatten).foldr (fun a m => max (a : WithBot α) m) ⊥ = (L.map (fun r => r.foldr (fun a m => max (a : WithBot α) m) ⊥)).foldr max ⊥

Correctness core of Baguette's vocabulary row-maxima fusion (Alpha commit be1bfeb5): the tied-vocabulary product stores each row's maximum over every 128-column tile, and the loss rows take the row's maximum as the maximum over those partials instead of scanning all 65,536 logits. Over any linear order extended with a bottom element (the model's FMNMX: -0 below +0, a NaN operand acting as the identity), the fold of max over the concatenation of the tiles equals the fold of max over the tiles' folds, so any tiling and grouping gives the same word.

How it was proved

Proved: 4 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Quot.sound, propext
Proof: 22 lines of Lean

A row's maximum is the maximum of its tiles' maxima

How it was proved

More proved statements