Prove the sharp 177-term floor for query-using P111 scatters (no κ)

research/p111-redundant-query-scatter/ORIGINS.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "files": {
+    "word.json.gz": {
+      "repository": "CrocSwap/integer-mult-bounds",
+      "pr": 1525,
+      "head": "90d39a5603c7fbfd8d8d957e9732d9b6ebd6317f",
+      "path": "research/p111-early-merge-query/inputs/word-base.json.gz",
+      "git_blob": "eacf8c773cb50637f93a762342b3b5f0853fe29a",
+      "sha256": "e8e6e78ff7422275c38324499e1f33fb2ecd30de9503aef2b8f1ee80d8c4df8e"
+    },
+    "CENTRE-SEED.json": {
+      "repository": "CrocSwap/integer-mult-bounds",
+      "pr": 1525,
+      "head": "90d39a5603c7fbfd8d8d957e9732d9b6ebd6317f",
+      "path": "research/p111-early-merge-query/CENTRE-SEED.json",
+      "git_blob": "d5bea849fdde3bb43d38ff44d7b5a2c34e754954",
+      "sha256": "228e178662fc01895bbcd8472a52114d3a3d11ea8c7ae44d99cd1c8cf9e89147"
+    },
+    "PR1525-NOTICE.md": {
+      "repository": "CrocSwap/integer-mult-bounds",
+      "pr": 1525,
+      "head": "90d39a5603c7fbfd8d8d957e9732d9b6ebd6317f",
+      "path": "research/p111-early-merge-query/NOTICE.md",
+      "git_blob": "0f587a9f5fc2394ebaca23f5ce9a25f039b12170",
+      "sha256": "15bcaa301ca2513b03809c18731051368daf40a8cf93f86441da30608a1a6a3e"
+    },
+    "PR1525-PREDECESSOR-NOTICE.md": {
+      "repository": "CrocSwap/integer-mult-bounds",
+      "pr": 1525,
+      "head": "90d39a5603c7fbfd8d8d957e9732d9b6ebd6317f",
+      "path": "research/p111-early-merge-query/PREDECESSOR-NOTICE.md",
+      "git_blob": "0c256b6df08327b4955e46fc34a3ef69f4c63205",
+      "sha256": "4c7ff8b40efb09d549d65ae59db04d99f24ae5d6ce4bc67f195b859484c3cb7c"
+    }
+  }
+}

research/p111-redundant-query-scatter/PROOF.md

@@ -0,0 +1,110 @@
+# A retained four-centre query cannot sparsify this scatter
+
+This scoped proof was produced by Nick Petalas. Work over the rational
+numbers. The same proof holds over the real or complex numbers. It concerns
+direct scalar ADD coefficients, with arbitrary coefficients permitted.
+
+Let c be an arbitrary vector of eight independent centre values in the order
+`(60,61,63,224,31,240,23,256)`. Put J=`{61,63,31,256}` and
+
+```text
+q = (c61+c63+c31+c256)/2.
+```
+
+Let S be the 112-by-8 matrix of the pinned PR1525 word's `cut` array. We
+ask for matrices B with nine columns such that
+
+```text
+B (c,q) = S c    for every c.
+```
+
+All eight old readouts are retained. Only their use in this direct scatter
+is being optimized. The price of B is its number of nonzero entries. Each
+entry denotes one scaled ADD to the corresponding arbitrary dirty output.
+No sharing, intermediate accumulator, target mixing or basis change is
+included in this price model. Readout acquisition and frames are not free
+physical operations merely because the algebra grants their availability.
+
+## Every exact correction and its cost
+
+Fix a row a of S. If the coefficient of q in its replacement row is t,
+coefficient comparison on the eight independent centre variables forces
+
+```text
+b_j = a_j-t/2 for j in J,
+b_j = a_j     for j outside J.
+```
+
+Conversely these coefficients work for every t. This describes every exact
+row, without a finite coefficient restriction. In particular no independent
+correction freedom is omitted by the following optimization.
+
+Let z be the number of zero entries of a on J. If t is nonzero, all z of
+these entries become nonzero, the query adds one nonzero entry, and the only
+cancellations are entries with a_j=t/2. If m(t/2) counts those entries, the
+exact increase in row support is
+
+```text
+1+z-m(t/2).
+```
+
+The finite source census below finds at most two nonzero entries on J in
+every row. Thus z>=2 and m(t/2)<=2. Every nonzero query coefficient strictly
+increases that row's support, by at least one. A query-free row is forced
+to equal a. Since the rows have independent coefficients, the unique
+minimum-support B is `[S | 0]`, of support 176.
+
+If at least one query coefficient must be nonzero, support is at least 177.
+Equality is possible exactly by activating one row with z=2 and two equal
+nonzero coefficients a_j=t/2, and leaving every other row unchanged. This
+also characterizes every matrix attaining 177.
+
+## Complete finite census and attainment
+
+Every coefficient of S is 0 or plus/minus 1/4. The checker classifies every
+row by its entries on J. The counts and minimum nonzero-query penalties are:
+
+| Entries on J | Rows | Minimum increase |
+|---|---:|---:|
+| Four zeros | 40 | 5 |
+| One nonzero | 56 | 3 |
+| Two equal nonzeros | 8 | 1 |
+| Two opposite nonzeros | 8 | 2 |
+
+For each of the eight equal-pair rows, choose t twice the common coefficient.
+The two original nonzero entries disappear, the two previously zero entries
+become their negatives, and q adds one term. This gives an exact 177-entry
+matrix. The replay reports all eight receiver IDs, and emits one attaining
+row's receiver and coefficient. The finite arithmetic census supplies the
+source-specific premise; the argument above supplies the quantifier over
+every rational coefficient and every exact direct-scatter matrix.
+
+An independent checker enumerates all 512 subsets of the nine readouts for
+each of the 112 rows. It uses exact integer elimination for rational span
+membership, without the frequency formula. With q present, a nonzero query
+coefficient exists if q is dependent on the selected centres, or, when it
+is independent, if a is absent from the selected-centre span. This also
+handles zero rows, where query use requires compensating centre terms.
+All 57,344 support-subset cases give the same two per-row minima.
+
+## Dirty values and the precise obstruction
+
+The matrix identity holds for arbitrary c. Therefore it holds for every
+possible prior linear or nonlinear dependence of c on original inputs and
+dirty workspace. Adding B(c,q) to arbitrary outputs preserves precisely the
+same dirty dependence as adding Sc. No original dirty coefficient has been
+discarded, specialized to zero or claimed compensated. The direct ADD program
+reads c and q without changing them. Reversing its ADD signs restores the
+outputs exactly. This is an algebraic restoration statement.
+
+The lower bound requires exact equality for every independent centre vector.
+Restricted-value inputs or a caller that needs a different output are other
+contracts. Shared arithmetic can compute a direct matrix more cheaply than
+its nonzero count, so this is not an ADD-circuit lower bound. Multiple new
+queries, changed source bases and changing the scatter itself are outside
+scope. In particular this result does not reject PR1525's whole research
+direction or reprove PR6640's different eight-readout price check.
+
+The two-zero premise matters. A row with coefficient 1/4 on all four query
+centres has four old terms and equals q/2, which has one. The replay includes
+this changed-premise positive control.

research/p111-redundant-query-scatter/README.md

@@ -0,0 +1,147 @@
+# Sharp support obstruction for the retained P111 line-7 query
+
+This contribution was produced by Nick Petalas. Claim type: scoped proof
+with exact finite corroboration. No new kappa is claimed.
+
+For the PR1525 puncture-0 scatter, retain all eight independent original
+centre readouts and add `q=(c61+c63+c31+c256)/2`. Among every rational
+direct-scatter matrix preserving the original map, the unique minimum has
+176 nonzero coefficients and ignores q. If q must be used, the exact minimum
+is 177. Exactly eight matrices attain that constrained minimum, one for each
+receiver in `(112,113,115,119,152,153,179,183)`.
+
+The new result closes a favorable direct-matrix relaxation of Open next
+question 2 in [unpaidmoon's PR6640](https://github.com/CrocSwap/integer-mult-bounds/pull/6640).
+The original eight readouts remain available, so this is a changed contract
+from substituting q for one centre. It is an obstruction over all rational
+coefficients, rather than a failed finite search. The predecessor's 176-entry
+scatter is the baseline input, not a new count claimed here.
+
+The [proof](PROOF.md) characterizes every exact correction. On each row a,
+the query coefficient t forces subtraction of t/2 from each of the four
+query-centre coefficients. Every source row omits at least two of these
+centres. A nonzero t therefore creates at least two new terms, cancels at
+most two, and adds its own term. This proves the strict penalty and the
+unique unrestricted optimum. Eight equal-pair rows attain penalty one.
+
+This prices direct coefficients only. General ADD circuits may share
+intermediates and have a smaller operation count. A ninth readout also has
+acquisition, frame, lifetime and restoration costs that are not priced here.
+This result supplies neither a physical scatter nor a complete paid invoice.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p111-redundant-query-scatter/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/p111-redundant-query-scatter/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p111-redundant-query-scatter
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p111-redundant-query-scatter --check-source-history
+```
+
+Another CPython 3.12 interpreter may replace the absolute local path.
+Direct replay prints `PASS_P111_REDUNDANT_QUERY_SCATTER` in a fresh JSON
+receipt bound to all twelve package files. It writes nothing. Registered
+normal and optimized checks run the same complete domain with explicit
+guards that remain enabled under `-O`.
+
+The primary checker constructs one attaining matrix and compares all eight
+formal centre coefficients of every output. It classifies all 112 rows.
+The separate [support oracle](oracle.py) enumerates all 512 readout subsets
+for each row, for 57,344 cases, and uses integer elimination over Q rather
+than the cancellation-frequency formula. It checks both unrestricted
+support and a genuinely nonzero query coefficient.
+
+Eight centre-basis fixtures use arbitrary nonzero rational dirty targets;
+the literal ADD interpreter checks the exact endpoint, unchanged readouts
+and reverse restoration. Six controls reject changed query/correction
+coefficients, a missing query centre, a false equal-cost claim and invalid
+target/denominator inputs. A dense-row positive control reduces four terms
+to one and confirms that the two-zero premise is essential. The written
+identity gives arbitrary dirty-input coverage; these fixtures corroborate
+its implementation.
+
+## Sources, credit and overlap
+
+Rohan Arun / rohanarun's [PR1525](https://github.com/CrocSwap/integer-mult-bounds/pull/1525),
+head `90d39a5603c7fbfd8d8d957e9732d9b6ebd6317f`, supplies the query and
+word. Four source files, including both unchanged predecessor notices, are
+retained under `inputs/`. [ORIGINS.json](ORIGINS.json) records their original
+paths, Git blobs and SHA256 values. They were first retained at commit
+`34ffd44f2d6257e9c2bcfd01970b5fce61113ab2`; [SOURCES.json](SOURCES.json)
+pins these ancestor bytes. No unmerged foreign Git object is required.
+The checker uses only the source `cut`, centre order and query terms. It
+does not execute or validate the predecessor's native, dirty-query or
+whole-word verifier.
+
+Credit unpaidmoon for the question and frozen-interface price screen, and
+JoyboyBrian for the earlier triangular identity in Discussion1166 comment
+19143427. Credit PR1297/1134/1060 and the retained Rohan Arun, Ali Romman,
+DreamingOfClouds, eumemic, geometry, supplier and controller lineage.
+Sparse linear representation and rational elimination are classical.
+Independent human and formal proof-kernel review are unclaimed.
+
+Related open work at the overlap checkpoint:
+
+- PR6640 studies the eight-readout substitution and its physical price.
+  This theorem optimizes a different, redundant nine-readout direct matrix.
+- PR1525 supplies the underlying query and leaves a physical continuation
+  open. This local obstruction does not settle that larger question.
+- PR1900 constructs five plane queries on the P111 boundary. That changes
+  both factors and is outside this single retained-query model.
+- PR3045 and PR2832 concern fitting-matrix decoder rank floors and global
+  decoder reductions. Neither is a direct coefficient-support objective
+  for the fixed centre query here.
+
+The live overlap cache covered 613 open PRs and 6,708 Discussion records.
+Its sparse local scan covered 127 of 8,917 note paths; main-branch README
+searches supplemented it. Closed PR and recent account searches were also
+used. This is a stated search scope, not proof of literature novelty.
+
+The joint-query-controller card is refined to this algebraic relaxation.
+The pinned catalogue is revision 8 at canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The selected record identifies
+PR6030; historical priority prose retains an older checkpoint. The selected
+frontier is unchanged.
+
+## Limits and implementation constraints
+
+The theorem requires the same exact output map for all independent centre
+values and all 112 original cut rows. Omitting a punctured or unused output
+changes the consumer contract. Restricted-value inputs, shared intermediate arithmetic, changed
+bases, other queries and a changed consumer remain outside scope. Native
+frames, query acquisition, independent dirty-state compensation, physical
+mixing, owner lifetimes, complete restoration costs, precision/tape,
+compiler closure and a complete supplier invoice remain unproved. The five
+framework assumptions remain. No selected cold replay, Lean or Docker run
+is claimed.
+
+The new checker has no recursion, network access or subprocesses. Every loop
+uses a finite bound: 112 rows, eight centre coordinates, nine readouts,
+512 support subsets, at most four cancellation candidates and at most
+1,024 source cut events. Elimination has at most ten rows and eight columns.
+Compressed/file reads are capped at one MiB and expanded word bytes at two
+MiB. Functions fit within 60 physical lines. Warning-strict normal and
+optimized commands are the available diagnostics; no new static-analysis
+dependency is added.
+
+Power-of-ten rule 3 deviation: CPython allocates managed integers, Fractions
+and containers during the bounded one-shot replay. Fixed runtime allocation
+is not available. The finite domains and byte limits above bound live
+resources; context managers close files on success and failure. A fixed
+allocation implementation would need a separate runtime if required.
+Rule 9 deviation: the rejection helper dispatches only six statically named
+local control calls. Each has a fixed fixture, and unexpected exceptions
+propagate. All six rejection paths run in both registered modes.
+
+## Open next questions
+
+Can shared intermediate arithmetic exploit this query after its actual
+acquisition, frame and restoration costs are charged? A useful first step
+is one explicit chronological shared-accumulator scatter with the same eight
+centres and q, followed by a complete price for its readouts and temporaries.
+A physical nine-readout caller and legal lifetime/restoration contract are
+the blockers. No wider construction search is reserved here.
+
+New work is Apache-2.0. Source notices are retained unchanged.

research/p111-redundant-query-scatter/SOURCES.json

@@ -0,0 +1,53 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/p111-redundant-query-scatter/ORIGINS.json",
+      "usage": "input",
+      "pin": "head:34ffd44f2d6257e9c2bcfd01970b5fce61113ab2:research/p111-redundant-query-scatter/ORIGINS.json",
+      "git_blob": "bb898f02db1ed6fb4b04836e3f8f6832a254f2e9",
+      "sha256": "2222abdd0dde549bdc118ae29b6e039f79ed2b422f8112f029f1a6eebea8ad7b"
+    },
+    {
+      "path": "research/p111-redundant-query-scatter/inputs/CENTRE-SEED.json",
+      "usage": "input",
+      "pin": "head:34ffd44f2d6257e9c2bcfd01970b5fce61113ab2:research/p111-redundant-query-scatter/inputs/CENTRE-SEED.json",
+      "git_blob": "d5bea849fdde3bb43d38ff44d7b5a2c34e754954",
+      "sha256": "228e178662fc01895bbcd8472a52114d3a3d11ea8c7ae44d99cd1c8cf9e89147"
+    },
+    {
+      "path": "research/p111-redundant-query-scatter/inputs/PR1525-NOTICE.md",
+      "usage": "input",
+      "pin": "head:34ffd44f2d6257e9c2bcfd01970b5fce61113ab2:research/p111-redundant-query-scatter/inputs/PR1525-NOTICE.md",
+      "git_blob": "0f587a9f5fc2394ebaca23f5ce9a25f039b12170",
+      "sha256": "15bcaa301ca2513b03809c18731051368daf40a8cf93f86441da30608a1a6a3e"
+    },
+    {
+      "path": "research/p111-redundant-query-scatter/inputs/PR1525-PREDECESSOR-NOTICE.md",
+      "usage": "input",
+      "pin": "head:34ffd44f2d6257e9c2bcfd01970b5fce61113ab2:research/p111-redundant-query-scatter/inputs/PR1525-PREDECESSOR-NOTICE.md",
+      "git_blob": "0c256b6df08327b4955e46fc34a3ef69f4c63205",
+      "sha256": "4c7ff8b40efb09d549d65ae59db04d99f24ae5d6ce4bc67f195b859484c3cb7c"
+    },
+    {
+      "path": "research/p111-redundant-query-scatter/inputs/word.json.gz",
+      "usage": "input",
+      "pin": "head:34ffd44f2d6257e9c2bcfd01970b5fce61113ab2:research/p111-redundant-query-scatter/inputs/word.json.gz",
+      "git_blob": "eacf8c773cb50637f93a762342b3b5f0853fe29a",
+      "sha256": "e8e6e78ff7422275c38324499e1f33fb2ecd30de9503aef2b8f1ee80d8c4df8e"
+    }
+  ]
+}