diff --git a/research/schur-intermediate-ranks/PROOF.md b/research/schur-intermediate-ranks/PROOF.md new file mode 100644 index 0000000000..234a86b25f --- /dev/null +++ b/research/schur-intermediate-ranks/PROOF.md @@ -0,0 +1,164 @@ +# Nonmaximal Schur-commutator ranks for prescribed pivots + +Nick Petalas. Apache-2.0. + +This answers, in part, Open next question 1 of Krzysztof Wojt's +[PR #5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128) +(`research/arbitrary-pivot-schur-minimum`). Its sector factorization, the maps +`L,R` of its equations (4), (7), (8) and its rank-`2d` minimum are cited, not +rechecked. Sections 1–4 are an all-field proof. Section 5 is a finite +certificate. + +## 0. Setting + +Let K be a field, d >= 1, A,B in GL_d(K), H in M_d(K). Put + +``` +T00 = I-A-B+H, T10 = A-H, T01 = B-H, T11 = H, nu_j = nullity T_j. +``` + +Consider commuting idempotents P,Q in M_n(K) with `P11=A`, `Q11=B`, +`(PQ)11=H`, Schur complements S, Z as in #5128, and ρ = rank(SZ-ZS). + +## 1. Reduction to two block subspaces + +By #5128 §3–4, such pairs are exactly the choices of sector spaces V_j and maps +`Y_j: U -> V_j`, `X_j: V_j -> U` with `X_j Y_j = T_j` (U = K^d); then +n = Σ dim V_j. By #5128 (5), (7), (8), + +``` +SZ-ZS ~ L R, L = Y G, R = G' X, +``` + +with `Y = diag(Y10,Y01,Y11)`, `X = diag(X10,X01,X11)` and fixed maps + +``` +G(x,y) = (A^-1 y, -B^-1(Hx+y), (I-B^-1 H)x + (A^-1-B^-1)y), +G'(a,b,c) = (A^-1 a - B^-1 b + (A^-1-B^-1)c, H B^-1 b + (H B^-1 - I)c). +``` + +The 00 sector does not enter L or R. Put `M = G G'` on U^3, +`I = im X = ⊕ I_j` and `N = ker Y = ⊕ N_j`. Then `I_j ⊇ im T_j`, +`N_j ⊆ ker T_j`, and + +``` +ρ = rank(Y M X) = dim(M I + N) - dim N =: f(I,N). (1) +``` + +**Cost.** For fixed (I_j, N_j) the least dim V_j is +`dim I_j + (d - dim N_j) - rank T_j`. Sylvester's inequality gives the lower +bound. For attainment, write T_j = σφ with σ a basis of im T_j, add +coordinates ψ reading a complement of N_j in ker T_j, and add columns τ +completing σ to a basis of I_j: + +``` +Y_j = [φ; ψ; 0], X_j = [σ, 0, τ]. +``` + +Then `X_j Y_j = T_j`, `im X_j = I_j`, `ker Y_j = N_j`. The 00 sector costs +at least rank T00, attained by a rank factorization. Hence + +``` +n_min(ρ) = rank T00 + Σ nu_j + min{ dim I - dim N : f(I,N) = ρ }, (2) +``` + +the minimum over block subspaces `im T_j ⊆ I_j`, `N_j ⊆ ker T_j`. Any larger +n is reached by padding the 00 sector. + +## 2. Unit steps + +Enlarging I by one dimension, or shrinking N by one, raises the cost in (2) +by exactly one and changes f by 0 or +1. For I this is immediate from (1). +For N' ⊂ N of codimension one, `dim(MI+N')` falls by at most one while +`dim N'` falls by exactly one. Every admissible (I,N) is reached from +`(im T, ker T)` by such steps. Consequences: + +* The least dimension at any rank is `n0 = rank T00 + Σ rank T_j`. At n0 the + rank is forced: `ρ0 = f(im T, ker T) = rank(T M T)`, with + `T = diag(T10,T01,T11)`. +* Every feasible rank lies in [ρ0, 2d]. If ρ is feasible at n, so is every + rank in [ρ0, ρ]: a step chain to the attaining pair passes through each + value. Thus **the ranks feasible at dimension n form the interval + [ρ0, ρmax(n)]** for n >= n0, and none are feasible below n0. +* `n_min(ρ) >= n0 + (ρ - ρ0)`. + +## 3. Deficiency identity + +Let `a = Σ (d - dim I_j)` and `b = Σ dim N_j`. Then + +``` +rank R = 2d - a, rank L = 2d - b. (3) +``` + +*R.* A row pair (u,v) annihilates R exactly when +`Φ(u,v) = (uA^-1, (-u+vH)B^-1, u(A^-1-B^-1) - v + vHB^-1)` lies in +`⊕ I_j^⊥` (#5128 (8)). Φ is injective because G' is onto. Each pure +covector lies in im Φ: + +``` +w(A-H)=0: Φ(wA, w) = (w, 0, 0), +w(B-H)=0: Φ(0, w) = (0, w, 0), +wH=0: Φ(0, -w) = (0, 0, w). +``` + +Since `I_j ⊇ im T_j`, `I_j^⊥` lies in the left kernel of T_j. Hence +`⊕ I_j^⊥ ⊆ im Φ`, the annihilator of R has dimension exactly a, and +`rank R = 2d - a`. + +*L.* `ker L = G^-1(N)`. Each pure vector of `⊕ ker T_j` lies in im G: + +``` +(A-H)z=0: G(-z, Az) = (z, 0, 0), +(B-H)z=0: G(z, 0) = (0, -z, 0), +Hz=0: G(z, 0) = (0, 0, z). +``` + +G is injective, so `dim ker L = dim N = b`. + +From (3), `2d - a - b <= ρ <= 2d - max(a,b)`. In particular +`a + b <= 2(2d - ρ)`. The cost in (2) equals `rank T00 + Σ nu_j + 3d - a - b`, +and `nmax = 3d + rank T00 + Σ nu_j` is #5128's formula. Therefore +`n_min(ρ) >= nmax - 2(2d - ρ)`. + +## 4. All-field theorem + +For every field, d, A,B in GL_d(K) and H in M_d(K): + +``` +feasible ranks at n = [ρ0, ρmax(n)] (n >= n0; empty below n0), +n0 = rank T00 + Σ rank T_j, ρ0 = rank(T M T), +n_min(ρ) >= max( n0 + ρ - ρ0, nmax - 2(2d - ρ) ), ρ0 <= ρ <= 2d. (4) +``` + +Both bounds are tight at their endpoints: n_min(ρ0) = n0 and +n_min(2d) = nmax (#5128). Also `2d - 2Σ nu_j <= ρ0 <= 2d - Σ nu_j`, by (3) +at a = b = Σ nu_j. + +Equality in (4) for all fields and all d is **not** proved here. Attainment +needs a pair with a = b and `im R ∩ ker L = 0` at every intermediate rank, plus +efficient unit steps below the crossover. Section 5 certifies equality only +for d = 2 over F2. + +## 5. Finite certificate: d = 2 over F2 + +`verify.py` enumerates all 576 triples A,B in GL_2(F2), H in M_2(F2) +(288 with AB != BA). For each it enumerates every admissible block pair +(I,N) and computes (1) and (2) exactly. It checks (3) and the sandwich on +every enumerated pair, and checks that equality holds in (4) for every ρ. +For every triple and every feasible rank it then assembles a literal pair +P,Q at the claimed least n, recomputes the Schur complements from the matrix +entries, and checks idempotence, commutation, the three blocks and the rank. +That is 2,496 literal witnesses. + +Outcome: ρ0 is 0 for 408 triples, 2 for 144 and 4 for 24; there are 16 +distinct profiles. Rank two, the first step named in #5128, is feasible at +n exactly when ρ0 <= 2 and `n >= max(n0 + 2 - ρ0, nmax - 4)`. The 24 triples +with ρ0 = 4 are those with T10, T01, T11 all invertible. They admit only +rank 4, at n = n0 = nmax. + +## 6. Boundary + +This concerns one common deletion with invertible pivots over a field. It +gives no header count, physical header producer or consumer, dirty-owner +restoration, precision, stock, recursive compilation or outer transfer. No +kappa changes. diff --git a/research/schur-intermediate-ranks/README.md b/research/schur-intermediate-ranks/README.md new file mode 100644 index 0000000000..fb9f561e88 --- /dev/null +++ b/research/schur-intermediate-ranks/README.md @@ -0,0 +1,115 @@ +# Nonmaximal Schur-commutator ranks for prescribed pivots + +**Scoped all-field proof plus an exact finite certificate. No new kappa.** +Produced by Nick Petalas. Apache-2.0. + +Krzysztof Wojt's [PR #5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128) +(`research/arbitrary-pivot-schur-minimum`) finds the least dimension n at which +commuting idempotents P,Q with prescribed invertible pivots `P11=A`, `Q11=B` +and product block `(PQ)11=H` reach Schur-commutator rank 2d. Its Open next +question 1 asks which smaller ranks are feasible at each ambient dimension. It +names d=2 over F2, rank two, as a first step. This package answers that first +step for every rank and proves an all-field lower bound. + +## Result + +Write `T00=I-A-B+H`, `T10=A-H`, `T01=B-H`, `T11=H`, `nu_j = nullity T_j`, +`nmax = 3d + rank T00 + Σ nu_j` (#5128), and + +``` +n0 = rank T00 + rank T10 + rank T01 + rank T11, +rho0 = rank(T M T), T = diag(T10,T01,T11), +``` + +where `M = G G'` is built from #5128's ordered factors (PROOF.md §1). + +**Theorem (every field, every d; [PROOF.md](PROOF.md)).** + +1. No pair exists below n0. At n0 the rank is forced to rho0. +2. For n >= n0, the feasible ranks form the interval `[rho0, rhomax(n)]`. + Ranks below rho0 never occur. +3. For rho0 <= rho <= 2d, + ``` + n_min(rho) >= max( n0 + rho - rho0, nmax - 2(2d - rho) ). + ``` + Both terms are tight at their endpoints: `n_min(rho0)=n0` and + `n_min(2d)=nmax`. + +The second term comes from a new deficiency identity. If the sector images +lose total dimension a and the sector kernels have total dimension b, then +`rank R = 2d-a` and `rank L = 2d-b` exactly. Hence +`2d-a-b <= rho <= 2d-max(a,b)`. + +**Finite certificate (d=2, F2).** Equality holds in (3) for all 576 triples +`A,B in GL_2(F2)`, `H in M_2(F2)`, 288 of them with AB != BA. rho0 is 0 for +408 triples, 2 for 144 and 4 for 24, with 16 distinct profiles. For the first +step named in #5128: rank two is feasible at n exactly when rho0 <= 2 and +`n >= max(n0+2-rho0, nmax-4)`. The 24 triples with T10, T01, T11 all +invertible admit only rank four. + +Example: A=B=H=I gives the profile n = 2, 4, 6, 8, 10 for rho = 0..4, so each +extra rank costs two dimensions. Profiles with crossover, such as +n = 3, 4, 5, 7, 9, show both terms of the maximum binding. + +## Evidence + +[verify.py](verify.py) is standard-library only. For each triple it enumerates +every admissible block pair `im T_j ⊆ I_j`, `N_j ⊆ ker T_j` and computes +the exact least dimension of every rank. On every enumerated pair it checks +`rank R = 2d-a`, `rank L = 2d-b` and the sandwich bound. It checks the closed +law for every triple. For every triple and every feasible rank, it then +assembles a literal pair P,Q at the claimed least n. It recomputes S and Z from +the matrix entries and checks idempotence, commutation, all three prescribed +blocks and the rank: 2,496 literal witnesses. Four seeded controls must be +rejected: a slope-one-only law, the rank-2d formula used at every rank, a +corrupted P entry and a wrong prescribed H. + +The exhaustive minimum is complete for d=2 over F2 because of the reduction +in PROOF.md §1. Every pair arises from sector factorizations, and the cost +of each (I,N) choice is its proved minimum. + +## Reproduce + +From the repository root (any CPython 3.12; about 2 s each): + +```sh +python3.12 -I -W error -B research/schur-intermediate-ranks/verify.py +python3.12 -I -O -W error -B research/schur-intermediate-ranks/verify.py +python3.12 -B scripts/research_package.py --package research/schur-intermediate-ranks +python3.12 -B scripts/check_research_commit.py --package research/schur-intermediate-ranks --check-source-history +``` + +Expected final line: `PASS_SCHUR_INTERMEDIATE_RANKS_D2_F2`, with +`rows_sha256 e18d15092793582f8d16939086fb512563ecbffc95e0f537ddece6873232dc81`. + +## Limitations + +Equality in the lower bound is proved only for d=2 over F2. For other d and +fields it is a bound, not a formula. The theorem concerns one common deletion +with invertible pivots. It gives no header frequency, physical producer or +consumer, dirty-owner restoration, precision, stock or outer transfer. The +selected frontier and kappa are unchanged. No independent human or formal +proof-kernel review is claimed. + +## Open next questions + +1. **Does equality hold for every d and field?** Equality would give a closed + form for the whole trade-off and complete #5128's question 1. First step: + run the same reduction for d=2 over F3 and d=3 over F2. Then try a two-phase + chain: single efficient steps up to the crossover, followed by paired I/N + steps that keep `im R ∩ ker L = 0`. Blocker: over small fields that + transversality might fail for every admissible choice. +2. **Is there a closed form for rho0?** The ranks of the T_j alone do not fix + it in the binary data. Begin with the proved sandwich + `2d - 2Σ nu_j <= rho0 <= 2d - Σ nu_j` and find the extra invariant. + +## Credit + +Produced by Nick Petalas. Krzysztof Wojt's #5128 supplies the arbitrary-pivot +sector factorization, the ordered maps L, R and the rank-2d minimum, and poses +the question answered here. These are cited, not rechecked. The earlier +Schur-family lineage credited in that package keeps its credit: ssafwann's +#4657/#4671 sector and split-factor method, Nick Petalas's #4597/#4746/#4771/ +#4774/#4785, Ryanson Jonathan's #4609/#4617 and lee-phys's #4634. The new work +is the reduction to block subspace pairs, the unit-step interval theorem, the +deficiency identity with its lower bound, and the d=2 binary certificate. diff --git a/research/schur-intermediate-ranks/SOURCES.json b/research/schur-intermediate-ranks/SOURCES.json new file mode 100644 index 0000000000..283a901b8c --- /dev/null +++ b/research/schur-intermediate-ranks/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/arbitrary-pivot-schur-minimum/PROOF.md", + "usage": "provenance", + "git_blob": "c7d58883b4df5ddab4f237a521458b7f506b3617", + "sha256": "77118415edf74aa4b6a49c94cb735913ad08377802ab44f3f51f66531b46593a" + } + ] +} diff --git a/research/schur-intermediate-ranks/TASK.json b/research/schur-intermediate-ranks/TASK.json new file mode 100644 index 0000000000..a053f44d27 --- /dev/null +++ b/research/schur-intermediate-ranks/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "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": "Which Schur-commutator ranks below 2d are feasible, and at which least ambient dimension, for commuting idempotents with prescribed invertible pivots A,B and product block H (Open next question 1 of PR #5128)?", + "scope_change_reason": "The card asks for decoder/coframe changes with a full signed moment. This package answers a structural open question posed by PR #5128 in the Schur block-deletion family, which bounds the rank available to such a decoder request. It does not price a decoder.", + "bottleneck_link": "Side result. It gives the exact rank/dimension trade-off for one Schur deletion request, which a header or decoder design would need before pricing. It does not change any supplier bill or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at an all-field lower bound and an exact d=2 F2 certificate; list general attainment as open rather than extending the search.", + "outcome": "partial", + "evidence": "PROOF.md proves, over every field, that feasible ranks at each n form an interval [rho0, rhomax(n)] and n_min(rho) >= max(n0+rho-rho0, nmax-2(2d-rho)). verify.py certifies equality for all 576 triples at d=2 over F2, with 2,496 literal commuting idempotent witnesses and 4 rejected controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does equality n_min(rho)=max(n0+rho-rho0, nmax-2(2d-rho)) hold for every d and every field?", + "why_it_matters": "It would give a closed form for the whole rank/dimension trade-off, completing PR #5128 Open next question 1.", + "first_step": "Run the same exhaustive reduction for d=2 over F3 and d=3 over F2, then try a two-phase step chain: efficient single steps up to the crossover, then paired I/N steps keeping im R and ker L transverse.", + "blocked_by": "Over small fields the transversality im R ∩ ker L = 0 may fail for every admissible choice; no general argument is given." + }, + { + "question": "Is there a closed form for rho0 = rank(T M T) in terms of A,B,H?", + "why_it_matters": "rho0 is the forced rank at the absolute minimum dimension n0; ranks alone of the T_j do not determine it (d=2, F2 data).", + "first_step": "Compare rho0 against the sandwich 2d-2*sum(nu_j) <= rho0 <= 2d-sum(nu_j) on the 576 binary triples and identify the extra invariant.", + "blocked_by": "None known." + } + ] +} diff --git a/research/schur-intermediate-ranks/VERIFY.json b/research/schur-intermediate-ranks/VERIFY.json new file mode 100644 index 0000000000..db5aeaae63 --- /dev/null +++ b/research/schur-intermediate-ranks/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 576 d=2 F2 triples: exhaustive block-subspace minimum, the closed law, rank R/L identities on every pair, 2,496 literal witnesses, 4 seeded controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same replay with assertions disabled; the verifier raises explicitly." + } + ] +} diff --git a/research/schur-intermediate-ranks/verify.py b/research/schur-intermediate-ranks/verify.py new file mode 100644 index 0000000000..58a2bb02d2 --- /dev/null +++ b/research/schur-intermediate-ranks/verify.py @@ -0,0 +1,365 @@ +#!/usr/bin/env python3 +"""Exact nonmaximal Schur-commutator rank profiles for d=2 over F2. + +Nick Petalas. Apache-2.0. Standard library only. + +For every A,B in GL_2(F2) and H in M_2(F2) this script +1. enumerates every sector choice I_j >= im T_j, N_j <= ker T_j and records + the least ambient dimension for each Schur-commutator rank; +2. checks the closed law n_min(rho)=max(n0+rho-rho0, nmax-2(2d-rho)) on the + feasible interval [rho0, 2d], and the rank identities rank R=2d-a, + rank L=2d-b on every enumerated choice; +3. builds a literal commuting idempotent pair for every (triple, rank) at the + claimed least dimension and recomputes its Schur commutator from scratch. +Seeded controls must be rejected. Exit status 0 means every check passed. +""" +from __future__ import annotations + +import hashlib +import itertools +import json +import sys + +D = 2 +SECTORS = ("10", "01", "11") + + +# ---- dense F2 matrices as lists of 0/1 rows ------------------------------- + +def mul(x, y): + cols = len(y[0]) + return [[sum(x[i][k] & y[k][j] for k in range(len(y))) & 1 + for j in range(cols)] for i in range(len(x))] + + +def add(x, y): + return [[(a ^ b) for a, b in zip(r, s)] for r, s in zip(x, y)] + + +def eye(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def zeros(r, c): + return [[0] * c for _ in range(r)] + + +def rows_to_masks(x): + return [sum(bit << j for j, bit in enumerate(row)) for row in x] + + +def mask_rank(masks): + basis = [] + for v in masks: + for b in basis: + v = min(v, v ^ b) + if v: + basis.append(v) + return len(basis) + + +def rank(x): + return mask_rank(rows_to_masks(x)) if x and x[0] else 0 + + +def transpose(x): + return [list(c) for c in zip(*x)] + + +def inverse(x): + n = len(x) + a = [row[:] + e for row, e in zip(x, eye(n))] + for c in range(n): + piv = next((r for r in range(c, n) if a[r][c]), None) + if piv is None: + raise ValueError("singular") + a[c], a[piv] = a[piv], a[c] + for r in range(n): + if r != c and a[r][c]: + a[r] = [u ^ v for u, v in zip(a[r], a[c])] + return [row[n:] for row in a] + + +def block(rows): + out = [] + for brow in rows: + for i in range(len(brow[0])): + out.append(sum((b[i] for b in brow), [])) + return out + + +def sub_block(x, r0, r1, c0, c1): + return [row[c0:c1] for row in x[r0:r1]] + + +# ---- subspaces of F2^2 as frozensets of vector tuples ----------------------- + +VECS = [tuple(v) for v in itertools.product((0, 1), repeat=D)] + + +def span(vs): + out = {tuple([0] * D)} + for v in vs: + out |= {tuple(a ^ b for a, b in zip(s, v)) for s in out} + return frozenset(out) + + +SUBSPACES = sorted({span(c) for k in range(D + 1) + for c in itertools.combinations(VECS, k)}, + key=lambda s: (len(s), sorted(s))) + + +def dim(s): + return len(s).bit_length() - 1 + + +def basis(s, start=()): + """Basis of s extending the independent list start (vectors in s).""" + out = list(start) + for v in sorted(s): + if span(out) != span(out + [v]): + out.append(v) + return out[len(start):] + + +def image(t): + return span([tuple(c) for c in transpose(t)]) + + +def kernel(t): + return frozenset(v for v in VECS + if all(sum(a & b for a, b in zip(row, v)) & 1 == 0 for row in t)) + + +# ---- the reduction ---------------------------------------------------------- + +def compressed(a, b, h): + i2 = eye(D) + return {"00": add(add(add(i2, a), b), h), "10": add(a, h), + "01": add(b, h), "11": h} + + +def factor_maps(a, b, h): + """G: U^2 -> U^3 and G': U^3 -> U^2 with L=Y G and R=G' X (PROOF.md).""" + ai, bi = inverse(a), inverse(b) + z = zeros(D, D) + bih, hbi = mul(bi, h), mul(h, bi) + g = block([[z, ai], [bih, bi], [add(eye(D), bih), add(ai, bi)]]) + gp = block([[ai, bi, add(ai, bi)], [z, hbi, add(hbi, eye(D))]]) + return g, gp + + +def embed(j, v): + out = [0] * (3 * D) + out[D * j:D * j + D] = v + return out + + +def profile(a, b, h, check_identities=True): + t = compressed(a, b, h) + g, gp = factor_maps(a, b, h) + m = mul(g, gp) + im = {s: image(t[s]) for s in SECTORS} + ker = {s: kernel(t[s]) for s in SECTORS} + ich = [[s for s in SUBSPACES if im[j] <= s] for j in SECTORS] + nch = [[s for s in SUBSPACES if s <= ker[j]] for j in SECTORS] + gt = transpose(g) + best = {} + witness = {} + for ichoice in itertools.product(*ich): + cols = [embed(k, list(v)) for k, s in enumerate(ichoice) for v in basis(s)] + mi = rows_to_masks([[sum(row[q] & c[q] for q in range(3 * D)) & 1 + for row in m] for c in cols]) + a_def = sum(D - dim(s) for s in ichoice) + rank_r = mask_rank(rows_to_masks([[sum(row[q] & c[q] for q in range(3 * D)) & 1 + for row in gp] for c in cols])) + for nchoice in itertools.product(*nch): + nb = rows_to_masks([embed(k, list(v)) for k, s in enumerate(nchoice) + for v in basis(s)]) + f = mask_rank(mi + nb) - len(nb) + b_def = len(nb) + if check_identities: + # rank L = 2d - b: rank of U^2 -> U^3/N, i.e. rank[G | N] - dim N. + rank_l = mask_rank(rows_to_masks(gt) + nb) - len(nb) + if rank_r != 2 * D - a_def or rank_l != 2 * D - b_def: + raise AssertionError("rank R/L identity fails") + if not (2 * D - a_def - b_def <= f <= 2 * D - max(a_def, b_def)): + raise AssertionError("Sylvester sandwich fails") + cost = sum(dim(s) for s in ichoice) - b_def + if cost < best.get(f, 10 ** 9): + best[f] = cost + witness[f] = (ichoice, nchoice) + base = rank(t["00"]) + sum(D - rank(t[j]) for j in SECTORS) + nmin = {f: base + c for f, c in best.items()} + tt = block([[t[s] if s == r else zeros(D, D) for s in SECTORS] for r in SECTORS]) + rho0 = rank(mul(mul(tt, m), tt)) + return t, nmin, witness, rho0 + + +def law(t, rho0): + n0 = rank(t["00"]) + sum(rank(t[j]) for j in SECTORS) + nmax = 3 * D + rank(t["00"]) + sum(D - rank(t[j]) for j in SECTORS) + return {r: max(n0 + r - rho0, nmax - 2 * (2 * D - r)) + for r in range(rho0, 2 * D + 1)}, n0, nmax + + +# ---- literal witness --------------------------------------------------------- + +def sector_factors(tj, ij, nj): + """X (d x r), Y (r x d) with XY=tj, im X=ij, ker Y=nj, r minimal.""" + imt = image(tj) + sigma = basis(imt) + phi_cols = [] + for col in transpose(tj): # coordinates of each column in basis sigma + for coeffs in itertools.product((0, 1), repeat=len(sigma)): + vec = tuple(sum(c & s[q] for c, s in zip(coeffs, sigma)) & 1 for q in range(D)) + if vec == tuple(col): + phi_cols.append(list(coeffs)) + break + phi = transpose(phi_cols) if sigma else [] + nbas = basis(nj) + kbas = basis(kernel(tj), nbas) + wbas = basis(frozenset(VECS), nbas + kbas) + full = nbas + kbas + wbas # basis of U; psi reads the kbas coordinates + coords = inverse(transpose([list(v) for v in full])) + psi = [coords[len(nbas) + q] for q in range(len(kbas))] + tau = basis(ij, sigma) + y = [row[:] for row in phi] + psi + [[0] * D for _ in tau] + x_cols = [list(s) for s in sigma] + [[0] * D for _ in psi] + [list(v) for v in tau] + x = transpose(x_cols) if x_cols else [[] for _ in range(D)] + return x, y + + +def build_pair(a, b, h, ichoice, nchoice): + t = compressed(a, b, h) + sel = {"00": (image(t["00"]), kernel(t["00"]))} + for k, j in enumerate(SECTORS): + sel[j] = (ichoice[k], nchoice[k]) + xs, ys, p0d, q0d = [], [], [], [] + for j in ("00",) + SECTORS: + x, y = sector_factors(t[j], *sel[j]) + xs.append(x) + ys += y + p0d += [int(j[0] == "1")] * len(y) + q0d += [int(j[1] == "1")] * len(y) + n = len(ys) + pi = [sum((x[r] for x in xs), []) for r in range(D)] + inc = ys + if mul(pi, inc) != eye(D): + raise AssertionError("pi i != I") + # basis of ker pi + kerpi = [] + for v in itertools.product((0, 1), repeat=n): + if len(kerpi) == n - D: + break + if any(sum(pi[r][q] & v[q] for q in range(n)) & 1 for r in range(D)): + continue + if mask_rank(rows_to_masks(kerpi + [list(v)])) == len(kerpi) + 1: + kerpi.append(list(v)) + mm = transpose(transpose(inc) + kerpi) + mi = inverse(mm) + p0 = [[int(i == j) * p0d[i] for j in range(n)] for i in range(n)] + q0 = [[int(i == j) * q0d[i] for j in range(n)] for i in range(n)] + return mul(mul(mi, p0), mm), mul(mul(mi, q0), mm) + + +def literal_rank(a, b, h, p, q): + n = len(p) + if mul(p, p) != p or mul(q, q) != q or mul(p, q) != mul(q, p): + raise AssertionError("not commuting idempotents") + if sub_block(p, 0, D, 0, D) != a or sub_block(q, 0, D, 0, D) != b \ + or sub_block(mul(p, q), 0, D, 0, D) != h: + raise AssertionError("prescribed blocks fail") + if n == D: + return 0 + ai, bi = inverse(a), inverse(b) + s = add(sub_block(p, D, n, D, n), + mul(mul(sub_block(p, D, n, 0, D), ai), sub_block(p, 0, D, D, n))) + z = add(sub_block(q, D, n, D, n), + mul(mul(sub_block(q, D, n, 0, D), bi), sub_block(q, 0, D, D, n))) + return rank(add(mul(s, z), mul(z, s))) + + +# ---- driver ------------------------------------------------------------------- + +def triples(): + mats = [[[w, x], [y, z]] for w, x, y, z in itertools.product((0, 1), repeat=4)] + gl = [m for m in mats if (m[0][0] & m[1][1]) ^ (m[0][1] & m[1][0])] + return [(a, b, h) for a in gl for b in gl for h in mats] + + +def run(): + rows = [] + witnesses = 0 + for a, b, h in triples(): + t, nmin, wit, rho0 = profile(a, b, h) + predicted, n0, nmax = law(t, rho0) + if nmin != predicted: + raise AssertionError(f"law fails at {a},{b},{h}: {nmin} vs {predicted}") + for r, (ich, nch) in wit.items(): + p, q = build_pair(a, b, h, ich, nch) + if len(p) != nmin[r] or literal_rank(a, b, h, p, q) != r: + raise AssertionError("literal witness fails") + witnesses += 1 + rows.append({"A": a, "B": b, "H": h, "noncommuting": mul(a, b) != mul(b, a), + "n0": n0, "rho0": rho0, "nmax": nmax, + "n_min": [nmin[r] for r in range(rho0, 2 * D + 1)]}) + return rows, witnesses + + +def controls(): + """Each seeded mutation must be rejected by the same checks.""" + a, b, h = eye(D), eye(D), eye(D) # A=B=H=I: slope-two profile 2,4,6,8,10 + t, nmin, wit, rho0 = profile(a, b, h) + predicted, _, _ = law(t, rho0) + rejected = 0 + # 1. slope-one-only law (drop the 2(2d-rho) branch) + n0 = rank(t["00"]) + sum(rank(t[j]) for j in SECTORS) + rejected += {r: n0 + r - rho0 for r in predicted} != nmin + # 2. #5128 formula alone for every rank + rejected += any(nmin[r] != predicted[2 * D] for r in nmin) is True + # 3. corrupted witness: flip one entry of P + ich, nch = wit[2] + p, q = build_pair(a, b, h, ich, nch) + p[-1][-1] ^= 1 + try: + literal_rank(a, b, h, p, q) + except AssertionError: + rejected += 1 + # 4. wrong prescribed H + p, q = build_pair(a, b, h, ich, nch) + try: + literal_rank(a, b, zeros(D, D), p, q) + except AssertionError: + rejected += 1 + return rejected + + +def main(): + rows, witnesses = run() + rejected = controls() + profiles = {} + for r in rows: + key = (r["rho0"], tuple(r["n_min"])) + profiles[key] = profiles.get(key, 0) + 1 + summary = { + "triples": len(rows), + "noncommuting_triples": sum(r["noncommuting"] for r in rows), + "literal_witnesses": witnesses, + "distinct_profiles": len(profiles), + "rho0_counts": {str(k): sum(1 for r in rows if r["rho0"] == k) for k in range(5)}, + "controls_rejected": rejected, + "rows_sha256": hashlib.sha256(json.dumps(rows, sort_keys=True).encode()).hexdigest(), + } + expected = {"triples": 576, "noncommuting_triples": 288, "controls_rejected": 4} + ok = all(summary[k] == v for k, v in expected.items()) + print(json.dumps(summary, indent=1, sort_keys=True)) + if not ok: + print("FAIL", file=sys.stderr) + return 1 + print("PASS_SCHUR_INTERMEDIATE_RANKS_D2_F2") + return 0 + + +if __name__ == "__main__": + sys.exit(main())