verify-peripheral-projection.py

#!/usr/bin/env python3
"""Exact algebra certificates. No triangulations or slopes are enumerated.

The integral classification uses GHHR's theorem and is proved in the note.
This program does not purport to verify that external theorem, convergence,
or independent-cusp symmetry of actual normal indices.
"""
from collections import defaultdict
from fractions import Fraction
from pathlib import Path
import json


# Ordered basis s,l,t,u; all powers below are powers of A.
zero = (0, 0, 0, 0)
s, l, t, u = [tuple(int(i == j) for i in range(4)) for j in range(4)]


def add(a, b):
    return tuple(x + y for x, y in zip(a, b))


def neg(a):
    return tuple(-x for x in a)


def scale(n, a):
    return tuple(n * x for x in a)


def omega(a, b):
    return 2 * sum(a[j] * b[j + 1] - a[j + 1] * b[j]
                   for j in (0, 2))


# Quantum torus polynomial: (boundary vector, A-power) -> rational coefficient.
def E(a):
    return {(a, 0): Fraction(1)}


def plus(*polys):
    out = defaultdict(Fraction)
    for p in polys:
        for k, c in p.items():
            out[k] += c
    return {k: c for k, c in out.items() if c}


def times(p, q):
    out = defaultdict(Fraction)
    for (a, i), x in p.items():
        for (b, j), y in q.items():
            out[(add(a, b), i + j + omega(a, b) // 2)] += x * y
    return {k: c for k, c in out.items() if c}


def sigma(p):
    return {(neg(a), i): c for (a, i), c in p.items()}


def scalar(c, p):
    return {k: c * v for k, v in p.items() if c * v}


def C(a):
    return plus(E(a), E(neg(a)))


def D(a):
    return plus(E(a), scalar(-1, E(neg(a))))


def a_power(n, p):
    return {(a, i + n): c for (a, i), c in p.items()}


checks = []


def check(name, predicate):
    assert predicate, name
    checks.append(name)


# Exact noncommuting word, not a commuting approximation.
word = times(times(C(t), C(u)), C(add(t, scale(2, u))))
check('noncommuting word retained', times(C(t), C(u)) != times(C(u), C(t)))
check('inversion fixes the whole word', sigma(word) == word)
check('inversion preserves product order',
      sigma(times(E(t), E(u))) == times(sigma(E(t)), sigma(E(u))))
check('inversion does not invert A',
      sigma(times(E(t), E(u))) == a_power(1, E(neg(add(t, u)))))
check('C-times-C product-to-sum',
      times(C(t), C(u)) == plus(a_power(1, C(add(t, u))),
                                a_power(-1, C(add(t, neg(u))))))

mixed = plus(word, a_power(3, D(t)), scalar(Fraction(2, 3), D(add(t, u))))
odd = scalar(Fraction(1, 2), plus(mixed, scalar(-1, sigma(mixed))))
even = scalar(Fraction(1, 2), plus(mixed, sigma(mixed)))
check('exact even/odd decomposition', plus(odd, even) == mixed)
check('odd projector squares to itself',
      scalar(Fraction(1, 2), plus(odd, scalar(-1, sigma(odd)))) == odd)
check('even component fixed', sigma(even) == even)

# Theorem 2.1 uses integral coordinate differences, not integral half-vectors.
raw = (3, 1, -1)
half = tuple(Fraction(x, 2) for x in raw)
normal = tuple(max(half) - x for x in half)
check('half-integral raw lift gives integral normal representative',
      normal == (0, 1, 2) and all(x.denominator == 1 for x in normal))
check('doubled tetrahedron coefficient is integral',
      tuple(2 * x + r for x, r in zip(normal, raw)) == (3, 3, 3))

def index_coefficients(epsilon):
    out = {zero: {0: 1}}
    if epsilon:
        for x in (add(t, neg(l)), add(neg(t), l)):
            out[x] = {4: epsilon}
    return out


def laurent_sum(*polys):
    out = defaultdict(Fraction)
    for p in polys:
        for degree, coefficient in p.items():
            out[degree] += coefficient
    return {d: c for d, c in out.items() if c}


def weighted_fiber(Z, gamma, r):
    """All n are handled exactly by solving support equations, no cutoff."""
    out = []
    for beta, value in Z.items():
        # beta = -gamma - r*l - n*s.
        residual = add(add(beta, gamma), scale(r, l))
        if any(residual[j] for j in (1, 2, 3)):
            continue
        n = -residual[0]
        out.append({degree + r * n: ((-1) ** (n % 2)) * c
                    for degree, c in value.items()})
    return laurent_sum(*out)


def vacuum(Z, gamma):
    # B(E_gamma)/c_l = H(gamma,-1)-H(gamma,1).
    return laurent_sum(weighted_fiber(Z, gamma, -1),
                       {d: -c for d, c in weighted_fiber(Z, gamma, 1).items()})


def functional(Z, p):
    terms = []
    for (gamma, power), coefficient in p.items():
        terms.append({d + power: coefficient * c
                      for d, c in vacuum(Z, gamma).items()})
    return laurent_sum(*terms)


# Intrinsic parity constraints: the two given vectors span a Lagrangian in F2^4.
k1 = add(t, l)
k2 = add(s, u)
check('parity kernel generators independent',
      k1 != zero and k2 != zero and k1 != k2)
check('parity kernel isotropic over F2', (omega(k1, k2) // 2) % 2 == 0)
Z0, Z1 = index_coefficients(0), index_coefficients(1)
for name, Z in [('zero-odd-model', Z0), ('nonzero-odd-model', Z1)]:
    check(name + ': simultaneous inversion',
          all(Z.get(neg(gamma), {}) == c for gamma, c in Z.items()))
    check(name + ': allowed parity support',
          all(tuple(x % 2 for x in gamma) in (zero, k1, k2, add(k1, k2))
              for gamma in Z))
    check(name + ': exact unit normalization', weighted_fiber(Z, zero, 0) == {0: 1})
    check(name + ': balanced vacuum zero', vacuum(Z, zero) == {})
    check(name + ': native insertion antisymmetry',
          vacuum(Z, neg(t)) == {d: -c for d, c in vacuum(Z, t).items()})
    check(name + ': noncommuting skein word invisible', functional(Z, word) == {})
    check(name + ': functional factors through odd projector',
          functional(Z, mixed) == functional(Z, odd))
check('constraints permit zero oriented value', vacuum(Z0, t) == {})
check('constraints permit nonzero oriented value', vacuum(Z1, t) == {4: 1})
check('oriented differences double the value', functional(Z1, D(t)) == {4: 2})

result = {
    'status': 'passed', 'check_count': len(checks), 'checks': checks,
    'formal_countermodels': {'Z0: B(E_t)/c_l': '0', 'Z1: B(E_t)/c_l': 'A^4'},
    'scope': 'Exact quantum torus algebra and formal boundary witnesses only. '
             'No topological input is enumerated. These witnesses are not actual normal indices.',
    'proof_only_dependencies': ['GHHR integral normal-homology theorem',
                                'retained all-input convergence',
                                'retained native named-action dictionary',
                                'GHHR simultaneous boundary inversion']
}
Path(__file__).with_name('exact-results.json').write_text(json.dumps(result, indent=2) + '\n')
print(json.dumps(result, indent=2))