Provedalphabaguettebaguette-zreversible

Backward recomputation reconstructs every intermediate state exactly

For all $\htmlData{mx=1}{G \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\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}}$ and $\htmlData{mx=5}{s : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\htmlData{mx=1}{G} \times \htmlData{mx=2}{G}}}$ , if $\htmlData{mx=38}{\forall l,\ \htmlData{mx=3}{\htmlData{mx=0}{s}(\htmlData{mx=2}{\htmlData{mx=1}{l} + 1})} \mathrel{\htmlData{mx=37}{=}} \htmlData{mx=36}{\left( \htmlData{mx=15}{\htmlData{mx=7}{\htmlData{mx=6}{\htmlData{mx=4}{s}(\htmlData{mx=5}{l})}_{1}} + \htmlData{mx=14}{\htmlData{mx=13}{\htmlData{mx=8}{F}(\htmlData{mx=9}{l}, \htmlData{mx=12}{\htmlData{mx=10}{s}(\htmlData{mx=11}{l})})}_{2}}}, \htmlData{mx=35}{\htmlData{mx=19}{\htmlData{mx=18}{\htmlData{mx=16}{s}(\htmlData{mx=17}{l})}_{2}} + \htmlData{mx=34}{\htmlData{mx=20}{H}(\htmlData{mx=21}{l}, \htmlData{mx=33}{\htmlData{mx=25}{\htmlData{mx=24}{\htmlData{mx=22}{s}(\htmlData{mx=23}{l})}_{1}} + \htmlData{mx=32}{\htmlData{mx=31}{\htmlData{mx=26}{F}(\htmlData{mx=27}{l}, \htmlData{mx=30}{\htmlData{mx=28}{s}(\htmlData{mx=29}{l})})}_{2}}})}} \right)}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{AddGroup}}\,\htmlData{mx=1}{G}}$ ), then

\begin{aligned} & \htmlData{mx=0}{\forall} l, \\ & \quad \htmlData{mx=39}{\left( \htmlData{mx=24}{\htmlData{mx=6}{\htmlData{mx=5}{\htmlData{mx=2}{s}(\htmlData{mx=4}{\htmlData{mx=3}{l} + 1})}_{1}} - \htmlData{mx=23}{\htmlData{mx=7}{F}(\htmlData{mx=8}{l}, \htmlData{mx=22}{\htmlData{mx=13}{\htmlData{mx=12}{\htmlData{mx=9}{s}(\htmlData{mx=11}{\htmlData{mx=10}{l} + 1})}_{2}} - \htmlData{mx=21}{\htmlData{mx=20}{\htmlData{mx=14}{H}(\htmlData{mx=15}{l}, \htmlData{mx=19}{\htmlData{mx=16}{s}(\htmlData{mx=18}{\htmlData{mx=17}{l} + 1})})}_{1}}})}}, \htmlData{mx=38}{\htmlData{mx=29}{\htmlData{mx=28}{\htmlData{mx=25}{s}(\htmlData{mx=27}{\htmlData{mx=26}{l} + 1})}_{2}} - \htmlData{mx=37}{\htmlData{mx=36}{\htmlData{mx=30}{H}(\htmlData{mx=31}{l}, \htmlData{mx=35}{\htmlData{mx=32}{s}(\htmlData{mx=34}{\htmlData{mx=33}{l} + 1})})}_{1}}} \right)} \\ & \quad \quad \htmlData{mx=1}{=} \htmlData{mx=42}{\htmlData{mx=40}{s}(\htmlData{mx=41}{l})} \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)
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 l. (∀ l, s (l + 1) = ((s l).1 + F l (s l).2…)
⟹Implies: If G, then G. (Between types, A → B is the type of functions from A to B.) (G → G)
×Product: Pairs of an element of G and an element of G. (G × G)
=Equality: s(l + 1) and (s(l).1 + F(l, s(l)).2, s(l).2 + H(l, s(l).1 + F(l, s(l)).… are the same. (s (l + 1) = ((s l).1 + F l (s l).2, (s …)
+Addition: l plus 1. (l + 1)
(a, b)Tuple: The ordered pair (or tuple) of s(l).1 + F(l, s(l)).2, s(l).2 + H(l, s(l).1 + F(l, s(l)).2). (((s l).1 + F l (s l).2, (s l).2 + H l (…)
p₁Component: Component 1 of s(l) (the first). ((s l).1)
-Subtraction: s(l + 1).2 minus H(l, s(l + 1)).1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. ((s (l + 1)).2 - H l (s (l + 1)).1)

theorem bz-rev-reconstruct-every-state {G : Type} [AddGroup G] (F H : ℕ → G → G) (s : ℕ → G × G) (hs : ∀ l, s (l + 1) = ((s l).1 + F l (s l).2, (s l).2 + H l ((s l).1 + F l (s l).2))) :
    ∀ l, ((s (l + 1)).1 - F l ((s (l + 1)).2 - H l (s (l + 1)).1), (s (l + 1)).2 - H l (s (l + 1)).1) = s l

If the stored-nothing forward pass satisfies s(l+1) = block_l(s(l)), then applying the explicit inverse of block l to s(l+1) returns s(l) exactly, for every layer l. No activations need to be saved. 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: propext
Proof: 14 lines of Lean

Backward recomputation reconstructs every intermediate state exactly

How it was proved

More proved statements