#!/usr/bin/env python3
"""Exact rational check of a finite simple regular graph's strict spectral bound.

This implements the contrast-space test described in family 178. It does not
implement the paper's construction, independently check the theorem or certify
the Python program formally. Bounded inputs avoid unplanned large computations.
"""
import argparse
import json
from fractions import Fraction
from pathlib import Path


def audit(adjacency):
    if not isinstance(adjacency,list) or not 4<=len(adjacency)<=64:
        raise ValueError('Supply an adjacency list for 4 to 64 vertices')
    n=len(adjacency)
    for i,row in enumerate(adjacency):
        if not isinstance(row,list) or not all(type(v) is int and 0<=v<n for v in row):
            raise ValueError('Neighbors must be valid integer vertex labels')
        if len(row)!=len(set(row)) or i in row:raise ValueError('Require a simple loopless graph')
    neighbors=[set(row) for row in adjacency]
    degree=len(neighbors[0])
    if degree<3 or any(len(row)!=degree for row in neighbors):raise ValueError('Require regular degree at least three')
    if any(i not in neighbors[j] for i,row in enumerate(neighbors) for j in row):raise ValueError('Adjacency must be symmetric')
    threshold_squared=4*(degree-1)
    # A^2_ij counts common neighbors. Form Q=B^T(threshold*I-A^2)B
    # for B=[e_0-e_(n-1),...,e_(n-2)-e_(n-1)]. No approximate eigensolve.
    matrix=[[threshold_squared*(i==j)-len(neighbors[i]&neighbors[j]) for j in range(n)] for i in range(n)]
    q=[[matrix[i][j]-matrix[i][-1]-matrix[-1][j]+matrix[-1][-1] for j in range(n-1)] for i in range(n-1)]
    size=n-1
    lower=[[Fraction(0) for _ in range(size)] for _ in range(size)]
    pivots=[]
    passed=True
    for i in range(size):
        diagonal=Fraction(q[i][i])-sum(lower[i][k]*lower[i][k]*pivots[k] for k in range(i))
        pivots.append(diagonal)
        if diagonal<=0:
            passed=False;break
        lower[i][i]=1
        for j in range(i+1,size):
            lower[j][i]=(Fraction(q[j][i])-sum(lower[j][k]*lower[i][k]*pivots[k] for k in range(i)))/diagonal
    return dict(vertices=n,degree=degree,strict_nonconstant_squared_eigenvalue_bound=threshold_squared,
                strict_ramanujan_test_passed=passed,
                contrast_ldl_pivots=[dict(numerator=str(p.numerator),denominator=str(p.denominator)) for p in pivots],
                arithmetic='exact_python_integer_and_fraction',
                interpretation='Positive contrast form is equivalent to every nonconstant adjacency eigenvalue having square less than 4(d-1).',
                new_graph_construction=False,independent_theorem_verification='not_run',formal_program_verification='not_run',
                source_url='https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Deterministic-nonbipartite-Ramanujan-graphs-in-every-fixed-degree-September-23-2026/paper.pdf')


def main():
    parser=argparse.ArgumentParser(description=__doc__)
    parser.add_argument('input',type=Path,help='JSON object with adjacency list')
    parser.add_argument('--output',type=Path)
    args=parser.parse_args();body=json.dumps(audit(json.loads(args.input.read_text())['adjacency']),indent=2)+'\n'
    if args.output:
        with args.output.open('x') as stream:stream.write(body)
    else:print(body,end='')


if __name__=='__main__':main()