#!/usr/bin/env python3
"""Exact coefficient comparison for the website/paper assessment, 2026-10-27.

Standard library only. No floats, assertions, or dependency on the paper's
checker. This certifies the stated finite parameter domain, not a whole-site
proof audit. Run: python network_parameter_audit.py
"""
from fractions import Fraction as F
from math import isqrt
import json

Q = 339949771344778
S = 10**15
H = 32767
Z = 25 * H


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


def atan_sum(n, terms):
    return sum((F((-1)**k, (2*k+1)*n**(2*k+1))
                for k in range(terms)), F(0))


def factor_bounds():
    base = 10**30
    root = isqrt(5*base*base)
    require(root*root < 5*base*base < (root+1)**2, 'sqrt bracket')
    pl, pu = F(base+root, 2*base), F(base+root+1, 2*base)
    pi_l = 16*atan_sum(5, 18)-4*atan_sum(239, 9)
    pi_u = 16*atan_sum(5, 19)-4*atan_sum(239, 8)
    require(F(3) < pi_l < pi_u < F(22, 7), 'pi ordering')
    lo, hi = pl/(pl+pi_u), pu/(pu+pi_l)
    require(F(Q, S) < lo < hi < F(Q+1, S), 'factor bracket')
    return lo, hi


def main():
    q = F(Q, S)
    profiles = {
        'minimum_modulus': F(4196, 12343),
        'signed32_horizon': F(49136, 144539),
        'baseline_horizon': F(846547, 2490212),
        'first_dyadic': F(22813643, 2**26),
        'globally_reduced': F(Q//2, S//2),
    }
    lo_lam, hi_lam = factor_bounds()
    lower, upper = F(0), F(1)
    lower_at, upper_at = 0, 0
    first = {name: None for name in profiles}
    for z in range(1, Z+1):
        t = Q*z//(25*S)
        ln, un = 25*t, 25*(t+1)
        if ln*lower.denominator > lower.numerator*z:
            lower, lower_at = F(ln, z), z
        if un*upper.denominator < upper.numerator*z:
            upper, upper_at = F(un, z), z
        require(t*25*lo_lam.denominator <= lo_lam.numerator*z,
                'lambda floor lower')
        require(hi_lam.numerator*z < (t+1)*25*hi_lam.denominator,
                'lambda floor upper')
        for name, p in profiles.items():
            if first[name] is None:
                candidate = p.numerator*z//(25*p.denominator)
                if candidate != t:
                    first[name] = {'z': z, 'canonical_output': t,
                                   'candidate_output': candidate}
    require(lower == F(211975, 623548), 'network lower endpoint')
    require(upper == F(268150, 788793), 'network upper endpoint')
    require(upper-lower == F(25, 491850297564), 'network interval width')
    require(lower <= q < upper, 'canonical factor in interval')
    require(lower < lo_lam < hi_lam < upper, 'ideal factor in interval')
    require(lower_at == 623548 and upper_at == 788793, 'active constraints')
    scalar_lower, scalar_upper = F(0), F(1)
    for d in range(1, H+1):
        t = Q*d//S
        scalar_lower = max(scalar_lower, F(t, d))
        scalar_upper = min(scalar_upper, F(t+1, d))
        for p in profiles.values():
            require(p.numerator*d//p.denominator == t,
                    'website scalar agreement')
    require((scalar_lower, scalar_upper) == (F(4196, 12343), F(7039, 20706)),
            'scalar interval')
    require(scalar_lower < lower < upper < scalar_upper, 'strict interval inclusion')
    require(first['minimum_modulus'] ==
            {'z': 127813, 'canonical_output': 1738, 'candidate_output': 1737},
            'minimum modulus counterexample')
    require(first['first_dyadic'] ==
            {'z': 165245, 'canonical_output': 2246, 'candidate_output': 2247},
            'dyadic counterexample')
    for name in ('signed32_horizon', 'baseline_horizon', 'globally_reduced'):
        require(first[name] is None and lower <= profiles[name] < upper,
                'preserving profile')
    # Every local integer is attainable on the canonical cube: center j gives
    # [13*j, 13*j+12*H], and these integer intervals overlap without gaps.
    require(12*H+1 >= 13 and 13*H+12*H == Z, 'attainable local-sum cover')
    witnesses = {
        'minimum_modulus': [H, H, H, 29512],
        'first_dyadic': [H, H, H, H, H, 1410],
    }
    for name, neighbors in witnesses.items():
        require(len(neighbors) <= 12 and all(0 <= a <= H for a in neighbors),
                'canonical neighbor values')
        require(sum(neighbors) == first[name]['z'], 'explicit local input')
    report = {
        'date': '2026-10-27',
        'canonical_Q': Q, 'canonical_S': S,
        'scalar_states_checked': H+1,
        'local_integer_cases_certified': Z+1,
        'scalar_parameter_interval': [str(scalar_lower), str(scalar_upper)],
        'network_parameter_interval': [str(lower), str(upper)],
        'interval_convention': 'left closed, right open',
        'network_interval_width': str(upper-lower),
        'active_network_constraints': [lower_at, upper_at],
        'actual_lambda_floor_agreement': True,
        'profiles': {name: {'factor': str(p), 'first_local_disagreement': first[name]}
                     for name, p in profiles.items()},
        'explicit_inputs': {'center': 0, 'neighbors': witnesses,
                            'other_neighbors_and_vertices': 0},
        'status': 'PASS',
    }
    print(json.dumps(report, indent=2))


if __name__ == '__main__':
    main()