Provedaitherhot-reloadsimulationb846d70

Aither: one-step simulation lifts to equal finite audio traces

For all $\htmlData{mx=1}{S, T, I, 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}{O}}}$ , $\htmlData{mx=5}{g \in \htmlData{mx=4}{\htmlData{mx=0}{\operatorname{Step}}\,\htmlData{mx=1}{T}\,\htmlData{mx=2}{I}\,\htmlData{mx=3}{O}}}$ and $\htmlData{mx=5}{R : \htmlData{mx=0}{S} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{T} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\operatorname{Prop}}}$ :

\begin{aligned} & \htmlData{mx=5}{\htmlData{mx=1}{\operatorname{StepSimulation}}\,\htmlData{mx=2}{f}\,\htmlData{mx=3}{g}\,\htmlData{mx=4}{R}} \\ & \htmlData{mx=0}{\implies} \htmlData{mx=6}{\forall} s \in \htmlData{mx=7}{S},\ t \in \htmlData{mx=8}{T},\ \mathit{inputs} : \htmlData{mx=11}{\htmlData{mx=9}{\operatorname{List}}\,\htmlData{mx=10}{I}}, \\ & \quad \htmlData{mx=16}{\htmlData{mx=13}{R}(\htmlData{mx=14}{s}, \htmlData{mx=15}{t})} \\ & \quad \htmlData{mx=12}{\implies} \htmlData{mx=32}{\htmlData{mx=31}{\htmlData{mx=25}{\htmlData{mx=24}{\htmlData{mx=18}{R}(\htmlData{mx=23}{\htmlData{mx=19}{\operatorname{run}}(\htmlData{mx=20}{f}, \htmlData{mx=21}{s}, \htmlData{mx=22}{\mathit{inputs}})})}_{1}}(\htmlData{mx=30}{\htmlData{mx=26}{\operatorname{run}}(\htmlData{mx=27}{g}, \htmlData{mx=28}{t}, \htmlData{mx=29}{\mathit{inputs}})})}_{1}} \\ & \quad \htmlData{mx=17}{\land} \htmlData{mx=38}{\htmlData{mx=37}{\htmlData{mx=33}{\operatorname{run}}(\htmlData{mx=34}{f}, \htmlData{mx=35}{s}, \htmlData{mx=36}{\mathit{inputs}})}_{2}} \mathrel{\htmlData{mx=45}{=}} \htmlData{mx=44}{\htmlData{mx=43}{\htmlData{mx=39}{\operatorname{run}}(\htmlData{mx=40}{g}, \htmlData{mx=41}{t}, \htmlData{mx=42}{\mathit{inputs}})}_{2}} \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, T, I, O range over Type: the statement must hold for every choice. ((S T 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)
StepSimulation: StepSimulation: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (StepSimulation)
⟹Implies: If T, then Prop. (Between types, A → B is the type of functions from A to B.) (T → Prop)
Prop: Prop: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Prop)
∀For all: The statement after the comma holds for every s, t, inputs. (∀ (s : S) (t : T) (inputs : List I), R …)
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 1 of R(run(f, s, inputs)) (the first). (R (run f s inputs).1)
∧And: Both hold: R(run(f, s, inputs)).1(run(g, t, inputs)).1, and run(f, s, inputs).2 = run(g, t, inputs).2. (R (run f s inputs).1 (run g t inputs).1…)
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)
=Equality: run(f, s, inputs).2 and run(g, t, inputs).2 are the same. ((run f s inputs).2 = (run g t inputs).2)

theorem aither-b846-hot-swap-simulation (S T I O : Type) (f : Step S I O) (g : Step T I O) (R : S → T → Prop) :
    StepSimulation f g R → ∀ (s : S) (t : T) (inputs : List I), R s t → R (run f s inputs).1 (run g t inputs).1 ∧ (run f s inputs).2 = (run g t inputs).2

If old and new transition systems preserve a state relation and emit equal outputs for every related one-step input, then every common finite input trace yields equal outputs and related final states. This is a nontrivial inductive lifting theorem, not a claim that arbitrary reloads satisfy its one-step premise.

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: None
Proof: 20 lines of Lean

Aither: one-step simulation lifts to equal finite audio traces

How it was proved

More proved statements