Provedaitherstereoevaluationb846d70

Aither: sharing a mono result advances state once; duplicate evaluation need not

For all $\htmlData{mx=1}{S, I, O \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=5}{f \in \htmlData{mx=4}{\htmlData{mx=0}{\operatorname{Step}}\,\htmlData{mx=1}{S}\,\htmlData{mx=2}{I}\,\htmlData{mx=3}{O}}}$ :

\begin{aligned} & \left(\right. \htmlData{mx=1}{\forall} s \in \htmlData{mx=2}{S},\ i \in \htmlData{mx=3}{I}, \\ & \quad \htmlData{mx=10}{\htmlData{mx=9}{\htmlData{mx=5}{\operatorname{share}}(\htmlData{mx=6}{f}, \htmlData{mx=7}{s}, \htmlData{mx=8}{i})}_{1}} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{\htmlData{mx=14}{\htmlData{mx=11}{f}(\htmlData{mx=12}{s}, \htmlData{mx=13}{i})}_{1}} \\ & \quad \htmlData{mx=4}{\land} \htmlData{mx=27}{\operatorname{2.1}\left(\htmlData{mx=26}{\htmlData{mx=22}{\operatorname{share}}(\htmlData{mx=23}{f}, \htmlData{mx=24}{s}, \htmlData{mx=25}{i})}\right)} \mathrel{\htmlData{mx=39}{=}} \htmlData{mx=38}{\operatorname{2.2}\left(\htmlData{mx=37}{\htmlData{mx=33}{\operatorname{share}}(\htmlData{mx=34}{f}, \htmlData{mx=35}{s}, \htmlData{mx=36}{i})}\right)} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=40}{\forall} n \in \htmlData{mx=41}{\mathbb{N}}, \\ & \quad \htmlData{mx=47}{\htmlData{mx=43}{\operatorname{share}}(\htmlData{mx=44}{\operatorname{counter}}, \htmlData{mx=45}{n}, \htmlData{mx=46}{\left( \right)})} \mathrel{\htmlData{mx=54}{=}} \htmlData{mx=53}{\left( \htmlData{mx=49}{\htmlData{mx=48}{n} + 1}, \htmlData{mx=52}{\left( \htmlData{mx=50}{n}, \htmlData{mx=51}{n} \right)} \right)} \\ & \quad \htmlData{mx=42}{\land} \htmlData{mx=59}{\htmlData{mx=55}{\operatorname{duplicate}}(\htmlData{mx=56}{\operatorname{counter}}, \htmlData{mx=57}{n}, \htmlData{mx=58}{\left( \right)})} \mathrel{\htmlData{mx=67}{=}} \htmlData{mx=66}{\left( \htmlData{mx=61}{\htmlData{mx=60}{n} + 2}, \htmlData{mx=65}{\left( \htmlData{mx=62}{n}, \htmlData{mx=64}{\htmlData{mx=63}{n} + 1} \right)} \right)} \\ & \quad \htmlData{mx=42}{\land} \htmlData{mx=73}{\htmlData{mx=72}{\htmlData{mx=68}{\operatorname{share}}(\htmlData{mx=69}{\operatorname{counter}}, \htmlData{mx=70}{n}, \htmlData{mx=71}{\left( \right)})}_{1}} \mathrel{\htmlData{mx=80}{\neq}} \htmlData{mx=79}{\htmlData{mx=78}{\htmlData{mx=74}{\operatorname{duplicate}}(\htmlData{mx=75}{\operatorname{counter}}, \htmlData{mx=76}{n}, \htmlData{mx=77}{\left( \right)})}_{1}} \left.\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)
x ∈ TVariables: S, I, O range over Type: the statement must hold for every choice. ((S I O : Type))
Step: Step: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Step)
f(x)Function application: Step applied to S, I, O. Lean writes f x; papers write f(x). (Step S I O)
∀For all: The statement after the comma holds for every s, i. (∀ (s : S) (i : I), (share f s i).1 = (f…)
p₁Component: Component 1 of share(f, s, i) (the first). ((share f s i).1)
=Equality: share(f, s, i).1 and f(s, i).1 are the same. ((share f s i).1 = (f s i).1)
∧And: Both hold: share(f, s, i).1 = f(s, i).1, and 2.1(share(f, s, i)) = 2.2(share(f, s, i)). ((share f s i).1 = (f s i).1 ∧ (share f …)
share: share: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (share)
e.f2.1: 2.1 of share(f, s, i): Lean's dot notation e.2.1 means 2.1 applied to e. ((share f s i).2.1)
e.f2.2: 2.2 of share(f, s, i): Lean's dot notation e.2.2 means 2.2 applied to e. ((share f s i).2.2)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
counter: counter: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (counter)
(a, b)Tuple: The ordered pair (or tuple) of . (())
+Addition: n plus 1. (n + 1)
duplicate: duplicate: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (duplicate)
≠Not equal: share(counter, n, ()).1 and duplicate(counter, n, ()).1 are different. ((share counter n ()).1 ≠ (duplicate cou…)

theorem aither-b846-evaluate-once (S I O : Type) (f : Step S I O) :
    (∀ (s : S) (i : I), (share f s i).1 = (f s i).1 ∧ (share f s i).2.1 = (share f s i).2.2) ∧ (∀ n : Nat, share counter n () = (n + 1, (n, n)) ∧ duplicate counter n () = (n + 2, (n, n + 1)) ∧ (share counter n ()).1 ≠ (duplicate counter n ()).1)

Abstract justification for emitStereo binding compound scalar expressions to a temporary. Sharing preserves a single step and equal channels; a counter proves duplicate evaluation advances twice and can produce unequal channel values. Not a complete code-generation correctness proof.

How it was proved

Proved: 1 October 2026
By: Ajax
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: 18 lines of Lean

Aither: sharing a mono result advances state once; duplicate evaluation need not

How it was proved

More proved statements