From 6c3562e62f43b8490fa327d745b877d9f8d9911b Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 09:28:52 -0400 Subject: [PATCH] =?UTF-8?q?Audit=20#6122's=20four-query=20capacity=20and?= =?UTF-8?q?=20extend=20it=20to=20every=20call=20count=20(no=20new=20=CE=BA?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Independent audit of PR6122 (head e4fb5699c): proof re-derived, no gap. Stdlib F2 exhaustion of every cap profile for n=2..6, including the first finite check of the n=6, r=2 exclusion. Proved corollaries: heterogeneous per-call caps at four calls, and exact k-call capacity n + ceil(n/m_k) <= k r for every k >= 3, answering PR6122 Open question 2. Co-Authored-By: Claude Opus 5.5 --- .../four-block-query-capacity-audit/README.md | 171 +++++++ .../RESULT.json | 142 ++++++ .../SOURCES.json | 24 + .../four-block-query-capacity-audit/TASK.json | 90 ++++ .../VERIFY.json | 18 + .../four-block-query-capacity-audit/verify.py | 425 ++++++++++++++++++ 6 files changed, 870 insertions(+) create mode 100644 research/four-block-query-capacity-audit/README.md create mode 100644 research/four-block-query-capacity-audit/RESULT.json create mode 100644 research/four-block-query-capacity-audit/SOURCES.json create mode 100644 research/four-block-query-capacity-audit/TASK.json create mode 100644 research/four-block-query-capacity-audit/VERIFY.json create mode 100644 research/four-block-query-capacity-audit/verify.py diff --git a/research/four-block-query-capacity-audit/README.md b/research/four-block-query-capacity-audit/README.md new file mode 100644 index 0000000000..dce26f6675 --- /dev/null +++ b/research/four-block-query-capacity-audit/README.md @@ -0,0 +1,171 @@ +# Audit of PR6122's four-query capacity, and the exact capacity for every call count + +Josie Elliston, prepared with Claude Code (Opus 5.5). Apache-2.0. + +**Independent audit plus scoped extension; no new κ.** This audits +[PR6122](https://github.com/CrocSwap/integer-mult-bounds/pull/6122) (Nick Petalas, +head `e4fb5699c1c390ada0e6ac738d48548c462448b1`, package +`research/four-block-query-capacity/`) and answers its Open next question 2. +It uses the same model as PR6122. K has characteristic two, Q is a central +involution, the free maps are constant matrices in GL_n(K), and each paid call +is I + Q N with N² = 0 and rank N ≤ r. There is no workspace, and the target is +Q I_n. + +## Findings + +1. **The theorem holds.** I re-derived every step of PR6122's PROOF.md: the + ε = Q + 1 normalization to Σ R_i = I_n, the trace parity, the Gram + factorization UV = I_n, the complement C = AB with BA = I_c, the block + idempotents E_i with Σ E_i = I_c, and the rank count c ≤ Σ (c − r_i). I found + no gap. The construction attains the bound. + +2. **PR6122's finite check never reaches the new step.** Its exhaustive control + covers n ≤ 4. Every case it decides there is already settled by trace parity + (n = 3) or by the elementary bound n ≤ 3r (n = 4, r = 1). The first case + where the new bound 3n ≤ 2S is needed is n = 6, r = 2 (6 ≤ 3r, but + 6 > 2⌊4r/3⌋ = 4). The Gram fixtures run only on feasible constructions. So + the headline exclusion "four rank-two queries cannot twist six" had no finite + evidence. It has some now: `verify.py` decides it by exhaustion over F2. + +3. **Exhaustion over F2, n = 2..6, every cap profile.** Here (c1, c2, c3, c4) + are per-call rank caps, 0 ≤ c_j ≤ n/2, giving 75 sorted profiles. The search + finds a witness exactly when + + n is even and Σ_j min(c_j, n/2) ≥ 3n/2. + + This covers n = 6 at uniform caps 2 (infeasible) and 3 (feasible). It also + covers n = 5, where both rank bounds allow uniform cap 2 and only parity + excludes it. The method does not use the Gram argument. R1 is put in + normal form, which conjugation invariance allows, and every square-zero R2 + is enumerated. Y = I + R1 + R2 must have rank ≤ c3 + c4. Membership of Y in + {R3 + R4} is a class function, so it is decided once per similarity class. + The complete invariant is rank p(Y)^k for each irreducible p over F2. + Membership is decided by enumerating every R3 and testing Y + R3. + +4. **Corollary: heterogeneous caps (proved, all fields).** With per-call caps + c_j, four calls reach Q I_n iff n is even and Σ min(c_j, n/2) ≥ 3n/2. + Necessity: PR6122 gives S ≥ 3n/2, and a square-zero R_j has rank at most + n/2. Sufficiency: put o_j = n/2 − min(c_j, n/2). These are nonnegative and + sum to at most n/2, so they can be topped up to omission counts summing to + exactly n/2. Running PR6122's omission schedule with those counts gives + rank n/2 − o_j ≤ c_j at call j. `verify.py` builds and replays 16,559 such + words (every even n ≤ 24 and every ordered cap profile with c_j ≤ n/2 + 1) + in F2[Q]/(Q²−1). + +5. **Extension: exact capacity for every call count k ≥ 3 (proved, all + fields).** Let m_k = 2⌊(k−1)/2⌋, so m_k = k−1 for odd k and k−2 for even k. + Then k paid calls of rank ≤ r reach Q I_n iff + + n is even and n + ⌈n/m_k⌉ ≤ k r. + + The least total paid rank is n + ⌈n/m_k⌉. For k = 4 this is PR6122's + n ≤ 2⌊4r/3⌋; the verifier checks that for r < 200. Five calls reach + n = 4r: five rank-two calls twist eight coordinates, while four can twist + only four. Six calls reach 4, 8, 14, 18, 24, 28 for r = 1..6. With + rank-one calls, the minimum number of calls for n coordinates is n + 1. That + is Cinna Davis's minimum-query simplex bound, which this reproduces as a + consistency check. + + The extreme odd case is already known. When k is odd and n = (k−1) r, this + is Ali Romman's block simplex at the shortest count (#5617 PROOF.md §9: + L = n+1 calls of rank q on N = nq). That section leaves N ≠ q(L−1) and + other call counts open. Finding 5 covers every n and k for uniform caps. + Mixed caps are covered only for k = 4 (finding 4). + + *Lower bound.* Normalize as in PR6122 §1, so Σ_{i≤k} R_i = I_n. For odd k, + append R_{k+1} = 0. The number K of summands is then even. PR6122 §2 never + uses K = 4 until its last line. It gives idempotents E_i of rank r_i on K^c, + with c = S − n and Σ E_i = I_c. So Σ (I_c − E_i) = (K−1) I_c = I_c, because + K − 1 is odd. Rank subadditivity gives c ≤ Kc − S, so (K−1) n ≤ (K−2) S. + Since K − 2 = m_k, this says S ≥ n + n/m_k. S is an integer, so + S ≥ n + ⌈n/m_k⌉, and S ≤ k r. + + For odd k the Gram step is not needed. The elementary bound gives the same + inequality. Σ_{j≠i} R_j = I + R_i is invertible, so n ≤ S − r_i. Summing + over i gives (k−1) S ≥ k n, which is S ≥ n + n/(k−1). PR6122's new step + matters exactly for even k, where it improves k n/(k−1) to + (k−1) n/(k−2). + + *Construction.* For even d, I_d is the sum of d + 1 rank-one square-zero + matrices over F2: + R_i = e_i (1 − e_i)^T for i < d, and R_d = J, the all-ones matrix. The rows + of the first d sum to J − I, and J² = dJ = 0. This is the n + 1 simplex of + Cinna Davis's GLOBAL-PROOF.md, written explicitly. Split n into ⌈n/m_k⌉ + even blocks of dimension ≤ m_k. A block of dimension d contributes d + 1 + rank-one terms, at most k of them. Lay all the terms on call positions + 1..k in cyclic order, wrapping around (McNaughton's rule). Each block then + uses distinct positions, and each position receives at most + ⌈(n + ⌈n/m_k⌉)/k⌉ ≤ r terms. Call j pays I + Q N_j, where N_j is the + direct sum of its terms, and is preceded by the free constant I + N_j. Then + (I + N)(I + Q N) = I + εN, and Π_j (I + εN_j) = I + ε I_n = Q I_n in any + order. `verify.py` replays 353 such words, for k = 3..9 and r = 1..6, with + literal F2[Q]/(Q²−1) arithmetic. Controls show that the constants are + required and that reversing the call order still works. + +## Evidence + +```sh +python3.12 -B research/four-block-query-capacity-audit/verify.py +python3.12 -B scripts/research_package.py --package research/four-block-query-capacity-audit +``` + +The verifier uses only the standard library. It imports nothing from PR6122 or +the repository, takes about 30 s and prints `PASS_FOUR_BLOCK_QUERY_CAPACITY_AUDIT`. +It compares its output with `RESULT.json` in full. Thirteen positive and +negative controls must all hold. They cover planted false witnesses, an +odd-trace target, a dropped layer, swapped layers, a rank-cap violation and +missing constants. The constructor must refuse (n, r) = (6, 2) and (10, 3) +at four calls, and n = 10 at five calls of rank 2. The verifier passes with +Python 3.10, 3.12 and 3.14, in both normal and `-O` modes. + +*Local search evidence only (shared venv, python-sat, not submitted).* A +separate SAT encoding uses R_j = U_j V_j with V_j U_j = 0. It agrees on the +positive cases n = 4, 6, 8 at four calls, on GF(4) with n = 6 and caps +(3, 2, 2, 2), and on k = 5, 6 witnesses at n = 4, 6, 8. Without symmetry +breaking, the n = 6, r = 2 UNSAT case did not finish within 300 s. That is why +the exclusion evidence here is the stdlib exhaustion. + +PR6122's own `verify.py` was read and run (Python 3.12): it passes, with 392 +construction fixtures and 170 Gram fixtures. + +An independent read-only OpenAI Codex review found no error in either +capacity proof or in the identity-target exhaustion. It found one verifier +defect. The decider also accepted a non-identity target but still fixed R1 +in normal form, which is valid only for a conjugation-invariant target. That +path now enumerates every R1, and its controls were moved to n = 2 and n = 3. + +## Limits + +The exhaustion is over F2 and n ≤ 6 only. For other fields and larger n, the +written proofs are the evidence. The model is PR6122's abstract interface: free +constant bases, square-zero constant paid matrices, no workspace, and the target +Q I_n. Nothing here supplies a native realization of a rank-r query, a physical +multi-bank primitive, a signed invoice, a supplier, or a κ change. No +literature search was made for the rank-capped "sum of square-zero matrices +equals I" statement, which is a rank-constrained case of the classical +sums-of-square-zero-matrices question. Priority for findings 4 and 5 is not +claimed beyond this repository. The merged package +`research/square-zero-idempotent-compiler/` is related but different: its +paid alphabet is rank-one idempotent couplings, and its target is I + (1+g)N. + +## Open next questions + +- **Do more calls actually pay?** Five calls twist 4r coordinates at rank r, + where four calls twist about 8r/3. The paid rank per twisted coordinate falls + from 3/2 to 5/4 and tends to 1 as k grows. Whether the extra calls cost less + than they save depends on the per-call charge in a real invoice. A first step + is to price the k = 5, n = 8, r = 2 word under the cost rule used by #6114 or + #5617. This needs a per-call price for a rank-2 query. +- **Can workspace or a non-square-zero paid matrix beat n + ⌈n/m_k⌉?** Both + are outside this model. The Gram step uses Σ R_i = I_n exactly, so dirty + workspace changes the equation that the argument starts from. + +## Credit + +The four-call theorem, its proof and the omission schedule are by Nick Petalas +(PR6122). The n + 1 rank-one simplex is from Cinna Davis / 1337isnot1337, +`research/productive-controller-basis-search/GLOBAL-PROOF.md`. The +coupled-port Gram framework and the block simplex at the shortest count are +by Ali Romman (#5617, PROOF.md §9). The source question is +Matarener's #6114. Session claim and handoff: +[discussion 1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166). diff --git a/research/four-block-query-capacity-audit/RESULT.json b/research/four-block-query-capacity-audit/RESULT.json new file mode 100644 index 0000000000..7cb13db5c3 --- /dev/null +++ b/research/four-block-query-capacity-audit/RESULT.json @@ -0,0 +1,142 @@ +{ + "construction": { + "max_dimension": 24, + "profiles_refused": 111111, + "words_replayed": 16559 + }, + "controls": { + "constructor_refuses_10_at_cap_3": true, + "constructor_refuses_6_at_cap_2": true, + "dropped_layer_rejected": true, + "five_call_word_needs_its_constants": true, + "five_call_word_order_free": true, + "five_calls_rank_two_refuse_ten": true, + "five_calls_rank_two_twist_eight": true, + "non_square_zero_witness_rejected": true, + "odd_trace_target_rejected": true, + "rank_cap_violation_rejected": true, + "reachable_nonidentity_target_found": true, + "swapped_layers_rejected": true + }, + "exhaustion": { + "2": { + "classes_tested_uniform_cap": { + "0": 0, + "1": 2 + }, + "feasible": 2, + "profiles": 5, + "square_zero_counts_by_rank": [ + 1, + 3 + ], + "uniform_cap_feasible": { + "0": false, + "1": true + } + }, + "3": { + "classes_tested_uniform_cap": { + "0": 0, + "1": 1 + }, + "feasible": 0, + "profiles": 5, + "square_zero_counts_by_rank": [ + 1, + 21 + ], + "uniform_cap_feasible": { + "0": false, + "1": false + } + }, + "4": { + "classes_tested_uniform_cap": { + "0": 0, + "1": 0, + "2": 1 + }, + "feasible": 4, + "profiles": 15, + "square_zero_counts_by_rank": [ + 1, + 105, + 210 + ], + "uniform_cap_feasible": { + "0": false, + "1": false, + "2": true + } + }, + "5": { + "classes_tested_uniform_cap": { + "0": 0, + "1": 0, + "2": 5 + }, + "feasible": 0, + "profiles": 15, + "square_zero_counts_by_rank": [ + 1, + 465, + 6510 + ], + "uniform_cap_feasible": { + "0": false, + "1": false, + "2": false + } + }, + "6": { + "classes_tested_uniform_cap": { + "0": 0, + "1": 0, + "2": 1, + "3": 1 + }, + "feasible": 7, + "profiles": 35, + "square_zero_counts_by_rank": [ + 1, + 1953, + 136710, + 234360 + ], + "uniform_cap_feasible": { + "0": false, + "1": false, + "2": false, + "3": true + } + } + }, + "k_calls": { + "cap_range": [ + 1, + 6 + ], + "five_call_capacity_r1_to_6": [ + 4, + 8, + 12, + 16, + 20, + 24 + ], + "k_range": [ + 3, + 9 + ], + "six_call_capacity_r1_to_6": [ + 4, + 8, + 14, + 18, + 24, + 28 + ], + "words_replayed": 353 + } +} diff --git a/research/four-block-query-capacity-audit/SOURCES.json b/research/four-block-query-capacity-audit/SOURCES.json new file mode 100644 index 0000000000..0ffb1128c9 --- /dev/null +++ b/research/four-block-query-capacity-audit/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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" + } + ] +} diff --git a/research/four-block-query-capacity-audit/TASK.json b/research/four-block-query-capacity-audit/TASK.json new file mode 100644 index 0000000000..6dca42d52f --- /dev/null +++ b/research/four-block-query-capacity-audit/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": "Independent audit of PR6122 (head e4fb5699c): four square-zero paid calls I+QN of rank <= r, char 2, free constant bases, no workspace, target Q I_n, capacity n <= 2 floor(4r/3). Proof re-derived; stdlib exhaustion over F2 of every cap profile for n = 2..6 (first finite check of the n=6, r=2 exclusion, which PR6122's n<=4 exhaustion cannot reach); proved corollary for heterogeneous per-call caps; proved extension to every call count k >= 3: feasible iff n even and n + ceil(n/m_k) <= k r with m_k = 2 floor((k-1)/2), answering PR6122 Open next question 2.", + "scope_change_reason": "Drawn track was independent-verification (card independent-moment, whose invoice question does not fit). Following the overnight coordinator's advice to audit a fresh unreviewed open PR, this audits PR6122, which belongs to joint-query-controller, so the package keeps that card. The k-call extension reuses PR6122's own lemma and answers its Open next question 2.", + "bottleneck_link": "Side result for the query-controller question: it bounds how many coordinates a fixed number of bounded-rank paid queries can twist in PR6122's abstract model, and shows that five or more calls lower the paid rank per twisted coordinate from 3/2 toward 1. It supplies no physical primitive, invoice or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the proof review, the F2 exhaustion at n <= 6 and the k-call theorem with replayed constructions; do not attempt larger-field or larger-n exhaustion or any invoice.", + "outcome": "completed", + "evidence": "research/four-block-query-capacity-audit/RESULT.json", + "author": "Josie Elliston", + "ai_assistance": "Prepared with Claude Code (Opus 5.5); local python-sat searches in a research venv (not submitted); optional read-only OpenAI Codex review.", + "open_questions": [ + { + "question": "Do five or more calls pay in a real invoice? Five rank-two calls twist eight coordinates, against four for four calls.", + "why_it_matters": "The paid rank per twisted coordinate falls from 3/2 (k=4) to 5/4 (k=5,6) and toward 1, but each call has its own charge.", + "first_step": "Price the k=5, n=8, r=2 word from verify.py construct_k under the per-call cost rule used by #6114 or #5617.", + "blocked_by": "A per-call price for a rank-2 query and a native realization." + }, + { + "question": "Can clean or dirty workspace, or non-square-zero paid matrices, beat n + ceil(n/m_k) total rank?", + "why_it_matters": "Both are outside PR6122's model; the Gram step starts from sum R_i = I_n exactly.", + "first_step": "Redo the PR6122 section 1 normalization with one extra clean coordinate and see what replaces sum R_i = I_n.", + "blocked_by": "None for the algebra; a physical workspace contract for relevance." + } + ] +} diff --git a/research/four-block-query-capacity-audit/VERIFY.json b/research/four-block-query-capacity-audit/VERIFY.json new file mode 100644 index 0000000000..a9e704e9d1 --- /dev/null +++ b/research/four-block-query-capacity-audit/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Stdlib, no repository imports. (1) F2 exhaustion of every cap profile c1>=c2>=c3>=c4, 0<=c_j<=n/2, n=2..6 (75 profiles): R1 in conjugation normal form, every square-zero R2, rank filter, membership of Y=I+R1+R2 in {R3+R4} once per similarity class (complete invariant rank p(Y)^k), every R3; result equals 'n even and sum min(c_j,n/2) >= 3n/2', including n=6 uniform cap 2 infeasible and cap 3 feasible. (2) 16,559 omission-schedule words for heterogeneous caps, n<=24, replayed in F2[Q]/(Q^2-1). (3) 353 k-call simplex-block words, k=3..9, r=1..6, replayed literally; k=4 rule equals 2 floor(4r/3) for r<200; rank-one minimum equals n+1. (4) 13 controls. RESULT.json compared in full." + } + ] +} diff --git a/research/four-block-query-capacity-audit/verify.py b/research/four-block-query-capacity-audit/verify.py new file mode 100644 index 0000000000..25aee96cdc --- /dev/null +++ b/research/four-block-query-capacity-audit/verify.py @@ -0,0 +1,425 @@ +"""Independent finite audit of PR6122's four-query capacity theorem over F2. + +Josie Elliston, prepared with Claude Code (Opus 5.5). Apache-2.0. + +Standard library only; imports nothing from PR6122 or the repository; writes no +files. Three parts: + +1. Exhaustion. For n = 2..6 and every cap profile c1 >= c2 >= c3 >= c4 with + 0 <= c_j <= n // 2, decide whether I_n = R1 + R2 + R3 + R4 with every R_j a + square-zero binary matrix of rank <= c_j. The decision uses conjugation + invariance (R1 in normal form), a rank filter, and the complete similarity + invariant rank p(Y)^k, not PR6122's Gram-complement argument. The answer is + compared with the rule n even and sum_j min(c_j, n/2) >= 3n/2. +2. Construction. For every even n <= 24 and every profile meeting the rule, + build the omission schedule and replay the literal word + (I + Q N_1)(I + Q N_2)(I + Q N_3)(I + Q N_4) S in F2[Q]/(Q^2 - 1). +3. Controls. The decider must reject planted false witnesses, an odd trace + target and a wrong target; the constructor must refuse profiles that break + the rule; mutated words must fail the replay. +""" + +import itertools +import json +from pathlib import Path +import sys + + +# ---------- binary matrices as tuples of row bitmasks (bit j = column j) ---------- + +def eye(n): + return tuple(1 << i for i in range(n)) + + +def zero(n): + return (0,) * 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: + v = 0 + j = 0 + while row: + if row & 1: + v ^= b[j] + row >>= 1 + j += 1 + out.append(v) + return tuple(out) + + +def rank(rows): + rows = [r for r in rows if r] + rk = 0 + while rows: + p = rows.pop() + rk += 1 + low = p & -p + rows = [r ^ p if r & low else r for r in rows] + rows = [r for r in rows if r] + return rk + + +def need(cond, msg): + if not cond: + raise SystemExit("FAIL: " + msg) + + +# ---------- enumeration of square-zero matrices ---------- + +def subspaces(vectors, t): + seen = {} + for combo in itertools.combinations(vectors, t): + span = {0} + for v in combo: + span |= {x ^ v for x in span} + if len(span) == 1 << t: + seen.setdefault(frozenset(span), combo) + return list(seen.values()) + + +def gl(t): + return [rows for rows in itertools.product(range(1, 1 << t), repeat=t) if rank(rows) == t] + + +def square_zero(n, t): + """Every square-zero n x n binary matrix of rank exactly t, each once: + column space W (basis B), row space Z inside the annihilator of W (basis C), + R = B M C with M invertible.""" + if t == 0: + return [zero(n)] + vecs = list(range(1, 1 << n)) + out = [] + G = gl(t) + for B in subspaces(vecs, t): + ann = [v for v in vecs if all(bin(v & w).count("1") % 2 == 0 for w in B)] + for C in subspaces(ann, t): + for M in G: + MC = [0] * t + for s in range(t): + for u in range(t): + if M[s] >> u & 1: + MC[s] ^= C[u] + rows = [] + for i in range(n): + v = 0 + for s in range(t): + if B[s] >> i & 1: + v ^= MC[s] + rows.append(v) + out.append(tuple(rows)) + return out + + +# ---------- complete similarity invariant over F2 ---------- + +def irreducibles(maxdeg): + def pmod(a, b): + db = b.bit_length() - 1 + while a and a.bit_length() - 1 >= db: + a ^= b << (a.bit_length() - 1 - db) + return a + irr = [] + for p in range(2, 1 << (maxdeg + 1)): + d = p.bit_length() - 1 + if all(pmod(p, q) for q in irr if 2 * (q.bit_length() - 1) <= d): + irr.append(p) + return irr + + +def poly_eval(p, Y): + n = len(Y) + acc = zero(n) + for i in range(p.bit_length() - 1, -1, -1): + acc = mul(acc, Y) + if p >> i & 1: + acc = add(acc, eye(n)) + return acc + + +def sim_key(Y, irr): + """(p, rank p(Y), rank p(Y)^2, ...) for each irreducible p with p(Y) singular. + These ranks determine every elementary divisor, so equal keys <=> similar.""" + n = len(Y) + key = [] + for p in irr: + d = p.bit_length() - 1 + P = poly_eval(p, Y) + rk = rank(P) + if rk == n: + continue + ranks = [rk] + Pk = P + for _ in range(n // d - 1): + Pk = mul(Pk, P) + ranks.append(rank(Pk)) + key.append((p, tuple(ranks))) + return tuple(key) + + +def normal_form(n, t): + return tuple((1 << (i + 1)) if i % 2 == 0 and i // 2 < t else 0 for i in range(n)) + + +def decide(n, caps, sz, irr, target=None): + """Exact decision of target = R1+R2+R3+R4 (default I_n) with caps c1..c4. + Returns (witness or None, number of similarity classes tested).""" + c1, c2, c3, c4 = caps + T = eye(n) if target is None else target + by_rank_desc = lambda c: [R for t in range(c, -1, -1) for R in sz[t]] + R2s, R3s = by_rank_desc(c2), by_rank_desc(c3) + classes = set() + if T == eye(n): + # conjugation fixes I_n, so R1 may be taken in normal form + firsts = [normal_form(n, t) for t in range(c1, -1, -1)] + need(all(mul(R, R) == zero(n) and rank(R) == t + for R, t in zip(firsts, range(c1, -1, -1))), "normal form") + else: + # a non-scalar target is not conjugation invariant: enumerate every R1 + firsts = by_rank_desc(c1) + for R1 in firsts: + for R2 in R2s: + Y = add(add(T, R1), R2) + if rank(Y) > c3 + c4: # Y = R3 + R4 forces rank Y <= c3 + c4 + continue + k = sim_key(Y, irr) + if k in classes: # membership in {R3+R4} is a class function + continue + classes.add(k) + for R3 in R3s: + Z = add(Y, R3) + if rank(Z) <= c4 and mul(Z, Z) == zero(n): + return (R1, R2, R3, Z), len(classes) + return None, len(classes) + + +def check_witness(w, caps, target): + n = len(target) + ok = all(mul(R, R) == zero(n) and rank(R) <= c for R, c in zip(w, caps, strict=True)) + total = zero(n) + for R in w: + total = add(total, R) + return ok and total == target + + +def rule(n, caps): + p = n // 2 + return n % 2 == 0 and sum(min(c, p) for c in caps) >= 3 * p + + +# ---------- omission-schedule construction and literal word replay ---------- + +def construct(n, caps): + """Return paid layers N_1..N_4 and final constant S, or None if the rule fails. + Pair k omits one position; position j is omitted by o_j >= p - c_j pairs.""" + if not rule(n, caps): + return None + p = n // 2 + omit = [max(0, p - min(c, p)) for c in caps] + spare = p - sum(omit) + for j in range(4): # top up to exactly p omissions + extra = min(spare, p - omit[j]) + omit[j] += extra + spare -= extra + need(spare == 0 and sum(omit) == p, "omission counts") + order = [j for j in range(4) for _ in range(omit[j])] + layers = [[0] * n for _ in range(4)] + for k, skipped in enumerate(order): + a, b = 2 * k, 2 * k + 1 + active = [j for j in range(4) if j != skipped] + layers[active[0]][a] |= 1 << b # E_ab + layers[active[1]][b] |= 1 << a # E_ba + layers[active[2]][a] |= 1 << b # E_ab + swap = tuple(1 << (i ^ 1) for i in range(n)) + return [tuple(x) for x in layers], swap + + +def replay(layers, final, caps): + """Literal product in F2[Q]/(Q^2-1): an element is (E, O) meaning E + Q O.""" + n = len(final) + E, O = eye(n), zero(n) + for N, c in zip(layers, caps, strict=True): + if mul(N, N) != zero(n) or rank(N) > c: + return False + # (E + Q O)(I + Q N) = (E + O N) + Q (O + E N), using Q^2 = 1 + E, O = add(E, mul(O, N)), add(O, mul(E, N)) + E, O = mul(E, final), mul(O, final) + return E == zero(n) and O == eye(n) + + +# ---------- k calls: simplex blocks and wrap-around packing ---------- + +def m_k(k): + """Largest even block dimension usable with k calls (a 2q-block needs 2q+1 calls).""" + return 2 * ((k - 1) // 2) + + +def k_rule(n, k, r): + """Claimed exact k-call capacity: n even, n >= 2 and n + ceil(n / m_k) <= k r.""" + m = m_k(k) + return m > 0 and n >= 2 and n % 2 == 0 and n + -(-n // m) <= k * r + + +def simplex(d): + """I_d = sum of d+1 rank-one square-zero binary matrices (d even): + R_i = e_i (1 - e_i)^T for i < d, and R_d = J (all ones).""" + full = (1 << d) - 1 + blocks = [tuple((full ^ (1 << i)) if row == i else 0 for row in range(d)) for i in range(d)] + blocks.append(tuple(full for _ in range(d))) + return blocks + + +def construct_k(n, k, r): + """Paid matrices N_1..N_k (square-zero, rank <= r) with sum I_n, or None. + Blocks of dimension m_k (and one smaller even block) are laid out on + consecutive call positions, wrapping around (McNaughton).""" + if not k_rule(n, k, r): + return None + m = m_k(k) + dims = [m] * (n // m) + ([n % m] if n % m else []) + layers = [[0] * n for _ in range(k)] + slot = offset = 0 + for d in dims: + for R in simplex(d): + pos = slot % k + for i, row in enumerate(R): + layers[pos][offset + i] |= row << offset + slot += 1 + offset += d + out = [tuple(x) for x in layers] + return out if all(rank(N) <= r for N in out) else "cap" + + +def replay_k(layers, r): + """Literal word prod_j (I + N_j)(I + Q N_j) in F2[Q]/(Q^2-1); (I + N_j) is the free constant.""" + n = len(layers[0]) + E, O = eye(n), zero(n) + for N in layers: + if mul(N, N) != zero(n) or rank(N) > r: + return False + C = add(eye(n), N) + E, O = mul(E, C), mul(O, C) + E, O = add(E, mul(O, N)), add(O, mul(E, N)) + return E == zero(n) and O == eye(n) + + +# ---------- main ---------- + +def main(compare=True): + need(sys.version_info >= (3, 10), "Python 3.10 or newer required") + result = {"exhaustion": {}, "construction": {}, "k_calls": {}, "controls": {}} + + # 1. exhaustion + store = {} + for n in range(2, 7): + sz = [square_zero(n, t) for t in range(n // 2 + 1)] + irr = irreducibles(n) + store[n] = (sz, irr) + rows = [] + for caps in itertools.combinations_with_replacement(range(n // 2, -1, -1), 4): + w, ncls = decide(n, caps, sz, irr) + if w is not None: + need(check_witness(w, caps, eye(n)), f"witness n={n} {caps}") + need((w is not None) == rule(n, caps), f"exhaustion disagrees with rule at n={n} {caps}") + rows.append([list(caps), w is not None, ncls]) + result["exhaustion"][str(n)] = { + "square_zero_counts_by_rank": [len(x) for x in sz], + "profiles": len(rows), + "feasible": sum(1 for r in rows if r[1]), + "uniform_cap_feasible": {str(r[0][0]): r[1] for r in rows if len(set(r[0])) == 1}, + "classes_tested_uniform_cap": {str(r[0][0]): r[2] for r in rows if len(set(r[0])) == 1}, + } + six = result["exhaustion"]["6"] + need(six["uniform_cap_feasible"]["2"] is False and six["uniform_cap_feasible"]["3"] is True, + "headline n=6 cap-2 exclusion") + + # 2. construction (every even n <= 24, every sorted profile with c_j <= n/2 + 1) + built = refused = 0 + for n in range(2, 25, 2): + top = n // 2 + 1 + for caps in itertools.combinations_with_replacement(range(top, -1, -1), 4): + for perm in sorted(set(itertools.permutations(caps))): + out = construct(n, perm) + if out is None: + need(not rule(n, perm), "constructor refused a rule-feasible profile") + refused += 1 + continue + need(replay(out[0], out[1], perm), f"replay n={n} {perm}") + need(sum(rank(N) for N in out[0]) == 3 * n // 2, "total rank 3n/2") + built += 1 + result["construction"] = {"words_replayed": built, "profiles_refused": refused, + "max_dimension": 24} + + # 2b. k calls, k = 3..9, caps r = 1..6: every claimed-feasible n is built and replayed + words_k = 0 + for k in range(3, 10): + for r in range(1, 7): + for n in range(2, k * r + 1, 2): + out = construct_k(n, k, r) + if not k_rule(n, k, r): + need(out is None, "k constructor accepted an excluded n") + continue + need(out not in (None, "cap"), f"k construction failed n={n} k={k} r={r}") + need(replay_k(out, r), f"k replay n={n} k={k} r={r}") + need(sum(rank(N) for N in out) == n + -(-n // m_k(k)), "k total rank") + words_k += 1 + for r in range(1, 200): # the k = 4 rule is PR6122's 2 floor(4r/3) + need(max(n for n in range(2, 4 * r + 1, 2) if k_rule(n, 4, r)) == 2 * (4 * r // 3), "k=4 agreement") + for n in range(2, 40, 2): # rank-one caps reproduce the n+1 minimum-query simplex + need(min(k for k in range(3, 50) if k_rule(n, k, 1)) == n + 1, "rank-one minimum") + result["k_calls"] = {"k_range": [3, 9], "cap_range": [1, 6], "words_replayed": words_k, + "five_call_capacity_r1_to_6": [max(n for n in range(2, 5 * r + 1, 2) if k_rule(n, 5, r)) for r in range(1, 7)], + "six_call_capacity_r1_to_6": [max(n for n in range(2, 6 * r + 1, 2) if k_rule(n, 6, r)) for r in range(1, 7)]} + + # 3. controls + ctl = {} + # (a) decider finds a witness for a reachable non-scalar target (E_21 at n=2, + # caps (1,0,0,0): the normal form E_12 alone would miss it) + sz2, irr2 = store[2] + target = (0, 1) + w, _ = decide(2, (1, 0, 0, 0), sz2, irr2, target) + ctl["reachable_nonidentity_target_found"] = w is not None and check_witness(w, (1, 0, 0, 0), target) + # (b) an invertible non-identity target with odd trace is unreachable at any caps + odd = tuple((1 << i) | ((1 << (i + 1)) if i < 2 else 0) for i in range(3)) + sz3, irr3 = store[3] + w, _ = decide(3, (1, 1, 1, 1), sz3, irr3, odd) + ctl["odd_trace_target_rejected"] = w is None + # (c) planted false witnesses fail the check + good = construct(6, (3, 3, 3, 0)) + need(good is not None and replay(*good, (3, 3, 3, 0)), "positive fixture") + bad_rank = check_witness((eye(6), zero(6), zero(6), zero(6)), (3, 3, 3, 3), eye(6)) + ctl["non_square_zero_witness_rejected"] = not bad_rank + # (d) mutated words fail the replay + layers, final = construct(8, (3, 3, 3, 3)) + m1 = [zero(8)] + layers[1:] + m2 = [layers[1], layers[0]] + layers[2:] + ctl["dropped_layer_rejected"] = not replay(m1, final, (3, 3, 3, 3)) + ctl["swapped_layers_rejected"] = not replay(m2, final, (3, 3, 3, 3)) + ctl["rank_cap_violation_rejected"] = not replay(layers, final, (2, 3, 3, 3)) + ctl["constructor_refuses_6_at_cap_2"] = construct(6, (2, 2, 2, 2)) is None + ctl["constructor_refuses_10_at_cap_3"] = construct(10, (3, 3, 3, 3)) is None + five = construct_k(8, 5, 2) + ctl["five_calls_rank_two_twist_eight"] = five not in (None, "cap") and replay_k(five, 2) + ctl["five_call_word_needs_its_constants"] = not replay(five, eye(8), (2,) * 5) + ctl["five_call_word_order_free"] = replay_k(list(reversed(five)), 2) + ctl["five_calls_rank_two_refuse_ten"] = construct_k(10, 5, 2) is None + need(all(ctl.values()), f"controls {ctl}") + result["controls"] = ctl + + if not compare: + print(json.dumps(result, sort_keys=True, indent=2)) + return + expected = json.loads((Path(__file__).resolve().parent / "RESULT.json").read_text()) + need(expected == result, "RESULT.json differs from the recomputed result") + print(json.dumps(result, sort_keys=True)) + print("PASS_FOUR_BLOCK_QUERY_CAPACITY_AUDIT") + + +if __name__ == "__main__": + need(sys.argv[1:] in ([], ["--print-result"]), "usage: verify.py [--print-result]") + main(compare=not sys.argv[1:])