diff --git a/research/span-lemma-every-dimension/PROOF.md b/research/span-lemma-every-dimension/PROOF.md new file mode 100644 index 0000000000..5f160fa562 --- /dev/null +++ b/research/span-lemma-every-dimension/PROOF.md @@ -0,0 +1,186 @@ +# The span-(m+1) lemma in every address dimension + +Produced by Nick Petalas. Apache-2.0. This is a written scoped proof with +an exact finite check of its combinatorial step. It is not independent human +review or proof-kernel verification. + +## 1. Model + +Fix an address dimension `m >= 1` and a register count `W >= 1`. Work in +the group algebra `R = F_2[M_m(Q)]` of the additive group of rational +`m x m` matrices, with formal symbols `[A][B] = [A+B]`. A paid call is + + D_N([A]) = I + ([A] - 1) N, rank_Q A = 1, N = x y^T, y^T x = 1, + +with `x, y` in `F_2^W`. A word of `k` paid calls is required to satisfy + + prod_{j=1}^{k} D_{N_j}([A_j]) = diag([C_1], ..., [C_W]), (1) + +with every `C_w` in `GL_m(Q)`. Equality is of every formal coefficient. +This is the scalar-idempotent abelian register model of eumemic's PR #288, +section 1.2, as stated by Ali Romman's PR #468 for `m = 3` +(`research/bit-three-register-lower-bound`, section 1). The normalization of +final scalar maps is the one recorded there. Only the dimension `m` changes. +Extra registers, clean or dirty helpers and free address maps between paid +calls are outside this note. + +Let `S` be the rational span of the paid frames `A_1, ..., A_k`. Every +target lies in `S`: diagonal entry `w` of the expanded product is an +`F_2`-combination of symbols of subset sums of frames, so `C_w` is such a +sum. This is PR #468, section 3. + +## 2. Statement + +**Theorem.** If `dim S <= m + 1`, then `k >= mW`. Write the normalized +extra frame of section 3 as `u v^T` and set `K = supp(u) ∩ supp(v)`. + +1. If `dim S <= m`, or `dim S = m + 1` and `|K| != 2`, the bound holds + for arbitrary invertible targets. +2. If `dim S = m + 1` and `|K| = 2`, the bound holds for invertible + lower-triangular targets, by PR #468's block flag argument. + +In particular, for invertible lower-triangular targets, a paid-frame span of +dimension at most `m + 1` needs at least `mW` calls in every dimension `m`. +PR #468 proves this for `m = 3` (its span-four lemma). + +The direct word attains `mW`: write each `C_w` as a sum of `m` rank-one +frames and use `m` calls with `N = E_ww`. For diagonal targets this word +also has frame span `m`. + +## 3. Normalization + +Choose a basis `B_i = u_i v_i^T`, `i = 1..s`, of `S` from the paid frames. +By Cauchy–Binet, + + det(sum_i c_i B_i) = sum_{|T| = m} (prod_{i in T} c_i) det U_T det V_T, + +where `U_T, V_T` are the `m x m` matrices with columns `u_i, v_i`, `i in T`. +Because `S` contains an invertible target, this polynomial is nonzero, so +some `T` has `det U_T det V_T != 0`. If `s < m`, no such `T` exists, so +`s >= m`. Put `P = U_T^{-1}` and `Q = V_T^{-T}`. Then `P B_i Q = E_ii` for +`i in T`, after relabeling. + +The map `A -> P A Q` is an automorphism of the additive group `M_m(Q)` that +preserves rank. It induces a ring automorphism of `R`. Applying it entrywise +to (1) gives an identity of the same form, with frames `P A_j Q` and +invertible targets `P C_w Q`. Lower-triangularity is not preserved. Section 5 +does not need it, and section 6 restores it as PR #468 does. + +If `s = m`, PR #468's low-span lemma, stated there for general `m`, gives +`k >= mW` for arbitrary invertible targets. From now on `s = m + 1`. Then +`S = {D + tB}`, with `D` diagonal and `B = u v^T` the remaining paid basis +frame. + +## 4. Line projection + +**Lemma A.** Let `b_0, ..., b_m` be a basis of `S` consisting of rank-one +matrices. Suppose every paid frame is a multiple of one `b_i`. Then +`k >= sum_w nnz(C_w) >= mW`, where `nnz` counts nonzero coordinates in +this basis. + +*Proof.* Let `phi_i` be the `i`th coordinate functional on `S`. All +exponents in (1) lie in `S`, so `[A] -> [phi_i(A)]` is a ring homomorphism +from `F_2[S]` to `F_2[Q]`. Apply it to (1). A call whose frame lies on +another line becomes `I + ([0] - 1)N = I`. Let `k_i` be the number of calls +on line `i`. Their product has the form `I + X T Y^T` with `k_i` columns, +over the fraction field of a Laurent polynomial domain (PR #468, section 2). +Its difference from `I` therefore has rank at most `k_i`. The right side +minus `I` is `diag([phi_i(C_w)] - 1)`, of rank `#{w : phi_i(C_w) != 0}`. +A nonzero frame lies on at most one line, so `k >= sum_i k_i`. Each `C_w` +is a combination of `nnz(C_w)` rank-one matrices, so +`m = rank C_w <= nnz(C_w)`. ∎ + +## 5. The new cases `|K| >= 3` and `|K| <= 1` + +**Lemma B (minor identity).** For distinct `i, k, l`, the minor of +`D + tB` on rows `{i, k}` and columns `{i, l}` equals `D_ii t u_k v_l`. + +*Proof.* The entries are `D_ii + t u_i v_i`, `t u_i v_l`, `t u_k v_i` and +`t u_k v_l`, because `k != l` and `k, l != i`. Expanding gives the +identity. ∎ + +**Lemma C.** If `|K| >= 3`, every rank-one matrix in `S` lies on one of +the `m + 1` lines `Q E_00, ..., Q E_{m-1,m-1}, Q B`. + +*Proof.* Let `M = D + tB` have rank one. If `t = 0`, `M` is a diagonal +rank-one matrix and lies on one `E_ii` line. Suppose `t != 0` and fix any +`i`. Because `|K \ {i}| >= 2`, there are distinct `k, l` in `K \ {i}`. +Then `u_k v_l != 0`, and Lemma B forces `D_ii = 0`. So `D = 0` and +`M = tB`. ∎ + +PR #468 uses this step at `m = 3` under the stronger hypothesis that +every coordinate of `u` and `v` is nonzero. In dimension `m >= 4`, the +condition `|K| >= 3` is weaker than full support. This covers frames with +zero coordinates, where PR #468's three-dimensional component bound no +longer applies. + +**Case `|K| >= 3`.** Lemmas C and A give `k >= mW` for arbitrary +invertible targets. + +**Lemma D.** Let `G` be the directed graph on `{0, ..., m-1}` with an arc +`i -> l`, `i != l`, when `u_i v_l != 0`. A vertex on a directed cycle has +an outgoing arc, so it is in `supp(u)`. It also has an incoming arc, so it +is in `supp(v)`. Every cycle therefore lies in `K`, and any two vertices of +`K` form a 2-cycle. Hence the nontrivial strongly connected components of +`G` are exactly `{K}` when `|K| >= 2`. There are none when `|K| <= 1`. + +**Case `|K| <= 1`.** `G` is acyclic. A simultaneous row and column +permutation along a topological order makes every element of `S` upper +triangular. The transformed targets are upper triangular and invertible, +so each has `m` nonzero diagonal entries. A rank-one triangular matrix has +characteristic polynomial `x^{m-1}(x - tr M)`, and its diagonal entries are +its eigenvalues, so at most one is nonzero. Project with the diagonal entry +functional `psi_i`, as in Lemma A. At least `W` calls have +`psi_i(A_j) != 0`, and these call sets are disjoint across `i`, so +`k >= mW` for arbitrary invertible targets. This is the common-flag +principle of huxint's PR #203 and PR #468, applied after normalization. + +## 6. The case `|K| = 2` + +By Lemma D, `S` is block upper triangular after a permutation. It has one +`2 x 2` diagonal block on `K` and `m - 2` blocks of size one. PR #468, +section 3, proves `k >= 3W` from exactly this structure at `m = 3`. A +rank-one element has at most one nonzero diagonal block. Common flags +restrict to the diagonal blocks. The dimension-two flag bound gives `2W` +per two-block and `W` per one-block. The argument uses only block sizes at +most two and their sum, which is `m` here. This note cites that argument +and does not recheck it. It uses PR #468's lower-triangular target +hypothesis. + +Without that hypothesis, the case can behave differently. The exact +control `u = v = (1, 1, 0)`, `D = diag(2, 2, 0)`, `t = -1` gives a rank-one +element `D + tB` off all the lines. So Lemma C fails at `|K| = 2`. + +## 7. Finite check + +`verify.py` checks the combinatorial step for every pair of nonempty +supports with `1 <= m <= 7`. If `|K| >= 3`, every index `i` has the +distinct witnesses `k, l` used in Lemma C. If `|K| = 2` or `|K| >= 3`, +the only nontrivial component is `K`. If `|K| <= 1`, the arc graph is +acyclic. It verifies Lemma B as a polynomial identity. It also runs an +exact integer grid of rank-one tests: + +| m | coordinate set for u, v | D entries | t | pairs with `|K| >= 3` | matrices | +| --- | --- | --- | --- | --- | --- | +| 3 | {-1,0,1,2} | {-1,0,1,2} | {1,-1,2} | 729 | 137,781 | +| 4 | {0,1,2} | {-1,0,1} | {1,-1} | 1,536 | 245,760 | +| 5 | {0,1} | {-1,0,1} | {1,-1} | 106 | 51,304 | + +No rank-one `D + tB` with `t != 0` and `D != 0` occurs. The grid is a +control, not the proof. Controls confirm that the rank test separates rank +one from rank two and that a `|K| = 2` pair has off-line rank-one elements. + +## 8. Scope + +This is a scoped proof in a formal group-algebra model. It gives no +construction, no native conversion, no supplier change and no new κ. It +does not cover frame span `m + 2` or more. It also leaves out non-triangular +targets when `|K| = 2`, extra clean or dirty registers, and free address +maps between paid calls. + +## References + +- eumemic, PR #288, section 1.2: scalar-idempotent abelian register model. +- Ali Romman, PR #468, `research/bit-three-register-lower-bound`: low-span + lemma, span-four lemma at `m = 3`, block flag argument, projection tools. +- huxint, PR #203: common triangular-flag obstruction. diff --git a/research/span-lemma-every-dimension/README.md b/research/span-lemma-every-dimension/README.md new file mode 100644 index 0000000000..a9b31c39d2 --- /dev/null +++ b/research/span-lemma-every-dimension/README.md @@ -0,0 +1,85 @@ +# Frame span m+1 cannot save a call in any address dimension + +In the abelian scalar-idempotent register model with `m x m` rational +frames and `W` registers, a paid-frame span of dimension at most `m + 1` +forces at least **`mW` calls** for invertible lower-triangular targets. +This holds for every `m`. PR #468 proves it only at `m = 3` (its span-four +lemma, nine calls for three registers). The direct word attains `mW`. + +After normalizing the span to `diag + t·uv^T`, set +`K = supp(u) ∩ supp(v)`. The lower-triangular hypothesis is needed only +when `|K| = 2`: + +| Case | Argument | Targets | +| --- | --- | --- | +| span `<= m` | PR #468 low-span lemma | any invertible | +| `|K| >= 3` | new: rank-one frames lie on `m + 1` lines | any invertible | +| `|K| <= 1` | new reduction: span is triangular after a permutation | any invertible | +| `|K| = 2` | PR #468 block flag argument, cited | lower triangular | + +The key step is a 2×2 minor identity. For distinct `i, k, l`, the minor of +`D + tB` on rows `{i,k}` and columns `{i,l}` is `D_ii t u_k v_l`. With +`|K| >= 3`, each `i` has such `k, l` in `K`, so every rank-one element of +the span lies on a basis line. PR #468 needs full support of `u, v` for +this step. In dimension four or more, that misses frames with zero +coordinates whose diagonal blocks have size above two. + +**Claim type:** a scoped written proof with an exact finite check of its +combinatorial step. No construction, native conversion, supplier change +or new κ. The selected frontier is unchanged. + +[PROOF.md](PROOF.md) has the model, theorem, proof and scope. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library only: + +```sh +python3.12 -I -W error -B research/span-lemma-every-dimension/verify.py +python3.12 -I -O -W error -B research/span-lemma-every-dimension/verify.py +``` + +Both print `PASS_SPAN_LEMMA_EVERY_DIMENSION` in under a second. The +verifier checks the support classification for all nonempty support pairs +with `m <= 7`. It checks the minor identity as a polynomial identity. It +runs an exact rank-one grid at `m = 3, 4, 5` (434,845 matrices, zero +off-line rank-one elements). It also runs two controls, including an +explicit off-line rank-one element at `|K| = 2`. + +## Limitations + +- The `|K| = 2` case cites PR #468's block flag argument and its + lower-triangular target hypothesis. That argument is not rechecked here. +- Span `m + 2` or more, extra clean or dirty registers, free address maps + between paid calls and nonabelian models are not covered. +- The finite grid is a control. The theorem rests on the written proof. + +## Open next questions + +1. Does `|K| = 2` still force `mW` calls for non-triangular invertible + targets? Start at `m = 2` with full-support `u, v`, where off-line + rank-one frames exist. +2. Does span `m + 2` force `mW` calls for `m >= 4`? Normalize to + `diag + span{B, B'}` and classify the joint support graph of the two + extra frames. +3. Do clean or dirty extra registers change the span-`(m+1)` bound? Check + whether the line projection of Lemma A survives identity helper targets. + +## Sources and credit + +The proof and verifier were produced by Nick Petalas. Apache-2.0. +The model is eumemic's PR #288, section 1.2. The low-span lemma, +span-four lemma at `m = 3`, projection tools and block flag argument are +Ali Romman's [PR #468](https://github.com/CrocSwap/integer-mult-bounds/pull/468) +(`research/bit-three-register-lower-bound`). The common triangular-flag +obstruction is huxint's [PR #203](https://github.com/CrocSwap/integer-mult-bounds/pull/203). +The new parts are the `|K| >= 3` line lemma in general dimension, the +`|K| <= 1` triangular reduction after normalization, and their assembly +into the all-dimension statement. + +[SOURCES.json](SOURCES.json) pins the input bytes at canonical main +`19fdb086ea96af9a9f87936a2b888e10af4ed810`. The +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226223) +records the scope. Main-tree, merged-PR and open-PR searches found no +general-dimension span-`(m+1)` lemma. This is search coverage, not a +guarantee about unpublished work. diff --git a/research/span-lemma-every-dimension/SOURCES.json b/research/span-lemma-every-dimension/SOURCES.json new file mode 100644 index 0000000000..bf5974c800 --- /dev/null +++ b/research/span-lemma-every-dimension/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ] +} diff --git a/research/span-lemma-every-dimension/TASK.json b/research/span-lemma-every-dimension/TASK.json new file mode 100644 index 0000000000..f1df98e049 --- /dev/null +++ b/research/span-lemma-every-dimension/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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": "changed", + "actual_scope": "Prove that a paid-frame span of dimension at most m+1 forces at least mW calls for W invertible lower-triangular targets in the abelian scalar-idempotent register model, in every address dimension m; the triangular hypothesis is needed only when the normalized extra frame uv^T has |supp u ∩ supp v| = 2.", + "scope_change_reason": "The card asks for a changed register model. This changes the address dimension, a hypothesis fixed at m=3 in PR #468's span-four lemma, whose all-nonzero and size-two-component steps do not extend directly. It is a lower-bound lemma, not a construction or a native conversion.", + "bottleneck_link": "Any m-dimensional bit-model escape must use frame span at least m+2; span m+1 cannot save a call over the direct mW word.", + "budget_minutes": 60, + "stop_rule": "Ship the first complete general-m proof of the span-(m+1) case. Do not extend to span m+2 or extra registers.", + "outcome": "completed", + "evidence": "Written proof in PROOF.md; verify.py checks the support classification for all nonempty support pairs with m<=7, the 2x2 minor identity as a polynomial identity, an exact rank-one grid at m=3,4,5 with zero off-line rank-one elements, and two controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the |K|=2 case of span m+1 still force mW calls for arbitrary invertible, non-triangular targets?", + "why_it_matters": "It would remove the last use of the lower-triangular hypothesis at span m+1.", + "first_step": "Treat m=2 with S = diag + t uv^T and u, v of full support, where off-line rank-one frames exist.", + "blocked_by": "The block flag bound uses a common flag of the targets; Lemma C fails at |K|=2." + }, + { + "question": "Does span m+2 force mW calls for m>=4?", + "why_it_matters": "At m=3 span five is still open outside known classes; a general-m reduction would locate the first dimension where a saving could exist.", + "first_step": "Normalize S = diag + span{B, B'} and classify the joint support graph of the two extra frames.", + "blocked_by": "Two extra frames can create rank-one combinations off every line even with large supports." + }, + { + "question": "Do clean or dirty extra registers change the span-(m+1) bound in dimension m?", + "why_it_matters": "Existing helper-register results are at m=3.", + "first_step": "Check that Lemma A's line projection stays valid when helper diagonal targets are the identity.", + "blocked_by": "Not attempted here." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226223", + "question_source": { + "pr": null, + "author": "original", + "question": "Original extension of PR #468's span-four lemma to every address dimension" + }, + "environment": { + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only", + "receipt": "Generated on stdout from a fresh complete computation; no stored receipt accepted." + } +} diff --git a/research/span-lemma-every-dimension/VERIFY.json b/research/span-lemma-every-dimension/VERIFY.json new file mode 100644 index 0000000000..ccb812adca --- /dev/null +++ b/research/span-lemma-every-dimension/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Support classification m<=7, minor identity, exact rank-one grid m=3,4,5 and controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same checks with assertions disabled." + } + ] +} diff --git a/research/span-lemma-every-dimension/verify.py b/research/span-lemma-every-dimension/verify.py new file mode 100644 index 0000000000..2f9f4e5fa1 --- /dev/null +++ b/research/span-lemma-every-dimension/verify.py @@ -0,0 +1,181 @@ +#!/usr/bin/env python3 +"""Exact checks for the span-(m+1) lemma in every address dimension. + +Produced by Nick Petalas. Apache-2.0. +Standard library only. No predecessor executable, network, Git or output file. +The written proof is PROOF.md; these checks cover its finite combinatorial +step, its 2x2 minor identity and an exact rank-one grid with controls. +""" + +import itertools +import json + +MAX_SUPPORT_DIMENSION = 7 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def edges(m, supp_u, supp_v): + return {(i, l) for i in supp_u for l in supp_v if i != l} + + +def strongly_connected_components(m, arcs): + reach = [[i == l for l in range(m)] for i in range(m)] + for i, l in arcs: + reach[i][l] = True + for mid in range(m): + for i in range(m): + if reach[i][mid]: + for l in range(m): + if reach[mid][l]: + reach[i][l] = True + return {frozenset(l for l in range(m) if reach[i][l] and reach[l][i]) + for i in range(m)} + + +def has_robust_minor(i, supp_u, supp_v): + return any(k != l and k != i and l != i + for k in supp_u for l in supp_v) + + +def check_supports(): + """Lemma 2/4 combinatorics for every pair of nonempty supports.""" + tally = {} + for m in range(1, MAX_SUPPORT_DIMENSION + 1): + subsets = [frozenset(c) for r in range(1, m + 1) + for c in itertools.combinations(range(m), r)] + counts = {"K>=3": 0, "K=2": 0, "K<=1": 0} + for supp_u in subsets: + for supp_v in subsets: + core = supp_u & supp_v + arcs = edges(m, supp_u, supp_v) + components = strongly_connected_components(m, arcs) + nontrivial = [c for c in components if len(c) > 1] + if len(core) >= 3: + counts["K>=3"] += 1 + need(all(has_robust_minor(i, supp_u, supp_v) + for i in range(m)), + "robust minor missing for |K|>=3") + need(nontrivial == [core], "|K|>=3 component mismatch") + elif len(core) == 2: + counts["K=2"] += 1 + need(nontrivial == [core], "|K|=2 component mismatch") + else: + counts["K<=1"] += 1 + need(not nontrivial, "|K|<=1 digraph has a cycle") + need(sum(counts.values()) == len(subsets) ** 2, "support count") + tally[str(m)] = counts + return tally + + +def poly_mul(left, right): + out = {} + for a, x in left.items(): + for b, y in right.items(): + key = tuple(p + q for p, q in zip(a, b)) + out[key] = out.get(key, 0) + x * y + return {k: v for k, v in out.items() if v} + + +def poly_add(left, right, sign=1): + out = dict(left) + for k, v in right.items(): + out[k] = out.get(k, 0) + sign * v + return {k: v for k, v in out.items() if v} + + +def monomial(**powers): + order = ("d", "t", "ui", "uk", "vi", "vl") + return {tuple(powers.get(name, 0) for name in order): 1} + + +def check_minor_identity(): + """det [[d+t ui vi, t ui vl], [t uk vi, t uk vl]] == d t uk vl.""" + a = poly_add(monomial(d=1), monomial(t=1, ui=1, vi=1)) + b = monomial(t=1, ui=1, vl=1) + c = monomial(t=1, uk=1, vi=1) + e = monomial(t=1, uk=1, vl=1) + det = poly_add(poly_mul(a, e), poly_mul(b, c), sign=-1) + need(det == monomial(d=1, t=1, uk=1, vl=1), "minor identity fails") + return "d*t*uk*vl" + + +def rank_at_most_one(matrix, m): + for r0, r1 in itertools.combinations(range(m), 2): + for c0, c1 in itertools.combinations(range(m), 2): + if (matrix[r0][c0] * matrix[r1][c1] + != matrix[r0][c1] * matrix[r1][c0]): + return False + return True + + +def grid(m, entries, diagonal, scalars): + """Rank-one D + tB with t != 0 on an exact integer grid.""" + stats = {"pairs": 0, "matrices": 0, "violations": 0} + vectors = [v for v in itertools.product(entries, repeat=m) if any(v)] + for u in vectors: + for v in vectors: + core = {i for i in range(m) if u[i] and v[i]} + if len(core) < 3: + continue + stats["pairs"] += 1 + for t in scalars: + b = [[t * u[i] * v[l] for l in range(m)] for i in range(m)] + for d in itertools.product(diagonal, repeat=m): + if not any(d): + continue + stats["matrices"] += 1 + matrix = [row[:] for row in b] + for i in range(m): + matrix[i][i] += d[i] + if rank_at_most_one(matrix, m): + stats["violations"] += 1 + need(stats["violations"] == 0, f"off-line rank-one element at m={m}") + return stats + + +def control_two_core(): + """|K|=2 admits off-line rank-one elements: the hypothesis is needed.""" + u = (1, 1, 0) + v = (1, 1, 0) + # D = diag(2, 2, 0), t = -1 gives [[1,-1,0],[-1,1,0],[0,0,0]], rank one. + found = [] + for t in (1, -1, 2): + for d in itertools.product((-1, 0, 1, 2), repeat=3): + if not any(d): + continue + matrix = [[t * u[i] * v[l] + (d[i] if i == l else 0) + for l in range(3)] for i in range(3)] + if any(any(row) for row in matrix) and rank_at_most_one(matrix, 3): + found.append({"t": t, "D": list(d)}) + need(found, "control: expected an off-line rank-one element for |K|=2") + return {"u": list(u), "v": list(v), "first": found[0], + "count": len(found)} + + +def control_detector(): + """The rank test rejects a rank-two matrix and accepts a rank-one one.""" + need(rank_at_most_one([[1, 2, 3], [2, 4, 6], [0, 0, 0]], 3), "rank one") + need(not rank_at_most_one([[1, 0, 0], [0, 1, 0], [0, 0, 0]], 3), "rank two") + return True + + +def main(): + result = { + "supports": check_supports(), + "minor_identity": check_minor_identity(), + "grid_m3": grid(3, (-1, 0, 1, 2), (-1, 0, 1, 2), (1, -1, 2)), + "grid_m4": grid(4, (0, 1, 2), (-1, 0, 1), (1, -1)), + "grid_m5": grid(5, (0, 1), (-1, 0, 1), (1, -1)), + "control_two_core": control_two_core(), + "control_detector": control_detector(), + } + print(json.dumps(result, sort_keys=True, indent=1)) + print("PASS_SPAN_LEMMA_EVERY_DIMENSION") + + +if __name__ == "__main__": + main()