Why it is a question
THEORY-884 states Proposition 4’s criterion and bound, and the record has proved both. The authors call the result “a finite-machine refinement construction in the tradition of Moore and Nerode” (LIT-1376, §4.4), and THEORY-884’s body repeats that. No classical source is read here.
What would answer it
A reading of Moore (1956) or Nerode (1958), or of a standard automata text, that identifies Proposition 4 as the minimal-machine construction (Myhill–Nerode, Moore partition refinement) applied to the target family {T_d ∘ J_u}, with its hypotheses: a finite state set closed under total deterministic revisions, and a state that includes any law needed to make revision Markovian. A classical statement that needs stronger hypotheses than these would answer it in part.