Provedalphabaguettebaguette-zreversible

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

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

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

For y₁ = x₁ + F x₂ and y₂ = x₂ + H y₁ over any additive group, (y₁ − F(y₂ − H y₁), y₂ − H y₁) = (x₁, x₂). 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 explicit inverse undoes the forward map

How it was proved

More proved statements