From e4fb5699c1c390ada0e6ac738d48548c462448b1 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 28 Oct 2026 12:55:31 +0000 Subject: [PATCH] feat(research): prove sharp four-query rank capacity --- research/four-block-query-capacity/PROOF.md | 148 +++++++++ research/four-block-query-capacity/README.md | 96 ++++++ .../four-block-query-capacity/SOURCES.json | 30 ++ research/four-block-query-capacity/TASK.json | 90 ++++++ .../four-block-query-capacity/VERIFY.json | 34 ++ research/four-block-query-capacity/verify.py | 291 ++++++++++++++++++ 6 files changed, 689 insertions(+) create mode 100644 research/four-block-query-capacity/PROOF.md create mode 100644 research/four-block-query-capacity/README.md create mode 100644 research/four-block-query-capacity/SOURCES.json create mode 100644 research/four-block-query-capacity/TASK.json create mode 100644 research/four-block-query-capacity/VERIFY.json create mode 100644 research/four-block-query-capacity/verify.py diff --git a/research/four-block-query-capacity/PROOF.md b/research/four-block-query-capacity/PROOF.md new file mode 100644 index 0000000000..4f02498b32 --- /dev/null +++ b/research/four-block-query-capacity/PROOF.md @@ -0,0 +1,148 @@ +# Exact capacity of four bounded-rank binary query shears + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Let K be any field of characteristic two and let +A = K[Q]/(Q²−1). There are n independent input coordinates and no additional +workspace. Free operations are arbitrary constant matrices in GL_n(K). +A paid operation has the form I_n + Q N, where N is a constant n-by-n +matrix, N²=0, and rank N≤r. Different calls may use different N. +All input coordinates must receive Q, so the exact desired endpoint is Q I_n. + +**Theorem.** For positive integers n,r, an endpoint Q I_n is possible with at +most four paid operations if and only if n is even and + + n ≤ 2 floor(4r/3). + +Equivalently, the least possible maximum paid rank is ceil(3n/8) for even n. +Every successful four-call word has total paid rank at least 3n/2. The +construction below attains this total rank as well as the optimal maximum. +Zero-rank padding represents an unused call, not a separately charged job. + +This is an abstract interface theorem. A native operation realizing an arbitrary +rank-r query, its helpers, physical scalar maps and complete recursive invoice +are not supplied. In particular, treating constant bases as free is an explicit +hypothesis, not a statement about the selected multiplier. + +## 1. Normalize the exact endpoint + +Put ε=Q+1, so ε²=0. For a paid factor, + + I+Q N = (I+N)(I+εN), (I+N)⁻¹=I+N. + +Move all constant factors to one end by conjugation. Conjugation preserves +rank and the square-zero property. Since the desired endpoint at ε=0 is I_n, +the combined constant factor is I_n. The remaining four factors have the form +I+εR_i, with R_i²=0 and rank R_i=r_i≤r. Their product is + + I+ε sum_i R_i = Q I_n = I+εI_n. + +Thus sum_i R_i=I_n. Taking traces shows n=0 in K, since a square-zero matrix +has trace zero. Therefore n is even. This reduction allows arbitrary free +constant bases between calls; it does not assume separate ports or a common +coordinate support for the R_i. + +## 2. Factor the query Gram projector and its complement + +Choose full-rank factorizations R_i=U_i V_i, with U_i having r_i columns and +V_i having r_i rows. Square-zero gives V_i U_i=0: multiply +U_i(V_i U_i)V_i=0 by a left inverse of U_i and a right inverse of V_i. +This also covers r_i=0 by empty blocks. + +Write S=sum_i r_i, concatenate the U_i into U and stack the V_i into V. +Then UV=I_n. Consequently G=VU is an idempotent of rank n in dimension S, +and its four diagonal blocks are zero. Its complementary idempotent +C=I_S−G has rank c=S−n and diagonal blocks I_(r_i). + +Factor C=AB with A of full column rank c and B of full row rank c. From +C²=C, left and right inverses give BA=I_c. Partition A into row blocks A_i +and B into column blocks B_i. The diagonal blocks say A_i B_i=I_(r_i). +Hence E_i=B_i A_i is an idempotent of rank r_i on K^c, and + + sum_i E_i = BA = I_c. + +The complements F_i=I_c−E_i have rank c−r_i. There are exactly four blocks, +and characteristic two gives + + sum_i F_i = 4I_c − sum_i E_i = I_c. + +Subadditivity of rank now implies + + c ≤ sum_i rank F_i = 4c−S, + S ≤ 3c = 3(S−n), + 3n ≤ 2S ≤ 8r. + +Since n is even, this proves n≤2 floor(4r/3). The inequality S≥3n/2 is the +additional rank cost missed by the simpler n≤3r complement-dimension bound. +For example, four rank-two queries cannot twist six independent coordinates; +four rank-three queries can twist eight, but cannot twist nine or ten. + +The use of the four complementary idempotents is the new step beyond the +minimum-query and block-simplex arguments credited below. + +## 3. Attain the bound by balancing omitted calls + +Write n=2p. On one coordinate pair, let + + A = [[0,1],[0,0]], B = [[0,0],[1,0]]. + +Both matrices are square-zero of rank one. The three-query identity is + + (I+Q A)(I+Q B)(I+Q A) = Q [[0,1],[1,0]], + +using Q²=1. A final constant swap makes this Q I_2. + +For each of the p disjoint coordinate pairs, omit one of four call positions +and place these three factors, in order, in the remaining positions. Assign +omitted positions cyclically 0,1,2,3,0,1,2,3,... . At each position, direct-sum +its active rank-one matrices. This produces one square-zero paid matrix whose +rank is the number of pairs active there. A final direct sum of swaps produces +Q I_n on every original input. + +Every call is omitted by at least floor(p/4) pairs, so the maximum rank is + + p − floor(p/4) = ceil(3p/4) = ceil(3n/8). + +The sum of the four ranks is exactly 3p. The required cap is therefore +ceil(3p/4)≤r, equivalent to p≤floor(4r/3). This proves the converse and both +sharpness claims. It works over F2, and therefore over every field K in the +contract. No search result is used to infer the unbounded construction. + +For r=3, take four pairs and omit a different call on each pair. Every query +then has rank three, there are eight independent outputs, and the total rank +is twelve. This is a concrete packing witness for the abstract changed model. + +## 4. Relation to predecessors + +Cinna Davis / 1337isnot1337's +`research/productive-controller-basis-search/GLOBAL-PROOF.md` supplies the +rank-one minimum-query simplex and its use in caller obstructions. Ali Romman's +PR #5617, `research/shortest-controller-stage-capacity/PROOF.md`, Section 9, +extends the Gram-complement method to coupled rank-q ports at the shortest +count. It derives the block simplex and its parity requirement there. + +Matarener's PR #6114, Open next question 1, asks about higher-rank or multi-bank +paid operations beyond its rank-one Laurent income bound. This package gives +a sharp abstract binary specialization of that question. It does not extend +#6114's rational Laurent theorem to physical multi-bank calls. None of those +predecessors' verifiers or reported numbers are rechecked here. The three-query +exchange identity and elementary rank factorization are standard tools; +worldwide priority for those tools is unclaimed. + +## 5. Verification boundary + +`verify.py` constructs every feasible even dimension for caps 1 through 24, +up to dimension 64. It checks exact matrices in F2[Q]/(Q²−1) and independently +checks their action on every original coefficient bit using a lifted binary +interpreter. Small witnesses also check the factored Gram complement and all +four complementary idempotents. Four conjugated witnesses mix coordinate pairs. + +The independent finite feasibility control enumerates every binary matrix in +dimensions two, three and four, retains every square-zero matrix, and uses all +pair sums to decide whether four such matrices sum to I at each rank cap. +This exhausts the normalized necessary condition in those finite domains. +It is not an enumeration of words in larger dimensions or a formal proof kernel. +Ten rejection controls exercise input bounds, a missing paid layer, a nonnilpotent +matrix and a rank-cap violation. Every check remains active with Python -O. diff --git a/research/four-block-query-capacity/README.md b/research/four-block-query-capacity/README.md new file mode 100644 index 0000000000..59c27082c7 --- /dev/null +++ b/research/four-block-query-capacity/README.md @@ -0,0 +1,96 @@ +# Four bounded-rank queries have exact capacity 2 floor(4r/3) + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with finite corroboration; no new κ.** Over any field of +characteristic two, let Q be a central formal involution. Allow arbitrary free +constant invertible bases and paid operations I+Q N with N²=0 and rank N≤r, +on exactly n independent coordinates with no auxiliary workspace. Then + +```text +Q I_n is attainable in at most four paid calls + if and only if n is even and n ≤ 2 floor(4r/3). +``` + +The least maximum paid rank at even n is ceil(3n/8). Every successful word has +total paid rank at least 3n/2, and an explicit balanced schedule attains both +minima. Four rank-two queries cannot twist six coordinates. Four rank-three +queries do twist eight coordinates. The proof permits scalar mixing across +all coordinates; it is not limited to separate-port lower bounds. + +[PROOF.md](PROOF.md) gives the quantified argument and constructor. The new +step factors the query Gram complement, then applies rank subadditivity to +its four complementary block idempotents. This strengthens the elementary +n≤3r capacity bound. The construction distributes three-query two-coordinate +exchange words over four positions, omitting a different position for each pair. + +The question comes from Matarener's [PR #6114, Open next question 1](https://github.com/CrocSwap/integer-mult-bounds/pull/6114). +Credit Cinna Davis / 1337isnot1337 for the minimum-query simplex and controller +lineage, Ali Romman for [PR #5617's coupled-port Gram framework](https://github.com/CrocSwap/integer-mult-bounds/pull/5617), +and the retained native/caller contributors credited in their sources. +Their results are cited as predecessors, without replaying their evidence. +The two merged proof documents are pinned as historical provenance in +SOURCES.json. Pending #6114 is bibliographic context, not a runtime dependency. + +## Reproduce + +From the repository root, using the interpreter used for local checks: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/four-block-query-capacity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/four-block-query-capacity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/four-block-query-capacity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/four-block-query-capacity --check-source-history +``` + +Elsewhere use a CPython 3.12 path. The verifier uses only the standard library, +imports no repository engine, reads no predecessor data and writes no files. +It emits `PASS_FOUR_BLOCK_QUERY_CAPACITY` and a generated JSON receipt bound +to SHA256 hashes of its package files. No receipt is handwritten. + +The direct check constructs 392 feasible instances for rank caps 1 through 24, +checks 17,696 original coefficient columns, checks 170 Gram factorizations +and four mixed-basis witnesses, and runs ten rejecting controls. It also +enumerates all 16, 512 and 65,536 binary matrices in dimensions two, three +and four. The square-zero counts by rank are respectively [1,3], [1,21] +and [1,105,210]. All pair sums decide the corresponding four-summand feasibility +questions. These finite checks corroborate the written proof. + +## Verifier bounds + +The executable fixes rank caps at 24 and dimensions at 64. Gram checks use +dimension at most 16, hence total rank at most 24. Exhaustion stops at 65,536 +matrices; pair-sum sets have at most 65,536 entries. Every loop is bounded by +these limits or a fixed four-call word, and the checker uses no recursion or +subprocesses. Python allocates dynamic objects; this is a managed-runtime +deviation from fixed-allocation guidance, with the live collections bounded +by those constants. Package hashing reads at most sixteen local files. +Warning-strict normal and optimized runs are registered; all mathematical +checks use explicit exceptions and remain active with assertions disabled. + +## Limitations + +This is an abstract algebraic interface result, not a finite multiplication +certificate or a complete multiplication theorem. A higher-rank query still +needs a legal physical native realization, arbitrary-input and helper contracts, +paid scalar bases, restoration, and a favorable complete signed invoice. +Constant bases are granted for free only in the theorem's declared model. + +The theorem does not cover extra clean or dirty workspace, characteristic zero, +an infinite-order Q, non-square-zero paid matrices, independent stage variables +or nonconstant free maps. No selected supplier replay, full framework proof, +physical implementation, outer-ledger change or proof-kernel check was run. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Can a physically legal multi-bank native job realize the rank-three query in + the eight-dimensional four-call construction? Begin with its four explicit + shear blocks and specify all returned helpers and actual paid ranks. A native + realization and complete signed invoice remain missing. +- What is the exact capacity at six or more calls in this same model? Begin with + the Gram complement and attainable omission schedules. This package stops at + four calls; it supplies no theorem for that larger domain. + +Structured relevance, first steps and blockers are in TASK.json. This changes +rather than completes the original card's physical consumer/invoice assignment. diff --git a/research/four-block-query-capacity/SOURCES.json b/research/four-block-query-capacity/SOURCES.json new file mode 100644 index 0000000000..d429ec9d88 --- /dev/null +++ b/research/four-block-query-capacity/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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/productive-controller-basis-search/GLOBAL-PROOF.md", + "usage": "provenance", + "git_blob": "74b67e22e6c063193a83825207cdec19a8fef7a4", + "sha256": "adc377b13924701bf5b0b50b091d8b69c90195d50ce0f6808f7fb4c7e0b16457" + }, + { + "path": "research/shortest-controller-stage-capacity/PROOF.md", + "usage": "provenance", + "git_blob": "3e1a1f6b1f773780927f01e20be6719fe08ca5f3", + "sha256": "df8c53e3b04fdfa9ea10dd02a8bf770ba3111c7fa2d561075e7dd00d2297613e" + } + ] +} diff --git a/research/four-block-query-capacity/TASK.json b/research/four-block-query-capacity/TASK.json new file mode 100644 index 0000000000..e10776f984 --- /dev/null +++ b/research/four-block-query-capacity/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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": "Determine the exact dimension attainable by at most four rank-at-most-r square-zero query shears with free constant bases over characteristic two and no auxiliary workspace.", + "scope_change_reason": "PR6114 Open next question 1 asks about higher-rank paid primitives. This isolates an abstract binary multi-bank query model and proves a sharp capacity theorem; it does not construct a physical primitive or complete the original consumer/invoice task.", + "bottleneck_link": "Higher-rank query batching is a proposed escape from rank-one caller bounds. The theorem gives an exact feasibility filter before native realization and complete signed pricing.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved sharp bound with an attaining construction and bounded exact controls; do not extend to more queries.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py constructs every feasible even dimension in its declared finite range, checks exact quotient-ring endpoints, and exhausts all four-by-four binary square-zero matrices.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a physically legal multi-bank native job realize the rank-three query used in the eight-dimensional four-call construction?", + "why_it_matters": "The abstract packing gain is not productive income until a physical caller and full invoice exist.", + "first_step": "Take the r=3,n=8 emitted shear blocks and specify actual inputs, returned helpers, native operators and paid rank.", + "blocked_by": "No physical multi-bank primitive or complete signed invoice is supplied." + }, + { + "question": "What is the exact capacity at six or more query calls with the same rank cap?", + "why_it_matters": "It would determine whether the four-call packing rule extends to larger caller changes.", + "first_step": "Repeat the Gram-complement rank argument with six blocks and compare attainable schedules.", + "blocked_by": "This package stops at four calls." + } + ] +} diff --git a/research/four-block-query-capacity/VERIFY.json b/research/four-block-query-capacity/VERIFY.json new file mode 100644 index 0000000000..62b93e5c75 --- /dev/null +++ b/research/four-block-query-capacity/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 quotient-ring construction endpoints, independent lifted-bit interpreter, Gram-complement rank certificate, complete 4x4 square-zero enumeration, and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete checks with Python assertions disabled." + } + ] +} diff --git a/research/four-block-query-capacity/verify.py b/research/four-block-query-capacity/verify.py new file mode 100644 index 0000000000..907a54a60c --- /dev/null +++ b/research/four-block-query-capacity/verify.py @@ -0,0 +1,291 @@ +"""Exact finite controls for the four-query capacity proof. Apache-2.0.""" + +from hashlib import sha256 +import json +from pathlib import Path +import sys + + +MAX_RANK = 24 +MAX_DIM = 64 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def eye(n): + return tuple(1 << i for i in range(n)) + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b, strict=True)) + + +def mul(a, b): + out = [] + for row in a: + value = 0 + for j in range(len(b)): + if row >> j & 1: + value ^= b[j] + out.append(value) + return tuple(out) + + +def independent_indices(rows, width): + pivots = [0] * width + indices = [] + for index, row in enumerate(rows): + value = row + for bit in range(width - 1, -1, -1): + if value >> bit & 1: + if pivots[bit]: + value ^= pivots[bit] + else: + pivots[bit] = value + indices.append(index) + break + return indices + + +def rank(rows, width): + return len(independent_indices(rows, width)) + + +def inverse(rows): + n = len(rows) + work = [row | (1 << (n + i)) for i, row in enumerate(rows)] + for col in range(n): + pivot = next((i for i in range(col, n) if work[i] >> col & 1), None) + need(pivot is not None, "singular constant basis") + work[col], work[pivot] = work[pivot], work[col] + for i in range(n): + if i != col and work[i] >> col & 1: + work[i] ^= work[col] + result = tuple(row >> n for row in work) + need(mul(rows, result) == eye(n), "inverse invariant") + return result + + +def factor(rows, width): + """Return a full-rank factorization A B of a binary rectangular matrix.""" + columns = tuple(sum(((row >> j) & 1) << i for i, row in enumerate(rows)) + for j in range(width)) + selected = independent_indices(columns, len(rows)) + r = len(selected) + left = tuple(sum(((row >> j) & 1) << k for k, j in enumerate(selected)) + for row in rows) + pivots = independent_indices(left, r) + right = mul(inverse(tuple(left[i] for i in pivots)), + tuple(rows[i] for i in pivots)) + need(mul(left, right) == rows, "rank factorization invariant") + return left, right + + +def construct(r, n): + need(1 <= r <= MAX_RANK, "rank outside finite constructor range") + need(2 <= n <= MAX_DIM and n % 2 == 0, "dimension must be positive and even") + need(n <= 2 * (4 * r // 3), "four-query capacity exceeded") + layers = [[0] * n for _ in range(4)] + for pair in range(n // 2): + active = [i for i in range(4) if i != pair % 4] + a, b = 2 * pair, 2 * pair + 1 + layers[active[0]][a] = 1 << b + layers[active[1]][b] = 1 << a + layers[active[2]][a] = 1 << b + return tuple(tuple(layer) for layer in layers), tuple(1 << (i ^ 1) for i in range(n)) + + +def quotient_check(layers, final, r): + """Replay in F2[Q]/(Q^2-1), keeping both coefficients separately.""" + n = len(final) + constant, odd = eye(n), (0,) * n + for nilpotent in layers: + need(mul(nilpotent, nilpotent) == (0,) * n, "paid matrix is not square-zero") + need(rank(nilpotent, n) <= r, "paid rank cap exceeded") + constant, odd = add(constant, mul(nilpotent, odd)), add(odd, mul(nilpotent, constant)) + endpoint = mul(final, constant), mul(final, odd) + need(endpoint == ((0,) * n, eye(n)), "endpoint is not Q times identity") + return endpoint + + +def lifted_check(layers, final): + """Independently replay every original coefficient bit as a 2n-bit map.""" + n = len(final) + rows = [1 << i for i in range(2 * n)] + for nilpotent in layers: + old = tuple(rows) + for i in range(n): + for j in range(n): + if nilpotent[i] >> j & 1: + rows[i] ^= old[n + j] + rows[n + i] ^= old[j] + old = tuple(rows) + result = [] + for half in range(2): + for row in final: + value = 0 + for j in range(n): + if row >> j & 1: + value ^= old[half * n + j] + result.append(value) + expected = tuple(1 << (n + i) for i in range(n)) + eye(n) + need(tuple(result) == expected, "lifted input-column endpoint failed") + + +def normalized_queries(layers, final): + n = len(final) + suffix = final + queries = [] + for nilpotent in reversed(layers): + query = mul(mul(suffix, nilpotent), inverse(suffix)) + queries.append(query) + suffix = mul(suffix, add(eye(n), nilpotent)) + need(suffix == eye(n), "constant endpoint is not identity") + total = (0,) * n + for query in queries: + need(mul(query, query) == (0,) * n, "normalized square-zero invariant") + total = add(total, query) + need(total == eye(n), "normalized queries do not sum to identity") + return tuple(queries) + + +def gram_check(queries, r): + n = len(queries[0]) + factors = [factor(query, n) for query in queries] + ranks = [len(right) for _, right in factors] + s = sum(ranks) + u = [0] * n + v = [] + offset = 0 + for (left, right), ri in zip(factors, ranks, strict=True): + need(mul(right, left) == (0,) * ri, "nilpotent factor pairing") + u = [row ^ (part << offset) for row, part in zip(u, left, strict=True)] + v.extend(right) + offset += ri + u, v = tuple(u), tuple(v) + need(mul(u, v) == eye(n), "UV must be identity") + k = mul(v, u) + cmat = add(eye(s), k) + need(mul(k, k) == k and rank(cmat, s) == s - n, "Gram complement invariant") + a, b = factor(cmat, s) + c = len(b) + need(mul(b, a) == eye(c), "complement factor pairing") + total_e, total_f = (0,) * c, (0,) * c + offset = 0 + for ri in ranks: + ai = a[offset:offset + ri] + bi = tuple((row >> offset) & ((1 << ri) - 1) for row in b) + need(mul(ai, bi) == eye(ri), "complement diagonal block") + e = mul(bi, ai) + f = add(eye(c), e) + need(mul(e, e) == e and rank(e, c) == ri, "block idempotent rank") + need(rank(f, c) == c - ri, "complementary block rank") + total_e, total_f = add(total_e, e), add(total_f, f) + offset += ri + need(total_e == eye(c) and total_f == eye(c), "four-block complementary sum") + need(3 * n <= 2 * s <= 8 * r, "sharp rank inequalities") + return s, c + + +def exhaustive_square_zero(): + summaries = [] + for n in (2, 3, 4): + by_rank = [[] for _ in range(n // 2 + 1)] + mask = (1 << n) - 1 + for encoded in range(1 << (n * n)): + rows = tuple((encoded >> (i * n)) & mask for i in range(n)) + if mul(rows, rows) == (0,) * n: + ri = rank(rows, n) + need(ri <= n // 2, "square-zero half-rank bound") + by_rank[ri].append(encoded) + target = sum(1 << (i * n + i) for i in range(n)) + feasible = [] + for r in range(1, n // 2 + 1): + choices = [x for part in by_rank[:r + 1] for x in part] + pair_sums = {a ^ b for a in choices for b in choices} + found = any((target ^ pair) in pair_sums for pair in pair_sums) + need(found == (n % 2 == 0 and n <= 2 * (4 * r // 3)), "exhaustive capacity mismatch") + feasible.append(found) + summaries.append({"dimension": n, "square_zero_counts_by_rank": [len(x) for x in by_rank], + "four_summand_feasible_by_cap": feasible}) + return summaries + + +def controls(): + count = 0 + for r, n in ((0, 2), (25, 2), (1, 0), (1, 3), (1, 4), (2, 6), (24, 66)): + try: + construct(r, n) + except ValueError: + count += 1 + else: + raise ValueError("invalid constructor request accepted") + layers, final = construct(3, 8) + for kind in range(3): + bad = list(layers) + if kind == 0: + bad[0] = (0,) * 8 + elif kind == 1: + bad[0] = eye(8) + try: + quotient_check(tuple(bad), final, 2 if kind == 2 else 3) + except ValueError: + count += 1 + else: + raise ValueError("mutated word accepted") + return count + + +def finite_constructions(): + fixtures = gram_fixtures = input_columns = 0 + examples = [] + for r in range(1, MAX_RANK + 1): + cap = 2 * (4 * r // 3) + for n in range(2, cap + 1, 2): + layers, final = construct(r, n) + quotient_check(layers, final, r) + lifted_check(layers, final) + input_columns += 2 * n + fixtures += 1 + if n <= 16: + s, c = gram_check(normalized_queries(layers, final), r) + need(s == 3 * n // 2 and c == n // 2, "attaining total rank") + gram_fixtures += 1 + if r <= 6: + examples.append({"rank_cap": r, "maximum_dimension": cap}) + for r in range(1, 5): + n = 2 * (4 * r // 3) + layers, final = construct(r, n) + basis = list(eye(n)) + for i in range(n - 1): + basis[i] ^= basis[i + 1] + basis, inv = tuple(basis), inverse(tuple(basis)) + mixed = tuple(mul(mul(basis, x), inv) for x in layers) + mixed_final = mul(mul(basis, final), inv) + quotient_check(mixed, mixed_final, r) + lifted_check(mixed, mixed_final) + gram_check(normalized_queries(mixed, mixed_final), r) + return {"construction_fixtures": fixtures, "original_coefficient_columns": input_columns, + "gram_fixtures": gram_fixtures, "mixed_basis_fixtures": 4, "examples": examples} + + +def main(): + need(sys.version_info >= (3, 12), "CPython 3.12 or newer required") + need(len(sys.argv) == 1, "no command-line arguments accepted") + receipt = finite_constructions() + receipt["exhaustive_square_zero"] = exhaustive_square_zero() + receipt["rejecting_controls"] = controls() + package = Path(__file__).resolve().parent + files = sorted(package.iterdir()) + need(len(files) <= 16, "unexpected package size") + receipt["sha256"] = {p.name: sha256(p.read_bytes()).hexdigest() + for p in files if p.is_file()} + receipt["status"] = "PASS_FOUR_BLOCK_QUERY_CAPACITY" + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()