diff --git a/research/restored-dirty-query-capacity/PROOF.md b/research/restored-dirty-query-capacity/PROOF.md new file mode 100644 index 0000000000..c5f4233189 --- /dev/null +++ b/research/restored-dirty-query-capacity/PROOF.md @@ -0,0 +1,171 @@ +# Restored dirty helpers do not increase square-zero query capacity + +This contribution was produced by Nick Petalas. Apache-2.0. + +## 1. Statement and credited premise + +Let K be any field of characteristic two and let +R = K[Q]/(Q^2-1). The symbol Q is a formal central involution. +Fix n>0 target coordinates, h>=0 arbitrary dirty helper coordinates, +k>=3 available paid calls, and a nonnegative integer rank cap r. +Free gates are arbitrary constant matrices in GL_(n+h)(K). +A paid gate is I+Q N, where N is constant, N^2=0, and rank(N)<=r. +The complete required endpoint on every input is + +```text +diag(Q I_n, I_h). +``` + +Thus every original helper value must return unchanged, without a promise +on its value or correlations with the target inputs. +Put m_k=2 floor((k-1)/2). The endpoint is possible with at most k calls iff + +```text +n is even and n + ceil(n/m_k) <= k r. +``` + +Whenever feasible, its least total paid rank with at most k calls is +n+ceil(n/m_k). +Neither statement depends on h. Zero-rank calls may pad a shorter word. + +The new part is necessity for arbitrary h. Josie Elliston's +[PR #6138](https://github.com/CrocSwap/integer-mult-bounds/pull/6138), +`research/four-block-query-capacity-audit/README.md`, finding 5, supplies +the workspace-free attaining construction. We use that theorem as a cited +premise and extend its words by the identity on h helpers. We do not replay +its computations or claim its construction. Its four-call theorem credits +Nick Petalas #6122, its simplex credits Cinna Davis, its Gram framework +credits Ali Romman #5617, and its source question credits Matarener #6114. + +## 2. Normalize to a projection, keeping every helper + +Set epsilon=Q+1, so epsilon^2=0 and R=K[epsilon]/(epsilon^2). +For square-zero N, + +```text +I+Q N = (I+N)(I+epsilon N). +``` + +Move the constant factors and free gates to one side, conjugating the N's +by constant invertible matrices. Rank and square-zero are preserved. +The constant part of the required endpoint is I, so the complete endpoint +is equivalent to + +```text +sum_(i=1)^k R_i = P, +R_i^2=0, +P=diag(I_n,0_h). +``` + +All products involving two epsilon terms vanish. Conversely, such a sum +implements I+epsilon P by preceding each paid I+Q R_i with the free I+R_i. +This equivalence keeps the whole arbitrary-input matrix, including both +off-diagonal helper blocks. It does not discard helper information. + +Let r_i=rank(R_i) and S=sum r_i. Since a square-zero matrix has trace zero, +trace(P)=n times 1_K=0, so n must be even. + +## 3. The projection Gram complement + +Factor R_i=U_i V_i with U_i injective and V_i surjective through K^(r_i). +Then V_i U_i=0, since U_i(V_i U_i)V_i=R_i^2=0. +Concatenate the U_i horizontally into U and the V_i vertically into V. +Thus UV=P. Let + +```text +X=VU on K^S, Y=I_S+X, d=S-n. +``` + +The call-diagonal blocks of X vanish, so Y_ii=I_(r_i). +Although P is a projection, X need not be one. Instead, + +```text +X^3=V P^2 U=V P U=X^2, +Y^3=Y. +``` + +The fixed space of X has dimension n. Indeed, U and V restrict to inverse +maps between ker(I_S+X) and im(P). For Xv=v, P(Uv)=Uv and VUv=v. +For Pw=w, XVw=Vw and UVw=w. Therefore rank(Y)=S-n=d. + +Take a full-rank factorization Y=A B through K^d. Since Y^3=Y, +injectivity of A and surjectivity of B give + +```text +C=BA, C^2=I_d. +``` + +In particular C is invertible. Partition A into call row blocks A_i +and B into matching column blocks B_i. The call-diagonal equations give + +```text +A_i B_i=I_(r_i), +E_i=B_i A_i, E_i^2=E_i, rank(E_i)=r_i, +sum E_i=C. +``` + +Consequently r_i<=d. When h=0, the old argument can take C=I_d. +With dirty helpers, C can be a nonidentity involution I_d+Z with Z^2=0. +Invertibility, rather than identity, is the property needed below. + +## 4. The rank bound for every call count + +If k is odd, sum r_i<=k d immediately gives + +```text +(k-1) S >= k n, +S >= n + ceil(n/(k-1)). +``` + +If k is even, characteristic two gives sum(I_d+E_i)=C. +Each I_d+E_i has rank d-r_i, while C has rank d. Rank subadditivity yields + +```text +d <= sum(d-r_i) = k d-S, +(k-2) S >= (k-1) n, +S >= n + ceil(n/(k-2)). +``` + +Together these say S>=n+ceil(n/m_k). Since S<=k r, the stated uniform-cap +condition is necessary. The credited workspace-free construction proves +sufficiency and equality for total rank. This finishes the scoped theorem. + +For example, four rank-two paid calls cannot twist six independent +coordinates even when any number of arbitrary dirty helpers may be mixed +into every call and must eventually return unchanged. The new conclusion +is the independence from the helper count, not the predecessor's +workspace-free numerical bound. + +## 5. A genuine nilpotent defect and the clean-helper boundary + +Write binary matrices as integer-coded rows, with the least significant +bit the first column. The four three-by-three matrices + +```text +(0,6,6), (6,6,6), (0,5,0), (7,7,0) +``` + +are square-zero rank-one matrices with sum diag(1,1,0). Their stacked +X=VU is not idempotent, and the complement factor has C!=I but C^2=I. +The verifier reconstructs these facts without treating the coded rows as +a receipt. Thus replacing the predecessor's identity by a projection +requires the new argument in section 3. + +Initialized clean helpers have a different contract. The two-by-two terms + +```text +(2,0), (0,1), (3,3) +``` + +sum to I_2 and yield endpoint Q I_2. On (x,0) this twists one target and +returns the zero helper, despite n=1 being odd. On (x,y) it also twists y. +It therefore fails dirty restoration. The theorem does not cover a +zero-initialized helper promise, discarded outputs, nonlinear controls, +Q-dependent free gates, non-square-zero paid gates or approximate equality. + +This is an abstract query-capacity obstruction. Native implementation, +physical basis-change costs, independent stage multipliers, storage, +precision, a complete supplier invoice and the five selected framework +assumptions remain outside the claim. No new kappa or complete +multiplication theorem follows. The all-field proof is written mathematics; +finite binary checks do not provide formal proof-kernel acceptance. diff --git a/research/restored-dirty-query-capacity/README.md b/research/restored-dirty-query-capacity/README.md new file mode 100644 index 0000000000..8df37528f5 --- /dev/null +++ b/research/restored-dirty-query-capacity/README.md @@ -0,0 +1,131 @@ +# Exact query capacity with restored dirty helpers + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with exact finite corroboration; no new kappa.** An arbitrary +finite bank of restored dirty helpers cannot lower the square-zero query +capacity in characteristic two. This answers the dirty-workspace part of +Josie Elliston's [PR #6138](https://github.com/CrocSwap/integer-mult-bounds/pull/6138), +second Open next question. Its workspace-free attaining theorem is a cited +premise, not a replay target. + +Over any characteristic-two field K, let Q be a formal central involution. +Free gates are constant invertible matrices. Each paid gate is I+Q N with +N^2=0 and rank(N)<=r. There are n>0 independent targets and any h>=0 +independent dirty helpers. The full endpoint must be diag(Q I_n,I_h). +For k>=3 available calls and m_k=2 floor((k-1)/2), feasibility is exactly + +```text +n is even and n + ceil(n/m_k) <= k r. +``` + +Whenever feasible, the least total paid rank is n+ceil(n/m_k), independently of h. +For example, adding restored dirty helpers cannot make four rank-two calls +twist six independent targets. The same capacity without helpers was +already proved by #6138; the new result is its invariance under arbitrary +finite dirty workspace. + +[PROOF.md](PROOF.md) gives the all-field argument. Normalization replaces +an identity endpoint by a projection P. The call Gram matrix X then only +satisfies X^3=X^2. Factoring Y=I+X yields an invertible complement core C +with C^2=I, rather than C=I. Its diagonal blocks still give idempotents. +Rank subadditivity recovers the same even-call bound; a separate dimension +count gives the odd-call bound. A nonidentity core occurs in the finite +fixtures, so the identity-only predecessor argument cannot be reused +without this step. + +## Evidence and reproduction + +From the repository root, with the interpreter used locally: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/restored-dirty-query-capacity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/restored-dirty-query-capacity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/restored-dirty-query-capacity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/restored-dirty-query-capacity --check-source-history +``` + +Elsewhere substitute a CPython 3.12 path. Only the standard library is +needed. The direct verifier emits `PASS_RESTORED_DIRTY_QUERY_CAPACITY` +in a generated JSON receipt bound to the six package files' SHA256 hashes. +It writes no files and imports no predecessor program. + +- A complete three-coordinate, four-call binary fixture uses two target + coordinates and one arbitrary restored dirty helper. Pair joins and a + separate direct scan of all 234,256 ordered four-tuples both find exactly + 648 valid words. The new complement identities hold for each, including + all 288 nonidentity cores. Literal quotient-ring execution checks all + eight dirty inputs of each word, for 5,184 executions. +- Padded dirty-helper fixtures exercise each call count from three through + eight, covering both parity branches of the new rank argument. +- A separate complete two-pair minimization on four coordinates, two targets + and two dirty helpers, gives minimum total rank three for caps one and + two. It includes respectively 11,236 and 99,856 ordered pairs and retains + every pair-sum cost. It does not enumerate all ordered four-tuples in this + larger domain. +- Four rejecting controls cover a non-square-zero summand with unchanged + total, the wrong complete endpoint, a nonprojection, and the enumeration + dimension limit. A literal clean-helper example shows why a zero-input + promise does not imply dirty restoration. + +The written proof, not these small fixtures, establishes arbitrary field, +helper count and dimension. No predecessor counts were replayed as the +contribution. [SOURCES.json](SOURCES.json) pins the source question and +attainment theorem as historical provenance at canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. + +## Limits and expansion decision + +This theorem requires exact formal equality, constant free controls, +square-zero paid terms, and restoration of every arbitrary helper input. +Initialized clean helpers, discarded helper outputs, non-square-zero paid +operations, nonlinear controls and approximation remain outside its scope. +The clean-helper example in the proof can twist one target using three +rank-one calls and a clean zero helper, while its full dirty endpoint fails. + +There is no physical multi-bank query, native alignment, charged basis +implementation, stage chronology, complete signed invoice, compiler or +precision/tape construction. The five selected framework assumptions are +unchanged. No selected cold replay, Lean or Docker run, independent human +review or formal proof-kernel acceptance is claimed. + +This closes the restored-dirty-workspace route in this model. Further +construction work needs a changed hypothesis and a complete favorable +physical bill. A larger search inside the same dirty model is unnecessary. +The non-square-zero and initialized-clean alternatives remain open and +are not assigned by this package. + +Power of Ten rule 3 has a managed-runtime deviation. Python allocates +integers, tuples and dictionaries during verification. Scientific loops +have fixed bounds: dimension at most four, at most 65,536 candidate +matrices per census, 234,256 streamed raw four-tuples, and at most 65,536 +pair-sum keys. Gram fixtures use at most eight calls and matrices of width +at most eight. There is no recursion, network operation, subprocess or +dynamic code in the verifier. Every function is below 60 physical lines. +Warning-strict normal and optimized commands are registered. The deviation +is confined to this terminating verifier; any larger search must introduce +new capacity bounds before expanding it. + +## Open next questions + +- Can initialized clean helpers reduce the paid-rank floor for even target + dimensions? This would separate clean from restored dirty capacity beyond + the odd-dimension example. First classify the permitted unspecified + helper-column blocks in a normalized endpoint. The complete endpoint and + clean-return contract need to be fixed before claiming a capacity. +- Which invertible non-square-zero paid alphabet can improve a real caller? + This is the remaining distinct branch of #6138's second question. First + specify a native gate, its complete arbitrary-input response and paid + rank. No such physical gate or profitable invoice is supplied here. + +## Credit + +Josie Elliston's #6138 supplies the question, all-call workspace-free +attainment theorem and its stated unresolved workspace boundary. Credit +Nick Petalas #6122 for the earlier four-call theorem, Cinna Davis for the +rank-one simplex and controller lineage, Ali Romman #5617 for the coupled +Gram framework and block simplex, and Matarener #6114 for the higher-rank +query question. Rank factorization, kernel correspondence and rank +subadditivity are standard linear algebra. The new contribution is the +projection-complement involution argument and the resulting sharp +restored-dirty-workspace exclusion. No predecessor credit line is changed. diff --git a/research/restored-dirty-query-capacity/SOURCES.json b/research/restored-dirty-query-capacity/SOURCES.json new file mode 100644 index 0000000000..3ccb844af1 --- /dev/null +++ b/research/restored-dirty-query-capacity/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/four-block-query-capacity-audit/README.md", + "usage": "provenance", + "git_blob": "dce26f6675af8df3b236ae62c80f10b9166ac739", + "sha256": "157b0e171f7fd9e6b4b0a090ddd7afd2c680efa59b4026a36e4910e56802d4b5" + } + ] +} diff --git a/research/restored-dirty-query-capacity/TASK.json b/research/restored-dirty-query-capacity/TASK.json new file mode 100644 index 0000000000..ac2b206882 --- /dev/null +++ b/research/restored-dirty-query-capacity/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Prove that any finite restored arbitrary dirty helper bank leaves the exact characteristic-two square-zero query capacity unchanged for every k>=3: n even and n+ceil(n/(2 floor((k-1)/2)))<=k r. Extend the projection Gram complement and cite PR6138 for workspace-free attainment.", + "scope_change_reason": "This answers PR6138 Open next question 2 in the restored-dirty subcase. It is an abstract query-capacity side result with a changed helper contract, rather than a physical current-supplier construction or an audit of predecessor mathematics.", + "bottleneck_link": "Closes restored dirty helper mixing as a capacity escape for bounded-rank central square-zero queries. Native realization, physical prices and a full supplier invoice remain separate; no kappa improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original projection-complement result and package it; do not extend to clean helpers or non-square-zero gates.", + "outcome": "completed", + "evidence": "PROOF.md sections 2-4; standalone exact verifier with complete binary dirty-helper fixtures and a nonidentity complement core.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can initialized clean helpers lower the floor at even target dimensions?", + "why_it_matters": "The theorem closes only full arbitrary-input dirty restoration; a clean promise can already evade target parity.", + "first_step": "Specify all normalized helper-column blocks allowed by the zero-input and clean-return contract.", + "blocked_by": "No physical clean-helper caller or complete price is supplied." + }, + { + "question": "Can an invertible non-square-zero paid alphabet improve an actual caller?", + "why_it_matters": "It changes the square-zero premise and is the remaining distinct branch of PR6138 question 2.", + "first_step": "Name one native gate and its full arbitrary-input response, rank and bill.", + "blocked_by": "No qualifying gate or complete profitable invoice is supplied." + } + ], + "source_question": { + "pr": 6138, + "author": "JosieElliston", + "location": "README.md, second Open next question", + "retained_at": "7c49fe32c55de02c2c873655c804b16e4c3fef0a" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19441276", + "local_environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "machine": "arm64" + } +} diff --git a/research/restored-dirty-query-capacity/VERIFY.json b/research/restored-dirty-query-capacity/VERIFY.json new file mode 100644 index 0000000000..537e1ee828 --- /dev/null +++ b/research/restored-dirty-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": 60, + "checks": "Projection Gram complement, complete dirty-helper fixture, independent raw enumeration, literal formal endpoints, exact two-pair minima and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same mathematical checks remain active under optimized Python." + } + ] +} diff --git a/research/restored-dirty-query-capacity/verify.py b/research/restored-dirty-query-capacity/verify.py new file mode 100644 index 0000000000..aee5fdb332 --- /dev/null +++ b/research/restored-dirty-query-capacity/verify.py @@ -0,0 +1,262 @@ +#!/usr/bin/env python3 +"""Exact checks for projection endpoints with restored arbitrary dirty helpers.""" + +import hashlib +import itertools +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def eye(n): + require(0 <= n <= 64, "matrix dimension outside fixture bound") + return tuple(1 << i for i in range(n)) + + +def add(a, b): + require(len(a) == len(b), "row count mismatch") + return tuple(x ^ y for x, y in zip(a, b)) + + +def mul(a, b): + require(len(a) <= 64 and len(b) <= 64, "matrix dimension limit") + require(all(0 <= row < (1 << len(b)) for row in a), "bad inner dimension") + result = [] + for row in a: + value = 0 + for j, other in enumerate(b): + if (row >> j) & 1: + value ^= other + result.append(value) + return tuple(result) + + +def factor(matrix): + """Return a full-rank factorization U V of a binary rectangular matrix.""" + require(len(matrix) <= 64, "too many rows") + require(all(0 <= row < (1 << 64) for row in matrix), "row width limit") + pivots = {} + for row in matrix: + value = row + for pivot in sorted(pivots, reverse=True): + if (value >> pivot) & 1: + value ^= pivots[pivot] + if value: + pivots[value.bit_length() - 1] = value + basis = tuple(pivots[p] for p in sorted(pivots, reverse=True)) + coordinates = [] + for row in matrix: + value, code = row, 0 + for j, vector in enumerate(basis): + if (value >> (vector.bit_length() - 1)) & 1: + value ^= vector + code ^= 1 << j + require(value == 0, "row not in computed span") + coordinates.append(code) + u = tuple(coordinates) + require(mul(u, basis) == matrix, "rank factorization residual") + return u, basis + + +def rank(matrix): + return len(factor(matrix)[1]) + + +def total(matrices, rows): + result = (0,) * rows + for matrix in matrices: + result = add(result, matrix) + return result + + +def complement_data(terms, projection): + """Check the new projection Gram lemma, including its nonidempotent case.""" + size = len(projection) + require(3 <= len(terms) <= 8 and size <= 4, "fixture bound exceeded") + require(mul(projection, projection) == projection, "endpoint is not a projection") + require(total(terms, size) == projection, "wrong complete dirty endpoint") + u_rows, v_rows, widths = [0] * size, [], [] + for term in terms: + require(mul(term, term) == (0,) * size, "paid term is not square-zero") + u, v = factor(term) + width = len(v) + require(mul(v, u) == (0,) * width, "factor is not square-zero") + for j in range(size): + u_rows[j] |= u[j] << len(v_rows) + v_rows.extend(v) + widths.append(width) + u, v = tuple(u_rows), tuple(v_rows) + s, n = len(v), rank(projection) + require(mul(u, v) == projection, "stacked factorization residual") + x = mul(v, u) + y = add(eye(s), x) + require(mul(mul(x, x), x) == mul(x, x), "X cubed differs from X squared") + require(mul(mul(y, y), y) == y, "Y cubed differs from Y") + d = s - n + require(rank(y) == d, "wrong complement dimension") + a, b = factor(y) + c = mul(b, a) + require(mul(c, c) == eye(d), "complement core is not an involution") + check_blocks(a, b, c, widths, n) + return c != eye(d), s + + +def check_blocks(a, b, c, widths, n): + d, offset, pieces = len(b), 0, [] + for width in widths: + ai = a[offset:offset + width] + bi = tuple((row >> offset) & ((1 << width) - 1) for row in b) + require(mul(ai, bi) == eye(width), "lost diagonal identity block") + e = mul(bi, ai) + require(mul(e, e) == e and rank(e) == width, "bad block idempotent") + pieces.append(e) + offset += width + require(total(pieces, d) == c, "block sum residual") + require(all(width <= d for width in widths), "elementary rank bound") + k, s = len(widths), sum(widths) + if k % 2 == 0: + complements = tuple(add(eye(d), e) for e in pieces) + require(total(complements, d) == c, "even-call complement sum") + require(d <= sum(d - width for width in widths), "even-call rank bound") + m = 2 * ((k - 1) // 2) + require(n % 2 == 0, "odd projection rank") + require(s >= n + (n + m - 1) // m, "claimed helper-independent floor") + + +def square_zeros(size, cap): + require(1 <= size <= 4 and 0 <= cap <= size // 2, "census bound exceeded") + result = [] + mask = (1 << size) - 1 + for packed in range(1 << (size * size)): + matrix = tuple((packed >> (size * j)) & mask for j in range(size)) + if mul(matrix, matrix) == (0,) * size: + cost = rank(matrix) + if cost <= cap: + result.append((matrix, cost)) + return tuple(result) + + +def apply_matrix(matrix, vector): + return sum(((row & vector).bit_count() & 1) << j for j, row in enumerate(matrix)) + + +def literal_word(terms, projection): + """Execute free I+R and paid I+Q R, with Q=1+epsilon, on every dirty input.""" + size = len(projection) + for value in range(1 << size): + constant, epsilon = value, 0 + for term in terms: + free = add(eye(size), term) + constant = apply_matrix(free, constant) + epsilon = apply_matrix(free, epsilon) + old = constant + constant = apply_matrix(free, old) + epsilon = apply_matrix(free, epsilon) ^ apply_matrix(term, old) + require(constant == value, "constant endpoint differs") + require(epsilon == apply_matrix(projection, value), "dirty epsilon endpoint differs") + + +def complete_three_coordinate_fixture(): + atoms = square_zeros(3, 1) + projection = (1, 2, 0) + pairs = {} + for first, second in itertools.product(atoms, repeat=2): + pairs.setdefault(add(first[0], second[0]), []).append((first[0], second[0])) + count, defects, executions, witness, short = 0, 0, 0, None, None + for value, left_pairs in pairs.items(): + for left in left_pairs: + for right in pairs.get(add(value, projection), ()): + terms = left + right + defect, cost = complement_data(terms, projection) + literal_word(terms, projection) + count += 1 + defects += int(defect) + executions += 8 + if defect and witness is None: + witness = {"terms": terms, "projection": projection, "total_rank": cost} + if short is None and (0, 0, 0) in terms: + short = tuple(term for term in terms if term != (0, 0, 0)) + require(witness is not None, "nilpotent-defect case was not exercised") + require(short is not None and len(short) == 3, "missing three-call fixture") + for k in range(3, 9): + complement_data(short + ((0, 0, 0),) * (k - 3), projection) + packed_atoms = tuple(sum(row << (3 * j) for j, row in enumerate(a)) for a, _ in atoms) + raw_count = sum(a ^ b ^ c ^ d == 17 + for a, b, c, d in itertools.product(packed_atoms, repeat=4)) + require(count == raw_count == 648 and defects == 288, "complete census mismatch") + return {"words": count, "nonidentity_cores": defects, + "dirty_input_executions": executions, "defect_witness": witness, + "raw_four_tuple_candidates": len(atoms) ** 4, "call_counts_checked": list(range(3, 9))} + + +def four_coordinate_minima(): + projection = (1, 2, 0, 0) + minima = {} + for cap in (1, 2): + atoms = square_zeros(4, cap) + pair_cost = {} + for (first, a), (second, b) in itertools.product(atoms, repeat=2): + key = add(first, second) + pair_cost[key] = min(pair_cost.get(key, 65), a + b) + best = min(cost + pair_cost[add(value, projection)] + for value, cost in pair_cost.items() + if add(value, projection) in pair_cost) + require(best == 3, "four-coordinate dirty minimum changed") + minima[str(cap)] = {"minimum_total_rank": best, + "pair_sums": len(pair_cost), "ordered_pairs": len(atoms) ** 2} + return minima + + +def rejecting_controls(): + projection = (1, 2, 0) + valid = ((0, 6, 6), (6, 6, 6), (0, 5, 0), (7, 7, 0)) + damaged = (add(valid[0], (1, 0, 0)), add(valid[1], (1, 0, 0))) + valid[2:] + bad = [ + (damaged, projection, "paid term is not square-zero"), + (((0, 0, 0),) * 4, projection, "wrong complete dirty endpoint"), + (((0, 0, 0),) * 4, (2, 0, 0), "endpoint is not a projection"), + ] + rejected = 0 + for terms, endpoint, message in bad: + try: + complement_data(terms, endpoint) + except ValueError as error: + require(str(error) == message, "wrong rejection reason") + rejected += 1 + try: + square_zeros(5, 2) + except ValueError as error: + require(str(error) == "census bound exceeded", "wrong dimension rejection") + rejected += 1 + require(rejected == len(bad) + 1, "a malformed candidate passed") + # These terms twist both coordinates. A zero second input stays zero, + # but an arbitrary dirty second input is twisted and is not restored. + clean_only = ((2, 0), (0, 1), (3, 3)) + literal_word(clean_only, eye(2)) + require(apply_matrix(eye(2), 1) == 1, "clean entrance control failed") + require(apply_matrix(eye(2), 2) != apply_matrix((1, 0), 2), + "arbitrary dirty input did not distinguish endpoints") + return {"rejected_candidates": rejected, "clean_helper_boundary": True} + + +def main(): + report = { + "status": "PASS_RESTORED_DIRTY_QUERY_CAPACITY", + "three_coordinate_complete_fixture": complete_three_coordinate_fixture(), + "four_coordinate_exact_minima": four_coordinate_minima(), + "controls": rejecting_controls(), + } + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + report["source_sha256"] = { + name: hashlib.sha256((package / name).read_bytes()).hexdigest() for name in names + } + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()