There is nothing left to add because m_2 is already the correct value:

- If m is also < p, then (m_1 - m_2) is obviously 0, and so will be h.

- If m >= p, then m must be of the form m_1 + k * p for some k. But we've already established that m = m_2, so m_1 - m_2 = (m - k * p) - m_2 = -k * p = 0 mod p. Thus h = 0.

So regardless of the value of qinv, we get m verbatim if it's less than q. d_p and d_q are d mod (p-1) and d mod (q-1) respectively.

Here, this Sage script is short enough that it all fits in a comment. I guess 624 bits and recover the remaining 400 with Coppersmith; this is fast enough to run in a few seconds.

    def oracle(c, d, p, q, qinv):
        m_1 = power_mod(c, d % (p-1), p)
        m_2 = power_mod(c, d % (q-1), q)
        h = (m_1 - m_2)*qinv % p
        m = m_2 + h * m_1
        return (m >> (211*8)) != 0 # check if sid != 0

    # Setup
    p = random_prime(2^1024, lbound=2^1023+2^1022)
    q = random_prime(2^1024, lbound=2^1023+2^1022)
    n = p*q
    e = 65537
    d = inverse_mod(e, (p-1)*(q-1))
    qinv = inverse_mod(q, p) + randint(0, 2^128) # random error block inserted in the least significant 128 bits

    msb_q = 0
    for bit in reversed(range(400, 1024)):
        # if m < q, we are within range
        if not oracle(power_mod(msb_q + 2^bit, e, n), d, p, q, qinv):
            msb_q += 2^bit

    # Find a small root of msb_q  + x modulo a divisor of n of size ~n^(1/2)
    P.<x> = Zmod(n)[]
    f = msb_q + x
    [lsb_q] = f.small_roots(beta=0.49, epsilon=1/32)
    # Check we've reached the correct solution
    assert(q == msb_q + lsb_q)

Right, but my question is, why is it the correct value? There's some math theorem which makes it true?

m_2 = c^d_q mod q

    = m^(e * d_q) mod q

    = m because?

That's just how RSA works, via Fermat's little theorem: e * d_q mod (q-1) = 1, so m^(e * d_q) mod q = m^1 mod q = m.

Got it, thank you!