#!/usr/bin/env python3
"""
Independent reproduction of the constant-weight-code (Johnson) upper bound on
A(2k,4,k) and the resulting chromatic lower bound for J(2k,k).

A(n,4,w) <= C_w exactly (our (k-1)-covering bound), but the recursive Johnson
bound can be strictly smaller, certifying A(2k,4,k) < C_k for many k and hence
chi(J(2k,k)) >= ceil(binom(2k,k)/bound) > k+1  =>  835(k) NO.

Recursion (as formalised in formal-conjectures 835.lean):
  jb(0,d,w)=1;  jb(n,d,0)=1;
  jb(n, d, w) = 1 if 2w<d else floor( n*jb(n-1,d,w-1)/w ).
"""
from math import comb
from functools import lru_cache
import json

@lru_cache(maxsize=None)
def jb(n,d,w):
    if n==0 or w==0: return 1
    if 2*w < d: return 1
    return (n*jb(n-1,d,w-1))//w

def catalan(k): return comb(2*k,k)//(k+1)
def is_prime(n):
    if n<2: return False
    if n%2==0: return n==2
    d=3
    while d*d<=n:
        if n%d==0: return False
        d+=2
    return True

rows=[]; decided=[]; undecided=[]
for k in range(3, 61):
    N=comb(2*k,k); Ck=catalan(k)
    bound=jb(2*k,4,k)              # Johnson upper bound on A(2k,4,k)
    bound=min(bound,Ck)           # never exceed the exact covering bound
    lb=-(-N//bound)               # ceil(N/bound) <= chi
    ok_no = lb > k+1              # bound alone proves 835(k) NO
    rows.append({"k":k,"k+1":k+1,"kplus1_prime":is_prime(k+1),
                 "A_le":bound,"Catalan_Ck":Ck,"chi_lower":lb,
                 "settled_NO_by_bound":ok_no})
    (decided if ok_no else undecided).append(k)

print("k  k+1 prime?  A(2k,4,k)<=   C_k        chi>=   NO-by-bound")
for r in rows:
    print(f"{r['k']:2d}  {r['k+1']:3d}  {str(r['kplus1_prime']):5s}  {r['A_le']:>12d}  {r['Catalan_Ck']:>12d}  {r['chi_lower']:>4d}   {r['settled_NO_by_bound']}")
print()
print("Settled NO by the Johnson bound alone (3<=k<=60):")
print(" ", decided)
print("NOT settled by this elementary bound (need Steiner/large-set/better codes):")
print(" ", undecided, " -> k+1 =", [k+1 for k in undecided], "all prime:", all(is_prime(k+1) for k in undecided))
json.dump(rows, open("johnson_bound_table.json","w"), indent=1)
print("\nWrote johnson_bound_table.json")