diff --git a/research/qq16-dyadic-unread-minors/README.md b/research/qq16-dyadic-unread-minors/README.md new file mode 100644 index 0000000000..caafa962ce --- /dev/null +++ b/research/qq16-dyadic-unread-minors/README.md @@ -0,0 +1,181 @@ +# Dyadic admission of QQ16 unread minors + +This is a scoped scalar-admission result submitted for review, not a supplier +or a new kappa. + +The unread basis used by [PR2443](https://github.com/CrocSwap/integer-mult-bounds/pull/2443), +`H0=[1,2,3,4,5,6,8,12]`, has determinant `-32` and a dyadic inverse. It passes the +check below. However, replacing just unread port 2 by port 25 gives a rationally +invertible minor with determinant `-80` and inverse entry `1/10`. That read set +cannot support a finite dyadic-linear decoder for all original inputs under the +same two-cut observations, even when access and retention are free. + +This does not contradict PR2443. Its specific basis is dyadic, its theorem is +rational, and it does not claim native execution. The new contribution is the +explicit alternative-set obstruction and a complete local census, useful before +optimizing which ports to leave unread. + +## Domain and result + +Use the actual integer `8 x 112` query matrix R and ordinary set U96 from the +retained [QQ16 packet](../joint-query/README.md). For an unread set H of size eight, +consider exact inversion of + +```text +w = R_H D_(2,H) x1_H, +x1_H = D_(2,H)^(-1) R_H^(-1) w. +``` + +The order is the one in PR2443. Each port's cover map must be undone after scalar +inversion. No commutation of the different port maps is assumed. + +Let `D=Z[1/2]`. An integer square matrix is invertible over D if and only if its +determinant is a unit of D, namely a signed power of two. Sufficiency follows +from the adjugate formula. Necessity follows by taking determinants of a left +inverse. Thus nonsingularity alone is insufficient for dyadic scalar admission. +The same odd-factor obstruction holds with Gaussian-dyadic coefficients. + +The exact census includes every unread set at exchange distance at most two +from H0. No random sampling is used. + +| Distance | Sets | Singular | Dyadic-unit determinant | Nonzero odd-factor determinant | +| --- | ---: | ---: | ---: | ---: | +| 0 | 1 | 0 | 1 | 0 | +| 1 | 704 | 185 | 485 | 34 | +| 2 | 107184 | 46180 | 58537 | 2467 | +| Total | 107889 | 46365 | 59023 | 2501 | + +The nonzero absolute determinants are `16,32,48,64,80,96`. The odd-factor values +are `48,80,96`. [RESULT.json](RESULT.json) contains every histogram, both complete +inverses and the counterexample. This is not a census of all eight-subsets of U96. +A unit determinant admits the scalar inverse, not a native read or a favorable bill. + +## A counterexample for the complete two-cut decoder + +The observation contract is exactly PR2443's. Retain `x1_A/T`, `y1_A/T` after +complete F0, read `x1_(U\H)` there, and retain `y2_A` and `C=x2_U` immediately +after B1. There is no intervening modification. No `y2_U` or additional original +input is observed. Here A and T are the retained selected sets. + +Use this order for the alternative unread ports and integer vector: + +```text +H = [1,25,3,4,5,6,8,12], +z = [1,2,1,1,1,1,3,-2]. +``` + +Exact multiplication gives `R_H z=10 e_1`, where centre coordinates are zero-indexed. +Set all owner and payload values constant, so every cover map acts as the identity. +Writing `P_A=R_A^T/4` and `q=10 e_1`, initialize + +```text +x_U = iota_H z, x_A = -P_A q, x_T = 0, +y_U = 0, y_A = P_A q, y_T = 0. +``` + +These are valid dyadic inputs, including the selected dirt. Since `R_A P_A=I`, +the first forward query is zero. The conserved F0 equations give + +```text +x1_U = y1_U = iota_H z, +x1_A = x1_T = y1_A = y1_T = 0. +``` + +At B1, its future logger gives `y2_A=P_A q` and its ordinary target subtraction +gives `C=0`. All 88 read coordinates vanish. Hence all allowed observations are +zero except `y2_A=(5/2) R_A^T e_1`. Every observed coordinate belongs to the ideal +`5D`, but the required original `x_1` equals 1. + +A finite D-linear circuit preserves `5D`. Therefore no such circuit can decode +all original inputs from these observations. The argument also covers finite +Gaussian-dyadic linear operations and owner permutations. The ideal `5D[i]` is +proper, as reduction modulo five with `i -> 2` maps 1 to 1 and five to zero. Extra dirty workspace or affine constants do not help a linear +implementation: compare the displayed input with the zero input using identical +workspace and subtract the two executions. The observation difference stays in +the ideal while the required output difference is 1. + +A frame change is covered only if its coefficients are separately shown to lie +in the proved ring. Normalized Clifford coefficients such as `1/sqrt(2)` are +outside `D[i]` and are not covered here. No binding of the complete native gate +alphabet to this ring is supplied, and no claim that all native operations are +Gaussian-dyadic is made. + +This is not an information-loss witness over Q. The rational inverse exists, +and its row 0, column 1 entry is `1/10`. Nor is it an obstruction to restoring +only the selected original inputs. In this displayed family those selected +inputs are already determined dyadically by `y2_A`. The claim concerns complete +input recovery, as in PR2443, under the fixed observations and coefficient ring. +Nonlinear exact integer division, odd-denominator gates, new observations or a +changed first pair are outside the result. + +## Reproduce + +Python 3.12 or later, standard library only: + +```sh +python3.12 -I -B scripts/research_package.py --package research/qq16-dyadic-unread-minors +python3.12 -I -O -B research/qq16-dyadic-unread-minors/verify.py +``` + +The registered replay checks source pins and runs: + +- `verify.py`, using the one-/two-column determinant lemma, exact Fraction + elimination, two inverse orders and the constant-owner two-cut witness; +- `oracle.py`, importing no primary verifier or pending PR code, using direct + fraction-free elimination on all 107889 matrices and adjugate cofactors for + both inverses; +- `test_verify.py`, checking optimized replay, a Git-free source export and + rejection of source corruption, receipt type corruption, a missing receipt + and an altered histogram. + +The six mathematical controls include a singular minor, a wrong inverse sign, +an odd denominator, treating every nonzero determinant as a dyadic unit, a +changed modular vector and a duplicate unread port. Default replay writes no +artifacts. `verify.py --emit` explicitly emits a new complete receipt to stdout. + +[SOURCES.json](SOURCES.json) pins retained main inputs at +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. Pending PRs are attribution and +contract context, not runtime dependencies. Native replay, chronological +retention, child hosting, precision, tape, all-size admission and the complete +supplier invoice are not established. The separate retained QQ16 local replay +was run as a baseline, not as verification of a new native decoder. + +## Engineering limits + +All loops have fixed finite domains: matrix dimension at most eight, 112 ports, +and 107889 streamed candidates. Python uses dynamic allocation and arbitrary-size +integers. This is a managed-runtime deviation from fixed steady-state allocation. +The exact hash-bound source, fixed matrix sizes and streamed census bound live +state; no list of all candidates is retained. Parser sizes are checked before +hashing/decompression. Functions stay below 60 physical lines. Direct and +optimized replays, warning-enabled tests and a second determinant algorithm are +the available interpreted-code checks. A future broader domain must add explicit +input bounds and recheck resource limits rather than reuse this bounded receipt. + +## Open next questions + +Can a dyadic-unit unread basis reduce a complete native decoder's cost? First +for a dyadic-linear implementation, filter candidate read sets by the determinant +gate, then compare actual endpoint frames and the full read, chart-map, retention +and cleanup invoice. The blocker +is physical access and sustainable retention, not nonsingularity. The original +PR2443 basis already passes the dyadic check. No broader search is justified by +this finite census alone. [TASK.json](TASK.json) records the structured handoff. + +## Credit + +Gareth Davidson's PR2432 supplies the unread-column criterion and H0, pinned at +`cbede349fc764aa38379aa533befe3215916cfcd`. starship-s's PR2443 supplies the +arbitrary-input rational decoder and explicit two-cut contract, pinned at +`545c05e17243c962b112b91e7f84b4c1a41de7b8`. thakrarsagar's PR2470, +`1b2eee3bf1ec67e68c0b0fa7f47c7b2a66febe56`, is the separate retention census. +None is adopted as a supplier or represented as independently reviewed here. + +Ali Romman and the retained QQ16 contributors supply the matrix, selected +sections, conserved maps and cover semantics. Adam Gall, commdata2338, +kyzer1023 and the coordinate-read predecessors retain their information-bound +credit. Rohan Arun, Jeremy Kothe, DreamingOfClouds and the earlier supplier and +compiler lineage retain their attribution through the unchanged +[QQ16 notice](../joint-query/NOTICE.md). No predecessor executable is imported or +vendored. New work is Apache-2.0. No independent human or proof-assistant review +is claimed. diff --git a/research/qq16-dyadic-unread-minors/RESULT.json b/research/qq16-dyadic-unread-minors/RESULT.json new file mode 100644 index 0000000000..b472c02eff --- /dev/null +++ b/research/qq16-dyadic-unread-minors/RESULT.json @@ -0,0 +1,307 @@ +{ + "absolute_determinant_histograms_by_distance": [ + { + "32": 1 + }, + { + "0": 185, + "16": 330, + "32": 145, + "48": 32, + "64": 10, + "80": 2 + }, + { + "0": 46180, + "16": 44809, + "32": 13168, + "48": 2385, + "64": 560, + "80": 78, + "96": 4 + } + ], + "certificate": { + "bad_determinant": -80, + "bad_inverse": [ + [ + "0", + "1/10", + "2/5", + "-3/10", + "-3/10", + "0", + "-1/10", + "-1/5" + ], + [ + "1/2", + "1/5", + "-1/5", + "-1/10", + "-1/10", + "0", + "-1/5", + "1/10" + ], + [ + "0", + "1/10", + "-1/10", + "1/5", + "-3/10", + "0", + "2/5", + "3/10" + ], + [ + "0", + "1/10", + "-1/10", + "1/5", + "1/5", + "-1/2", + "-1/10", + "-1/5" + ], + [ + "0", + "1/10", + "-1/10", + "1/5", + "1/5", + "1/2", + "-1/10", + "-1/5" + ], + [ + "-1/2", + "1/10", + "2/5", + "1/5", + "1/5", + "0", + "-1/10", + "3/10" + ], + [ + "0", + "3/10", + "-3/10", + "-2/5", + "1/10", + "0", + "1/5", + "-1/10" + ], + [ + "1/2", + "-1/5", + "1/5", + "1/10", + "1/10", + "0", + "1/5", + "-1/10" + ] + ], + "bad_ports_ordered": [ + 1, + 25, + 3, + 4, + 5, + 6, + 8, + 12 + ], + "base_determinant": -32, + "base_inverse": [ + [ + "-1/4", + "0", + "1/2", + "-1/4", + "-1/4", + "0", + "0", + "-1/4" + ], + [ + "5/4", + "1/2", + "-1/2", + "-1/4", + "-1/4", + "0", + "-1/2", + "1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "-1/4", + "0", + "1/2", + "1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "1/4", + "-1/2", + "0", + "-1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "1/4", + "1/2", + "0", + "-1/4" + ], + [ + "1/2", + "1/2", + "0", + "0", + "0", + "0", + "-1/2", + "1/2" + ], + [ + "-3/4", + "0", + "0", + "-1/4", + "1/4", + "0", + "1/2", + "-1/4" + ], + [ + "-1/4", + "-1/2", + "1/2", + "1/4", + "1/4", + "0", + "1/2", + "-1/4" + ] + ], + "base_ports_ordered": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 12 + ], + "exchange": { + "inserted": 25, + "removed": 2 + }, + "integer_image": [ + 0, + 10, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "integer_vector": [ + 1, + 2, + 1, + 1, + 1, + 1, + 3, + -2 + ], + "modular_prime": 5, + "non_dyadic_inverse_entry": { + "column": 1, + "row": 0, + "value": "1/10" + } + }, + "classification_totals": { + "dyadic_unit": 59023, + "odd_factor": 2501, + "singular": 46365 + }, + "constant_two_cut_witness": { + "constant_owner_and_payload": true, + "observed_y2_A": [ + "5/2", + "-5/2", + "0", + "5/2", + "0", + "0", + "-5/2", + "0" + ], + "observed_y2_A_order": [ + 0, + 7, + 20, + 27, + 36, + 46, + 57, + 111 + ], + "other_observed_arrays_zero": 216, + "query_image": [ + "0", + "10", + "0", + "0", + "0", + "0", + "0", + "0" + ], + "required_original_X_port": 1, + "required_value": "1" + }, + "domain": { + "maximum_exchanges": 2, + "ports": 96, + "sets": 107889, + "sets_at_distance": [ + 1, + 704, + 107184 + ], + "unread": 8 + }, + "payload_sha256": "2efe83c59978aa9c0db2c3e4eccc14cbfdcd3c9ce499432601b5dd34083472ef", + "rejecting_controls": [ + "singular minor", + "wrong inverse sign", + "odd denominator", + "nonzero determinant is not a dyadic unit", + "changed modular vector", + "duplicate unread port" + ], + "schema_version": 1, + "scope": "Dyadic-linear complete-input decoding under the PR2443 two-cut contract; not a selected-input obstruction, native implementation or supplier.", + "source_sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "status": "PASS_QQ16_DYADIC_UNREAD_MINORS" +} diff --git a/research/qq16-dyadic-unread-minors/SOURCES.json b/research/qq16-dyadic-unread-minors/SOURCES.json new file mode 100644 index 0000000000..fb2c688730 --- /dev/null +++ b/research/qq16-dyadic-unread-minors/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/source_data.py", + "usage": "input", + "git_blob": "c9d465ed47500304bef65fcb588befe356c5cf09", + "sha256": "d23924511e3aed41e5e64511ca70126a636d91c8aa02e656cb61d6ceca1fe0a0" + } + ] +} diff --git a/research/qq16-dyadic-unread-minors/TASK.json b/research/qq16-dyadic-unread-minors/TASK.json new file mode 100644 index 0000000000..03e65a9e76 --- /dev/null +++ b/research/qq16-dyadic-unread-minors/TASK.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "joint-query-controller", + "question": "Can one explicitly changed QQ16 interface recover the missing chart query and close a two-call controller within a favorable full budget?", + "starting_points": [ + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Add one explicitly priced ordinary-to-selected observation and derive the ordered two-call map and inverse.", + "Change the first local pair or retained state, then test the existing lost-observation witness and price all new operations." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the fixed-first-pair QQ16 witness before designing a controller. The checked #1969 local words do not evade that witness or supply global placement.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Apply the existing witness to one proposed extra observation or changed first pair. If it still loses the required record, stop. Otherwise derive one ordered two-call identity and charge the added read, chart maps and restoration before extending to more stages.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969" + ] + }, + "scope_status": "changed", + "actual_scope": "Classify exact dyadic inversion of unread-eight centre minors at exchange distance at most two from PR2443's basis, and test complete-input recovery under its retained two-cut observation contract.", + "scope_change_reason": "Live overlap already answers the initial paid-B2 repair question. One bounded pivot audits scalar-ring admission for the alternative coordinate read sets suggested by PR2432 and PR2443, rather than constructing or claiming a completed controller.", + "bottleneck_link": "A side result on the native-admission obligation: rational information recovery does not imply that a dyadic-only linear circuit realizes the decoder. It supplies a determinant filter before read-set route/storage optimization; it does not improve the supplier budget.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact 107889-set radius-two census, one explicit modular obstruction, a dyadic positive control, a separate direct determinant oracle and corruption checks. No larger search or second research pivot.", + "outcome": "negative-result", + "evidence": "RESULT.json records 59023 dyadic-unit, 2501 odd-factor and 46365 singular minors, the exact two-sided inverses and the constant-owner two-cut obstruction. verify.py and oracle.py independently recompute every determinant histogram; test_verify.py exercises entrypoint failures.", + "author": "Nick Petalas", + "ai_assistance": "Substantial computational assistance in implementation and verification; no independent human or proof-assistant review is claimed.", + "scope_key": "qq16-coordinate-cut-decoder/unread8-radius2/dyadic-inverse-admission", + "predecessors": [ + {"pr": 1969, "source": "research/joint-query on pinned main", "credit": "Ali Romman and the retained QQ16 lineage"}, + {"pr": 2432, "head": "cbede349fc764aa38379aa533befe3215916cfcd", "credit": "Gareth Davidson, unread-column independence and basis"}, + {"pr": 2443, "head": "545c05e17243c962b112b91e7f84b4c1a41de7b8", "credit": "starship-s, arbitrary-input retained-cut rational decoder"}, + {"pr": 2470, "head": "1b2eee3bf1ec67e68c0b0fa7f47c7b2a66febe56", "credit": "thakrarsagar, separate cut-retention audit"} + ], + "publication_status": "Prepared for public review; no maintainer acceptance claimed.", + "freshness": { + "upstream_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "upstream_checked_utc": "2026-10-15T13:29:22Z", + "priority_revision": 4, + "open_pr_snapshot_utc": "2026-10-15T13:29:30.952161+00:00", + "open_pr_count": 719, + "discussion_snapshot_utc": "2026-10-15T13:31:28.472828+00:00", + "discussion_records": 1208, + "complete_pagination": true, + "guidance_selected_and_predecessor_heads": "Unchanged at final checkpoint; relevant exact PR heads rechecked through GraphQL. Helper coverage excludes arbitrary code diffs and is not a novelty certificate." + }, + "open_questions": [ + { + "question": "Among dyadic-unit unread bases, does one admit a cheaper complete native decoder than the retained basis?", + "why_it_matters": "The determinant gate removes algebraically illegal alternatives before optimizing actual read, frame-map and storage costs.", + "first_step": "Filter candidate read sets by dyadic-unit determinant, then compare their actual chronological endpoint frames and the full read/map/retention/cleanup invoice.", + "blocked_by": "No legal native read, sustainable cut retention, recursive precision or complete supplier invoice is supplied here. The original PR2443 basis already passes the dyadic test." + } + ] +} diff --git a/research/qq16-dyadic-unread-minors/VERIFY.json b/research/qq16-dyadic-unread-minors/VERIFY.json new file mode 100644 index 0000000000..58ee023f33 --- /dev/null +++ b/research/qq16-dyadic-unread-minors/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/source_data.py" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Exact determinant-lemma census, two-sided dyadic and rational inverse controls, and constant-owner two-cut modular obstruction." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/oracle.py"], + "timeout_seconds": 60, + "checks": "Separate direct Bareiss census of all 107889 sets and cofactor reconstruction of both complete inverses, with no primary-verifier import." + }, + { + "argv": ["{python}", "-I", "-B", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "Optimized Git-free source export; corrupted source, receipt type, missing receipt and mutated determinant histogram must reject." + } + ] +} diff --git a/research/qq16-dyadic-unread-minors/oracle.py b/research/qq16-dyadic-unread-minors/oracle.py new file mode 100644 index 0000000000..6a30d1f014 --- /dev/null +++ b/research/qq16-dyadic-unread-minors/oracle.py @@ -0,0 +1,113 @@ +#!/usr/bin/env python3 +"""Direct integer-elimination oracle. Imports no primary verifier code. Apache-2.0.""" + +import argparse +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations +import gzip +import json +from pathlib import Path + + +SOURCE = "research/joint-query/certificate.json.gz" +DIGEST = "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" +BASE = (1, 2, 3, 4, 5, 6, 8, 12) +HERE = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def determinant(matrix): + """Fraction-free elimination, including row-pivot sign and exact division.""" + n = len(matrix) + need(1 <= n <= 8 and all(len(row) == n for row in matrix), "matrix shape") + work = [row[:] for row in matrix] + previous, sign = 1, 1 + for k in range(n - 1): + pivot_row = next((i for i in range(k, n) if work[i][k]), None) + if pivot_row is None: + return 0 + if pivot_row != k: + work[k], work[pivot_row] = work[pivot_row], work[k] + sign = -sign + pivot = work[k][k] + for i in range(k + 1, n): + for j in range(k + 1, n): + value = work[i][j] * pivot - work[i][k] * work[k][j] + quotient, remainder = divmod(value, previous) + need(remainder == 0, "nonexact Bareiss division") + work[i][j] = quotient + work[i][k] = 0 + previous = pivot + return sign * work[-1][-1] + + +def adjugate_inverse(matrix): + det = determinant(matrix) + need(det != 0, "singular adjugate input") + result = [] + for i in range(8): + row = [] + for j in range(8): + submatrix = [[matrix[a][b] for b in range(8) if b != i] + for a in range(8) if a != j] + cofactor = (-1) ** (i + j) * determinant(submatrix) + row.append(str(Fraction(cofactor, det))) + result.append(row) + return result + + +def direct_census(matrix, ordinary): + outside = tuple(p for p in ordinary if p not in BASE) + need(len(outside) == 88 and len(set(ordinary)) == 96, "ordinary alphabet") + histograms = [] + for distance in range(3): + counts = Counter() + for removed in combinations(BASE, distance): + retained = tuple(p for p in BASE if p not in removed) + for inserted in combinations(outside, distance): + ports = retained + inserted + square = [[row[p] for p in ports] for row in matrix] + counts[abs(determinant(square))] += 1 + histograms.append({str(d): count for d, count in sorted(counts.items())}) + return histograms + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=HERE.parents[1]) + parser.add_argument("--receipt", type=Path, default=HERE / "RESULT.json") + args = parser.parse_args() + path = args.repo / SOURCE + need(path.stat().st_size <= 8_000_000, "oversize input") + raw = path.read_bytes() + need(sha256(raw).hexdigest() == DIGEST, "oracle source pin differs") + packet = json.loads(gzip.decompress(raw)) + matrix = [[int(row.get(str(p), "0")) for p in range(112)] + for row in packet["R_rows"]] + need(len(matrix) == 8, "query dimension") + receipt = json.loads(args.receipt.read_text(encoding="utf-8")) + histograms = direct_census(matrix, tuple(packet["U_ports"])) + need(histograms == receipt["absolute_determinant_histograms_by_distance"], + "direct census and determinant lemma disagree") + certificate = receipt["certificate"] + for prefix in ("base", "bad"): + ports = certificate[prefix + "_ports_ordered"] + need(len(ports) == len(set(ports)) == 8, "certificate port shape") + square = [[row[p] for p in ports] for row in matrix] + need(determinant(square) == certificate[prefix + "_determinant"], + "direct witness determinant disagrees") + need(adjugate_inverse(square) == certificate[prefix + "_inverse"], + "cofactor inverse disagrees") + need(determinant([[0, 1], [1, 0]]) == -1, "pivot-sign control") + need(determinant([[1, 2], [2, 4]]) == 0, "singular control") + print("PASS_QQ16_DIRECT_MINOR_ORACLE sets=107889 full_census_and_cofactor_inverses") + + +if __name__ == "__main__": + main() diff --git a/research/qq16-dyadic-unread-minors/test_verify.py b/research/qq16-dyadic-unread-minors/test_verify.py new file mode 100644 index 0000000000..d01808929a --- /dev/null +++ b/research/qq16-dyadic-unread-minors/test_verify.py @@ -0,0 +1,78 @@ +#!/usr/bin/env python3 +"""Exercise the public checker commands, including deliberate corruptions.""" + +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = "research/joint-query/certificate.json.gz" + + +def run(script, *arguments, optimized=False): + command = [sys.executable, "-I", "-B"] + if optimized: + command.append("-O") + return subprocess.run(command + [str(HERE / script), *map(str, arguments)], + capture_output=True, text=True, timeout=30, check=False) + + +class EntryPointTests(unittest.TestCase): + def test_optimized_and_git_free_source_export(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + source = root / SOURCE + source.parent.mkdir(parents=True) + source.write_bytes((ROOT / SOURCE).read_bytes()) + before = source.read_bytes() + result = run("verify.py", "--repo", root, optimized=True) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("sets=107889 dyadic=59023 odd_factor=2501", result.stdout) + self.assertEqual(source.read_bytes(), before) + self.assertFalse((root / ".git").exists()) + + def test_source_corruption_rejected(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + source = root / SOURCE + source.parent.mkdir(parents=True) + raw = (ROOT / SOURCE).read_bytes() + source.write_bytes(raw[:-1] + bytes([raw[-1] ^ 1])) + result = run("verify.py", "--repo", root, "--emit", optimized=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn("packet source pin differs", result.stderr) + + def test_receipt_type_corruption_rejected(self): + receipt = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + receipt["schema_version"] = True + with tempfile.TemporaryDirectory() as temporary: + path = Path(temporary) / "RESULT.json" + path.write_text(json.dumps(receipt), encoding="utf-8") + result = run("verify.py", "--receipt", path, optimized=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn("receipt differs from complete recomputation", result.stderr) + + def test_missing_receipt_rejected(self): + with tempfile.TemporaryDirectory() as temporary: + result = run("verify.py", "--receipt", Path(temporary) / "absent.json") + self.assertNotEqual(result.returncode, 0) + self.assertIn("FileNotFoundError", result.stderr) + + def test_direct_oracle_rejects_histogram_corruption(self): + receipt = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + receipt["absolute_determinant_histograms_by_distance"][1]["48"] += 1 + with tempfile.TemporaryDirectory() as temporary: + path = Path(temporary) / "RESULT.json" + path.write_text(json.dumps(receipt), encoding="utf-8") + result = run("oracle.py", "--receipt", path) + self.assertNotEqual(result.returncode, 0) + self.assertIn("direct census and determinant lemma disagree", result.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-dyadic-unread-minors/verify.py b/research/qq16-dyadic-unread-minors/verify.py new file mode 100644 index 0000000000..bde851c6ae --- /dev/null +++ b/research/qq16-dyadic-unread-minors/verify.py @@ -0,0 +1,300 @@ +#!/usr/bin/env python3 +"""Exact dyadic-admission census for a fixed QQ16 unread-basis neighborhood. + +Standard library only. All validation remains active under -O. Apache-2.0. +""" + +import argparse +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import combinations +import gzip +import json +from pathlib import Path + + +PACKET = "research/joint-query/certificate.json.gz" +PACKET_SHA256 = "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" +PAYLOAD_SHA256 = "2efe83c59978aa9c0db2c3e4eccc14cbfdcd3c9ce499432601b5dd34083472ef" +BASE_PORTS = (1, 2, 3, 4, 5, 6, 8, 12) +BAD_PORTS = (1, 25, 3, 4, 5, 6, 8, 12) +KERNEL_VECTOR = (1, 2, 1, 1, 1, 1, 3, -2) +A_PORTS = (0, 7, 20, 27, 36, 46, 57, 111) +T_PORTS = (21, 37, 47, 76, 81, 87, 92, 110) +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def load_matrix(root): + path = root / PACKET + require(path.stat().st_size <= 8_000_000, "source container too large") + raw = path.read_bytes() + require(sha256(raw).hexdigest() == PACKET_SHA256, "packet source pin differs") + payload = gzip.decompress(raw) + require(sha256(payload).hexdigest() == PAYLOAD_SHA256, "packet payload differs") + packet = json.loads(payload) + require(len(packet["R_rows"]) == 8, "wrong query dimension") + matrix = [[Q(row.get(str(p), "0")) for p in range(112)] + for row in packet["R_rows"]] + require(all(x.denominator == 1 and abs(x) <= 1 + for row in matrix for x in row), "query matrix is not signed binary") + ordinary = tuple(packet["U_ports"]) + selected = tuple(packet["A_ports"] + packet["T_ports"]) + require(tuple(packet["A_ports"]) == A_PORTS + and tuple(packet["T_ports"]) == T_PORTS, "selected minors differ") + require(len(ordinary) == len(set(ordinary)) == 96, "wrong ordinary partition") + require(len(selected) == len(set(selected)) == 16, "wrong selected partition") + require(set(ordinary).isdisjoint(selected) + and set(ordinary + selected) == set(range(112)), "incomplete partition") + gram = [[sum(matrix[i][p] * matrix[j][p] for p in ordinary) + for j in range(8)] for i in range(8)] + require(gram == [[Q(48 * (i == j)) for j in range(8)] + for i in range(8)], "ordinary Gram differs") + for ports in (A_PORTS, T_PORTS): + selected_gram = [[sum(matrix[i][p] * matrix[j][p] for p in ports) + for j in range(8)] for i in range(8)] + require(selected_gram == [[Q(4 * (i == j)) for j in range(8)] + for i in range(8)], "selected Gram differs") + return matrix, ordinary + + +def minor(matrix, ports): + require(len(ports) == len(set(ports)) == 8, "minor needs eight distinct ports") + require(all(0 <= p < 112 for p in ports), "port outside matrix") + return [[row[p] for p in ports] for row in matrix] + + +def inverse(matrix): + """Return the rational inverse and signed determinant, or None and zero.""" + n = len(matrix) + require(n == 8 and all(len(row) == n for row in matrix), "expected 8x8 matrix") + work = [list(map(Q, row)) + [Q(i == j) for j in range(n)] + for i, row in enumerate(matrix)] + determinant = Q(1) + for i in range(n): + pivot = next((j for j in range(i, n) if work[j][i]), None) + if pivot is None: + return None, Q(0) + if pivot != i: + work[i], work[pivot] = work[pivot], work[i] + determinant = -determinant + value = work[i][i] + determinant *= value + work[i] = [x / value for x in work[i]] + for j in range(n): + if j != i: + value = work[j][i] + work[j] = [x - value * y for x, y in zip(work[j], work[i])] + return [row[n:] for row in work], determinant + + +def product(left, right): + return [[sum(left[i][k] * right[k][j] for k in range(8)) + for j in range(8)] for i in range(8)] + + +def identity(): + return [[Q(i == j) for j in range(8)] for i in range(8)] + + +def dyadic(value): + denominator = Q(value).denominator + return denominator & (denominator - 1) == 0 + + +def determinant_unit(value): + value = abs(Q(value)) + return bool(value) and dyadic(value) and dyadic(1 / value) + + +def integer(value): + value = Q(value) + require(value.denominator == 1, "nonintegral determinant or coordinate") + return value.numerator + + +def census(matrix, ordinary, base_inverse, base_determinant): + """Use the one-/two-column determinant lemma, with integral scaled coordinates.""" + outside = tuple(p for p in ordinary if p not in BASE_PORTS) + require(len(outside) == 88, "wrong exchange alphabet") + coordinates = { + p: [integer(4 * sum(base_inverse[i][k] * matrix[k][p] + for k in range(8))) for i in range(8)] + for p in outside + } + histograms = [Counter({abs(integer(base_determinant)): 1}), Counter(), Counter()] + for i in range(8): + for p in outside: + det = integer(base_determinant * coordinates[p][i] / 4) + histograms[1][abs(det)] += 1 + for i, j in combinations(range(8), 2): + for p, q in combinations(outside, 2): + small_det = (coordinates[p][i] * coordinates[q][j] + - coordinates[q][i] * coordinates[p][j]) + det = integer(base_determinant * small_det / 16) + histograms[2][abs(det)] += 1 + expected_counts = (1, 704, 107184) + require(tuple(sum(h.values()) for h in histograms) == expected_counts, + "exchange domain incomplete") + return [{str(d): count for d, count in sorted(h.items())} for h in histograms] + + +def witness(matrix): + base = minor(matrix, BASE_PORTS) + base_inverse, base_det = inverse(base) + require(base_det == -32, "base determinant differs") + require(product(base, base_inverse) == product(base_inverse, base) == identity(), + "base inverse differs") + require(all(dyadic(x) for row in base_inverse for x in row), + "positive base is not dyadically invertible") + bad = minor(matrix, BAD_PORTS) + bad_inverse, bad_det = inverse(bad) + require(bad_det == -80, "obstructed determinant differs") + require(product(bad, bad_inverse) == product(bad_inverse, bad) == identity(), + "rational inverse does not exist") + image = [integer(sum(row[j] * KERNEL_VECTOR[j] for j in range(8))) + for row in bad] + require(image == [0, 10, 0, 0, 0, 0, 0, 0], "mod-five certificate differs") + require(KERNEL_VECTOR[0] % 5 != 0 and all(x % 5 == 0 for x in image), + "mod-five kernel is trivial") + require(bad_inverse[0][1] == Q(1, 10), "non-dyadic coefficient differs") + require(not determinant_unit(bad_det) + and not all(dyadic(x) for row in bad_inverse for x in row), + "bad example admits a dyadic inverse") + return base_inverse, base_det, { + "base_ports_ordered": list(BASE_PORTS), + "base_determinant": integer(base_det), + "base_inverse": [[str(x) for x in row] for row in base_inverse], + "bad_ports_ordered": list(BAD_PORTS), + "exchange": {"removed": 2, "inserted": 25}, + "bad_determinant": integer(bad_det), + "bad_inverse": [[str(x) for x in row] for row in bad_inverse], + "modular_prime": 5, "integer_vector": list(KERNEL_VECTOR), + "integer_image": image, + "non_dyadic_inverse_entry": {"row": 0, "column": 1, "value": "1/10"}, + } + + +def cut_witness(matrix, ordinary): + """Replay the constant-owner two-cut family, including its selected dirt.""" + def query(values, ports): + return [sum(row[p] * values[p] for p in ports) for row in matrix] + + def section(q, p): + return sum(matrix[k][p] * q[k] for k in range(8)) / 4 + + selected = A_PORTS + T_PORTS + x, y = [Q(0)] * 112, [Q(0)] * 112 + for p, value in zip(BAD_PORTS, KERNEL_VECTOR): + x[p] = Q(value) + q = query(x, ordinary) + for p in A_PORTS: + x[p], y[p] = -section(q, p), section(q, p) + f, c = query(x, range(112)), query(x, T_PORTS) + require(f == c == [Q(0)] * 8, "constant-family F0 driver differs") + x1, y1 = x[:], y[:] + for p in ordinary: + x1[p] = x[p] - section(f, p) + y1[p] = y[p] + x1[p] + for p in selected: + x1[p] = section(c if p in A_PORTS else f, p) + y1[p] = x[p] + y[p] - x1[p] + u = y1[:] + future = query(y1, range(112)) + for p in A_PORTS: + u[p] = section(future, p) + # The exact B1 equations give y2_A=u_A and C=x1_U-y1_U. + observed_a = [u[p] for p in A_PORTS] + observed_other = ([x1[p] for p in ordinary if p not in BAD_PORTS] + + [x1[p] for p in selected] + [y1[p] for p in selected] + + [x1[p] - y1[p] for p in ordinary]) + require(all(value == 0 for value in observed_other), "other cut records nonzero") + require(any(observed_a) and all(dyadic(value / 5) for value in observed_a), + "observed records are not in the ideal 5 Z[1/2]") + require(x[BAD_PORTS[0]] == 1, "required output has no unit coordinate") + return {"constant_owner_and_payload": True, + "observed_y2_A_order": list(A_PORTS), + "observed_y2_A": [str(value) for value in observed_a], + "other_observed_arrays_zero": len(observed_other), + "required_original_X_port": BAD_PORTS[0], "required_value": "1", + "query_image": [str(value) for value in q]} + + +def controls(matrix, base_inverse): + duplicate = minor(matrix, BASE_PORTS) + for row in duplicate: + row[1] = row[0] + require(inverse(duplicate) == (None, Q(0)), "singular control accepted") + wrong = [row[:] for row in base_inverse] + wrong[0][0] = -wrong[0][0] + require(product(wrong, minor(matrix, BASE_PORTS)) != identity(), + "wrong inverse control accepted") + require(dyadic(Q(1, 4)) and not dyadic(Q(1, 10)), "denominator control failed") + require(determinant_unit(-32) and not determinant_unit(-80), + "nonzero-as-unit control accepted") + changed = list(KERNEL_VECTOR) + changed[0] += 1 + image = [sum(row[j] * changed[j] for j in range(8)) + for row in minor(matrix, BAD_PORTS)] + require(any(x % 5 for x in image), "changed modular witness accepted") + try: + minor(matrix, BASE_PORTS[:-1] + (BASE_PORTS[0],)) + except ValueError: + pass + else: + raise ValueError("duplicate-port control accepted") + return ["singular minor", "wrong inverse sign", "odd denominator", + "nonzero determinant is not a dyadic unit", "changed modular vector", + "duplicate unread port"] + + +def report(root): + matrix, ordinary = load_matrix(root) + base_inverse, base_det, certificate = witness(matrix) + histograms = census(matrix, ordinary, base_inverse, base_det) + totals = Counter() + for histogram in histograms: + for det, count in histogram.items(): + label = ("singular" if det == "0" else + "dyadic_unit" if determinant_unit(int(det)) else "odd_factor") + totals[label] += count + require(dict(totals) == {"dyadic_unit": 59023, "singular": 46365, + "odd_factor": 2501}, "census totals differ") + return { + "schema_version": 1, "status": "PASS_QQ16_DYADIC_UNREAD_MINORS", + "source_sha256": PACKET_SHA256, "payload_sha256": PAYLOAD_SHA256, + "domain": {"ports": 96, "unread": 8, "maximum_exchanges": 2, + "sets": 107889, "sets_at_distance": [1, 704, 107184]}, + "absolute_determinant_histograms_by_distance": histograms, + "classification_totals": dict(sorted(totals.items())), + "certificate": certificate, "constant_two_cut_witness": cut_witness(matrix, ordinary), + "rejecting_controls": controls(matrix, base_inverse), + "scope": "Dyadic-linear complete-input decoding under the PR2443 two-cut contract; not a selected-input obstruction, native implementation or supplier.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=ROOT) + parser.add_argument("--receipt", type=Path, default=PACKAGE / "RESULT.json") + parser.add_argument("--emit", action="store_true", help="emit a receipt without reading one") + args = parser.parse_args() + result = report(args.repo) + encoded = json.dumps(result, sort_keys=True, indent=2) + "\n" + if args.emit: + print(encoded, end="") + return + expected = json.loads(args.receipt.read_text(encoding="utf-8")) + require(json.dumps(expected, sort_keys=True, indent=2) + "\n" == encoded, + "receipt differs from complete recomputation") + print("PASS_QQ16_DYADIC_UNREAD_MINORS sets=107889 dyadic=59023 odd_factor=2501 singular=46365") + + +if __name__ == "__main__": + main()