Time's arrow is traditionally explained via thermodynamic entropy and boundary conditions. This paper proves a complementary, theorem-grade statement: stable records already force an arrow at the level of semantics. Using the Closure calculus (Paper 27), the strength-ordered barrier schema (Paper 29), and the chronology/information constraints developed in Papers 37–38, we define a record filtration (the record fragment available by time t) and a corresponding family of stage world-types. We prove: (1) Arrow as refinement: if the record fragment grows monotonically, later stages refine earlier with canonical forgetful maps; strict growth yields strict refinement. (2) No-overwrite: any dynamics step that flips a stable record forces non-categoricity (multiple world-types) and hence selection. (3) Irreversibility: once refinement is strict, there is no globally invertible "time-reversal" preserving record semantics at all stages without branching/selection. (4) Selection barrier for retrodiction: under diagonal capability (), selecting among consistent pasts cannot be total-effective internally. The development is mechanized in Lean 4 as the ArrowOfTime library in nems-lean, with zero sorry and no custom axioms. Time travel (Paper 37) and black hole information (Paper 38) appear as direct corollaries. Trust boundary. Arrow, no-overwrite, and retrodiction-barrier claims assume the record filtration and Closure inputs stated in the formalization; chronology and black-hole corollaries inherit Papers 37–38 premise bundles. Mechanization is nems-lean. See.
Nova Spivack (Sun,) studied this question.