Provedalphabaguettebaguette-zinvariant

Skipping non-finite or out-of-range gradients preserves the state invariant

For all $\htmlData{mx=1}{\mathit{St}, \mathit{Gr} \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=5}{\mathit{update} : \htmlData{mx=0}{\mathit{St}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{\mathit{Gr}} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathit{St}}}$ , $\htmlData{mx=3}{\mathit{ok} : \htmlData{mx=0}{\mathit{Gr}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\operatorname{Prop}}}$ , $\htmlData{mx=3}{I : \htmlData{mx=0}{\mathit{St}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\operatorname{Prop}}}$ and $\htmlData{mx=15}{\mathit{hupd} : \htmlData{mx=14}{\forall s, g,\ \htmlData{mx=2}{\htmlData{mx=0}{I}(\htmlData{mx=1}{s})} \mathrel{\htmlData{mx=13}{\implies}} \htmlData{mx=5}{\htmlData{mx=3}{\mathit{ok}}(\htmlData{mx=4}{g})} \mathrel{\htmlData{mx=12}{\implies}} \htmlData{mx=11}{\htmlData{mx=6}{I}(\htmlData{mx=10}{\htmlData{mx=7}{\mathit{update}}(\htmlData{mx=8}{s}, \htmlData{mx=9}{g})})}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{DecidablePred}}\,\htmlData{mx=1}{\mathit{ok}}}$ ):

\htmlData{mx=15}{\forall s, g,\ \htmlData{mx=2}{\htmlData{mx=0}{I}(\htmlData{mx=1}{s})} \mathrel{\htmlData{mx=14}{\implies}} \htmlData{mx=13}{\htmlData{mx=3}{I}\left(\htmlData{mx=12}{\begin{cases} \htmlData{mx=7}{\htmlData{mx=4}{\mathit{update}}(\htmlData{mx=5}{s}, \htmlData{mx=6}{g})} & \text{if } \htmlData{mx=10}{\htmlData{mx=8}{\mathit{ok}}(\htmlData{mx=9}{g})} \\ \htmlData{mx=11}{s} & \text{otherwise} \end{cases}}\right)}}

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)
x ∈ TVariables: St, Gr range over Type: the statement must hold for every choice. ((St Gr : Type))
DecidablePred: DecidablePred: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (DecidablePred)
f(x)Function application: DecidablePred applied to ok. Lean writes f x; papers write f(x). (DecidablePred ok)
∀For all: The statement after the comma holds for every s, g. (∀ s g, I s → ok g → I (update s g))
⟹Implies: If Gr, then St. (Between types, A → B is the type of functions from A to B.) (Gr → 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)
{ a if c; b otherwiseCases (if … then … else): update(s, g) when ok(g), and s otherwise. (if ok g then update s g else s)

theorem bz-skip-policy-preserves-invariant {St Gr : Type} (update : St → Gr → St) (ok : Gr → Prop) [DecidablePred ok] (I : St → Prop) (hupd : ∀ s g, I s → ok g → I (update s g)) :
    ∀ s g, I s → I (if ok g then update s g else s)

Baguette refuses nonfinite updates before mutation. Formally: if updates preserve I whenever the gradient check passes, then 'update if ok else keep' always preserves I. 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

Skipping non-finite or out-of-range gradients preserves the state invariant

How it was proved

More proved statements