#!/usr/bin/env python3
"""Exact core certificates, permanent tail, and conditional capacity arithmetic.

Python 3.10+, standard library only. No assertions, floating point, external
data, or numerical eigensolver. The low-degree absolute-minor coefficients
are supplied here, not recomputed. The companion orbit/minor checker and
retained geometric verifiers compute them separately. This is not an exact
maximum-fiber calculation or a practical speed claim.
"""
from hashlib import sha256
from itertools import combinations, permutations, product
from math import gcd
from pathlib import Path
import json

Q=339949771344778
D=25000000000000000
H=4948372000
PIN='40bc6a1d52efab3d75cf343e65ac06b314f9c9c375fc02bf6d45bf6bb21f9529'

def require(ok, message):
    if not ok:
        raise ArithmeticError(message)

def graph():
    vertices=set()
    for i in range(4):
        for s in (-1,1):
            v=[(0,0)]*4
            v[i]=(2*s,0)
            vertices.add(tuple(v))
    for signs in product((-1,1),repeat=4):
        vertices.add(tuple((s,0) for s in signs))
    even=[p for p in permutations(range(4))
          if sum(p[i]>p[j] for i in range(4)
                 for j in range(i+1,4))%2==0]
    for a,b,c in product((-1,1),repeat=3):
        v=((0,0),(a,0),(0,b),(-c,c))
        vertices.update(tuple(v[i] for i in p) for p in even)
    vertices=sorted(vertices)
    neighbors=[[] for _ in vertices]
    for i,j in combinations(range(len(vertices)),2):
        x=y=0
        for (a,b),(c,d) in zip(vertices[i],vertices[j]):
            u,v=a-c,b-d
            x+=u*u+v*v
            y+=2*u*v+v*v
        if (x,y)==(8,-4):
            neighbors[i].append(j)
            neighbors[j].append(i)
    fixture={
        'coordinate_rule':
            'vertex coordinate is (a+b*phi)/2 for pair [a,b]',
        'neighbors':neighbors,
        'schema':'OMEGA_600CELL_GRAPH_FIXTURE/1',
        'vertex_order':
            'Python lexicographic order of tuples of four integer pairs',
        'vertices':vertices}
    raw=(json.dumps(fixture,sort_keys=True,separators=(',',':'))+'\n').encode()
    require(sha256(raw).hexdigest()==PIN,'graph identity')
    require(len(vertices)==120 and all(len(v)==12 for v in neighbors),
            'dimension and degree')
    return neighbors

def bareiss_positive(a):
    a=[list(row) for row in a]
    n=len(a)
    previous=1
    minors=[]
    for k in range(n):
        pivot=a[k][k]
        require(pivot>0,'positive leading determinant')
        minors.append(pivot)
        for i in range(k+1,n):
            for j in range(k+1,n):
                num=a[i][j]*pivot-a[i][k]*a[k][j]
                value,remainder=divmod(num,previous)
                require(remainder==0,'exact Bareiss division')
                a[i][j]=value
            a[i][k]=0
        previous=pivot
    return minors

def multiply_M(a,neighbors):
    return [[13*a[i][k]+sum(a[j][k] for j in neighbors[i])
             for k in range(120)] for i in range(120)]

def polynomial_product(a,b):
    c=[0]*(len(a)+len(b)-1)
    for i,x in enumerate(a):
        for j,y in enumerate(b):
            c[i+j]+=x*y
    return c

def permanent_coefficients(matrix):
    """All rectangular minor permanent sums by descending-mask updates."""
    m=len(matrix)
    require(m>0 and all(len(row)==len(matrix[0]) for row in matrix),
            'rectangular matching matrix')
    require(all(type(x) is int and x>=0 for row in matrix for x in row),
            'nonnegative integer matching weights')
    dp=[1]+[0]*((1<<m)-1)
    for j in range(len(matrix[0])):
        nz=[(1<<i,matrix[i][j]) for i in range(m) if matrix[i][j]]
        for mask in range((1<<m)-1,-1,-1):
            value=dp[mask]
            if value:
                for bit,weight in nz:
                    if not mask&bit:
                        dp[mask|bit]+=value*weight
    coeff=[0]*(m+1)
    for mask,value in enumerate(dp):
        coeff[mask.bit_count()]+=value
    return coeff

def verify():
    neighbors=graph()
    M=[[13 if i==j else int(j in neighbors[i])
        for j in range(120)] for i in range(120)]
    positive=bareiss_positive([
        [M[i][j]-9*int(i==j) for j in range(120)]
        for i in range(120)])
    determinant=bareiss_positive(M)[-1]
    delta=2**80*5**27*11**36*13**25*41**9*211**4
    require(determinant==delta,'exact determinant')
    f=[1]
    for factor in ([[-r,1] for r in (10,11,13,16,25)]
                   +[[211,-32,1],[205,-30,1]]):
        f=polynomial_product(f,factor)
    require(f[0]==-5*H,'annihilator constant')
    g=[[f[-1]*int(i==j) for j in range(120)]
       for i in range(120)]
    for coefficient in reversed(f[1:-1]):
        g=multiply_M(g,neighbors)
        for i in range(120):
            g[i][i]+=coefficient
    mg=multiply_M(g,neighbors)
    require(all(mg[i][j]==5*H*int(i==j)
                for i in range(120) for j in range(120)),
            'annihilating polynomial identity')
    require(all(v%5==0 for row in g for v in row),'integer inverse numerator')
    N=[[v//5 for v in row] for row in g]
    mn=multiply_M(N,neighbors)
    require(all(mn[i][j]==H*int(i==j)
                for i in range(120) for j in range(120)),
            'exact inverse identity')
    norm=max(sum(abs(v) for v in row) for row in N)
    require(norm==801320608 and 73*norm<12*H,'inverse interval width')
    require(73*Q<D<74*Q and 80*Q>D,'quantization inequalities')
    require(8**120==2**360,'modulo-eight capacity')
    require(2**430<12**120<2**431,'modulo-twelve capacity')
    require(0<gcd(Q*H,D)<=D-73*Q<Q,'phase hypotheses')
    require(2**306*delta<74**120<2**307*delta,'averaging thresholds')
    W=[0]+list(range(33,45))
    require(sorted([0]+neighbors[0])==W,'closed neighborhood W')
    permanent=permanent_coefficients([M[i] for i in W])
    require(permanent[8:]==[
        82326531807696,879734614473680,6510322192690880,
        31533042290406720,89385221732384160,111664804452677280],
        'recomputed permanent tail')
    supplied_a=[1,325,45408,3647440,188983720,6697090056,
                167581390636,3007006391716]
    L7=sum(a*73**(13-r) for r,a in enumerate(supplied_a))
    U=L7+sum(permanent[r]*73**(13-r) for r in range(8,14))
    require(L7==57869157529977646724169246,'partial volume assembly')
    require(U==58067516542393048415542654,'upper volume assembly')
    require(U**120<(2**352*delta)**13,'352-bit threshold arithmetic')
    require(L7**120>(2**351*delta)**13,'same-cover 351-bit obstruction')
    return {
        'schema':'OMEGA_PAPER_IX_CORE_CERTIFICATE/1','status':'PASS',
        'graph_sha256':PIN,'dimension':120,'degree':12,
        'M_minus_9I_positive_leading_minors':len(positive),
        'positive_leading_determinants':[str(v) for v in positive],
        'inverse_denominator':H,'inverse_row_norm_numerator':norm,
        'determinant_M':str(delta),'witness_bits':360,
        'recomputed_permanent_coefficients':permanent,
        'supplied_absolute_minor_coefficients_not_recomputed':supplied_a,
        'partial_volume_L7':str(L7),'upper_volume_U':str(U),
        'threshold_352_arithmetic_passes':True,
        'same_cover_351_obstruction_arithmetic_passes':True,
        'global_cover_checked_by_this_script':False,
        'low_degree_coefficients_recomputed_by_this_script':False,
        'source_sha256':sha256(Path(__file__).read_bytes()).hexdigest()}

if __name__=='__main__':
    print(json.dumps(verify(),indent=2,sort_keys=True))