"""Check Lemma 5.4's regular-coordinate construction in exact rank-one algebra. Check all matrix units at two body representatives, changes of section, the odd-degree bounds, and rejection of the former parameter-free construction. """ from math import factorial import sympy as sp from grass import G, mzero, meye, mmul, madd, msub PARITY = [0, 1, 0, 1] # RB, RF, AB, AF IDENTITY = meye(4) def scale_left(scalar, matrix): return [[scalar * value for value in row] for row in matrix] def numeric(matrix): return [[G.c(matrix[i, j]) for j in range(4)] for i in range(4)] def conjugate(matrix, left, right): return mmul(mmul(left, matrix), right) def project(matrix, part): result = mzero(4) for i in range(4): for j in range(4): block = ('k' if i // 2 == j // 2 else 'm0' if PARITY[i] == PARITY[j] else 'm1') if block == part: result[i][j] = matrix[i][j] return result def exponential(matrix): # There are at most six odd generators, and every entry has zero body. result, power = meye(4), meye(4) for n in range(1, 7): power = mmul(power, matrix) result = madd(result, scale_left(sp.Rational(1, factorial(n)), power)) assert_zero(mmul(power, matrix), 'exponential terminates') return result def assert_zero(matrix, label): for i, row in enumerate(matrix): for j, value in enumerate(row): for monomial, coefficient in value.d.items(): assert sp.simplify(coefficient) == 0, ( label, i, j, monomial, coefficient) def solve(theta, rhs): minus_theta = scale_left(-1, theta) exp_theta, exp_minus_theta = exponential(theta), exponential(minus_theta) def linear_map(matrix): ordinary = conjugate(project(matrix, 'm0'), exp_minus_theta, exp_theta) odd, commutator = mzero(4), project(matrix, 'm1') for n in range(5): odd = madd(odd, scale_left(sp.Rational((-1) ** n, factorial(n + 1)), commutator)) commutator = msub(mmul(theta, commutator), mmul(commutator, theta)) assert_zero(commutator, 'adjoint series terminates') return madd(madd(ordinary, odd), project(matrix, 'k')) # The correction to the identity raises degree in the four regular generators. solution, term = mzero(4), rhs for _ in range(5): solution = madd(solution, term) term = msub(term, linear_map(term)) assert_zero(term, 'Neumann series terminates') assert_zero(msub(linear_map(solution), rhs), 'parameterized decomposition') return tuple(project(solution, part) for part in ['m0', 'm1', 'k']) def variations(g, theta, source): rhs = conjugate(source, numeric(g.inv()), numeric(g)) rhs = conjugate(rhs, exponential(scale_left(-1, theta)), exponential(theta)) return solve(theta, rhs) def check_factorization(g, theta, source, changes): u, v, c = changes lhs = mmul(mmul(madd(IDENTITY, source), numeric(g)), exponential(theta)) rhs = mmul(mmul(mmul(numeric(g), madd(IDENTITY, u)), exponential(madd(theta, v))), madd(IDENTITY, c)) assert_zero(msub(lhs, rhs), 'group factorization') lam = numeric(sp.diag(1, 1, -1, -1)) q = conjugate(conjugate(lam, exponential(theta), exponential(scale_left(-1, theta))), numeric(g), numeric(g.inv())) shifted_q = conjugate(lam, exponential(madd(theta, v)), exponential(scale_left(-1, madd(theta, v)))) shifted_q = conjugate(shifted_q, madd(IDENTITY, u), msub(IDENTITY, u)) shifted_q = conjugate(shifted_q, numeric(g), numeric(g.inv())) required = conjugate(q, madd(IDENTITY, source), msub(IDENTITY, source)) assert_zero(msub(shifted_q, required), 'defining action on Q') theta = mzero(4) for a, (i, j) in enumerate([(0, 3), (1, 2), (2, 1), (3, 0)], 1): theta[i][j] = G.gen(a) g0 = sp.eye(4) g1 = sp.Matrix([[sp.Rational(5, 3), 0, sp.Rational(4, 3), 0], [0, sp.Rational(3, 5), 0, sp.Rational(4, 5)], [sp.Rational(4, 3), 0, sp.Rational(5, 3), 0], [0, -sp.Rational(4, 5), 0, sp.Rational(3, 5)]]) real_form_metric = sp.diag(1, 1, -1, 1) assert g1.conjugate().T * real_form_metric * g1 == real_form_metric section = sp.diag(1, sp.I, -1, -sp.I) rotated_theta = conjugate(theta, numeric(section.inv()), numeric(section)) checked, sections = 0, 0 for g in [g0, g1]: for i in range(4): for j in range(4): parity = (PARITY[i] + PARITY[j]) % 2 # Model the even first-order parameter by two fresh odd generators. eta = G.gen(5) if parity else G.gen(5) * G.gen(6) source = mzero(4) source[i][j] = eta changes = variations(g, theta, source) check_factorization(g, theta, source, changes) checked += 1 if parity: a, theta1, _ = ([[x.dleft(5) for x in row] for row in matrix] for matrix in changes) y = mzero(4) y[i][j] = G.c(1) leading = project(conjugate(y, numeric(g.inv()), numeric(g)), 'm1') residual = msub(theta1, leading) for row in a: for value in row: assert all(len(m) >= 1 and len(m) % 2 == 1 for m in value.d) for row in residual: for value in row: assert all(len(m) >= 2 and len(m) % 2 == 0 for m in value.d) if g == g1: rotated = variations(g * section, rotated_theta, source) for actual, original in zip(rotated, changes): expected = conjugate(original, numeric(section.inv()), numeric(section)) assert_zero(msub(actual, expected), 'section equivariance') sections += 1 # The original counterexample must distinguish the repaired construction. chi, eta = G.gen(1), G.gen(5) small_theta, y = mzero(4), mzero(4) small_theta[0][3], y[3][2] = chi, G.c(1) source = scale_left(eta, y) corrected = variations(g0, small_theta, source) expected_u = mzero(4) expected_u[0][2] = eta * chi assert_zero(msub(corrected[0], expected_u), 'counterexample corrected sign') old_rhs = conjugate(y, exponential(scale_left(-1, small_theta)), exponential(small_theta)) old_changes = tuple(scale_left(eta, part) for part in solve(small_theta, old_rhs)) try: check_factorization(g0, small_theta, source, old_changes) except AssertionError: print('ok: former parameter-free construction rejected by the counterexample') else: raise AssertionError('negative control failed to detect the former sign error') check_factorization(g0, small_theta, source, corrected) print(f'passed {checked} generator-point pairs: exact factorization and action on Q') print(f'passed {sections} changes of section and all odd leading-degree checks')