"""Independent check of the first-escape counts, written by the verifier from the paper alone.

Different arithmetic from both of the bundle's methods: base-10 interval arithmetic with the
standard library's decimal module, 90 significant digits, lower ends rounded toward -inf and
upper ends toward +inf. z_0 = 0, z_{n+1} = z_n^2 + c_T, c_T = 1/4 + 1/(16 (T+1)^2).
First escape: the least n with z_n > 2, certified when the lower end exceeds 2 while every
earlier upper end is at most 2. Also checks C1's bound z_n <= 17/32 for n <= T.
"""
import json
from decimal import Context, Decimal, ROUND_CEILING, ROUND_FLOOR
from fractions import Fraction

DIGITS = 90
DOWN = Context(prec=DIGITS, rounding=ROUND_FLOOR)
UP = Context(prec=DIGITS, rounding=ROUND_CEILING)
TWO = Decimal(2)
BOUND = Decimal(17) / Decimal(32)  # exact in decimal: 0.53125


def enclose(q):
    return DOWN.divide(Decimal(q.numerator), Decimal(q.denominator)), UP.divide(Decimal(q.numerator), Decimal(q.denominator))


def first_escape(cutoff):
    c = Fraction(1, 4) + Fraction(1, 16 * (cutoff + 1) ** 2)
    c_lo, c_hi = enclose(c)
    lo = hi = Decimal(0)
    n = 0
    limit = 32 * (cutoff + 1) ** 2 + 1
    while n < limit:
        prev_hi = hi
        lo = DOWN.add(DOWN.multiply(lo, lo), c_lo)
        hi = UP.add(UP.multiply(hi, hi), c_hi)
        n += 1
        if n <= cutoff and not (lo >= 0 and hi <= BOUND):
            raise AssertionError(f"C1 bound not certified at T={cutoff}, n={n}")
        if lo > TWO:
            assert prev_hi <= TWO
            return n, limit
        if hi > TWO:
            raise ArithmeticError(f"undecided at T={cutoff}, n={n}")
    raise ArithmeticError("no escape within the analytic bound")


def floats(cutoff):
    c = 0.25 + 1.0 / (16 * (cutoff + 1) ** 2)
    z, n = 0.0, 0
    while z <= 2:
        z = z * z + c
        n += 1
    return n


cutoffs = [1, 4, 16, 64, 256, 1024, 4096]
rows = []
for t in cutoffs:
    n, limit = first_escape(t)
    rows.append({"cutoff": t, "first_escape": n, "analytic_limit": limit, "float64_first_escape": floats(t)})
out = {"digits": DIGITS, "escape_iterations": [r["first_escape"] for r in rows], "rows": rows}
print(json.dumps(out, indent=2))
