From b6d49298b6ca5f40c47532866ae45dc16b8416ca Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 15:23:30 +0000 Subject: [PATCH] feat(research): complete the (1,2,4) Boolean fanout Pareto frontier Decide every eight-ADD one-insertion count vector for the PR #5514 demand over F2^3 by enumerating all ADD-only words with at most four gates. Two extra ADDs may sit in the insertion row and any other row, never in both non-insertion rows. Six new unexposed vectors join the 25 price-envelope vectors to give a 31-vector aggregate frontier. --- .../fanout-one-insertion-pareto/README.md | 127 +++++++++ .../fanout-one-insertion-pareto/SOURCES.json | 24 ++ .../fanout-one-insertion-pareto/TASK.json | 84 ++++++ .../fanout-one-insertion-pareto/VERIFY.json | 36 +++ .../fanout-one-insertion-pareto/verify.py | 262 ++++++++++++++++++ 5 files changed, 533 insertions(+) create mode 100644 research/fanout-one-insertion-pareto/README.md create mode 100644 research/fanout-one-insertion-pareto/SOURCES.json create mode 100644 research/fanout-one-insertion-pareto/TASK.json create mode 100644 research/fanout-one-insertion-pareto/VERIFY.json create mode 100644 research/fanout-one-insertion-pareto/verify.py diff --git a/research/fanout-one-insertion-pareto/README.md b/research/fanout-one-insertion-pareto/README.md new file mode 100644 index 0000000000..0a6b3d408d --- /dev/null +++ b/research/fanout-one-insertion-pareto/README.md @@ -0,0 +1,127 @@ +# Complete Pareto frontier for the (1,2,4) Boolean fanout + +This contribution was produced by Nick Petalas. Apache-2.0. + +For lee-phys's [PR #5514](https://github.com/CrocSwap/integer-mult-bounds/pull/5514) +demand `(1,2,4)` over `F2^3`, the aggregate count vectors +`(P_0,P_1,P_2; K_0,K_1,K_2)` of insertions and incoming ADDs have exactly +**31 Pareto-minimal elements**. The 25 vectors exposed by #5514's price +envelope are all of them except **six new unexposed vectors**: + + P = e_i, K = (2,2,2) + e_i + e_h, h != i. + +So a one-insertion word can split its two extra ADDs between the insertion +row and any other row. It cannot place them in the two non-insertion rows: +`K = (2,2,2) + e_j + e_k` with `i` not in `{j,k}` is impossible. This +answers #5514 Open next question 1, including its suggested first step on +`(3,3,2)` and its permutations. + +Claim type: **exact finite certificate** for the one-insertion layer over +`F2^3`, combined with #5514's **written** componentwise multi-insertion +bounds. The six new words are also proved for every commutative unital +Boolean ring with a nonzero pairwise orthogonal demand triple. No new +kappa, physical supplier or selected-frontier change is claimed. + +## Contract + +Unchanged from #5514: three arbitrary dirty rows, one preserved source, +gates `P_i(beta)` and `E_ij(alpha)` with every nonzero coefficient, any +finite word, and every original dirt column restored. Encode `x0+2x1+4x2`; +the ring identity is `7` and `g = 7`. + +## The new words + +For insertion row 0 with the extra ADD in row 2, write `l_r` for lambda_r: + + E_02(l1+l2), E_20(l1+l2), E_01(l1), E_10(l1), + P_0(g), + E_10(l1), E_20(l1+l2), E_02(l1+l2), E_21(l1). + +The suffix moves the source column +`(g,0,0) -> (g,l1,0) -> (g,l1,l1+l2) -> (l0,l1,l1+l2) -> (l0,l1,l2)`. +Its dirt matrix `L` also has the four-gate word +`E_10(l1), E_01(l1), E_20(l1+l2), E_02(l1+l2)`, doubled in row 0. The +prefix is that word reversed, which is `L^-1` because every `E_ij` is an +involution in characteristic two. Incoming counts are `(2,1,1)` before and +`(1,1,2)` after the insertion, so `K = (3,2,3)`. The receipt lists all six +words, one per insertion row `i` and extra row `h != i`. + +Every coefficient is a sum of distinct lambdas, hence nonzero. The words +are checked over the universal ring `F2[l0,l1,l2]/(l_r^2-l_r, l_r l_s)`, +which is `F2^4`. Any Boolean ring with a nonzero orthogonal triple receives +a ring map from it, so restoration and the source column transfer. + +## Why the frontier is complete + +1. **One insertion, at least eight ADDs.** #5514 shows the single insertion + is `P_i(g)` and that the ADD-only suffix `L` and the prefix `L^-1` each + need a gate into every row. Here the enumeration independently finds no + word with at most three gates whose column `i` equals lambda. Hence + `K >= (2,2,2)` and each side has exactly four gates when `sum K = 8`. +2. **The eight-ADD layer.** The verifier enumerates every word of exactly + four nonzero gates (42 gates, 202,192 distinct matrices). For each root, + 104 matrices `L` split `g e_i`. Each has one or two destination-count + vectors among its four-gate words. Pairing a suffix vector with a prefix + vector of the same `L` gives exactly the five totals + `(2,2,2)+2e_h` and `(2,2,2)+e_i+e_h`. For root 0 the classes are 56 + matrices doubled only in row 0, 20 only in row 1, 20 only in row 2, and + 4 each doubled in `{0,1}` or `{0,2}`. No matrix is doubled in both + non-root rows. +3. **Nine or more ADDs are dominated.** The excess `K-(2,2,2)` has total at + least three. Every such excess has a coordinate at least two or covers + `e_i+e_h`, so it dominates one of the five eight-ADD excesses. +4. **Two or more insertions.** #5514's case analysis gives componentwise + lower bounds dominating `D`, `T_i`, `R_(i,j;k)` or `M_(i,j;k)`, and + attains each. These 16 vectors are cited, not replayed here. +5. The verifier checks that the 31 vectors are pairwise non-dominating. + +Each new vector costs `mu_i + 2 sum(c) + c_i + c_h`, the average of +`U_(i,i)` and `U_(i,h)`. It therefore never uniquely minimizes a price, +which is why the 25-term envelope cannot see it. + +## Evidence and reproduction + +From the worktree root, with the repository CPython 3.12 interpreter: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/fanout-one-insertion-pareto/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/fanout-one-insertion-pareto/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fanout-one-insertion-pareto +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fanout-one-insertion-pareto --check-source-history +``` + +Standard library only; about one second per run. The verifier prints a +JSON receipt with SHA256 hashes of the five package files, then +`PASS_FANOUT_ONE_INSERTION_PARETO`. It writes no files. Coverage: all +ADD-only words with at most four nonzero gates, every root, six new words +on formal columns over `F2^3` and `F2^4` plus their reversed inverses, +24,576 literal width-one inputs, and 17 mutation controls (each deleted +gate and each altered ADD coefficient of one new word is rejected). + +## Limits + +The exclusion of non-root extra ADDs is a finite certificate over `F2^3` +only; no written proof is given, and larger Boolean rings are open. The +multi-insertion part rests on #5514's written proof, which is cited and +pinned, not re-verified. Directed-edge prices, helpers, restricted +coefficients and non-Boolean rings are outside this result. Independent +human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Does the non-root exclusion hold over every Boolean ring with a nonzero + orthogonal triple? Start with the same four-gate enumeration over the + universal ring `F2^4` (90 gates), or a written invariant for suffix words + doubled in a non-insertion row. +- What is the frontier with independently priced directed edges (#5514 + Open next question 2)? Start from the directed-edge multisets of the + four-gate split words found here; destination counts lose parent data. + +## Credit + +lee-phys's #5514 supplies the question, contract, column lemma, return +lemma, multi-insertion case analysis and the 25 attaining words. That +proof credits #3063, #4916, #5163, #5139, #5259, #5304 and Ali Romman's +#5310; their roles are retained. New work: the exhaustive eight-ADD +one-insertion decision, the six new words, the universal-ring transfer and +the 31-vector frontier. diff --git a/research/fanout-one-insertion-pareto/SOURCES.json b/research/fanout-one-insertion-pareto/SOURCES.json new file mode 100644 index 0000000000..29bed57c1f --- /dev/null +++ b/research/fanout-one-insertion-pareto/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/orthogonal-boolean-fanout/README.md", + "usage": "input", + "git_blob": "fa02e1e5850044a9aafb6131f6e50421e5c34d1b", + "sha256": "9ae4f5beb80fbb0795bd40c148eb4a22d7c7b1def2e9af61df855df57151b5d6" + } + ] +} diff --git a/research/fanout-one-insertion-pareto/TASK.json b/research/fanout-one-insertion-pareto/TASK.json new file mode 100644 index 0000000000..5b6d59d492 --- /dev/null +++ b/research/fanout-one-insertion-pareto/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Decide every eight-ADD one-insertion incoming-count vector for lee-phys PR #5514's demand (1,2,4) over F2^3, and combine it with that PR's componentwise multi-insertion bounds to list the complete aggregate Pareto frontier of (insertion, incoming-ADD) count vectors.", + "scope_change_reason": "Answers PR #5514 Open next question 1 (aggregate Pareto frontier). This is an abstract dirty-input tariff side result, not a G20 helper path or a physical supplier change.", + "bottleneck_link": "Side result: an exact count frontier for one restoring fanout demand. Physical access, routing, precision, stock and supplier admission remain separate. No new kappa.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact decision of the (3,3,2) one-insertion branch; do not extend to directed-edge prices or larger rings.", + "outcome": "completed", + "evidence": "verify.py enumerates every ADD-only word with at most four nonzero gates over F2^3 (1, 42, 1111, 18472 and 202192 distinct matrices for exactly 0 to 4 gates), decides every eight-ADD one-insertion total for each insertion row, replays six new words over F2^3 and the universal ring F2^4 with a separate interpreter, runs 24,576 literal input checks and 17 mutation controls, and checks pairwise non-domination of the 31 frontier vectors. Stdout receipt binds the package files by SHA256.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the exclusion of extra ADDs in the two non-insertion rows hold for every Boolean ring with a nonzero orthogonal demand triple?", + "why_it_matters": "The six new words hold in every such ring, but the exclusion is certified only over F2^3; larger rings allow more coefficients.", + "first_step": "Repeat the four-gate enumeration over the universal ring F2^4 (90 gates), or find a written invariant separating suffix words whose doubled destination is a non-insertion row.", + "blocked_by": "No written proof of the exclusion is supplied; the F2^3 certificate does not transfer to larger rings by a ring homomorphism." + }, + { + "question": "What is the Pareto frontier for the same demand with independently priced directed ADD edges (PR #5514 Open next question 2)?", + "why_it_matters": "Destination counts lose parent information; edge-level vectors can separate words that this frontier identifies.", + "first_step": "Record the directed-edge multiset of every four-gate split word found here and recompute non-domination at edge granularity.", + "blocked_by": "The multi-insertion bounds cited from PR #5514 are destination-count bounds, not edge-count bounds." + } + ], + "question_source": "PR #5514" +} diff --git a/research/fanout-one-insertion-pareto/VERIFY.json b/research/fanout-one-insertion-pareto/VERIFY.json new file mode 100644 index 0000000000..c4d3fedb2d --- /dev/null +++ b/research/fanout-one-insertion-pareto/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/orthogonal-boolean-fanout/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All ADD-only words with at most four gates over F2^3, every eight-ADD one-insertion total, six new words over F2^3 and F2^4, literal inputs, mutation controls and 31-vector non-domination; normal mode." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete check in optimized mode; every check uses explicit failures, not assert." + } + ] +} diff --git a/research/fanout-one-insertion-pareto/verify.py b/research/fanout-one-insertion-pareto/verify.py new file mode 100644 index 0000000000..b16c2a1c9c --- /dev/null +++ b/research/fanout-one-insertion-pareto/verify.py @@ -0,0 +1,262 @@ +#!/usr/bin/env python3 +"""Exact one-insertion Pareto layer for demand (1,2,4) over F2^3. + +Self-contained standard-library verifier. It enumerates every ADD-only word +with at most four nonzero gates over R = F2^3, decides every eight-ADD +one-insertion count vector, replays the six new attaining words with a +separate scalar interpreter over F2^3 and over the universal ring F2^4, and +checks the 31-vector aggregate frontier for pairwise non-domination. +Writes no files. Produced by Nick Petalas. Apache-2.0. +""" + +import hashlib +import itertools +import json +import pathlib +import sys + +ROWS = 3 +LAMBDA = (1, 2, 4) # bitmask encoding x0 + 2 x1 + 4 x2 of PR #5514 +ONE = 7 +G = 7 # g = lambda_0 + lambda_1 + lambda_2 +MAX_GATES = 4 +GATES = tuple((i, j, a) for i in range(ROWS) for j in range(ROWS) if i != j + for a in range(1, 8)) +IDENTITY = (ONE, 0, 0, 0, ONE, 0, 0, 0, ONE) +PACKAGE = pathlib.Path(__file__).resolve().parent +PACKAGE_FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", + "verify.py") + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def apply_gate(matrix, gate): + """Left-multiply a row-major 3x3 matrix over F2^3 by E_ij(a).""" + i, j, a = gate + out = list(matrix) + for c in range(ROWS): + out[ROWS * i + c] ^= a & matrix[ROWS * j + c] + return tuple(out) + + +def unit(r): + return tuple(1 if t == r else 0 for t in range(ROWS)) + + +def add(u, v): + return tuple(x + y for x, y in zip(u, v)) + + +def enumerate_levels(): + """levels[k]: matrix -> {count vector: witness word} for exactly k gates.""" + levels = [{IDENTITY: {(0, 0, 0): ()}}] + for _ in range(MAX_GATES): + nxt = {} + for matrix, witnesses in levels[-1].items(): + for gate in GATES: + image = apply_gate(matrix, gate) + slot = nxt.setdefault(image, {}) + for counts, word in witnesses.items(): + grown = add(counts, unit(gate[0])) + if grown not in slot: + slot[grown] = word + (gate,) + levels.append(nxt) + require(len(GATES) == 42, "gate alphabet size") + return levels + + +def column(matrix, r): + return tuple(matrix[ROWS * t + r] for t in range(ROWS)) + + +def expected_totals(root): + base = (2, 2, 2) + out = {add(add(base, unit(h)), unit(h)) for h in range(ROWS)} + out |= {add(add(base, unit(root)), unit(h)) for h in range(ROWS) if h != root} + return out + + +def one_insertion_layer(levels): + for k in range(MAX_GATES): + for matrix in levels[k]: + for root in range(ROWS): + require(column(matrix, root) != LAMBDA, + f"a {k}-gate ADD word already splits g e_{root}") + report, words = {}, {} + for root in range(ROWS): + good = {m: w for m, w in levels[MAX_GATES].items() + if column(m, root) == LAMBDA} + totals = {add(s, p) for w in good.values() for s in w for p in w} + require(totals == expected_totals(root), f"eight-ADD totals, root {root}") + excluded = {add(add((2, 2, 2), unit(j)), unit(k)) + for j in range(ROWS) for k in range(j + 1, ROWS) + if root not in (j, k)} + require(excluded and not excluded & totals, "non-root (3,3,2) exclusion") + classes = {} + for w in good.values(): + key = ",".join("".join(map(str, c)) for c in sorted(w)) + classes[key] = classes.get(key, 0) + 1 + report[root] = {"suffix_matrices": len(good), + "count_set_classes": dict(sorted(classes.items())), + "totals": sorted(totals), "excluded": sorted(excluded)} + for h in range(ROWS): + if h == root: + continue + for w in good.values(): + s = add(add((1, 1, 1), unit(h)), (0, 0, 0)) + p = add((1, 1, 1), unit(root)) + if s in w and p in w: + prefix = tuple(reversed(w[p])) # E_ij(a) is an involution + words[(root, h)] = prefix + (("P", root, G),) + w[s] + break + require((root, h) in words, f"witness word for root {root}, h {h}") + return report, words + + +def lift(a): + """Map an F2^3 coefficient to the matching sum of universal idempotents.""" + return sum(1 << r for r in range(ROWS) if a >> r & 1) + + +def run_scalar(word, rows, source, ring_one, lift_coeff): + """Separate interpreter: dirty rows are dicts {column: ring element}.""" + rows = [dict(r) for r in rows] + for gate in word: + if gate[0] == "P": + _, i, b = gate + rows[i]["p"] = rows[i].get("p", 0) ^ (lift_coeff(b) & source) + else: + i, j, a = gate + coeff = lift_coeff(a) + require(coeff != 0, "zero coefficient") + for key, val in rows[j].items(): + rows[i][key] = rows[i].get(key, 0) ^ (coeff & val) + return rows + + +def check_word(word, root, h, ring_one, lam, lift_coeff): + """Formal columns: one symbolic dirt column per row plus the source.""" + start = [{f"d{r}": ring_one} for r in range(ROWS)] + end = run_scalar(word, start, ring_one, ring_one, lift_coeff) + for r in range(ROWS): + dirt = {k: v for k, v in end[r].items() if k != "p" and v} + require(dirt == {f"d{r}": ring_one}, f"dirt row {r} not restored") + require(end[r].get("p", 0) == lam[r], f"source coefficient row {r}") + counts = [0] * ROWS + inserts = 0 + for gate in word: + if gate[0] == "P": + inserts += 1 + else: + counts[gate[0]] += 1 + want = add(add((2, 2, 2), unit(root)), unit(h)) + require(inserts == 1 and tuple(counts) == want, "word counts") + back = run_scalar(tuple(reversed(word)), end, ring_one, ring_one, lift_coeff) + for r in range(ROWS): + rest = {k: v for k, v in back[r].items() if v} + require(rest == {f"d{r}": ring_one}, "reversed word is not the inverse") + + +def literal_check(word): + """All 8^3 dirty inputs and 8 sources at width one over F2^3.""" + checked = 0 + for a in itertools.product(range(8), repeat=ROWS): + for p in range(8): + vals = list(a) + for gate in word: + if gate[0] == "P": + vals[gate[1]] ^= gate[2] & p + else: + vals[gate[0]] ^= gate[2] & vals[gate[1]] + require(tuple(vals) == tuple(a[r] ^ (LAMBDA[r] & p) + for r in range(ROWS)), "literal input") + checked += 1 + return checked + + +def frontier(): + vecs = {} + for i in range(ROWS): + j, k = [r for r in range(ROWS) if r != i] + vecs[f"T_{i}"] = (add(unit(i), unit(i)), add(add(unit(j), unit(j)), add(unit(k), unit(k)))) + for h in range(ROWS): + vecs[f"U_({i},{h})"] = (unit(i), add((2, 2, 2), add(unit(h), unit(h)))) + if h != i: + vecs[f"V_({i},{h})"] = (unit(i), add((2, 2, 2), add(unit(i), unit(h)))) + vecs["D"] = ((1, 1, 1), (0, 0, 0)) + for i, j in itertools.permutations(range(ROWS), 2): + k = 3 - i - j + vecs[f"R_({i},{j};{k})"] = (add(add(unit(i), unit(i)), unit(j)), + add(unit(k), unit(k))) + vecs[f"M_({i},{j};{k})"] = (add(unit(i), unit(j)), + add(add(unit(i), unit(i)), add(unit(k), unit(k)))) + flat = {n: v[0] + v[1] for n, v in vecs.items()} + for a, b in itertools.permutations(flat, 2): + require(not all(x <= y for x, y in zip(flat[a], flat[b])), + f"{a} dominates {b}") + # Every one-insertion vector with >= 9 ADDs is dominated: it is >= (2,2,2) + # plus an excess of total >= 3, and every excess of total exactly 3 already + # dominates one of the five eight-ADD excesses of its root. + for root in range(ROWS): + eight = [tuple(x - 2 for x in t) for t in expected_totals(root)] + for x in itertools.product(range(4), repeat=ROWS): + if sum(x) == 3: + require(any(all(u <= v for u, v in zip(e, x)) for e in eight), + f"undominated nine-ADD excess {x}") + return vecs + + +def controls(word): + rejected = 0 + for pos, gate in enumerate(word): + bad = word[:pos] + word[pos + 1:] + try: + literal_check(bad) + except SystemExit: + rejected += 1 + if gate[0] != "P": + changed = word[:pos] + ((gate[0], gate[1], gate[2] ^ 1 or 2),) + word[pos + 1:] + try: + literal_check(changed) + except SystemExit: + rejected += 1 + require(rejected == 2 * len(word) - 1, f"mutation controls rejected {rejected}") + return rejected + + +def main(): + levels = enumerate_levels() + sizes = [len(level) for level in levels] + report, words = one_insertion_layer(levels) + literal = 0 + for (root, h), word in sorted(words.items()): + check_word(word, root, h, ONE, LAMBDA, lambda a: a) + check_word(word, root, h, 15, (1, 2, 4), lift) # universal ring F2^4 + literal += literal_check(word) + vecs = frontier() + rejected = controls(words[(0, 1)]) + digests = {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + receipt = { + "marker": "PASS_FANOUT_ONE_INSERTION_PARETO", + "level_sizes": sizes, + "one_insertion": {str(k): v for k, v in report.items()}, + "new_words": {f"root{r}_extra{h}": [list(g) for g in w] + for (r, h), w in sorted(words.items())}, + "literal_input_checks": literal, + "frontier_size": len(vecs), + "frontier": {n: list(p) + list(k) for n, (p, k) in sorted(vecs.items())}, + "mutation_controls_rejected": rejected, + "sha256": digests, + "python": sys.version.split()[0], + } + require(len(vecs) == 31 and sizes[MAX_GATES] == 202192, "frontier totals") + print(json.dumps(receipt, sort_keys=True)) + print("PASS_FANOUT_ONE_INSERTION_PARETO") + + +if __name__ == "__main__": + main()