Provedalphabaguettebaguette-zreversible

Two-stream block: the forward map undoes the explicit inverse

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

\begin{aligned} & \htmlData{mx=43}{\left( \htmlData{mx=17}{\htmlData{mx=9}{\htmlData{mx=1}{y_{1}} - \htmlData{mx=8}{\htmlData{mx=2}{F}(\htmlData{mx=7}{\htmlData{mx=3}{y_{2}} - \htmlData{mx=6}{\htmlData{mx=4}{H}(\htmlData{mx=5}{y_{1}})}})}} + \htmlData{mx=16}{\htmlData{mx=10}{F}(\htmlData{mx=15}{\htmlData{mx=11}{y_{2}} - \htmlData{mx=14}{\htmlData{mx=12}{H}(\htmlData{mx=13}{y_{1}})}})}}, \htmlData{mx=42}{\htmlData{mx=22}{\htmlData{mx=18}{y_{2}} - \htmlData{mx=21}{\htmlData{mx=19}{H}(\htmlData{mx=20}{y_{1}})}} + \htmlData{mx=41}{\htmlData{mx=23}{H}(\htmlData{mx=40}{\htmlData{mx=32}{\htmlData{mx=24}{y_{1}} - \htmlData{mx=31}{\htmlData{mx=25}{F}(\htmlData{mx=30}{\htmlData{mx=26}{y_{2}} - \htmlData{mx=29}{\htmlData{mx=27}{H}(\htmlData{mx=28}{y_{1}})}})}} + \htmlData{mx=39}{\htmlData{mx=33}{F}(\htmlData{mx=38}{\htmlData{mx=34}{y_{2}} - \htmlData{mx=37}{\htmlData{mx=35}{H}(\htmlData{mx=36}{y_{1}})}})}})}} \right)} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=46}{\left( \htmlData{mx=44}{y_{1}}, \htmlData{mx=45}{y_{2}} \right)} \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)
⟹Implies: If G, then G. (Between types, A → B is the type of functions from A to B.) (G → G)
x : TVariables: F, H range over G → G: the statement must hold for every choice. ((F H : G → G))
x ∈ TVariables: y₁, y₂ range over G: the statement must hold for every choice. ((y₁ y₂ : G))
(a, b)Tuple: The ordered pair (or tuple) of y₁ − F(y₂ − H(y₁)) + F(y₂ − H(y₁)), y₂ − H(y₁) + H(y₁ − F(y₂ − H(y₁)) + F(y₂ − H(y₁))). (((y₁ - F (y₂ - H y₁)) + F (y₂ - H y₁), …)
=Equality: (y₁ − F(y₂ − H(y₁)) + F(y₂ − H(y₁)), y₂ − H(y₁) + H(y₁ − F… and (y₁, y₂) are the same. (((y₁ - F (y₂ - H y₁)) + F (y₂ - H y₁), …)
+Addition: y₁ − F(y₂ − H(y₁)) plus F(y₂ − H(y₁)). ((y₁ - F (y₂ - H y₁)) + F (y₂ - H y₁))
-Subtraction: y₂ minus H(y₁). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (y₂ - H y₁)

theorem bz-rev-right-inverse {G : Type} [AddGroup G] (F H : G → G) (y₁ y₂ : G) :
    ((y₁ - F (y₂ - H y₁)) + F (y₂ - H y₁), (y₂ - H y₁) + H ((y₁ - F (y₂ - H y₁)) + F (y₂ - H y₁))) = (y₁, y₂)

Applying the block to (y₁ − F(y₂ − H y₁), y₂ − H y₁) returns (y₁, y₂): the inverse is two-sided. 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: 12 lines of Lean

Two-stream block: the forward map undoes the explicit inverse

How it was proved

More proved statements