Provedalphabaguettebaguette-zreversible

A stack of any depth of two-stream integer blocks is a bijection

For all $\htmlData{mx=1}{G \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=5}{F, H : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{G} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{G}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{AddGroup}}\,\htmlData{mx=1}{G}}$ ):

\htmlData{mx=10}{\htmlData{mx=9}{\forall n \in \htmlData{mx=8}{\mathbb{N}},\ \htmlData{mx=7}{\htmlData{mx=6}{p \mapsto \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{rec}}(\htmlData{mx=1}{\operatorname{motive}})}} \text{ is bijective}}}(\mathtt{:=\ fun\ \_\ =>\ G\ \times \ G)\ p\ (fun\ l\ q\ =>\ (q.1\ +\ F\ l\ q.2,\ q.2\ +\ H\ l\ (q.1\ +\ F\ l\ q.2)))\ n)})}

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)
AddGroup: AddGroup: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (AddGroup)
f(x)Function application: AddGroup applied to G. Lean writes f x; papers write f(x). (AddGroup G)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x : TVariables: F, H range over ℕ → G → G: the statement must hold for every choice. ((F H : ℕ → G → G))
∀For all: The statement after the comma holds for every n. (∀ n : ℕ, Function.Bijective (fun p : G …)
⟹Implies: If G, then G. (Between types, A → B is the type of functions from A to B.) (G → G)
bijectiveBijective: p ↦ rec(motive) pairs inputs and outputs one to one. (Function.Bijective (fun p : G × G => Na…)
x ↦ f(x)Function (λ-abstraction): The function sending p to rec(motive). Lean writes fun x => …; papers write x ↦ …. (fun p : G × G => Nat.rec (motive)
×Product: Pairs of an element of G and an element of G. (G × G)
rec: Nat.rec: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Nat.rec)
motive: motive: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (motive)

theorem bz-rev-stack-bijective {G : Type} [AddGroup G] (F H : ℕ → G → G) :
    ∀ n : ℕ, Function.Bijective (fun p : G × G => Nat.rec (motive := fun _ => G × G) p (fun l q => (q.1 + F l q.2, q.2 + H l (q.1 + F l q.2))) n)

Composing L two-stream blocks with arbitrary per-layer sublayers F l, H l gives a bijection of the state space for every L. Baguette-Z's 80 layers (40 attention/feed pairs, or 80 pairs) are exactly invertible. 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, propext
Proof: 23 lines of Lean

A stack of any depth of two-stream integer blocks is a bijection

How it was proved

More proved statements