diff --git a/research/p111-redundant-query-scatter/ORIGINS.json b/research/p111-redundant-query-scatter/ORIGINS.json new file mode 100644 index 0000000000..bb898f02db --- /dev/null +++ b/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" + } + } +} diff --git a/research/p111-redundant-query-scatter/PROOF.md b/research/p111-redundant-query-scatter/PROOF.md new file mode 100644 index 0000000000..600832f994 --- /dev/null +++ b/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. diff --git a/research/p111-redundant-query-scatter/README.md b/research/p111-redundant-query-scatter/README.md new file mode 100644 index 0000000000..06b5f21d3d --- /dev/null +++ b/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. diff --git a/research/p111-redundant-query-scatter/SOURCES.json b/research/p111-redundant-query-scatter/SOURCES.json new file mode 100644 index 0000000000..1e026e86cd --- /dev/null +++ b/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" + } + ] +} diff --git a/research/p111-redundant-query-scatter/TASK.json b/research/p111-redundant-query-scatter/TASK.json new file mode 100644 index 0000000000..f52d7e1156 --- /dev/null +++ b/research/p111-redundant-query-scatter/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Prove the sharp direct-scatter coefficient-support optimum for the fixed PR1525 puncture-0 query when all eight original independent centre readouts are retained alongside the query. The unique unrestricted optimum ignores the query and has 176 coefficients; requiring query use has exact optimum 177 and eight attaining matrices.", + "scope_change_reason": "The caller question is restricted to an algebraic nine-readout relaxation. This grants additional readout availability and optimizes direct matrix support, not shared circuit complexity or physical delivery.", + "bottleneck_link": "Rules out direct matrix sparsification by this single added query, even under favorable retained-readout availability. A useful continuation must change basis, share intermediate arithmetic, add other queries or change the consumer; no supplier improvement follows.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact sparse-scatter optimum and attaining witness; package it without expanding the mechanism.", + "outcome": "negative-result", + "evidence": "PROOF.md and freshly generated verify.py output; 112 rows, 57344 support-subset cases, 8 dirty-basis endpoint/inverse cases and 6 rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can shared intermediate arithmetic exploit this query after its actual acquisition, frame and restoration costs are charged?", + "why_it_matters": "The direct support obstruction does not bound general ADD circuits, which can share computations across rows.", + "first_step": "Give one explicit chronological shared-accumulator scatter with the same eight original centre values and q, then price the extra readout and every temporary.", + "blocked_by": "A physical nine-readout caller, legal frames, availability, restoration and complete paid invoice are absent." + } + ], + "predecessors": [ + { + "pr": 6640, + "author": "unpaidmoon", + "role": "Open next question 2 and frozen triangular price context; not replayed" + }, + { + "pr": 1525, + "author": "Rohan Arun / rohanarun", + "head": "90d39a5603c7fbfd8d8d957e9732d9b6ebd6317f", + "role": "Fixed centre query and cut matrix; four exact source files retained" + }, + { + "discussion_comment": 19143427, + "author": "JoyboyBrian", + "role": "Earlier triangular identity; cited context only" + } + ] +} diff --git a/research/p111-redundant-query-scatter/VERIFY.json b/research/p111-redundant-query-scatter/VERIFY.json new file mode 100644 index 0000000000..71dff5031c --- /dev/null +++ b/research/p111-redundant-query-scatter/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p111-redundant-query-scatter/ORIGINS.json", + "research/p111-redundant-query-scatter/inputs/CENTRE-SEED.json", + "research/p111-redundant-query-scatter/inputs/PR1525-NOTICE.md", + "research/p111-redundant-query-scatter/inputs/PR1525-PREDECESSOR-NOTICE.md", + "research/p111-redundant-query-scatter/inputs/word.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete exact support optimization, 57344 subset-span oracle cases, formal identity, dirty endpoints/inverses, six rejecting controls and dense positive control" + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete evidence with Python assertions disabled; guards remain explicit" + } + ] +} diff --git a/research/p111-redundant-query-scatter/inputs/CENTRE-SEED.json b/research/p111-redundant-query-scatter/inputs/CENTRE-SEED.json new file mode 100644 index 0000000000..d5bea849fd --- /dev/null +++ b/research/p111-redundant-query-scatter/inputs/CENTRE-SEED.json @@ -0,0 +1,172 @@ +{ + "status": "PASS_SCOPED_NONNESTED_CENTRE_QUERY_NATIVE", + "puncture": 0, + "terms": [ + { + "center": 61, + "weight": "1/2", + "frame": [ + 256, + 128, + 64, + 32, + 16, + 8, + 5, + 3 + ] + }, + { + "center": 63, + "weight": "1/2", + "frame": [ + 256, + 128, + 64, + 32, + 17, + 9, + 4, + 2 + ] + }, + { + "center": 31, + "weight": "1/2", + "frame": [ + 256, + 128, + 65, + 33, + 17, + 9, + 4, + 2 + ] + }, + { + "center": 256, + "weight": "1/2", + "frame": [ + 256, + 128, + 65, + 33, + 16, + 8, + 5, + 3 + ] + } + ], + "query_frame": [ + 2, + 5, + 9, + 16, + 32, + 64, + 128, + 256 + ], + "transport_profile": { + "2": 4 + }, + "rank_mass": 8, + "omitted_source_coefficient": "2", + "dirty_columns": 62, + "dirty_coefficients": { + "239": "-1", + "225": "-1", + "237": "-1", + "224": "2", + "255": "-1", + "241": "-1", + "253": "-1", + "240": "1", + "242": "1", + "271": "-2", + "256": "1", + "261": "1", + "270": "1", + "351": "-3", + "340": "1", + "350": "1", + "336": "1", + "367": "-1", + "356": "1", + "366": "1", + "352": "1", + "383": "-1", + "379": "1", + "368": "1", + "399": "-2", + "388": "1", + "398": "1", + "395": "1", + "227": "1", + "283": "-1", + "287": "-2", + "280": "-1", + "272": "1", + "299": "-1", + "303": "-2", + "292": "1", + "302": "1", + "400": "1", + "403": "2", + "409": "1", + "402": "-1", + "411": "1", + "416": "1", + "419": "1", + "425": "1", + "418": "-1", + "421": "1", + "430": "1", + "417": "1", + "429": "1", + "243": "1", + "319": "-2", + "435": "1", + "441": "1", + "434": "-1", + "437": "1", + "446": "1", + "433": "1", + "445": "1", + "267": "-1", + "431": "-1", + "447": "-1" + }, + "fixtures": [ + { + "trial": 0, + "forward_and_inverse_transpose": true, + "streaming_peak_temporaries": 2, + "weighted_accumulations": 4, + "source_copies": 4, + "temporary_discards": 5 + }, + { + "trial": 1, + "forward_and_inverse_transpose": true, + "streaming_peak_temporaries": 2, + "weighted_accumulations": 4, + "source_copies": 4, + "temporary_discards": 5 + } + ], + "optimistic_moment": "0.999971277929646601478394497346102075481621", + "optimistic_profile": { + "1": 2340, + "4": 130, + "3": 414, + "2": 508, + "5": 80, + "8": 7, + "7": 1 + }, + "optimistic_idle": 14274, + "scope": "Four source-stable whole-stream copies at nonnested frame transitions. Exact signed Pauli/global phase checks and two dense Gaussian fixtures in each orientation. The omitted source must be zero and dirty response compensated. Two-stream peak includes query accumulator and one live converted centre copy. Storage, all-size native recursion, nonmonotone owner hosting, full scatter and exact recovery/precision/analytic transfer are unadmitted. Favorable moment grants incompatible deletion/endpoint/hosting credits, not a new bound." +} \ No newline at end of file diff --git a/research/p111-redundant-query-scatter/inputs/PR1525-NOTICE.md b/research/p111-redundant-query-scatter/inputs/PR1525-NOTICE.md new file mode 100644 index 0000000000..0f587a9f5f --- /dev/null +++ b/research/p111-redundant-query-scatter/inputs/PR1525-NOTICE.md @@ -0,0 +1,19 @@ +SPDX-License-Identifier: Apache-2.0 + +Prepared for Rohan Arun with substantial OpenAI Codex assistance. No independent +human review is claimed. This draft is a scoped query-tree witness, not a kappa +record or complete multiplication theorem. + +Credit Ali Romman / PR1134 for the fixed-U8 transport obstruction, favorable +volume accounting, and rational moment checker; PR1060 for the physical P111 +decoder and nonzero-endpoint-last schedule. The vendored PR1134 verifier is +retained byte-for-byte, with only its arithmetic/subspace functions used here; +its original main pipeline is not run or claimed replayed. + +Credit DreamingOfClouds / PR717 and themilkman216 / PR968 for P111 decoder and +copy-cost results; Rohan Arun / PR1297,1319,1485 for current word and endpoint; +Jeremy Kothe, Jeremy Diviney, Thomas DiFiore, Hao Yan, Zhihao Chen / icekylinx, +eumemic, Douglas Colkitt, and the retained geometry/supplier/controller lineage. +See PREDECESSOR-NOTICE.md for the current-word package's retained notices. + +Native interface extension: unchanged exact Clifford compiler, literal Gaussian array executor and transpose helper from PR1060 (head d27499553138bde007f5b1163e65e71da1b18899); original Apache-2.0 code and authorship retained. Source hashes in SOURCES.json and pr1060/SOURCE-RECEIPT.json. This extension verifies only our local query interface. diff --git a/research/p111-redundant-query-scatter/inputs/PR1525-PREDECESSOR-NOTICE.md b/research/p111-redundant-query-scatter/inputs/PR1525-PREDECESSOR-NOTICE.md new file mode 100644 index 0000000000..0c256b6df0 --- /dev/null +++ b/research/p111-redundant-query-scatter/inputs/PR1525-PREDECESSOR-NOTICE.md @@ -0,0 +1,8 @@ +New research prepared by Rohan Arun with substantial OpenAI Codex assistance. Apache-2.0. Parent words and build recipe method derive from Jeremy Kothe PR1274 and Rohan Arun PR1218, with lineage credited in README.md. All inherited mathematical qualifications are retained. +Additional pivot555 and567 composition by Rohan Arun with substantial OpenAI Codex assistance. + +T74 exact-fill owner construction by Rohan Arun with substantial OpenAI Codex assistance. + +PR1377 grid refinement credited to Jeremy Kothe. Outer witness refinement by Rohan Arun with OpenAI Codex assistance; construction unchanged. + +PR1458 finer base-two engine and endpoint refinement: Jeremy Kothe, with oh-my-pi assistance. Further finite64 endpoint and outer refinement: Rohan Arun with OpenAI Codex assistance. Construction unchanged. diff --git a/research/p111-redundant-query-scatter/inputs/word.json.gz b/research/p111-redundant-query-scatter/inputs/word.json.gz new file mode 100644 index 0000000000..eacf8c773c Binary files /dev/null and b/research/p111-redundant-query-scatter/inputs/word.json.gz differ diff --git a/research/p111-redundant-query-scatter/oracle.py b/research/p111-redundant-query-scatter/oracle.py new file mode 100644 index 0000000000..1559bb6094 --- /dev/null +++ b/research/p111-redundant-query-scatter/oracle.py @@ -0,0 +1,54 @@ +"""Exhaust readout supports using exact rational ranks. + +This checker does not use the row-frequency optimization in verify.py. +Produced by Nick Petalas. Apache-2.0. +""" + + +def rank(rows): + """Fraction-free elimination with at most ten rows of length eight.""" + if len(rows) > 10 or any(len(row) != 8 for row in rows): + raise ValueError("rank domain is at most 10 by 8") + work = [list(row) for row in rows] + used = 0 + for col in range(8): + pivot = next((i for i in range(used, len(work)) if work[i][col]), None) + if pivot is None: + continue + work[used], work[pivot] = work[pivot], work[used] + for i in range(used + 1, len(work)): + multiplier = work[i][col] + if multiplier: + value = work[used][col] + work[i] = [value * a - multiplier * b + for a, b in zip(work[i], work[used], strict=True)] + used += 1 + return used + + +def support_oracle(rows, query_slots): + """Return each row's unrestricted and genuinely-query-using minima.""" + if len(rows) != 112 or len(query_slots) != 4: + raise ValueError("oracle requires 112 rows and four query slots") + vectors = [tuple(int(i == j) for i in range(8)) for j in range(8)] + vectors.append(tuple(int(i in query_slots) for i in range(8))) + supports = [] + for mask in range(512): + old = [vectors[i] for i in range(8) if mask >> i & 1] + full = old + ([vectors[8]] if mask >> 8 & 1 else []) + supports.append((mask.bit_count(), old, full, rank(old), rank(full))) + answers = [] + for row in rows: + best, active = 10, 10 + for mask, (cost, old, full, old_rank, full_rank) in enumerate(supports): + if rank(full + [row]) != full_rank: + continue + best = min(best, cost) + if mask >> 8 & 1: + # Dependent q admits any coefficient. Otherwise it is forced. + if full_rank == old_rank or rank(old + [row]) > old_rank: + active = min(active, cost) + if best == 10 or active == 10: + raise AssertionError("dictionary must span every row") + answers.append((best, active)) + return answers, 112 * 512 diff --git a/research/p111-redundant-query-scatter/verify.py b/research/p111-redundant-query-scatter/verify.py new file mode 100644 index 0000000000..71801e8be4 --- /dev/null +++ b/research/p111-redundant-query-scatter/verify.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Sharp direct-scatter support obstruction for one retained P111 query. + +Produced by Nick Petalas. Apache-2.0. +""" +import gzip +import hashlib +import io +import json +import platform +import sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +from oracle import support_oracle + +ROOT = Path(__file__).resolve().parent +CENTRES = (60, 61, 63, 224, 31, 240, 23, 256) +QUERY_CENTRES = (61, 63, 31, 256) +FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "verify.py", "oracle.py", "ORIGINS.json", "inputs/word.json.gz", + "inputs/CENTRE-SEED.json", "inputs/PR1525-NOTICE.md", + "inputs/PR1525-PREDECESSOR-NOTICE.md", +) + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def read_bytes(name): + with (ROOT / name).open("rb") as handle: + raw = handle.read(1_048_577) + need(len(raw) <= 1_048_576, "file size bound: " + name) + return raw + + +def read_inputs(): + origins = json.loads(read_bytes("ORIGINS.json"))["files"] + need(len(origins) == 4, "four retained source files") + for name, origin in origins.items(): + need(name in {Path(f).name for f in FILES if f.startswith("inputs/")}, + "unexpected source path") + raw = read_bytes("inputs/" + name) + need(hashlib.sha256(raw).hexdigest() == origin["sha256"], "source hash") + blob = b"blob " + str(len(raw)).encode("ascii") + b"\0" + raw + need(hashlib.sha1(blob).hexdigest() == origin["git_blob"], "source blob") + raw = read_bytes("inputs/word.json.gz") + need(hashlib.sha256(raw).hexdigest() == + "e8e6e78ff7422275c38324499e1f33fb2ecd30de9503aef2b8f1ee80d8c4df8e", + "fixed PR1525 word") + with gzip.GzipFile(fileobj=io.BytesIO(raw)) as handle: + expanded = handle.read(2_097_153) + need(len(expanded) <= 2_097_152, "decompressed word bound") + word = json.loads(expanded) + seed_raw = read_bytes("inputs/CENTRE-SEED.json") + need(hashlib.sha256(seed_raw).hexdigest() == + "228e178662fc01895bbcd8472a52114d3a3d11ea8c7ae44d99cd1c8cf9e89147", + "fixed PR1525 query seed") + seed = json.loads(seed_raw) + need(word["centers"] == list(CENTRES), "centre order") + terms = seed["terms"] + need(seed["puncture"] == 0 and len(terms) == 4, "query domain") + need(tuple(t["center"] for t in terms) == QUERY_CENTRES, "query support") + need(all(Q(t["weight"]) == Q(1, 2) for t in terms), "query weights") + return word + + +def scatter(word): + events = word["cut"] + need(isinstance(events, list) and len(events) <= 1024, "cut bound") + result = [[Q(0) for _ in range(8)] for _ in range(112)] + for event in events: + need(isinstance(event, list) and len(event) == 6, "cut event shape") + op, target, source, numerator, denominator, frame = event + need(op == "add" and frame is None, "cut event kind") + need(type(target) is int and 112 <= target < 224, "output role") + need(type(source) is int and source in CENTRES, "centre role") + need(type(numerator) is int and numerator in (-1, 1), "numerator") + need(type(denominator) is int and denominator == 4, "denominator") + result[target - 112][CENTRES.index(source)] += Q(numerator, denominator) + need(all(value in (Q(-1, 4), Q(0), Q(1, 4)) + for row in result for value in row), "quarter-grid scatter") + return result + + +def corrected(row, coefficient, slots): + return [value - coefficient / 2 if j in slots else value + for j, value in enumerate(row)] + [coefficient] + + +def nnz(row): + return sum(value != 0 for value in row) + + +def row_optimum(row, slots): + # All exceptional cancellation points, plus zero and one generic point. + candidates = {Q(0), Q(1)} | {2 * row[j] for j in slots if row[j]} + need(len(candidates) <= 4, "bounded candidate set") + costs = [(nnz(corrected(row, t, slots)), t) for t in sorted(candidates)] + best = min(cost for cost, _ in costs) + active = min((cost, t) for cost, t in costs if t) + need([t for cost, t in costs if cost == best] == [Q(0)], + "unique optimum must ignore query") + return best, active + + +def check_identity(original, replacement, slots): + need(len(original) == len(replacement) == 112, "matrix rows") + for old, new in zip(original, replacement, strict=True): + need(len(old) == 8 and len(new) == 9, "matrix columns") + actual = [new[j] + new[8] / 2 if j in slots else new[j] + for j in range(8)] + need(actual == old, "exact formal centre identity") + + +def execute(matrix, centres, targets, reverse=False): + need(len(centres) == 9 and len(targets) == 112, "execution domain") + output = targets[:] + sign = -1 if reverse else 1 + for i, row in enumerate(matrix): + for value, source in zip(row, centres, strict=True): + if value: + output[i] += sign * value * source + return output + + +def expect_failure(action): + try: + action() + except (AssertionError, ValueError): + return + raise AssertionError("control was accepted") + + +def controls(rows, witness, slots): + bad = [row[:] for row in witness] + chosen = next(i for i, row in enumerate(bad) if row[8]) + bad[chosen][8] = 0 + expect_failure(lambda: check_identity(rows, bad, slots)) + bad = [row[:] for row in witness] + bad[chosen][slots[0]] += Q(1, 4) + expect_failure(lambda: check_identity(rows, bad, slots)) + expect_failure(lambda: check_identity(rows, witness, slots[:-1])) + expect_failure(lambda: need(sum(nnz(row) for row in witness) == 176, + "query use increases support cost")) + # Without the two-zero premise a query really can save terms. + dense = [Q(1, 4) if j in slots else Q(0) for j in range(8)] + need(nnz(corrected(dense, Q(1, 2), slots)) == 1 < nnz(dense), + "dense changed-contract positive control") + expect_failure(lambda: scatter({"cut": [["add", 111, 61, 1, 4, None]]})) + expect_failure(lambda: scatter({"cut": [["add", 112, 61, 1, 0, None]]})) + return 6 + + +def analyze(rows, slots): + types, minima, active, witnesses = Counter(), [], [], [] + for i, row in enumerate(rows): + values = [row[j] for j in slots if row[j]] + need(len(values) <= 2, "at least two absent query centres in each row") + kind = ("zero" if not values else "single" if len(values) == 1 + else "same" if values[0] == values[1] else "opposite") + types[kind] += 1 + best, (cost, t) = row_optimum(row, slots) + minima.append(best) + active.append(cost) + if cost - best == 1: + witnesses.append((i, t)) + need(types == {"zero": 40, "single": 56, "same": 8, "opposite": 8}, + "complete row census") + need(sum(minima) == 176 and len(witnesses) == 8, "exact optima") + need(Counter(b - a for a, b in zip(minima, active, strict=True)) + == {1: 8, 2: 8, 3: 56, 5: 40}, "all row activation penalties") + integers = [[int(4 * value) for value in row] for row in rows] + answers, cases = support_oracle(integers, slots) + need(answers == list(zip(minima, active, strict=True)), "support oracle") + return types, witnesses, cases + + +def dirty_checks(rows, matrix, slots): + for column in range(8): + centres = [Q(int(j == column)) for j in range(8)] + query = sum(centres[j] for j in slots) / 2 + dirty = [Q((7 * j) % 23 - 11, j % 5 + 1) for j in range(112)] + readouts = centres + [query] + saved = readouts[:] + output = execute(matrix, readouts, dirty) + expected = [dirty[j] + rows[j][column] for j in range(112)] + need(output == expected and readouts == saved, "dirty endpoint") + need(execute(matrix, readouts, output, reverse=True) == dirty, + "literal reverse ADD restoration") + need(readouts == saved, "reverse readout restoration") + + +def main(): + rows = scatter(read_inputs()) + slots = tuple(CENTRES.index(c) for c in QUERY_CENTRES) + types, witnesses, cases = analyze(rows, slots) + matrix = [row + [Q(0)] for row in rows] + index, coefficient = witnesses[0] + matrix[index] = corrected(rows[index], coefficient, slots) + check_identity(rows, matrix, slots) + need(sum(nnz(row) for row in matrix) == 177, "attaining forced-query matrix") + dirty_checks(rows, matrix, slots) + rejected = controls(rows, matrix, slots) + receipt = { + "status": "PASS_P111_REDUNDANT_QUERY_SCATTER", "claim_type": "scoped proof", + "unrestricted_minimum": 176, "query_used_minimum": 177, + "query_free_optimum_unique": True, "row_types": dict(types), + "optimal_query_receivers": [112 + i for i, _ in witnesses], + "witness_receiver": 112 + index, + "witness_query_coefficient": str(coefficient), + "support_subsets_checked": cases, "rejection_controls": rejected, + "dirty_basis_cases": 8, "dense_scope_control": "4 terms to 1", + "python": sys.version, "platform": platform.platform(), "no_new_kappa": True, + "sha256": {name: hashlib.sha256(read_bytes(name)).hexdigest() for name in FILES}, + } + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()