"""SymPy and numerical checks of the elementary estimates used in Sections 3 and 4: the monotonicity of
x/sqrt(log x) and x/(log x)^a, the arithmetic of the constant eps_0 and of the exponent in Theorem 4.9,
the comparison showing that the length form of ETH fails for C < 1/2, the bound s <= 6km + k^2 used for
Theorem 3.10, and the counts of clause splitting.
Usage: python check_asymptotics.py   (requires SymPy)
"""
import sympy as sp
x,a,L,c0,b0,C,q=sp.symbols('x a L c0 b0 C q',positive=True)
lg=lambda t: sp.log(t,2)
# monotonicity of x/sqrt(log x): derivative sign
d=sp.simplify(sp.diff(x/sp.sqrt(lg(x)),x)*lg(x)**sp.Rational(3,2))
print("d/dx[x/sqrt(log x)]*(log x)^1.5 =",d, " zero at x=",sp.nsolve(d,x,1.5))
# N/(log N)^a increasing iff log2 N >= a/ln2
d2=sp.simplify(sp.diff(x/lg(x)**a,x)*lg(x)**(a+1)); print("d/dx[x/(log x)^a]*(log x)^(a+1) =",d2)
# eps0 arithmetic
eps0=1/(q*2**(q+2)); R=sp.symbols('R',positive=True)
print("2eps0 - (R/2)/(q2^qR) =",sp.simplify(2*eps0-(R/2)/(q*2**q*R)))
# constacc consequence: exponent N/(log N)^(C+b0+1) at N=c0 L (log L)^b0, upper bounded using log N >= log L
NL=c0*L*lg(L)**b0
ub=c0*L/lg(L)**(C+1)
import math
for (cc0,bb0,CC) in [(1e3,3,0.6),(1e6,5,1.0),(10,1,0.51)]:
    # find L where c0 L/(log L)^(C+1) + 10*log2(L) < L/(log L)^C  (poly(L)=L^10)
    lo=4.0
    for e in range(2,400):
        LL=2.0**e
        if cc0*LL/math.log2(LL)**(CC+1)+10*math.log2(LL) < LL/math.log2(LL)**CC: print("c0,b0,C=",cc0,bb0,CC," holds from log2 L ~",e); break
# exact check ex: actual exponent <= ub numerically
for (cc0,bb0,CC,e) in [(1e3,3,0.6,40),(1e6,5,1.0,100)]:
    LL=2.0**e; N=cc0*LL*e**bb0
    print("N/(logN)^(C+b0+1) <= c0L/(logL)^(C+1):", N/math.log2(N)**(CC+bb0+1) <= cc0*LL/e**(CC+1))
# hyp:leneth: 3C1 L/sqrt(log L) vs L/(log L)^C for C<1/2: ratio
C1=sp.symbols('C1',positive=True)
print("ratio (3C1/sqrt(log L))/(1/(log L)^C) =",sp.simplify((3*C1/sp.sqrt(lg(L)))*lg(L)**C))
# moderate: s=max(4km, m+1, k^2) <= 6km + k^2 for k,m>=1 ; spot check
import itertools
ok=all(max(4*k*m,m+1,k*k)<=6*k*m+k*k for k in range(1,40) for m in range(1,200)); print("s<=6km+k^2:",ok)
# splitting: clauses sum max(1,w-2)<=sum w ; vars occ + sum max(0,w-3) <= 2L
ok=True
import random
for _ in range(2000):
    ws=[random.randint(1,12) for _ in range(random.randint(1,30))]; Lc=sum(ws)
    if sum(max(1,w-2) for w in ws)>Lc or Lc+sum(max(0,w-3) for w in ws)>2*Lc: ok=False
print("splitting counts:",ok)