diff --git a/research/r439-four-omission-boundary/CERTIFICATE.json b/research/r439-four-omission-boundary/CERTIFICATE.json new file mode 100644 index 0000000000..92b3259733 --- /dev/null +++ b/research/r439-four-omission-boundary/CERTIFICATE.json @@ -0,0 +1,55 @@ +{ + "columns": 661, + "controls": { + "dense_neutral_counts": [ + 21, + 16, + 13, + 10, + 21, + 16, + 13, + 10 + ], + "dense_orderings": 8, + "dense_quartets": 47880, + "literal_deletion_subsets": 128, + "malformed_factor_rejections": 4, + "orientation_chronology_dirty_controls": 5, + "positive_rank_strata": 2 + }, + "distinct_covectors": 761, + "distinct_image_vectors": 530, + "dual_partition": { + "distinct_covectors": 530, + "distinct_image_vectors": 761, + "factors": 5563, + "image_planes": 289016, + "neutral_four_rank_one": 0, + "neutral_four_rank_two": 0, + "neutral_four_total": 0, + "neutral_triples": 0, + "pair_count": 15470703, + "peak_rank_two_plane_pairs": 690, + "rank_one_pairs": 193704, + "rank_two_pairs": 15276999, + "three_member_image_planes": 82, + "witness": null + }, + "factor_sha256": "7780b09a855f20f2ba822a271b2fe767a70c1dd7e8acab20bebda4c085abceff", + "factors": 5563, + "four_subsets_covered": 39861761780790, + "image_planes": 140053, + "literal_single_replays": 5563, + "neutral_four_rank_one": 0, + "neutral_four_rank_two": 0, + "neutral_four_total": 0, + "neutral_triples": 0, + "new_kappa": false, + "pair_count": 15470703, + "peak_rank_two_plane_pairs": 11812, + "rank_one_pairs": 193704, + "rank_two_pairs": 15276999, + "three_member_image_planes": 66, + "witness": null +} diff --git a/research/r439-four-omission-boundary/README.md b/research/r439-four-omission-boundary/README.md new file mode 100644 index 0000000000..5ca52f3a05 --- /dev/null +++ b/research/r439-four-omission-boundary/README.md @@ -0,0 +1,233 @@ +# Four omitted ADDs cannot preserve the frozen PR967 helper-star boundary + +**Finite certificate and scoped algebraic reduction; no new kappa.** None of +the **39,861,761,780,790** four-position subsets of PR967's frozen 5,563-ADD +`D` word can be deleted while preserving its full linear map on all 661 +arbitrary dirty input columns. This resolves the explicit four-omission question +in [woklerx's PR1446](https://github.com/CrocSwap/integer-mult-bounds/pull/1446). +The one-, two- and three-omission results are PR1446's contribution; their +premises and zero counts are corroborated here. Any nonempty neutral omission +set, if one exists, therefore contains at least five positions. + +This excludes one small, fixed simplification class. It does not prove that +the helper-star circuit is shortest, and it does not exclude inserted gates, +reordering, another helper basis, a changed interface, or a different word. +The selected supplier, paid recursive profile and exponent are unchanged. + +## Object, provenance and new contribution + +The input is +`research/r439-helper-stars-seed19/candidate.json.gz`, SHA256 +`d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8`. +Flatten each `D` record's source list in its stored order: one source is one +elementary XOR/ADD position, numbered from zero. All these gates are at frame +zero. No source, target or helper column is treated as clean or unobserved. + +Exact base: `1ff9c501b624ec354e1330b1b9be571a6adba9cb`. +Exact retained predecessor heads: + +| Predecessor | Head | Contribution used | +|---|---|---| +| PR1446, woklerx | `83bab0ac63d7297309e769641d176ca3f12b0124` | Transported-transvection reduction, one/two/three omission results and four-omission handoff | +| PR967, Sricharan Vagvala / theon199 | `c6caa79e6655d83780a3b70a1d658313126fb0b3` | Frozen helper-star construction | + +All live input blobs and SHA256 values are in [SOURCES.json](SOURCES.json). +No pending implementation or unreviewed mathematical claim is a dependency. +The predecessor factor digest is used for corroboration; no predecessor Python +module is imported as an acceptance oracle. + +The new work is the complete four-omission census and its exact image-plane +partition, which avoids retaining a table of all 15,470,703 pair products. +The largest image-plane bucket contains only 11,812 pairs. A second full +census partitions the same domain by covector planes; its largest bucket is +690 pairs. These are two uses of the same census implementation, not two +independently authored verifiers. Separately implemented dense matrix and +literal deletion checks provide the independent finite controls below. + +The chooser selected `bit-helper-contract`, priority revision 3. The scope is +explicitly **changed** from proposing a replacement H2/K interface to PR1446's +named boundary audit, because PR1194/1311 already cover the immediate semantic-D +replacement. Its value is a precise stopping rule for this local simplification +class; it is a side result, not progress on the binding complex moment. +[TASK.json](TASK.json) records the complete scope and stop rule. +The claim is in [discussion #2004](https://github.com/CrocSwap/integer-mult-bounds/discussions/2004). + +## Proof of the reduction and exhaustive coverage + +Work over F2. Let the chronological elementary gates be +`L_i = I + e_dst e_src^T`, with distinct operands, and +`P = L_(n-1) ... L_0`. Each `L_i` is an involution. For its **original baseline +suffix** `B_i = L_(n-1) ... L_(i+1)`, define + +``` +T_i = B_i L_i B_i^-1 = I + u_i v_i^T, +u_i = B_i e_dst, v_i^T = e_src^T B_i^-1. +``` + +Both factors are nonzero and `v_i^T u_i = 0`. As in PR1446, cancellation of +baseline suffixes gives, for omissions `a < b < c < d`, + +``` +P_deleted P^-1 = T_d T_c T_b T_a. +``` + +Thus the four omissions are neutral exactly when + +``` +T_b T_a = T_c T_d. (1) +``` + +The right side is the **inverse** of the late chronological pair product. +Using `T_d T_c` there would be wrong for noncommuting pairs. The checker keeps +both orientations and includes a positive example that detects this mistake. + +All 5,563 transported factors are distinct. For two distinct factors, + +``` +T_b T_a - I + = [u_a,u_b] [[1,0],[v_b^T u_a,1]] [v_a^T;v_b^T]. (2) +``` + +If `u_a = u_b`, the product minus identity is +`u_a (v_a+v_b)^T`; if `v_a = v_b`, it is +`(u_a+u_b) v_a^T`. Nilpotency removes the cross term in either case. +These are rank-one products and the factors commute. No pair belongs to both +cases, since the original factors are distinct. Rank-one equality is tested +with its unique nonzero binary outer-product factors. + +Otherwise both two-column/two-row outer matrices in (2) have rank two and +the middle matrix is invertible. The product minus identity has rank two and +image exactly `span(u_a,u_b)`. Consequently two such products can be equal +only if their image planes are equal. A binary plane has exactly three nonzero +vectors. For each pair of distinct image vectors present in the source, the +checker includes their sum if it is also present; a three-member plane is +visited only at its two smallest vectors. A two-member plane is visited once. +This partitions every rank-two pair without any numerical hash approximation. + +Fix a basis `(x,y)` of one such plane. Every product in that bucket has a +unique representation + +``` +T_b T_a - I = x r^T + y s^T. +``` + +The two exact 661-bit row masks `(r,s)` are its key. The implementation +computes these directly from (2) and separately computes the inverse product +key. Python dictionary collisions are resolved by exact tuple equality; a +digest is never used to decide product equality. + +For each forward key, keep the earlier pair endings `b` in sorted order. For +each late inverse key `(c,d)`, count only endings **strictly less than c**. +This enforces `a> i) & 1] + direct = audit.compose(audit.replay(word, 3, omitted), inverse) + transported = [1, 2, 4] + for i in omitted: + transported = audit.compose(audit.transvection_rows(factors[i], 3), transported) + self.assertEqual(direct, transported) + checked += 1 + self.assertEqual(checked, 1728) + + def test_noncommuting_orientation(self): + factors = [(1, 2), (2, 4), (3, 4), (1, 6)] + self.assertEqual(audit.four_census(factors)["neutral_four_rank_two"], 1) + swapped = [factors[i] for i in (1, 0, 2, 3)] + self.assertEqual(audit.four_census(swapped)["neutral_four_total"], 0) + self.assertEqual(audit.dense_oracle(swapped, 3), []) + + def test_three_member_plane_and_transpose(self): + factors = [(1, 2), (1, 4), (6, 6), (7, 6)] + direct = audit.four_census(factors) + dual = audit.four_census([(v, u) for u, v in factors]) + self.assertEqual(direct["three_member_image_planes"], 1) + self.assertEqual(direct["neutral_four_total"], 1) + self.assertEqual(dual["neutral_four_total"], 1) + + def test_strict_chronological_split(self): + f = {"same": [(0, 1), (0, 2), (1, 2)]} + self.assertEqual(audit.ordered_matches(f, [("same", 1, 3)])[0], 0) + self.assertEqual(audit.ordered_matches(f, [("same", 2, 3)])[0], 1) + self.assertEqual(audit.ordered_matches(f, [("same", 3, 4)])[0], 3) + + def test_all_two_dimensional_factor_subsets(self): + factors = [(u, v) for u in range(1, 4) for v in range(1, 4) + if not audit.parity(u & v)] + for size in range(len(factors) + 1): + for subset in itertools.combinations(factors, size): + result = audit.four_census(subset) + self.assertEqual(result["neutral_four_total"], len(audit.dense_oracle(subset, 2))) + + def test_arbitrary_dirty_helper_is_observed(self): + rows = audit.replay([(0, 2)], 3) + self.assertEqual([r & 3 for r in rows[:2]], [1, 2]) + self.assertNotEqual(rows, [1, 2, 4]) + self.assertEqual(rows[0] & 4, 4) + + def test_source_factor_and_receipt_mutations(self): + gates, width = audit.load_bound_word() + factors = audit.factors_from_suffixes(gates, width) + bad = factors.copy() + u, v = bad[0] + bad[0] = (u, v ^ 1) + with self.assertRaisesRegex(ValueError, "incoming factor transport"): + audit.check_factors(gates, width, bad) + fixture = audit.four_census([(1, 2), (2, 4), (3, 4), (1, 6)]) + audit.check_certificate(fixture, copy.deepcopy(fixture)) + for key in ("pair_count", "neutral_four_total", "neutral_four_rank_two"): + changed = copy.deepcopy(fixture) + changed[key] += 1 + with self.assertRaisesRegex(ValueError, "certificate mismatch"): + audit.check_certificate(fixture, changed) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/r439-four-omission-boundary/verify.py b/research/r439-four-omission-boundary/verify.py new file mode 100644 index 0000000000..40d677420f --- /dev/null +++ b/research/r439-four-omission-boundary/verify.py @@ -0,0 +1,351 @@ +#!/usr/bin/env python3 +"""Exact chronological four-omission census. Apache-2.0. + +Prepared for commdata2338 with substantial OpenAI Codex assistance. +Transported-transvection reduction: woklerx, PR1446/PR1017. +""" +from bisect import bisect_left +from collections import defaultdict +import argparse +import gzip +import hashlib +from itertools import combinations +import json +import math +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/r439-helper-stars-seed19/candidate.json.gz" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def parity(x): + return x.bit_count() & 1 + + +def replay(gates, width, omitted=()): + rows = [1 << i for i in range(width)] + omitted = set(omitted) + for i, (dst, src) in enumerate(gates): + if i not in omitted: + rows[dst] ^= rows[src] + return rows + + +def row_times(vector, rows): + result = 0 + while vector: + bit = vector & -vector + result ^= rows[bit.bit_length() - 1] + vector ^= bit + return result + + +def compose(left, right): + return [row_times(row, right) for row in left] + + +def transvection_rows(factor, width): + u, v = factor + return [(1 << i) ^ (v if (u >> i) & 1 else 0) + for i in range(width)] + + +def factors_from_suffixes(gates, width): + """u=B e_dst, v=e_src^T B^-1, using exact baseline suffixes B.""" + columns = [1 << i for i in range(width)] + inverse_rows = columns.copy() + factors = [None] * len(gates) + for i in range(len(gates) - 1, -1, -1): + dst, src = gates[i] + require(0 <= dst < width and 0 <= src < width and dst != src, + "invalid elementary ADD") + factors[i] = (columns[dst], inverse_rows[src]) + columns[src] ^= columns[dst] + inverse_rows[dst] ^= inverse_rows[src] + return factors + + +def check_factors(gates, width, factors, literal_singles=False): + """Separate forward-prefix construction; optionally every literal omission.""" + baseline = replay(gates, width) + inverse = replay(gates[::-1], width) + require(compose(baseline, inverse) == [1 << i for i in range(width)], + "baseline inverse") + prefixes = [1 << i for i in range(width)] + for i, (dst, src) in enumerate(gates): + u, v = factors[i] + incoming = prefixes[src] + require(v == row_times(incoming, inverse), "incoming factor transport") + if literal_singles: + changed = replay(gates, width, (i,)) + require(all((changed[j] ^ baseline[j]) == + (incoming if (u >> j) & 1 else 0) + for j in range(width)), "literal single omission") + prefixes[dst] ^= prefixes[src] + require(prefixes == baseline, "forward prefix boundary") + + +def ordered_matches(forward, backward): + """Count (a,b),(c,d) with b 0 and v > 0 and not parity(u & v) for u, v in factors), + "nontrivial transvection premise") + by_u, by_v = defaultdict(list), defaultdict(list) + for i, (u, v) in enumerate(factors): + by_u[u].append((i, v)) + by_v[v].append((i, u)) + + rank_one = defaultdict(list) + rank_one_pairs = 0 + for side, groups in enumerate((by_u, by_v)): + for common, members in groups.items(): + for (a, x), (b, y) in combinations(members, 2): + key = (common, x ^ y) if side == 0 else (x ^ y, common) + rank_one[key].append((a, b)) + rank_one_pairs += 1 + count_one, witness_one = ordered_matches( + rank_one, ((key, c, d) for key, pairs in rank_one.items() for c, d in pairs)) + triple_set = set() + index = {factor: i for i, factor in enumerate(factors)} + for key, pairs in rank_one.items(): + if key in index: + for a, b in pairs: + triple_set.add(tuple(sorted((a, b, index[key])))) + + us = sorted(by_u) + position = {u: i for i, u in enumerate(us)} + count_two = rank_two_pairs = plane_count = three_member_planes = 0 + peak_plane_pairs = 0 + witness_two = None + for ia, x in enumerate(us): + for ib in range(ia + 1, len(us)): + y = us[ib] + ic = position.get(x ^ y) + if ic is not None and ic < ib: + continue # visit a three-member plane at its two smallest u's + plane_count += 1 + groups = [(x, 1, by_u[x]), (y, 2, by_u[y])] + if ic is not None: + three_member_planes += 1 + groups.append((x ^ y, 3, by_u[x ^ y])) + forward = defaultdict(list) + backward = [] + for (ug, cg, group_g), (uh, ch, group_h) in combinations(groups, 2): + for i, vg in group_g: + for j, vh in group_h: + if vg == vh: + continue # already covered by the rank-one by_v bucket + if i < j: + a, b, ua, ub, va, vb, ca, cb = i, j, ug, uh, vg, vh, cg, ch + else: + a, b, ua, ub, va, vb, ca, cb = j, i, uh, ug, vh, vg, ch, cg + # T_b T_a-I = ua va + ub (vb + (vb.ua) va). + q = vb ^ (va if parity(vb & ua) else 0) + f0 = (va if ca & 1 else 0) ^ (q if cb & 1 else 0) + f1 = (va if ca & 2 else 0) ^ (q if cb & 2 else 0) + # The inverse is T_a T_b, with the other cross term. + p = va ^ (vb if parity(va & ub) else 0) + g0 = (p if ca & 1 else 0) ^ (vb if cb & 1 else 0) + g1 = (p if ca & 2 else 0) ^ (vb if cb & 2 else 0) + forward[(f0, f1)].append((a, b)) + backward.append(((g0, g1), a, b)) + plane_pairs = len(backward) + peak_plane_pairs = max(peak_plane_pairs, plane_pairs) + rank_two_pairs += plane_pairs + matches, witness = ordered_matches(forward, backward) + count_two += matches + if witness is not None: + witness_two = witness if witness_two is None else min(witness_two, witness) + require(rank_one_pairs + rank_two_pairs == math.comb(len(factors), 2), + "pair partition coverage") + witnesses = [w for w in (witness_one, witness_two) if w is not None] + return { + "factors": len(factors), + "distinct_image_vectors": len(by_u), + "distinct_covectors": len(by_v), + "pair_count": rank_one_pairs + rank_two_pairs, + "rank_one_pairs": rank_one_pairs, + "rank_two_pairs": rank_two_pairs, + "image_planes": plane_count, + "three_member_image_planes": three_member_planes, + "peak_rank_two_plane_pairs": peak_plane_pairs, + "neutral_triples": len(triple_set), + "neutral_four_rank_one": count_one, + "neutral_four_rank_two": count_two, + "neutral_four_total": count_one + count_two, + "witness": list(min(witnesses)) if witnesses else None, + } + + +def dense_oracle(factors, width): + """Small-domain oracle: literal dense matrices, no pair-bucket logic.""" + identity = [1 << i for i in range(width)] + matrices = [transvection_rows(factor, width) for factor in factors] + neutral = [] + for indices in combinations(range(len(factors)), 4): + product = identity + for i in indices: + product = compose(matrices[i], product) + if product == identity: + neutral.append(indices) + return neutral + + +def controls(): + # Every 3D transvection and several complete chronological orderings. + small = [(u, v) for u in range(1, 8) for v in range(1, 8) + if not parity(u & v)] + require(len(small) == 21, "small transvection domain") + orders = [[small[(k * j) % 21] for j in range(21)] for k in (1, 2, 4, 5)] + orders += [order[::-1] for order in orders.copy()] + counts = [] + for ordered in orders: + expected = dense_oracle(ordered, 3) + observed = four_census(ordered) + require(observed["neutral_four_total"] == len(expected), "dense quartet oracle") + require(observed["witness"] is None or tuple(observed["witness"]) in expected, + "dense quartet witness") + counts.append(len(expected)) + + # Both rank strata contain positive examples. The second is noncommuting. + one = [(1, 2), (1, 4), (6, 6), (7, 6)] + two = [(1, 2), (2, 4), (3, 4), (1, 6)] + require(four_census(one)["neutral_four_rank_one"] == 1, "rank-one positive") + require(four_census(two)["neutral_four_rank_two"] == 1, "rank-two positive") + left = compose(transvection_rows(two[1], 3), transvection_rows(two[0], 3)) + wrong_right = compose(transvection_rows(two[3], 3), transvection_rows(two[2], 3)) + require(left != wrong_right, "same-orientation mutant must fail") + wrong_order = [two[i] for i in (1, 0, 2, 3)] + require(not dense_oracle(wrong_order, 3) and + four_census(wrong_order)["neutral_four_total"] == 0, + "chronology mutant must fail") + require(ordered_matches({0: [(0, 2)]}, [(0, 1, 3)])[0] == 0, + "interleaved pairs are not chronological splits") + require(ordered_matches({0: [(0, 2)]}, [(0, 2, 3)])[0] == 0, + "shared-position pairs are not disjoint") + require(ordered_matches({0: [(0, 1), (0, 2), (1, 2)]}, [(0, 3, 4)])[0] == 3, + "all compatible earlier pairs must be counted") + rejected = 0 + for bad in [[(1, 2), (1, 2)], [(1, 1)], [(0, 2)], [(1, 0)]]: + try: + four_census(bad) + except ValueError: + rejected += 1 + require(rejected == 4, "malformed factor controls") + # Restored zero helpers would hide this change; arbitrary dirt does not. + dirty_rows = replay([(0, 2)], 3) + require([r & 3 for r in dirty_rows[:2]] == [1, 2] and dirty_rows != [1, 2, 4], + "clean-input-only counterexample") + # Check the deletion formula for every subset (not just size four) of + # a literal word with noncommuting gates, using original baseline suffixes. + gates = [(0, 1), (1, 2), (2, 0), (0, 2), (1, 0), (2, 1), (0, 1)] + factors = factors_from_suffixes(gates, 3) + check_factors(gates, 3, factors, literal_singles=True) + baseline = replay(gates, 3) + inverse = replay(gates[::-1], 3) + for mask in range(1 << len(gates)): + omitted = [i for i in range(len(gates)) if (mask >> i) & 1] + product = [1, 2, 4] + for i in omitted: + product = compose(transvection_rows(factors[i], 3), product) + require(compose(replay(gates, 3, omitted), inverse) == product, + "literal deletion transport formula") + require(baseline != [1, 2, 4], "nontrivial literal positive word") + return {"dense_orderings": len(orders), "dense_quartets": len(orders) * math.comb(21, 4), + "dense_neutral_counts": counts, "literal_deletion_subsets": 1 << len(gates), + "positive_rank_strata": 2, "malformed_factor_rejections": rejected, + "orientation_chronology_dirty_controls": 5} + + +def load_bound_word(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for source in manifest["files"]: + if source["usage"] == "input": + data = (ROOT / source["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == source["sha256"], + "source digest: " + source["path"]) + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + require((word["v"], word["R"]) == (111, 439), "source dimensions") + require(all(frame == 0 for frame, dst, srcs in word["D"]), "zero-frame D") + gates = [(dst, src) for frame, dst, srcs in word["D"] for src in srcs] + require(len(gates) == 5563, "elementary gate count") + return gates, 661 + + +def check_certificate(result, expected): + require(result == expected, "certificate mismatch") + + +def run(): + gates, width = load_bound_word() + factors = factors_from_suffixes(gates, width) + check_factors(gates, width, factors, literal_singles=True) + digest = hashlib.sha256(json.dumps([[str(u), str(v)] for u, v in factors], + separators=(",", ":")).encode()).hexdigest() + predecessor = json.loads((ROOT / "research/r439-three-omission-distance/CERTIFICATE.json").read_text()) + require(digest == predecessor["factor_sha256"], "PR1446 factor corroboration") + result = four_census(factors) + # Same full finite domain, partitioned independently by covector planes. + # Transpose reverses products; reversing four involutions preserves I. + dual = four_census([(v, u) for u, v in factors]) + for key in ("pair_count", "rank_one_pairs", "rank_two_pairs", "neutral_triples", + "neutral_four_rank_one", "neutral_four_rank_two", "neutral_four_total"): + require(result[key] == dual[key], "dual-plane corroboration: " + key) + witness = result["witness"] + if witness is not None: + require(replay(gates, width, witness) == replay(gates, width), + "literal four-omission witness") + result.update({"columns": width, "four_subsets_covered": math.comb(len(gates), 4), + "factor_sha256": digest, "literal_single_replays": len(gates), + "dual_partition": dual, "controls": controls(), "new_kappa": False}) + return result + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="write the deterministic receipt") + args = parser.parse_args() + result = run() + certificate = HERE / "CERTIFICATE.json" + if args.write: + certificate.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + check_certificate(result, json.loads(certificate.read_text())) + print("PASS_FOUR_OMISSION_CENSUS" + f" gates={result['factors']} pairs={result['pair_count']}" + f" four_subsets={result['four_subsets_covered']}" + f" neutral={result['neutral_four_total']} columns={result['columns']}" + f" dual_neutral={result['dual_partition']['neutral_four_total']}" + f" dense_controls={result['controls']['dense_quartets']} no_new_kappa")