diff --git a/research/schur-ranks-all-fields/PROOF.md b/research/schur-ranks-all-fields/PROOF.md new file mode 100644 index 0000000000..698b34aba7 --- /dev/null +++ b/research/schur-ranks-all-fields/PROOF.md @@ -0,0 +1,317 @@ +# Exact intermediate Schur ranks over every field + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. + +This resolves both open next questions in Nick Petalas's +[PR #6031](https://github.com/CrocSwap/integer-mult-bounds/pull/6031), +`research/schur-intermediate-ranks`, scientific head +`acc000f4edfa0b0c4a90b505c6e02a4c3572f74c`. We use its sector-subspace reduction +and minimum realization cost, and Krzysztof Wojt's +[PR #5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128), +`research/arbitrary-pivot-schur-minimum`, scientific head +`2839d35e58b3285a1992a3ecbae2809ebef7661b`, for the Schur factorization and +commuting-idempotent realization. Those predecessor reductions are cited, +not claimed as new or independently re-proved here. The added argument is a +sector-preserving decomposition into two bilinear pairings. Reducing a +bilinear pairing to a rank core and its radicals is classical linear algebra; +no historical priority is claimed for that operation. + +## 1. Statement and setting + +Let K be any field, let d >= 1, and fix A,B in GL_d(K) and H in M_d(K). +No commutation among A,B,H is assumed. Define + +``` +F = A-H, J = B-H, T00 = I-A-B+H, +s = nullity F + nullity J + nullity H, +n0 = rank T00 + rank F + rank J + rank H, +nmax = 3d + rank T00 + s. +``` + +Here `nmax` denotes the least dimension attaining the maximum commutator +rank 2d, as in #5128; it is not an upper bound on the ambient dimension. +Consider all commuting idempotents P,Q in M_n(K) satisfying + +``` +P11 = A, Q11 = B, (PQ)11 = H, +``` + +where the leading block has size d. Their Schur complements are + +``` +S = P22 - P21 A^-1 P12, Z = Q22 - Q21 B^-1 Q12. +``` + +Put rho = rank(SZ-ZS), and let n_min(rho) be the least ambient dimension +for that rank with the prescribed A,B,H. + +**Theorem.** The minimum possible rank is + +``` +rho0 = rank(J A^-1 F) + rank(F B^-1 J) + 2 rank H - 2d. (1) +``` + +For every integer rho with rho0 <= rho <= 2d, + +``` +n_min(rho) = max(n0 + rho - rho0, nmax - 2(2d-rho)). (2) +``` + +There are no other possible ranks. A rank rho in this interval is feasible +at dimension n exactly when n >= n_min(rho). Thus the theorem also decides +the complete rank set at every ambient dimension. Both formulas hold in +arbitrary characteristic and over finite or infinite fields. + +## 2. Cited reduction and the deficiency pairing + +Write U = K^d and E = U direct-sum U. In the 10,01,11 sectors put +`T10=F`, `T01=J`, `T11=H`. The reduction in #6031, Sections 1--3, permits +arbitrary sectorwise subspaces + +``` +im Tj <= Ij <= U, Nj <= ker Tj. (3) +``` + +They are realized by maps Xj,Yj with XjYj=Tj, im Xj=Ij and ker Yj=Nj. +Their least sector dimension is +`dim Ij + d - dim Nj - rank Tj`; the 00 sector can have dimension +rank T00. In particular, with + +``` +a = sum_j (d - dim Ij), b = sum_j dim Nj, +``` + +the least ambient dimension realizing these choices is + +``` +n = nmax - a - b. (4) +``` + +The same predecessor supplies the maps + +``` +G(x,y) = (A^-1 y, -B^-1(Hx+y), (I-B^-1 H)x + (A^-1-B^-1)y), +G'(u,v,w) = (A^-1 u - B^-1 v + (A^-1-B^-1)w, + H B^-1 v + (H B^-1-I)w). +``` + +Here G:E -> U^3 is injective and G':U^3 -> E is surjective. If +`I = I10 direct-sum I01 direct-sum I11` and similarly N, the Schur +commutator rank equals the rank of `L R`, with `L=Y G`, `R=G' X`. +Let + +``` +C = G'I <= E, D' = annihilator(C) <= E*, +K' = G^-1 N <= E. +``` + +The deficiency identities in #6031 give dim D'=a and dim K'=b. Restrict +the natural bilinear evaluation pairing `E* x E -> K` to D' x K', +and call its rank q. Its right kernel is K' intersect C. Therefore + +``` +rho = dim C - dim(C intersect K') + = 2d - a - b + q. (5) +``` + +All annihilators here are algebraic dual annihilators, not Hermitian +orthogonal complements. + +For the largest possible deficiencies, take Ij=im Tj and Nj=ker Tj. +Their spaces D,K have the following direct-sum decompositions; w is a +row covector and z is a column vector: + +``` +D10 = {(wA,w) : wF=0}, K10 = {(-z,Az) : Fz=0}, +D01 = {(0,w) : wJ=0}, K01 = {(z,0) : Jz=0}, +D11 = {(0,-w) : wH=0}, K11 = {(z,0) : Hz=0}, +D = D10 + D01 + D11, K = K10 + K01 + K11. (6) +``` + +These are precisely the pure-sector lifts in #6031's deficiency proof. +For example G(-z,Az)=(z,0,0) when Fz=0, whereas G(z,0)=(0,-z,0) +when Jz=0 and G(z,0)=(0,0,z) when Hz=0. The minus sign in the 01 lift +does not change its subspace. The covector lifts follow by composing +with G'. Injectivity of G and of the dual map of G' proves that the +sums in (6) are direct. Each of D and K has dimension s. + +More generally D' is an arbitrary direct sum of subspaces of the three +Dj, and K' an arbitrary direct sum of subspaces of the three Kj. +Indeed, a choice of covectors Wj <= left ker Tj corresponds exactly +to Ij=annihilator(Wj), and a subspace of Kj corresponds exactly to Nj. +Thus every sectorwise subspace choice made below is allowed by (3), +not merely a choice in the unrestricted spaces E or E*. + +## 3. Only two pairing blocks survive + +Compute the evaluation pairing of (6). The entry in each cell is the +value on the corresponding w,z, with their row and column constraints: + +| | K10 | K01 | K11 | +|---|---|---|---| +| D10 | 0 | w H z | 0 | +| D01 | w H z | 0 | 0 | +| D11 | 0 | 0 | 0 | + +For example the D10,K10 entry is `-wAz+wAz=0`. The D10,K01 entry +is wAz=wHz because wF=0; the D01,K10 entry is wAz=wHz because Fz=0. +The D10,K11 entry vanishes since wA=wH and Hz=0. The D11,K10 entry +vanishes since Az=Hz and wH=0. All remaining entries vanish directly. +These identities also hold in characteristic two. + +Let + +``` +r1 = rank of (left ker F) x (ker J) -> K, (w,z) |-> wHz, +r2 = rank of (left ker J) x (ker F) -> K, (w,z) |-> wHz, +r = r1 + r2. (7) +``` + +The two nonzero blocks have separate domain and codomain sectors, so +the full D x K pairing has rank r. The two ranks need not be equal. +At the largest deficiencies a=b=s, equation (5) gives + +``` +rho0 = 2d - 2s + r. (8) +``` + +Every restriction has q <= r and a,b <= s. More precisely, the +rank lower bound rho >= rho0 follows either from the unit-step +argument in #6031 or by deleting one basis direction at a time +from the full pairing: such a deletion lowers a+b by one and q by +zero or one, so (5) cannot decrease. Thus (8) is the minimum rank. +Its least dimension is `nmax-2s=n0` by (4). + +## 4. Sharp dimension for every intermediate rank + +Put delta=2d-rho. For any admissible pair D',K', equation (5) says +`delta=a+b-q`. Since q <= min(a,b,r), + +``` +a+b <= 2 delta, a+b <= delta+r. +``` + +Equation (4), or the corresponding lower bound for a nonminimal +realization of the same subspaces, therefore implies + +``` +n >= nmax - delta - min(delta,r). (9) +``` + +We now attain (9), for every integer +`0 <= delta <= 2s-r = 2d-rho0`, while respecting all three sectors. + +Reduce each of the two nonzero bilinear blocks in the table to rank +normal form by choosing bases within its row and column sectors. +Each block is a direct sum of paired one-dimensional coordinates +with evaluation matrix I, and zero left/right radical coordinates. +Because the blocks use disjoint sectors, these two basis changes +can be performed independently. There are r paired coordinates on +each side in total, and `2s-2r` unpaired radical coordinates across +the two sides, including both 11 sectors. + +* If `0 <= delta <= r`, choose any delta of the paired coordinates, + retaining each on both sides. This gives a=b=delta and q=delta. + Hence the resulting rank is `2d-delta`, with cost `nmax-2delta`. +* If `r <= delta <= 2s-r`, retain all r paired coordinates on both + sides and add any `delta-r` radical coordinates. There are enough + because `delta-r <= 2s-2r`. Then a+b=delta+r and q=r, giving rank + `2d-delta` with cost `nmax-delta-r`. + +The normal forms and all the selections are within individual sectors. +Section 2 therefore realizes them by actual commuting idempotents +with the prescribed three leading blocks. No field-size condition +or generic choice of a vector is needed. + +Consequently equality holds in (9). Since + +``` +n0 = nmax-2s, rho0 = 2d-2s+r, +n0+rho-rho0 = nmax-delta-r, +``` + +this equality is exactly (2). It also establishes every integer rank +in the stated interval; the factorization through E excludes ranks +above 2d. Padding the 00 sector with any number of coordinates on +which both X00 and Y00 are zero preserves A,B,H and the commutator +rank. It attains every larger ambient dimension. This proves the +claimed feasibility statement for each n, including zero-size Schur +complements when n=d. + +## 5. Eliminating nullspace bases from rho0 + +For arbitrary square F,J,H of size d, the rank of the pairing +`(left ker F) x (ker J) -> K`, `(w,z) |-> wHz`, is + +``` +r1 = rank [[F,H],[0,J]] - rank F - rank J. (10) +``` + +One way to see (10) is to project the image of the block matrix to +its bottom component. That projection has image im J; its kernel +inside the block-matrix image is the top-component subspace +`im F + H ker J`. Subtracting rank F leaves the rank of the induced +map `ker J -> U/im F`, which is also the rank of the displayed +pairing against left ker F. + +In our setting F+H=A is invertible. Adding the second block column +to the first changes the block matrix to `[[A,H],[J,J]]`. Eliminating +the bottom-left block gives the Schur complement + +``` +J - J A^-1 H = J A^-1 F. +``` + +Therefore + +``` +r1 = d + rank(J A^-1 F) - rank F - rank J, +r2 = d + rank(F B^-1 J) - rank F - rank J. (11) +``` + +The second identity uses J+H=B and the swapped pairing. Substitute +(11) and `s=3d-rank F-rank J-rank H` into (8) to obtain (1). +The order of factors is essential; A,B,H need not commute. + +## 6. An odd minimum-rank fixture over F3 + +Take d=2 over F3 and + +``` +H = [[1,0],[0,1]], +A = [[1,0],[0,2]], B = [[1,1],[0,1]], +F = [[0,0],[0,1]], J = [[0,1],[0,0]], +T00 = [[0,2],[0,2]]. +``` + +Then s=2, n0=5 and nmax=9. In this field + +``` +J A^-1 F = [[0,2],[0,0]], F B^-1 J = [[0,0],[0,0]], +r1=1, r2=0, rho0=1. +``` + +Formula (2) gives the exact minimum dimensions + +| rho | 1 | 2 | 3 | 4 | +|---|---|---|---|---| +| n_min(rho) | 5 | 6 | 7 | 9 | + +In particular, neither equality of the two pairing ranks nor evenness +of rho0 can be imported from the binary d=2 census in #6031. +That census remains valid; this fixture is over a different field. + +## 7. Scope and verification boundary + +This is a written algebraic proof for one common deletion with invertible +pivots. The independent finite checks accompanying the package corroborate +its identities and constructions; they do not prove its universal +quantifiers or constitute proof-kernel verification. The theorem depends +on the cited predecessor factorization and sector realization. + +It supplies no physical header producer or consumer, header count, +dirty-owner restoration protocol, precision bound, stock estimate, +recursive compilation or outer transfer. Those costs are unpriced here, +not zero. It changes neither the selected multiplication construction nor +kappa, and it makes no claim that archival publication is scientific +acceptance of the theorem. diff --git a/research/schur-ranks-all-fields/README.md b/research/schur-ranks-all-fields/README.md new file mode 100644 index 0000000000..3fa5a483a8 --- /dev/null +++ b/research/schur-ranks-all-fields/README.md @@ -0,0 +1,124 @@ +# Exact Schur rank–dimension law over every field + +**Scoped algebraic theorem with finite corroboration; no new κ.** This resolves +both open questions in Nick Petalas's [PR #6031](https://github.com/CrocSwap/integer-mult-bounds/pull/6031): +the minimum-dimension law holds for every field and every positive block size, +and the forced minimum rank has a formula using only d-by-d matrix products. +The [proof](PROOF.md) supplies the universal claim; finite computations do not. + +For prescribed A,B in GL_d(K), H in M_d(K), put F=A-H, J=B-H and +T00=I-A-B+H. Among commuting idempotents P,Q with leading blocks A,B and +(PQ)11=H, and Schur complements S,Z, let rho=rank(SZ-ZS). Then + +``` +n0 = rank T00 + rank F + rank J + rank H, +nmax = 3d + rank T00 + nullity F + nullity J + nullity H, +rho0 = rank(J A^-1 F) + rank(F B^-1 J) + 2 rank H - 2d, +n_min(rho) = max(n0 + rho - rho0, nmax - 2(2d-rho)). +``` + +Every integer rho in [rho0,2d] occurs, and it occurs at ambient dimension n +exactly when n >= n_min(rho). No other rank occurs. Here nmax names the least +dimension attaining rank 2d, not a maximum ambient dimension. The argument +preserves sector constraints: the deficiency pairing has two independent +cross-sector blocks, each admitting a rank core and radicals over any field. +Selecting matched coordinates and radical coordinates attains the lower bound. + +PR #6031 established the lower bound and certified equality only at d=2 over +F2. The new proof removes both restrictions. It also explains the missing +invariant: the two cross-sector pairing ranks. They need not agree. For +A=diag(1,2), B=[[1,1],[0,1]], H=I over F3, rho0=1 and the minimum dimensions +at ranks 1,2,3,4 are 5,6,7,9. Thus binary d=2 evenness does not generalize. + +## Reproduction and evidence + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -W error -B research/schur-ranks-all-fields/verify.py +python3.12 -I -O -W error -B research/schur-ranks-all-fields/verify.py +python3.12 -B scripts/research_package.py --package research/schur-ranks-all-fields +python3.12 -B scripts/check_research_commit.py --package research/schur-ranks-all-fields --check-source-history +``` + +The verifier independently enumerates admissible sector subspaces and computes +their direct G G' image/quotient ranks, rather than deriving the oracle's minima +from the new pairing formula. The oracle and formula checks share the exact +prime-field arithmetic module; independence is at the algorithmic level. +It compares both formulas, constructs literal +commuting idempotent witnesses, and recomputes their Schur complements. Its +printed receipt records exact finite coverage, controls and a result digest. +The code supports only its declared bounded prime-field test domains; the proof +also covers extension fields and infinite fields. No predecessor executable is +imported and no network or Git is needed by the standalone verifier. + +Finite coverage: **886 triples, 303,878 admissible subspace pairs and 3,516 +literal witnesses**. Exhaustive domains are d=1 over F2/F3/F5 (2/12/80 +triples) and all 576 d=2 binary triples. The remaining domains are fixed +deterministic samples: 192 d=2 ternary triples and 24 d=3 binary triples, +including high-nullity and odd-rank cases. Eight controls reject omitted or +equated cross blocks, forced evenness, an incorrect minimum, a corrupted +witness, a wrong product block, a slope-one-only law and reordered products. +Gaussian-binomial counts check the complete subspace inventories. The verifier +checks the expected coverage and digest, including the predecessor's 576-triple / +2,496-witness binary census. Expected rows SHA256: +`c38f9ced06db3ecf1bc4c7f8802df7f1b3228f3435946700e7340b115d3156db`. +Each direct replay takes about 4.5 seconds on CPython 3.12.14, macOS arm64. +Timing is descriptive, not a performance claim. +Independent subagent derivations checked the proof and the odd-rank fixture; +this is AI-assisted review, not independent human or proof-kernel acceptance. + +## Scope, sources and contribution process + +The base is canonical main `721c03822c421b7f7fcbb2598993b947c4d88419`, priority +revision 8, selected conditional κ=0.003125804. [TASK.json](TASK.json) retains +the original `formal-interface-lemma` card with an explicit changed scope: +a released algebraic side question, not formalization or discharge of any of +the five selected-record assumptions. [SOURCES.json](SOURCES.json) binds exact +predecessor bytes as provenance. [VERIFY.json](VERIFY.json) registers bounded +normal and optimized checks with no external live inputs. + +Family-expansion decision: + +1. Exact sources are #6031 at `acc000f4edfa0b0c4a90b505c6e02a4c3572f74c` + and Krzysztof Wojt's #5128 at `2839d35e58b3285a1992a3ecbae2809ebef7661b`. + Both are merged archives; that status is not scientific acceptance. +2. Boundary: one common block deletion, invertible prescribed pivots, arbitrary + product block. Neither a physical header nor an implemented supplier follows. +3. The complete algebraic cost here is ambient dimension. Physical header + production/consumption, restoration, precision, stock, compiler and outer + costs remain unpriced, not free. There is no signed invoice or κ comparison. +4. The result settles the predecessor's open attainment question and decides + which rank/dimension requests are algebraically feasible before pricing. +5. Immediate pencil follow-ups to our #5672 were already covered by #5683, + #5689, #5692 and #5712. The active P104 correction line has distinct physical + obligations. This released question offered a bounded proof with a clear + stop rule; no further construction round is justified without a caller. + +The live #1166 handoff `discussioncomment-19230733` explicitly released #6031's +scope. Targeted all-state searches for Schur ranks and #6031 found no subsequent +extension at intake; recent board claims were inspected. Coverage is targeted, +not a census of arbitrary historical diffs or unpublished work. The [canonical progress update](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19232628) +records the preliminary local result and publication plan. Browser trouble +delayed the post; it is not described as an advance claim. + +## Open next questions + +Can an actual decoder/header caller use a point on this sharp frontier with a +favorable complete physical bill? First specify its exact A,B,H, desired rank, +allowed sector dimensions, and charged production/consumption/restoration +operations, then evaluate the theorem at that boundary. The missing caller and +cost contract are blockers; an algebraic minimum alone is not a saving. +The corresponding structured question is in [TASK.json](TASK.json). + +## Credit + +New proof and verifier prepared by **apoursh**, with substantial OpenAI Codex +assistance in derivation, implementation, independent subagent checking and +verification. Apache-2.0. Nick Petalas #6031 supplies the open questions, +sector-subspace cost reduction, lower bounds and binary census; Krzysztof Wojt +#5128 supplies the arbitrary-pivot maximal-rank theorem and realization. The +literal witness construction follows those credited predecessors. The ordered +Schur factorization is Nick Petalas #4597; sector/split methods retain ssafwann +#4657/#4671 and Nick Petalas #4746/#4771/#4774/#4785 attribution. Classical +bilinear rank normal form is used without a historical-priority claim. diff --git a/research/schur-ranks-all-fields/SOURCES.json b/research/schur-ranks-all-fields/SOURCES.json new file mode 100644 index 0000000000..0af5f8827a --- /dev/null +++ b/research/schur-ranks-all-fields/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/schur-intermediate-ranks/PROOF.md", + "usage": "provenance", + "git_blob": "234a86b25f24e5fe85b64ebef0c24ca39fff278e", + "sha256": "2c79b6beff2d2cce1f6d5c75230d63b4a980156ee32f8027c826a30b7f39030e" + }, + { + "path": "research/schur-intermediate-ranks/verify.py", + "usage": "provenance", + "git_blob": "58a2bb02d28b0d9b7a8b683a7f9a2c8247ad6142", + "sha256": "ad3cd5bc2fd712a4ac182946b4db0918f6f2fdb7795a6ef11e81ac1ee48d6748" + }, + { + "path": "research/arbitrary-pivot-schur-minimum/PROOF.md", + "usage": "provenance", + "git_blob": "c7d58883b4df5ddab4f237a521458b7f506b3617", + "sha256": "77118415edf74aa4b6a49c94cb735913ad08377802ab44f3f51f66531b46593a" + } + ] +} diff --git a/research/schur-ranks-all-fields/TASK.json b/research/schur-ranks-all-fields/TASK.json new file mode 100644 index 0000000000..605913a30a --- /dev/null +++ b/research/schur-ranks-all-fields/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "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": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Resolve PR6031 open questions 1 and 2: exact minimum dimension at every Schur-commutator rank over every field and d, and a closed formula for rho0.", + "scope_change_reason": "Handoff-first mathematical side question rather than proof-assistant formalization or discharge of a selected-record assumption. PR6031 proves the lower bound and checks equality only at d=2 over F2.", + "bottleneck_link": "Side result: exact rank/dimension trade-off for prescribed-pivot Schur deletion; no supplier invoice, selected assumption or kappa changes.", + "budget_minutes": 60, + "stop_rule": "Stop after the two scoped all-field proofs, independent derivation and bounded exact finite-field checks; do not expand to physical header construction or all-field exhaustive search.", + "outcome": "completed", + "evidence": "PROOF.md proves the exact minimum-dimension law over every field and d and the closed rho0 formula. Bounded independent sector-subspace enumeration and literal idempotent witnesses corroborate both formulas; see README and generated verifier receipt.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, independent subagent audit and verification.", + "open_questions": [ + { + "question": "Can an actual decoder/header caller use a point on this sharp frontier with a favorable complete physical bill?", + "why_it_matters": "The algebraic minimum alone does not improve a signed supplier invoice.", + "first_step": "Specify exact A,B,H, desired rank, allowed sector dimensions and all charged production/consumption/restoration operations; evaluate the frontier at that boundary.", + "blocked_by": "No concrete physical caller and complete cost contract are supplied by this algebraic side result." + } + ] +} diff --git a/research/schur-ranks-all-fields/VERIFY.json b/research/schur-ranks-all-fields/VERIFY.json new file mode 100644 index 0000000000..8cb92c874c --- /dev/null +++ b/research/schur-ranks-all-fields/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": "Exhaustive and sampled prime-field sector-subspace minima, closed rho0, literal idempotent Schur witnesses, coverage and mutation controls; finite corroboration only." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive and sampled prime-field sector-subspace minima, closed rho0, literal idempotent Schur witnesses, coverage and mutation controls; finite corroboration only." + } + ] +} diff --git a/research/schur-ranks-all-fields/algebra.py b/research/schur-ranks-all-fields/algebra.py new file mode 100644 index 0000000000..d9cb3ca6e3 --- /dev/null +++ b/research/schur-ranks-all-fields/algebra.py @@ -0,0 +1,206 @@ +"""Exact prime-field arithmetic for bounded corroboration, not all fields. + +apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Sector-factor construction credits Nick Petalas PR6031 and Krzysztof Wojt +PR5128, generalized here from the binary verifier. +""" +from functools import lru_cache +from itertools import product + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +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 transpose(a): + return [list(x) for x in zip(*a)] + + +def add(a, b, p, sign=1): + return [[(x + sign * y) % p for x, y in zip(r, s)] + for r, s in zip(a, b)] + + +def scale(a, c, p): + return [[c * x % p for x in r] for r in a] + + +def mul(a, b, p, columns=0): + cols = transpose(b) if b else [[] for _ in range(columns)] + return [[sum(x * y for x, y in zip(r, c)) % p for c in cols] + for r in a] + + +def apply(a, v, p): + return tuple(sum(x * y for x, y in zip(r, v)) % p for r in a) + + +def rref(a, p): + rows = [list(r) for r in a] + if not rows: + return (), () + pivots = [] + for j in range(len(rows[0])): + k = next((i for i in range(len(pivots), len(rows)) if rows[i][j]), None) + if k is None: + continue + q = len(pivots) + rows[q], rows[k] = rows[k], rows[q] + c = pow(rows[q][j], -1, p) + rows[q] = [c * x % p for x in rows[q]] + for i in range(len(rows)): + if i != q and rows[i][j]: + c = rows[i][j] + rows[i] = [(x - c * y) % p for x, y in zip(rows[i], rows[q])] + pivots.append(j) + return tuple(tuple(r) for r in rows[:len(pivots)]), tuple(pivots) + + +def rank(a, p): + return len(rref(a, p)[0]) + + +def inverse(a, p): + n = len(a) + rows, pivots = rref([list(r) + e for r, e in zip(a, eye(n))], p) + require(pivots[:n] == tuple(range(n)), "singular inverse") + return [list(r[n:]) for r in rows] + + +def kernel(a, p): + rows, pivots = rref(a, p) + n = len(a[0]) + out = [] + for j in range(n): + if j not in pivots: + v = [int(i == j) for i in range(n)] + for i, k in enumerate(pivots): + v[k] = -rows[i][j] % p + out.append(tuple(v)) + return tuple(out) + + +def image(a, p): + return rref(transpose(a), p)[0] + + +def extend(start, candidates, p): + chosen = [tuple(v) for v in start] + extra = [] + for v in candidates: + if rank(chosen + [tuple(v)], p) > len(chosen): + chosen.append(tuple(v)) + extra.append(tuple(v)) + return extra + + +def block(parts): + return [sum((a[i] for a in row), []) + for row in parts for i in range(len(row[0]))] + + +def sub(a, r0, r1, c0, c1): + return [r[c0:c1] for r in a[r0:r1]] + + +@lru_cache(None) +def subspaces(d, p): + vectors = tuple(product(range(p), repeat=d)) + spaces = {()} + frontier = {()} + for _ in range(d): + new = {rref(space + (v,), p)[0] for space in frontier for v in vectors} + frontier = new - spaces + spaces.update(new) + return tuple(sorted(spaces, key=lambda s: (len(s), s))) + + +@lru_cache(None) +def choices(t, p): + im, ker = image(t, p), kernel(t, p) + spaces = subspaces(len(t), p) + ich = tuple(s for s in spaces if rank(s + im, p) == len(s)) + nch = tuple(s for s in spaces if rank(s + ker, p) == len(ker)) + return ich, nch + + +def compressed(a, b, h, p): + return [add(add(add(eye(len(a)), a, p, -1), b, p, -1), h, p), + add(a, h, p, -1), add(b, h, p, -1), h] + + +def factor_maps(a, b, h, p): + d = len(a) + ai, bi = inverse(a, p), inverse(b, p) + bih, hbi = mul(bi, h, p), mul(h, bi, p) + z, i = zeros(d, d), eye(d) + g = block([[z, ai], [scale(bih, -1, p), scale(bi, -1, p)], + [add(i, bih, p, -1), add(ai, bi, p, -1)]]) + gp = block([[ai, scale(bi, -1, p), add(ai, bi, p, -1)], + [z, hbi, add(hbi, i, p, -1)]]) + return g, gp + + +def sector_factors(t, ij, nj, p): + """Minimal XY=t with image(X)=ij and kernel(Y)=nj; cited construction.""" + d = len(t) + sigma = image(t, p) + full = list(sigma) + extend(sigma, eye(d), p) + coordinates = mul(inverse(transpose(full), p), t, p) + phi = coordinates[:len(sigma)] + kb = extend(nj, kernel(t, p), p) + full = list(nj) + kb + full += extend(full, eye(d), p) + coords = inverse(transpose(full), p) + psi = coords[len(nj):len(nj) + len(kb)] + tau = extend(sigma, ij, p) + y = phi + psi + zeros(len(tau), d) + columns = list(sigma) + zeros(len(psi), d) + tau + x = transpose(columns) if columns else [[] for _ in range(d)] + require(mul(x, y, p, d) == t, "sector product") + require(rank(x, p) == len(ij) and d - rank(y, p) == len(nj), "sector ranks") + return x, y + + +def build_pair(a, b, h, ichoice, nchoice, p): + t = compressed(a, b, h, p) + select = [(image(t[0], p), kernel(t[0], p))] + list(zip(ichoice, nchoice)) + xs, ys, pd, qd = [], [], [], [] + for j, (tj, (ij, nj)) in enumerate(zip(t, select)): + x, y = sector_factors(tj, ij, nj, p) + xs.append(x) + ys.extend(y) + pd.extend([int(j in (1, 3))] * len(y)) + qd.extend([int(j in (2, 3))] * len(y)) + projection = [sum((x[i] for x in xs), []) for i in range(len(a))] + require(mul(projection, ys, p) == eye(len(a)), "split identity") + m = transpose(transpose(ys) + list(kernel(projection, p))) + mi = inverse(m, p) + pp = mul(mi, [[s * x % p for x in row] for s, row in zip(pd, m)], p) + qq = mul(mi, [[s * x % p for x in row] for s, row in zip(qd, m)], p) + return pp, qq + + +def literal_rank(a, b, h, pp, qq, p): + d, n = len(a), len(pp) + pq, qp = mul(pp, qq, p), mul(qq, pp, p) + require(mul(pp, pp, p) == pp and mul(qq, qq, p) == qq and pq == qp, + "not commuting idempotents") + require(sub(pp, 0, d, 0, d) == a and sub(qq, 0, d, 0, d) == b + and sub(pq, 0, d, 0, d) == h, "wrong prescribed blocks") + complements = [] + for matrix, pivot in ((pp, a), (qq, b)): + correction = mul(mul(sub(matrix, d, n, 0, d), inverse(pivot, p), p), + sub(matrix, 0, d, d, n), p) + complements.append(add(sub(matrix, d, n, d, n), correction, p, -1)) + s, z = complements + return rank(add(mul(s, z, p), mul(z, s, p), p, -1), p) diff --git a/research/schur-ranks-all-fields/oracle.py b/research/schur-ranks-all-fields/oracle.py new file mode 100644 index 0000000000..fe4eaa75f1 --- /dev/null +++ b/research/schur-ranks-all-fields/oracle.py @@ -0,0 +1,43 @@ +"""Direct G G' subspace enumeration; pairing law is not used for optimization. + +apoursh with substantial OpenAI Codex assistance; Apache-2.0. +The reduction and exhaustive sector-search approach credit Nick Petalas PR6031. +""" +from itertools import product + + +def install(algebra): + """Explicitly bind the already source-loaded arithmetic module.""" + globals()["la"] = algebra + + +def embed(j, v, d): + return tuple([0] * (j * d) + list(v) + [0] * ((2 - j) * d)) + + +def profile(a, b, h, p): + d = len(a) + ts = la.compressed(a, b, h, p) + g, gp = la.factor_maps(a, b, h, p) + m = la.mul(g, gp, p) + options = [la.choices(tuple(map(tuple, t)), p) for t in ts[1:]] + nchoices = [] + for ns in product(*(o[1] for o in options)): + nb = [embed(j, v, d) for j, space in enumerate(ns) for v in space] + nchoices.append((ns, nb)) + base = la.rank(ts[0], p) + sum(d - la.rank(t, p) for t in ts[1:]) + best, witnesses, pairs = {}, {}, 0 + for iss in product(*(o[0] for o in options)): + ib = [embed(j, v, d) for j, space in enumerate(iss) for v in space] + mi = [la.apply(m, v, p) for v in ib] + for ns, nb in nchoices: + rho = la.rank(mi + nb, p) - len(nb) + cost = base + len(ib) - len(nb) + pairs += 1 + if cost < best.get(rho, 10**9): + best[rho], witnesses[rho] = cost, (iss, ns) + zero = la.zeros(d, d) + tt = la.block([[ts[i + 1] if i == j else zero for j in range(3)] + for i in range(3)]) + rho0 = la.rank(la.mul(la.mul(tt, m, p), tt, p), p) + return ts, best, witnesses, rho0, pairs diff --git a/research/schur-ranks-all-fields/verify.py b/research/schur-ranks-all-fields/verify.py new file mode 100644 index 0000000000..d88d4bfaeb --- /dev/null +++ b/research/schur-ranks-all-fields/verify.py @@ -0,0 +1,191 @@ +#!/usr/bin/env python3 +"""Bounded exact corroboration of the all-field Schur rank/dimension law. + +Not a proof-kernel verification. No external inputs or dependencies. +apoursh with substantial OpenAI Codex assistance; Apache-2.0. +Predecessor factorization/construction: Krzysztof Wojt PR5128; sector search: +Nick Petalas PR6031. The all-field proof is separate in PROOF.md. +""" +import hashlib +import itertools +import json +from pathlib import Path +import random +import types + + +def source_module(name): + path = Path(__file__).with_name(name + ".py") + module = types.ModuleType(name) + exec(compile(path.read_bytes(), str(path), "exec"), module.__dict__) + return module + + +la = source_module("algebra") +oracle = source_module("oracle") +oracle.install(la) + + +def closed_rho0(a, b, h, p): + """Basis-free formula; the order of the three factors is essential.""" + _, f, j, _ = la.compressed(a, b, h, p) + first = la.mul(la.mul(j, la.inverse(a, p), p), f, p) + second = la.mul(la.mul(f, la.inverse(b, p), p), j, p) + return la.rank(first, p) + la.rank(second, p) + 2 * la.rank(h, p) - 2 * len(a) + + +def invariant(a, b, h, p): + d = len(a) + ts = la.compressed(a, b, h, p) + right = [la.kernel(t, p) for t in ts[1:]] + left = [la.kernel(la.transpose(t), p) for t in ts[1:]] + cross = [] + for i, j in ((0, 1), (1, 0)): + pairing = [[sum(x * y for x, y in zip(w, la.apply(h, z, p))) % p + for z in right[j]] for w in left[i]] + cross.append(la.rank(pairing, p)) + s, r = sum(map(len, right)), sum(cross) + rho0 = 2 * d - 2 * s + r + nmax = 3 * d + la.rank(ts[0], p) + s + law = {rho: nmax - (2 * d - rho) - min(2 * d - rho, r) + for rho in range(rho0, 2 * d + 1)} + return rho0, law, cross + + +def matrices(d, p): + return [[list(v[i:i + d]) for i in range(0, d * d, d)] + for v in itertools.product(range(p), repeat=d * d)] + + +def sampled_triples(d, p, count): + mats = matrices(d, p) + gl = [a for a in mats if la.rank(a, p) == d] + rng = random.Random(6031 + 100 * d + p) + picked = {} + def take(a, b, h): + key = tuple(tuple(tuple(row) for row in m) for m in (a, b, h)) + picked[key] = (a, b, h) + for a in gl[::max(1, len(gl) // 4)][:4]: + take(a, a, a) + take(a, a, la.zeros(d, d)) + take(a, la.eye(d), a) + if (d, p) == (2, 3): + take([[1, 0], [0, 2]], [[1, 1], [0, 1]], la.eye(2)) + while len(picked) < count: + take(rng.choice(gl), rng.choice(gl), rng.choice(mats)) + return list(picked.values()) + + +def cases(): + for d, p in ((1, 2), (1, 3), (1, 5), (2, 2)): + mats = matrices(d, p) + gl = [a for a in mats if la.rank(a, p) == d] + yield d, p, "exhaustive", list(itertools.product(gl, gl, mats)) + yield 2, 3, "deterministic sample", sampled_triples(2, 3, 192) + yield 3, 2, "deterministic sample", sampled_triples(3, 2, 24) + + +def check_case(a, b, h, p): + _, actual, witnesses, direct_rho0, pairs = oracle.profile(a, b, h, p) + rho0, predicted, cross = invariant(a, b, h, p) + la.require(rho0 == direct_rho0, "cross-block rho0 versus TMT") + la.require(closed_rho0(a, b, h, p) == direct_rho0, "ordered product rho0 versus TMT") + la.require(actual == predicted, "exact minimum dimension versus direct search") + for rho, (iss, ns) in witnesses.items(): + pp, qq = la.build_pair(a, b, h, iss, ns, p) + la.require(len(pp) == actual[rho], "wrong witness dimension") + la.require(la.literal_rank(a, b, h, pp, qq, p) == rho, "wrong witness rank") + row = {"A": a, "B": b, "H": h, "rho0": rho0, "cross_ranks": cross, + "profile": sorted(actual.items())} + return row, pairs, len(witnesses) + + +def rejects(operation): + try: + operation() + except ValueError: + return True + return False + + +def controls(): + a, b, h, p = [[1, 0], [0, 2]], [[1, 1], [0, 1]], la.eye(2), 3 + _, exact, wit, direct, _ = oracle.profile(a, b, h, p) + rho0, predicted, cross = invariant(a, b, h, p) + la.require(exact == {1: 5, 2: 6, 3: 7, 4: 9} and cross == [1, 0], "odd fixture") + tests = { + "omit_cross_pairing": rejects(lambda: la.require(rho0 - sum(cross) == direct, "omitted cross")), + "force_equal_cross_ranks": rejects(lambda: la.require(cross[0] == cross[1], "unequal cross")), + "force_even_rank": rejects(lambda: la.require(direct % 2 == 0, "odd rank")), + "wrong_minimum": rejects(lambda: la.require({**predicted, 2: 5} == exact, "wrong minimum")), + } + iss, ns = wit[1] + pp, qq = la.build_pair(a, b, h, iss, ns, p) + changed = [r[:] for r in pp] + changed[0][0] = (changed[0][0] + 1) % p + tests["changed_witness"] = rejects(lambda: la.literal_rank(a, b, h, changed, qq, p)) + tests["wrong_product_block"] = rejects(lambda: la.literal_rank(a, b, la.zeros(2, 2), pp, qq, p)) + _, slope, _, start, _ = oracle.profile(h, h, h, p) + slope_one = {rho: slope[start] + rho - start for rho in slope} + tests["slope_one_only"] = rejects(lambda: la.require(slope_one == slope, "slope two required")) + a = b = [[0, 1], [1, 0]] + h, p = [[0, 1], [1, 1]], 2 + _, f, j, _ = la.compressed(a, b, h, p) + wrong_first = la.mul(la.mul(la.inverse(a, p), j, p), f, p) + wrong_second = la.mul(la.mul(la.inverse(b, p), f, p), j, p) + wrong = la.rank(wrong_first, p) + la.rank(wrong_second, p) + 2 * la.rank(h, p) - 4 + _, _, _, direct, _ = oracle.profile(a, b, h, p) + la.require(closed_rho0(a, b, h, p) == direct == 0 and wrong == 2, "order fixture") + tests["commute_inverse_past_factor"] = rejects(lambda: la.require(wrong == direct, "ordered factors")) + la.require(all(tests.values()), "a mutation survived") + return tests + + +def check_subspace_inventory(): + """Gaussian-binomial dimension counts, independent of search results.""" + expected = {(1, 2): [1, 1], (1, 3): [1, 1], (1, 5): [1, 1], + (2, 2): [1, 3, 1], (2, 3): [1, 4, 1], (3, 2): [1, 7, 7, 1]} + for (d, p), counts in expected.items(): + actual = [sum(len(s) == k for s in la.subspaces(d, p)) for k in range(d + 1)] + la.require(actual == counts, "incomplete subspace inventory") + return {f"d{d}_F{p}": counts for (d, p), counts in expected.items()} + + +def check_coverage(coverage): + expected = [(1, 2, 2, 20, 6, 0, 0), (1, 3, 12, 66, 32, 0, 0), + (1, 5, 80, 260, 168, 0, 0), (2, 2, 576, 21690, 2496, 0, 288), + (2, 3, 192, 8326, 668, 6, 151), (3, 2, 24, 273516, 146, 6, 11)] + keys = ("d", "p", "triples", "subspace_pairs", "literal_witnesses", + "odd_rho0", "noncommuting_pivots") + la.require([tuple(row[k] for k in keys) for row in coverage] == expected, + "coverage differs from recorded fixture inventory") + + +def main(): + subspace_histograms = check_subspace_inventory() + rows, coverage = [], [] + for d, p, scope, triples in cases(): + pairs = witnesses = odd = noncommuting = 0 + for a, b, h in triples: + row, count, n = check_case(a, b, h, p) + pairs += count + witnesses += n + odd += row["rho0"] % 2 + noncommuting += la.mul(a, b, p) != la.mul(b, a, p) + rows.append({"d": d, "p": p, **row}) + coverage.append({"d": d, "p": p, "scope": scope, "triples": len(triples), + "subspace_pairs": pairs, "literal_witnesses": witnesses, + "odd_rho0": odd, "noncommuting_pivots": noncommuting}) + check_coverage(coverage) + summary = {"coverage": coverage, "controls": controls(), + "subspace_histograms": subspace_histograms, + "rows_sha256": hashlib.sha256(json.dumps(rows, sort_keys=True, + separators=(",", ":")).encode()).hexdigest()} + la.require(summary["rows_sha256"] == "c38f9ced06db3ecf1bc4c7f8802df7f1b3228f3435946700e7340b115d3156db", + "fixture result digest changed") + print(json.dumps(summary, sort_keys=True, indent=2)) + print("PASS_SCHUR_RANKS_ALL_FIELDS_BOUNDED_CHECKS") + + +if __name__ == "__main__": + main()