From 133ab618a11c17b2b90ad5c1dba97bff8048a8c0 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 11:22:30 +0000 Subject: [PATCH] feat(research): exclude scratch-reading two-FULL completions --- .../scratch-reading-full-obstruction/PROOF.md | 134 ++++++++++ .../README.md | 100 ++++++++ .../SOURCES.json | 30 +++ .../TASK.json | 81 +++++++ .../VERIFY.json | 34 +++ .../verify.py | 228 ++++++++++++++++++ 6 files changed, 607 insertions(+) create mode 100644 research/scratch-reading-full-obstruction/PROOF.md create mode 100644 research/scratch-reading-full-obstruction/README.md create mode 100644 research/scratch-reading-full-obstruction/SOURCES.json create mode 100644 research/scratch-reading-full-obstruction/TASK.json create mode 100644 research/scratch-reading-full-obstruction/VERIFY.json create mode 100644 research/scratch-reading-full-obstruction/verify.py diff --git a/research/scratch-reading-full-obstruction/PROOF.md b/research/scratch-reading-full-obstruction/PROOF.md new file mode 100644 index 0000000000..63e36fbbcd --- /dev/null +++ b/research/scratch-reading-full-obstruction/PROOF.md @@ -0,0 +1,134 @@ +# Two FULL shears on arbitrary owners retain a low-grade image + +This is a scoped algebraic proof, produced by Nick Petalas. It answers the +scratch-reading follow-up in unpaidmoon's [PR #5843](https://github.com/CrocSwap/integer-mult-bounds/pull/5843). +The changed hypothesis is the location of each elementary shear. Either +source or destination may now be any owner, including an identity scratch +owner. No physical realization of that larger macro is assumed. + +## Statement + +Let A be a unital algebra over a field K and B a unital subalgebra with +finite positive dimension d over K. Let F_r be increasing K-linear +subspaces of A with B contained in F_0, B F_r B contained in F_r, and +F_r F_s contained in F_(r+s). Fix nonnegative s,t and a K-linear +B-bimodule projection pi on A which fixes every element of F_(s+t). + +There are n >= 2 owners. Allow arbitrary L,W,R in GL_n(B). Let + + D1 = diag(a_0,...,a_(n-1)), a_i in F_s and a_i a unit of A, + D2 = diag(b_0,...,b_(n-1)), b_i in F_t and b_i a unit of A. + +Choose any distinct p_1,q_1 and any distinct p_2,q_2 from the n owners. +The two elementary shears and FULL factors are + + E1 = I + e_(p_1) c_1 e_(q_1)^T, T1 = D1 E1, + E2 = I + e_(p_2) c_2 e_(q_2)^T, T2 = D2 E2, + +where c_1,c_2 are arbitrary elements of A. They need not be central, pure +words, or invertible. Neither coefficient has a grade bound. Matrix +products act on columns from right to left. + +Apply pi entrywise, and regard pi(L T2 W T1 R) as a K-linear map from +B^n to A^n by left multiplication. Then + + rank_K pi(L T2 W T1 R) >= (n-1)d. (1) + +In particular, if pi(g_0)=pi(g_1)=0, this word cannot equal + + J = diag(g_0,g_1,I,...,I), + +because rank_K pi(J)=(n-2)d. The statement requires arbitrary initial +scratch inputs and their identity endpoint. It grants reads and writes +of those inputs inside either shear. + +## Proof + +Set S = {x in B^n : x_(q_1)=0}. It has dimension (n-1)d. On this exact +subspace E1 x=x, regardless of whether q_1 is main or scratch. Therefore +u=W D1 x has every coordinate in F_s. Also x -> u is injective, since +D1 is invertible over A and W is invertible over B and hence over A. + +Suppose pi(D2 E2 u)=0. Row q_2 is untouched by E2 since p_2 != q_2. +Its output is b_(q_2) u_(q_2), which lies in F_(s+t). The projection fixes +this element, so its vanishing forces u_(q_2)=0 because b_(q_2) is a unit. +This kills the entire c_2 u_(q_2) term. Every remaining output is now +b_i u_i, again in F_(s+t). Projected vanishing forces all u_i=0. Thus +pi(T2 W T1) is injective on S and has rank at least (n-1)d. + +Finally the bimodule property gives + + pi(L T2 W T1 R) = L pi(T2 W T1) R. + +Right multiplication by R is an automorphism of the domain B^n. Left +multiplication by L is an automorphism of the codomain A^n. Both preserve +the K-rank. This proves (1). Since pi fixes B, the displayed target has +exactly the scratch image B^(n-2), proving its exclusion. + +No commutation, positivity, domain property, or inverse grade bound is +used. In particular B may have zero divisors. The free subspace is chosen +using the actual first read coordinate, which removes any need for the +main-only endpoint restriction on the two shears. + +## Sharpness and hypothesis controls + +When a unit g satisfies pi(g)=pi(g^-1)=0, take D1=D2=I and W=I. On any +two owners choose E1=I+e_1 g e_0^T and E2=I-e_0 g^-1 e_1^T. The exact +two-owner product is + + E2 E1 = [[0,-g^-1],[g,1]]. + +Its projection has rank d on those owners and identity on the others. +Thus the uniform lower bound (n-1)d is attained. The labels 0,1 in this +example can be replaced by any distinct owner indices, including scratch. +This equality example is elementary algebra and is not a native construction. + +The unit condition, the cutoff s+t, and W in GL_n(B) are essential to this +argument. Setting D1=0 destroys the bound. Two grade-one factors on +different coordinates can have grade two, so cutoff one cannot retain +them. A high-grade diagonal W outside Mat_n(B) can make the entire +projected map vanish. Three queries can attain diag(g,g^-1), after a +scalar signed swap, through the usual three-shear identity. These are +explicit controls of the theorem's hypotheses, not new optimization claims. + +## Application to the cited FULL boundary + +Chris R / Clear1nsight's [PR #4920](https://github.com/CrocSwap/integer-mult-bounds/pull/4920) +supplies the full-monomial Clifford grade model and its tensor-separation +lemma. unpaidmoon's #5843 supplies the main-only two-shear rank argument +with identity scratch and explicitly asks about a scratch-reading shear. +The contribution here removes that restriction by choosing S using q_1. +No predecessor numerical result is replayed or recertified. + +For that model, take B to be the full monomial subgroup algebra and F_r +the span of words of Fourier grade at most r. These spaces have the +required bimodule and product properties. Use s=t=8 and pi=pi_(<=16). +The actual diagonal transverse factors have grade eight on main owners +and identity on scratch, so they satisfy the hypotheses even when the +new shear touches scratch. Two pure grade-17 main targets with restored +identity scratch remain impossible in this enlarged algebraic class. + +The cited separation lemma transfers the obstruction to every sufficiently +large tensor width in the fixed finite columnwise alphabet. This use is +conditional on the predecessor's stated grade and separation premises. +It supplies no new width bound, literal native implementation, or claim +about accidental relations at small widths. + +thu-nmrc's [PR #5200](https://github.com/CrocSwap/integer-mult-bounds/pull/5200) +is a different extension. It covers joint native main banks and identity +scratch, with possibly dense query blocks confined to the main owners. +The present result permits scratch in either single-coordinate query; +it does not extend #5200's multiple-query block theorem to scratch blocks. +Credit its joint-bank result and the retained Cinna Davis, Cao Yifan, +zxv, Jacob Alan Sussman, Ali Romman, Dugongue and native/compiler lineage. + +## Evidence limits + +The executable is a fresh finite group-algebra example, not a Clifford +operator replay. Its complete declared owner-pair enumeration corroborates +the new coordinate freedom. The written argument proves the arbitrary +field and owner-count statement. Neither is proof-kernel verification. +Productive transformed helpers, clean COPY/CLEAR, noninvertible controls, +new query blocks, changed transverse grades and noncolumnwise operations +require their own analysis. No invoice, supplier admission, new kappa, or +complete multiplication theorem is claimed. diff --git a/research/scratch-reading-full-obstruction/README.md b/research/scratch-reading-full-obstruction/README.md new file mode 100644 index 0000000000..a5b03d0dbd --- /dev/null +++ b/research/scratch-reading-full-obstruction/README.md @@ -0,0 +1,100 @@ +# Scratch access does not rescue two elementary FULL shears + +This scoped algebraic proof is produced by Nick Petalas. It answers the +scratch-reading follow-up in unpaidmoon's +[PR #5843](https://github.com/CrocSwap/integer-mult-bounds/pull/5843). +Either shear may read or write any owner, including dirty scratch. Under +the stated low-grade transverse and free-control hypotheses, its projected +image still has rank at least `(n-1) dim B`. Two pure high-grade targets +with restored identity scratch have rank only `(n-2) dim B`, so remain +impossible. No new kappa is claimed. + +[PROOF.md](PROOF.md) states and proves the more general filtered-algebra +theorem. The new step chooses the first read-coordinate kernel regardless +of which owner the shear reads. It requires no commutation or domain +property. Its lower bound is sharp in the declared algebraic class. + +## Reproduce + +From the repository root, use CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/scratch-reading-full-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/scratch-reading-full-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/scratch-reading-full-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/scratch-reading-full-obstruction --check-source-history +``` + +The standalone command prints `PASS_SCRATCH_READING_FULL_OBSTRUCTION` in +its JSON result. Both registered checks run the same finite domain under +normal and optimized execution. They write nothing into the checkout. + +## Finite evidence + +The checker constructs `F2[S3^3]`, dimension 216, with the dimension-eight +subgroup algebra of `{identity,(01)}^3`. Grade counts coordinates outside +that subgroup. The projection retains grades at most two. Diagonal units +have grade at most one. The two target units have grade three. + +Every ordered pair of distinct first-shear owners and every ordered pair +of distinct second-shear owners is checked for each of four explicit +coefficient/diagonal/free-control fixtures, at n=2,3,4. This gives 736 +cases, including 512 with a scratch read, 512 with a scratch write and +176 with a scratch-to-scratch shear. The categories overlap. In 368 cases +the diagonal transverse factors remain identity on scratch, as in the +predecessor's setup; the rest exercise the theorem's wider diagonal class. +These are fixed fixtures, not every group-algebra coefficient or control. + +Direct binary elimination finds full projected rank in all 736 cases: +16 cases at rank 16, 144 at rank 24 and 576 at rank 32. It separately +checks rank `(n-1)*8` on the actual first-read kernel, the projected target, +and whole maps with outer subgroup-algebra controls. Bitset coefficients +lift to integral group-algebra coefficients. Full rank modulo two also +certifies full rational rank for those lifted whole-word fixtures. + +Separate equality examples attain the sharp `(n-1)*8` lower bound. The +controls exercise a too-low cutoff, a nonfree middle matrix, a nonunit +diagonal and an additional third query, plus noncommutativity, a nonzero +nilpotent free coefficient and a rejected same-owner shear. +The runtime JSON is generated from the arithmetic and records its scope. + +## Sources and limits + +The exact question source is #5843, pinned in [TASK.json](TASK.json). +[SOURCES.json](SOURCES.json) pins the main-branch grade proof from Chris R / +Clear1nsight #4920 and the distinct joint-bank theorem of thu-nmrc #5200 +as provenance. They are cited premises, not audited deliverables or runtime +imports. Credit unpaidmoon for the question and clean-output argument, +Chris R / Clear1nsight for the full-monomial grade framework, thu-nmrc for +joint-main-bank stability, and their retained predecessor lineage. + +The finite checker uses a small untwisted group algebra. It does not +reconstruct the physical Clifford macro. The written proof covers twisted +algebras when the stated filtration and bimodule hypotheses hold. The +source application's all-large-width implication uses #4920's separation +lemma. No new sufficient width, native/compiler/precision/tape/outer replay, +formal proof-kernel review, or independent human acceptance is claimed. +The selected frontier is unchanged. New material is Apache-2.0. + +The chosen card's baseline command passed source-binding orientation. +The actual scope changes from helper construction to the explicit +scratch-access obstruction, as recorded in TASK.json. This rules out one +escape before anyone pays for a larger native or invoice search. + +## Open next questions + +Can a changed FULL macro with two independent query source coordinates +evade this obstruction at a favorable complete tariff? First specify a +legal macro and its complete target, transverse, restoration and paid-call +contract, then compute its projected image. The proof uses one read +coordinate per shear. No physical macro or complete invoice for that +changed premise is supplied here. TASK.json records the same question. + +## Engineering notes + +The verifier has no recursion, dynamic code generation or external +dependencies. Its fixed algebra has 216 basis elements, at most four owners +and at most 32 domain columns. All loops are bounded by these declarations +or finite case products. Python requires dynamic integer and collection +allocation; those dimensions bound live data. Each function is below 60 +lines. Acceptance uses explicit exceptions and remains active under `-O`. diff --git a/research/scratch-reading-full-obstruction/SOURCES.json b/research/scratch-reading-full-obstruction/SOURCES.json new file mode 100644 index 0000000000..691a6d6169 --- /dev/null +++ b/research/scratch-reading-full-obstruction/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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/two-full-central-obstruction/grade/PROOF.md", + "usage": "provenance", + "git_blob": "4cdf1e1a29b2113e88513f7a7d983f1e52adb6db", + "sha256": "8fd775a9903eca0f53b186d7fb684d9f5f74afc9c105082b3d4981bd950fca33" + }, + { + "path": "research/two-full-dirty-stability/PROOF.md", + "usage": "provenance", + "git_blob": "fc8bbd4cfc9bf5b349aecaa8b87740d1a23144d5", + "sha256": "5c9331d51246ec9f3c6aabcb11b25eb6e438a3db4aee15cb61a9d24f55bfdf2f" + } + ] +} diff --git a/research/scratch-reading-full-obstruction/TASK.json b/research/scratch-reading-full-obstruction/TASK.json new file mode 100644 index 0000000000..a11ae7dfae --- /dev/null +++ b/research/scratch-reading-full-obstruction/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?", + "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" + ], + "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 source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "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": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "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": "A low-grade projected-rank obstruction for two elementary FULL shears on arbitrary owner pairs, including scratch reads and writes.", + "scope_change_reason": "The donation assignment requests an original result rather than auditing predecessors. This answers the scratch-reading question in PR5843, changing its main-only shear hypothesis while retaining identity scratch at the endpoint.", + "bottleneck_link": "Scratch access cannot rescue two FULLs with low-grade diagonal transverse factors and monomial-algebra controls. A proposed escape must change another named hypothesis before native or invoice development.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved scratch-reading extension after exact finite corroboration; do not optimize or expand the construction.", + "outcome": "completed", + "evidence": "PROOF.md gives the arbitrary-field filtered-algebra theorem. verify.py enumerates the declared finite group-algebra fixtures and checks projected ranks directly.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a changed FULL macro with two independent query source coordinates evade this obstruction at a favorable complete tariff?", + "why_it_matters": "The proof uses one source coordinate per shear. A higher-dimensional query block changes that hypothesis.", + "first_step": "Specify one legal macro and its complete target, transverse, restoration and paid-call contract before testing its projected image.", + "blocked_by": "No source-bound physical macro or complete invoice is supplied here." + } + ], + "claim_type": "scoped proof", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19215589", + "question_source": { + "pr": 5843, + "head": "050b99f3f355a83f90189218c4c95c8131f8a991", + "question": "One FULL shear that reads a scratch owner, with its projected image." + } +} diff --git a/research/scratch-reading-full-obstruction/VERIFY.json b/research/scratch-reading-full-obstruction/VERIFY.json new file mode 100644 index 0000000000..d3ad4e6e6e --- /dev/null +++ b/research/scratch-reading-full-obstruction/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Direct finite group-algebra projected ranks for every declared owner pair, sharpness and hypothesis rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same finite arithmetic and controls with assertions disabled." + } + ] +} diff --git a/research/scratch-reading-full-obstruction/verify.py b/research/scratch-reading-full-obstruction/verify.py new file mode 100644 index 0000000000..6d2b9f4a10 --- /dev/null +++ b/research/scratch-reading-full-obstruction/verify.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Finite corroboration in F2[S3^3], with no predecessor imports or writes. + +The written proof is universal. Live allocation is bounded by the fixed +216-element algebra, four owners, and 736 explicitly enumerated cases. +""" +from itertools import permutations, product +from hashlib import sha256 +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def algebra(): + perms = tuple(permutations(range(3))) + mul6 = tuple(tuple(perms.index(tuple(a[b[i]] for i in range(3))) + for b in perms) for a in perms) + words = tuple(product(range(6), repeat=3)) + index = {word: i for i, word in enumerate(words)} + table = tuple(tuple(index[tuple(mul6[a[k]][b[k]] for k in range(3))] + for b in words) for a in words) + # permutations[2] is (1,0,2); these two elements form a subgroup. + h = tuple(i for i, w in enumerate(words) if all(x in (0, 2) for x in w)) + grades = tuple(sum(x not in (0, 2) for x in w) for w in words) + keep = sum(1 << i for i, grade in enumerate(grades) if grade <= 2) + need(len(words) == 216 and len(h) == 8, "wrong algebra dimensions") + return words, table, h, grades, keep + + +def support(value): + need(type(value) is int and 0 <= value < (1 << 216), "invalid algebra element") + return tuple(i for i in range(value.bit_length()) if value >> i & 1) + + +def mul(a, b, table): + answer = 0 + for i in support(a): + for j in support(b): + answer ^= 1 << table[i][j] + return answer + + +def shear(vector, dst, src, coefficient, table): + need(0 <= dst < len(vector) and 0 <= src < len(vector) and dst != src, + "invalid shear endpoints") + out = list(vector) + out[dst] ^= mul(coefficient, vector[src], table) + return tuple(out) + + +def diagonal(vector, units, table): + need(len(vector) == len(units), "wrong diagonal size") + return tuple(mul(1 << unit, entry, table) for unit, entry in zip(units, vector)) + + +def free(vector, variant, h, table): + n = len(vector) + out = vector + for k in range(2 * n): + src = (k + variant) % n + dst = (src + 1 + k % (n - 1)) % n + # Elementary controls stay invertible with zero-divisor coefficients. + coefficient = (1 << h[(k + variant) % 8]) ^ (1 << h[(k + 3) % 8]) + out = shear(out, dst, src, coefficient, table) + return out[variant % n:] + out[:variant % n] + + +def packed(vector, keep): + return sum((entry & keep) << (216 * i) for i, entry in enumerate(vector)) + + +def binary_rank(columns): + need(len(columns) <= 32, "rank capacity exceeded") + basis = {} + for original in columns: + value = original + for _ in range(32): + if not value: + break + pivot = value.bit_length() - 1 + if pivot not in basis: + basis[pivot] = value + break + value ^= basis[pivot] + else: + need(not value, "elimination capacity exhausted") + return len(basis) + + +def fixture(n, first, second, variant, context): + words, table, h, grades, keep = context + low = tuple(i for i, g in enumerate(grades) if g == 1) + high = tuple(i for i, g in enumerate(grades) if g == 3) + d1 = tuple(low[(7 * i + variant) % 48] if i < 2 or variant & 1 else 0 + for i in range(n)) + d2 = tuple(low[(11 * i + 5 + variant) % 48] if i < 2 or variant & 1 else 0 + for i in range(n)) + q1 = 1 << high[variant] + q2 = (1 << high[variant + 2]) ^ (1 << low[variant + 9]) + if variant & 2: + q1 ^= 1 << low[variant + 1] + columns, restricted, outer = [], [], [] + for owner, b in product(range(n), h): + vector = tuple((1 << b) if i == owner else 0 for i in range(n)) + mid = shear(vector, *first, q1, table) + mid = free(diagonal(mid, d1, table), variant, h, table) + out = diagonal(shear(mid, *second, q2, table), d2, table) + columns.append(packed(out, keep)) + if owner != first[1]: + restricted.append(packed(out, keep)) + # A separately executed whole map includes outer B-controls. + mid = free(vector, variant + 1, h, table) + mid = diagonal(shear(mid, *first, q1, table), d1, table) + mid = free(mid, variant, h, table) + mid = diagonal(shear(mid, *second, q2, table), d2, table) + outer.append(packed(free(mid, variant + 2, h, table), keep)) + floor = (n - 1) * len(h) + need(binary_rank(restricted) == floor, "restriction is not injective") + rank = binary_rank(columns) + need(rank >= floor, "projected rank below theorem bound") + need(binary_rank(outer) == rank, "outer B-control changed projected rank") + target = [] + for owner, b in product(range(n), h): + entry = mul(1 << high[0], 1 << b, table) if owner < 2 else 1 << b + target.append(packed(tuple(entry if i == owner else 0 for i in range(n)), keep)) + need(binary_rank(target) == (n - 2) * len(h), "wrong target image") + return rank + + +def controls(context): + words, table, h, grades, keep = context + g = words.index((1, 1, 1)) + inverse = next(i for i in range(216) if table[g][i] == table[i][g] == 0) + a, b = words.index((1, 0, 0)), words.index((0, 1, 0)) + lowkeep = sum(1 << i for i, grade in enumerate(grades) if grade <= 1) + checked = [] + for n in (2, 3, 4): + columns, below, nonfree, nonunit, three = [], [], [], [], [] + for owner, x in product(range(n), h): + v = tuple((1 << x) if i == owner else 0 for i in range(n)) + z = shear(shear(v, 1, 0, 1 << g, table), 0, 1, 1 << inverse, table) + columns.append(packed(z, keep)) + z = diagonal(diagonal(v, (a,) * n, table), (b,) * n, table) + below.append(packed(z, lowkeep)) + nonfree.append(packed(diagonal(v, (g,) * n, table), keep)) + nonunit.append(packed(tuple(0 for _ in v), keep)) + # A third query and a scalar owner swap attain two high targets. + z = shear(shear(shear(v, 0, 1, 1 << g, table), + 1, 0, 1 << inverse, table), 0, 1, 1 << g, table) + z = (z[1], z[0]) + z[2:] + three.append(packed(z, keep)) + need(binary_rank(columns) == (n - 1) * 8, "sharpness fixture failed") + need(binary_rank(below) == 0, "cutoff control failed") + need(binary_rank(nonfree) == 0, "non-B control failed") + need(binary_rank(nonunit) == 0, "nonunit control failed") + need(binary_rank(three) == (n - 2) * 8, "third-query control failed") + checked.extend(f"n{n}:{name}" for name in + ("sharpness", "cutoff", "nonfree", "nonunit", "third_query")) + nilpotent = 1 ^ (1 << h[1]) + need(nilpotent != 0 and mul(nilpotent, nilpotent, table) == 0, + "zero-divisor control failed") + p, q = words.index((1, 0, 0)), words.index((2, 0, 0)) + need(table[p][q] != table[q][p], "noncommutative control failed") + checked.extend(("nilpotent_free_coefficient", "noncommutativity")) + try: + shear((1, 1), 0, 0, 1, table) + except ValueError: + checked.append("same_owner_rejected") + return checked + raise ValueError("diagonal shear was accepted") + + +def arithmetic_checks(context): + _, table, h, grades, _ = context + products_checked = 0 + for a, b in product(range(216), repeat=2): + need(grades[table[a][b]] <= grades[a] + grades[b], "grade is not subadditive") + if a in h: + need(grades[table[a][b]] == grades[b], "left B-invariance failed") + if b in h: + need(grades[table[a][b]] == grades[a], "right B-invariance failed") + products_checked += 1 + matrices_checked = 0 + for rows, cols in product(range(4), repeat=2): + for bits in range(1 << (rows * cols)): + columns = tuple((bits >> (rows * i)) & ((1 << rows) - 1) + for i in range(cols)) + span = {0} + for column in columns: + span = span | {x ^ column for x in span} + need(len(span) == 1 << binary_rank(columns), "rank/span oracle disagrees") + matrices_checked += 1 + return {"grade_products": products_checked, "rank_oracle_matrices": matrices_checked} + + +def verify(): + context = algebra() + counts = {"cases": 0, "scratch_read": 0, "scratch_write": 0, + "scratch_to_scratch": 0, "original_transverse_placement": 0} + histogram = {} + for n in (2, 3, 4): + pairs = tuple((i, j) for i, j in product(range(n), repeat=2) if i != j) + for first, second, variant in product(pairs, pairs, range(4)): + rank = fixture(n, first, second, variant, context) + counts["cases"] += 1 + counts["scratch_read"] += first[1] >= 2 or second[1] >= 2 + counts["scratch_write"] += first[0] >= 2 or second[0] >= 2 + counts["scratch_to_scratch"] += min(first) >= 2 or min(second) >= 2 + counts["original_transverse_placement"] += not variant & 1 + key = f"n{n}:rank{rank}" + histogram[key] = histogram.get(key, 0) + 1 + need(counts["cases"] == 736, "incomplete owner-pair enumeration") + checked = controls(context) + result = {"status": "PASS_SCRATCH_READING_FULL_OBSTRUCTION", **counts, + "algebra_dimension": 216, "subgroup_dimension": 8, + "controls": len(checked), "control_names": checked, + "rank_histogram": histogram, **arithmetic_checks(context), + "source_sha256": {name: sha256(Path(__file__).with_name(name).read_bytes()).hexdigest() + for name in ("verify.py", "PROOF.md")}} + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + verify()