From f79470a7931f3943360c10d15b428e0e4e479c22 Mon Sep 17 00:00:00 2001 From: commdata2338 <199849969+commdata2338@users.noreply.github.com> Date: Wed, 14 Oct 2026 17:02:56 -0500 Subject: [PATCH] Research: prove QQ16 two-query recovery at a recorded first-pair cut Answers the two-record handoff of PR #2153. With the two initial ordinary records (B0 X_U, B2 X_U), the post-B1 selected values of pair 0, the forward histories f0 and f2, and the completed-X descendant Y_(0,U)^final, a decoder D with D O = J recovers pair 0's original selected A/T inputs for arbitrary inputs in all four bank pairs, not only PR #2153's erased family. The tail identity is Y_(0,U)^initial = Y_(0,U)^final - K_(2,U) f2, and the decoder reconstructs the transient F0 A output instead of saving it. Access to the post-B1 cut is a premise; this is an information lemma, not a final-only controller or a paid bill. No supplier or kappa change. Adds research/qq16-two-query-kernel/ only. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01X86sCSXdoDd61SDFfC1PKG --- research/qq16-two-query-kernel/PROOF.md | 231 +++++++++ research/qq16-two-query-kernel/README.md | 104 ++++ research/qq16-two-query-kernel/RESULT.json | 242 +++++++++ research/qq16-two-query-kernel/SOURCES.json | 129 +++++ research/qq16-two-query-kernel/TASK.json | 142 ++++++ research/qq16-two-query-kernel/VERIFY.json | 50 ++ research/qq16-two-query-kernel/test_verify.py | 51 ++ research/qq16-two-query-kernel/verify.py | 466 ++++++++++++++++++ 8 files changed, 1415 insertions(+) create mode 100644 research/qq16-two-query-kernel/PROOF.md create mode 100644 research/qq16-two-query-kernel/README.md create mode 100644 research/qq16-two-query-kernel/RESULT.json create mode 100644 research/qq16-two-query-kernel/SOURCES.json create mode 100644 research/qq16-two-query-kernel/TASK.json create mode 100644 research/qq16-two-query-kernel/VERIFY.json create mode 100644 research/qq16-two-query-kernel/test_verify.py create mode 100644 research/qq16-two-query-kernel/verify.py diff --git a/research/qq16-two-query-kernel/PROOF.md b/research/qq16-two-query-kernel/PROOF.md new file mode 100644 index 0000000000..98c5595194 --- /dev/null +++ b/research/qq16-two-query-kernel/PROOF.md @@ -0,0 +1,231 @@ +# Two initial ordinary queries recover the first QQ16 pair at a recorded cut + +This is a **scoped ordered identity**, conditional on the retained logical +QQ16 maps. It answers the two-record handoff in +[PR #2153](https://github.com/CrocSwap/integer-mult-bounds/pull/2153), +head `5646398dcdc01769df83b939c6b3eb5ecb4d5ebd`, on its explicitly granted +post-B1 observation contract. It does not construct a final-only controller. + +The new assertion covers arbitrary inputs in all four bank pairs, rather +than just the erased family in that predecessor. The conclusion concerns +the original selected inputs of **pair 0**. It does not restore every bank's +selected inputs from two records on pair 0. + +## 1. Precise observation contract + +Use Ali Romman's conserved F/B maps from PR #1969, retained in +[CONSERVED-QQ16.md](../joint-query/evidence/CONSERVED-QQ16.md), equations +(1)--(3), and [the ordered proof](../joint-query/evidence/JOINT-QUERY-TRANSFER.md). +The first calls are F0 and B_1_2 on pair 0. Let `B_s=R_s iota_U`, +`K_s=K_(s,U)`, and write the selected sections as `P_(s,A), P_(s,T)` +with inverses `ell_(s,A), ell_(s,T)` on their respective eight-coordinate +spaces. The actual sets A and T have eight ports each; U has 96. + +The following logical values are observations: + +* **Two added pre-F0 records** `q0=B0 X_(0,U)^initial` and + `q2=B2 X_(0,U)^initial`, each with eight query coordinates per owner. + These read the original ordinary X input. Neither is a full-source + query or a query of the changed post-F0 baseline. +* The four selected outputs of pair 0 **at the cut immediately after + B_1_2**. We use only their sums `p_A=X_A+Y_A`, `p_T=X_T+Y_T`, and + `d_A=Y_A` at that cut. Conservation identifies the sums with the + original selected sums. +* The retained forward histories `f0,f2`. The other three granted + histories `f4,f6,f8` are unnecessary for this decoder. +* `C=Y_(0,U)^final`, the completed-X descendant of pair 0 after the + retained terminal `(X,Y)->(Y,-X)`. This is the **named final Y**, + not the named final X carrying the former-Y hole. + +In particular, the transient F0 A output is **not** saved. The decoder +reconstructs it. Nor does it read a query directly from a former-Y hole. +This contract grants logical access; it makes no claim that a physical +implementation can retain or read the observations for free. + +Post-B1 selected values are explicit in PR #2153's Section 1 contract. +If only the final selected values of a particular controller are supplied, +one must separately prove that they recover `p_A,p_T,d_A`. That implication +is not supplied here. Arbitrary later selected-only operations may discard +information; this theorem does not give them an unconditional inverse. +Such operations may change later query values, but the identity below +still uses their actual logged values. The ordinary schedule must remain +unchanged, with no new writes to ordinary fields. + +## 2. The ordinary tail recovers the initial Y input + +Write `z=X_(0,U)^initial`, `w=Y_(0,U)^initial`, and `f=f0`. +After F0 the ordinary pair is + +```text +X_U = z-K0 f, +Y_U = w+z-K0 f. +``` + +The B_1_2 target rule is `X'_U=X_U-Y_U`, so immediately after B1, + +```text +X_(0,U)^B1 = -w. (1) +``` + +This cancellation holds for arbitrary inputs; it is not a consequence of +the old `w=0` witness. The B source update and all selected baselines may +be nonzero. + +The pinned [tail receipt](../joint-query/evidence/QQ16-SELECTED-WITNESS.json) +lists sixteen operations followed by the terminal, but omits the pair +field on local calls. We bind those fields to `recipe` in +`t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz` inside the selected +replay archive. The complete recipe also equals the retained PR377 +`RECIPE-9.json.gz`, byte-pinned in SOURCES.json. Its local pair sequence +for stages 0 through 8 is **0,0,0,1,1,2,2,3,3**. The retained PR377 +`PROOF.txt.gz` specifies `newX=oldY, newY=-oldX`; known physical endpoint +corrections are interpreted through the inherited logical convention. + +An ordinary bridge +`src=i,dst=j,coefficient=c` acts by + +```text +X_j += c X_i; Y_i -= c Y_j. +``` + +The first plus bridge adds `X_1` to `X_0`; F2 acts on **pair 0** and +subtracts `K2 f2` from that sum; the following minus bridge subtracts +the unchanged ordinary `X_1`. Their combined change to `X_0` is exactly +`-K2 f2`. No subsequent bridge targets bank 0, and no subsequent local +call acts on bank 0. In particular, F8 acts on pair 3. Therefore + +```text +X_(0,U)^preterminal = -w-K2 f2, +C = w+K2 f2, +w = C-K2 f2. (2) +``` + +Other bank inputs need not be zero. Their contributions cancel across +the two first bridges, even when F2's source or query is nonzero. +The verifier propagates free operator expressions for all eight initial +ordinary bank variables and independent F histories/B drivers through +every event. It checks (2) without specializing them to the old witness. + +## 3. Ordered reconstruction of all four selected inputs + +Let `t` denote the transient F0 A output. The forward rule gives + +```text +t = P_(0,A) ell_(0,T) X_T^initial, +X_T^F0 = P_(0,T) f, +Y_A^F0 = p_A-t, +Y_T^F0 = p_T-P_(0,T) f. (3) +``` + +The future logger in B_1_2 leaves the ordinary and T source rows alone +and writes + +```text +Y_A^B1 = Y_A^F0 + + P_(2,A) [B2 Y_U^F0 + ell_(2,T) Y_T^F0]. (4) +``` + +Substitute `Y_U^F0=w+z-K0 f`, (3), and `B2 z=q2`. Solving (4) +for t gives the explicit decoder + +```text +w = C-K2 f2, + +t = p_A-d_A + + P_(2,A) [B2 w+q2-B2 K0 f + +ell_(2,T)(p_T-P_(0,T) f)], + +X_T^initial = P_(0,T) ell_(0,A) t, +X_A^initial = P_(0,A) [f-q0-ell_(0,T) X_T^initial], +Y_A^initial = p_A-X_A^initial, +Y_T^initial = p_T-X_T^initial. (5) +``` + +Every product is ordered. The first reconstruction uses only the +two-sided selected unit identities. The second uses +`f=B0 z+ell_(0,A)X_A^initial+ell_(0,T)X_T^initial`. +Thus (5) reconstructs the four selected input blocks for every input. +There is no inverse of an ordinary query, centre response, Schur +complement, or changing-chart matrix. No condition `B1 h=0` is needed. + +Equivalently, let O be the observation operator in Section 1 on all +original bank inputs and let J select pair 0's original four selected +blocks. Equation (5) is a linear map D with `D O=J`. Hence + +```text +ker O is contained in ker J. (6) +``` + +This is the complete kernel implication for this explicit observation +operator, not merely its restriction to a chosen family of inputs. +It is not injectivity on all ordinary bank data: those data need not +be determined by O. + +The argument is valid over the ordered logical coefficient ring whenever +the retained maps and selected units exist. In particular it applies to +the actual rational cover operators and their tensor payload actions. +No cover quotient, commutativity assumption, floating-point rank, or +identification of distinct owners is used. Actual physical access to +these operator-valued reads is a separate obligation. + +## 4. Independent algebra and finite checks + +The free-algebra check uses normalized selected coordinates +`a=ell_(0,A)X_A`, `c=ell_(0,T)X_T`, normalized sums, and +`D=ell_(0,A)P_(2,A)`, `E=ell_(2,T)P_(0,T)`. +It expands (5) with independent noncommuting symbols for D, E, B0, +B2, K0 and K2. The three residuals for w, c and a contain zero +terms. This is a finite symbolic check of the displayed identity; +the link to the QQ16 contract is the source-pinned written derivation. +It is not a proof-assistant formalization. + +A separate rational simulator uses the literal three-step forward +source word and the backward E/exchange/H factorization, rather than +the decoder's row formulas. Two noncommuting models have query dimension +2 or 3 and four ordinary bank pairs. All 64 and 96 basis inputs pass. +Independent exact row reduction gives + +| Model | rank O | rank [O;J] | rank J | +|---|---:|---:|---:| +| query dimension 2 | 18 | 18 | 8 | +| query dimension 3 | 27 | 27 | 12 | + +The fixtures check failure modes, not the universal quantifier or the +actual enormous regular cover. Nine wrong decoders fail, including +discarding initial Y dirt, omitting or reversing the F2 correction, +using the wrong terminal sign, dropping either initial read, dropping +the changed source or T baseline, and reversing selected section roles. +Corrupting a query coefficient, the first negative bridge, or the local +pair assignment also fails. In particular `pair=stage//2 mod 4` is +incorrect: it moves F2 to pair 1 and F8 to pair 0. The old zero-witness +trajectory does not distinguish those choices, which is why this +general-input tail calculation binds the full recipe separately. +The packet check rebinds the actual port partition, ordinary Gram and +both selected two-sided inverses. The local native compiler and helper +restoration remain inherited from PR #1969; they are not rerun here. + +## 5. Cost boundary and next implication + +The added record has sixteen query coordinates per owner. This is a +storage/interface description, **not** a claim of sixteen independent +directions, sixteen paid rank units, one rank-16 recursive child, or an +optimal transcript width. The 13--15-coordinate question remains open. + +Equation (5) additionally uses `B2 C` from a completed-X descendant, +two forward histories, selected endpoint values and their chart +transports. Logical reconstruction does not implement those reads or +restore query storage. A complete bill must charge the two initial +reads, their retention and cleanup, access to the post-B1 selected cut, +the completed-X query, every frame/cover map, writes/restoration, +ownership, tape and recursive precision. No favorable completed bill +has been established, so this session stops at the information lemma. +No construction is promoted from a profile-only screen. + +The first useful next task is to choose an actual selected controller +and prove that its available final records recover `p_A,p_T,d_A`, or +price their explicit retention. Then price one legal `B2 C` read and +the two pre-F0 records together. Only a favorable complete budget +would justify extending this to all four pairs and a supplier. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex +assistance. Apache-2.0. Predecessor credit is retained in README.md. diff --git a/research/qq16-two-query-kernel/README.md b/research/qq16-two-query-kernel/README.md new file mode 100644 index 0000000000..e44c76ac59 --- /dev/null +++ b/research/qq16-two-query-kernel/README.md @@ -0,0 +1,104 @@ +# QQ16: two-query recovery at a recorded first-pair cut + +**Scoped proof; no new supplier or κ.** The two initial ordinary records +`(B0 X_U, B2 X_U)` recover pair 0's original selected X/Y inputs when +combined with the explicitly granted post-B1 selected values, forward +histories and a completed-X descendant. This holds for arbitrary inputs +in all four bank pairs, beyond the particular erased family of this +account's [PR #2153](https://github.com/CrocSwap/integer-mult-bounds/pull/2153). + +The [proof](PROOF.md) specifies the observation operator and gives a +decoder D with `D O=J`, where J selects the original four A/T blocks of +pair 0. In particular, its complete kernel has no selected-input defect. +The useful tail identity is + +```text +Y_(0,U)^initial = Y_(0,U)^final - K_(2,U) f2. +``` + +Here final **Y** is the completed-X descendant after the retained signed +terminal. It is not the former-Y hole. The decoder reconstructs the +transient F0 A value; it does not save an extra copy of that value. + +**Access to the post-B1 selected cut is a premise.** A controller that +offers only final selected values still needs to preserve or reconstruct +those cut values. This is an information lemma, not physical execution, +a final-only controller, recovery for every bank from two pair-0 reads, +or a complete recursive-cost invoice. Sixteen query coordinates are not +silently identified with sixteen paid rank units. + +## Evidence and reproduction + +[RESULT.json](RESULT.json) records three zero residuals in a free +noncommutative operator algebra; symbolic propagation of the 17-event +tail; all 160 basis inputs of two independent rational models; and +twelve rejecting controls. Exact row reduction independently checks +`rank [O;J]=rank O` in both models (18 and 27). The actual QQ16 packet's +port partition, Gram identities and selected inverses are rebound to +main. Local call pairs are read from the complete selected template: +F2 is on pair 0, and F8 is on pair 3. The native compiler, +actual-cover full matrix and full selected +cold replay are not rerun. Evidence is author-checked, with no independent +human review or proof-assistant claim. + +Standard-library Python 3.12, from the repository root: + +```sh +python3 -I -B scripts/research_package.py --package research/qq16-two-query-kernel +``` + +The registered hook runs normal and optimized replays plus artifact +tests. The direct read-only command also works in a source export: + +```sh +python3 -I -O -B research/qq16-two-query-kernel/verify.py +``` + +Expected marker: + +```text +PASS_QQ16_TWO_QUERY_KERNEL pair0_selected_recovered symbolic=3 tail=17 basis=160 controls=12 no_new_kappa +``` + +`--write` explicitly regenerates the receipt. Default verification changes +no file and compares the complete canonical JSON payload. Source pins +are in [SOURCES.json](SOURCES.json); scope, predecessor heads and next +questions are in [TASK.json](TASK.json). The claim is in +[discussion #2074](https://github.com/CrocSwap/integer-mult-bounds/discussions/2074). + +## Open next questions + +* Can one actual controller recover `p_A,p_T,d_A` at the B1 cut from its + final selected records? Trace its literal selected program first. + This determines whether the present information lemma supplies its + missing decoder or requires additional paid retention. +* What is the complete native cost of the two pre-F0 records and the + decoder's `B2` read of a completed-X descendant? Start with the + actual endpoint frames and charge storage, all chart maps and cleanup + together. No favorable completed budget is established here; physical + access, hosting, tape and precision remain the blockers. +* Can 13--15 query coordinates suffice under the same explicit cut + contract? PR #2153 excludes at most twelve on its erased family. + First test a proposed compression against the full observation + operator, rather than only that family. No sharp minimum is claimed. + +## Credit + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +Apache-2.0. + +Ali Romman's PR #1969 supplies the ordered conserved maps, selected +sections, actual native words and ordinary witness schedule. Their +inverse formulas and local realization are not claimed as new here. +This account's PR #2153 supplied the transcript-capacity obstruction and +the explicit two-record handoff. Ross Richardson's PR #2104 supplied +the three-query rank method; Cinna Davis's PR #2079/#2122 tested one +ordinary query and one compressed affine record. Adam Gall's +PR #2086/#2093 provided adjacent logger and query obstructions. +The retained Rohan Arun, Jeremy Kothe, DreamingOfClouds and complex +supplier lineage remains credited in the source package. No pending +executable is imported and no pending result is adopted as a supplier. +Zhihao Chen's PR #377 supplies the retained complete recipe and signed +terminal. Jose Manuel's retained `paired-log-ordered-decoder` package +provides a useful comparison on a different, independent-dirty-log +interface; its global decoder is not a QQ16 selected-port decoder. diff --git a/research/qq16-two-query-kernel/RESULT.json b/research/qq16-two-query-kernel/RESULT.json new file mode 100644 index 0000000000..b212139bab --- /dev/null +++ b/research/qq16-two-query-kernel/RESULT.json @@ -0,0 +1,242 @@ +{ + "status": "PASS_QQ16_TWO_QUERY_KERNEL", + "source": { + "ports": [ + 96, + 8, + 8 + ], + "ordinary_gram": 48, + "selected_grams": [ + 4, + 4 + ], + "R_sha256": "70055070e6f0465dcb9f99773769809f032043e7a1cba4f0c0fe5e5c365f0213" + }, + "ordered_identity": { + "residual_term_counts": [ + 0, + 0, + 0 + ], + "backward_A_normal_form": [ + [ + [], + "c", + -1 + ], + [ + [], + "pA", + 1 + ], + [ + [ + "D", + "B2" + ], + "w", + 1 + ], + [ + [ + "D", + "B2" + ], + "z", + 1 + ], + [ + [ + "D", + "B2", + "K0" + ], + "a", + -1 + ], + [ + [ + "D", + "B2", + "K0" + ], + "c", + -1 + ], + [ + [ + "D", + "B2", + "K0", + "B0" + ], + "z", + -1 + ], + [ + [ + "D", + "E" + ], + "a", + -1 + ], + [ + [ + "D", + "E" + ], + "c", + -1 + ], + [ + [ + "D", + "E" + ], + "pT", + 1 + ], + [ + [ + "D", + "E", + "B0" + ], + "z", + -1 + ] + ], + "completed_X_normal_form": [ + [ + [], + "w", + 1 + ], + [ + [ + "K2" + ], + "f2", + 1 + ] + ], + "commuted_D_E_residual_terms": 8 + }, + "tail": { + "events": 17, + "stages": [ + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "local_pairs": [ + 0, + 1, + 1, + 2, + 2, + 3, + 3 + ], + "Y_final_0": [ + [ + [], + "x0", + -1 + ], + [ + [ + "K2" + ], + "f2", + 1 + ] + ], + "state_hashes": [ + "546ef5213ae8a8fe9001acaaf3c5117be7827c2d58f267ea7aa3cc7a91b27d34", + "fc2d8766cdebf8775ca1c78d1525e97502b9320d8756b04cdb6391a9dd1724b3", + "aace21552c353631eec3d5fa12b216945a10f8b12d8f6b8920b795186a4a36ca", + "9f916ab4efcead19fb9f5bc4fa8763b911ee36c41926e3fe9b7e4bc739c20c62", + "b8c48ae5e560d64e0938f14471fac3db41005781db2c1bde41ee2488be5ad496", + "be36114f89930c4c2749a6ac3032609a67457a6357b3909d92003b02ba495887", + "299a27a6c8f9e5595feb7b621901f815196fde9bd50c97a12a1e11204f631455", + "9117232cdbc9dfa55a2538499e4584beca314736209cfd3e6b1ebed0fd4aee9a", + "421ddb0b5eba10a1692f6a61149eef66d4baa7aaff4922cbae4fb77e468d2bad", + "22c9762777f150936d2c8e5ff6539361f2d33b6cf0e8cc29c3a05d4ed36e19ae", + "69b531c16fbb8d149c2ddb63fb39a78087a518bb21be545e3b7cf5bd39934148", + "e5c9e5def9d3d4c486293ce83a784c45b4923202879c8e3ab3b3cf267d7520d0", + "3caafb7387590cbbca436ed6e2f6c25861544e77f39d4c6a16e50552bcfa8714", + "595804e794aa1d147625469837dd19d4fa024fae0289ba8d30e41871a77c8aa9", + "9fee34fd7aba173004e99e48d523e383b4cd688b0cacd7c40f6baf4c4cf22f9a", + "5e844eaacebc74ebb016a366dea497195ed041a7c7907c2a6953cc197e505dfa", + "174eab1c7ee2a4b2fc4c14721afed6a2b54a9f267340c44b8414d63e252e19ec" + ] + }, + "finite_fixtures": [ + { + "label": "noncommuting-q2", + "centre_dimension": 2, + "ordinary_dimension": 4, + "basis_inputs": 64, + "observation_rank": 18, + "observation_plus_selected_rank": 18, + "selected_target_rank": 8, + "mutants_rejected_at_basis": { + "omit_F2": 0, + "F2_sign": 0, + "terminal_sign": 0, + "omit_baseline_shift": 0, + "omit_second_read": 0, + "omit_T_baseline": 0, + "omit_first_read": 0, + "commute_selected_units": 6, + "discard_initial_Y": 8 + }, + "observation_matrix_sha256": "6598c3c8e681c5ce989e1c3925838624b14ba870c8646645652b64811c8f1fc1" + }, + { + "label": "noncommuting-q3", + "centre_dimension": 3, + "ordinary_dimension": 6, + "basis_inputs": 96, + "observation_rank": 27, + "observation_plus_selected_rank": 27, + "selected_target_rank": 12, + "mutants_rejected_at_basis": { + "omit_F2": 0, + "F2_sign": 0, + "terminal_sign": 0, + "omit_baseline_shift": 0, + "omit_second_read": 0, + "omit_T_baseline": 0, + "omit_first_read": 0, + "commute_selected_units": 9, + "discard_initial_Y": 12 + }, + "observation_matrix_sha256": "69930e83296c48c6b727a66dc7b134404eae0514ce232860f94ff50b51a8bf3b" + } + ], + "decoder_controls": [ + "discard_initial_Y", + "omit_F2", + "F2_sign", + "terminal_sign", + "omit_baseline_shift", + "omit_second_read", + "omit_T_baseline", + "commute_selected_units", + "omit_first_read" + ], + "source_and_schedule_controls": [ + "query coefficient", + "first negative bridge", + "guessed stage pair" + ], + "scope": "pair0 arbitrary selected inputs; recorded post-B1 selected cut; logical information only; no supplier or kappa" +} diff --git a/research/qq16-two-query-kernel/SOURCES.json b/research/qq16-two-query-kernel/SOURCES.json new file mode 100644 index 0000000000..cb569e4d53 --- /dev/null +++ b/research/qq16-two-query-kernel/SOURCES.json @@ -0,0 +1,129 @@ +{ + "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/CONSERVED-QQ16.md", + "usage": "input", + "git_blob": "4639583c1be02c2fb60ed8a8072c9969ef1569ce", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "usage": "input", + "git_blob": "c6ecf75654a084a9cc001bd62663f341976bae7a", + "sha256": "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49" + }, + { + "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" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/community-reconciliation-third100-audit/regenerated/pr377-outputs/work/odd-stages/RECIPE-9.json.gz", + "usage": "input", + "git_blob": "a9e6f99d80c4d3c712535bad13086153eaf6ac3b", + "sha256": "910fffd7b8980f1130d8bbec56d5ac34f92986c2a2c480b6aea40754b4b832ac" + }, + { + "path": "research/community-reconciliation-third100-audit/regenerated/pr377-outputs/work/complex-nine-native/PROOF.txt.gz", + "usage": "input", + "git_blob": "99623ee925bb87d1ccc52e8f3843b27490166227", + "sha256": "13b4d870a1ec1f2c080ff14500444b6901e25532b7543af648fe58c9f38dd82c" + } + ], + "archive_member": { + "archive": "research/community-frontier1042-audit/selected-replay.tar.gz", + "member": "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz", + "sha256": "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", + "decompressed_sha256": "8904bbbf46dfbf1c6df0e43479a23913fc59a410e879188112e88f16c850ede8", + "role": "Exact stage-to-pair assignments agree with the retained PR377 recipe; witness receipt omits pair fields." + }, + "context_predecessors": [ + { + "pr": 1969, + "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "author": "Ali Romman and retained contributors", + "role": "Logical conserved maps and local native evidence, consumed from main." + }, + { + "pr": 2153, + "head": "5646398dcdc01769df83b939c6b3eb5ecb4d5ebd", + "author": "commdata2338, with substantial OpenAI Codex assistance", + "role": "Explicit post-B1 cut observation contract, erased-family capacity theorem and two-record handoff. No pending executable imported." + }, + { + "pr": 2104, + "head": "4bdc574da394a39f955e8cf4637075649c43a632", + "author": "Ross Richardson", + "role": "Three-query trace method and earlier one-query obstruction; contextual." + }, + { + "pr": 2079, + "head": "49df8190b158e3028e702b2c6b798117006f7249", + "author": "Cinna Davis", + "role": "Extra B2 observation proposal; contextual." + }, + { + "pr": 2122, + "head": "7045301a8c15eb4408e3e9d80969c9d50a914cde", + "author": "Cinna Davis", + "role": "One compressed affine record; contextual." + }, + { + "pr": 377, + "head": "d0a620fcc99ba012468d61d01f5bb14007076d50", + "author": "Zhihao Chen", + "role": "Retained complete recipe and signed terminal; rebound to selected archive." + }, + { + "commit": "9a3a967693055eba38ee4a5f5d311295fc4c224c", + "author": "Jose Manuel (@jmbarrancoml)", + "role": "paired-log-ordered-decoder is comparison only: different independent-log interface; no code imported." + } + ], + "consulted_pending_proof": { + "pr": 2153, + "head": "5646398dcdc01769df83b939c6b3eb5ecb4d5ebd", + "path": "research/qq16-transcript-capacity/PROOF.md", + "sha256": "6e8cc826576e8c253278b8b9155d2fab4afb0e716193ccf413dedfc89ac128ba", + "usage": "Context for observation contract and handoff; no runtime dependency or inherited capacity result needed by the new reconstruction." + } +} diff --git a/research/qq16-two-query-kernel/TASK.json b/research/qq16-two-query-kernel/TASK.json new file mode 100644 index 0000000000..4ea5da3eab --- /dev/null +++ b/research/qq16-two-query-kernel/TASK.json @@ -0,0 +1,142 @@ +{ + "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": "Prove complete selected-input recovery for pair 0 under the explicit post-B1 cut observation contract, using two initial ordinary queries and a source-bound completed-X tail identity; no final-only controller or native cost claim.", + "scope_change_reason": "Take PR2153\u2019s released two-record handoff in Discussion2074 under revision4\u2019s central-handoff preference, rather than the chooser\u2019s generic bit-mechanisms cards. Extend from its erased family to arbitrary original inputs in all four pairs. The exact selected cut observation is explicit; full supplier admission remains outside this component.", + "bottleneck_link": "The existing fixed QQ16 observation loses selected inputs. This identifies a sufficient changed information interface at a precisely recorded cut, isolating the remaining retention and native-read cost instead of repeating the erased-family obstruction.", + "budget_minutes": 60, + "stop_rule": "Stop after the ordered kernel implication, exact source binding and rejecting controls. Do not build a controller or infer rank tariffs from information dimension without a favorable complete physical bill.", + "outcome": "completed", + "evidence": "PROOF.md gives D O=J for all inputs under its explicit observation contract. RESULT.json records three free noncommutative zero residuals, 17 tail events from the exact selected recipe, 160 rational basis columns, exact row-space checks and twelve controls. Native compiler, final-only retention and complete bill are unrun.", + "author": "commdata2338", + "ai_assistance": "Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance in mathematics, implementation, checking and prose. No independent human review or proof-assistant verification claimed.", + "open_questions": [ + { + "question": "Can an actual final selected controller recover the post-B1 values p_A, p_T and d_A without extra retained state?", + "why_it_matters": "They are explicit premises of the sufficient observation operator, not free final outputs.", + "first_step": "Trace one literal selected program from the B1 cut and write an ordered reconstruction or a counterexample.", + "blocked_by": "No such selected final-state decoder or priced retention contract is established here." + }, + { + "question": "What is the complete physical invoice for the two pre-F0 records and the B2 completed-X read?", + "why_it_matters": "Logical information recovery alone supplies no recursive saving.", + "first_step": "Bind the exact endpoint frames and price the reads, storage, all chart maps, cleanup and output writes as one component.", + "blocked_by": "Native access, chronological ownership, restoration, tape and precision remain unpriced." + }, + { + "question": "Can thirteen to fifteen query coordinates suffice under this same explicit cut contract?", + "why_it_matters": "PR2153 excludes twelve or fewer on an erased subfamily; sixteen coordinates now suffice for the stated pair-0 information interface.", + "first_step": "Specify a linear compression and test ker O against the original selected-input projection on all inputs.", + "blocked_by": "No sharp transcript-rank bound or compression construction is proved." + } + ], + "result_kind": "scoped-proof", + "selection": { + "nonce": "ae4dafd62a69238bac3a959fcb3d7803", + "drawn_track": "bit-mechanisms", + "taken_task": "joint-query-controller", + "scope_key": "0e34adbc1dd119161c3a", + "refined_scope_key": "QQ16-fixed-F0-B12/two-initial-ordinary-records-B0-B2/complete-recorded-cut-kernel", + "override": "Released central handoff from this account\u2019s PR2153; same exact-algebra expertise. No reroll.", + "passed_over": [ + { + "task_id": "bit-helper-contract", + "scope_key": "3475f46c8358c6a9211b", + "reason": "Immediate semantic-D and omission questions already covered, including this account\u2019s PR1306/2018." + }, + { + "task_id": "bit-new-register-model", + "scope_key": "7084092dd726e7ba1f2f", + "reason": "Four earlier account results and crowded coordinate-register scopes; a concrete central interface is preferred." + } + ] + }, + "observation_contract": { + "target": "Original X_A, X_T, Y_A, Y_T of pair0 only; all original banks arbitrary.", + "added": "Read-only initial B0 X_(0,U) and B2 X_(0,U).", + "retained": "Post-B1 selected p_A,p_T,d_A; forward histories f0,f2; logical completed-X descendant named final Y_(0,U).", + "not_granted": "Transient F0 A snapshot, direct old-Y-hole query, recovery of cut values from arbitrary final-only selected controls." + }, + "local_task_card": { + "object": "Full kernel of the explicit pair0 observation operator O, projected by J to original selected inputs.", + "changed_premise": "Two separate initial ordinary query records replace the insufficient one-record proposals; first pair and ordinary recipe remain fixed.", + "method_and_domain": "Ordered linear identities over the inherited coefficient ring, source-bound full nine-stage bank recipe, free noncommuting polynomial expansion, exact rational all-input models in query dimensions2 and3.", + "optimistic_budget": "Logical access is a favorable information relaxation. The sixteen query coordinates are not a paid child rank. No favorable completed physical budget is established, so stop at the lemma.", + "falsification": "A nonzero selected defect in ker O, a nonzero free-algebra residual, or failure of the independently implemented all-basis checks.", + "nearest_overlap": "PR2153 covers only the erased-family capacity; PR2104/2079/2122 cover one ordinary/mixed record; PR2086/2093 change other interface premises; paired-log-ordered-decoder uses independent external dirty logs.", + "expected_artifact": "PROOF.md, verify.py, deterministic RESULT.json, source pins and registered replay." + }, + "unchecked_obligations": [ + "Post-B1 selected retention from actual final controller outputs", + "Other bank selected-input recovery from this pair0 record", + "Native query/frame execution and complete paid invoice", + "Chronological hosting and query-storage cleanup", + "Tape and recursive precision", + "Full actual-cover matrix/native replay", + "Selected supplier cold replay and all-size admission", + "Sharp transcript minimum" + ], + "coordination": { + "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2074", + "handoff_comment": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18934227", + "priority_revision": 4, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18934635" + }, + "freshness_checkpoint": { + "checked_at_utc": "2026-10-14T21:55:45Z", + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "change": "No change from the scientific base; guidance, selected record and inputs unchanged. Continue the bounded scope.", + "open_prs_fetched_at": "2026-10-14T21:48:46.733255+00:00", + "open_pr_records": 417, + "discussions_fetched_at": "2026-10-14T21:51:47.765589+00:00", + "discussion_records": 849, + "complete_pagination": true, + "limitation": "Cached offline overlap; later updates can be absent. Text search is not proof of novelty." + } +} diff --git a/research/qq16-two-query-kernel/VERIFY.json b/research/qq16-two-query-kernel/VERIFY.json new file mode 100644 index 0000000000..77874dd8cf --- /dev/null +++ b/research/qq16-two-query-kernel/VERIFY.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/community-reconciliation-third100-audit/regenerated/pr377-outputs/work/odd-stages/RECIPE-9.json.gz", + "research/community-reconciliation-third100-audit/regenerated/pr377-outputs/work/complex-nine-native/PROOF.txt.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned source/selected-recipe binding, free ordered identity, full tail, exact arbitrary-input fixtures and twelve rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All semantic checks remain active with assertions disabled; complete canonical receipt comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Actual source-byte corruption, proof-relevant receipt type change and ambiguous JSON reject." + } + ] +} diff --git a/research/qq16-two-query-kernel/test_verify.py b/research/qq16-two-query-kernel/test_verify.py new file mode 100644 index 0000000000..31e4783eec --- /dev/null +++ b/research/qq16-two-query-kernel/test_verify.py @@ -0,0 +1,51 @@ +"""Artifact rejection tests for the scoped QQ16 verifier. Apache-2.0.""" +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("qq16_kernel_verify", HERE / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +class Artifacts(unittest.TestCase): + def test_source_corruption(self): + with tempfile.TemporaryDirectory(prefix="qq16-source-", dir=Path.cwd()) as tmp: + root = Path(tmp) + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for entry in manifest["files"]: + if entry["usage"] == "input": + target = root / entry["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(v.ROOT / entry["path"], target) + self.assertEqual(set(v.load_sources(root)), set(v.load_sources(v.ROOT))) + with (root / v.TAIL).open("ab") as stream: + stream.write(b"\n") + with self.assertRaisesRegex(v.Failure, "source digest"): + v.load_sources(root) + + def test_receipt_type_change_rejected(self): + with tempfile.TemporaryDirectory(prefix="qq16-receipt-", dir=Path.cwd()) as tmp: + receipt = json.loads((HERE / "RESULT.json").read_text()) + receipt["ordered_identity"]["residual_term_counts"][0] = False + path = Path(tmp) / "bad.json" + path.write_text(json.dumps(receipt)) + result = subprocess.run([sys.executable, "-I", "-O", "-B", str(HERE / "verify.py"), + "--receipt", str(path)], text=True, capture_output=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn("receipt mismatch", result.stderr) + + def test_ambiguous_json_rejected(self): + for raw in ('{"a":0,"a":1}', '{"a":NaN}', '{"a":Infinity}'): + with self.assertRaises(v.Failure): + v.read_json(raw) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-two-query-kernel/verify.py b/research/qq16-two-query-kernel/verify.py new file mode 100644 index 0000000000..b1965113ca --- /dev/null +++ b/research/qq16-two-query-kernel/verify.py @@ -0,0 +1,466 @@ +#!/usr/bin/env python3 +"""Ordered QQ16 two-query recovery; exact standard-library checks. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +Apache-2.0. F/B maps and schedule: Ali Romman, PR1969. No predecessor +executable is imported. PROOF.md states the quantified claim. +""" +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +from io import BytesIO +import json +from pathlib import Path +import tarfile + +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" +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +RECIPE = "research/community-reconciliation-third100-audit/regenerated/pr377-outputs/work/odd-stages/RECIPE-9.json.gz" +TEMPLATE_MEMBER = "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz" +TEMPLATE_SHA256 = "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518" +MARKER = "PASS_QQ16_TWO_QUERY_KERNEL" +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] + + +class Failure(ValueError): + pass + + +def need(ok, why): + if not ok: + raise Failure(why) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def digest(raw): + return hashlib.sha256(raw).hexdigest() + + +def read_json(raw): + def pairs(items): + out = {} + for key, value in items: + need(key not in out, "duplicate JSON key") + out[key] = value + return out + def constant(value): + raise Failure("nonfinite JSON: " + value) + return json.loads(raw, object_pairs_hook=pairs, parse_constant=constant) + + +def load_sources(root): + manifest = read_json((HERE / "SOURCES.json").read_bytes()) + raw = {} + for entry in manifest["files"]: + if entry["usage"] == "input": + data = (root / entry["path"]).read_bytes() + need(digest(data) == entry["sha256"], "source digest: " + entry["path"]) + raw[entry["path"]] = data + need({PACKET, TAIL, ARCHIVE, RECIPE} <= raw.keys(), "source inventory") + return raw + + +def eye(n, scale=1): + return [[Q(scale * (i == j)) for j in range(n)] for i in range(n)] + + +def tr(a): + return [list(c) for c in zip(*a)] + + +def mv(a, v): + need(all(len(row) == len(v) for row in a), "matrix/vector shape") + return [sum(x*y for x, y in zip(row, v)) for row in a] + + +def mm(a, b): + return tr([mv(a, c) for c in tr(b)]) + + +def add(*vectors): + need(vectors and len({len(v) for v in vectors}) == 1, "vector shape") + return [sum(c) for c in zip(*vectors)] + + +def scale(c, v): + return [c*x for x in v] + + +def sub(a, b): + return add(a, scale(-1, b)) + + +def rref(a): + a = [list(map(Q, row)) for row in a] + need(a and len({len(row) for row in a}) == 1, "rectangular matrix") + pivots = [] + for j in range(len(a[0])): + k = next((i for i in range(len(pivots), len(a)) if a[i][j]), None) + if k is None: + continue + i = len(pivots) + a[i], a[k] = a[k], a[i] + c = a[i][j] + a[i] = [x/c for x in a[i]] + for k in range(len(a)): + if k != i and a[k][j]: + c = a[k][j] + a[k] = [x-c*y for x, y in zip(a[k], a[i])] + pivots.append(j) + if len(pivots) == len(a): + break + return a, pivots + + +def inverse(a): + n = len(a) + out, pivots = rref([row+unit for row, unit in zip(a, eye(n))]) + need(pivots == list(range(n)), "selected inverse") + return [row[n:] for row in out] + + +# Linear forms over a free NONCOMMUTATIVE operator algebra. A key is +# (ordered operator word, input symbol); these checks do not sample matrices. +def var(name): + return {((), name): 1} + + +def lin(*terms): + out = {} + for coefficient, expression in terms: + for key, value in expression.items(): + out[key] = out.get(key, 0) + coefficient*value + return {key: value for key, value in out.items() if value} + + +def op(name, expression): + return {((name,)+word, variable): value + for (word, variable), value in expression.items()} + + +def expression_json(expression): + return [[list(word), name, coefficient] + for (word, name), coefficient in sorted(expression.items())] + + +def symbolic_decoder(): + z, w, a, c, pa, pt, f2 = map(var, ("z", "w", "a", "c", "pA", "pT", "f2")) + q0, q2 = op("B0", z), op("B2", z) + f = lin((1, q0), (1, a), (1, c)) + source_after_f = lin((1, w), (1, z), (-1, op("K0", f))) + # D = ell_0,A P_2,A, E = ell_2,T P_0,T. Factors never commute. + inside = lin((1, op("B2", source_after_f)), (1, op("E", lin((1, pt), (-1, f))))) + d = lin((1, pa), (-1, c), (1, op("D", inside))) + completed = lin((1, w), (1, op("K2", f2))) + rw = lin((1, completed), (-1, op("K2", f2))) + inner = lin((1, op("B2", rw)), (1, q2), (-1, op("B2", op("K0", f))), + (1, op("E", lin((1, pt), (-1, f))))) + rc = lin((1, pa), (-1, d), (1, op("D", inner))) + ra = lin((1, f), (-1, q0), (-1, rc)) + residuals = [lin((1, rw), (-1, w)), lin((1, rc), (-1, c)), lin((1, ra), (-1, a))] + need(all(not r for r in residuals), "free ordered recovery identity") + base = lin((1, op("B2", rw)), (1, q2), (-1, op("B2", op("K0", f)))) + wrong = lin((1, pa), (-1, d), (1, op("D", base)), + (1, op("E", op("D", lin((1, pt), (-1, f)))))) + need(wrong != c, "noncommutative-order control") + need(lin((1, rc), (-1, op("D", q2))) != c, "missing second read control") + return {"residual_term_counts": [len(r) for r in residuals], + "backward_A_normal_form": expression_json(d), + "completed_X_normal_form": expression_json(completed), + "commuted_D_E_residual_terms": len(lin((1, wrong), (-1, c)))} + + +def bind_schedule(raw): + # The old zero-witness receipt omits local pair assignments. Bind them to + # the complete selected template, rather than guessing from stage parity. + recipe = read_json(gzip.decompress(raw[RECIPE])) + with tarfile.open(fileobj=BytesIO(raw[ARCHIVE]), mode="r:gz") as archive: + matches = [m for m in archive.getmembers() if m.name == TEMPLATE_MEMBER] + need(len(matches) == 1 and matches[0].isfile(), "one regular template member") + member = archive.extractfile(matches[0]).read() + need(digest(member) == TEMPLATE_SHA256, "selected template member") + template = read_json(gzip.decompress(member)) + need(template["recipe"] == recipe, "selected and retained recipe agreement") + need(recipe[:2] == [{"kind": "local", "pair": 0, "reverse": False, "stage": 0}, + {"kind": "local", "pair": 0, "reverse": True, "stage": 1}], "first pair") + need(len(recipe) == 19 and recipe[-1] == {"kind": "terminal", "pairs": 4}, "recipe boundary") + witness = read_json(raw[TAIL])["trajectory_after_B1"] + events = recipe[2:] + need(len(events) == len(witness), "witness event coverage") + for actual, old in zip(events, witness): + keys = {"kind", "stage", "src", "dst", "coefficient"} & actual.keys() + need(all(actual[k] == old[k] for k in keys), "witness event binding") + return events + + +def tail_symbols(events): + x = [var("x"+str(i)) for i in range(4)] + y = [var("y"+str(i)) for i in range(4)] + stages, history = [], [] + for event in events: + kind = event["kind"] + if kind == "bridge": + i, j, k = event["src"], event["dst"], event["coefficient"] + need(i in range(4) and j in range(4) and i != j and k in (-1, 1), "bridge domain") + x[j] = lin((1, x[j]), (k, x[i])) + y[i] = lin((1, y[i]), (-k, y[j])) + elif kind == "local": + s = event["stage"] + stages.append(s) + i = event["pair"] + need(i in range(4) and event["reverse"] == bool(s % 2), "local pair/orientation") + if not event["reverse"]: + x[i] = lin((1, x[i]), (-1, op("K"+str(s), var("f"+str(s))))) + y[i] = lin((1, y[i]), (1, x[i])) + else: + old_y = y[i] + x[i] = lin((1, x[i]), (-1, old_y)) + y[i] = lin((1, old_y), (1, op("K"+str(s), var("a"+str(s))))) + else: + need(kind == "terminal", "tail event kind") + x, y = y, [lin((-1, v)) for v in x] + history.append(digest(canonical([expression_json(v) for v in x+y]).encode())) + need(stages == list(range(2, 9)), "complete ordered tail stages") + expected = lin((-1, var("x0")), (1, op("K2", var("f2")))) + need(y[0] == expected, "completed-X tail identity") + return {"events": len(events), "stages": stages, + "local_pairs": [e["pair"] for e in events if e["kind"] == "local"], + "Y_final_0": expression_json(y[0]), "state_hashes": history} + + +def packet_check(packet): + need((packet["A_ports"], packet["T_ports"], packet["U_ports"]) == (A, T, U), "port partition") + R = [[Q(row.get(str(p), 0)) for p in range(112)] for row in packet["R_rows"]] + need(len(R) == 8, "query dimension") + blocks = [[[row[p] for p in ports] for row in R] for ports in (U, A, T)] + need(mm(blocks[0], tr(blocks[0])) == eye(8, 48), "ordinary Gram") + for block in blocks[1:]: + need(mm(block, tr(block)) == eye(8, 4), "selected unit minor") + inv = inverse(block) + need(mm(inv, block) == mm(block, inv) == eye(8), "two-sided selected unit") + need(all("F_"+str(s) in packet["programs"] for s in range(9)), "forward programs") + need("B_1_2" in packet["programs"], "first backward program") + return R, {"ports": [len(U), len(A), len(T)], "ordinary_gram": 48, + "selected_grams": [4, 4], "R_sha256": digest(canonical([[str(x) for x in row] for row in R]).encode())} + + +def chart(B, LA, LT, K): + need(mm(B, K) == eye(len(B), 12), "centre response") + return {"B": B, "LA": LA, "LT": LT, "PA": inverse(LA), "PT": inverse(LT), "K": K} + + +def shear(q, step): + a = eye(q) + i, j = step % q, (step+1) % q + a[i][j] = Q(1 + step % 3) + return a + + +def fixture(q): + charts = [] + for s in range(9): + D, E = shear(q, s), shear(q, s+1) + B = [a+b for a, b in zip(D, E)] + K = [[12*x for x in row] for row in inverse(D)] + [[Q(0)]*q for _ in range(q)] + charts.append(chart(B, shear(q, s+2), shear(q, s+3), K)) + return charts + + +def query(ch, data): + u, a, t = data + return add(mv(ch["B"], u), mv(ch["LA"], a), mv(ch["LT"], t)) + + +def forward_scalar(ch, pair): + # Literal three-step source word, independent of the reconstruction. + x, y = deepcopy(pair) + z, a, c = x[0], mv(ch["LA"], x[1]), mv(ch["LT"], x[2]) + c = add(c, mv(ch["B"], z), a) + f = c[:] + z = sub(z, mv(ch["K"], c)) + a = sub(scale(-1, a), add(mv(ch["B"], z), scale(11, c))) + nx = [z, mv(ch["PA"], a), mv(ch["PT"], c)] + ny = [add(y[0], z), sub(add(x[1], y[1]), nx[1]), sub(add(x[2], y[2]), nx[2])] + return [nx, ny], f + + +def backward_exchange(ch, future, pair): + # E, full-query exchange, H and conserved sums; a separate implementation + # from the row formula used in the proof. All intermediate inputs are dirty. + x, y = deepcopy(pair) + u = deepcopy(y) + u[1] = add(u[1], mv(future["PA"], add(mv(future["B"], y[0]), mv(future["LT"], y[2])))) + a, b = mv(ch["LT"], x[2]), query(ch, u) + v = deepcopy(u) + v[2] = add(v[2], mv(ch["PT"], sub(a, b))) + rv = query(ch, v) + ny = [add(v[0], mv(ch["K"], rv)), v[1], sub(v[2], mv(ch["PT"], scale(12, rv)))] + nx = [sub(x[0], y[0]), sub(add(x[1], y[1]), ny[1]), sub(add(x[2], y[2]), ny[2])] + return [nx, ny] + + +def run(charts, events, values): + q, u = len(charts[0]["LA"]), len(charts[0]["K"]) + n = u+2*q + banks = [] + for i in range(4): + pair = [] + for j in range(2): + v = list(values[(2*i+j)*n:(2*i+j+1)*n]) + pair.append([v[:u], v[u:u+q], v[u+q:]]) + banks.append(pair) + original = deepcopy(banks[0]) + q0, q2 = mv(charts[0]["B"], original[0][0]), mv(charts[2]["B"], original[0][0]) + banks[0], f0 = forward_scalar(charts[0], banks[0]) + banks[0] = backward_exchange(charts[1], charts[2], banks[0]) + first = deepcopy(banks[0]) + need(first[0][0] == scale(-1, original[1][0]), "first pair ordinary cancellation") + queries = {0: f0} + for event in events: + kind = event["kind"] + if kind == "bridge": + i, j, k = event["src"], event["dst"], event["coefficient"] + banks[j][0][0] = add(banks[j][0][0], scale(k, banks[i][0][0])) + banks[i][1][0] = sub(banks[i][1][0], scale(k, banks[j][1][0])) + elif kind == "local": + s = event["stage"] + i = event["pair"] + if not event["reverse"]: + banks[i], queries[s] = forward_scalar(charts[s], banks[i]) + else: + banks[i] = backward_exchange(charts[s], charts[s+1], banks[i]) + else: + need(kind == "terminal", "terminal event") + for pair in banks: + pair[0][0], pair[1][0] = pair[1][0], scale(-1, pair[0][0]) + obs = {"q0": q0, "q2": q2, "f0": f0, "f2": queries[2], + "pA": add(first[0][1], first[1][1]), "pT": add(first[0][2], first[1][2]), + "dA": first[1][1], "completed": banks[0][1][0]} + return obs, original + + +def decode(charts, o, mutation=None): + ch0, ch2 = charts[0], charts[2] + f = o["f0"] + w = sub(o["completed"], mv(ch2["K"], o["f2"])) + if mutation == "discard_initial_Y": + w = [Q(0)]*len(w) + elif mutation == "omit_F2": + w = add(w, mv(ch2["K"], o["f2"])) + elif mutation == "F2_sign": + w = add(w, scale(2, mv(ch2["K"], o["f2"]))) + elif mutation == "terminal_sign": + w = sub(w, scale(2, o["completed"])) + source = add(mv(ch2["B"], w), o["q2"], scale(-1, mv(ch2["B"], mv(ch0["K"], f)))) + if mutation == "omit_baseline_shift": + source = add(source, mv(ch2["B"], mv(ch0["K"], f))) + elif mutation == "omit_second_read": + source = sub(source, o["q2"]) + target = mv(ch2["LT"], sub(o["pT"], mv(ch0["PT"], f))) + if mutation == "omit_T_baseline": + target = [Q(0)]*len(target) + temp = add(o["pA"], scale(-1, o["dA"]), mv(ch2["PA"], add(source, target))) + # Reconstruct the transient F0 A value; it is NOT an observation. + if mutation == "commute_selected_units": + xt = mv(ch0["PA"], mv(ch0["LT"], temp)) + else: + xt = mv(ch0["PT"], mv(ch0["LA"], temp)) + xa = mv(ch0["PA"], sub(sub(f, o["q0"]), mv(ch0["LT"], xt))) + if mutation == "omit_first_read": + xa = add(xa, mv(ch0["PA"], o["q0"])) + return [xa, xt, sub(o["pA"], xa), sub(o["pT"], xt)], w + + +MUTANTS = ["discard_initial_Y", "omit_F2", "F2_sign", "terminal_sign", "omit_baseline_shift", + "omit_second_read", "omit_T_baseline", "commute_selected_units", "omit_first_read"] + + +def finite_check(charts, events, label): + q, u = len(charts[0]["LA"]), len(charts[0]["K"]) + dimension = 8*(u+2*q) + observation_columns, target_columns, rejected = [], [], {} + for i in range(dimension): + values = [Q(int(i == j)) for j in range(dimension)] + obs, original = run(charts, events, values) + result, w = decode(charts, obs) + expected = original[0][1:] + original[1][1:] + need(result == expected and w == original[1][0], "arbitrary-input recovery: " + label) + observation_columns.append([x for key in sorted(obs) for x in obs[key]]) + target_columns.append([x for block in expected for x in block]) + for mutation in MUTANTS: + if mutation not in rejected and decode(charts, obs, mutation)[0] != expected: + rejected[mutation] = i + observation, target = tr(observation_columns), tr(target_columns) + observation_rank = len(rref(observation)[1]) + stacked_rank = len(rref(observation+target)[1]) + need(stacked_rank == observation_rank, "complete observation-kernel projection") + return {"label": label, "centre_dimension": q, "ordinary_dimension": u, + "basis_inputs": dimension, "observation_rank": observation_rank, + "observation_plus_selected_rank": stacked_rank, + "selected_target_rank": len(rref(target)[1]), "mutants_rejected_at_basis": rejected, + "observation_matrix_sha256": digest(canonical([[str(x) for x in row] for row in observation]).encode())} + + +def reject(call, fragment): + try: + call() + except Failure as exc: + need(fragment in str(exc), "unexpected rejection: " + str(exc)) + else: + raise Failure("accepted mutation: " + fragment) + + +def report(root): + raw = load_sources(root) + packet = read_json(gzip.decompress(raw[PACKET])) + events = bind_schedule(raw) + _, source = packet_check(packet) + symbolic, tail_result = symbolic_decoder(), tail_symbols(events) + fixtures = [finite_check(fixture(q), events, "noncommuting-q"+str(q)) for q in (2, 3)] + need(all(set(r["mutants_rejected_at_basis"]) == set(MUTANTS) for r in fixtures), "complete decoder controls") + bad = deepcopy(packet) + bad["R_rows"][0][str(U[0])] = str(Q(bad["R_rows"][0].get(str(U[0]), 0))+1) + reject(lambda: packet_check(bad), "ordinary Gram") + bad_events = deepcopy(events) + next(e for e in bad_events if e.get("coefficient") == -1)["coefficient"] = 1 + reject(lambda: tail_symbols(bad_events), "completed-X tail identity") + bad_pairs = deepcopy(events) + for event in bad_pairs: + if event["kind"] == "local": + event["pair"] = event["stage"]//2 % 4 + reject(lambda: tail_symbols(bad_pairs), "completed-X tail identity") + return {"status": MARKER, "source": source, "ordered_identity": symbolic, "tail": tail_result, + "finite_fixtures": fixtures, "decoder_controls": MUTANTS, + "source_and_schedule_controls": ["query coefficient", "first negative bridge", "guessed stage pair"], + "scope": "pair0 arbitrary selected inputs; recorded post-B1 selected cut; logical information only; no supplier or kappa"} + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--root", type=Path, default=ROOT) + ap.add_argument("--receipt", type=Path, default=HERE / "RESULT.json") + ap.add_argument("--write", action="store_true", help="explicitly regenerate the package receipt") + args = ap.parse_args() + try: + result = report(args.root) + if args.write: + args.receipt.write_text(json.dumps(result, indent=2)+"\n", encoding="utf-8") + else: + need(canonical(read_json(args.receipt.read_bytes())) == canonical(result), "receipt mismatch") + except (Failure, OSError, KeyError, ValueError) as exc: + raise SystemExit("FAIL_QQ16_TWO_QUERY_KERNEL: " + str(exc)) + print(MARKER + " pair0_selected_recovered symbolic=3 tail=17 basis=160 controls=12 no_new_kappa") + + +if __name__ == "__main__": + main()