proofs
Provedaitheraudiosemanticsb846d70

Aither: independent product-state channels stay independent for every finite trace

For all S,T,I,O,P∈Type⁡\htmlData{mx=1}{S, T, I, O, P \in \htmlData{mx=0}{\operatorname{Type}}}, f∈Step⁡ S I O\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}}} and g∈Step⁡ T I P\htmlData{mx=5}{g \in \htmlData{mx=4}{\htmlData{mx=0}{\operatorname{Step}}\,\htmlData{mx=1}{T}\,\htmlData{mx=2}{I}\,\htmlData{mx=3}{P}}}:

∀s∈S, t∈T, xs:List⁡ I, 1.1⁡(run⁡(parallel⁡(f,g),(s,t),xs))=run⁡(f,s,xs)1∧1.2⁡(run⁡(parallel⁡(f,g),(s,t),xs))=run⁡(g,t,xs)1∧run⁡(parallel⁡(f,g),(s,t),xs)2(.map Prod.fst = (run f s xs).2 ∧ (run (parallel f g) (s, t) xs).2.map Prod.snd = (run g t xs).2)\htmlData{mx=75}{\htmlData{mx=74}{\forall s \in \htmlData{mx=69}{S},\ t \in \htmlData{mx=70}{T},\ \mathit{xs} : \htmlData{mx=73}{\htmlData{mx=71}{\operatorname{List}}\,\htmlData{mx=72}{I}},\ \htmlData{mx=20}{\operatorname{1.1}\left(\htmlData{mx=19}{\htmlData{mx=10}{\operatorname{run}}(\htmlData{mx=14}{\htmlData{mx=11}{\operatorname{parallel}}(\htmlData{mx=12}{f}, \htmlData{mx=13}{g})}, \htmlData{mx=17}{\left( \htmlData{mx=15}{s}, \htmlData{mx=16}{t} \right)}, \htmlData{mx=18}{\mathit{xs}})}\right)} \mathrel{\htmlData{mx=27}{=}} \htmlData{mx=26}{\htmlData{mx=25}{\htmlData{mx=21}{\operatorname{run}}(\htmlData{mx=22}{f}, \htmlData{mx=23}{s}, \htmlData{mx=24}{\mathit{xs}})}_{1}} \mathbin{\htmlData{mx=68}{\land}} \htmlData{mx=48}{\operatorname{1.2}\left(\htmlData{mx=47}{\htmlData{mx=38}{\operatorname{run}}(\htmlData{mx=42}{\htmlData{mx=39}{\operatorname{parallel}}(\htmlData{mx=40}{f}, \htmlData{mx=41}{g})}, \htmlData{mx=45}{\left( \htmlData{mx=43}{s}, \htmlData{mx=44}{t} \right)}, \htmlData{mx=46}{\mathit{xs}})}\right)} \mathrel{\htmlData{mx=55}{=}} \htmlData{mx=54}{\htmlData{mx=53}{\htmlData{mx=49}{\operatorname{run}}(\htmlData{mx=50}{g}, \htmlData{mx=51}{t}, \htmlData{mx=52}{\mathit{xs}})}_{1}} \mathbin{\htmlData{mx=67}{\land}} \htmlData{mx=66}{\htmlData{mx=65}{\htmlData{mx=56}{\operatorname{run}}(\htmlData{mx=60}{\htmlData{mx=57}{\operatorname{parallel}}(\htmlData{mx=58}{f}, \htmlData{mx=59}{g})}, \htmlData{mx=63}{\left( \htmlData{mx=61}{s}, \htmlData{mx=62}{t} \right)}, \htmlData{mx=64}{\mathit{xs}})}_{2}}}(\mathtt{.map\ Prod.fst\ =\ (run\ f\ s\ xs).2\ \text{∧}\ (run\ (parallel\ f\ g)\ (s,\ t)\ xs).2.map\ Prod.snd\ =\ (run\ g\ t\ xs).2})}
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, T, I, O, P range over Type: the statement must hold for every choice. ((S T I O P : 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, t, xs. (∀ (s : S) (t : T) (xs : List I), (run (…)
List
List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
e.f1.1
1.1 of run(parallel(f, g), (s, t), xs): Lean's dot notation e.1.1 means 1.1 applied to e. ((run (parallel f g) (s, t) xs).1.1)
=Equality
1.1(run(parallel(f, g), (s, t), xs)) and run(f, s, xs).1 are the same. ((run (parallel f g) (s, t) xs).1.1 = (r…)
run
run: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (run)
parallel
parallel: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (parallel)
(a, b)Tuple
The ordered pair (or tuple) of s, t. ((s, t))
p₁Component
Component 1 of run(f, s, xs) (the first). ((run f s xs).1)
e.f1.2
1.2 of run(parallel(f, g), (s, t), xs): Lean's dot notation e.1.2 means 1.2 applied to e. ((run (parallel f g) (s, t) xs).1.2)
∧And
Both hold: 1.2(run(parallel(f, g), (s, t), xs)) = run(g, t, xs).1, and run(parallel(f, g), (s, t), xs).2. ((run (parallel f g) (s, t) xs).1.2 = (r…)

Product-state analogue of codegen.nim TransparentHelpers. Projected channel states and output traces equal running each channel alone. This does not prove the generated C uses independent addresses; the native cursor counterexample records that separate gap.

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
propext
Proof
19 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements