Memoryless concretization relation

The paper’s Theorem 4 (that MCR implies the memoryless concretization property) matches the model’s Part (a) and is proved correctly in the PDF. However, for Theorem 5 (necessity), the paper’s proof uses the MCR-interface IMCR_R inside a contraposition argument where it can be empty when R is not MCR, which breaks the construction; the text explicitly selects u1 ∈ IMCR_R(x1,x2,u2), an element that need not exist under the negated premise (see the proof block for Theorem 5 in the PDF). The correct necessity proof must use the ASR-interface IASR_R (guaranteed nonempty by S1 ⪯ASR_R S2), exactly as in the candidate solution’s Part (b). Thus, the statement is right but the paper’s proof is flawed/incomplete, while the model’s proof is sound. See Theorem 4, Property 2, and the printed proof of Theorem 5 in the PDF for context and the error locus .