#!/usr/bin/env python3
"""RIGOR MORTIS · Public finite-check reproducer v1.
Python >= 3.9, standard library only. No network, no participant data.
Finite examples test particular claims: they are NOT universal proofs or
independent expert adjudication of the 111 proof autopsy labels.
"""
from math import floor, gcd, comb, factorial
from fractions import Fraction

def check_imo_2019_p5():
    states = 0
    for n in range(1, 10):
        total = 0
        def V(m):
            k = m.bit_count()
            s = sum(i+1 for i in range(n) if m & (1 << i))
            return 2*s-k*k
        for bits in range(1 << n):
            states += 1
            x = bits
            steps = 0
            expected = V(x)
            while x:
                k = x.bit_count()
                x2 = x ^ (1 << (k-1))
                assert V(x2) == V(x)-1
                x = x2
                steps += 1
                assert steps <= n*n
            assert steps == expected
            total += steps
        assert 4*total == n*(n+1)*(1 << n)
    assert states == 1022
    print("PASS IMO 2019 P5: 1,022 finite coin configurations")

def check_imo_2024_p6():
    xs = {Fraction(k,d) for d in range(1,8) for k in range(-14,15)}
    assert len(xs) == 135
    def f(x):
        return 2*floor(x)-x
    pairs = 0
    for x in xs:
        for y in xs:
            assert f(x+f(y))==f(x)+y or f(f(x)+y)==x+f(y)
            pairs += 1
    assert pairs == 18225
    assert {f(x)+f(-x) for x in xs} == {0,-2}
    print("PASS IMO 2024 P6: 18,225 exact rational pairs")

def check_polynomials_and_gcd():
    ds=(1,2,3,5,7,11)
    polynomials=((1,1,1),(4,-3,5,2),(2,-5,1))
    counts=0
    for n in range(-200,201):
        for d in ds:
            for coef in polynomials:
                def P(x):
                    return sum(c*x**i for i,c in enumerate(coef))
                assert (P(n+d)-P(n))%d==0
                counts += 1
        assert gcd(n*n+n+1,(n+1)*(n+1)+(n+1)+1)==1
    assert counts == 7218
    print("PASS IMO 2006 P5: 7,218 polynomial pairs")
    print("PASS IMO 2016 P4: 401 adjacent-gcd identities")

def check_lagrange():
    for n in range(1,10):
        w=[(-1)**(n-i)*comb(n,i) for i in range(n+1)]
        for a in range(n):
            assert sum(w[i]*i**a for i in range(n+1))==0
        assert sum(w[i]*i**n for i in range(n+1))==factorial(n)
    print("PASS IMO 2007 P6: 9 exact binomial-weight moment families")

if __name__ == "__main__":
    check_imo_2019_p5()
    check_imo_2024_p6()
    check_polynomials_and_gcd()
    check_lagrange()
    print("ALL FINITE CHECKS PASS; THIS IS NOT A FORMAL PROOF.")