The Arrow of Time as a Theorem: Transforming the Second Law of Thermodynamics from Law to Theorem on Reversible Dynamics

Since Loschmidt the arrow of time has posed one question: how can microscopic dynamics that run equally well backwards produce a law that runs one way? The Second Law of Thermodynamics has stood as a law, not a theorem, because every derivation from reversible mechanics needed a premise to close that gap. This paper transforms it into a theorem. Take any finite state space and let the microscopic dynamics be any permutation of it: reversible, information-preserving, Liouville's theorem in finite form. A macrostate is a set of microstates and its Boltzmann multiplicity W the number of them. A macroscopic process from A to B is reproducible when every microstate prepared in A is carried into B: the prepared record persists, which is existence stated on the record and Jaynes's reproducibility. The main theorem: a process is reproducible under some reversible dynamics if and only if W ( A) ≤ W ( B). The forward half is the Second Law, Jaynes's 1965 argument made exact: reversible mechanics obeys the Second Law on every reproducible process. The converse, achievability, says every pair of macrostates that does not lower entropy is reproduced by some permutation of the state space; dynamics with further conservation laws restrict which. The arrow follows as theorems. After a rise in W no reversible dynamics reproduces the return. Each direction is reproducible exactly when W is unchanged. And Loschmidt's objection is located: the inverse dynamics returns every trajectory it carried, yet whenever W rose it does not carry the macrostate back, because reversal returns trajectories, not macrostates. The one hypothesis is reproducibility, and it is where time's direction enters: a process is prepared, then observed, and the act of repeatable preparation supplies the arrow that the time-symmetric dynamics cannot. Existence is self-recursive: every state lies in its own record, and the record of anything in a record is that record. On the nine states 2a 3b graded by the prime count Ω = a + b the multiplicities are 1, 2, 3, 2, 1; the count is raised reproducibly from 0 to 1 and from 1 to 2, never lowered from 1 to 0, and the widest shell has no reproducible exit. Every theorem is proved in Lean 4 with Mathlib, each cone pinned. The arrow of time, as the Second Law states it for reproducible processes, is a theorem of reversible dynamics.