#!/usr/bin/env python3 """Exact small-matrix check for the five-pattern integral-packing theorem. The proof in the manuscript is structural. This independent computation lists the possible nonempty basic remainders with at most five columns. Only Python's standard library is used. """ from __future__ import annotations from collections import Counter from fractions import Fraction from itertools import combinations, combinations_with_replacement, permutations, product import json from typing import Sequence def rref(matrix: Sequence[Sequence[int | Fraction]], columns: int): """Reduced row echelon form, pivoting in the first `columns` columns.""" a = [[Fraction(x) for x in row] for row in matrix] if any(len(row) < columns for row in a): raise ValueError('Too few columns') pivots = [] for col in range(columns): row = next((i for i in range(len(pivots), len(a)) if a[i][col]), None) if row is None: continue p = len(pivots) a[p], a[row] = a[row], a[p] scale = a[p][col] a[p] = [x / scale for x in a[p]] for i in range(len(a)): if i != p and a[i][col]: scale = a[i][col] a[i] = [x - scale * y for x, y in zip(a[i], a[p])] pivots.append(col) return a, pivots def nullspace(matrix, columns: int): reduced, pivots = rref(matrix, columns) basis = [] for col in range(columns): if col in pivots: continue vector = [Fraction(0)] * columns vector[col] = Fraction(1) for row, pivot in enumerate(pivots): vector[pivot] = -reduced[row][col] basis.append(vector) return basis def canonical(triples, t: int): """Minimize over all row orders within equal row-sum classes.""" degrees = Counter(u for triple in triples for u in triple) groups = [[u for u in range(t) if degrees[u] == d] for d in sorted(set(degrees.values()))] best = None for choices in product(*(permutations(group) for group in groups)): order = tuple(u for group in choices for u in group) relabel = {u: i for i, u in enumerate(order)} key = tuple(sorted(tuple(sorted(relabel[u] for u in triple)) for triple in triples)) if best is None or key < best: best = key return best def column_sets(t: int, k: int): """List distinct columns with overlap at most one and row sums at least two.""" triples = list(combinations_with_replacement(range(t), 3)) vectors = [tuple(triple.count(u) for u in range(t)) for triple in triples] compatible = [sum(1 << j for j in range(i + 1, len(vectors)) if sum(min(x, y) for x, y in zip(vectors[i], vectors[j])) <= 1) for i in range(len(vectors))] def visit(chosen, candidates, sums): if len(chosen) == k: if min(sums) >= 2: yield tuple(triples[i] for i in chosen) return while candidates: bit = candidates & -candidates candidates ^= bit i = bit.bit_length() - 1 needed = k - len(chosen) - 1 if candidates.bit_count() < needed: break updated = tuple(x + y for x, y in zip(sums, vectors[i])) if sum(max(0, 2 - x) for x in updated) > 3 * needed: continue yield from visit(chosen + (i,), candidates & compatible[i], updated) yield from visit((), (1 << len(triples)) - 1, (0,) * t) def check_case(t: int, k: int): classes = Counter(canonical(triples, t) for triples in column_sets(t, k)) counts = Counter() decompositions = [] for triples in sorted(classes): matrix = [[triple.count(u) for triple in triples] for u in range(t)] _, pivots = rref(matrix, k) if len(pivots) < k: counts['rank_deficient'] += 1 continue basis = nullspace(list(zip(*matrix)), t) if any(all(b[u] == b[v] for b in basis) for u, v in combinations(range(t), 2)): counts['forced_equal_values'] += 1 continue counts['distinct_values_possible'] += 1 degrees = [sum(row) for row in matrix] for residual in product(*(range(1, d) for d in degrees)): if sum(residual) % 3: continue augmented = [row + [b] for row, b in zip(matrix, residual)] reduced, pivots = rref(augmented, k) if any(not any(row[:k]) and row[k] for row in reduced): continue coefficient = [reduced[j][k] for j in range(k)] if not all(0 < x < 1 for x in coefficient): continue counts['strict_integer_remainders'] += 1 # All zero triples common to the complete left nullspace. zero = [] for triple in combinations_with_replacement(range(t), 3): vector = tuple(triple.count(u) for u in range(t)) if (all(x <= r for x, r in zip(vector, residual)) and all(sum(b[u] for u in triple) == 0 for b in basis)): zero.append(vector) def partition(left): if not any(left): return () u = next(i for i, n in enumerate(left) if n) for vector in zero: if vector[u] and all(x <= r for x, r in zip(vector, left)): tail = partition(tuple(r - x for r, x in zip(left, vector))) if tail is not None: return (vector,) + tail return None packing = partition(residual) if packing is None: raise AssertionError('A remainder lacks a common zero-sum partition') assert all(sum(vector) == 3 for vector in packing) assert all(sum(vector[u] for vector in packing) == residual[u] for u in range(t)) decompositions.append({ 'columns': triples, 'residual': residual, 'coefficients': [str(x) for x in coefficient], 'zero_sum_partition': packing, }) return {'types': t, 'columns': k, 'labelled_column_sets': sum(classes.values()), 'row_column_classes': len(classes), 'counts': dict(counts), 'decompositions': decompositions} def main(): if not __debug__: raise RuntimeError('Run without -O: assertion checks are required') result = [check_case(t, k) for t, k in [(5, 4), (6, 4), (6, 5)]] expected = [(895, 14, 1), (240, 3, 1), (32616, 70, 0)] for row, (labelled, classes, remainders) in zip(result, expected): assert row['labelled_column_sets'] == labelled assert row['row_column_classes'] == classes assert row['counts'].get('strict_integer_remainders', 0) == remainders print(json.dumps({'cases': result}, indent=2)) if __name__ == '__main__': main()