Provedaitheraudiosemanticsb846d70

Aither: finite traces compose in time and in signal pipelines

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

\htmlData{mx=11}{(\htmlData{mx=10}{\forall s \in \htmlData{mx=6}{S},\ \mathit{xs} : \htmlData{mx=9}{\htmlData{mx=7}{\operatorname{List}}\,\htmlData{mx=8}{I}},\ \htmlData{mx=5}{\htmlData{mx=4}{\htmlData{mx=0}{\operatorname{run}}(\htmlData{mx=1}{f}, \htmlData{mx=2}{s}, \htmlData{mx=3}{\mathit{xs}})}_{2}}})(\mathtt{.length\ =\ xs.length)\ \text{∧}\ (\forall \ (s\ :\ S)\ (xs\ ys\ :\ List\ I),\ run\ f\ s\ (xs\ ++\ ys)\ =\ ((run\ f\ (run\ f\ s\ xs).1\ ys).1,\ (run\ f\ s\ xs).2\ ++\ (run\ f\ (run\ f\ s\ xs).1\ ys).2))\ \text{∧}\ (\forall \ (s\ :\ S)\ (t\ :\ T)\ (xs\ :\ List\ I),\ run\ (serial\ f\ g)\ (s,\ t)\ xs\ =\ (((run\ f\ s\ xs).1,\ (run\ g\ t\ (run\ f\ s\ xs).2).1),\ (run\ g\ t\ (run\ f\ s\ xs).2).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, M, O range over Type: the statement must hold for every choice. ((S T I M 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, M. Lean writes f x; papers write f(x). (Step S I M)
∀For all: The statement after the comma holds for every s, xs. (∀ (s : S) (xs : List I), (run f s xs).2)
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)
p₁Component: Component 2 of run(f, s, xs) (the second). ((run f s xs).2)
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)

theorem aither-b846-trace-composition (S T I M O : Type) (f : Step S I M) (g : Step T M O) :
    (∀ (s : S) (xs : List I), (run f s xs).2.length = xs.length) ∧ (∀ (s : S) (xs ys : List I), run f s (xs ++ ys) = ((run f (run f s xs).1 ys).1, (run f s xs).2 ++ (run f (run f s xs).1 ys).2)) ∧ (∀ (s : S) (t : T) (xs : List I), run (serial f g) (s, t) xs = (((run f s xs).1, (run g t (run f s xs).2).1), (run g t (run f s xs).2).2))

Abstract state-transition contract motivated by README f(state) -> sample. One output per input, chunking invariance, and serial composition equivalent to feeding the intermediate trace into the second machine. External input is explicit. Not a compiler-extraction or real-time scheduling 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: propext
Proof: 34 lines of Lean

Aither: finite traces compose in time and in signal pipelines

How it was proved

More proved statements