Refinement Flow of World-Types: Time as Growth of Stable Distinguishability Paper 41 of the NEMS Suite

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' → 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 .