From 3351f1b59db9c094877227bad16ccd4597bbc8c1 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Sun, 1 Nov 2026 13:33:48 +0000 Subject: [PATCH] Prove idle helpers do not lower the span-(m+1) line bound Extra clean or dirty monomial registers leave the direct m*t call count optimal whenever the rational frame span has dimension at most m+1 and the normalized extra frame is not in the |K|=2 block. No new kappa. Co-authored-by: unpaidmoon --- research/span-lemma-idle-helpers/PROOF.md | 194 ++++++++++++++ research/span-lemma-idle-helpers/README.md | 113 +++++++++ research/span-lemma-idle-helpers/SOURCES.json | 30 +++ research/span-lemma-idle-helpers/TASK.json | 75 ++++++ research/span-lemma-idle-helpers/VERIFY.json | 37 +++ research/span-lemma-idle-helpers/verify.py | 238 ++++++++++++++++++ 6 files changed, 687 insertions(+) create mode 100644 research/span-lemma-idle-helpers/PROOF.md create mode 100644 research/span-lemma-idle-helpers/README.md create mode 100644 research/span-lemma-idle-helpers/SOURCES.json create mode 100644 research/span-lemma-idle-helpers/TASK.json create mode 100644 research/span-lemma-idle-helpers/VERIFY.json create mode 100644 research/span-lemma-idle-helpers/verify.py diff --git a/research/span-lemma-idle-helpers/PROOF.md b/research/span-lemma-idle-helpers/PROOF.md new file mode 100644 index 0000000000..0a52d77f4c --- /dev/null +++ b/research/span-lemma-idle-helpers/PROOF.md @@ -0,0 +1,194 @@ +# Idle registers do not lower the span-(m+1) line bound + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +This is a written scoped proof. The finite checks in `verify.py` corroborate +algebraic steps; they are not a substitute for the argument and they are not +proof-kernel verification. + +## 1. Model + +Fix an address dimension `m >= 1`, a data-register count `t >= 1` and a helper +count `r >= 0`. Set `n = t + r`. Work in the group algebra `R = F_2[M_m(Q)]` +of the additive group of rational `m x m` matrices, with `[A][B] = [A+B]`. +The identity element is `[0]`. A paid call is + + D_N([A]) = I_n + ([A] - 1) N, rank_Q(A) = 1, N = x y^T, y^T x = 1, + +with `x, y` in `F_2^n`. A word of `k` paid calls is required to satisfy + + prod_j D_{N_j}([A_j]) = diag([C_1], ..., [C_t], [H_1], ..., [H_r]), (1) + +where every `C_s` is invertible and every helper exponent `H_j` is an +arbitrary single matrix. A clean helper has `H_j = 0`. A dirty helper may +carry any monomial `[H_j]`. Equality is of every formal coefficient. There +is no free address map between calls. + +This is the scalar-idempotent model of eumemic's PR #288, section 1.2, as +used by Ali Romman's PR #468 and by Nick Petalas's +`research/span-lemma-every-dimension`. Those statements take `r = 0` and +require every diagonal entry to be invertible. The one-relation theorem in +`research/bit-one-relation-any-registers` already allows arbitrary `n` when +the frames have at most one rational relation. It is not reused as a lemma +here; the span window below is the complementary small-span regime. + +Let `S` be the rational span of the paid frames. As in PR #468, section 3, +every exponent that survives in (1) lies in `S`, because a diagonal entry is +an `F_2`-combination of subset sums of frames and the surviving symbol is a +single group element. + +## 2. Statement + +**Theorem.** Suppose `dim S <= m + 1`, and write the normalized extra frame +of `research/span-lemma-every-dimension`, section 3, as `u v^T` with +`K = supp(u) ∩ supp(v)`. + +1. If `dim S <= m`, or `dim S = m + 1` and `|K| != 2`, then `k >= m t`. +2. The same word with `r` clean helpers attains `k = m t`. + +Identity helpers and arbitrary dirty monomial helpers therefore do not lower +the call bound in every case that the predecessor reduces to its Lemma A +(the line projection) or to the triangular diagonal projection. The +`|K| = 2` flag bound is not extended. + +No new κ follows. The selected record stays the value pinned in +`certificates/selected-result.json`. + +## 3. Rank of a rank-one product + +**Lemma R.** Over a commutative ring, let `a_j` be scalars and let +`x_j, y_j` be column vectors. Then + + P = prod_{j=1}^{k} (I + a_j x_j y_j^T) + +satisfies `rank(P - I) <= k` whenever the scalar ring is an integral domain +and the rank is computed over its fraction field. Idempotence of the +updates is not required. + +*Proof.* Proceed by induction on the column space. The case `k = 0` is +`P = I`. If the columns of `P_{j-1} - I` lie in `span{x_1, ..., x_{j-1}}`, +then + + P_j - I = (P_{j-1} - I) + a_j x_j (y_j^T P_{j-1}). + +The row `y_j^T P_{j-1}` is a coordinate row, so the second summand has +columns in `span{x_j}`. The columns of `P_j - I` lie in +`span{x_1, ..., x_j}`. ∎ + +PR #468, section 2, records the sharper triangular factorization +`P = I + X T Y^T` for the idempotent case. Lemma R is the only rank input +used below. + +## 4. Line projection with helpers + +**Lemma A'.** Let `b_0, ..., b_s` be a basis of `S` made of rank-one +matrices, and suppose every paid frame is a rational multiple of one +`b_i`. Then + + k >= sum_{s=1}^{t} nnz(C_s) >= m t, + +where `nnz` is the number of nonzero coordinates in this basis. Helper +exponents do not appear on the right-hand side. + +*Proof.* Let `phi_i` be the `i`th coordinate functional on `S`. The rule +`[A] -> [phi_i(A)]` is a ring homomorphism from `F_2[S]` onto its image in +`F_2[Q]`. Apply it entrywise to (1). A call whose frame lies on another +line has `phi_i(A_j) = 0`, so that call maps to `I`. Let `k_i` be the +number of calls on line `i`. Lemma R, applied over the fraction field of a +Laurent polynomial domain, gives rank at most `k_i` for the image of the +product minus `I`. + +The image of the right-hand side minus `I` is the diagonal matrix with +entries `[phi_i(C_s)] - 1` and `[phi_i(H_j)] - 1`. In that fraction field, +`t^c - 1 = 0` if and only if `c = 0`. The rank of a diagonal matrix equals +the number of nonzero diagonal entries, so the rank is at least the number +of data indices with `phi_i(C_s) != 0`. A helper can add a nonzero entry. +It cannot cancel a data entry, because the output is diagonal. Therefore +`k_i >= #{s : phi_i(C_s) != 0}`. + +A frame lies on at most one line: it is a multiple of a single basis +matrix. Summing over lines gives `k >= sum_s nnz(C_s)`. Each `C_s` is a +sum of `nnz(C_s)` rank-one matrices, so `m = rank(C_s) <= nnz(C_s)`. ∎ + +The clean case `H_j = 0` has `phi_i(H_j) = 0` on every line, so those +diagonal entries contribute nothing. That is the identity-helper case asked +for by the predecessor's open question. + +## 5. The three address cases that reduce to a projection + +The normalization in `research/span-lemma-every-dimension`, section 3, is a +change of address coordinates `A -> P A Q`. It is an automorphism of the +additive group, preserves rank, and does not depend on `n` or on which +diagonal entries are invertible. Invertible targets remain invertible, and +the zero matrix remains zero. After that normalization the predecessor's +address lemmas apply verbatim. They never mention the register count. + +**Dimension at most `m`.** An invertible `m x m` matrix cannot lie in a +rational matrix space of dimension less than `m`. Thus `dim S = m`. PR #468's +low-span lemma puts `S` on `m` diagonal lines `E_ii`, and every paid frame +in that diagonal space is a multiple of one `E_ii`. An invertible diagonal +matrix has every diagonal entry nonzero, so `nnz(C_s) = m`. Lemma A' gives +`k >= m t`. + +**`|K| >= 3`.** Lemma C of the predecessor says every rank-one matrix of +`S` lies on one of the `m + 1` lines spanned by `E_00, ..., E_{m-1,m-1}` and +`B = u v^T`. The minor identity used there is an address calculation. Lemma +A' again gives `k >= m t` for arbitrary invertible data targets. + +**`|K| <= 1`.** The predecessor's Lemma D makes `S` triangular after a +permutation. Each transformed data target is invertible and triangular, so +all `m` diagonal entries are nonzero. A rank-one triangular matrix has at +most one nonzero diagonal entry: two nonzero diagonal entries `i` and `j` +would force both off-diagonal entries of that `2 x 2` block to be nonzero, +because a rank-one matrix is an outer product. Projecting onto that +diagonal coordinate, as in Lemma A', assigns each paid call to at most one +coordinate and shows that each coordinate is hit by at least `t` calls. +Hence `k >= m t`. + +## 6. What stays open at `|K| = 2` + +The predecessor's `|K| = 2` case cites PR #468's block flag bound: `2W` +calls on the `2 x 2` block and `W` calls on each `1 x 1` block, using that +every one of the `W` targets has invertible diagonal blocks. A clean helper +has exponent `0`, whose diagonal blocks are zero, not invertible. Lemma A' +does not apply, because Lemma C fails at `|K| = 2` (the predecessor's +explicit off-line example `u = v = (1, 1, 0)`, `D = diag(2, 2, 0)`, +`t = -1`). This note does not claim `k >= m t` for that case. + +## 7. The bound is attained with any number of clean helpers + +Write each invertible `C_s` as a sum of `m` rank-one matrices and apply +those `m` frames with the coordinate projector `E_{ss}`. No call touches a +helper register, so each helper stays at `[0]`. The product is (1), the +frame span has dimension at most `m`, and `k = m t`. Adding clean helpers +does not create a shorter word in the regimes of section 5, and it does +not increase the direct cost. + +## 8. Neighbouring results that do not already contain this statement + +- PR #468 proves `k >= m W` when `r = 0` and `m = 3` for span at most 4. + Its statement excludes extra registers. +- `research/span-lemma-every-dimension` extends that span bound to every + `m`, still with `r = 0`. Its open question 3 asks whether Lemma A + survives identity helper targets. Sections 4 and 5 answer that question + for every case the predecessor reduces to a line or diagonal projection. +- `research/three-data-aux-direct` checks one direct nine-call word and the + pigeonhole for eight coordinate projectors on four roles. It does not + treat a general frame on a line, and it leaves the 120 four-register + projectors unclassified. Lemma A' is the projection those coordinate + assignments instantiate. +- `research/bit-one-relation-any-registers` removes the register-count + restriction when `dim S >= k - 1`. Two or more relations remain open + there. This note does not re-prove the one-relation regime. +- The GL3 census behind PR #1974, recorded in + `research/bit-gl3-mixed-targets-length10`, uses two registers, the + finite alphabet of coordinate CNOTs in `F_2[GL_3(F_2)]`, and free + `GL_2(F_2)` mixing. PR #2027's mixed-root tariff is a UT4 quotient. + Neither alphabet is the rational matrix group used here, so neither + census is a special case of Lemma A' or a counterexample to it. + +## 9. Scope + +This is a formal group-algebra bound. It gives no native schedule, no +hosting or precision bill, and no change to the selected frontier. It does +not cover frame span `m + 2` or more, free address maps between calls, or +the `|K| = 2` block with helper registers. diff --git a/research/span-lemma-idle-helpers/README.md b/research/span-lemma-idle-helpers/README.md new file mode 100644 index 0000000000..6b9a2e17bf --- /dev/null +++ b/research/span-lemma-idle-helpers/README.md @@ -0,0 +1,113 @@ +# Idle helpers do not lower the span-(m+1) line bound + +**Scoped negative result; no new kappa.** In the abelian scalar-idempotent +register model, `t` invertible `m x m` rational targets plus any number of +clean or dirty monomial helper registers still need at least `m t` paid +calls when the paid-frame span has dimension at most `m + 1`, except in the +normalized `|K| = 2` block. The direct coordinate word attains `m t` and +leaves every clean helper at the group identity. + +This answers open question 3 of +[`research/span-lemma-every-dimension`](../span-lemma-every-dimension/README.md): +Lemma A's line projection survives identity helper targets. Extra registers +do not escape that part of the three-register obstruction. + +The selected frontier is unchanged. On this base, +`certificates/selected-result.json` records +`781451/250000000`. + +## Result + +Let `S` be the rational span of the paid frames and let `K` be the support +intersection of the normalized extra frame `u v^T`. + +| Hypothesis | Bound | Helpers | +| --- | --- | --- | +| `dim S <= m` | `k >= m t` | clean or arbitrary monomials | +| `dim S = m + 1` and `|K| >= 3` | `k >= m t` | clean or arbitrary monomials | +| `dim S = m + 1` and `|K| <= 1` | `k >= m t` | clean or arbitrary monomials | +| `dim S = m + 1` and `|K| = 2` | not extended | flag bound still assumes invertible blocks | +| direct word | `k = m t` | any number of untouched clean helpers | + +[PROOF.md](PROOF.md) gives Lemma R (rank of a rank-one product) and Lemma A' +(line projection with helper outputs), then invokes the address normalization +from the predecessor. That normalization does not depend on the register +count. + +## What was compared before the proof + +The card's first experiment names the #1974 GL3 census and the #2027 +mixed-root tariff. + +- `#1974`, as recorded in `research/bit-gl3-mixed-targets-length10`, is a + two-register census in `F_2[GL_3(F_2)]` with coordinate-CNOT labels and + free `GL_2(F_2)` mixing. It is not the rational matrix group used here. +- `#2027` is a UT4 mixed-root tariff. It does not convert these rational + frames. +- `research/bit-one-relation-any-registers` already allows every register + count when the frames have at most one rational relation. This note does + not reprove that regime. The small-span window is the complementary case. +- `research/three-data-aux-direct` checks eight coordinate projectors on + four roles. Lemma A' is the projection those assignments instantiate; it + is not a classification of the 120 four-register projectors. + +## Reproduce + +From the repository root, CPython 3.12, standard library only: + +```sh +python3 -I -W error -B research/span-lemma-idle-helpers/verify.py +python3 -I -O -W error -B research/span-lemma-idle-helpers/verify.py +python3 scripts/research_package.py --package research/span-lemma-idle-helpers +``` + +Both verifier commands print `PASS_SPAN_LEMMA_IDLE_HELPERS`. The package +command prints `PASS_REGISTERED_RESEARCH_PACKAGE`. A passing run reports +28 and 120 idempotents, 14400 pair products, a diagonal one-line grid, +direct words for 0, 1 and 2 clean helpers, the `(3,3,2,0)` rank-2 failure, +a three-coordinate block call that is not the direct word, and zero +eight-call covers of three lines. + +The pair check evaluates every `3 x 3` minor of `(I + a N)(I + b M) - I` +at `a, b in {1, 2, 3, 5}`. Each minor has degree at most 3 in each scalar, +so those four values certify that the minor polynomial is identically zero. +The grid is a control for Lemma R. The induction in PROOF.md is the proof. + +## Limitations + +- `|K| = 2` with helper registers is open. The predecessor's off-line + example shows that frames need not lie on the diagonal-plus-`B` lines. +- Span `m + 2` and two or more frame relations are open. One idle register + does not remove the two-relation hypothesis already stated in + `research/bit-one-relation-any-registers`. +- No native schedule, hosting bill, precision bill, or selected-frontier + change is claimed. Unknown physical costs are not zero; they are outside + this formal identity. + +## Open next questions + +1. Does the `|K| = 2` flag bound still give `k >= m t` for clean identity + helpers? The cited `2W` count assumes every diagonal block is invertible, + and a clean helper has zero blocks. First step: recompute the + dimension-two flag inequalities at `m = 3` with `t` invertible targets + and `r` zero targets. Blocker: Lemma C fails at `|K| = 2`. +2. Can one idle register together with two independent frame relations + realize three invertible targets in fewer than `m t` calls? First step: + fix `m = 3`, `t = 3`, `r = 1` and one explicit span-5 frame list, and + decide whether any eight-call word exists. Blocker: the two-relation + Laurent kernel is not principal. + +## Credit + +The model is eumemic's PR #288, section 1.2. The low-span lemma, the `m = 3` +span-four argument and the block flag bound are Ali Romman's PR #468 +(`research/bit-three-register-lower-bound`). The all-dimension span lemma +and its open question 3 are Nick Petalas's +`research/span-lemma-every-dimension`. The arbitrary-register one-relation +theorem is `research/bit-one-relation-any-registers`. The coordinate +auxiliary check is `research/three-data-aux-direct`. The GL3 census +comparison uses Hanson Sun's seed and the length-10 closure in +`research/bit-gl3-mixed-targets-length10`. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No independent human or formal-kernel review is claimed. diff --git a/research/span-lemma-idle-helpers/SOURCES.json b/research/span-lemma-idle-helpers/SOURCES.json new file mode 100644 index 0000000000..b6ac309f76 --- /dev/null +++ b/research/span-lemma-idle-helpers/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "626e936ce4d61f2584316914fc71baf96940c512", + "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/bit-one-relation-any-registers/README.md", + "usage": "input", + "git_blob": "7453a3f10c9cbaad746f108dc65dcfc514d0fdb5", + "sha256": "1f2899320e646a4158531c3f8260ba32b4761ae883fdb5bce4d3e3b0a4d8cb8c" + }, + { + "path": "research/span-lemma-every-dimension/PROOF.md", + "usage": "input", + "git_blob": "5f160fa562dbec44d7f5c388ffc9d0a8972223d3", + "sha256": "37aa8abd29629f8945710a0f675f3ad0a6241436d4e584b2e4741b36aead9f12" + } + ] +} diff --git a/research/span-lemma-idle-helpers/TASK.json b/research/span-lemma-idle-helpers/TASK.json new file mode 100644 index 0000000000..4201c8cff6 --- /dev/null +++ b/research/span-lemma-idle-helpers/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "626e936ce4d61f2584316914fc71baf96940c512", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "In the abelian scalar-idempotent model, t invertible rational-matrix targets plus any number of clean or dirty monomial helper registers still need at least m*t paid calls when the frame span has dimension at most m+1 and the normalized extra frame satisfies |K|!=2. The direct word attains m*t. This answers open question 3 of research/span-lemma-every-dimension.", + "scope_change_reason": "The card allows a fixed larger register count. The three-register theorem and the all-dimension span lemma both exclude extra registers. This note keeps their alphabet and asks whether idle helpers lower the span-(m+1) line bound. They do not, except in the |K|=2 flag case, which is left open.", + "bottleneck_link": "A larger register file does not by itself improve the bit primitive inside the span-(m+1) projection regimes: the direct m*t word remains optimal there, with or without clean helpers. A saving still needs span at least m+2, two frame relations, or the unsettled |K|=2 block.", + "budget_minutes": 60, + "stop_rule": "Stop after the line-projection statement and the matching direct word. Do not search span m+2, classify the 120 four-register projectors, or price a native schedule.", + "outcome": "completed", + "evidence": "PROOF.md proves Lemma R, Lemma A' with helper outputs, and the three address cases dim<=m, |K|>=3 and |K|<=1. verify.py checks all 14400 four-register idempotent pairs, the diagonal one-line grid, the direct word for r=0,1,2, the (3,3,2,0) failure, the block-projector control, and the eight-call pigeonhole.", + "author": "unpaidmoon", + "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent human or proof-kernel review is claimed.", + "open_questions": [ + { + "question": "Does the |K|=2 block flag bound still give k>=m*t when some registers are clean identity helpers?", + "why_it_matters": "It is the only span-(m+1) case this note does not extend to idle registers.", + "first_step": "Rewrite PR #468's dimension-two flag count with t invertible blocks and r zero blocks, starting at m=3.", + "blocked_by": "Lemma C fails at |K|=2, and the cited 2W bound assumes every target block is invertible." + }, + { + "question": "Can one idle register and two independent frame relations realize three invertible targets in fewer than m*t calls?", + "why_it_matters": "bit-one-relation-any-registers already rules out fewer than two relations for every register count. This is the first remaining escape window.", + "first_step": "Fix m=3, t=3, r=1 and one explicit span-5 frame list, and test whether an eight-call word exists before a general classification.", + "blocked_by": "The two-relation Laurent kernel is not principal, so the one-relation derivative no longer forces a single off-diagonal pattern." + } + ], + "question_source": { + "pr": null, + "author": "Nick Petalas", + "question": "Open question 3 of research/span-lemma-every-dimension: do clean or dirty extra registers change the span-(m+1) bound?" + } +} diff --git a/research/span-lemma-idle-helpers/VERIFY.json b/research/span-lemma-idle-helpers/VERIFY.json new file mode 100644 index 0000000000..b8627edd68 --- /dev/null +++ b/research/span-lemma-idle-helpers/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-one-relation-any-registers/README.md", + "research/span-lemma-every-dimension/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pair rank identity, diagonal one-line grid, direct word with clean helpers, eight-call failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks with assertions disabled; the verifier uses need() rather than assert." + } + ] +} diff --git a/research/span-lemma-idle-helpers/verify.py b/research/span-lemma-idle-helpers/verify.py new file mode 100644 index 0000000000..535ef85c2d --- /dev/null +++ b/research/span-lemma-idle-helpers/verify.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Exact checks for the idle-helper span line bound. + +PROOF.md is the argument. These controls check the two-update rank identity +by evaluation, the one-line property of a diagonal span, the direct word +with clean helpers, and the eight-call line pigeonhole. +""" + +from itertools import combinations, product + + +def need(condition, message): + if not condition: + raise SystemExit(message) + + +def idempotents(width): + found = [] + for mask_x in range(1 << width): + for mask_y in range(1 << width): + if (mask_x & mask_y).bit_count() % 2 != 1: + continue + found.append( + tuple( + tuple(((mask_x >> row) & 1) & ((mask_y >> col) & 1) for col in range(width)) + for row in range(width) + ) + ) + return found + + +def mat_mul(left, right): + width = len(left) + return tuple( + tuple(sum(left[row][mid] * right[mid][col] for mid in range(width)) for col in range(width)) + for row in range(width) + ) + + +def scaled_update(projector, scalar): + width = len(projector) + return tuple( + tuple((1 if row == col else 0) + scalar * projector[row][col] for col in range(width)) + for row in range(width) + ) + + +def det3(matrix): + (a00, a01, a02), (a10, a11, a12), (a20, a21, a22) = matrix + return ( + a00 * (a11 * a22 - a12 * a21) + - a01 * (a10 * a22 - a12 * a20) + + a02 * (a10 * a21 - a11 * a20) + ) + + +def check_pair_rank(projectors): + width = len(projectors[0]) + samples = (1, 2, 3, 5) + checked = 0 + for left, right in product(projectors, repeat=2): + for scalar_a, scalar_b in product(samples, repeat=2): + product_matrix = mat_mul(scaled_update(left, scalar_a), scaled_update(right, scalar_b)) + difference = tuple( + tuple(product_matrix[row][col] - (1 if row == col else 0) for col in range(width)) + for row in range(width) + ) + row_sets = list(combinations(range(width), 3)) + for row_set in row_sets: + for col_set in row_sets: + minor = tuple( + tuple(difference[row][col] for col in col_set) for row in row_set + ) + need(det3(minor) == 0, "two rank-one updates produced rank above 2") + checked += 1 + return checked + + +def check_diagonal_lines(): + # Every nonzero rank-one matrix u v^T that is diagonal uses exactly one line. + diagonal_rank_one = 0 + multi_line = 0 + for left in product(range(-2, 3), repeat=3): + for right in product(range(-2, 3), repeat=3): + matrix = tuple(tuple(left[row] * right[col] for col in range(3)) for row in range(3)) + if any(matrix[row][col] for row in range(3) for col in range(3) if row != col): + continue + if not any(matrix[row][row] for row in range(3)): + continue + diagonal_rank_one += 1 + if sum(matrix[row][row] != 0 for row in range(3)) != 1: + multi_line += 1 + need(diagonal_rank_one > 0 and multi_line == 0, "diagonal rank-one matrix meets two lines") + return diagonal_rank_one + + +def add_poly(left, right): + out = set(left) + for exponent in right: + if exponent in out: + out.remove(exponent) + else: + out.add(exponent) + return frozenset(out) + + +def shift(poly, exponent): + return frozenset(tuple(coord + extra for coord, extra in zip(term, exponent)) for term in poly) + + +def apply_call(state, projector, frame): + width = int(len(state) ** 0.5) + need(width * width == len(state), "state is not square") + rows = [list(state[width * row : width * row + width]) for row in range(width)] + image = None + support = [] + for row in range(width): + if any(projector[row]): + if image is None: + image = projector[row] + need(projector[row] == image, "idempotent rows disagree") + support.append(row) + need(image is not None, "empty projector") + acc = [frozenset() for _ in range(width)] + for col, bit in enumerate(image): + if bit: + acc = [add_poly(acc[entry], rows[col][entry]) for entry in range(width)] + delta = [add_poly(shift(part, frame), part) for part in acc] + for row in support: + rows[row] = [add_poly(rows[row][entry], delta[entry]) for entry in range(width)] + return tuple(entry for row in rows for entry in row) + + +def identity_state(width, degree): + zero = frozenset() + one = frozenset([tuple(0 for _ in range(degree))]) + return tuple(one if row == col else zero for row in range(width) for col in range(width)) + + +def coordinate_projector(width, index): + return tuple( + tuple(1 if row == index and col == index else 0 for col in range(width)) + for row in range(width) + ) + + +def direct_word(data, helpers, address): + width = data + helpers + state = identity_state(width, address) + for register in range(data): + for axis in range(address): + frame = tuple(1 if coord == axis else 0 for coord in range(address)) + state = apply_call(state, coordinate_projector(width, register), frame) + return state + + +def expect_direct(state, data, helpers, address): + width = data + helpers + zero = frozenset() + full = frozenset([tuple(1 for _ in range(address))]) + one = frozenset([tuple(0 for _ in range(address))]) + for row in range(width): + for col in range(width): + entry = state[width * row + col] + if row != col: + need(entry == zero, "direct word created an off-diagonal entry") + elif row < data: + need(entry == full, "direct word missed a data target") + else: + need(entry == one, "clean helper was not restored") + + +def short_register_fails(address=3): + width = 4 + state = identity_state(width, address) + plan = (3, 3, 2, 0) + for register, count in enumerate(plan): + for axis in range(count): + frame = tuple(1 if coord == (axis % address) else 0 for coord in range(address)) + state = apply_call(state, coordinate_projector(width, register), frame) + exponent = next(iter(state[2 * width + 2])) + need(sum(exponent) == 2, "two calls did not leave rank 2") + need(exponent != tuple(1 for _ in range(address)), "two calls produced I") + return exponent + + +def block_projector_is_not_three_multiplies(): + width = 4 + degree = 3 + mask = 0b0111 + projector = tuple( + tuple(((mask >> row) & 1) & ((mask >> col) & 1) for col in range(width)) + for row in range(width) + ) + state = apply_call(identity_state(width, degree), projector, (1, 0, 0)) + need(state != direct_word(3, 1, degree), "one block call reproduced the direct word") + return len(state[0]) + + +def pigeonhole(): + solutions = [ + counts + for counts in product(range(9), repeat=3) + if sum(counts) == 8 and all(count >= 3 for count in counts) + ] + need(solutions == [], "eight calls cover three lines") + attained = [ + counts + for counts in product(range(10), repeat=3) + if sum(counts) == 9 and all(count >= 3 for count in counts) + ] + need(attained == [(3, 3, 3)], "the direct line split is not the unique nine-call cover") + return len(solutions) + + +def main(): + three = idempotents(3) + four = idempotents(4) + need(len(three) == 28, "three-register idempotent count") + need(len(four) == 120, "four-register idempotent count") + pairs = check_pair_rank(four) + diagonal = check_diagonal_lines() + for helpers in (0, 1, 2): + expect_direct(direct_word(3, helpers, 3), 3, helpers, 3) + short = short_register_fails() + block_terms = block_projector_is_not_three_multiplies() + empty = pigeonhole() + print( + "PASS_SPAN_LEMMA_IDLE_HELPERS" + f" idempotents_w3={len(three)} idempotents_w4={len(four)}" + f" pair_products={pairs} diagonal_grid={diagonal}" + f" short_exponent={short} block_entry_terms={block_terms}" + f" eight_call_line_covers={empty} bound=m*t sharp=true no_new_kappa" + ) + + +if __name__ == "__main__": + main()