diff --git a/research/qq16-shear-old-chart-kernel/README.md b/research/qq16-shear-old-chart-kernel/README.md new file mode 100644 index 0000000000..7521f66f70 --- /dev/null +++ b/research/qq16-shear-old-chart-kernel/README.md @@ -0,0 +1,251 @@ +# The QQ16 shear still loses selected inputs with a dense old-chart record + +Grant the paired A-to-T shear between F0 and B1 and retain the complete +ordinary old-chart query `q0 = B0 X_U^initial`. These changes still do not +restore all original selected inputs. For a finite regular cover of size +`N`, at least `ceil(32N/7)` dimensions of selected-input differences remain +invisible under the observation contract below. + +This is a scoped linear-algebra obstruction, not a new supplier or κ. +It answers the dense-observation handoff in [PR #2326](https://github.com/CrocSwap/integer-mult-bounds/pull/2326). +It does not claim that every dense query fails. The new step is a graph +intersection for the changed first pair; the three-query rank estimate +and ordinary-tail argument are credited predecessor results. + +## Exact scope + +Use the conserved F0 and B_1_2 maps from +[the retained QQ16 package](../joint-query/README.md), with its A, T and U +port sets, selected sections, owner action and ordinary tail. All arrays +are arbitrary over the rationals. Restrict the counterexamples to fields +constant in payload coordinates, but allow independent cover-owner values. +This preserves the actual owner action; it does not replace routes by a +nonfaithful quotient. + +After the complete F0, insert the logical paired shear from +[PR #2216](https://github.com/CrocSwap/integer-mult-bounds/pull/2216): + +```text +X_T <- X_T + C X_A +Y_T <- Y_T - C X_A. +``` + +Here `C` is the identity pairing from the eight ordered A fields to the +eight ordered T fields. No ordinary field changes. The proof also works +for any fixed invertible rational-linear `C` between those selected spaces. + +The observations are: + +- `q0 = B0 X_U^initial`, retained without loss; +- every selected output immediately after B1 and at all later cuts; +- all five forward-query histories; +- all final completed-X descendants under the retained endpoint typing. + +A separately retained transient F0 A/T output, a later ordinary read and +the final former-Y hole are **not** observations. Later homogeneous +selected-only linear controls are allowed. The observation record does +not feed back into ordinary state. The final decoder may be nonlinear: +two identical observation tuples still cannot have different answers. + +Grant the shear, read, storage, native frame conversions, address work, +cleanup, hosting and precision zero cost. Recovery fails even in this +favorable relaxation, so no construction or moment claim is made. In +particular, this does not adopt PR #2216's bare-scalar native pricing. + +## Ordered kernel construction + +Write `B_s = R_s iota_U` and `K_1 = K_(1,U)`, so `B1 K_1 = 12 I`. +Let `P0A = P_(0,A)`, `P0T = P_(0,T)` and `P1T = P_(1,T)`. +Every selected section and its selected query are two-sided inverses. +Define the following ordered maps from query coordinates: + +```text +L = ell_(1,T) C P0A +M = (ell_(2,A) + ell_(2,T) C) P0A. +``` + +`L` is invertible. Take a query vector `c` and an ordinary vector `w` +satisfying + +```text +B0 w = 0, +B1 w = -11 L c, +B2 w = M c. (1) +``` + +Only pair 0 is initially nonzero: + +```text +X_U = w, Y_U = 0, +X_A = -P0A c, Y_A = P0A c, +X_T = P0T c, Y_T = -P0T c. (2) +``` + +The other pairs and borrowed helpers may be set to zero: this is an +allowed subspace of an arbitrary-dirty-input contract. Both selected pair +sums vanish. The initial selected defect is injective in `c`. + +The F0 query is `f0 = B0 w - c + c = 0`. Its exact output is + +```text +X_U = Y_U = w, +X_A = P0A c, Y_A = -P0A c, +X_T = Y_T = 0. +``` + +After the shear, `X_T = C P0A c` and `Y_T = -C P0A c`. +Set `a = L c`. The future query at B1 is + +```text +q2 = R2 Y = B2 w - M c = 0. +``` + +The systematic logger `E2` therefore gives `u_A = P_(2,A) q2 = 0`, +`u_U = w` and `u_T = -C P0A c = -P1T a`. Consequently + +```text +b = R1 u = B1 w - a = -12a. +``` + +The conserved backward equations from the +[ordered QQ16 proof](../joint-query/evidence/JOINT-QUERY-TRANSFER.md) give + +```text +Y'_U = w + K_1 a = h, +Y'_A = 0, +Y'_T = u_T - P1T b - 11 P1T a = 0, +X'_U = w - w = 0, +X'_A = X'_T = 0. (3) +``` + +No operators have been commuted. The output (3) is exactly the +[retained witness's post-B1 form](../joint-query/evidence/QQ16-SELECTED-WITNESS.md), +with an arbitrary ordinary value `h`. That tail argument does not require +`B1 h = 0`: the first positive bridge puts `-h` in Y1, F2 has zero X +source, and the negative bridge removes `-h` before B3. Later active +pairs are zero. The terminal moves `h` to named final X0 with the +former-Y native type. Every selected output, forward history and +completed-X descendant is zero. Homogeneous selected-only controls keep +the selected state zero. + +Finally `q0 = B0 w = 0`. Thus every solution of (1) gives the same +allowed observations as the zero input, despite the selected defect (2). + +## Why nonzero solutions exist on the actual cover + +Let `S = [B0; B1; B2]`, a map into a `24N`-dimensional query space, +and let + +```text +H = { (0, -11 L c, M c) : c in Q^(8N) }. +``` + +Because `L` is invertible, `dim H = 8N`, and every vector of +`im S intersect H` determines a unique `c`. The elementary intersection +inequality gives + +```text +dim(im S intersect H) >= rank(S) + 8N - 24N + = rank(S) - 16N. (4) +``` + +Every vector in this intersection has a rational preimage `w`, so (4) +counts actual invisible selected defects, not just unconstrained query +values. The zero element is the only one with `c = 0`. + +The second-moment argument in [PR #2104](https://github.com/CrocSwap/integer-mult-bounds/pull/2104), +rebound to the retained packet by [PR #2153](https://github.com/CrocSwap/integer-mult-bounds/pull/2153), +gives `rank(S) >= 144N/7`. Its finite premises are rechecked here: + +```text +sum_(p in U) r_p r_p^T = 48 I_8, ||r_p||^2 = 4, +R_A R_A^T = R_T R_T^T = 4 I_8, +g_(s,p) g_(t,p)^-1 distinct for all 96 p, each s= (tr K)^2 / tr K^2 = 144N/7. +``` + +Combining this with (4) proves the stated `ceil(32N/7)` lower bound. +The dimension is across the full owner array, not a per-owner native +rank tariff. Clearing rational denominators and scaling yields dyadic +inputs of arbitrarily small nonzero magnitude. This proves existence; +it does not give a compact actual-cover vector or a precision bound. + +## Reproduce and verification boundary + +From the repository root, with Python 3.12 and the standard library: + +```sh +python3.12 scripts/research_package.py --package research/qq16-shear-old-chart-kernel +python3.12 -I -O -B research/qq16-shear-old-chart-kernel/verify.py +``` + +The checker binds the packet and proof inputs through [SOURCES.json](SOURCES.json), +checks the actual three-chart route distinctions and Gram identities, +and exercises (1)--(3) with exact rational noncommuting selected-section +fixtures. It also checks the retained formal-h tail and deliberate +failures. Finite fixtures do not prove the quantified intersection +argument; the proof is written above. + +The registered normal and optimized replays passed on CPython 3.12.13: +three sets of 96 relative routes, four rational basis fixtures, 17 tail +events and six rejection-control groups. A Git-free relocated optimized +replay preserved all 11 copied files; corrupting a copied source was +rejected by its digest check. Separate Astra/max agent reviews found no +blocking mathematical/spec or verifier-quality issue. These are agent +reviews, not independent human review. + +No pending executable is imported. The packet's reviewed scalar/native +binding is inherited, not cold-replayed. There is no full supplier replay, +proof-assistant check or independent human review. The stronger later +moment estimates are not needed or reverified here. The selected record +and all frozen sources remain unchanged. + +## Open next questions + +Can a changed first-pair interface make a *different* eight-coordinate +dense record sufficient? This matters because detecting a known witness +is weaker than closing the complete kernel. Start by writing its ordered +analogue of (1) and intersecting its query graph with `im S`. Actual +native access, retention and a favorable complete bill remain blockers +even if that algebra succeeds. + +Can one recover the privileged post-B1 selected cut used by +[PR #2174](https://github.com/CrocSwap/integer-mult-bounds/pull/2174) +from legal final records? Its two-record theorem is a different positive +contract. The first step is an ordered reconstruction of that cut; the +current obstruction neither supplies nor contradicts it. + +## Provenance and credit + +Base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +The accepted chooser nonce is `7dcbcbed93c608a2c89c3e8330a31a30`; +`joint-query-controller` is a refined scope on the recursive-interfaces track. +[Task metadata](TASK.json) records the claim, overlap and stopping rule. + +- Ali Romman, PR #1969 and the [retained notices](../joint-query/NOTICE.md): + local maps, selected sections, owner action and ordinary tail. +- Ross Richardson, PR #2104 `4bdc574da394a39f955e8cf4637075649c43a632`, + and commdata2338, PR #2153 `5646398dcdc01769df83b939c6b3eb5ecb4d5ebd`: + the three-query rank method and source-binding checks. +- Cinna Davis, PR #2216 `b80e9ba43367fb8b20877a97da1cb677c34f9264`: + the paired shear and its bounded witness-separation result; + PR #2122 `7045301a8c15eb4408e3e9d80969c9d50a914cde`: the mixed-helper + obstruction for the unchanged first pair. The new graph argument here + accounts for the intervening shear rather than reusing that trajectory. +- commdata2338, PR #2326 `fb7d64cd4a51c49bc56920305b0aca64011a420c`: + the coordinate-access obstruction and dense-query handoff; + PR #2174 `f79470a7931f3943360c10d15b428e0e4e479c22`: the adjacent + two-record recovery theorem and recorded-cut boundary. +- Adam Gall, PR #2093 `8b21a900eb520e4f11ea177b310f66316f8e8983`: + the common-axis witness family. The active coordinate-threshold and + whole-owner separation investigations concern that different family. + +Prepared by @starship-s with substantial Hermes and OpenAI Codex assistance. +New material is Apache-2.0. No predecessor result is claimed as new. diff --git a/research/qq16-shear-old-chart-kernel/SOURCES.json b/research/qq16-shear-old-chart-kernel/SOURCES.json new file mode 100644 index 0000000000..0e3cd112d2 --- /dev/null +++ b/research/qq16-shear-old-chart-kernel/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "research/community-reconciliation-third100-audit/regenerated/pr377-outputs/work/odd-stages/RECIPE-9.json.gz", + "usage": "input", + "git_blob": "a9e6f99d80c4d3c712535bad13086153eaf6ac3b", + "sha256": "910fffd7b8980f1130d8bbec56d5ac34f92986c2a2c480b6aea40754b4b832ac" + }, + { + "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/evidence/QQ16-COVER-ACTION-ADDENDUM.md", + "usage": "input", + "git_blob": "3dd1a990d7b9d57cfb20cf8e8dd45548f043a944", + "sha256": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "usage": "input", + "git_blob": "5082d791d0b993492cbc5bf61ac3b69e82c96f3f", + "sha256": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "usage": "input", + "git_blob": "307650f45e37c28d14fe913958efa4fb429242b7", + "sha256": "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc" + } + ] +} diff --git a/research/qq16-shear-old-chart-kernel/TASK.json b/research/qq16-shear-old-chart-kernel/TASK.json new file mode 100644 index 0000000000..51075db748 --- /dev/null +++ b/research/qq16-shear-old-chart-kernel/TASK.json @@ -0,0 +1,103 @@ +{ + "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": "refined", + "actual_scope": "QQ16 F0-to-B1 paired A-to-T shear with one retained dense old-chart record B0 X_U^initial: an ordered selected-input kernel obstruction under the retained post-B1 observation contract.", + "scope_change_reason": "Take PR2326's explicit dense-observation handoff. Unlike the concurrent fixed-coordinate and common-axis-family investigations, permit the full old-chart read and test a new graph-defined family of arbitrary original selected inputs.", + "bottleneck_link": "Rule out a specific apparently favorable query repair before spending effort on native implementation or a supplier invoice.", + "budget_minutes": 60, + "stop_rule": "Stop construction if a nonzero selected defect remains when the shear, query, retention, physical access and all additional costs are granted free. Do not change maps or observations to rescue this target.", + "outcome": "negative-result", + "evidence": "README ordered proof; verify.py rechecks actual source Grams and routes, the 144/7 rank premise and 32/7 defect bound, four exact rational basis fixtures, sharp fixture intersection, 17-event tail and six rejection-control groups. The proof is not inferred from the finite fixtures.", + "author": "starship-s", + "ai_assistance": "Substantial Hermes and OpenAI Codex assistance with proof, implementation and verification. No independent human or proof-assistant review is claimed.", + "chooser_seed": "7dcbcbed93c608a2c89c3e8330a31a30", + "track": "recursive-interfaces", + "selector_scope_key": "0e34adbc1dd119161c3a", + "refined_scope_key": "QQ16/shear-plus-initial-B0-read/ordered-graph-kernel", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2205#discussioncomment-18942212", + "overlap": { + "searched_at": "2026-10-15T06:06:32Z", + "open_prs": 559, + "discussion_records": 1067, + "complete_pagination": true, + "discussion_snapshot_at": "2026-10-15T06:03:23Z", + "limits": "Open PR bodies, Discussion bodies/comments/replies and local package notes, not arbitrary code diffs. The live canonical thread was also read before claiming. Search absence is not a novelty certificate." + }, + "submission_checkpoint": { + "upstream_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "checked_at_utc": "2026-10-15T06:39:28Z", + "open_prs": 572, + "discussion_records": 1087, + "complete_pagination": true, + "warnings": [], + "assessment": "Main and exact predecessor heads unchanged. Concurrent PR2354, head 308ebc7405303bb7ed91b012bb705949c6091a16, eliminates the common-axis family's defect with a fixed coordinate set; it explicitly leaves the dense-record full-kernel question to this claim. No competing exact scope identified in the searched coverage." + }, + "predecessor_heads": { + "2104": "4bdc574da394a39f955e8cf4637075649c43a632", + "2153": "5646398dcdc01769df83b939c6b3eb5ecb4d5ebd", + "2174": "f79470a7931f3943360c10d15b428e0e4e479c22", + "2216": "b80e9ba43367fb8b20877a97da1cb677c34f9264", + "2326": "fb7d64cd4a51c49bc56920305b0aca64011a420c", + "2093": "8b21a900eb520e4f11ea177b310f66316f8e8983" + }, + "open_questions": [ + { + "question": "Can a changed first pair make a different eight-coordinate dense record sufficient?", + "why_it_matters": "Detecting a known witness does not establish full selected-input recovery.", + "first_step": "Write the ordered kernel equations for one precisely specified record and intersect its query graph with the actual three-query image.", + "blocked_by": "A complete kernel argument, legal native reads and retention, and a favorable full invoice." + }, + { + "question": "Can legal final records recover the privileged post-B1 cut used by PR2174?", + "why_it_matters": "The two-record positive theorem assumes this cut and is not a final-only controller.", + "first_step": "Derive an ordered reconstruction of its selected cut variables from one fixed final observation set.", + "blocked_by": "Final endpoint typing, retained information and physical access costs." + } + ] +} diff --git a/research/qq16-shear-old-chart-kernel/VERIFY.json b/research/qq16-shear-old-chart-kernel/VERIFY.json new file mode 100644 index 0000000000..39b054c0e5 --- /dev/null +++ b/research/qq16-shear-old-chart-kernel/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-reconciliation-third100-audit/regenerated/pr377-outputs/work/odd-stages/RECIPE-9.json.gz", + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Source pins, exact three-chart Gram/route premises, rational ordered-map fixtures, intersection dimension, retained tail and six negative-control groups." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "The same validation and rejection controls remain active with Python assertions disabled." + } + ] +} diff --git a/research/qq16-shear-old-chart-kernel/verify.py b/research/qq16-shear-old-chart-kernel/verify.py new file mode 100644 index 0000000000..2d09009630 --- /dev/null +++ b/research/qq16-shear-old-chart-kernel/verify.py @@ -0,0 +1,617 @@ +#!/usr/bin/env python3 +"""Exact checks for the scoped QQ16 old-chart kernel argument. + +Apache-2.0. The three-query trace method is credited to Ross Richardson / PR2104; +packet binding follows commdata2338 / PR2153. Local maps and tail schedule are +credited to Ali Romman / PR1969, with the corrected tail binding from PR2174. +""" + +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import sys + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKET = "research/joint-query/certificate.json.gz" +TAIL = "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json" +RECIPE = "research/community-reconciliation-third100-audit/regenerated/pr377-outputs/work/odd-stages/RECIPE-9.json.gz" +A = [0, 7, 20, 27, 36, 46, 57, 111] +T = [21, 37, 47, 76, 81, 87, 92, 110] +U = [p for p in range(112) if p not in A + T] +AXES = tuple(1 << i for i in range(73)) +MARKER = "PASS_QQ16_SHEAR_OLD_CHART_KERNEL" + + +class Failure(ValueError): + pass + + +def need(condition, message): + if not condition: + raise Failure(message) + + +def read_json(raw, label): + def pairs(items): + result = {} + for key, value in items: + need(key not in result, label + ": duplicate JSON key " + key) + result[key] = value + return result + + def constant(value): + raise Failure(label + ": nonfinite JSON value " + value) + + try: + return json.loads(raw, object_pairs_hook=pairs, parse_constant=constant) + except Failure: + raise + except (ValueError, UnicodeDecodeError, TypeError) as exc: + raise Failure(label + ": invalid JSON: " + str(exc)) from exc + + +def digest(raw): + return hashlib.sha256(raw).hexdigest() + + +def load_sources(): + manifest = read_json((HERE / "SOURCES.json").read_bytes(), "SOURCES.json") + need(manifest.get("schema_version") == 1 and isinstance(manifest.get("files"), list), + "source manifest schema") + inputs, seen = {}, set() + for entry in manifest["files"]: + need(isinstance(entry, dict) and isinstance(entry.get("path"), str), "source entry") + if entry.get("usage") != "input": + continue + path = entry["path"] + need(path not in seen, "duplicate input path: " + path) + seen.add(path) + source = (ROOT / path).resolve() + need(source.is_relative_to(ROOT), "source path escapes repository: " + path) + try: + raw = source.read_bytes() + except OSError as exc: + raise Failure("missing source input: " + path) from exc + need(isinstance(entry.get("sha256"), str) and digest(raw) == entry["sha256"], + "source digest: " + path) + inputs[path] = raw + required = {PACKET, TAIL, RECIPE} + need(required <= inputs.keys(), "required input pins missing: " + ", ".join(sorted(required - inputs.keys()))) + return inputs + + +def eye(n, scale=1): + return [[Q(scale if i == j else 0) for j in range(n)] for i in range(n)] + + +def transpose(a): + need(bool(a) and all(len(row) == len(a[0]) for row in a), "matrix is rectangular") + return [list(col) for col in zip(*a)] + + +def add(a, b, factor=1): + need(len(a) == len(b), "vector addition shape") + return [x + factor * y for x, y in zip(a, b)] + + +def scale(a, factor): + return [factor * x for x in a] + + +def matmul(a, b): + need(bool(a) and bool(b) and all(len(row) == len(a[0]) for row in a), "left matrix shape") + need(all(len(row) == len(b[0]) for row in b) and len(a[0]) == len(b), "matrix product shape") + bt = transpose(b) + return [[sum((x * y for x, y in zip(row, col)), Q(0)) for col in bt] for row in a] + + +def mv(a, v): + need(bool(a) and all(len(row) == len(v) for row in a), "matrix-vector shape") + return [sum((x * y for x, y in zip(row, v)), Q(0)) for row in a] + + +def rref(rows): + need(bool(rows) and all(len(row) == len(rows[0]) for row in rows), "elimination matrix shape") + a = [list(map(Q, row)) for row in rows] + pivots = [] + for j in range(len(a[0])): + pivot = next((i for i in range(len(pivots), len(a)) if a[i][j]), None) + if pivot is None: + continue + r = len(pivots) + a[pivot], a[r] = a[r], a[pivot] + a[r] = [x / a[r][j] for x in a[r]] + for i in range(len(a)): + if i != r and a[i][j]: + k = a[i][j] + a[i] = [x - k * y for x, y in zip(a[i], a[r])] + pivots.append(j) + if len(pivots) == len(a): + break + return a, pivots + + +def rank(a): + return len(rref(a)[1]) + + +def inverse(a): + n = len(a) + reduced, pivots = rref([list(row) + ident for row, ident in zip(a, eye(n))]) + need(pivots == list(range(n)), "selected chart matrix is invertible") + return [row[n:] for row in reduced] + + +def columns(a, ports): + return [[row[p] for p in ports] for row in a] + + +def rows(a, ports): + return [a[p][:] for p in ports] + + +def parse_rational_rows(sparse_rows, nrows, ncols, label): + need(isinstance(sparse_rows, list) and len(sparse_rows) == nrows, label + " row count") + out = [] + for row in sparse_rows: + need(isinstance(row, dict), label + " sparse row") + need(all(isinstance(k, str) and k.isdecimal() and int(k) < ncols for k in row), + label + " column key") + values = [] + for j in range(ncols): + value = row.get(str(j), 0) + need(type(value) is int or isinstance(value, str), label + " rational encoding") + try: + values.append(Q(value)) + except (ValueError, ZeroDivisionError) as exc: + raise Failure(label + " invalid rational") from exc + out.append(values) + return out + + +def parse_packet(raw): + try: + packet = read_json(gzip.decompress(raw), "QQ16 packet") + except (OSError, EOFError) as exc: + raise Failure("QQ16 packet gzip") from exc + need((packet.get("A_ports"), packet.get("T_ports"), packet.get("U_ports")) == (A, T, U), + "packet A/T/U partition") + need(set(A + T + U) == set(range(112)) and len(set(A + T + U)) == 112, + "packet ports are disjoint and complete") + R = parse_rational_rows(packet.get("R_rows"), 8, 112, "R_rows") + K = parse_rational_rows(packet.get("K_rows"), 112, 8, "K_rows") + return packet, R, K + + +def check_packet_grams(R, K): + ru = columns(R, U) + need(matmul(ru, transpose(ru)) == eye(8, 48), "ordinary Gram R_U R_U^T = 48I") + need(all(sum((R[i][p] * R[i][p] for i in range(8)), Q(0)) == 4 for p in U), + "ordinary column norm 4") + for label, ports in (("A", A), ("T", T)): + block = columns(R, ports) + need(matmul(block, transpose(block)) == eye(8, 4), "selected " + label + " Gram = 4I") + section = rows(K, ports) + need(matmul(block, section) == matmul(section, block) == eye(8), + "selected " + label + " query/section two-sided inverse") + need(K == [[R[j][i] / 4 for j in range(8)] for i in range(112)], + "K_rows equals R transpose divided by 4") + ku = rows(K, U) + common_products = [] + for stage in range(3): + need(matmul(ru, ku) == eye(8, 12), "common-chart R_%d K_(%d,U) = 12I" % (stage, stage)) + common_products.append("12I") + return {"ordinary_gram": "48I", "ordinary_columns": 96, "ordinary_column_norm": 4, + "selected_grams": ["4I", "4I"], "common_chart_Rs_KsU": common_products} + + +def binary_apply(g, vector): + result = 0 + while vector: + bit = vector & -vector + result ^= g[bit.bit_length() - 1] + vector ^= bit + return result + + +def binary_product(left, right): + return tuple(binary_apply(left, vector) for vector in right) + + +def owner_route(packet, event): + need(isinstance(event, list) and len(event) >= 3 and event[0] == "cover_map", + "literal cover-map alignment event") + key = event[2] + entry = packet.get("map_registry", {}).get(key) + need(isinstance(entry, dict), "literal alignment map registry entry") + route = entry.get("owner_right_matrix_columns") + need(isinstance(route, list) and len(route) == 73 and + all(type(v) is int and 0 <= v < 1 << 73 for v in route), "73-bit owner route") + return tuple(route) + + +def alignment_routes(packet, events, offset): + need(len(events) == 112, "literal route alignment width") + result = [] + for p, event in enumerate(events): + need(event[1] == ["L", offset + p], "literal route field order") + result.append(owner_route(packet, event)) + return result + + +def packet_routes(packet): + programs = packet.get("programs", {}) + f0 = programs.get("F_0", []) + need(len(f0) > 1 and f0[0][:3] == ["retained_core", "forward", 0], "stage-zero forward word") + need(f0[1][:2] == ["cover_sweep", "X_A_fused_query"], "stage-zero identity boundary") + need(not any(event[0] == "cover_map" for event in f0[:1]), "stage-zero identity routes") + routes = [[tuple(1 << i for i in range(73)) for _ in range(112)]] + for stage in (1, 2): + word = programs.get("F_" + str(stage), []) + need(len(word) > 113 and word[0][:3] == ["retained_core", "forward", stage], + "stage-%d forward word" % stage) + need(word[113][:2] == ["cover_sweep", "X_A_fused_query"], + "stage-%d initial alignment boundary" % stage) + routes.append(alignment_routes(packet, word[1:113], 0)) + backward = programs.get("B_1_2", []) + future = [i for i, e in enumerate(backward) if e[:2] == ["cover_sweep", "future_E_t"]] + current = [i for i, e in enumerate(backward) if e[:2] == ["cover_sweep", "Y_U_from_X_T"]] + need(len(future) == len(current) == 1, "unique B_1_2 current/future alignment blocks") + fi, ci = future[0], current[0] + future_events = backward[fi - 112:fi] + current_events = backward[ci - 120:ci - 8] + selected_events = backward[ci - 8:ci] + need(alignment_routes(packet, future_events, 112) == routes[2], + "B_1_2 future alignment equals literal F_2 initial alignment") + need(alignment_routes(packet, current_events, 112) == routes[1], + "B_1_2 current alignment equals literal F_1 initial alignment") + need(len(selected_events) == len(T), "B_1_2 selected current alignment width") + need([e[1] for e in selected_events] == [["L", p] for p in T], + "B_1_2 selected current field order") + need([owner_route(packet, e) for e in selected_events] == [routes[1][p] for p in T], + "B_1_2 selected routes equal current F_1 routes") + for stage, stage_routes in enumerate(routes): + for route in stage_routes: + need(binary_product(route, route) == AXES, "owner route involution stage %d" % stage) + need(all((x & y).bit_count() % 2 == int(i == j) + for i, x in enumerate(route) for j, y in enumerate(route)), + "owner route orthogonality stage %d" % stage) + return routes + + +def distinct_relative_routes(routes): + reports = [] + for s, t in ((0, 1), (0, 2), (1, 2)): + relative = [binary_product(routes[s][p], routes[t][p]) for p in U] + need(len(set(relative)) == 96, "relative-route collision for stages %d,%d" % (s, t)) + reports.append({"stages": [s, t], "distinct_ordinary_routes": len(set(relative))}) + return reports + + +def source_moment_report(R, routes): + route_pairs = distinct_relative_routes(routes) + ru = columns(R, U) + gram = matmul(ru, transpose(ru)) + weighted = [[sum((sum((R[k][p] ** 2 for k in range(8)), Q(0)) * R[i][p] * R[j][p] + for p in U), Q(0)) for j in range(8)] for i in range(8)] + need(weighted == eye(8, 192), "cross-Gram identity coefficient 192I") + trace = 3 * sum((gram[i][i] for i in range(8)), Q(0)) + square_trace = 3 * sum((x * x for row in gram for x in row), Q(0)) + square_trace += 2 * 3 * sum((weighted[i][i] for i in range(8)), Q(0)) + rank_lower = Q(trace * trace, square_trace) + residual = rank_lower - 16 + need(trace == 1152 and square_trace == 64512, "three-query trace moments") + need(rank_lower == Q(144, 7), "three-query rank lower bound") + need(residual == Q(32, 7), "old-chart residual lower bound") + return {"trace_per_owner": str(trace), "square_trace_per_owner": str(square_trace), + "rank_lower_per_owner": str(rank_lower), "residual_lower_per_owner": str(residual), + "integer_bound": "ceil(32N/7)", "relative_routes": route_pairs} + + +def fixture(C): + # Distinct upper/lower unipotents give noncommuting selected A/T charts. + P = [ + {"A": [[1, 1], [0, 1]], "T": [[1, 0], [1, 1]]}, + {"A": [[2, 1], [1, 1]], "T": [[1, 1], [0, 1]]}, + {"A": [[1, 2], [0, 1]], "T": [[1, 0], [0, Q(1, 2)]]}, + ] + E = [{kind: inverse(P[s][kind]) for kind in ("A", "T")} for s in range(3)] + need(matmul(P[0]["A"], P[0]["T"]) != matmul(P[0]["T"], P[0]["A"]), + "fixture selected A/T charts do not commute") + need(matmul(C, inverse(C)) == matmul(inverse(C), C) == eye(2), "fixture shear C invertible") + B = [] + for start in (0, 2, 4): + B.append([[Q(int(j == start + i)) for j in range(6)] for i in range(2)]) + K = [scale_row(transpose(b), 12) for b in B] + L = matmul(matmul(E[1]["T"], C), P[0]["A"]) + M = matmul(add_matrix(E[2]["A"], matmul(E[2]["T"], C)), P[0]["A"]) + return {"P": P, "E": E, "B": B, "K": K, "C": C, "L": L, "M": M} + + +def scale_row(a, factor): + return [[factor * x for x in row] for row in a] + + +def add_matrix(a, b, factor=1): + need(len(a) == len(b) and all(len(x) == len(y) for x, y in zip(a, b)), "matrix addition shape") + return [[x + factor * y for x, y in zip(ar, br)] for ar, br in zip(a, b)] + + +def query(ch, stage, side): + return add(add(mv(ch["B"][stage], side[0]), mv(ch["E"][stage]["A"], side[1])), + mv(ch["E"][stage]["T"], side[2])) + + +def forward(ch, pair): + x, y = pair + q = query(ch, 0, x) + z = add(x[0], mv(ch["K"][0], q), -1) + a = mv(ch["E"][0]["A"], x[1]) + a = add(add(scale(a, -1), mv(ch["B"][0], z), -1), scale(q, 11), -1) + nx = [z, mv(ch["P"][0]["A"], a), mv(ch["P"][0]["T"], q)] + ny = [add(y[0], z), add(add(x[1], y[1]), nx[1], -1), add(add(x[2], y[2]), nx[2], -1)] + return [nx, ny], q + + +def backward(ch, future, pair): + x, y = pair + u = [v[:] for v in y] + u[1] = add(u[1], mv(future["P"]["A"], add(mv(future["B"], y[0]), + mv(future["E"]["T"], y[2])))) + a = mv(ch["E"][1]["T"], x[2]) + b = query(ch, 1, u) + v = [part[:] for part in u] + v[2] = add(v[2], mv(ch["P"][1]["T"], add(a, b, -1))) + rv = query(ch, 1, v) + ny = [add(v[0], mv(ch["K"][1], rv)), v[1], + add(v[2], mv(ch["P"][1]["T"], scale(rv, 12)), -1)] + nx = [add(x[0], y[0], -1), add(add(x[1], y[1]), ny[1], -1), + add(add(x[2], y[2]), ny[2], -1)] + return [nx, ny] + + +def initial_state(ch, c, coefficient=-11, M=None): + L, matrix = ch["L"], ch["M"] if M is None else M + lc, mc = mv(L, c), mv(matrix, c) + w = [Q(0), Q(0)] + scale(lc, coefficient) + mc + xa, xt = scale(mv(ch["P"][0]["A"], c), -1), mv(ch["P"][0]["T"], c) + ya, yt = scale(mv(ch["P"][0]["A"], c), 1), scale(xt, -1) + return [[w, xa, xt], [[Q(0)] * 6, ya, yt]], w + + +def shear(pair, C, y_sign=-1): + x, y = pair + out = [[v[:] for v in x], [v[:] for v in y]] + out[0][2] = add(out[0][2], mv(C, x[1])) + out[1][2] = add(out[1][2], mv(C, x[1]), y_sign) + return out + + +def selected_sums(pair): + return [add(pair[0][i], pair[1][i]) for i in (1, 2)] + + +def require_selected_invisible(pair): + if any(any(vector) for side in pair for vector in side[1:]): + raise Failure("selected invisibility: a post-B1 A/T coordinate is nonzero") + + +def run_witness(ch, c, coefficient=-11, M=None, shear_y_sign=-1): + original, w = initial_state(ch, c, coefficient, M) + pair_sums = selected_sums(original) + after_f, f0 = forward(ch, original) + need(selected_sums(after_f) == pair_sums, "selected pair sum after F0") + after_shear = shear(after_f, ch["C"], shear_y_sign) + need(selected_sums(after_shear) == pair_sums, "selected pair sum after paired shear") + q2 = query(ch, 2, after_shear[1]) + after_b = backward(ch, {"P": {"A": ch["P"][2]["A"]}, "B": ch["B"][2], "E": {"T": ch["E"][2]["T"]}}, + after_shear) + need(selected_sums(after_b) == pair_sums, "selected pair sum after B1") + return {"initial": original, "w": w, "f0": f0, "q0": mv(ch["B"][0], original[0][0]), + "q2": q2, "after_f": after_f, "after_shear": after_shear, "after_b": after_b} + + +def rank_intersection_fixture(ch): + S = ch["B"][0] + ch["B"][1] + ch["B"][2] + zero = [[Q(0), Q(0)] for _ in range(2)] + H = zero + scale_row(ch["L"], -11) + ch["M"] + joined = [list(row) + list(extra) for row, extra in zip(S, H)] + rs, rh, rjoin = rank(S), rank(H), rank(joined) + exact_intersection = rs + rh - rjoin + analytic_lower = rs + rh - len(S) + need(rs == 6 and rh == 2 and rjoin == 6, "exact-elimination fixture ranks") + need(exact_intersection == analytic_lower == 2, "fixture intersection is sharp") + return {"rank_S": rs, "rank_H": rh, "rank_join": rjoin, + "intersection_dimension": exact_intersection, "sharp": True} + + +def reject(function, expected): + try: + function() + except Failure as exc: + need(expected in str(exc), "negative control rejected for wrong reason: " + str(exc)) + else: + raise Failure("negative control accepted: " + expected) + + +def positive_fixture(): + identities = eye(2) + swap = [[Q(0), Q(1)], [Q(1), Q(0)]] + reports = [] + noncommuting = fixture(swap) + need(matmul(noncommuting["E"][2]["T"], swap) != matmul(swap, noncommuting["E"][2]["T"]), + "fixture shear C does not commute with selected chart") + for C, label in ((identities, "identity"), (swap, "noncommuting")): + ch = fixture(C) + controls = {"basis_vectors": 2} + for i in range(2): + c = [Q(int(j == i)) for j in range(2)] + result = run_witness(ch, c) + p0a = mv(ch["P"][0]["A"], c) + cp0a = mv(C, p0a) + zero2 = [Q(0)] * 2 + expected_f = [[result["w"], p0a, zero2], + [result["w"], scale(p0a, -1), zero2]] + need(result["after_f"] == expected_f, "every conserved F0 output coordinate") + expected_shear = [[result["w"], p0a, cp0a], + [result["w"], scale(p0a, -1), scale(cp0a, -1)]] + need(result["after_shear"] == expected_shear, "every paired-shear output coordinate") + need(result["q0"] == [0, 0], "retained q0 is zero") + need(result["f0"] == [0, 0], "F0 query history is zero") + need(result["q2"] == [0, 0], "future B2 query is zero") + need(mv(ch["B"][0], result["w"]) == [0, 0] and + mv(ch["B"][1], result["w"]) == scale(mv(ch["L"], c), -11) and + mv(ch["B"][2], result["w"]) == mv(ch["M"], c), + "constructed w satisfies B0/B1/B2 equations") + need(any(v for side in result["initial"] for vec in side[1:] for v in vec), + "original selected defect is nonzero") + need(result["w"] == [Q(0), Q(0)] + scale(mv(ch["L"], c), -11) + mv(ch["M"], c), + "constructed ordinary vector satisfies all three B_s equations") + h = add(result["w"], mv(ch["K"][1], mv(ch["L"], c))) + expected = [[Q(0)] * 6, [Q(0)] * 2, [Q(0)] * 2] + need(result["after_b"][0] == expected and result["after_b"][1] == [h, [Q(0)] * 2, [Q(0)] * 2], + "all post-B1 output coordinates equal the ordered kernel form") + require_selected_invisible(result["after_b"]) + reports.append({"C": label, "basis_vectors": controls["basis_vectors"], + "f0_q0_q2_zero": True, "selected_outputs_zero": True, + "finite_rational_regression_only": True}) + return reports, rank_intersection_fixture(noncommuting) + + +def negative_controls(R, routes, events, trajectory): + bad_R = [row[:] for row in R] + bad_R[0][U[0]] += 1 + reject(lambda: check_packet_grams(bad_R, [[Q(0)] * 8 for _ in range(112)]), + "ordinary Gram") + bad_routes = [[list(stage) for stage in route_set] for route_set in routes] + bad_routes[1][U[1]] = bad_routes[1][U[0]] + reject(lambda: distinct_relative_routes(bad_routes), "relative-route collision") + + C = [[Q(1), Q(0)], [Q(0), Q(1)]] + ch = fixture(C) + c = [Q(1), Q(0)] + state, _ = initial_state(ch, c) + after_f, _ = forward(ch, state) + wrong = shear(after_f, C, 1) + reject(lambda: need(selected_sums(wrong) == selected_sums(after_f), "selected pair sum"), + "selected pair sum") + + for c in ([Q(1), Q(0)], [Q(0), Q(1)]): + bad_ten = run_witness(ch, c, coefficient=-10) + reject(lambda bad=bad_ten: require_selected_invisible(bad["after_b"]), "selected invisibility") + + swapped = [[Q(0), Q(1)], [Q(1), Q(0)]] + ch = fixture(swapped) + reverse_M = matmul(add_matrix(ch["E"][2]["A"], matmul(swapped, ch["E"][2]["T"])), + ch["P"][0]["A"]) + for c in ([Q(1), Q(0)], [Q(0), Q(1)]): + reversed_result = run_witness(ch, c, M=reverse_M) + reject(lambda result=reversed_result: require_selected_invisible(result["after_b"]), + "selected invisibility") + + tail = events[2:] + first_negative = next(i for i, event in enumerate(tail) + if event.get("kind") == "bridge" and event.get("coefficient") == -1) + omitted = tail[:first_negative] + tail[first_negative + 1:] + reject(lambda: replay_tail(omitted, trajectory), "backward tail source is zero") + return ["changed_R_gram", "duplicate_relative_route", "wrong_shear_sign_pair_sum", + "coefficient_minus_10_invisible", "reversed_M_factor_invisible", "omitted_first_negative_bridge"] + + +def bind_tail(raw_recipe, witness): + try: + recipe = read_json(gzip.decompress(raw_recipe), "RECIPE-9") + except (OSError, EOFError) as exc: + raise Failure("RECIPE-9 gzip") from exc + need(len(recipe) == 19 and recipe[-1] == {"kind": "terminal", "pairs": 4}, + "retained 19-event schedule boundary") + locals_all = [event for event in recipe if event.get("kind") == "local"] + need([(e.get("stage"), e.get("pair"), e.get("reverse")) for e in locals_all] == [ + (0, 0, False), (1, 0, True), (2, 0, False), (3, 1, True), (4, 1, False), + (5, 2, True), (6, 2, False), (7, 3, True), (8, 3, False)], + "retained local pair schedule") + tail = recipe[2:] + trajectory = witness.get("trajectory_after_B1") + need(len(tail) == len(trajectory) == 17, "retained tail/witness event coverage") + for actual, old in zip(tail, trajectory): + for key in ("kind", "stage", "src", "dst", "coefficient"): + if key in actual or key in old: + need(actual.get(key) == old.get(key), "retained tail/witness event binding: " + key) + return tail + + +def replay_tail(events, trajectory): + # Each entry is a coefficient of arbitrary formal h, not a numeric witness. + x, y = [Q(0)] * 4, [Q(1), Q(0), Q(0), Q(0)] + for i, event in enumerate(events): + kind = event.get("kind") + if kind == "bridge": + src, dst, coefficient = event.get("src"), event.get("dst"), event.get("coefficient") + need(src in range(4) and dst in range(4) and src != dst and coefficient in (-1, 1), + "tail bridge domain") + x[dst] += coefficient * x[src] + y[src] -= coefficient * y[dst] + elif kind == "local": + stage, pair = event.get("stage"), event.get("pair") + need(stage in range(2, 9) and pair in range(4) and event.get("reverse") == bool(stage % 2), + "tail local event domain") + if event["reverse"]: + need(y[pair] == 0, "backward tail source is zero") + x[pair] -= y[pair] + else: + need(x[pair] == 0, "forward tail source is zero") + y[pair] += x[pair] + else: + need(kind == "terminal" and event.get("pairs") == 4, "tail terminal event") + x, y = y, [-value for value in x] + need(i < len(trajectory), "tail has excess events") + state = [value for pair in zip(x, y) for value in pair] + expected = trajectory[i].get("ordinary") + need(expected is not None and state == [Q(value) for value in expected], + "tail trajectory state at event %d" % i) + need(len(events) == len(trajectory), "tail event count") + need(y[0] == 0 and x[0] == 1, "final completed-X Y=0 and former-Y X0=h") + return {"events": len(events), "local_pairs_stages_0_to_8": [0, 0, 0, 1, 1, 2, 2, 3, 3], + "final_completed_X_named_Y": str(y[0]), "final_former_Y_named_X0": str(x[0]), + "arbitrary_formal_h": True} + + +def verify(): + raw = load_sources() + packet, R, K = parse_packet(raw[PACKET]) + witness = read_json(raw[TAIL], "QQ16 selected witness") + need((witness.get("A"), witness.get("T"), witness.get("U")) == (A, T, U), + "tail witness A/T/U binding") + gram_report = check_packet_grams(R, K) + routes = packet_routes(packet) + moment_report = source_moment_report(R, routes) + + fixtures, sharp = positive_fixture() + events = bind_tail(raw[RECIPE], witness) + tail_report = replay_tail(events, witness["trajectory_after_B1"]) + recipe = read_json(gzip.decompress(raw[RECIPE]), "RECIPE-9") + controls = negative_controls(R, routes, recipe, witness["trajectory_after_B1"]) + return {"scope": "scoped rational fixture and retained-source checks; not a formal proof or native replay", + "sources_sha256": {path: digest(value) for path, value in sorted(raw.items())}, + "packet": gram_report, "moment_recheck": moment_report, + "positive_fixtures": fixtures, "fixture_intersection": sharp, + "tail": tail_report, "negative_controls": controls} + + +def main(): + try: + result = verify() + except Failure as exc: + print("FAIL_QQ16_SHEAR_OLD_CHART_KERNEL: " + str(exc), file=sys.stderr) + return 1 + print(json.dumps(result, sort_keys=True, separators=(",", ":"))) + print(MARKER) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())