From 635db411fe7b455cf75028607f07d3744b614687 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 14:07:35 +0100 Subject: [PATCH] feat(research): prove the sharp H6 bivariate kernel rank --- research/h6-bivariate-rank/README.md | 236 +++++++++++ research/h6-bivariate-rank/RESULT.json | 508 ++++++++++++++++++++++++ research/h6-bivariate-rank/SOURCES.json | 30 ++ research/h6-bivariate-rank/TASK.json | 79 ++++ research/h6-bivariate-rank/VERIFY.json | 34 ++ research/h6-bivariate-rank/verify.py | 253 ++++++++++++ 6 files changed, 1140 insertions(+) create mode 100644 research/h6-bivariate-rank/README.md create mode 100644 research/h6-bivariate-rank/RESULT.json create mode 100644 research/h6-bivariate-rank/SOURCES.json create mode 100644 research/h6-bivariate-rank/TASK.json create mode 100644 research/h6-bivariate-rank/VERIFY.json create mode 100644 research/h6-bivariate-rank/verify.py diff --git a/research/h6-bivariate-rank/README.md b/research/h6-bivariate-rank/README.md new file mode 100644 index 0000000000..376bdfbeb4 --- /dev/null +++ b/research/h6-bivariate-rank/README.md @@ -0,0 +1,236 @@ +# Separate E8 inner products do not lower the H6 rank + +Claim type: scoped mathematical proof with an exact finite support certificate. +This contribution was produced by Nick Petalas. Apache-2.0. + +Over every characteristic-zero field, the canonical 28,800-port H6 root-product +block has minimum rank **800** among all fitting kernels that depend separately +on the two E8 inner products and are odd under simultaneous sign reversal. +The unique minimizer is the existing cubic + +```text +F(s,t) = ((s+t)^3 - 4(s+t))/48. +``` + +Ross Richardson's [PR3649](https://github.com/CrocSwap/integer-mult-bounds/pull/3649) +proved rank 800 for this cubic and sharp larger ranks for the other kernels +depending only on s+t. Its first open question asks about nonisotropic kernels. +The new result excludes an improvement throughout the larger six-dimensional +affine family below, including kernels without exchange symmetry. The existing +800-rank witness and E8 projector theorem are cited premises, not new claims +or re-verification deliverables. This does not optimize arbitrary nonisotropic +kernels, a physical supplier, or the full 30,960-port H6 matrix. + +## Exact domain + +Let E be the 240 signed E8 roots of ordinary norm two, with inner products in +D={-2,-1,0,1,2}. The canonical root-product ports are E x E modulo simultaneous +antipodes. Its representatives use the 120 first roots whose first nonzero +coordinate is positive and all 240 signed second roots. For ports +(a,b),(c,d), put s=a dot c and t=b dot d. +The kernel has entry F(s,t), with values in an arbitrary characteristic-zero +field K. Require + +```text +F(-s,-t) = -F(s,t), +F(2,2) = 1, +F(s,t) = 0 whenever s+t is even, except at (2,2) and (-2,-2). +``` + +Oddness forces F(-2,-2)=-1. That value belongs to the signed lift, not a +second diagonal of the canonical matrix. The other even entries are exactly +the forced off-diagonal zeros of the retained scalar fitting interface. +Odd s+t entries are unconstrained. There is no requirement F(s,t)=F(t,s), +F(s,t)=f(s+t), or any polynomial formula away from D x D. + +Modulo oddness, the fitting conditions are exactly the six evaluations + +```text +(s,t): (2,2) (2,0) (0,2) (2,-2) (1,1) (1,-1) +F(s,t): 1 0 0 0 0 0. +``` + +Every pair in D x D occurs on signed root products. The canonical orientation +and simultaneous oddness retain all these constraints. + +## Proof + +Use the five mutually orthogonal root-algebra projectors P_i in +[PR3649's proof](../h6-odd-gram-rank/PROOF.md), of ranks + +```text +(d0,d1,d2,d3,d4) = (1,8,35,112,84). +``` + +Their entries at root inner product s are + +```text +p0(s) = 1/240 +p1(s) = s/60 +p2(s) = s^2/24 - 1/48 +p3(s) = (1_{s=2} - 1_{s=-2})/2 - s/60 +p4(s) = (1_{s=2} + 1_{s=-2})/2 - s^2/24 + 1/60. +``` + +These five functions form a basis on D. Functions p1,p3 are odd; p0,p2,p4 +are even. Therefore every allowed odd F has a unique expansion + +```text +F(s,t) = sum lambda_ij p_i(s)p_j(t), +``` + +over the twelve pairs with exactly one odd index. On the signed product its +operator is the same sum of P_i tensor P_j, so its rank is exactly +sum_{lambda_ij != 0} d_i d_j. Simultaneous antipodal oddness expresses the +signed matrix as [[M,-M],[-M,M]], where M is the canonical matrix. In +characteristic zero this has rank rank(M), with twice M on its odd subspace. +Consequently the same rank formula holds on the 28,800 canonical ports. +The signed eigenvalues lambda_ij are twice the canonical eigenvalues. + +The twelve sector ranks, followed by all possible solutions after the four +sectors of rank at least 3920 are set to zero, are as follows. + +| Sector ij | Rank d_i d_j | Low-rank coefficient lambda_ij | +|---|---:|---| +| 01 | 8 | 14y-390 | +| 03 | 112 | 60-2y | +| 10 | 8 | 30-7x | +| 12 | 280 | x+30 | +| 14 | 672 | 30-x/2 | +| 21 | 280 | 90-2y | +| 23 | 3920 | 0 | +| 30 | 112 | x | +| 32 | 3920 | 0 | +| 34 | 9408 | 0 | +| 41 | 672 | y | +| 43 | 9408 | 0 | + +Here x,y range independently over K. To derive this table, substitute the +five p_i in the six evaluation equations and solve linearly. For an explicit +rank certificate, multiply the six-by-twelve coefficient matrix by 57600. +The minor on columns 01,03,10,12,21,30 has determinant -94371840000. +Thus those six columns are independent over every characteristic-zero field. +The displayed affine table satisfies all six equations and has free +coordinates lambda_30=x, lambda_41=y. It is therefore the complete low-sector +solution. The full six-by-twelve system also has rank six, so the entire +fitting family has affine dimension six. + +If any of the four omitted coefficients is nonzero, rank is at least 3920, +already larger than the cubic's 800. Otherwise split the rank sum into the +four x-dependent sectors 10,12,14,30 and the four y-dependent sectors +01,03,21,41. + +At x=60 the first group has rank 8+280+112=400. At every other x its +rank-672 coefficient 30-x/2 is nonzero, so this group's rank is at least +672, strictly greater than 400. At y=0 the second group has rank +8+112+280=400. At every other y its rank-672 coefficient y is nonzero, +so it too has rank strictly greater than 400. Hence the total minimum is +800, attained only at x=60,y=0. + +At these parameters the nonzero signed eigenvalues are + +```text +lambda_01=lambda_10=-390, +lambda_03=lambda_30=60, +lambda_12=lambda_21=90. +``` + +Substitution into the p_i expansion gives the cubic on every point of +D x D. It satisfies all fitting conditions and has rank 800. This proves +both attainment and uniqueness. QED. + +## Exact evidence and reproduction + +[verify.py](verify.py) implements the new optimization using only rational +arithmetic and the standard library. It does not import or run a predecessor +verifier. The written proof uses PR3649's root projectors and ranks as cited +mathematical premises. + +The checker enumerates every one of the 4096 sector supports. For each, it +compares the rational ranks of the restricted six-equation coefficient matrix +and its augmentation. Exactly 1764 supports permit a fitting solution. This +counts permitted supports, which may contain zero coefficients; it does not +claim that all those supports occur exactly. The unique least-cost permitted +support is the six cubic sectors, cost 800, and its coefficients are unique. +Rational solvability is equivalent to solvability over any characteristic-zero +extension field because these matrices have rational entries. + +Separately, the checker certifies the two-parameter table by affine identities +and matrix ranks, checks every possible one-parameter zero stratum and one +generic stratum, checks all 25 cubic values, and verifies 300 basis-parity +identities. Thirteen controls reject a cheaper nonfitting kernel, six omitted +minimum sectors, an asymmetric redistribution with the same diagonal, +infeasible cheap/empty supports, and three invalid matrix shapes. The generated +[RESULT.json](RESULT.json) binds the other five package files by SHA256. +Normal verification writes no files and checks remain active under -O. + +From the repository root, with CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/h6-bivariate-rank/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/h6-bivariate-rank/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/h6-bivariate-rank +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/h6-bivariate-rank --check-source-history +``` + +Any CPython 3.12 installation can replace that local path. The scientific +marker is `PASS_H6_BIVARIATE_RANK minimum=800 unique=cubic supports=4096`. +The standalone verifier also works in a Git-free export containing all six +package files. `--emit-to NEW_EXTERNAL_FILE` exclusively creates a regenerated +receipt outside the checkout. + +## Scope, provenance and limitations + +Canonical base ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c, priority revision 7. +The complex-rank-shape-decoder card is changed to this algebraic side result +from PR3649's open nonisotropic-kernel question. The first control was its +rank-800 cubic. The selected-source metadata baseline passed as orientation +only. The selected result and its frontier are unchanged. + +[SOURCES.json](SOURCES.json) pins exact predecessor proof/README bytes and +catalogue/selected-record provenance in ancestral main history. Those sources +are cited historical premises, not runtime inputs or rechecked scientific +results. The novel step is the minimum and equality theorem for the larger +bivariate family. Live PRs, handoffs, recent account work, local reservations, +main-tree and merged-PR term searches found no matching claim. The cached +overlap snapshot covered 341 open PRs and 4444 Discussion records; sparse local +coverage was incomplete. No exhaustive novelty or literature-priority claim +follows. + +The theorem assumes characteristic zero, simultaneous oddness, dependence only +on s,t, the fixed root-product ports and the retained fitting zeros. It gives +no rank bound for arbitrary coordinate-dependent kernels, operator-valued +factors, changed geometry, nonodd kernels or positive characteristic. Its +800 is the root-product rank, not the full H6 kernel rank or a physical +helper count. Scalar factorization rank does not price reuse, partial-frame +visits, copies, compensation or restoration. Those costs, physical/native +realization, hosting, stock, precision/tapes, compiler and complete outer +transfer remain unpriced. No supplier, new kappa, selected cold replay, +Lean or Docker result is claimed. Independent human and formal proof-kernel +review are unclaimed. + +The checker has no recursion, subprocesses or dynamic code generation. Its +4096 support iterations use at most 25-by-13 rational elimination matrices. +Each function is below 60 lines. CPython managed allocation is the documented +deviation from fixed preallocation; collection sizes and all loops are bounded +by these fixed domains. Registered commands treat warnings as errors. + +## Open next questions + +Can a kernel that distinguishes root pairs with the same (s,t) reduce the +root-product rank? This would escape the exact obstruction proved here. +Start with one explicit coordinate-dependent orbit refinement and its full +fitting constraints. The present tensor-projector diagonalization no longer +applies, and no such fitting kernel or complete physical cost is supplied. +The structured question and remaining obligations are in [TASK.json](TASK.json). + +## Credit + +Credit Ross Richardson for PR3649's projectors, rank formula, cubic witness, +odd-Gram classification and open nonisotropic-kernel question, and for +PR1830's H6 compensation/encoder and spectral context. Credit Dominik Scholz +for PR606's E8 geometry/factorization and DreamingOfClouds for the H6/Walsh +proposal. The retained predecessor notices and earlier source lineage remain +unchanged. The new theorem is the exact bivariate minimum and its unique +optimizer. No priority is claimed for tensor-product projector algebra or +linear-system support optimization. diff --git a/research/h6-bivariate-rank/RESULT.json b/research/h6-bivariate-rank/RESULT.json new file mode 100644 index 0000000000..d67cca5362 --- /dev/null +++ b/research/h6-bivariate-rank/RESULT.json @@ -0,0 +1,508 @@ +{ + "claim_type": "scoped proof with exact finite support certificate", + "constraint_rank": 6, + "cubic_entries": 25, + "entry_basis_rank": 12, + "feasible_cost_histogram": { + "10096": 2, + "10200": 2, + "10208": 2, + "10320": 2, + "10488": 6, + "10592": 6, + "10600": 6, + "10656": 2, + "10760": 6, + "10768": 6, + "10864": 2, + "10872": 6, + "10880": 6, + "10984": 2, + "10992": 2, + "11048": 2, + "11152": 6, + "11160": 6, + "11256": 2, + "11264": 6, + "11272": 4, + "11320": 2, + "11328": 2, + "11424": 2, + "11432": 6, + "11440": 4, + "11536": 2, + "11544": 4, + "11552": 2, + "1192": 2, + "13568": 2, + "1360": 2, + "13736": 6, + "13840": 6, + "13848": 6, + "13904": 2, + "14008": 6, + "14016": 6, + "14112": 2, + "14120": 6, + "14128": 10, + "14232": 6, + "14240": 6, + "14296": 6, + "14400": 20, + "14408": 20, + "14504": 6, + "14512": 20, + "14520": 14, + "14568": 6, + "14576": 6, + "1464": 2, + "14672": 6, + "14680": 20, + "14688": 16, + "1472": 2, + "14784": 6, + "14792": 20, + "14800": 14, + "14896": 2, + "14904": 6, + "14912": 4, + "14960": 6, + "14968": 6, + "15064": 6, + "15072": 20, + "15080": 14, + "15176": 6, + "15184": 14, + "15192": 8, + "15232": 2, + "15240": 6, + "15248": 4, + "15344": 6, + "15352": 14, + "15360": 8, + "15456": 4, + "15464": 8, + "15472": 4, + "1584": 1, + "17376": 2, + "17480": 2, + "17488": 2, + "1752": 2, + "17544": 2, + "17648": 6, + "17656": 6, + "17752": 2, + "17760": 6, + "17768": 4, + "17816": 2, + "17824": 2, + "17920": 2, + "17928": 6, + "17936": 6, + "18032": 2, + "18040": 10, + "18048": 8, + "18144": 2, + "18152": 6, + "18160": 4, + "18208": 6, + "18216": 6, + "18312": 6, + "18320": 20, + "18328": 14, + "18424": 6, + "18432": 14, + "18440": 8, + "18480": 2, + "18488": 6, + "18496": 4, + "1856": 2, + "18592": 6, + "18600": 16, + "18608": 10, + "1864": 2, + "18704": 6, + "18712": 14, + "18720": 8, + "18816": 2, + "18824": 4, + "18832": 2, + "18872": 2, + "18880": 6, + "18888": 4, + "18984": 6, + "18992": 14, + "19000": 8, + "19056": 1, + "19096": 4, + "19104": 8, + "19112": 4, + "19152": 2, + "19160": 4, + "19168": 2, + "1920": 1, + "19224": 2, + "19264": 4, + "19272": 8, + "19280": 4, + "19328": 2, + "19336": 2, + "19376": 2, + "19384": 4, + "19392": 3, + "19496": 2, + "19504": 2, + "19600": 1, + "19608": 2, + "19616": 3, + "19720": 2, + "19728": 2, + "19784": 2, + "19888": 6, + "19896": 6, + "19992": 2, + "20000": 6, + "20008": 4, + "20056": 2, + "20064": 2, + "20160": 2, + "20168": 6, + "20176": 5, + "2024": 2, + "20272": 2, + "20280": 6, + "20288": 4, + "2032": 2, + "20384": 1, + "20392": 2, + "20400": 1, + "20448": 2, + "20456": 2, + "20552": 2, + "20560": 6, + "20568": 4, + "20664": 2, + "20672": 4, + "20680": 2, + "20720": 1, + "20728": 2, + "20736": 1, + "20832": 2, + "20840": 4, + "20848": 2, + "20944": 1, + "20952": 2, + "20960": 1, + "2128": 1, + "2136": 2, + "2144": 1, + "22864": 2, + "22968": 2, + "22976": 2, + "23032": 2, + "23136": 6, + "23144": 6, + "23240": 2, + "23248": 6, + "23256": 4, + "23304": 2, + "23312": 2, + "23408": 2, + "23416": 6, + "23424": 6, + "23520": 2, + "23528": 10, + "23536": 8, + "23632": 2, + "23640": 6, + "23648": 4, + "23696": 6, + "23704": 6, + "23800": 6, + "23808": 20, + "23816": 14, + "23912": 6, + "23920": 14, + "23928": 8, + "23968": 2, + "23976": 6, + "23984": 4, + "24080": 6, + "24088": 16, + "24096": 10, + "24192": 6, + "24200": 14, + "24208": 8, + "24304": 2, + "24312": 4, + "24320": 2, + "24360": 2, + "24368": 6, + "24376": 4, + "24472": 6, + "24480": 14, + "24488": 8, + "24584": 4, + "24592": 8, + "24600": 4, + "24640": 2, + "24648": 4, + "24656": 2, + "24752": 4, + "24760": 8, + "24768": 4, + "24864": 2, + "24872": 4, + "24880": 2, + "26672": 1, + "26776": 2, + "26784": 2, + "26880": 1, + "26888": 2, + "26896": 1, + "26944": 2, + "26952": 2, + "27048": 2, + "27056": 6, + "27064": 4, + "27160": 2, + "27168": 4, + "27176": 2, + "27216": 1, + "27224": 2, + "27232": 1, + "27328": 2, + "27336": 6, + "27344": 4, + "27440": 3, + "27448": 8, + "27456": 5, + "27552": 2, + "27560": 4, + "27568": 2, + "27608": 2, + "27616": 6, + "27624": 4, + "27720": 6, + "27728": 14, + "27736": 8, + "27832": 4, + "27840": 8, + "27848": 4, + "27888": 2, + "27896": 4, + "27904": 2, + "28000": 5, + "28008": 10, + "28016": 5, + "28112": 4, + "28120": 8, + "28128": 4, + "28224": 1, + "28232": 2, + "28240": 1, + "28280": 2, + "28288": 4, + "28296": 2, + "28392": 4, + "28400": 8, + "28408": 4, + "28504": 2, + "28512": 4, + "28520": 2, + "28560": 1, + "28568": 2, + "28576": 1, + "28672": 2, + "28680": 4, + "28688": 2, + "28784": 1, + "28792": 2, + "28800": 1, + "4440": 2, + "4608": 2, + "4712": 2, + "4720": 2, + "4832": 2, + "5000": 6, + "5104": 6, + "5112": 6, + "5168": 2, + "5272": 6, + "5280": 6, + "5376": 2, + "5384": 6, + "5392": 6, + "5496": 2, + "5504": 2, + "5560": 2, + "5664": 6, + "5672": 6, + "5768": 2, + "5776": 6, + "5784": 4, + "5832": 2, + "5840": 2, + "5936": 2, + "5944": 6, + "5952": 4, + "6048": 2, + "6056": 4, + "6064": 2, + "800": 1, + "8080": 1, + "8248": 2, + "8352": 2, + "8360": 2, + "8416": 1, + "8520": 2, + "8528": 2, + "8624": 1, + "8632": 2, + "8640": 3, + "8744": 2, + "8752": 2, + "8808": 2, + "8912": 6, + "8920": 6, + "9016": 2, + "9024": 6, + "9032": 4, + "9080": 2, + "9088": 2, + "9184": 2, + "9192": 6, + "9200": 5, + "9296": 2, + "9304": 6, + "9312": 4, + "9408": 1, + "9416": 2, + "9424": 1, + "9472": 2, + "9480": 2, + "9576": 2, + "9584": 6, + "9592": 4, + "9688": 2, + "9696": 4, + "9704": 2, + "9744": 1, + "9752": 2, + "9760": 1, + "9856": 2, + "9864": 4, + "9872": 2, + "9928": 2, + "9968": 1, + "9976": 2, + "9984": 1 + }, + "feasible_supports": 1764, + "low_family_dimension": 2, + "minimum_rank": 800, + "minimum_signed_eigenvalues": [ + -390, + 60, + -390, + 90, + 0, + 90, + 0, + 60, + 0, + 0, + 0, + 0 + ], + "parity_checks": 300, + "rejection_controls": 13, + "scaled_minor_determinant": -94371840000, + "sector_ranks": [ + 8, + 112, + 8, + 280, + 672, + 280, + 3920, + 112, + 3920, + 9408, + 672, + 9408 + ], + "sectors": [ + [ + 0, + 1 + ], + [ + 0, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 1, + 4 + ], + [ + 2, + 1 + ], + [ + 2, + 3 + ], + [ + 3, + 0 + ], + [ + 3, + 2 + ], + [ + 3, + 4 + ], + [ + 4, + 1 + ], + [ + 4, + 3 + ] + ], + "sha256": { + "README.md": "0207eb5f8fe808644655c091f5165295f3f0897ac9a50ff96ff96ea0afdb986d", + "SOURCES.json": "fa077b2e0493f287fae4b87e580e53902fdf51f22094a79ffc486d048b7e7721", + "TASK.json": "66c6e90e4de87971c6019c2c89ed021397f7ead8c2101a0ef7b4e372775939dd", + "VERIFY.json": "e4db7b7a6f9fd2f386ec3137ea08b9664fceefca7350ccb177e66e81e1fce934", + "verify.py": "c5428ad6ebdcafe8151927ff2d6c32f3334097daed0118453c01691449e1d688" + }, + "supports_checked": 4096, + "unique_minimum_support": 175, + "x_stratum_ranks": [ + 960, + 792, + 1064, + 400, + 1072 + ], + "y_stratum_ranks": [ + 400, + 960, + 792, + 1064, + 1072 + ] +} diff --git a/research/h6-bivariate-rank/SOURCES.json b/research/h6-bivariate-rank/SOURCES.json new file mode 100644 index 0000000000..bd633fd317 --- /dev/null +++ b/research/h6-bivariate-rank/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/h6-odd-gram-rank/PROOF.md", + "usage": "provenance", + "git_blob": "76836a7b3b7b27c985685549d9768ce91ec5d6fc", + "sha256": "00525fedbe8a5fe3173fb0966313540bb197f930c90cd968589475c43a527035" + }, + { + "path": "research/h6-odd-gram-rank/README.md", + "usage": "provenance", + "git_blob": "618b403aefde85ddd213f10313b01b3532d6ec3c", + "sha256": "2b23ddceb742f1d7bdf5c4a3a3bee047fe6739ab55982ba82842f0ad1e385f23" + } + ] +} diff --git a/research/h6-bivariate-rank/TASK.json b/research/h6-bivariate-rank/TASK.json new file mode 100644 index 0000000000..a9caa8cc3e --- /dev/null +++ b/research/h6-bivariate-rank/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact minimum rank 800 and unique cubic optimizer for all characteristic-zero bivariate simultaneous-odd fitting kernels on the canonical 28800 H6 E8 root-product ports.", + "scope_change_reason": "Handoff-first selection of the explicitly open nonisotropic-kernel question in Ross Richardson PR3649. This is an exact scalar rank obstruction in a larger six-dimensional affine kernel family, not a physical decoder profile or a replay of the isotropic rank theorem.", + "bottleneck_link": "Algebraic side result: separate dependence on the two root inner products cannot lower the scalar factorization rank below the existing 800. Lower rank would require leaving this bivariate simultaneous-odd family; physical factor and compensation costs remain unpriced.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact minimum and equality result. Do not extend to coordinate-dependent kernels, full-shell ranks or physical construction.", + "outcome": "completed", + "evidence": "Written characteristic-zero proof; complete rational feasibility of all 4096 sector supports, 1764 feasible permitted supports, unique minimum rank 800; six-equation minor and affine identities; 25 cubic entries, 300 parity checks and 13 controls. Normal/optimized registered and direct replay are the verification contract.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a kernel distinguishing root pairs with the same two inner products lower the H6 root-product rank?", + "why_it_matters": "Such a kernel would escape the exact minimum-rank obstruction established here.", + "first_step": "Specify one coordinate-dependent orbit refinement, write every retained fitting constraint and seek a lower-rank exact kernel.", + "blocked_by": "The present tensor-projector diagonalization no longer applies; no coordinate-dependent fitting kernel or complete physical invoice is supplied." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146117", + "scientific_base": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "predecessor_pr": 3649, + "predecessor_head": "f8768756d8ac4abb263295170a436ba54562fdcd", + "overlap_limitations": "341 open PRs and 4444 Discussion records in complete cached pagination; live claims and main/merged term searches checked separately. Sparse local-note coverage and unpublished work are not complete." + } +} diff --git a/research/h6-bivariate-rank/VERIFY.json b/research/h6-bivariate-rank/VERIFY.json new file mode 100644 index 0000000000..b832e6fd51 --- /dev/null +++ b/research/h6-bivariate-rank/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": "Exact bivariate rank minimum and uniqueness, all 4096 support feasibility systems, affine/minor certificate, full value table, parity identities and rejection controls; source-hash receipt equality." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact bivariate rank minimum and uniqueness, all 4096 support feasibility systems, affine/minor certificate, full value table, parity identities and rejection controls; source-hash receipt equality." + } + ] +} diff --git a/research/h6-bivariate-rank/verify.py b/research/h6-bivariate-rank/verify.py new file mode 100644 index 0000000000..a7b7aebb22 --- /dev/null +++ b/research/h6-bivariate-rank/verify.py @@ -0,0 +1,253 @@ +#!/usr/bin/env python3 +"""Exact support certificate for the H6 bivariate fitting-kernel theorem. + +Produced by Nick Petalas. Apache-2.0. +The five E8 projectors and their ranks are cited from Ross Richardson PR3649. +This program proves the new finite support optimization, not those premises. +""" + +import argparse +import hashlib +import json +from collections import Counter +from fractions import Fraction as Q +from itertools import product +from pathlib import Path + +HERE = Path(__file__).resolve().parent +RANKS = (1, 8, 35, 112, 84) +SECTORS = tuple((i, j) for i, j in product(range(5), repeat=2) + if (i in (1, 3)) != (j in (1, 3))) +WEIGHTS = tuple(RANKS[i] * RANKS[j] for i, j in SECTORS) +CONSTRAINTS = ((2, 2), (2, 0), (0, 2), (2, -2), (1, 1), (1, -1)) +TARGET = (1, 0, 0, 0, 0, 0) +CUBIC = (-390, 60, -390, 90, 0, 90, 0, 60, 0, 0, 0, 0) +SOURCE_FILES = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def projector(i, s): + """Entry of the cited projector on roots of ordinary inner product s.""" + return (Q(1, 240), Q(s, 60), Q(s * s, 24) - Q(1, 48), + Q(int(s == 2) - int(s == -2), 2) - Q(s, 60), + Q(int(abs(s) == 2), 2) - Q(s * s, 24) + Q(1, 60))[i] + + +def entry(coefficients, s, t): + return sum(value * projector(i, s) * projector(j, t) + for value, (i, j) in zip(coefficients, SECTORS, strict=True)) + + +def matrix_rank(rows): + """Bounded rational elimination, at most 25 rows and 13 columns.""" + require(len(rows) <= 25, "too many rows") + width = len(rows[0]) if rows else 0 + require(width <= 13 and all(len(row) == width for row in rows), "bad row shape") + work = [[Q(value) for value in row] for row in rows] + rank = 0 + for column in range(width): + pivot = next((r for r in range(rank, len(work)) if work[r][column]), None) + if pivot is None: + continue + work[rank], work[pivot] = work[pivot], work[rank] + divisor = work[rank][column] + work[rank] = [value / divisor for value in work[rank]] + for row in range(rank + 1, len(work)): + factor = work[row][column] + if factor: + work[row] = [x - factor * y + for x, y in zip(work[row], work[rank], strict=True)] + rank += 1 + if rank == len(work): + break + return rank + + +def constraint_matrix(): + return [[projector(i, s) * projector(j, t) for i, j in SECTORS] + for s, t in CONSTRAINTS] + + +def feasible(matrix, target, active): + restricted = [[row[j] for j in active] for row in matrix] + augmented = [row + [Q(value)] + for row, value in zip(restricted, target, strict=True)] + return matrix_rank(restricted) == matrix_rank(augmented) + + +def determinant(rows): + require(len(rows) == 6 and all(len(row) == 6 for row in rows), + "expected six-square") + work = [[Q(value) for value in row] for row in rows] + result = Q(1) + for column in range(6): + pivot = next((r for r in range(column, 6) if work[r][column]), None) + if pivot is None: + return Q(0) + if pivot != column: + work[column], work[pivot] = work[pivot], work[column] + result = -result + value = work[column][column] + result *= value + for row in range(column + 1, 6): + factor = work[row][column] / value + work[row] = [a - factor * b + for a, b in zip(work[row], work[column], strict=True)] + return result + + +def support_optimization(matrix): + histogram = Counter() + optimum = sum(WEIGHTS) + 1 + winners = [] + feasible_count = 0 + for mask in range(1 << len(SECTORS)): + active = tuple(j for j in range(len(SECTORS)) if mask >> j & 1) + if not feasible(matrix, TARGET, active): + continue + feasible_count += 1 + cost = sum(WEIGHTS[j] for j in active) + histogram[cost] += 1 + if cost < optimum: + optimum, winners = cost, [mask] + elif cost == optimum: + winners.append(mask) + cubic_mask = sum(1 << j for j, value in enumerate(CUBIC) if value) + require(optimum == 800 and winners == [cubic_mask], "rank optimum/support differs") + active = tuple(j for j, value in enumerate(CUBIC) if value) + require(matrix_rank([[row[j] for j in active] for row in matrix]) == len(active), + "minimum support does not determine a unique kernel") + return {"supports_checked": 4096, "feasible_supports": feasible_count, + "minimum_rank": optimum, "unique_minimum_support": cubic_mask, + "feasible_cost_histogram": {str(cost): count + for cost, count in sorted(histogram.items())}} + + +def low_family(x, y): + """All solutions after excluding the four sectors of weight at least 3920.""" + return (14 * y - 390, 60 - 2 * y, 30 - 7 * x, x + 30, + 30 - x / 2, 90 - 2 * y, 0, x, 0, 0, y, 0) + + +def analytic_certificate(matrix): + low = tuple(j for j, weight in enumerate(WEIGHTS) if weight < 3920) + require(len(low) == 8 and matrix_rank(matrix) == 6, "constraint rank differs") + require(matrix_rank([[row[j] for j in low] for row in matrix]) == 6, + "low-family dimension differs") + minor = [[57600 * row[j] for j in (0, 1, 2, 3, 5, 7)] for row in matrix] + require(determinant(minor) == -94371840000, "displayed minor differs") + # Affine identities at zero and two independent directions prove every x,y. + for x, y in ((Q(0), Q(0)), (Q(1), Q(0)), (Q(0), Q(1))): + values = low_family(x, y) + require(tuple(entry(values, s, t) for s, t in CONSTRAINTS) == TARGET, + "affine family violates fitting") + require(low_family(Q(60), Q(0)) == CUBIC, "cubic parameter differs") + x_values = (Q(0), Q(-30), Q(30, 7), Q(60), Q(1)) + y_values = (Q(0), Q(30), Q(45), Q(195, 7), Q(1)) + # All possible zero collisions, plus one generic stratum, in each parameter. + x_costs = [sum(WEIGHTS[j] for j in (2, 3, 4, 7) if low_family(x, Q(0))[j]) + for x in x_values] + y_costs = [sum(WEIGHTS[j] for j in (0, 1, 5, 10) if low_family(Q(60), y)[j]) + for y in y_values] + require(min(x_costs) == min(y_costs) == 400, "one-parameter minimum differs") + require(x_costs.count(400) == y_costs.count(400) == 1, "minimum not unique") + return {"constraint_rank": 6, "low_family_dimension": 2, + "scaled_minor_determinant": -94371840000, + "x_stratum_ranks": x_costs, "y_stratum_ranks": y_costs} + + +def value_checks(): + values = (-2, -1, 0, 1, 2) + transform = [[projector(i, s) * projector(j, t) for i, j in SECTORS] + for s, t in product(values, repeat=2)] + require(matrix_rank(transform) == 12, "tensor entries do not span the odd family") + parity_checks = 0 + for k in range(12): + vector = tuple(int(j == k) for j in range(12)) + for s, t in product(values, repeat=2): + require(entry(vector, -s, -t) == -entry(vector, s, t), "wrong parity") + parity_checks += 1 + for s, t in product(values, repeat=2): + require(entry(CUBIC, s, t) == Q((s + t)**3 - 4 * (s + t), 48), + "minimum kernel is not the inherited cubic") + if (s + t) % 2 == 0: + expected = 1 if (s, t) == (2, 2) else -1 if (s, t) == (-2, -2) else 0 + require(entry(CUBIC, s, t) == expected, "cubic fitting failure") + return {"entry_basis_rank": 12, "parity_checks": parity_checks, "cubic_entries": 25} + + +def controls(matrix): + # A rank-eight projector is cheaper but fails the required zero at (0,2). + cheap = [Q(0)] * 12 + cheap[0] = Q(1) / (projector(0, 2) * projector(1, 2)) + require(entry(cheap, 2, 2) == 1 and entry(cheap, 2, 0) == 0 + and entry(cheap, 0, 2) != 0, "cheap nonfitting control ineffective") + for j, value in enumerate(CUBIC): + if not value: + continue + mutant = list(CUBIC) + mutant[j] = 0 + require(tuple(entry(mutant, s, t) for s, t in CONSTRAINTS) != TARGET, + "omitted minimum sector was accepted") + swapped = list(CUBIC) + swapped[0], swapped[2] = 0, -780 + require(entry(swapped, 2, 2) == 1 + and tuple(entry(swapped, s, t) for s, t in CONSTRAINTS) != TARGET, + "nonsymmetric factor-weight control ineffective") + require(not feasible(matrix, TARGET, (0,)), "rank-eight support incorrectly fits") + require(not feasible(matrix, TARGET, ()), "zero support incorrectly fits") + for malformed in ([[0] * 14], [[1], []], [[0]] * 26): + try: + matrix_rank(malformed) + except ValueError: + continue + raise ValueError("invalid matrix shape accepted") + return 13 + + +def compute_receipt(): + matrix = constraint_matrix() + result = {"claim_type": "scoped proof with exact finite support certificate", + "sectors": [list(pair) for pair in SECTORS], + "sector_ranks": list(WEIGHTS), + "minimum_signed_eigenvalues": list(CUBIC)} + result.update(value_checks()) + result.update(analytic_certificate(matrix)) + result.update(support_optimization(matrix)) + result["rejection_controls"] = controls(matrix) + result["sha256"] = {name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() + for name in SOURCE_FILES} + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-to", type=Path, + help="exclusively create an external receipt") + args = parser.parse_args() + result = compute_receipt() + if args.emit_to is not None: + output = args.emit_to.resolve() + require(not output.is_relative_to(HERE.parents[1]), + "receipt output must be external") + payload = json.dumps(result, indent=2, sort_keys=True) + "\n" + with output.open("x", encoding="utf-8") as stream: + require(stream.write(payload) == len(payload), "incomplete receipt write") + else: + receipt_path = HERE / "RESULT.json" + require(receipt_path.stat().st_size <= 1024 * 1024, + "receipt exceeds size bound") + expected = json.loads(receipt_path.read_text(encoding="utf-8")) + require(json.dumps(result, sort_keys=True) == + json.dumps(expected, sort_keys=True), + "generated receipt differs") + print("PASS_H6_BIVARIATE_RANK minimum=800 unique=cubic supports=4096") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()