Optional exact-arithmetic checker

The following optional Python code independently reconstructs the kernel and inspects all sixteen truth tables. It uses rational arithmetic and integer square roots only. It is not needed as a premise of the printed proof. No execution is asserted.

from fractions import Fraction as F from itertools import product from math import isqrt

vertices = [(1,1), (1,-1), (-1,1), (-1,-1)] rho = F(1,2) Q = 100000

def kernel(x, y): out = F(1) for xi, yi in zip(x, y): out *= (1 + rho*xi*yi)/2 return out

K = [[kernel(x,y) for y in vertices] for x in vertices] expected = [ [9,3,3,1], [3,9,1,3], [3,1,9,3], [1,3,3,9] ] assert K == [[F(a,16) for a in row] for row in expected] assert all(sum(row, F(0)) == 1 for row in K) assert all(sum(K[i][j] for i in range(4)) == 1 for j in range(4))

def noise(f): return tuple( sum((K[y][x]*f[x] for x in range(4)), F(0)) for y in range(4) )

def sqrt_interval(z): assert z >= 0 A = z.numerator * Q*Q B = z.denominator a = isqrt(A // B) assert a*a*B <= A < (a+1)*(a+1)*B return F(a,Q), F(a+1,Q)

def H_interval(t): return sqrt_interval(1-t*t)

coord = set() for i in range(2): for sign in (-1,1): coord.add(tuple(sign*x[i] for x in vertices))

assert len(coord) == 4 assert noise((1,1,-1,-1)) == ( F(1,2),F(1,2),-F(1,2),-F(1,2) ) assert noise((1,-1,-1,1)) == ( F(1,4),-F(1,4),-F(1,4),F(1,4) ) assert noise((-1,1,1,1)) == ( -F(1,8),F(5,8),F(5,8),F(7,8) )

slo, shi = H_interval(rho) counts = "constant":0, "coordinate":0, "parity":0, "exceptional":0

for f in product((-1,1), repeat=4): m = F(sum(f),4) d = noise(f)

if f in coord: counts["coordinate"] += 1 assert m == 0 assert all(abs(v) == rho for v in d) continue

if abs(m) == 1: counts["constant"] += 1 elif m == 0: counts["parity"] += 1 else: counts["exceptional"] += 1

hlo, hhi = H_interval(m) intervals = [H_interval(v) for v in d] blo = sum((a for a,b in intervals), F(0))/4 bhi = sum((b for a,b in intervals), F(0))/4

gap_lower = (1-shi)-hhi+blo gap_upper = (1-slo)-hlo+bhi

assert gap_lower > F(27,1000) if m == 0: assert gap_lower > F(102,1000) assert gap_upper < F(103,1000) if abs(m) == F(1,2): assert gap_upper < F(28,1000)

assert counts == "constant":2, "coordinate":4, "parity":2, "exceptional":8

root_rows = [ (3,173205,173206,27975,318436), (7,264575,264576,69375,459776), (15,387298,387299,259196,515401), (39,624499,624500,998999,250000) ] for k,a,b,left,right in root_rows: assert k*Q*Q-a*a == left > 0 assert b*b-k*Q*Q == right > 0

The integer-root routine is sound because

implies $a/Q\le \sqrt{z}<(a+1)/Q$. The checker covers a finite list of sixteen objects. It makes no assertion about all dimensions.