Provedalphabaguettebaguette-zinvariant

A state invariant preserved by every step holds for the whole training run

For all $\htmlData{mx=1}{\mathit{St} \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=5}{\mathit{step} : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{\mathit{St}} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathit{St}}}$ , $\htmlData{mx=3}{I : \htmlData{mx=0}{\mathit{St}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\operatorname{Prop}}}$ , $\htmlData{mx=1}{s_{0} \in \htmlData{mx=0}{\mathit{St}}}$ , $\htmlData{mx=3}{h_{0} \in \htmlData{mx=2}{\htmlData{mx=0}{I}\,\htmlData{mx=1}{s_{0}}}}$ and $\htmlData{mx=11}{\mathit{hstep} : \htmlData{mx=10}{\forall t, s,\ \htmlData{mx=2}{\htmlData{mx=0}{I}(\htmlData{mx=1}{s})} \mathrel{\htmlData{mx=9}{\implies}} \htmlData{mx=8}{\htmlData{mx=3}{I}(\htmlData{mx=7}{\htmlData{mx=4}{\mathit{step}}(\htmlData{mx=5}{t}, \htmlData{mx=6}{s})})}}}$ :

\htmlData{mx=6}{\htmlData{mx=5}{\forall T,\ \htmlData{mx=4}{\htmlData{mx=0}{I}(\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{rec}}(\htmlData{mx=2}{\operatorname{motive}})})}}(\mathtt{:=\ fun\ \_\ =>\ St)\ s0\ (fun\ t\ s\ =>\ step\ t\ s)\ T)})}

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)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
f(x)Function application: I applied to s0. Lean writes f x; papers write f(x). (I s0)
∀For all: The statement after the comma holds for every t, s. (∀ t s, I s → I (step t s))
⟹Implies: If St, then St. (Between types, A → B is the type of functions from A to B.) (St → St)
Prop: Prop: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Prop)
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-invariant-for-all-steps {St : Type} (step : ℕ → St → St) (I : St → Prop) (s0 : St) (h0 : I s0) (hstep : ∀ t s, I s → I (step t s)) :
    ∀ T, I (Nat.rec (motive := fun _ => St) s0 (fun t s => step t s) T)

If the initial state satisfies the box invariant I and every step maps I-states to I-states, all states of the run satisfy I. This composes the moment, weight and residual boxes into a whole-run certificate. 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: None
Proof: 15 lines of Lean

A state invariant preserved by every step holds for the whole training run

How it was proved

More proved statements