diff --git a/research/g20-extended-wire-boundary-floor/README.md b/research/g20-extended-wire-boundary-floor/README.md new file mode 100644 index 0000000000..584fb43012 --- /dev/null +++ b/research/g20-extended-wire-boundary-floor/README.md @@ -0,0 +1,134 @@ +# Extra wires do not lower the G20 boundary below 38 ADDs + +This scoped proof was produced by Nick Petalas. **No new κ.** It answers the +open question of unpaidmoon's +[PR6641](https://github.com/CrocSwap/integer-mult-bounds/pull/6641) +(`5af623f5912f997163639e061feca4ebcf7e189e`): neither a priced scratch wire +nor a gate that leaves the 32 boundary wires lowers a legal GL(2)-commutant +side of the pinned PR5840 G20 boundary below **38 unit ADDs**. This holds for +any number of extra wires, under any nonnegative tariff, and whether each extra +wire is clean, dirty and restored, or left holding garbage. The scratch-free +words attain 38, so the exact minimum stays **38 per side and 76 per port**. + +## Lemma + +Work over F2 on `N = n + k` wires. A unit ADD is `x_d <- x_d + x_s` with +`d != s`; a SWAP costs three ADDs. A word of length `T` has matrix `M`. Let `A` +be the `n x n` block of `M` on a fixed set of n data wires (data outputs as +functions of data inputs). Let `v(A)` be the number of components of the +undirected graph on the data wires with an edge `{i, j}` when `A_ij = 1` or +`A_ji = 1`, and let `z(A)` be the number of zero diagonal entries of `A`. Then + +```text +T >= n - v(A) + z(A). +``` + +Nothing is assumed about the extra wires' inputs or outputs, or about the +other three blocks of `M`. + +**Proof.** This is the counting argument of Bu, Fan and Joo (arXiv:2408.07898, +Lemma 3.6 and Theorem 5.2), as written out for 32 wires in JoyboyBrian's +[PR6105](https://github.com/CrocSwap/integer-mult-bounds/pull/6105), run on +all `N` wires and then restricted to the data block. Let `P_t` be the partition +of the `N` wires into components of the graph of the first `t` gates. + +1. *Support invariant.* `M_t[i][j] = 1` implies `i, j` lie in one block of + `P_t`. This holds at `t = 0`. A gate `d <- d + s` changes only row `d`, to a + row supported in the blocks of `d` and `s`, which the gate merges. +2. *Potential.* Put `Φ_t = N - |P_t| + z_N(M_t)`, where `z_N` counts zero + diagonal entries over all `N` wires, so `Φ_0 = 0`. If a gate joins two + blocks, `|P|` drops by one and `M_t[s][d] = 0` by step 1, so no diagonal + entry changes. Otherwise `|P|` is unchanged and only entry `d` can change. + Either way `Φ` grows by at most one per gate, so `Φ_T <= T`. +3. *Restriction.* The data block of `M` is `A`, so `z_N(M) >= z(A)`. If + `A_ij = 1`, then `i, j` share a block of `P_T` by step 1. Each block of `P_T` + that meets the data wires is therefore a union of support components of + `A`, so at most `v(A)` blocks meet them. The other blocks lie among the `k` + extra wires. Hence `|P_T| <= v(A) + k` and + `T >= Φ_T >= n + k - v(A) - k + z(A) = n - v(A) + z(A)`. ∎ + +## Consequence for the G20 boundary + +The consumer reads the 32 labelled wires, so a word that implements one side +must have that side as its data block, with the data block's inputs on the +same 32 labels. For a legal basis `S` in PR6641's commutant `GL(2, F2)^16`, +the side is `S^{-1} L` or `R S`. PR6641 proves that the minimum of +`n - v + z` over that commutant is 38 on each side. By the lemma, every +extended word for every legal side therefore costs at least 38. A scratch +tariff is added on top, and the published scratch-free words reach 38, so no +nonnegative tariff helps. + +The same lemma settles the scalar part of the two-helper question in +[PR5898](https://github.com/CrocSwap/integer-mult-bounds/pull/5898): any bank +exchange `(a, b) -> (A b, B a)` has `z = 4` and `v <= 2`, so it costs at least +six ADDs with any number of helpers. + +## Evidence + +`verify.py` uses only the standard library and writes nothing: + +- **Pinned boundary.** Both programs replay to the stored rows of the + SHA256-pinned controller, each expands to 38 ADDs and each side has + `n - v + z = 38`. +- **Eight extended-wire controls.** On a 33rd wire, per side: a clean scratch + that copies data and is cleared from final rows (47 left, 41 right), a garbage + scratch (39), a clean relay that carries wire 31 through the whole word (42) + and a dirty live wire that carries wire 31 and is restored exactly (44). Each + realizes the same data block, respects the floor and costs more than 38. +- **Potential trace.** On 400 seeded random words with one to three extra + wires, every step checks the support invariant, the unchanged diagonal at + joins and `Φ_t <= t`. 47 words meet the floor with equality. +- **Complete width four.** Breadth-first search gives exact distances for all + 20,160 elements of GL(4, F2). All 302,400 (state, data subset) pairs respect + the floor. As a statistic, 140 of the 480 reachable data blocks of width one + to three meet it at their least distance. + +The finite checks test the lemma's arithmetic. The proof above is the claim. + +## Reproduce + +From the repository root, with CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/g20-extended-wire-boundary-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/g20-extended-wire-boundary-floor +``` + +Expected output: + +```text +PASS_G20_EXTENDED_WIRE_FLOOR side=38 port=76 witness=38/38 controls=8 control_lengths=[39, 41, 42, 44, 47] random_words=400 random_tight=47 gl4_states=20160 gl4_checks=302400 gl4_blocks=480 gl4_attained=140 no_new_kappa +``` + +Use another CPython 3.12 path on another machine. The run takes under a second. + +## Limits + +This is a scoped proof for unit two-wire XOR words, plus SWAPs at three ADDs. +It is not a multiplication theorem or a supplier admission. Selected +conditional κ and its five framework assumptions are unchanged. Not covered: + +- outputs that end on different physical wires, with the consumer relabelled; +- nonlinear gates, multi-target XORs at unit cost and non-unit tariffs; +- a changed controller, target diagonal or basis outside PR6641's commutant; +- native, ownership, compiler, precision and caller obligations. + +The commutant minimum of 38 is PR6641's result, cited at its head and not +replayed here. No Lean, Docker, native or selected-frontier replay was run. + +## Open next questions + +1. Can a side that leaves its data on other physical wires, with the consumer's + relabelling charged, beat 76 ADDs per port? The first step is to price the + relabel and compute `n - v + z` for the row-permuted data block. +2. Does a priced multi-target or nonlinear gate lower either side? The + potential count above uses two-wire XOR gates only. Test one priced + multi-target XOR on the four-wire exchange corner first. + +## Credit + +unpaidmoon posed the question and proved the commutant floor (PR6641). +JoyboyBrian proved the fixed-boundary 38-ADD floor and wrote out the counting +proof extended here (PR6105). Alan Bu, Evan Fan and Robert Joo own the +`n - v + z` bound. Ali Romman supplied the PR5840 controller, retained by +Charan . in PR5851. Nick Petalas's PR5898 posed the two-helper question. diff --git a/research/g20-extended-wire-boundary-floor/SOURCES.json b/research/g20-extended-wire-boundary-floor/SOURCES.json new file mode 100644 index 0000000000..c5932a03b1 --- /dev/null +++ b/research/g20-extended-wire-boundary-floor/SOURCES.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json", + "usage": "input", + "git_blob": "73fa9f40a032f11dabf357eba69066fcf9bf0a02", + "sha256": "978536e852c0cfbc150f143e19d2cfddbb434bac6017d914974eb99f641593a8" + } + ], + "mathematical_references": [ + { + "pr": 6641, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6641", + "head": "5af623f5912f997163639e061feca4ebcf7e189e", + "path": "research/g20-gl2-commutant-floor/README.md", + "author": "unpaidmoon", + "use": "Question source and the commutant minimum 38 of n - v + z over GL(2)^16, used as a cited step, not replayed." + }, + { + "pr": 6105, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6105", + "author": "JoyboyBrian", + "path": "research/g20-full-boundary-floor/README.md", + "use": "Scratch-free fixed-boundary floor whose counting proof is extended here." + }, + { + "reference": "Alan Bu, Evan Fan and Robert Joo, Minimum Synthesis Cost of CNOT Circuits, arXiv:2408.07898, Lemma 3.6 and Theorem 5.2", + "use": "The n - v + z counting bound on n wires." + } + ] +} diff --git a/research/g20-extended-wire-boundary-floor/TASK.json b/research/g20-extended-wire-boundary-floor/TASK.json new file mode 100644 index 0000000000..374f644c6f --- /dev/null +++ b/research/g20-extended-wire-boundary-floor/TASK.json @@ -0,0 +1,116 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Prove that the n - v + z unit-ADD floor of a target data block holds for every word on any number of added wires, whatever their initial or final contract, and apply it to the pinned PR5840 G20 boundary: no scratch wire, external wire or tariff lowers a legal GL(2)-commutant side below 38 unit ADDs.", + "scope_change_reason": "The card asks for a changed G20 helper path or target split. PR6641 leaves a narrower live question on the same boundary: whether one priced scratch wire, or a gate that leaves the 32 wires, lowers the 38-ADD side. That question is answered here for every number of extra wires. Helpers, targets and the recursive moment are unchanged.", + "bottleneck_link": "A cheaper boundary word would lower the scalar BIT conversion invoice. Workspace was the remaining unpriced route left by the scratch-free floors. It is closed for unit binary ADD words, so a BIT improvement on this boundary must change the target, the controller or the gate alphabet.", + "budget_minutes": 60, + "stop_rule": "Stop when the extended-wire floor is proved and bound to the pinned boundary. Do not search for nonlinear gates or changed output placements.", + "outcome": "negative-result", + "evidence": "PROOF in README.md; verify.py replays both pinned sides, eight extended-wire controls, a step-by-step potential check on 400 seeded random words with extra wires, and every state of GL(4, F2) against every data-wire subset.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a word that leaves the data on a different set of physical wires, charged for the consumer's relabelling, beat 76 ADDs per port?", + "why_it_matters": "The floor fixes the 32 output labels. Ending a side on scratch wires and relabelling the consumer is a different contract that this proof does not cover.", + "first_step": "Price the consumer-side relabel and compute n - v + z for the row-permuted data block of one side.", + "blocked_by": "Requires a caller contract that accepts relocated outputs." + }, + { + "question": "Does a nonlinear or non-unit gate (Toffoli, carry, multi-target XOR at one unit) lower either side?", + "why_it_matters": "The potential argument uses only two-wire XOR gates. A multi-target or controlled gate changes the alphabet and the bound.", + "first_step": "Fix one priced multi-target XOR tariff and redo the potential count on the four-wire exchange corner.", + "blocked_by": "No such gate is priced in the current native model." + } + ], + "predecessors": [ + { + "pr": 5840, + "author": "Ali Romman", + "relationship": "Controller, equal-target diagonal, and boundary programs used as the live input." + }, + { + "pr": 5851, + "author": "Charan .", + "relationship": "Vendored controller retained by the isolated-exchange package; not re-proved." + }, + { + "pr": 6081, + "author": "JoyboyBrian", + "relationship": "Fixed-endpoint 38-ADD theorem whose open GL2 question this package answers." + }, + { + "pr": 6105, + "author": "JoyboyBrian", + "relationship": "Full fixed-boundary 38-ADD floor with cross-component gates; scratch excluded there." + }, + { + "pr": 6641, + "author": "unpaidmoon", + "relationship": "GL(2)-commutant 38-ADD floor at head 5af623f5912f997163639e061feca4ebcf7e189e and the open question answered here. Cited, not replayed." + }, + { + "pr": 5898, + "author": "Nick Petalas", + "relationship": "One-clean-helper bank-exchange floor; the lemma here also covers its open two-helper question for the scalar floor." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376826" +} diff --git a/research/g20-extended-wire-boundary-floor/VERIFY.json b/research/g20-extended-wire-boundary-floor/VERIFY.json new file mode 100644 index 0000000000..edb96e64d1 --- /dev/null +++ b/research/g20-extended-wire-boundary-floor/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned boundary replay and floor 38, eight extended-wire controls, step-by-step potential on 400 seeded words with extra wires, and every GL(4, F2) state against every data subset." + } + ] +} diff --git a/research/g20-extended-wire-boundary-floor/verify.py b/research/g20-extended-wire-boundary-floor/verify.py new file mode 100644 index 0000000000..c8a52b5c81 --- /dev/null +++ b/research/g20-extended-wire-boundary-floor/verify.py @@ -0,0 +1,280 @@ +#!/usr/bin/env python3 +"""Extra wires cannot lower the n - v + z floor of a unit-ADD data block. + +Checks, in order: +1. The pinned PR5840 controller: both programs replay to the stored sides, + each has length 38, and each side's data-block floor n - v + z is 38. +2. Extended-wire controls on that boundary: words with a clean scratch wire, + a garbage scratch wire and a restored dirty external wire realize the same + 32-wire data block, cost more than 38, and respect the floor. +3. The potential invariant of the written proof, step by step, on seeded + random words with added wires. +4. A complete finite check at width four: every element of GL(4, F2), at its + exact unit-ADD distance, respects the floor for every choice of data wires. + +Standard library only. No file is written. +""" + +import hashlib +import json +import random +import sys +from collections import deque +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +CONTROLLER = ROOT / "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json" +CONTROLLER_SHA256 = "978536e852c0cfbc150f143e19d2cfddbb434bac6017d914974eb99f641593a8" +WIDTH = 32 +SIDE_FLOOR = 38 +RANDOM_WORDS = 400 +SEED = 20261103 + + +def require(ok, message): + if not ok: + raise SystemExit("FAIL: " + message) + + +def apply_word(word, wires): + rows = [1 << i for i in range(wires)] + for dest, source in word: + require(0 <= dest < wires and 0 <= source < wires and dest != source, "invalid gate") + rows[dest] ^= rows[source] + return rows + + +def expand_program(program): + word = [] + for op, dest, source in program: + require(op in ("ADD", "SWAP"), "unknown opcode") + if op == "ADD": + word.append((dest, source)) + else: + word.extend(((dest, source), (source, dest), (dest, source))) + return word + + +def data_block(rows, data): + """Top-left block on the listed data wires, re-indexed 0..len(data)-1.""" + block = [] + for r in data: + value = 0 + for j, c in enumerate(data): + if (rows[r] >> c) & 1: + value |= 1 << j + block.append(value) + return block + + +def floor_bound(block): + """n - v + z for a square binary block given as row bitmasks.""" + n = len(block) + parent = list(range(n)) + + def find(x): + while parent[x] != x: + parent[x] = parent[parent[x]] + x = parent[x] + return x + + for i in range(n): + for j in range(n): + if i != j and (block[i] >> j) & 1: + a, b = find(i), find(j) + if a != b: + parent[a] = b + v = len({find(i) for i in range(n)}) + z = sum(1 for i in range(n) if not (block[i] >> i) & 1) + return n - v + z + + +def check_controller(): + raw = CONTROLLER.read_bytes() + require(hashlib.sha256(raw).hexdigest() == CONTROLLER_SHA256, "controller hash changed") + boundary = json.loads(raw)["boundaries"] + words = {} + for side in ("left", "right"): + word = expand_program(boundary[side + "_program"]) + rows = apply_word(word, WIDTH) + require(rows == boundary[side + "_rows"], side + " program does not replay") + require(len(word) == SIDE_FLOOR, side + " word length is not 38") + require(floor_bound(rows) == SIDE_FLOOR, side + " floor is not 38") + words[side] = word + require(boundary["boundary_unit_ADDs_per_port"] == 2 * SIDE_FLOOR, "port invoice changed") + return boundary, words + + +def express(rows, target, wires): + """Return wire indices whose current rows XOR to target (Gaussian elimination).""" + basis = [] # (pivot row value, set of wires) + for w in wires: + value, combo = rows[w], {w} + for b_value, b_combo in basis: + if value ^ b_value < value: + value ^= b_value + combo ^= b_combo + if value: + basis.append((value, combo)) + basis.sort(key=lambda item: -item[0]) + value, combo = target, set() + for b_value, b_combo in basis: + if value ^ b_value < value: + value ^= b_value + combo ^= b_combo + require(value == 0, "target not in span") + return sorted(combo) + + +def relabel(word, old, new): + return [(new if d == old else d, new if s == old else s) for d, s in word] + + +def check_extended_controls(boundary, words): + """Each control realizes the same 32-wire data block on 33 wires; S = wire 32. + + clean: S starts at zero, copies x0, and is cleared from final data rows. + garbage: S starts at zero and ends holding x3. + relay: S starts at zero and carries wire 31's data through the whole word. + dirty: S holds unknown live data, carries wire 31 and is restored. + """ + data = list(range(WIDTH)) + s = WIDTH + full = (1 << WIDTH) - 1 + lengths = [] + for side in ("left", "right"): + target = boundary[side + "_rows"] + word = words[side] + final = apply_word(word, WIDTH) + clear = [(s, w) for w in express(final, 1, data)] + swap = [(s, 31), (31, s), (s, 31)] + controls = { + "clean": [(s, 0)] + word + clear, + "garbage": [(s, 3)] + word, + "relay": [(s, 31), (31, s)] + relabel(word, 31, s) + [(31, s), (s, 31)], + "dirty": swap + relabel(word, 31, s) + swap, + } + for name, control in controls.items(): + rows = apply_word(control, WIDTH + 1) + # Rows over 33 input coordinates; bit 32 is the extra wire's input. + require(data_block(rows, data) == target, side + " " + name + " data block differs") + if name in ("clean", "relay"): + require(rows[s] & full == 0, side + " " + name + " scratch not clean") + if name == "garbage": + require(rows[s] & full == 1 << 3, side + " garbage contents") + if name == "dirty": + require(rows[s] == 1 << s, side + " dirty wire not restored") + require(all(not (rows[r] >> s) & 1 for r in data), side + " dirty leak") + bound = floor_bound(data_block(rows, data)) + require(bound == SIDE_FLOOR < len(control), side + " " + name + " floor") + lengths.append(len(control)) + return lengths + + +def potential_run(word, wires, data): + """Check the written potential step by step; return final (bound, length).""" + rows = [1 << i for i in range(wires)] + parent = list(range(wires)) + + def find(x): + while parent[x] != x: + parent[x] = parent[parent[x]] + x = parent[x] + return x + + blocks = wires + zeros = 0 + for step, (dest, source) in enumerate(word, 1): + joins = find(dest) != find(source) + before = (rows[dest] >> dest) & 1 + if joins: + require(not (rows[source] >> dest) & 1, "cross-block entry before a join") + rows[dest] ^= rows[source] + after = (rows[dest] >> dest) & 1 + if joins: + require(before == after, "join changed a diagonal entry") + parent[find(dest)] = find(source) + blocks -= 1 + zeros += (before == 1 and after == 0) - (before == 0 and after == 1) + require(zeros == sum(1 for i in range(wires) if not (rows[i] >> i) & 1), "zero count") + # Support invariant: every nonzero entry lies inside one gate block. + for i in range(wires): + for j in range(wires): + if (rows[i] >> j) & 1: + require(find(i) == find(j), "entry crosses gate blocks") + require(wires - blocks + zeros <= step, "potential exceeds length") + block = data_block(rows, data) + return floor_bound(block), len(word) + + +def check_random_words(): + rng = random.Random(SEED) + tight = 0 + for _ in range(RANDOM_WORDS): + n = rng.randint(1, 6) + k = rng.randint(1, 3) + wires = n + k + length = rng.randint(0, 14) + word = [] + for _ in range(length): + d, s = rng.sample(range(wires), 2) + word.append((d, s)) + data = sorted(rng.sample(range(wires), n)) + bound, used = potential_run(word, wires, data) + require(bound <= used, "random word beats the floor") + tight += bound == used + return tight + + +def check_width_four(): + """Exact distances on GL(4, F2); every data subset of every state obeys the floor.""" + wires = 4 + start = tuple(1 << i for i in range(wires)) + dist = {start: 0} + queue = deque([start]) + gates = [(d, s) for d in range(wires) for s in range(wires) if d != s] + while queue: + state = queue.popleft() + for d, s in gates: + nxt = list(state) + nxt[d] ^= nxt[s] + nxt = tuple(nxt) + if nxt not in dist: + dist[nxt] = dist[state] + 1 + queue.append(nxt) + require(len(dist) == 20160, "GL(4, F2) order") + subsets = [[i for i in range(wires) if (mask >> i) & 1] for mask in range(1, 1 << wires)] + checks = 0 + best = {} + for state, d in dist.items(): + for data in subsets: + block = tuple(data_block(state, data)) + require(floor_bound(list(block)) <= d, "width-four state beats the floor") + checks += 1 + if len(data) < wires: + key = (len(data), block) + if key not in best or d < best[key]: + best[key] = d + # Statistic only: data blocks (widths one to three, the other wires as + # unrestricted extras) whose least exact distance equals the floor. + attained = sum(1 for (n, block), d in best.items() if floor_bound(list(block)) == d) + return len(dist), checks, len(best), attained + + +def main(): + require(sys.version_info[:2] == (3, 12), "CPython 3.12 required") + boundary, words = check_controller() + controls = check_extended_controls(boundary, words) + tight = check_random_words() + states, checks, blocks, attained = check_width_four() + print( + "PASS_G20_EXTENDED_WIRE_FLOOR side=38 port=76 witness=38/38 " + f"controls={len(controls)} control_lengths={sorted(set(controls))} " + f"random_words={RANDOM_WORDS} random_tight={tight} " + f"gl4_states={states} gl4_checks={checks} gl4_blocks={blocks} gl4_attained={attained} " + "no_new_kappa" + ) + + +if __name__ == "__main__": + main()