Provedalphabaguettebaguette-zrange

Both reversible streams grow at most linearly: |xᵢ(L)| ≤ |xᵢ(0)| + L·A

For all $\htmlData{mx=3}{x_{1}, x_{2}, F, H : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{A \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=12}{\forall l,\ \htmlData{mx=3}{\htmlData{mx=0}{x_{1}}(\htmlData{mx=2}{\htmlData{mx=1}{l} + 1})} \mathrel{\htmlData{mx=11}{=}} \htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=4}{x_{1}}(\htmlData{mx=5}{l})} + \htmlData{mx=9}{\htmlData{mx=7}{F}(\htmlData{mx=8}{l})}}}$ , $\htmlData{mx=12}{\forall l,\ \htmlData{mx=3}{\htmlData{mx=0}{x_{2}}(\htmlData{mx=2}{\htmlData{mx=1}{l} + 1})} \mathrel{\htmlData{mx=11}{=}} \htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=4}{x_{2}}(\htmlData{mx=5}{l})} + \htmlData{mx=9}{\htmlData{mx=7}{H}(\htmlData{mx=8}{l})}}}$ , $\htmlData{mx=6}{\forall l,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{F}(\htmlData{mx=1}{l})} \right\rvert} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{A}}$ and $\htmlData{mx=6}{\forall l,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{H}(\htmlData{mx=1}{l})} \right\rvert} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{A}}$ , then

\htmlData{mx=26}{\forall L \in \htmlData{mx=25}{\mathbb{N}},\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{x_{1}}(\htmlData{mx=1}{L})} \right\rvert} \mathrel{\htmlData{mx=11}{\leq}} \htmlData{mx=10}{\htmlData{mx=6}{\left\lvert \htmlData{mx=5}{\htmlData{mx=4}{x_{1}}(0)} \right\rvert} + \htmlData{mx=9}{\htmlData{mx=7}{L} \cdot \htmlData{mx=8}{A}}} \mathbin{\htmlData{mx=24}{\land}} \htmlData{mx=15}{\left\lvert \htmlData{mx=14}{\htmlData{mx=12}{x_{2}}(\htmlData{mx=13}{L})} \right\rvert} \mathrel{\htmlData{mx=23}{\leq}} \htmlData{mx=22}{\htmlData{mx=18}{\left\lvert \htmlData{mx=17}{\htmlData{mx=16}{x_{2}}(0)} \right\rvert} + \htmlData{mx=21}{\htmlData{mx=19}{L} \cdot \htmlData{mx=20}{A}}}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
⟹Implies: If ℕ, then ℝ. (Between types, A → B is the type of functions from A to B.) (ℕ → ℝ)
x : TVariables: x₁, x₂, F, H range over ℕ → ℝ: the statement must hold for every choice. ((x₁ x₂ F H : ℕ → ℝ))
∀For all: The statement after the comma holds for every l. (∀ l, x₁ (l + 1) = x₁ l + F l)
RReal numbers: The real numbers: every point on the number line. (ℝ)
f(x)Function application: x₁ applied to l + 1. Lean writes f x; papers write f(x). (x₁ (l + 1))
=Equality: x₁(l + 1) and x₁(l) + F(l) are the same. (x₁ (l + 1) = x₁ l + F l)
|x|Absolute value: The size of F(l) without its sign. (|F l|)
≤At most: |F(l)| is less than or equal to A. (|F l| ≤ A)
+Addition: l plus 1. (l + 1)
∧And: Both hold: |x₁(L)| ≤ |x₁(0)| + L · A, and |x₂(L)| ≤ |x₂(0)| + L · A. (|x₁ L| ≤ |x₁ 0| + L * A ∧ |x₂ L| ≤ |x₂ …)
·Multiplication: L times A. (L * A)

theorem bz-two-stream-linear-growth (x₁ x₂ F H : ℕ → ℝ) (hx₁ : ∀ l, x₁ (l + 1) = x₁ l + F l) (hx₂ : ∀ l, x₂ (l + 1) = x₂ l + H l) (A : ℝ) (hF : ∀ l, |F l| ≤ A) (hH : ∀ l, |H l| ≤ A) :
    ∀ L : ℕ, |x₁ L| ≤ |x₁ 0| + L * A ∧ |x₂ L| ≤ |x₂ 0| + L * A

If every sublayer increment is bounded by A, after L blocks each stream is within L·A of its start. This gives a compile-time integer width for the whole reversible stack. 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: Classical.choice, Quot.sound, propext
Proof: 23 lines of Lean

Both reversible streams grow at most linearly: |xᵢ(L)| ≤ |xᵢ(0)| + L·A

How it was proved

More proved statements