Provedalphabaguettebaguette-zreversible

Exactness holds with arbitrarily-rounded real sublayers on integer streams

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=11}{f, h : (\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{Z}}) \mathrel{\htmlData{mx=10}{\to}} \htmlData{mx=7}{\htmlData{mx=5}{\operatorname{Fin}}\,\htmlData{mx=6}{n}} \mathrel{\htmlData{mx=9}{\to}} \htmlData{mx=8}{\mathbb{R}}}$ :

\htmlData{mx=36}{\htmlData{mx=35}{p \mapsto \htmlData{mx=23}{\left( \htmlData{mx=7}{\htmlData{mx=0}{p_{1}} + (\htmlData{mx=6}{i \mapsto \htmlData{mx=5}{\left\lfloor \htmlData{mx=4}{\htmlData{mx=1}{f}(\htmlData{mx=2}{p_{2}}, \htmlData{mx=3}{i})} \right\rfloor}})}, \htmlData{mx=22}{\htmlData{mx=8}{p_{2}} + (\htmlData{mx=21}{i \mapsto \htmlData{mx=20}{\left\lfloor \htmlData{mx=19}{\htmlData{mx=9}{h}(\htmlData{mx=17}{\htmlData{mx=10}{p_{1}} + (\htmlData{mx=16}{i \mapsto \htmlData{mx=15}{\left\lfloor \htmlData{mx=14}{\htmlData{mx=11}{f}(\htmlData{mx=12}{p_{2}}, \htmlData{mx=13}{i})} \right\rfloor}})}, \htmlData{mx=18}{i})} \right\rfloor}})} \right)}} \text{ is bijective}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x : TVariables: f, h range over (Fin n → ℤ) → (Fin n → ℝ): the statement must hold for every choice. ((f h : (Fin n → ℤ) → (Fin n → ℝ)))
bijectiveBijective: p ↦ (p.1 + (i ↦ ⌊f(p.2, i)⌋), p.2 + (i ↦ ⌊h(p.1 + (i ↦ ⌊f(… pairs inputs and outputs one to one. (Function.Bijective (fun p : (Fin n → ℤ)…)
Fin: Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
f(x)Function application: Fin applied to n. Lean writes f x; papers write f(x). (Fin n)
⟹Implies: If Fin(n), then ℤ. (Between types, A → B is the type of functions from A to B.) (Fin n → ℤ)
ZIntegers: The integers …, −2, −1, 0, 1, 2, …. (ℤ)
RReal numbers: The real numbers: every point on the number line. (ℝ)
×Product: Pairs of an element of Fin(n) → ℤ and an element of Fin(n) → ℤ. ((Fin n → ℤ) × (Fin n → ℤ))
(a, b)Tuple: The ordered pair (or tuple) of p.1 + (i ↦ ⌊f(p.2, i)⌋), p.2 + (i ↦ ⌊h(p.1 + (i ↦ ⌊f(p.2, i)⌋), i)⌋). ((p.1 + (fun i => ⌊f p.2 i⌋), p.2 + (fun…)
p₁Component: The first component of the pair p. (p.1)
+Addition: p.1 plus i ↦ ⌊f(p.2, i)⌋. (p.1 + (fun i => ⌊f p.2 i⌋))
x ↦ f(x)Function (λ-abstraction): The function sending i to ⌊f(p.2, i)⌋. Lean writes fun x => …; papers write x ↦ …. (fun i => ⌊f p.2 i⌋)
⌊x⌋Floor: The largest integer not above f(p.2, i). (⌊f p.2 i⌋)

theorem bz-rev-quantized-sublayers-bijective (n : ℕ) (f h : (Fin n → ℤ) → (Fin n → ℝ)) :
    Function.Bijective (fun p : (Fin n → ℤ) × (Fin n → ℤ) => (p.1 + (fun i => ⌊f p.2 i⌋), p.2 + (fun i => ⌊h (p.1 + (fun i => ⌊f p.2 i⌋)) i⌋)))

On integer vectors, the block (x₁ + ⌊f(x₂)⌋, x₂ + ⌊h(·)⌋) is a bijection for any real-valued sublayers f, h: the sublayers may be computed in BF16/FP32 with any rounding, and reconstruction is still exact. 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: 17 lines of Lean

Exactness holds with arbitrarily-rounded real sublayers on integer streams

How it was proved

More proved statements