Paper 36 showed that stable records force an arrow of time at the level of semantics: record filtration, stage world-types, and forgetful maps from later to earlier stages. This paper reframes that development as a refinement flow: the primitive evolution is not "state evolves" but equivalence classes of observational indistinguishability refine as records accumulate. We extend the ArrowOfTime library with iterated forget maps (ₜ' t), prove their coherence (agreement with the quotient at the earlier stage) and naturality (composition of forgets along a chain), and give a toy witness (two-bit world). The development is mechanized in Lean 4 as the RefinementFlow library in nems-lean, building on ArrowOfTime, with zero sorry and no custom axioms. Trust boundary. Refinement-flow lemmas extend Paper 36's record-filtration formalism; the two-bit toy is illustrative only. Mechanization is nems-lean. See.
Nova Spivack (2026) studied this question.