From d54576b126e39033e97d4ae34fd51ef9ff524281 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 10:13:19 +0000 Subject: [PATCH] feat(research): prove global thirteen-add fanout minimum --- research/global-thirteen-add-fanout/PROOF.md | 125 ++++++++++ research/global-thirteen-add-fanout/README.md | 146 ++++++++++++ .../global-thirteen-add-fanout/SOURCES.json | 24 ++ research/global-thirteen-add-fanout/TASK.json | 95 ++++++++ .../global-thirteen-add-fanout/VERIFY.json | 34 +++ research/global-thirteen-add-fanout/verify.py | 213 ++++++++++++++++++ 6 files changed, 637 insertions(+) create mode 100644 research/global-thirteen-add-fanout/PROOF.md create mode 100644 research/global-thirteen-add-fanout/README.md create mode 100644 research/global-thirteen-add-fanout/SOURCES.json create mode 100644 research/global-thirteen-add-fanout/TASK.json create mode 100644 research/global-thirteen-add-fanout/VERIFY.json create mode 100644 research/global-thirteen-add-fanout/verify.py diff --git a/research/global-thirteen-add-fanout/PROOF.md b/research/global-thirteen-add-fanout/PROOF.md new file mode 100644 index 0000000000..4b9acb79c7 --- /dev/null +++ b/research/global-thirteen-add-fanout/PROOF.md @@ -0,0 +1,125 @@ +# The global thirteen-ADD lower bound + +This scoped proof was produced by Nick Petalas. New work is Apache-2.0. + +## Statement + +Let A, B, C, X_i, Y_i, Z_i for i=1,2,3, and any finite number of +additional rows be arbitrary independent elements of F2^L, L>=1. Every +instruction is one paid row XOR r_d <- r_d + r_s, with d != s. Sources, +targets and additional rows may all be read or written in any order. There +are no free operations, clean initial rows or input-dependent instructions. +The endpoint preserves A, B, C and every additional row, and requires + + X_i' = X_i + A+B, + Y_i' = Y_i + A+B+C, + Z_i' = Z_i + A+C. + +Every such finite program has at least thirteen instructions. Consequently +Cinna Davis's thirteen-instruction construction in PR2271 is globally optimal +in this larger program class. The new result is the lower bound; that +construction and its earlier one-anchor optimality retain their original +credit. No predecessor executable or finite certificate is used in this proof. + +It suffices to prove the bound at L=1. Write each current row as a formal +binary linear combination of all original rows. These coefficient rows form +an invertible matrix at every cut, since each instruction is an elementary +row operation. In particular no current coefficient row is zero. + +## 1. Count incoming writes + +Let c_v count instructions whose destination is row v. Each of the nine +targets has c_v>=1, since its prescribed change is nonzero. Every unchanged +row has either c_v=0 or c_v>=2. Indeed, a row written exactly once has its +original value until that instruction, which adds a nonzero coefficient row; +its value then stays changed to the endpoint. + +Suppose the whole program has at most twelve instructions. There are at most +three writes beyond the nine mandatory target writes: + + sum_targets (c_v-1) + sum_unchanged c_v <= 3. (1) + +Call a target written exactly once light. At every cut a light target j is +either its original row e_j or its final row e_j+p_j, where p_j is its +prescribed source parity. Both have exactly the same coefficients on all +original nonsource rows. At its sole write, the input must be exactly p_j. +All prescribed parities have at least two source coordinates. + +## 2. Some original source must be written + +Suppose A, B and C are never written. Order them first. At every cut the +coefficient matrix has the block form + + [ I_3 0 ] + [ U V ], + +where V is invertible. Source-to-nonsource instructions leave V unchanged; +nonsource-to-nonsource instructions perform elementary row operations on V. +Thus every nonsource row has a nonzero coefficient on original nonsource +inputs. It can never equal a pure source parity. The three unchanged source +rows are single source coordinates, so they cannot supply p_j either. + +By (1), at most three targets are written more than once. There is a light +target, whose required input p_j is therefore unavailable. This contradiction +shows that at least one original source is written. + +## 3. Only one source can be written + +By (1) and the unchanged-row rule, exactly one original source a can be +written, and its write count m is either two or three. All additional rows +and the other two sources are never written. + +If m=3, all nine targets are light. Every row other than a is either an +unchanged original source coordinate, an unchanged additional dirty row, +or a light target. None can equal a prescribed pure parity. Hence a must +supply all three distinct parities A+B, A+B+C, A+C. + +But a starts and ends at its original single source coordinate. Three +writes give at most two intermediate values, so a cannot supply three +specified values distinct from its starting value. This excludes m=3. + +## 4. A twice-written target cannot supply the missing parity + +Now m=2. There is at most one non-light target t, with exactly two writes. +If it does not exist, only a could supply pure parities, and its one +intermediate value is insufficient. Suppose t exists. + +Let e_t be the coefficient of t's original dirty input. Every light target +and unchanged row other than a has e_t coefficient zero. Only a and t can +have that coefficient. If t ever holds a pure source value, this occurs +between its two writes. Its first write must cancel its original e_t, so +its input is a with e_t coefficient one. + +At that point at least one write into a has occurred. Both cannot already +have occurred, because a would then have its final original source value +and e_t coefficient zero. Thus exactly one write into a has occurred. That +write could have acquired e_t only by reading t. Since t has not yet been +written, it was still its bare original row e_t. Therefore + + a = a_original + e_t, + t_after_first_write = e_t + a = a_original. (2) + +Thus the only possible pure source value of t is the original single +source coordinate a_original. It is none of the required multi-source +parities. This argument permits arbitrary interleavings of all light-target +writes and does not assume a source-only tour. + +Only a can therefore supply a light target's prescribed input. Each parity +class has three targets, and at most one target is non-light, so every +class still has a light target. Row a would have to supply all three +parities. Its two writes give only one intermediate value distinct from +its original value. This is impossible. + +All programs of length at most twelve are excluded. The bound holds for +any finite dirty workspace and arbitrary target feedback. Combining it +with the credited thirteen-call construction proves the stated optimum. + +## Scope + +The argument is algebraic, with unit cost per whole-row XOR. It applies +bitwise at every positive common width. It does not optimize bit gates that +mix different coordinates inside a row. Clean initialization, arbitrary +free linear maps, nonlinear or input-dependent instructions, native calls, +physical layout, tape travel, precision and recursive prices are outside +this alphabet. No multiplication theorem, new kappa or supplier admission +follows. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/global-thirteen-add-fanout/README.md b/research/global-thirteen-add-fanout/README.md new file mode 100644 index 0000000000..6b4ffa0e1e --- /dev/null +++ b/research/global-thirteen-add-fanout/README.md @@ -0,0 +1,146 @@ +# Thirteen row ADDs are globally necessary for the PR2271 boundary + +This scoped mathematical proof was produced by Nick Petalas. Apache-2.0. + +Cinna Davis's [PR2271](https://github.com/CrocSwap/integer-mult-bounds/pull/2271) +gives a thirteen-ADD circuit for three copies each of the source parities +A+B, A+B+C and A+C. It proves optimality within one-anchor tours. The new +lower bound permits arbitrary CNOT ordering, target feedback and any finite +number of additional restored dirty rows. **Thirteen is still the minimum.** + +For arbitrary independent source and target rows over F2^L, L>=1, require + +```text +A, B, C and every additional row return unchanged; +X_i += A+B; Y_i += A+B+C; Z_i += A+C, i=1,2,3. +Every instruction is one paid r_d ^= r_s, d != s. +``` + +There are no free maps or clean initial rows. Every scalar row is an +independent arbitrary input. The new result is an unrestricted lower bound +inside this row-XOR alphabet. The upper construction is credited to PR2271 +and is cited without replaying its verifier or finite certificate. + +## Proof and evidence + +[PROOF.md](PROOF.md) gives the complete written argument. Nine target writes +are mandatory. An unchanged row cannot be written exactly once. A putative +twelve-gate circuit therefore has only three surplus writes. If no source +changes, an invertible dirty-input block excludes every needed pure parity. +Otherwise only one source changes, either twice or three times. The +three-write case has too few intermediate values. In the two-write case, +at most one target can be written twice; if that target becomes pure, its +only possible pure value is the original single source coordinate. It +cannot supply a missing multi-source parity. This exhausts the budget. + +The arbitrary-workspace conclusion is a written proof. The self-contained +verifier corroborates its lemmas on complete, explicitly finite domains: + +- All 168 invertible binary three-row bases and all 1,008 single CNOT + transitions change their destination row. +- All 55,987 words of length at most six on two fixed sources and two dirty + rows preserve the invertible dirty block, across 380,713 prefix visits. +- All 12,288 four-write words with two writes into A and two into T, over + eight frozen-row source offsets. Of these, 2,720 restore A. Their eight + pure intermediate T values are all the original single A coordinate. +- All 680 surplus allocations across nine targets, three sources and two + extra rows. The 275 allocations respecting the unchanged-row rule include + 33 with a changed source, all in the two cases used in the proof. +- All 219 closed pure-source itineraries with one through three writes, + allowing even zero as an intermediate state. None visits all three masks. + A four-write positive control does visit them. +- Interpreter-domain rejections and semantic controls distinguish missing + source restoration, a changed source and a singular dirty block. Exact + executed counts are emitted by the verifier. + +These are new lemma checks, not a census of twelve-gate programs, a replay +of PR2271 or a proof-kernel certificate. The program writes no files and +prints a generated receipt binding all six package files by SHA256. + +## Reproduce + +From the repository root, with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/global-thirteen-add-fanout/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/global-thirteen-add-fanout/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/global-thirteen-add-fanout +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/global-thirteen-add-fanout --check-source-history +``` + +Substitute another CPython 3.12 path on other machines. The direct marker is +`PASS_GLOBAL_THIRTEEN_ADD_LOWER_BOUND`; the registered and publication checks +report `PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +Run the last command after committing. Registered commands have independent +120-second timeouts. Direct replay also works without Git or repository +imports. Provenance documents are pinned historical inputs, not live +scientific dependencies. + +## Scope, overlap and credit + +Credit Cinna Davis / 1337isnot1337 for PR2271's exact boundary, borrowed-source +construction, complete restoration and earlier restricted optimality. Its +retained dirty-fanout and connector lineage remains credited in the unchanged +source. The new contribution is the incoming-write lower-bound argument, +its arbitrary-workspace application and the independent lemma corroboration. +Elementary binary linear algebra and CNOT circuits retain their classical +status; no global literature-priority claim is made. + +Nick Petalas's older [PR4899](https://github.com/CrocSwap/integer-mult-bounds/pull/4899) +prices weighted pair-mask tours; recent +[PR6427](https://github.com/CrocSwap/integer-mult-bounds/pull/6427) prices +fixed-weight tours. Both restrict the program to an anchor-tour alphabet. +This result changes that hypothesis to arbitrary row CNOTs and proves a +lower bound on PR2271's original boundary. It does not take another mask +family in those restricted models. + +The bit-helper-contract card is explicitly changed to this local algebraic +side result in [TASK.json](TASK.json). Canonical base is +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. +The selected-binding positive control passed for selected PR6030; it is +metadata orientation, not a selected scientific replay. +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371190). +Live PRs, recent account contributions, handoff claims, reservations, +all-main README and merged-PR searches were checked. Sparse notes, +unpublished work and arbitrary historical code diffs remain coverage limits. + +This does not supply a physical caller, bit-coordinate mixing optimum, +native implementation, routing/tape bound, precision/stock ledger, recursive +invoice, supplier admission, new kappa or selected-frontier change. All five +framework assumptions remain. Clean inputs, free basis changes, nonlinear +instructions and input-dependent programs are outside the theorem. No +predecessor scientific suite, selected cold replay, Lean or Docker build +was run. Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Does the minimum survive one initially clean, zero-return row? Begin with + this exact endpoint and charge initialization and restoration. The dirty + invertibility argument does not cover the changed initial condition. +- Can an actual supplier use this boundary after complete physical costs? + First identify a literal common-frame occurrence, then price its source + references, movement, native work and restoration. No such occurrence or + full recursive invoice is supplied here. + +Structured first steps and blockers are in TASK.json. No broader search is +needed to obtain this first strengthening. + +## Verifier bounds + +The interpreter caps rows at eight and word length at twelve. Exhaustive +word loops have respectively at most 6^6 and 8*6*4^4 iterations. Prefix +storage has at most thirteen states of eight coefficients. Every function +is below sixty physical lines; there is no recursion, subprocess, network, +dynamic execution or predecessor import. Explicit guards remain enabled +under optimization. Source reads are capped at 256 KiB for each of six +files. The direct command has no output-file path or mutable external state. +Warning-strict normal/optimized execution and source compilation are the +available Python diagnostics. + +Power of Ten rule 3 deviation: CPython and its standard library dynamically +allocate arithmetic values, tuples and iterator states. Scope is this +terminating, fixed-domain verifier. Fixed enumeration limits and one current +word bound live data; no allocator-internals or steady-service guarantee is +claimed. Both registered commands exercise the capacities and rejection +controls. A fixed-allocation runtime would be needed before reusing this +code under a no-allocation execution contract. diff --git a/research/global-thirteen-add-fanout/SOURCES.json b/research/global-thirteen-add-fanout/SOURCES.json new file mode 100644 index 0000000000..9b2afb94fe --- /dev/null +++ b/research/global-thirteen-add-fanout/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/borrowed-source-gray-mask-fanout-seed9b2fe133/README.md", + "usage": "provenance", + "git_blob": "32c2ea04e8e25c5a199861d8e0906127ffd9a5ce", + "sha256": "fb81510e09747ea2917318d23b667edaca28e09535b9a833e221672b9910f8f4" + } + ] +} diff --git a/research/global-thirteen-add-fanout/TASK.json b/research/global-thirteen-add-fanout/TASK.json new file mode 100644 index 0000000000..e5c7dc5907 --- /dev/null +++ b/research/global-thirteen-add-fanout/TASK.json @@ -0,0 +1,95 @@ +{ + "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": "Global lower bound of thirteen unit row XORs for the exact nine-target boundary of PR2271, allowing arbitrary CNOT order, target feedback and any finite restored dirty workspace.", + "scope_change_reason": "The card concerns a current G20 supplier path. This instead proves a local row-register obstruction beyond PR2271's one-anchor tour class. It is a side result, not a complete BIT improvement. Recent PR6427 remains restricted to anchor tours; the changed operation class here is essential.", + "bottleneck_link": "Closes a local transition-sharing route: changing the anchor-only schedule to arbitrary dirty row feedback cannot reduce this exact thirteen-call bill. No selected supplier uses this boundary here; no paid-profile or kappa change is inferred.", + "budget_minutes": 60, + "stop_rule": "Stop after the first global lower bound and bounded corroboration. Do not search other parity families or add a physical caller.", + "outcome": "completed", + "evidence": "PROOF.md proves the arbitrary-workspace lower bound. verify.py corroborates the one-write, fixed-source, two-write, surplus and itinerary lemmas on complete declared finite domains; it does not enumerate twelve-gate programs or replay the predecessor construction.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the thirteen-call minimum survive one initially clean, zero-return row?", + "why_it_matters": "The proof uses independent arbitrary dirt in every nonsource row. A clean role changes the algebraic invariant.", + "first_step": "State a fixed clean-role contract and test the same nine-target endpoint with all initialization and restoration charged.", + "blocked_by": "No lower bound or shorter construction in that changed alphabet is provided." + }, + { + "question": "Can an actual bit supplier exploit the exact thirteen-call boundary after physical costs?", + "why_it_matters": "The local row count alone does not improve the selected recursive invoice.", + "first_step": "Identify a literal common-frame occurrence and charge its source references, row routes, native calls and restoration.", + "blocked_by": "No selected caller occurrence or complete physical and recursive invoice is supplied." + } + ], + "predecessor": { + "pr": 2271, + "author": "1337isnot1337", + "head": "95fd439596f72575d3869277c2d01aca1ca6ab6a", + "result_used": "The thirteen-call upper construction and its exact boundary; credited rather than replayed." + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371190", + "overlap": { + "main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "checks": "Live open/account PRs and Discussion claims, local reservations, all-main README searches and merged-PR object/formula searches. PR4899 and PR6427 have restricted tour alphabets, without this global lower bound.", + "limits": "Sparse local notes, arbitrary historical code diffs, unpublished work and global literature priority are not covered." + } +} diff --git a/research/global-thirteen-add-fanout/VERIFY.json b/research/global-thirteen-add-fanout/VERIFY.json new file mode 100644 index 0000000000..2ff9738f73 --- /dev/null +++ b/research/global-thirteen-add-fanout/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact finite corroboration of the new lower-bound lemmas and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete domains with optimization enabled and explicit runtime guards." + } + ] +} diff --git a/research/global-thirteen-add-fanout/verify.py b/research/global-thirteen-add-fanout/verify.py new file mode 100644 index 0000000000..fd385a7b6d --- /dev/null +++ b/research/global-thirteen-add-fanout/verify.py @@ -0,0 +1,213 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the new low-overhead lower-bound lemmas.""" + +import hashlib +import itertools +import json +import platform +from pathlib import Path + + +FILES = ('README.md', 'PROOF.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def replay(initial, word): + """Bounded formal-row interpreter, with explicit checks under -O.""" + n = len(initial) + require(2 <= n <= 8, 'row capacity') + require(len(word) <= 12, 'word capacity') + require(all(type(x) is int and 0 < x < 1 << n for x in initial), 'row domain') + require(rank(initial, n) == n, 'initial coefficient matrix') + rows = list(initial) + states = [tuple(rows)] + for gate in word: + require(type(gate) is tuple and len(gate) == 2, 'gate shape') + d, s = gate + require(type(d) is int and type(s) is int, 'gate type') + require(0 <= d < n and 0 <= s < n and d != s, 'gate indices') + rows[d] ^= rows[s] + states.append(tuple(rows)) + return states + + +def rank(rows, n): + require(1 <= n <= 8 and len(rows) <= 8, 'rank capacity') + pivots = [0] * n + result = 0 + for original in rows: + x = original + for bit in range(n - 1, -1, -1): + if not x >> bit & 1: + continue + if pivots[bit]: + x ^= pivots[bit] + else: + pivots[bit] = x + result += 1 + break + return result + + +def one_write_check(): + """Every nonzero CNOT input changes its destination in all GL3 bases.""" + bases = transitions = 0 + for rows in itertools.product(range(1, 8), repeat=3): + if rank(rows, 3) != 3: + continue + bases += 1 + for d, s in itertools.permutations(range(3), 2): + end = replay(rows, ((d, s),))[-1] + require(end[d] != rows[d], 'single incoming write returned unchanged') + transitions += 1 + require(bases == 168 and transitions == 1008, 'GL3 enumeration') + return {'bases': bases, 'transitions': transitions} + + +def fixed_source_check(): + """Complete words through six gates on two sources and two dirty rows.""" + alphabet = tuple((d, s) for d in (2, 3) for s in range(4) if s != d) + words = cuts = 0 + for length in range(7): + for word in itertools.product(alphabet, repeat=length): + states = replay((1, 2, 4, 8), word) + for rows in states: + require(rows[:2] == (1, 2), 'source changed') + x, y = rows[2] >> 2, rows[3] >> 2 + determinant = (x & 1) * (y >> 1 & 1) ^ (x >> 1 & 1) * (y & 1) + require(determinant == 1, 'dirty block not invertible') + require(x != 0 and y != 0, 'pure source row appeared') + cuts += 1 + words += 1 + require(words == sum(6 ** j for j in range(7)), 'word coverage') + return {'words': words, 'cuts': cuts} + + +def twice_written_check(): + """All 2+2 writes on A,T, with three frozen external rows.""" + words = restored = pure = 0 + orders = tuple(sorted(set(itertools.permutations((0, 0, 1, 1))))) + source_choices = tuple(tuple(s for s in range(5) if s != d) for d in (0, 1)) + for p in range(8): + source_part = (p & 1) | ((p >> 1 & 1) << 2) | ((p >> 2 & 1) << 3) + initial = (1, 2, 4, 8, 16 | source_part) + for order in orders: + for choices in itertools.product(range(4), repeat=4): + word = tuple((d, source_choices[d][q]) for d, q in zip(order, choices)) + states = replay(initial, word) + words += 1 + if states[-1][0] != 1: + continue + restored += 1 + after_first_t = states[order.index(1) + 1][1] + if after_first_t & 18 == 0: + require(after_first_t == 1, 'twice-written target supplied a parity') + pure += 1 + require(words == 8 * 6 * 4 ** 4, 'two-write coverage') + require(pure > 0, 'pure-intermediate case was not exercised') + return {'words': words, 'restored_source': restored, 'pure_intermediates': pure} + + +def budget_check(): + """Enumerate surplus allocations for nine targets, three sources, two extras.""" + profiles = valid = with_source = 0 + for surplus in range(4): + for destinations in itertools.combinations_with_replacement(range(14), surplus): + counts = [0] * 14 + for d in destinations: + counts[d] += 1 + profiles += 1 + if any(counts[d] == 1 for d in range(9, 14)): + continue + valid += 1 + changed_sources = [d for d in range(9, 12) if counts[d]] + if not changed_sources: + require(sum(counts[:9]) <= 3, 'no-source surplus') + continue + with_source += 1 + require(len(changed_sources) == 1, 'two changed sources fit the budget') + m = counts[changed_sources[0]] + require(m in (2, 3) and counts[12:] == [0, 0], 'source case classification') + require(sum(counts[:9]) <= 3 - m, 'remaining target writes') + return {'profiles': profiles, 'valid_profiles': valid, 'source_profiles': with_source} + + +def itinerary_check(): + """Relaxation allows every pure source mask, including zero, at each cut.""" + required = {3, 5, 7} + cases = 0 + for anchor in (1, 2, 4): + for writes in (1, 2, 3): + for middle in itertools.product(range(8), repeat=writes - 1): + states = (anchor,) + middle + (anchor,) + require(not required.issubset(states), 'short closed itinerary covered all parities') + cases += 1 + require(cases == 219, 'itinerary coverage') + require(required.issubset((1, 3, 7, 5, 1)), 'four-write boundary control') + return {'closed_itineraries': cases, 'four_write_control': 1} + + +def controls(): + bad = ( + ((1,), ()), + ((1, 2), ((0, 0),)), + ((1, 2), ((2, 0),)), + ((1, 2), ((True, 0),)), + ((1, 0), ()), + ((1, 1), ()), + ((1, 2), ((0, 1, 0),)), + ((1, 2), ((0, 1),) * 13), + ) + rejected = 0 + for initial, word in bad: + try: + replay(initial, word) + except ValueError: + rejected += 1 + else: + raise ValueError('invalid interpreter input accepted') + require(rejected == len(bad), 'rejection count') + leaking = replay((1, 2, 4, 8), ((0, 1), (0, 2), (1, 0), (1, 3))) + require(leaking[-1][0] != 1 and leaking[3][1] == 5, 'restoration discriminator') + coded = replay((1, 2, 4), ((0, 1), (2, 0))) + require(coded[-1][2] == 7, 'fixed-source premise discriminator') + require(rank((1, 1), 2) == 1, 'dirty singularity discriminator') + return {'invalid_inputs_rejected': rejected, 'semantic_controls': 3} + + +def receipt_hashes(): + root = Path(__file__).resolve().parent + hashes = {} + for name in FILES: + with (root / name).open('rb') as stream: + payload = stream.read(262145) + require(len(payload) <= 262144, 'receipt file capacity') + hashes[name] = hashlib.sha256(payload).hexdigest() + return hashes + + +def main(): + counts = { + 'one_write': one_write_check(), + 'fixed_sources': fixed_source_check(), + 'twice_written': twice_written_check(), + 'surplus': budget_check(), + 'itineraries': itinerary_check(), + 'controls': controls(), + } + print(json.dumps({ + 'status': 'PASS_GLOBAL_THIRTEEN_ADD_LOWER_BOUND', + 'claim_type': 'scoped written proof; finite lemma corroboration', + 'lower_bound': 13, + 'counts': counts, + 'python': platform.python_version(), + 'sha256': receipt_hashes(), + }, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()