proofs
Provedaithercounterexamplehot-reloadb846d70

Aither: identical persistent state does not guarantee identical audio

(∀s∈N, i∈Unit⁡, constantOutput⁡(0,s,i)1=constantOutput⁡(1,s,i)1)∧constantOutput⁡(0,0,())2≠constantOutput⁡(1,0,())2\begin{aligned} & (\htmlData{mx=14}{\forall s \in \htmlData{mx=12}{\mathbb{N}},\ i \in \htmlData{mx=13}{\operatorname{Unit}},\ \htmlData{mx=5}{\htmlData{mx=4}{\htmlData{mx=1}{\operatorname{constantOutput}}(0, \htmlData{mx=2}{s}, \htmlData{mx=3}{i})}_{1}} \mathrel{\htmlData{mx=11}{=}} \htmlData{mx=10}{\htmlData{mx=9}{\htmlData{mx=6}{\operatorname{constantOutput}}(1, \htmlData{mx=7}{s}, \htmlData{mx=8}{i})}_{1}}}) \\ & \htmlData{mx=0}{\land} \htmlData{mx=18}{\htmlData{mx=17}{\htmlData{mx=15}{\operatorname{constantOutput}}(0, 0, \htmlData{mx=16}{\left( \right)})}_{2}} \mathrel{\htmlData{mx=23}{\neq}} \htmlData{mx=22}{\htmlData{mx=21}{\htmlData{mx=19}{\operatorname{constantOutput}}(1, 0, \htmlData{mx=20}{\left( \right)})}_{2}} \end{aligned}
What the notation means · or point at any symbol
∧And
Both hold: ∀ s, i, constantOutput(0, s, i).1 = constantOutput(1, s, i…, and constantOutput(0, 0, ()).2 ≠ constantOutput(1, 0, ()).2. ((∀ (s : Nat) (i : Unit), (constantOutpu…)
∀For all
The statement after the comma holds for every s, i. (∀ (s : Nat) (i : Unit), (constantOutput…)
NNatural numbers
The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
Unit
Unit: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Unit)
p₁Component
Component 1 of constantOutput(0, s, i) (the first). ((constantOutput 0 s i).1)
=Equality
constantOutput(0, s, i).1 and constantOutput(1, s, i).1 are the same. ((constantOutput 0 s i).1 = (constantOut…)
constantOutput
constantOutput: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (constantOutput)
f(x)Function application
constantOutput applied to 0, s, i. Lean writes f x; papers write f(x). (constantOutput 0 s i)
≠Not equal
constantOutput(0, 0, ()).2 and constantOutput(1, 0, ()).2 are different. ((constantOutput 0 0 ()).2 ≠ (constantOu…)
(a, b)Tuple
The ordered pair (or tuple) of . (())

Concrete counterexample to equating state retention with waveform equivalence or click freedom. Two machines preserve every state identically but emit different constant samples. Motivates the separate simulation obligation and an acoustic transition policy; not a claim that all reloads click.

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

More proved statements