diff --git a/research/full-mask-separated-excess/PROOF.md b/research/full-mask-separated-excess/PROOF.md new file mode 100644 index 0000000000..6cd9f7563c --- /dev/null +++ b/research/full-mask-separated-excess/PROOF.md @@ -0,0 +1,101 @@ +# Full-mask attainment with separated-port excess + +This is a scoped algebraic proof over every field. The finite checks corroborate +the new constructions. No physical tariff or multiplication theorem is proved. + +## Contract and credited premises + +Use the 112 ports, matching and strict ordered mask of Sagar Thakrar's +PR2484, retained in `paired-plane-block-rank`. If port i lies in plane E_i, +a fitting matrix has diagonal block I_(n_i), and its ordered (i,j) block is +zero for i != j unless E_i and E_j are orthogonal. Permitted rectangular +blocks are arbitrary. They need not be symmetric or commute. + +The credited premises are: + +1. PR2484's 49 supports partition the ports, and distinct ports within a + support are permitted pairs. +2. Its 22-plane set Q is pairwise nonorthogonal and nonorthogonal to the + five planes C=(13,23,35,16,34). The induced permitted graph on C is C5. + Both ports within a plane have forced off-diagonal zeros. +3. The all-field C5 block lemma in `paired-plane-block-rank` gives rank at + least 5d when each cycle plane has total width 2d. + +These are predecessor results, cited as dependencies. This package does not +claim to discover their geometry, partition or uniform rank 49d, and does +not replay their verification suites. Source bytes and proofs are pinned. +Tekalign's PR3362 extends the C5 lower bound to unequal widths and explicitly +leaves full unequal-mask attainment open. We settle one restricted family. + +## Theorem + +Let T be the 44 ports in the planes of Q. Choose an integer d>=1 and +arbitrary integers e_p>=0 for p in T. Set + + n_p = d+e_p for p in T, and n_p=d otherwise. + E = sum_(p in T) e_p. + +The exact minimum rank of a fitting matrix on the complete 112-port mask is + + 49d + E. + +Equivalently this is the exact minimum intermediate field-coordinate +dimension for a linear factorization M=A B of such a fitting matrix. +This is a full-mask result for this family, not just a principal-mask bound. + +## Lower bound + +Restrict any fitting matrix to the 44 Q ports and the ten C ports. All +ordered cross blocks between those two sets vanish. The Q part is the +identity of dimension 44d+E. The cycle part, grouping the two ports within +each plane, has five diagonal blocks I_(2d) and forbidden nonneighbor +blocks. The credited C5 lemma bounds its rank below by 5d over every field. +The principal submatrix therefore has rank at least 49d+E, as does the +full matrix. This applies to all arbitrary ordered free blocks. + +## Attaining construction + +No two distinct Q ports can occur in the same partition support: Q ports +are mutually forbidden, whereas each support consists of permitted pairs. +Thus exactly 44 of the 49 supports contain a Q port, each containing one. + +For each support S allocate a query vector of dimension + + c_S = max_(p in S) n_p. + +At port p in S, embed its n_p coordinates as the first n_p coordinates +of this vector. Sum these embeddings to encode the query. Decode at p by +projection onto its first n_p coordinates. The self-block is I_(n_p). +Blocks between distinct supports vanish. Blocks within a support are +rectangular initial-coordinate overlaps, which the mask permits. This +constructs an actual full-mask factorization over every field using only +zero and one coefficients. + +For a support containing Q port p, c_S=d+e_p. For the other five supports, +c_S=d. Consequently total query dimension is exactly 49d+E, attaining +the lower bound. The construction is independent of the characteristic. + +One can also see its exact rank directly. For each support and local +coordinate, the associated expanded matrix is a nonempty all-ones block +on the ports that possess that coordinate. These blocks use disjoint row +and column sets. Each has rank one over every field, so their total rank +is sum_S c_S. Arbitrary independent invertible port charts preserve the +identity/zero mask and rank, though they do not reduce the universal floor. + +## First instance and scope + +Set d=1 and add one coordinate at Q port 0. The full matrix has 113 rows +and columns and exact minimum rank 50. No assertion is made that every +unequal vector satisfies a formula based only on total excess. Allowing +excess at other ports changes the family and can change both bounds. + +The compressed recipe stores 112 widths and 49 capacities. It does not +expand enormous payload matrices or implement the queries on a physical +machine. Native copies, access, frame changes, dirty restoration, numerical +precision, hosting and complete supplier costs remain outside the theorem. + +This contribution is produced by Nick Petalas. Credit Sagar Thakrar/PR2484, +Tekalign/PR3362, ywz65/PR2541 and PR2471, Cinna Davis/PR1825, +Adam Gall/PR1889, ctoth, Philippe Van Velzen and the retained P112 lineage. +The support embedding and rank arguments use elementary linear algebra; +no claim of literature priority for those methods is made. Apache-2.0. diff --git a/research/full-mask-separated-excess/README.md b/research/full-mask-separated-excess/README.md new file mode 100644 index 0000000000..df4dc007e9 --- /dev/null +++ b/research/full-mask-separated-excess/README.md @@ -0,0 +1,106 @@ +# Exact full-mask rank for separated-port excess payloads + +The complete fixed PR2484 112-port mask has minimum fitting rank + + 49d + sum_(p in T) e_p + +when every port has width d>=1 and only the 44 ports T of the retained +separated 22-plane set Q receive arbitrary excess widths e_p>=0. +The theorem holds over every field, with arbitrary rectangular ordered free +blocks, and the bound is attained on the full mask. This is a scoped proof +with finite corroboration. No new kappa or supplier admission is claimed. + +This answers a restricted family of Tekalign's [PR3362](https://github.com/CrocSwap/integer-mult-bounds/pull/3362) +Open next question 1, which asks for full unequal-width 112-port attainment. +The credited uniform 49d theorem and Q/C5 lower bound are dependencies. +The new result is the full-mask lift for all 44 independently increased +separated widths. The first example has d=1, width two at port 0, all other +widths one, and exact minimum rank 50 in a 113-by-113 matrix. + +[PROOF.md](PROOF.md) gives the lower bound and explicit support-wise encoder +and decoder. It also separates the result from the general unequal-width +problem. [SOURCES.json](SOURCES.json) pins the predecessor proofs, partition, +matching and label archive at canonical base +`624de9dc66858af0945e5f8a0942488d62280d43`. No predecessor executable is imported +or run. The card's scope is explicitly changed to this algebraic side result; +this does not supply a new paid profile or satisfy the physical mechanism gate. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/full-mask-separated-excess +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/full-mask-separated-excess/verify.py +``` + +Expected direct output: + +```text +PASS_FULL_MASK_SEPARATED_EXCESS matrices=50 field_ranks=150 controls=10 +``` + +The registered hook runs normal and optimized isolated checks. The direct +verifier works without Git when the declared input files retain their paths. +`--emit` prints a newly generated receipt; acceptance compares the complete +canonical JSON to [RESULT.json](RESULT.json). The receipt binds package and +proof file hashes and the source manifest. It is generated, not hand-written. + +The 50 full-mask matrices are all new nonuniform payloads: one single-unit +increase at each of the 44 Q ports, then three larger patterns both with and +without independent invertible port charts. Each is checked against every +forced identity and ordered zero block and ranked by literal elimination over +F2, F3 and F101. The patterns include d=2 and simultaneously unequal excesses. +A 201-bit base-width recipe is checked without expanding its matrix. These +finite instances corroborate the universal written proof; they do not enumerate +all fitting matrices or prove the universal lower bound by search. + +Ten controls cover invalid base widths, malformed/negative/Boolean excesses, +a one-direction forbidden leak, a changed diagonal identity, an omitted +extra-coordinate charge, and refusal to expand beyond 512 coordinates. +The archive and source files are authenticated before use. All acceptance +checks remain enabled under optimized Python. + +## Limits and implementation checks + +This is an exact linear query-capacity theorem. It does not price native +copies, access, frames, dirty restoration, precision, hosting or a complete +consumer. No complete multiplication theorem, selected-frontier change, +independent human review or formal proof-kernel acceptance is claimed. + +The verifier uses managed Python allocation, a documented Power of Ten +memory-rule deviation. Expanded matrices are capped at 512 coordinates; +there are 50 fixed fixtures and three fixed finite fields. Compressed input +integers have at most 4096 bits, and compressed arrays have fixed sizes +112 and 49. Pinned files are capped at 16 MiB and the extracted JSON member +is capped at 16 MiB. Tar/JSON/Python runtime allocation is not statically +controlled. Functions stay below 60 lines and there is no recursion. The +small callback set in rejection controls is a documented indirect-call +exception, restricted to the ten immediate controls. The source hash bounds +the exact runtime input. `-W error` is part of both registered commands; no +additional project Python linter configuration was found. The finite expansion +cap is exercised by a rejection control. A future larger replay must revise +these bounds before expansion. No asynchronous or persistent work is started. + +## Open next questions + +- Can excess widths on the ten C5 ports, or on the other 58 ports, also + attain Tekalign's principal lower bound on the full mask? First increase + one such width, compare the support capacity with that bound, and give + a full fitting factorization or a stronger obstruction. The present + theorem leaves those changes open. +- Can one of these unequal query layers improve a fully paid native + implementation? First choose source/target charts and price every read, + copy, frame change and restoration. Those costs remain unknown here. + +## Credit + +This contribution is produced by Nick Petalas. Credit Sagar Thakrar/PR2484 +for the scalar partition and Q/C5 witness; ywz65/PR2541 and PR2471 for the +all-field uniform block theorem and earlier mask work; Tekalign/PR3362 +for the unequal principal theorem and full-mask question; Cinna Davis/PR1825, +Adam Gall/PR1889, ctoth, Philippe Van Velzen and the retained E8/P112 lineage. +No predecessor credit is changed. Elementary support embeddings and linear +rank inequalities are classical methods; no literature-priority claim is made. +New material is Apache-2.0. Independent human and formal proof-kernel review +are unclaimed. diff --git a/research/full-mask-separated-excess/RESULT.json b/research/full-mask-separated-excess/RESULT.json new file mode 100644 index 0000000000..20a991c8a3 --- /dev/null +++ b/research/full-mask-separated-excess/RESULT.json @@ -0,0 +1,859 @@ +{ + "cases": [ + { + "charts": false, + "d": 1, + "excess": { + "0": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "1": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "2": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "3": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "4": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "5": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "6": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "7": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "8": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "9": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "10": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "11": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "12": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "13": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "14": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "15": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "16": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "17": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "18": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "19": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "20": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "21": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "22": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "23": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "24": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "25": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "26": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "27": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "28": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "29": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "30": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "31": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "32": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "33": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "34": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "35": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "36": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "37": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "38": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "39": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "40": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "41": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "42": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "43": 1 + }, + "field_ranks": [ + 50, + 50, + 50 + ], + "rank": 50, + "size": 113 + }, + { + "charts": false, + "d": 1, + "excess": { + "0": 1, + "1": 1, + "10": 1, + "11": 1, + "12": 1, + "13": 1, + "14": 1, + "15": 1, + "16": 1, + "17": 1, + "18": 1, + "19": 1, + "2": 1, + "20": 1, + "21": 1, + "22": 1, + "23": 1, + "24": 1, + "25": 1, + "26": 1, + "27": 1, + "28": 1, + "29": 1, + "3": 1, + "30": 1, + "31": 1, + "32": 1, + "33": 1, + "34": 1, + "35": 1, + "36": 1, + "37": 1, + "38": 1, + "39": 1, + "4": 1, + "40": 1, + "41": 1, + "42": 1, + "43": 1, + "5": 1, + "6": 1, + "7": 1, + "8": 1, + "9": 1 + }, + "field_ranks": [ + 93, + 93, + 93 + ], + "rank": 93, + "size": 156 + }, + { + "charts": true, + "d": 1, + "excess": { + "0": 1, + "1": 1, + "10": 1, + "11": 1, + "12": 1, + "13": 1, + "14": 1, + "15": 1, + "16": 1, + "17": 1, + "18": 1, + "19": 1, + "2": 1, + "20": 1, + "21": 1, + "22": 1, + "23": 1, + "24": 1, + "25": 1, + "26": 1, + "27": 1, + "28": 1, + "29": 1, + "3": 1, + "30": 1, + "31": 1, + "32": 1, + "33": 1, + "34": 1, + "35": 1, + "36": 1, + "37": 1, + "38": 1, + "39": 1, + "4": 1, + "40": 1, + "41": 1, + "42": 1, + "43": 1, + "5": 1, + "6": 1, + "7": 1, + "8": 1, + "9": 1 + }, + "field_ranks": [ + 93, + 93, + 93 + ], + "rank": 93, + "size": 156 + }, + { + "charts": false, + "d": 2, + "excess": { + "0": 1 + }, + "field_ranks": [ + 99, + 99, + 99 + ], + "rank": 99, + "size": 225 + }, + { + "charts": true, + "d": 2, + "excess": { + "0": 1 + }, + "field_ranks": [ + 99, + 99, + 99 + ], + "rank": 99, + "size": 225 + }, + { + "charts": false, + "d": 2, + "excess": { + "1": 1, + "10": 1, + "11": 2, + "13": 1, + "14": 2, + "16": 1, + "17": 2, + "19": 1, + "2": 2, + "20": 2, + "22": 1, + "23": 2, + "25": 1, + "26": 2, + "28": 1, + "29": 2, + "31": 1, + "32": 2, + "34": 1, + "35": 2, + "37": 1, + "38": 2, + "4": 1, + "40": 1, + "41": 2, + "43": 1, + "5": 2, + "7": 1, + "8": 2 + }, + "field_ranks": [ + 141, + 141, + 141 + ], + "rank": 141, + "size": 267 + }, + { + "charts": true, + "d": 2, + "excess": { + "1": 1, + "10": 1, + "11": 2, + "13": 1, + "14": 2, + "16": 1, + "17": 2, + "19": 1, + "2": 2, + "20": 2, + "22": 1, + "23": 2, + "25": 1, + "26": 2, + "28": 1, + "29": 2, + "31": 1, + "32": 2, + "34": 1, + "35": 2, + "37": 1, + "38": 2, + "4": 1, + "40": 1, + "41": 2, + "43": 1, + "5": 2, + "7": 1, + "8": 2 + }, + "field_ranks": [ + 141, + 141, + 141 + ], + "rank": 141, + "size": 267 + } + ], + "claim_type": "scoped proof with finite corroboration", + "controls": 10, + "large_recipe_rank": 78739964168690523523856887723246323014523436738603713732543410, + "literal_field_rank_checks": 150, + "matrix_cases": 50, + "package_sha256": { + "PROOF.md": "ff43584ebc22c28c119531ac3782152587216e3875a1d772e8a82ba53ba29c7d", + "README.md": "d77055ab9947c944a6c0b6e62a2abea8ff997f9919b90a9340f4e9c90144f84a", + "SOURCES.json": "f905f72def439b041ccb32a54b2558e1d23aeb54c80a6062454f8092ce001358", + "TASK.json": "579ab2018e672f59036c2e845969ee372e15827f9ae58234f2de441d743f53cf", + "VERIFY.json": "70a8a87baf7ed29f940d6463e7c8be8dd947ccd09697793a676704f370cdda4b", + "verify.py": "41fcccd6c3ba78666e2f79bce4ffe56e29aceeafcae8b5bae2503bb4e518ad55" + } +} diff --git a/research/full-mask-separated-excess/SOURCES.json b/research/full-mask-separated-excess/SOURCES.json new file mode 100644 index 0000000000..b3f1b80487 --- /dev/null +++ b/research/full-mask-separated-excess/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/paired-plane-block-rank/README.md", + "usage": "input", + "git_blob": "d0d06862952ba99c25a732ce9f43cee7f0f039cb", + "sha256": "0d9e5849dc7440738526c3020a669cc239254a8e16413e7df69108f9572fcf1e" + }, + { + "path": "research/paired-plane-block-rank/predecessor/PR2484-CERTIFICATE.json", + "usage": "input", + "git_blob": "393db5def16d76b3a0ebddc983c9bab6c3cc25fc", + "sha256": "6f5d3478290156c4fe703104572cc3aa593ad50079476ae08c942833714e3179" + }, + { + "path": "research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json", + "usage": "input", + "git_blob": "7ca668d7d50c7276e89b0f6f9575e1b9f1ad9ef6", + "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + }, + { + "path": "research/unequal-cycle-payloads/README.md", + "usage": "input", + "git_blob": "8e1e01bb308b7a9147847446a7070b0c7bb9f354", + "sha256": "834cd8c46c3893962afe96bdf13eccf21f698fcf26e8fe0ac3c9efd1cea1e4c4" + } + ] +} diff --git a/research/full-mask-separated-excess/TASK.json b/research/full-mask-separated-excess/TASK.json new file mode 100644 index 0000000000..32f90ba227 --- /dev/null +++ b/research/full-mask-separated-excess/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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": "Exact full-mask rank 49d plus total excess when only the 44 separated Q ports receive excess payload width.", + "scope_change_reason": "Take the restricted full-mask attainment case of Tekalign PR3362 Open next question 1; unequal full-mask query capacity is an algebraic side problem, not a new paid supplier.", + "bottleneck_link": "Resolve a full-mask unequal-query capacity case before proposing any physical or recursive benefit; the complete cost remains unpriced.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact scoped result; test the single-unit fixture, construct the 44-parameter family, and package without extending to other ports.", + "outcome": "completed", + "evidence": "PROOF.md and generated RESULT.json; 50 nonuniform full-mask fits over three fields, large compressed recipe, ten controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can excess widths outside Q attain the principal lower bound on the full fixed mask?", + "why_it_matters": "The theorem handles only the separated-port cone.", + "first_step": "Increase one C5 or remaining port and construct the full fit or give a stronger lower bound.", + "blocked_by": "full-mask factorization or stronger obstruction" + }, + { + "question": "Can the unequal query recipe reduce a complete native implementation bill?", + "why_it_matters": "Query dimension alone is not a supplier saving.", + "first_step": "Specify charts and price every read, copy, frame change and restoration.", + "blocked_by": "physical costs and complete consumer" + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134622", + "claim_type": "scoped proof with finite corroboration", + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit" + }, + "family_decision": "Stop after the exact algebraic family. Physical native consumer, access, frames, restoration, precision and hosting remain unknown; no mechanism expansion or new kappa.", + "overlap": { + "open_prs": 428, + "discussion_records": 3964, + "cached_at": "2026-10-22T23:38:13Z", + "materialized_notes": 121, + "head_notes": 6319, + "limits": "Sparse notes, arbitrary diffs and unpublished work; live PR bodies, recent account posts, full-main README grep and merged-term searches supplemented the cache." + } +} diff --git a/research/full-mask-separated-excess/VERIFY.json b/research/full-mask-separated-excess/VERIFY.json new file mode 100644 index 0000000000..857e38cb61 --- /dev/null +++ b/research/full-mask-separated-excess/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/paired-plane-block-rank/README.md", + "research/paired-plane-block-rank/predecessor/PR2484-CERTIFICATE.json", + "research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json", + "research/unequal-cycle-payloads/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "50 new nonuniform full-mask matrices, 150 literal finite-field ranks, compressed recipe and ten rejection/boundary controls with source/package receipt hashes." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete acceptance checks with optimized Python." + } + ] +} diff --git a/research/full-mask-separated-excess/verify.py b/research/full-mask-separated-excess/verify.py new file mode 100644 index 0000000000..707bdda897 --- /dev/null +++ b/research/full-mask-separated-excess/verify.py @@ -0,0 +1,216 @@ +#!/usr/bin/env python3 +"""Construct full-mask fits for separated-port excess payloads. Standard library.""" +import argparse +import hashlib +import io +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +CERT = 'research/paired-plane-block-rank/predecessor/PR2484-CERTIFICATE.json' +MATCH = 'research/paired-plane-scalar-mask-obstruction/PR1825-CERTIFICATE.json' +ARCHIVE = 'research/community-frontier1094-audit/selected-replay.tar.gz' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def inputs(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + raw = {} + for entry in manifest['files']: + if entry['usage'] != 'input': + continue + path = ROOT / entry['path'] + need(path.stat().st_size <= 16 * 1024 * 1024, 'input size') + data = path.read_bytes() + need(hashlib.sha256(data).hexdigest() == entry['sha256'], 'input hash') + raw[entry['path']] = data + source = json.loads(raw[CERT]) + matching = json.loads(raw[MATCH])['matching'] + with tarfile.open(fileobj=io.BytesIO(raw[ARCHIVE]), mode='r:gz') as archive: + member = archive.getmember(MEMBER) + need(member.isfile() and member.size <= 16 * 1024 * 1024, 'member size') + with archive.extractfile(member) as stream: + data = json.load(stream) + labels = [row['q'] for row in data['recipes']] + need(len(labels) == 112 and len(matching) == 56, 'source dimensions') + owners = {port: plane for plane, pair in enumerate(matching) for port in pair} + allowed = [[i != j and all((labels[a] & labels[b]).bit_count() % 2 == 0 + for a in matching[owners[i]] for b in matching[owners[j]]) + for j in range(112)] for i in range(112)] + qports = [p for plane in source['clique22'] for p in matching[plane]] + return source['rank49_supports'], qports, allowed + + +def construct(d, excess, supports, qports): + need(type(d) is int and 1 <= d and d.bit_length() <= 4096, 'base width') + need(len(excess) == 44 and all(type(e) is int and 0 <= e and + e.bit_length() <= 4096 for e in excess), 'excess vector') + dimensions = [d] * 112 + for port, value in zip(qports, excess): + dimensions[port] += value + capacities = [max(dimensions[p] for p in support) for support in supports] + return dimensions, capacities + + +def expand(dimensions, capacities, supports): + size = sum(dimensions) + need(size <= 512, 'expanded size limit') + offsets = [0] + for width in dimensions: + offsets.append(offsets[-1] + width) + matrix = [[0] * size for _ in range(size)] + groups = [] + for support, capacity in zip(supports, capacities): + for coordinate in range(capacity): + group = [offsets[p] + coordinate for p in support + if coordinate < dimensions[p]] + need(bool(group), 'empty query') + groups.append(group) + for row in group: + for column in group: + matrix[row][column] = 1 + return matrix, offsets, groups + + +def fits(matrix, dimensions, offsets, allowed): + size = sum(dimensions) + need(len(matrix) == size and all(len(row) == size for row in matrix), 'shape') + for i in range(112): + for j in range(112): + if i != j and allowed[i][j]: + continue + for a in range(dimensions[i]): + for b in range(dimensions[j]): + need(matrix[offsets[i]+a][offsets[j]+b] == + int(i == j and a == b), 'ordered mask or identity') + + +def rank(matrix, prime): + rows = [[value % prime for value in row] for row in matrix] + height = len(rows) + pivot = 0 + for column in range(len(rows[0])): + candidates = [i for i in range(pivot, height) if rows[i][column]] + if not candidates: + continue + index = candidates[0] + rows[pivot], rows[index] = rows[index], rows[pivot] + inverse = pow(rows[pivot][column], -1, prime) + rows[pivot] = [(x * inverse) % prime for x in rows[pivot]] + for i in range(pivot + 1, height): + scalar = rows[i][column] + if scalar: + rows[i] = [(x - scalar*y) % prime + for x, y in zip(rows[i], rows[pivot])] + pivot += 1 + if pivot == height: + break + return pivot + + +def change_charts(matrix, dimensions, offsets): + result = [row[:] for row in matrix] + for port, width in enumerate(dimensions): + if width < 2: + continue + a, b = offsets[port], offsets[port] + 1 + if port % 2: + a, b = b, a + result[a] = [x+y for x, y in zip(result[a], result[b])] + for row in result: + row[b] -= row[a] + return result + + +def check_case(d, excess, supports, qports, allowed, charts=False): + dimensions, capacities = construct(d, excess, supports, qports) + expected = 49*d + sum(excess) + need(sum(capacities) == expected, 'capacity formula') + matrix, offsets, groups = expand(dimensions, capacities, supports) + need(len(groups) == expected, 'query count') + flattened = sorted(x for group in groups for x in group) + need(flattened == list(range(sum(dimensions))), 'factor coordinates') + if charts: + matrix = change_charts(matrix, dimensions, offsets) + fits(matrix, dimensions, offsets, allowed) + observed = [rank(matrix, p) for p in (2, 3, 101)] + need(observed == [expected]*3, 'literal matrix ranks') + return {'d': d, 'excess': {str(i): e for i, e in enumerate(excess) if e}, + 'size': sum(dimensions), + 'rank': expected, 'field_ranks': observed, 'charts': charts} + + +def rejects(operation): + try: + operation() + except ValueError: + return + raise ValueError('negative control was accepted') + + +def controls(supports, qports, allowed): + for d in (0, -1, True): + rejects(lambda: construct(d, [1]*44, supports, qports)) + for excess in ([1]*43, [-1]+[0]*43, [True]+[0]*43): + rejects(lambda: construct(1, excess, supports, qports)) + dims, caps = construct(1, [1]+[0]*43, supports, qports) + matrix, offsets, groups = expand(dims, caps, supports) + bad = [row[:] for row in matrix] + bad[offsets[qports[0]]][offsets[qports[1]]] = 1 + rejects(lambda: fits(bad, dims, offsets, allowed)) + bad = [row[:] for row in matrix] + bad[0][0] = 0 + rejects(lambda: fits(bad, dims, offsets, allowed)) + need(len(groups) != 49, 'unpaid extra coordinate control') + rejects(lambda: expand([5]*112, [5]*49, supports)) + return 10 + + +def receipt(): + supports, qports, allowed = inputs() + cases = [] + for i in range(44): + excess = [0]*44 + excess[i] = 1 + cases.append(check_case(1, excess, supports, qports, allowed)) + for d, excess in ((1, [1]*44), (2, [1]+[0]*43), + (2, [i % 3 for i in range(44)])): + cases.append(check_case(d, excess, supports, qports, allowed)) + cases.append(check_case(d, excess, supports, qports, allowed, True)) + large = [2**(100+i)+i for i in range(44)] + dims, caps = construct(2**200, large, supports, qports) + need(sum(caps) == 49*2**200 + sum(large), 'large exact recipe') + count = controls(supports, qports, allowed) + hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file() and + p.name != 'RESULT.json'} + return {'claim_type': 'scoped proof with finite corroboration', + 'cases': cases, 'matrix_cases': len(cases), + 'literal_field_rank_checks': 3*len(cases), 'controls': count, + 'large_recipe_rank': sum(caps), 'package_sha256': hashes} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + result = receipt() + canonical = json.dumps(result, sort_keys=True, indent=2) + '\n' + if args.emit: + print(canonical, end='') + return + expected = json.loads((HERE / 'RESULT.json').read_text()) + need(canonical == json.dumps(expected, sort_keys=True, indent=2)+'\n', + 'receipt mismatch') + print('PASS_FULL_MASK_SEPARATED_EXCESS matrices=50 field_ranks=150 controls=10') + + +if __name__ == '__main__': + main()