From aa4afaff6211267088634abc1b233a552ce15bec Mon Sep 17 00:00:00 2001 From: ywz65 <154373401+ywz65@users.noreply.github.com> Date: Thu, 15 Oct 2026 06:51:31 -0700 Subject: [PATCH] Prove exact Dn coordinate pairing spectrum --- .../dn-coordinate-pairing-spectrum/README.md | 151 ++++++++++ .../RESULT.json | 138 +++++++++ .../SOURCES.json | 50 ++++ .../dn-coordinate-pairing-spectrum/TASK.json | 102 +++++++ .../VERIFY.json | 31 +++ .../test_boundary.py | 57 ++++ .../dn-coordinate-pairing-spectrum/verify.py | 261 ++++++++++++++++++ 7 files changed, 790 insertions(+) create mode 100644 research/dn-coordinate-pairing-spectrum/README.md create mode 100644 research/dn-coordinate-pairing-spectrum/RESULT.json create mode 100644 research/dn-coordinate-pairing-spectrum/SOURCES.json create mode 100644 research/dn-coordinate-pairing-spectrum/TASK.json create mode 100644 research/dn-coordinate-pairing-spectrum/VERIFY.json create mode 100644 research/dn-coordinate-pairing-spectrum/test_boundary.py create mode 100644 research/dn-coordinate-pairing-spectrum/verify.py diff --git a/research/dn-coordinate-pairing-spectrum/README.md b/research/dn-coordinate-pairing-spectrum/README.md new file mode 100644 index 0000000000..3b32e14f3e --- /dev/null +++ b/research/dn-coordinate-pairing-spectrum/README.md @@ -0,0 +1,151 @@ +# Exact pairing spectrum for every standard-coordinate D_n puncture + +For any subset of the projective roots `2e_i +/- 2e_j` of `D_n`, with its +**fixed standard-coordinate Gram decoder**, the minimum COPY cost over every +admissible binary pairing is twice the number of represented coordinate edges. +This includes asymmetric pairings. Consequently no such puncture has cost below +its number of root lines. A puncture ties exactly when it is a union of complete +opposite-sign pairs. + +This answers the pairing-minimization handoff in Aaron Wang's +[PR 2272](https://github.com/CrocSwap/integer-mult-bounds/pull/2272), Open next +questions item 2, retained by +[PR 2518](https://github.com/CrocSwap/integer-mult-bounds/pull/2518). +All 1,023 previously observed D5 ties remain optimal over **all** admissible B. +The new result is the arbitrary-pairing theorem and exact cost distribution; +the B0 puncture counts and original root model belong to those predecessors +and DreamingOfClouds's +[PR 2125](https://github.com/CrocSwap/integer-mult-bounds/pull/2125). + +## Model and theorem + +Let `n >= 2`, and choose any nonempty subset S of the `n(n-1)` root lines, +represented once by `2e_i+2e_j` and `2e_i-2e_j` for `i> i & 1]) for support in masks + if (block := support & live)) + + +def admissible(rs, rows): + size = len(rs) + need(len(rows) == size, 'pairing shape') + for i, row in enumerate(rows): + need(type(row) is int and 0 <= row < 1 << size, 'pairing binary shape') + need(row >> i & 1, 'pairing diagonal') + for j, r in enumerate(rs): + need(i == j or not (row >> j & 1) or dot(rs[i], r) == 0, + 'pairing forced zero') + + +def geometry(rs): + edges = [frozenset(i for i, x in enumerate(r) if x) for r in rs] + counts = Counter(edges) + e = len(counts) + m = sum(v == 2 for v in counts.values()) + d = sum(not a & b for a, b in combinations(edges, 2)) + return e, m, d, edges + + +def predicted(rs, rows): + e, m, d, edges = geometry(rs) + bad = sum(edges[i] == edges[j] and + not ((rows[i] >> j & 1) and (rows[j] >> i & 1)) + for i, j in combinations(range(len(rs)), 2)) + return 2*e+2*bad + + +def relevant_census(n, independent=False): + """7 states/edge; disjoint-edge entries are zero representatives.""" + rs = roots(n) + masks = supports(rs) + edge_count = len(rs)//2 + hist = {} + symmetric = {} + checked = 0 + # (live signs, forward mate bit, reverse mate bit) + states = ((0, 0, 0), (1, 0, 0), (2, 0, 0), + (3, 1, 1), (3, 0, 0), (3, 0, 1), (3, 1, 0)) + for word in product(range(7), repeat=edge_count): + live, e, m, bad = 0, 0, 0, 0 + rows = [1 << i for i in range(len(rs))] + sym = True + for t, state in enumerate(word): + occupied, a, b = states[state] + live |= occupied << (2*t) + e += bool(occupied) + m += occupied == 3 + bad += occupied == 3 and not (a and b) + rows[2*t] |= a << (2*t+1) + rows[2*t+1] |= b << (2*t) + sym &= a == b + if not live: + continue + actual = price(rows, masks, live) + need(actual == 2*e+2*bad, 'relevant cost mismatch') + if independent: + need(price(rows, masks, live, span_rank) == actual, 'row-span mismatch') + hist.setdefault(live, Counter())[actual] += 1 + if sym: + symmetric.setdefault(live, Counter())[actual] += 1 + checked += 1 + for live, costs in hist.items(): + occupancy = [(live >> (2*t)) & 3 for t in range(edge_count)] + e, m = sum(bool(x) for x in occupancy), occupancy.count(3) + need(dict(costs) == {2*e+2*k: comb(m, k)*3**k for k in range(m+1)}, + 'directed polynomial mismatch') + need(dict(symmetric[live]) == {2*e+2*k: comb(m, k) for k in range(m+1)}, + 'symmetric polynomial mismatch') + need(checked == 7**edge_count-1 and len(hist) == 4**edge_count-1, + 'census domain mismatch') + return {'n': n, 'punctures': len(hist), 'relevant_pairings': checked, + 'symmetric_relevant_pairings': sum(sum(x.values()) for x in symmetric.values()), + 'independent_row_span': independent} + + +def d5_punctures(): + rs = roots(5) + masks = supports(rs) + rows = [sum(1 << j for j, b in enumerate(rs) if i == j or dot(a, b) == 0) + for i, a in enumerate(rs)] + admissible(rs, rows) + lookup = [] + for support in masks: + indices = [i for i in range(20) if support >> i & 1] + table = {} + for local in range(1 << len(indices)): + live = sum(1 << i for bit, i in enumerate(indices) if local >> bit & 1) + selected = [row & live for i, row in enumerate(rows) if live >> i & 1] + value = rank(selected) + need(value == span_rank(selected), 'D5 independent subblock rank') + table[live] = value + lookup.append(table) + even = sum(1 << (2*t) for t in range(10)) + hist = Counter() + for live in range(1, 1 << 20): + actual = sum(table[live & support] for table, support in zip(lookup, masks)) + edges = ((live | (live >> 1)) & even).bit_count() + single = ((live ^ (live >> 1)) & even).bit_count() + need(actual == 2*edges and actual-live.bit_count() == single, + 'D5 puncture minimum mismatch') + hist[actual-live.bit_count()] += 1 + expected = {j: 2**10*comb(10, j)-(j == 0) for j in range(11)} + need(dict(hist) == expected, 'D5 puncture histogram') + return {'punctures': sum(hist.values()), 'ties': hist[0], + 'minimum_minus_v_histogram': dict(sorted(hist.items())), + 'direct_subblock_ranks': sum(len(t) for t in lookup), + 'roots_sha256': sha256(json.dumps(rs, separators=(',', ':')).encode()).hexdigest()} + + +def random_pairings(): + rng = Random(2026101513) + checked = 0 + for n in range(2, 11): + all_roots = roots(n) + for trial in range(40): + rs = [r for r in all_roots if trial == 0 or rng.randrange(4)] + if not rs: + rs = all_roots[:1] + rows = [sum(1 << j for j, b in enumerate(rs) + if i == j or (dot(a, b) == 0 and rng.randrange(2))) + for i, a in enumerate(rs)] + admissible(rs, rows) + need(price(rows, supports(rs), (1 << len(rs))-1) == predicted(rs, rows), + 'arbitrary directed pairing mismatch') + checked += 1 + return checked + + +def controls(): + rs = roots(3) + all_ones = [(1 << len(rs))-1] * len(rs) + need(price(all_ones, supports(rs), (1 << len(rs))-1) == 3 < len(rs), + 'inadmissible gain control') + try: + admissible(rs, all_ones) + except ValueError as exc: + need(str(exc) == 'pairing forced zero', 'wrong inadmissibility control') + else: + raise ValueError('nonorthogonal pairing accepted') + try: + admissible(roots(2), [0, 2]) + except ValueError as exc: + need(str(exc) == 'pairing diagonal', 'wrong diagonal control') + else: + raise ValueError('zero diagonal accepted') + mate_costs = [] + for a, b in product(range(2), repeat=2): + rows = [1 | a << 1, 2 | b] + admissible(roots(2), rows) + mate_costs.append(price(rows, supports(roots(2)), 3)) + need(mate_costs == [4, 4, 4, 2], 'directed mate control') + # Same singleton Gram [8]; changed factor supports p=(1,0), q=(8,0). + need(dot((2, 2), (2, 2)) == dot((1, 0), (8, 0)) == 8, + 'basis boundary identity') + standard = price([1], [1, 1], 1) + changed = rank([1]) + rank([]) + need((standard, changed) == (2, 1), 'fixed-basis boundary control') + return {'invalid_forced_zero_rejected': True, 'invalid_diagonal_rejected': True, + 'directed_mate_costs_00_01_10_11': mate_costs, + 'same_singleton_gram_standard_changed_costs': [standard, changed]} + + +def compute(): + full = {} + for n in range(2, 11): + rs = roots(n) + e, m, d, _ = geometry(rs) + need(d == 12*comb(n, 4), 'disjoint-root count') + full[n] = {'v': len(rs), 'minimum': 2*e, 'complete_pairs': m, + 'disjoint_root_pairs': d, 'directed_optimizers': 2**(2*d), + 'symmetric_optimizers': 2**d, 'tied_punctures': 2**e-1} + return {'schema_version': 1, 'scope': 'fixed standard D_n coordinate Gram decoder', + 'formula': 'cost=2e+2k; directed polynomial=2^(2d)*z^(2e)*(1+3z^2)^m', + 'relevant_censuses': [relevant_census(3, True), relevant_census(4)], + 'd5': d5_punctures(), 'directed_sample_cases': random_pairings(), + 'full_families': full, 'controls': controls()} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--out', type=Path) + args = parser.parse_args() + result = compute() + encoded = json.dumps(result, indent=2, sort_keys=True)+'\n' + if args.out: + with args.out.open('x', encoding='utf-8', newline='\n') as output: + output.write(encoded) + else: + need(json.loads((HERE/'RESULT.json').read_text()) == json.loads(encoded), + 'complete receipt mismatch') + print('PASS_DN_PAIRING_SPECTRUM D4_relevant_pairings=117648 D5_punctures=1048575 ties=1023') + + +if __name__ == '__main__': + main()