Exact rational checker for the finite comparisons

The following optional code checks only the arithmetic comparisons in Lemma lem:arithmetic. It is not a checker for the external entropy inequalities, coding theorem, or manuscript. Every stored number is rational. No successful execution is asserted.

from fractions import Fraction as F

ZERO = F(0) ONE = F(1)

def L(z, n): return sum((z**k / F(2*k + 1) for k in range(n)), ZERO)

def T(z, n): return z**n / (F(2*n + 1) * (ONE-z))

def J(z, n): return sum( (z**k / F(2*k*(2*k-1)) for k in range(1, n+1)), ZERO )

def R(z, n): return z**(n+1) / ( F((2*n+2)*(2*n+1)) * (ONE-z) )

def x(p): return F(3,4)-p

def d(p): return p-F(1,4)

def q(p): return F(5,8)-d(p)**2

N = 32 a = F(469,1000) b = F(47,100) p0 = F(939,2000)

def D_lower(p): xx = x(p) dd = d(p) zz = q(p) assert xx > 0 and dd > 0 assert 0 <= xx**2 < 1 and 0 <= zz < 1 return xx*L(xx**2,N)-dd*(L(zz,N)+T(zz,N))

def D_upper(p): xx = x(p) dd = d(p) zz = q(p) return xx*(L(xx**2,N)+T(xx**2,N))-dd*L(zz,N)

assert D_lower(a) > F(1,1000) assert D_upper(b) < -F(1,10000) assert F(0) < D_lower(p0) assert D_lower(p0) <= D_upper(p0) < F(1,1000)

ell_lower = F(2,3)*L(F(1,9),12) ell_upper = ell_lower + F(2,3)*T(F(1,9),12)

x0sq = F(314721,4000000) q0 = F(2307279,4000000)

assert x(p0) == F(561,2000) assert x(p0)**2 == x0sq assert q(p0) == q0

A_lower = J(q0,N)-J(x0sq,N)-R(x0sq,N) A_upper = J(q0,N)+R(q0,N)-J(x0sq,N)

assert A_lower > 0 assert ell_lower > F(1,2)

# These are the two cleared-denominator value checks. assert 10**6*A_lower - 412377*ell_upper > 0 assert ( 412378*ell_lower - 10**6*(A_upper+F(1,2000000)) ) > 0

Lcert = A_lower/ell_upper Ucert = (A_upper+F(1,2000000))/ell_lower

assert F(412377,10**6) < Lcert < Ucert < F(412378,10**6)

# Independent output-matrix determinant check. population = F(1439,4000) coherence_squared = F(996279,8000000) determinant = population*(1-population)-coherence_squared

assert determinant == F(1692721,16000000) assert 1-4*determinant == q0

The arithmetic cost is explicitly finite: fixed sums of at most 32 terms and fixed rational powers, followed by rational comparisons. No efficiency theorem for arbitrary channel inputs or exact closed-form maximizers is claimed.