#!/usr/bin/env python3
"""Focused second review of OMEGA Synthesis 1.0; Python 3.9+, stdlib.

An independent Farey-neighbor certificate establishes the first floor-map
disagreement without calling the supplied floor_sum implementation.
Rational intervals certify the noninteger Sacks counterexample. Checks
remain active under -O and -OO. This is arithmetic plus written mathematics,
not a proof-assistant kernel certificate or a decoder integration audit.
"""
from fractions import Fraction as R
from math import isqrt


def require(condition, message):
    if not condition:
        raise ValueError(message)


def atan_box(denominator, terms=64):
    power = denominator
    partial = R(0)
    for k in range(terms):
        partial += R((-1)**k, (2*k+1)*power)
        power *= denominator*denominator
    adjacent = partial + R((-1)**terms, (2*terms+1)*power)
    return min(partial, adjacent), max(partial, adjacent)


def root_box(n):
    scale = 10**60
    root = isqrt(n*scale*scale)
    require(root*root < n*scale*scale < (root+1)**2, "strict root enclosure")
    return R(root, scale), R(root+1, scale)


def sine_box(x, terms=24):
    require(0 < x < 1, "monotone small-angle domain")
    term, partial = x, R(0)
    for i in range(terms):
        partial += term
        term *= -x*x / ((2*i+2)*(2*i+3))
    return min(partial, partial+term), max(partial, partial+term)


def decimal_bound(x, upward=False, digits=12):
    scale = 10**digits
    shifted = x*scale
    n = -((-shifted.numerator)//shifted.denominator) if upward else shifted.numerator//shifted.denominator
    sign = "-" if n < 0 else ""
    n = abs(n)
    return sign + str(n//scale) + "." + str(n % scale).zfill(digits)


def main():
    Q, S = 339949771344778, 10**15
    q = R(Q, S)
    alo, ahi = atan_box(5)
    blo, bhi = atan_box(239)
    pi_lo, pi_hi = 16*alo-4*bhi, 16*ahi-4*blo
    root_lo, root_hi = root_box(5)
    phi_lo, phi_hi = (1+root_lo)/2, (1+root_hi)/2
    lam_lo, lam_hi = phi_lo/(phi_lo+pi_hi), phi_hi/(phi_hi+pi_lo)
    published_lo = R(339949771344778929576702809321, 10**30)
    published_hi = R(339949771344778929576702809322, 10**30)
    require(q < published_lo < lam_lo < lam_hi < published_hi, "lambda enclosure")

    # If a/b < r/s < c/d and bc-ad=1, the positive integers
    # x=cs-dr and y=br-as obey s=bx+dy >= b+d.
    # Hence no rational strictly between these neighbors has denominator
    # below b+d. Any floor mismatch at a positive input s would supply
    # such a rational r/s between q and lambda.
    a, b, c, d = 846547, 2490212, 13495616, 39698853
    require(b*c-a*d == 1, "unimodular neighbor determinant")
    require(R(a,b) < q < published_lo < published_hi < R(c,d), "bracketing neighbors")
    numerator, denominator = a+c, b+d
    require((numerator,denominator) == (14342163,42189065), "boundary mediant")
    require(q < R(numerator,denominator) < published_lo, "mismatch witness")
    require((published_lo*denominator).__floor__() == (published_hi*denominator).__floor__() == numerator,
            "lambda floor at boundary")
    require(Q*denominator//S == numerator-1, "rational floor at boundary")
    print("PASS independent Farey boundary: first disagreement =", denominator)
    print("Neighbor certificate:", str(R(a,b)), str(R(c,d)), "determinant = 1")

    # At m=1, k=5/2: r=sqrt(11)/2, t=2, epsilon=2-r.
    # Actual Y=r*sin(2*pi*r)=-r*sin(pi*(sqrt(11)-3)).
    # The printed finite-error RHS is H-r*sin(2*pi*epsilon)=H+Y,
    # while its LHS is H-Y. Their difference is -2Y>0.
    r11lo, r11hi = root_box(11)
    angle_lo, angle_hi = pi_lo*(r11lo-3), pi_hi*(r11hi-3)
    sin_lo = sine_box(angle_lo)[0]
    sin_hi = sine_box(angle_hi)[1]
    amplitude_lo, amplitude_hi = r11lo*sin_lo/2, r11hi*sin_hi/2
    require(0 < amplitude_lo <= amplitude_hi, "strict Sacks discrepancy")
    print("PASS Sacks real-parameter counterexample: m=1, k=5/2")
    print("Y enclosed by", decimal_bound(-amplitude_hi), decimal_bound(-amplitude_lo, upward=True))
    print("Printed LHS minus RHS enclosed by", decimal_bound(2*amplitude_lo),
          decimal_bound(2*amplitude_hi, upward=True))

    scale, residue, byte = R(1,2), 0, 255
    quotient = (256*residue+byte)//scale
    require(0 <= residue < scale and quotient == 510, "real-scale digit counterexample")
    print("PASS missing streaming domain: s=1/2, r=0, b=255 gives q=510")
    # Correct integer claim: 256*r+b <= 256*(s-1)+255=256*s-1.
    cases = 0
    for s in (1,2,3,7,256,32768,10**15):
        for r in set((0,s//2,s-1)):
            for byte in (0,1,127,255):
                quotient, remainder = divmod(256*r+byte,s)
                require(0 <= quotient < 256 and 0 <= remainder < s, "integer byte division")
                cases += 1
    print("PASS corrected integer streaming examples:", cases)
    print("ALL FOCUSED CLAIM CHECKS PASS")


if __name__ == "__main__":
    main()