"""Brute-force checks for Erdős #552 / #85 from the definitions (no Lean involved).

R(n) = R(C4, K_{1,n}): least m such that every graph on m vertices has a C4 or a vertex with
>= n non-neighbours. f85(n): least k such that every graph on n vertices with minimum degree >= k
contains a C4. All graphs on up to 7 vertices come from the NetworkX graph atlas (complete up to
isomorphism). Small and cheap: about 1,250 graphs.
"""
import itertools
import networkx as nx

ATLAS = [g for g in nx.graph_atlas_g() if g.number_of_nodes() >= 1]
BY_N = {m: [g for g in ATLAS if g.number_of_nodes() == m] for m in range(1, 8)}
OEIS = {1: 4, 2: 4, 3: 6, 4: 7, 5: 8, 6: 9, 7: 11, 8: 12}   # A006672, terms 1..8

def has_c4(g):
    # a C4 exists iff two distinct vertices have two distinct common neighbours
    for u, v in itertools.combinations(g.nodes, 2):
        if len(set(g[u]) & set(g[v])) >= 2:
            return True
    return False

C4FREE = {m: [g for g in BY_N[m] if not has_c4(g)] for m in BY_N}

def max_nonnbrs_min(g):
    # largest number of non-neighbours of any vertex
    m = g.number_of_nodes()
    return max(m - 1 - d for _, d in g.degree)

def in_set(m, n):
    """Every graph on m vertices has a C4 or a vertex with >= n non-neighbours."""
    return all(max_nonnbrs_min(g) >= n for g in C4FREE[m])

def R(n):
    for m in range(1, 8):
        if in_set(m, n):
            return m
    return None   # beyond the atlas

def f85(n):
    for k in range(0, n + 1):
        if all(has_c4(g) for g in BY_N[n] if min(d for _, d in g.degree) >= k):
            return k

Rv = {n: R(n) for n in range(1, 6)}
print('R(C4,K1n) brute force:', Rv, '| OEIS:', OEIS)
assert all(Rv[n] == OEIS[n] for n in Rv if Rv[n] is not None), 'mismatch with OEIS'
known = {n: v for n, v in Rv.items() if v is not None}
print('Chen R(n+1) <= R(n)+2:', all(known[n + 1] <= known[n] + 2 for n in known if n + 1 in known))
print('R(n) >= n+2 (n>=1):', all(v >= n + 2 for n, v in known.items()))
print('2n+2 in the set (n=1..2, m<=7):', all(in_set(2 * n + 2, n) for n in (1, 2)))
# Erdős #85: website formula vs corrected formula, using OEIS values of R where the atlas stops
Rall = {**OEIS, **known}
for n in range(4, 8):
    true_f = f85(n)
    site = next((m for m in range(1, n + 1) if n - m >= 1 and m >= Rall[n - m]), None)
    fixed = next((k for k in range(1, n) if Rall[n - k] <= n), None)
    print(f'f85({n}) brute force = {true_f} | site formula min{{m: m >= R(n-m)}} -> {site} | '
          f'corrected min{{k: R(n-k) <= n}} -> {fixed}')