From 5646398dcdc01769df83b939c6b3eb5ecb4d5ebd Mon Sep 17 00:00:00 2001 From: commdata2338 <199849969+commdata2338@users.noreply.github.com> Date: Wed, 14 Oct 2026 16:11:12 -0500 Subject: [PATCH] Research: bound QQ16 transcript capacity; the full initial R2 query fails At the fixed QQ16 F0/B1 cut, the known erased-input family carries an original selected A/T defect of dimension at least ceil(88|G|/7). An added read-only rational-linear record of rank d leaves at least max(0, ceil(88|G|/7) - d) of it invisible. So the full initial R2 X query (at most 8|G| outputs on the family) does not restore the selected inputs, and neither does any record of at most twelve scalars per cover owner. Thirteen is necessary, not shown sufficient. PR #2104's three-query trace bound is rederived against main's packet. This is information dimension, not paid rank; no supplier or kappa change. Adds research/qq16-transcript-capacity/ 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-transcript-capacity/PROOF.md | 236 +++++++ research/qq16-transcript-capacity/README.md | 106 ++++ research/qq16-transcript-capacity/RESULT.json | 596 ++++++++++++++++++ .../qq16-transcript-capacity/SOURCES.json | 104 +++ research/qq16-transcript-capacity/TASK.json | 102 +++ research/qq16-transcript-capacity/VERIFY.json | 38 ++ .../qq16-transcript-capacity/test_verify.py | 85 +++ research/qq16-transcript-capacity/verify.py | 462 ++++++++++++++ 8 files changed, 1729 insertions(+) create mode 100644 research/qq16-transcript-capacity/PROOF.md create mode 100644 research/qq16-transcript-capacity/README.md create mode 100644 research/qq16-transcript-capacity/RESULT.json create mode 100644 research/qq16-transcript-capacity/SOURCES.json create mode 100644 research/qq16-transcript-capacity/TASK.json create mode 100644 research/qq16-transcript-capacity/VERIFY.json create mode 100644 research/qq16-transcript-capacity/test_verify.py create mode 100644 research/qq16-transcript-capacity/verify.py diff --git a/research/qq16-transcript-capacity/PROOF.md b/research/qq16-transcript-capacity/PROOF.md new file mode 100644 index 0000000000..aaaf04f5df --- /dev/null +++ b/research/qq16-transcript-capacity/PROOF.md @@ -0,0 +1,236 @@ +# Information required by the fixed QQ16 erasure family + +Fix the conserved `F0/B_1_2` pair and ordinary tail from +[PR #1969](https://github.com/CrocSwap/integer-mult-bounds/pull/1969), +as retained in `research/joint-query`. Let `G` be a finite regular cover +containing the actual routes and let `N=|G|`. + +**Claim.** Suppose an additional read-only rational-linear record, taken +from the original input, has rank at most `d` on the family below. +The dimension of original selected `(X_A,X_T)` values still invisible +after adding that record is at least + +```text +max(0, ceil(88 N / 7) - d). (1) +``` + +Consequently the complete initial query `R2 X`, of rank at most `8N` +on this family, does not repair selected-input recovery. Every record +of at most twelve rational scalars per cover owner also fails. +Thirteen is a necessary integer width in this model, not a sufficient +width, exact minimum, native operation count or recursive rank bill. + +The three-query rank method belongs to +[PR #2104](https://github.com/CrocSwap/integer-mult-bounds/pull/2104); +the erased-state injection belongs to the original QQ16 work. +The new step measures the **joint A/T defect** before choosing a +record. It allows selected-input reads and arbitrary rational mixing +across cover owners, answering the full-initial-`R2 X` handoff in +[discussion #2074](https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18932289). +It also extends the specific scalar-mixer family in +[PR #2122](https://github.com/CrocSwap/integer-mult-bounds/pull/2122). +The predecessor calculations are not claimed as new here. + +## 1. Observation and capacity contract + +Use logical coordinates and the selected sets + +```text +A = [0,7,20,27,36,46,57,111], +T = [21,37,47,76,81,87,92,110], +U = {0,...,111} minus (A union T). +``` + +The old observations are selected endpoints after `B_1_2` and their +later selected-only descendants, completed-X descendants at the retained +output endpoint, and the five forward-query histories. The first pair +and ordinary tail are unchanged. There is no separately saved copy of +F0's transient A output: it is generally nonzero on this family and +would be additional information. Reading the former-Y hole as a +completed-X output is also outside this contract. + +Grant a record `L z + c + H` before F0, where z is the complete original +logical input, L is rational-linear, c is fixed and the arbitrary dirty +baseline H is common to the two compared executions. Grant exact reads, +indefinite retention and all physical costs for free. The record does +not change the first pair or ordinary schedule. The final decoder may +be nonlinear; the record encoder L is linear. Records at several cuts +are covered if their combined restriction to this family is linear of +rank at most d and they do not change its trajectory. + +Capacity counts independent rational scalars **on this family**, not +field names. A q-coordinate field with one scalar per cover owner has +capacity at most qN. Encoding extra independent information in payload +modes or other storage must count the increased rank. The actual full +query `R2 X` preserves the payload-constant subspace and has at most +8N outputs there. + +Use arbitrary cover values constant in every payload block. Actual +cover maps retain their regular owner action; their payload translations +act trivially on this subspace. Distinct owners are not identified. +The inherited invertible endpoint gauges in +[BRIDGE-REVIEW.md](../joint-query/evidence/BRIDGE-REVIEW.md) transport +indistinguishable logical inputs to physical inputs. They are not +presumed free to execute. This works at every positive tensor size +but supplies no recursive precision bound. + +## 2. Rebound three-query premise + +Write `B_s=R_s iota_U`, s=0,1,2. For each ordinary port p let r_p +be its column of R and g_(s,p) its owner route. Exact packet checks give + +```text +|U|=96, r_p^T r_p=4, +sum_(p in U) r_p r_p^T=48 I_8, +R_A R_A^T=R_T R_T^T=4 I_8, +g_(s,p) g_(t,p)^-1 distinct over p in U, for each s=tr(K)^2/tr(K^2)=144 N/7. (2) +``` + +The inequality is Cauchy--Schwarz on K's nonzero eigenvalues; rational +and real ranks agree. This is PR #2104's calculation, rebound to main's +packet. Distinct abstract labels in a nonfaithful quotient would not +justify the regular-trace step; no such quotient is used. + +## 3. The complete selected defect + +Let `V=ker B1`. For h in V set only pair 0 nonzero and define W(h) by + +```text +X_U=h, Y_U=0, +X_A=-P_(0,A)B0h-P_(2,A)B2h, Y_A=-X_A, +X_T=P_(0,T)ell_(0,A)P_(2,A)B2h, Y_T=-X_T. (3) +``` + +Other pairs and helpers are zero, an admissible subspace of the +arbitrary-input contract. The selected sections and queries are +two-sided inverses on their selected spaces. Operator order matters. + +The defect `J(h)=(X_A,X_T)` retains exactly `(B0h,B2h)`, since + +```text +B0h=-ell_(0,A)X_A-ell_(0,T)X_T, +B2h=ell_(2,A)P_(0,A)ell_(0,T)X_T. (4) +``` + +Thus `ker J=ker[B0;B2]` on V. The rank identity for restriction to a +kernel and `B1 B1*=48I` imply + +```text +dim J(V)=rank([B0;B1;B2])-rank(B1) + =rank(S)-8N >= ceil(88N/7). (5) +``` + +Both selected blocks matter. An A defect can remain when B2h=0; +other directions carry a T defect. Counting only one block would not +give (5). + +For every h in V, substitution in the ordered forward map gives +`f0=B0h+ell_(0,A)X_A+ell_(0,T)X_T=0`. After F0, + +```text +X_U=Y_U=h, +X_A=P_(2,A)B2h, Y_A=-P_(2,A)B2h, +X_T=Y_T=0. +``` + +At B1, `R2 Y=B2h-B2h=0`, so E2 makes `u_A=0`, with u_U=h, +u_T=0. Also a1=ell_(1,T)X=0 and b1=R1u=B1h=0. The conserved +B formulas leave only `Y_(0,U)=h`. + +The retained tail follows the original +[selected witness](../joint-query/evidence/QQ16-SELECTED-WITNESS.md): +the first plus bridge creates -h in Y1; the first minus bridge removes +it before B3; every later active local source is zero. The terminal +leaves h only in the former-Y hole. Selected endpoints after B1, +completed-X descendants and all five forward queries are zero. +The executable replays this formal-h tail and checks every stored +state. This is an inherited schedule, not a new scheduling theorem. +Later homogeneous selected-only linear controls preserve zero. + +## 4. Arbitrary records and the full R2 read + +Restrict the record to (3): `C=L W|V`, of rank at most d. For linear +maps J and C on a finite-dimensional space, + +```text +dim J(ker C) >= dim J(V)-rank(C). (6) +``` + +A complement of ker C has dimension rank(C); its J-image can add +at most that many dimensions to J(ker C). Equations (5)--(6) prove +(1). A positive bound supplies h with Ch=0 and J(h)!=0. The inputs +W(h) and zero agree on all observations, including the common dirty +baseline and offset, but need different selected outputs. No decoder +from these records can restore all inputs. + +Rational nullspaces give rational h. Clearing denominators makes h +integral; the selected sections are dyadic. Further common scaling +gives dyadic logical inputs of arbitrarily small nonzero magnitude. +Their inherited physical pullbacks are admissible complex dyadic +inputs. No compact formula for h on the actual regular cover, bit-length +bound or recursive precision bound is asserted. + +The full original R2 X on (3) is + +```text +-ell_(2,A)P_(0,A)B0h ++ell_(2,T)P_(0,T)ell_(0,A)P_(2,A)B2h. (7) +``` + +It is not B2h. It can detect an earlier B2-only counterexample, but +still has at most 8N independent outputs. Hence at least ceil(32N/7) +selected-defect dimensions remain invisible. The operators in (7) +may mix owners; no scalar-mixer or commutation assumption is needed. + +For q scalars per owner the residual is at least +`max(0,ceil((88/7-q)N))`. At q=12 it is ceil(4N/7)>0. At q=13 +this lower bound is zero and supplies no obstruction or construction. + +As a positive boundary control, the sixteen-coordinate record +`(B0 X_U,B2 X_U)` determines J on W(V) by (3). This establishes +recovery only on that family, not on all inputs or the full controller. + +## 5. Verification and limits + +The executable checks source pins, actual routes and Gram identities, +selected units, trace arithmetic and the retained formal-h tail. Exact +rational fixtures with noncommuting selected section matrices test +(3), (4), (7), both local maps and a concrete full-query invisible +direction. Separate rank calculations check (6), a dimension-sharp +example and a sufficient two-record control. These are failure-mode +tests; the quantified assertion follows from the written proof. + +Thirteen through sixteen coordinates remain unresolved for the full +controller. Nonlinear encoders, changed trajectories or first pairs, +and uncounted independent payload storage are outside this theorem. +Native reads, endpoint access, chronological hosting, dirty workspace +restoration, recursive precision, supplier admission and a new +multiplication exponent remain open. No formal-kernel proof is claimed. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex +assistance. Apache-2.0. Predecessor credit is retained in the README. diff --git a/research/qq16-transcript-capacity/README.md b/research/qq16-transcript-capacity/README.md new file mode 100644 index 0000000000..a35c512a1b --- /dev/null +++ b/research/qq16-transcript-capacity/README.md @@ -0,0 +1,106 @@ +# QQ16 needs more than twelve coordinates of retained linear information + +The fixed QQ16 `F0/B_1_2` controller still loses original selected inputs +when given the **full initial `R2 X` query** for free. Its known erased +family contains at least `ceil(88|G|/7)` dimensions of original A/T data. +A read-only rational-linear transcript of rank d leaves at least +`max(0,ceil(88|G|/7)-d)` of them invisible. + +For a record with one scalar in each of q coordinates per regular-cover +owner, every q<=12 fails. Thirteen is only a necessary width in this +model. Information dimension is not recursive-child rank or native +cost. No supplier or kappa change is claimed. + +## What this adds + +The claim is in [discussion #2074](https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18933989), +taking its full-initial-`R2 X` handoff. [The proof](PROOF.md) combines +the joint A/T defect of Ali Romman's QQ16 witness with Ross Richardson's +three-query rank calculation in +[PR #2104](https://github.com/CrocSwap/integer-mult-bounds/pull/2104). +It permits arbitrary rational linear records of all original coordinates, +including selected inputs and mixing across cover owners. + +[PR #2079](https://github.com/CrocSwap/integer-mult-bounds/pull/2079) +tests `B2 X_U`; #2104 quantifies its remaining A loss. +[PR #2122](https://github.com/CrocSwap/integer-mult-bounds/pull/2122) +excludes the scalar-mixer family `B0+M B2`. This result concerns total +record dimension and the different full-source query. Those predecessors +retain credit for their calculations; the three-query trace bound is +not claimed as a new or independently invented result. + +## Exact scope + +Keep the first pair and ordinary schedule. Observe selected endpoints +after B1, completed-X descendants at the retained output endpoint and +all five forward-query histories. Saving F0's transient A endpoint +would count as extra information. Records are side-effect-free; +common dirty affine baselines are allowed. Nonlinear record encoders +and changes to the first pair are excluded. + +Capacity counts actual rank on the erased family. Independent payload +modes must be counted even when they share a named field. The full +`R2 X` query preserves the payload-constant subspace and has capacity +at most `8|G|` there. + +This is an author-checked scoped proof with exact finite source checks. +It has not received independent review or formal-kernel verification. +Native access, full word replay, hosting, recursive precision and the +complete supplier invoice are not checked. No compact witness for the +actual regular cover is emitted; its existence follows from the rank +argument. The small explicit witness is a rational control fixture. + +## Reproduce + +From the repository root, Python 3.12 and its standard library: + +```sh +python3 -I -B scripts/research_package.py --package research/qq16-transcript-capacity +python3 -I -O -B research/qq16-transcript-capacity/verify.py +``` + +Expected verifier line: + +```text +PASS_QQ16_TRANSCRIPT_CAPACITY defect>=88|G|/7 q<=12_excluded full_R2_X_insufficient +``` + +The registered replay checks [RESULT.json](RESULT.json), source pins, +actual owner-route distinctness, Gram facts, the retained tail, exact +noncommuting-chart fixtures and semantic failure controls. It reads +main's frozen QQ16 packet and imports no predecessor verifier. No +network or pending PR checkout is needed. [SOURCES.json](SOURCES.json) +records exact blobs and byte hashes; [TASK.json](TASK.json) records +scope and remaining questions. The selected record and catalogue are +historical provenance, not live mathematical inputs. + +## Open next questions + +1. **Can two query records recover the complete controller?** + `(B0 X_U,B2 X_U)` recovers the selected defect on this erased family. + First characterize the complete observation kernel on all inputs, + then test that pair on it. This family is only a subspace; its + recovery is insufficient for a controller or favorable physical bill. +2. **What is the exact required record dimension?** The gap between + necessary width thirteen and the sixteen-coordinate description of + the family remains. First sharpen the exact rank of `[B0;B1;B2]` + using its actual route algebra. The trace inequality is a lower + bound; the regular cover is too large for naive matrix expansion. + A sharper rank still would not price a legal implementation. + +## Credit + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Ali Romman and the contributors in +[joint-query/NOTICE.md](../joint-query/NOTICE.md) supplied the maps, +ordered sections, bridge semantics and original witness (PR #1969, +`a6e6ad3936f67b8f63b5b68c5e75d540610a65e7`). Ross Richardson supplied the trace +bound and full-R2 handoff (PR #2104, +`4bdc574da394a39f955e8cf4637075649c43a632`). Cinna Davis supplied the +extra-B2 and mixed-helper investigations (PR #2079, +`49df8190b158e3028e702b2c6b798117006f7249`; PR #2122, +`7045301a8c15eb4408e3e9d80969c9d50a914cde`). Adam Gall's PR #2086 and +#2093 are adjacent logger and explicit nonzero-chart obstructions. +The retained lineage, including Rohan Arun and Jeremy Kothe, keeps its +existing notices. New work is Apache-2.0. diff --git a/research/qq16-transcript-capacity/RESULT.json b/research/qq16-transcript-capacity/RESULT.json new file mode 100644 index 0000000000..1fb7cd806a --- /dev/null +++ b/research/qq16-transcript-capacity/RESULT.json @@ -0,0 +1,596 @@ +{ + "kind": "scoped proof with finite source checks", + "negative_controls": [ + "changed_R", + "collapsed_route", + "misbound_field", + "wrong_bridge_sign", + "commuted_section_order", + "missing_A_compensation", + "duplicate_key", + "nonfinite_number" + ], + "ordered_fixture": { + "centre_dimension": 2, + "full_query_plus_saved_F0_A_rank": 4, + "full_query_rank": 2, + "hidden_B2_X_U": [ + "1", + "0" + ], + "hidden_defect_rank": 2, + "hidden_full_R2_X": [ + "0", + "0" + ], + "hidden_h": [ + "-1", + "0", + "0", + "0", + "1", + "0" + ], + "hidden_initial_X_A": [ + "0", + "1" + ], + "hidden_initial_X_T": [ + "0", + "-1" + ], + "joint_defect_rank": 4, + "kernel_dimension": 4, + "ordinary_dimension": 6, + "transient_F0_X_A": [ + "1", + "-1" + ], + "two_record_rank": 4 + }, + "rank_lemma_controls": [ + { + "defect_rank": 3, + "lower": 3, + "record_rank": 0, + "remaining": 3 + }, + { + "defect_rank": 3, + "lower": 2, + "record_rank": 1, + "remaining": 3 + }, + { + "defect_rank": 3, + "lower": 1, + "record_rank": 2, + "remaining": 1 + }, + { + "defect_rank": 3, + "lower": 0, + "record_rank": 3, + "remaining": 0 + }, + { + "defect_rank": 3, + "lower": 2, + "record_rank": 1, + "remaining": 3 + }, + { + "defect_rank": 3, + "lower": 2, + "record_rank": 1, + "remaining": 3 + }, + { + "defect_rank": 3, + "lower": 0, + "record_rank": 5, + "remaining": 0 + } + ], + "schema": 1, + "source_rank": { + "R_sha256": "4766159d79608cc4e943b59d971f37763835ceb07f39e5a8319f5ebc4fcad91f", + "defect_rank_lower_per_owner": "88/7", + "first_width_not_excluded": 13, + "full_initial_R2_residual_lower_per_owner": "32/7", + "pairs": [ + { + "distinct": 96, + "identity_coefficient": [ + [ + 192, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 192, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 192, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 192, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 192, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 192, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 192, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 192 + ] + ], + "relative_routes_sha256": "3ab11c32aa2a2fe41cfcd48af4156bfdab95d1dccdc0a52cec01ff9544b5e8fa", + "stages": [ + 0, + 1 + ] + }, + { + "distinct": 96, + "identity_coefficient": [ + [ + 192, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 192, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 192, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 192, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 192, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 192, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 192, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 192 + ] + ], + "relative_routes_sha256": "a071cc6f2fdd1335103470d6092a9ad86ec37f43534621dd4b4de7319e0edbd5", + "stages": [ + 0, + 2 + ] + }, + { + "distinct": 96, + "identity_coefficient": [ + [ + 192, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 192, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 192, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 192, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 192, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 192, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 192, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 192 + ] + ], + "relative_routes_sha256": "57c975bc42b34a7130779c11944eda6d3ad3ff82ee46af1de94ae4b3d7828c4d", + "stages": [ + 1, + 2 + ] + } + ], + "residual_lower_per_owner_by_q": { + "0": "88/7", + "1": "81/7", + "10": "18/7", + "11": "11/7", + "12": "4/7", + "13": "0", + "14": "0", + "15": "0", + "16": "0", + "2": "74/7", + "3": "67/7", + "4": "60/7", + "5": "53/7", + "6": "46/7", + "7": "39/7", + "8": "32/7", + "9": "25/7" + }, + "square_trace_per_owner": 64512, + "stack_rank_lower_per_owner": "144/7", + "trace_per_owner": 1152 + }, + "source_sha256": { + "research/joint-query/NOTICE.md": "0e6f26a1453a98dc73c2d50e9bdd76a78e57411cd1b3f84331dc1590b128b0ff", + "research/joint-query/certificate.json.gz": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/joint-query/evidence/BRIDGE-REVIEW.md": "d01b5f4959f7c91f835496d050dfae3eeab9dee2f581571c316a42571eaa1cd3", + "research/joint-query/evidence/CONSERVED-QQ16.md": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75", + "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md": "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md": "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc" + }, + "status": "PASS_QQ16_TRANSCRIPT_CAPACITY", + "tail": { + "later_local_stages": [ + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "states": [ + [ + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + ], + "terminal_completed_X": [ + 0, + 0, + 0, + 0 + ] + } +} diff --git a/research/qq16-transcript-capacity/SOURCES.json b/research/qq16-transcript-capacity/SOURCES.json new file mode 100644 index 0000000000..2e020cd0d4 --- /dev/null +++ b/research/qq16-transcript-capacity/SOURCES.json @@ -0,0 +1,104 @@ +{ + "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/NOTICE.md", + "usage": "input", + "git_blob": "297ac2775cd01d6a69f4b5afc54287ded8f14682", + "sha256": "0e6f26a1453a98dc73c2d50e9bdd76a78e57411cd1b3f84331dc1590b128b0ff" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/BRIDGE-REVIEW.md", + "usage": "input", + "git_blob": "86139908c418235588045324f0873de6ac9f9707", + "sha256": "d01b5f4959f7c91f835496d050dfae3eeab9dee2f581571c316a42571eaa1cd3" + }, + { + "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" + } + ], + "context_predecessors": [ + { + "pr": 1969, + "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "author": "Ali Romman and retained joint-query contributors", + "role": "Local maps, selected sections, bridge and original erasure witness; consumed from main." + }, + { + "pr": 2104, + "head": "4bdc574da394a39f955e8cf4637075649c43a632", + "author": "Ross Richardson", + "role": "Three-query trace method and full-initial-R2-X handoff; proof rederived here from main packet, no pending code dependency." + }, + { + "pr": 2079, + "head": "49df8190b158e3028e702b2c6b798117006f7249", + "author": "Cinna Davis", + "role": "Extra ordinary B2 observation proposal; context only." + }, + { + "pr": 2122, + "head": "7045301a8c15eb4408e3e9d80969c9d50a914cde", + "author": "Cinna Davis", + "role": "Specific scalar-mixed affine helper obstruction; context only." + }, + { + "pr": 2086, + "head": "68dcf180ce3918a9ee1998bfc5455f42516c6009", + "author": "Adam Gall", + "role": "Changed A-logger obstruction; context only." + }, + { + "pr": 2093, + "head": "8b21a900eb520e4f11ea177b310f66316f8e8983", + "author": "Adam Gall", + "role": "Explicit all-nonzero-chart ordinary witness; context only." + } + ] +} diff --git a/research/qq16-transcript-capacity/TASK.json b/research/qq16-transcript-capacity/TASK.json new file mode 100644 index 0000000000..f58adbac0a --- /dev/null +++ b/research/qq16-transcript-capacity/TASK.json @@ -0,0 +1,102 @@ +{ + "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": "Fixed QQ16 F0/B1 erasure family: joint A/T defect dimension and a lower bound for arbitrary read-only rational-linear transcripts, including the full initial R2 X query.", + "scope_change_reason": "Take the live full-initial-R2-X handoff in Discussion2074 after the revision4 guidance preference, overriding the generic recursive-interface suggestions. Measure the joint A/T defect before choosing a transcript; the first pair and tail remain fixed.", + "bottleneck_link": "The local QQ16 words exist but selected input recovery is missing. The bound rejects every transcript of rank at most12|G| on the erased family before any physical construction, and in particular the full initial R2 X query. Information dimension is not paid recursive rank.", + "budget_minutes": 60, + "stop_rule": "Stop the proposed one-query repair if the fully free information relaxation is noninjective. This scoped proof ends the session without a controller, cost or kappa claim. No broader circuit search.", + "outcome": "completed", + "evidence": "PROOF.md supplies the quantified rank argument; RESULT.json and verify.py check actual frozen packet routes, source Grams, selected section units, the retained tail, exact ordered rational fixtures and semantic failure controls.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, source inspection, coding, verification and writing. No independent human, agent or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "Do two retained records B0 X_U and B2 X_U suffice for recovery on the complete controller input space?", + "why_it_matters": "These sixteen coordinates recover the present erased family, but a working controller needs every input.", + "first_step": "Characterize the full kernel of the retained endpoint/history observation map and test both records on it before pricing native access.", + "blocked_by": "The present erased family is only a subspace. Complete chronology and native record access remain unproved." + }, + { + "question": "What is the exact joint selected-defect dimension of the actual erased family?", + "why_it_matters": "The trace bound gives necessary integer width13 while sixteen coordinates describe the defect; neither is proved optimal.", + "first_step": "Sharpen rank([B0;B1;B2]) using exact actual-route algebra without expanding the full regular representation.", + "blocked_by": "The trace estimate need not be sharp and the regular cover is very large; no native tariff follows from rank alone." + } + ], + "chooser": { + "nonce": "714dbcab67b2539705b72cb500a3f046", + "track": "recursive-interfaces", + "priority_revision": 4, + "suggestions": [ + { + "task_id": "connector-alphabet-change", + "scope_key": "0c9f43f3c7d61edb36fe" + }, + { + "task_id": "coverage-law-change", + "scope_key": "f383d8fc405ee6982cdd" + }, + { + "task_id": "centre-path-sharing", + "scope_key": "184695337cedab03152e" + } + ], + "override": "live central full-initial-R2-X handoff in Discussion2074 comment18932289", + "retrieved_card_scope_key": "0e34adbc1dd119161c3a" + }, + "scope_key": "QQ16-fixed-F0-B1/full-initial-R2-X/arbitrary-linear-transcript/A-T-defect-dimension", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18933989", + "final_refresh": { + "utc": "2026-10-14T21:02:37.508381+00:00", + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "changes_since_base": [], + "decision": "Continue the scoped proof; canonical main, guidance, selected record and consumed sources are unchanged." + } +} diff --git a/research/qq16-transcript-capacity/VERIFY.json b/research/qq16-transcript-capacity/VERIFY.json new file mode 100644 index 0000000000..61d06638db --- /dev/null +++ b/research/qq16-transcript-capacity/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/NOTICE.md", + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/BRIDGE-REVIEW.md", + "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" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Immutable source hashes, actual QQ16 owner-route binding and distinctness, Gram/trace arithmetic, formal-h tail, noncommuting selected-section fixtures, general rank-lemma controls and complete receipt comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Read-only relocated source export under optimized Python without Git, wrong mathematical receipt rejection and mutated immutable source rejection." + } + ] +} diff --git a/research/qq16-transcript-capacity/test_verify.py b/research/qq16-transcript-capacity/test_verify.py new file mode 100644 index 0000000000..0458104555 --- /dev/null +++ b/research/qq16-transcript-capacity/test_verify.py @@ -0,0 +1,85 @@ +#!/usr/bin/env python3 +"""Behavioral checks for the independently runnable mathematical artifact. + +Prepared for commdata2338 with substantial OpenAI Codex assistance. +Apache-2.0. Temporary copies never modify the frozen input packages. +""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +class ArtifactTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + # TMPDIR may be supplied by the caller; there is no fixed external path. + cls.temp = tempfile.TemporaryDirectory(prefix="qq16-transcript-") + cls.export = Path(cls.temp.name) / "source export" + cls.package = cls.export / "research/qq16-transcript-capacity" + cls.package.parent.mkdir(parents=True) + shutil.copytree(HERE, cls.package) + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for entry in manifest["files"]: + if entry["usage"] == "input": + target = cls.export / entry["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / entry["path"], target) + + @classmethod + def tearDownClass(cls): + cls.temp.cleanup() + + def run_export(self, *args): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(self.package / "verify.py"), *args], + cwd=self.export, capture_output=True, text=True, timeout=90) + + def test_read_only_export_without_git(self): + files = [p for p in self.export.rglob("*") if p.is_file()] + directories = [self.export] + [p for p in self.export.rglob("*") if p.is_dir()] + try: + for p in files: + p.chmod(0o444) + for p in directories: + p.chmod(0o555) + result = self.run_export() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_QQ16_TRANSCRIPT_CAPACITY", result.stdout) + self.assertFalse((self.export / ".git").exists()) + finally: + for p in directories: + p.chmod(0o755) + for p in files: + p.chmod(0o644) + + def test_mutated_mathematical_receipt(self): + receipt = json.loads((HERE / "RESULT.json").read_text()) + receipt["source_rank"]["first_width_not_excluded"] = 12 + target = Path(self.temp.name) / "wrong-capacity.json" + target.write_text(json.dumps(receipt)) + result = self.run_export("--certificate", str(target)) + self.assertNotEqual(result.returncode, 0) + self.assertIn("complete receipt mismatch", result.stderr) + + def test_mutated_source_is_rejected_before_algebra(self): + target = self.export / "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json" + original = target.read_bytes() + try: + witness = json.loads(original) + witness["trajectory_after_B1"][0]["coefficient"] = -1 + target.write_text(json.dumps(witness)) + result = self.run_export() + self.assertNotEqual(result.returncode, 0) + self.assertIn("source digest:", result.stderr) + finally: + target.write_bytes(original) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-transcript-capacity/verify.py b/research/qq16-transcript-capacity/verify.py new file mode 100644 index 0000000000..93158c2652 --- /dev/null +++ b/research/qq16-transcript-capacity/verify.py @@ -0,0 +1,462 @@ +#!/usr/bin/env python3 +"""QQ16 transcript-capacity source checks and exact rational controls. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +Apache-2.0. The trace method is credited to Ross Richardson / PR2104. No predecessor +executable is imported. Quantified claims are proved in PROOF.md. +""" +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path + +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" +BASE = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" +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_TRANSCRIPT_CAPACITY" + + +class Failure(ValueError): + pass + + +def need(condition, message): + if not condition: + raise Failure(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False).encode() + + +def digest(raw): + return hashlib.sha256(raw).hexdigest() + + +def read_json(raw): + def pairs(items): + result = {} + for key, value in items: + need(key not in result, "duplicate JSON key") + result[key] = value + return result + def nonfinite(value): + raise Failure("nonfinite JSON: " + value) + return json.loads(raw, object_pairs_hook=pairs, parse_constant=nonfinite) + + +def sources(repo): + manifest = read_json((HERE / "SOURCES.json").read_bytes()) + need(manifest["base_commit"] == BASE, "source base") + result = {} + for entry in manifest["files"]: + if entry["usage"] != "input": + continue # Historical provenance is checked by research_package.py. + raw = (repo / entry["path"]).read_bytes() + need(digest(raw) == entry["sha256"], "source digest: " + entry["path"]) + result[entry["path"]] = raw + need({PACKET, TAIL} <= result.keys(), "required source inventory") + return result + + +def transpose(a): + return [list(col) for col in zip(*a)] + + +def eye(n, scale=1): + return [[scale * int(i == j) for j in range(n)] for i in range(n)] + + +def mul(a, b): + need(len(a[0]) == len(b), "matrix shape") + return [[sum(x*y for x, y in zip(row, col)) for col in zip(*b)] for row in a] + + +def mv(a, v): + return [sum(x*y for x, y in zip(row, v)) for row in a] + + +def plus(a, b): + return [x+y for x, y in zip(a, b)] + + +def neg(v): + return [-x for x in v] + + +def sub(a, b): + return plus(a, neg(b)) + + +def rref(rows): + a = [list(map(Q, row)) for row in rows] + need(bool(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 + r = len(pivots) + a[k], a[r] = a[r], a[k] + scale = a[r][j] + a[r] = [x/scale for x in a[r]] + for i in range(len(a)): + if i != r and a[i][j]: + factor = a[i][j] + a[i] = [x-factor*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 nullspace(a): + reduced, pivots = rref(a) + result = [] + for j in range(len(a[0])): + if j in pivots: + continue + v = [Q(0)]*len(a[0]) + v[j] = Q(1) + for i, p in enumerate(pivots): + v[p] = -reduced[i][j] + result.append(v) + return result + + +def inverse(a): + n = len(a) + reduced, pivots = rref([row+ident for row, ident in zip(a, eye(n))]) + need(pivots == list(range(n)), "invertible selected section") + return [row[n:] for row in reduced] + + +def binary_apply(columns, vector): + result = 0 + while vector: + bit = vector & -vector + result ^= columns[bit.bit_length()-1] + vector ^= bit + return result + + +def binary_product(left, right): + return tuple(binary_apply(left, x) for x in right) + + +def owner(packet, event): + need(event[0] == "cover_map", "literal cover-map event") + columns = tuple(packet["map_registry"][event[2]]["owner_right_matrix_columns"]) + need(len(columns) == 73 and all(type(x) is int and 0 < x < 1 << 73 for x in columns), + "73-dimensional owner route") + return columns + + +def packet_inputs(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 and all(x.denominator == 1 for row in R for x in row), "integer query matrix") + R = [[int(x) for x in row] for row in R] + routes = [[AXES]*112] + for s in (1, 2): + word = packet["programs"][f"F_{s}"] + first = next(i for i, e in enumerate(word) if e[0] == "cover_sweep") + need(first == 113 and word[first][1] == "X_A_fused_query", "forward alignment boundary") + alignment = word[1:first] + need([e[1] for e in alignment] == [["L", p] for p in range(112)], "forward aligned fields") + routes.append([owner(packet, e) for e in alignment]) + need(packet["programs"]["F_0"][1][:2] == ["cover_sweep", "X_A_fused_query"], "stage-zero identity") + word = packet["programs"]["B_1_2"] + future = next(i for i, e in enumerate(word) if e[:2] == ["cover_sweep", "future_E_t"]) + current = next(i for i, e in enumerate(word) if e[:2] == ["cover_sweep", "Y_U_from_X_T"]) + for s, alignment in ((2, word[future-112:future]), (1, word[current-120:current-8])): + need([e[1] for e in alignment] == [["L", 112+p] for p in range(112)], "backward aligned fields") + need([owner(packet, e) for e in alignment] == routes[s], "forward/backward route binding") + selected = word[current-8:current] + need([e[1] for e in selected] == [["L", p] for p in T], "backward selected aligned fields") + need([owner(packet, e) for e in selected] == [routes[1][p] for p in T], "selected route binding") + for row in routes: + for g in row: + need(binary_product(g, g) == AXES, "owner route involution") + need(all((x & y).bit_count() % 2 == int(i == j) + for i, x in enumerate(g) for j, y in enumerate(g)), "owner route orthogonality") + return R, routes + + +def gram(R, ports): + columns = [[row[p] for p in ports] for row in R] + return mul(columns, transpose(columns)) + + +def source_rank_report(R, routes): + need(gram(R, U) == eye(8, 48), "ordinary Gram") + need(gram(R, A) == gram(R, T) == eye(8, 4), "selected unit minors") + need(all(sum(row[p]**2 for row in R) == 4 for p in U), "column norms") + pairs = [] + 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") + # Collision-free routes leave precisely these diagonal port products. + coefficient = [[sum(sum(row[p]**2 for row in R)*R[i][p]*R[j][p] for p in U) + for j in range(8)] for i in range(8)] + need(coefficient == eye(8, 192), "cross-Gram identity coefficient") + pairs.append({"stages": [s, t], "distinct": len(set(relative)), + "relative_routes_sha256": digest(canonical(relative)), + "identity_coefficient": coefficient}) + trace = 3*sum(gram(R, U)[i][i] for i in range(8)) + square = 3*sum(x*x for row in gram(R, U) for x in row) + square += 2*sum(sum(p["identity_coefficient"][i][i] for i in range(8)) for p in pairs) + stack = Q(trace*trace, square) + need(stack == Q(144, 7), "three-query rank bound") + defect = stack-8 + need(defect == Q(88, 7) and 12 < defect < 13, "transcript threshold") + return {"R_sha256": digest(canonical(R)), "pairs": pairs, + "trace_per_owner": trace, "square_trace_per_owner": square, + "stack_rank_lower_per_owner": str(stack), "defect_rank_lower_per_owner": str(defect), + "residual_lower_per_owner_by_q": {str(q): str(max(0, defect-q)) for q in range(17)}, + "first_width_not_excluded": 13, "full_initial_R2_residual_lower_per_owner": str(defect-8)} + + +def tail_report(events): + x, y = [0]*4, [1, 0, 0, 0] + history, stages = [], [] + for e in events: + if e["kind"] == "bridge": + src, dst, c = e["src"], e["dst"], e["coefficient"] + need(src in range(4) and dst in range(4) and src != dst and c in (-1, 1), "bridge domain") + x[dst] += c*x[src] + y[src] -= c*y[dst] + elif e["kind"] == "local": + s = e["stage"] + need(s in range(2, 9), "tail stage domain") + need((x if s % 2 == 0 else y)[s//2 % 4] == 0, "nonzero active tail source") + stages.append(s) + else: + need(e["kind"] == "terminal", "tail event") + x, y = y, neg(x) + state = [value for pair in zip(x, y) for value in pair] + need(state == e["ordinary"], "tail stored state") + history.append(state) + need(stages == list(range(2, 9)), "tail stage coverage") + need(x == [1, 0, 0, 0] and y == [0]*4, "former-Y endpoint") + return {"states": history, "later_local_stages": stages, "terminal_completed_X": [0]*4} + + +def fixture_data(): + # Three 2x6 ordinary queries with a full six-row stack; not the actual cover. + B = [eye(6)[i:i+2] for i in (0, 2, 4)] + LA = [[[1, 1], [0, 1]], [[1, 0], [1, 1]], [[2, 1], [1, 1]]] + LT = [[[1, 0], [1, 1]], [[1, 1], [1, 2]], [[1, 2], [0, 1]]] + PA, PT = [inverse(a) for a in LA], [inverse(t) for t in LT] + KU = [[[Q(12)*x for x in row] for row in transpose(b)] for b in B] + return B, LA, LT, PA, PT, KU + + +def initial(h, data): + B, LA, LT, PA, PT, _ = data + b0, b2 = mv(B[0], h), mv(B[2], h) + xa = neg(plus(mv(PA[0], b0), mv(PA[2], b2))) + xt = mv(PT[0], mv(LA[0], mv(PA[2], b2))) + return [h, xa, xt, [Q(0)]*6, neg(xa), neg(xt)] + + +def full_query(state, s, data): + B, LA, LT, _, _, _ = data + xu, xa, xt = state[:3] + return plus(mv(B[s], xu), plus(mv(LA[s], xa), mv(LT[s], xt))) + + +def forward(state, data): + _, LA, LT, PA, PT, KU = data + xu, xa, xt, yu, ya, yt = state + f = full_query(state, 0, data) + a = mv(PA[0], mv(LT[0], xt)) + t = mv(PT[0], f) + u = sub(xu, mv(KU[0], f)) + return [u, a, t, plus(yu, u), sub(plus(xa, ya), a), sub(plus(xt, yt), t)], f + + +def backward(state, data): + B, LA, LT, PA, PT, KU = data + xu, xa, xt, yu, ya, yt = state + ua = plus(ya, mv(PA[2], plus(mv(B[2], yu), mv(LT[2], yt)))) + a = mv(LT[1], xt) + b = plus(mv(B[1], yu), plus(mv(LA[1], ua), mv(LT[1], yt))) + out_yu = plus(yu, mv(KU[1], a)) + out_yt = sub(yt, mv(PT[1], plus(b, [11*x for x in a]))) + out_xt = mv(PT[1], plus(b, [12*x for x in a])) + return [sub(xu, yu), sub(plus(xa, ya), ua), out_xt, out_yu, ua, out_yt] + + +def erased_family_check(state, h, data): + after_f, f = forward(state, data) + after_b = backward(after_f, data) + need(not any(f), "nonzero F0 history") + need(after_b == [[0]*6, [0]*2, [0]*2, h, [0]*2, [0]*2], "erased two-call endpoint") + return after_f + + +def ordered_fixture(): + data = fixture_data() + B, LA, LT, PA, PT, _ = data + need(mul(LA[0], LA[2]) != mul(LA[2], LA[0]), "noncommuting fixture") + basis = nullspace(B[1]) + defects, queries, F_A = [], [], [] + for h in basis: + state = initial(h, data) + after_f = erased_family_check(state, h, data) + xa, xt = state[1:3] + recovered0 = neg(plus(mv(LA[0], xa), mv(LT[0], xt))) + recovered2 = mv(LA[2], mv(PA[0], mv(LT[0], xt))) + need(recovered0 == mv(B[0], h) and recovered2 == mv(B[2], h), "joint defect inverse") + q = full_query(state, 2, data) + formula = sub(mv(LT[2], mv(PT[0], mv(LA[0], mv(PA[2], mv(B[2], h))))), + mv(LA[2], mv(PA[0], mv(B[0], h)))) + need(q == formula, "ordered full-source query") + defects.append(xa+xt) + queries.append(q) + F_A.append(after_f[1]) + J, C = transpose(defects), transpose(queries) + need(rank(J) == 4 and rank(C) == 2, "fixture capacities") + hidden_coefficients = nullspace(C) + hidden = mul(J, transpose(hidden_coefficients)) + need(rank(hidden) == 2, "full-source residual dimension") + h = [sum(c*b[i] for c, b in zip(hidden_coefficients[0], basis)) for i in range(6)] + state = initial(h, data) + after_f = erased_family_check(state, h, data) + need(not any(full_query(state, 2, data)) and any(state[1]+state[2]), "invisible full-source witness") + # A saved F0 A endpoint is EXTRA information, not part of the old observations. + need(any(after_f[1]), "transient A observation matters") + # The proposed full query differs from ordinary B2; substitution is unsound. + need(any(mv(B[2], h)), "full/ordinary-query distinction") + bpair = transpose([mv(B[0], v)+mv(B[2], v) for v in basis]) + need(rank(bpair) == 4 and rank(bpair+J) == 4, "two-record recovery on family") + saved = C+transpose(F_A) + need(rank(saved) == 4, "saved-transient-A capacity control") + return {"centre_dimension": 2, "ordinary_dimension": 6, "kernel_dimension": len(basis), + "joint_defect_rank": rank(J), "full_query_rank": rank(C), + "hidden_defect_rank": rank(hidden), "two_record_rank": rank(bpair), + "full_query_plus_saved_F0_A_rank": rank(saved), + "hidden_h": list(map(str, h)), "hidden_initial_X_A": list(map(str, state[1])), + "hidden_initial_X_T": list(map(str, state[2])), + "hidden_full_R2_X": list(map(str, full_query(state, 2, data))), + "hidden_B2_X_U": list(map(str, mv(B[2], h))), + "transient_F0_X_A": list(map(str, after_f[1]))} + + +def rank_lemma_controls(): + # Exact small models of dim J(ker C)>=rank(J)-rank(C), independent of QQ16. + J = [[1, 0, 2, 0, 0], [0, 1, 0, 0, 0], [0, 0, 0, 1, 0]] + records = [ + [[0]*5], [[1, 0, 0, 0, 0]], [[1, 0, 2, 0, 0], [0, 1, 0, 0, 0]], + J, [[1, 2, 0, 1, 0], [2, 4, 0, 2, 0]], + [[0, 0, 0, 0, 1]], eye(5), + ] + reports = [] + for C in records: + kernel = nullspace(C) + actual = rank(mul(J, transpose(kernel))) if kernel else 0 + identity = rank(C+J)-rank(C) + lower = max(0, rank(J)-rank(C)) + need(actual == identity and actual >= lower, "rank-restriction lemma") + reports.append({"record_rank": rank(C), "defect_rank": rank(J), + "remaining": actual, "lower": lower}) + need(any(x["remaining"] == x["lower"] > 0 for x in reports), "sharp positive rank fixture") + need(any(x["remaining"] > x["lower"] for x in reports), "bound need not be sharp") + need(reports[3]["remaining"] == 0, "sufficient-record control") + return reports + + +def reject(function, expected): + try: + function() + except Failure as exc: + need(expected in str(exc), "unexpected control rejection: " + str(exc)) + else: + raise Failure("control accepted: " + expected) + + +def negative_controls(packet, R, routes, events): + bad = deepcopy(R) + bad[0][U[0]] += 1 + reject(lambda: source_rank_report(bad, routes), "ordinary Gram") + bad_routes = deepcopy(routes) + bad_routes[1][U[1]] = bad_routes[1][U[0]] + reject(lambda: source_rank_report(R, bad_routes), "relative-route collision") + altered = deepcopy(packet) + altered["programs"]["F_1"][1][1] = ["L", 1] + reject(lambda: packet_inputs(altered), "forward aligned fields") + bad_tail = deepcopy(events) + i = next(i for i, e in enumerate(bad_tail) if e.get("coefficient") == -1) + bad_tail[i]["coefficient"] = 1 + reject(lambda: tail_report(bad_tail), "tail stored state") + data = fixture_data() + h = nullspace(data[0][1])[-1] + bad_state = initial(h, data) + bad_state[2] = mv(data[3][2], mv(data[1][0], mv(data[4][0], mv(data[0][2], h)))) + bad_state[5] = neg(bad_state[2]) + reject(lambda: erased_family_check(bad_state, h, data), "nonzero F0 history") + state = initial(h, data) + state[1] = [0, 0] + state[4] = [0, 0] + reject(lambda: erased_family_check(state, h, data), "nonzero F0 history") + reject(lambda: read_json('{"q":1,"q":2}'), "duplicate JSON key") + reject(lambda: read_json('{"q":NaN}'), "nonfinite JSON") + return ["changed_R", "collapsed_route", "misbound_field", "wrong_bridge_sign", + "commuted_section_order", "missing_A_compensation", "duplicate_key", "nonfinite_number"] + + +def build(repo): + raw = sources(repo) + packet = read_json(gzip.decompress(raw[PACKET])) + witness = read_json(raw[TAIL]) + need((witness["A"], witness["T"], witness["U"]) == (A, T, U), "tail port binding") + R, routes = packet_inputs(packet) + events = witness["trajectory_after_B1"] + return {"schema": 1, "status": MARKER, "kind": "scoped proof with finite source checks", + "source_rank": source_rank_report(R, routes), "tail": tail_report(events), + "ordered_fixture": ordered_fixture(), "rank_lemma_controls": rank_lemma_controls(), + "negative_controls": negative_controls(packet, R, routes, events), + "source_sha256": {p: digest(v) for p, v in sorted(raw.items())}} + + +def validate(expected, actual): + need(canonical(expected) == canonical(actual), "complete receipt mismatch") + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--repo", type=Path, default=ROOT) + ap.add_argument("--certificate", type=Path, default=HERE / "RESULT.json") + ap.add_argument("--write", type=Path, help="generate a new receipt, refusing overwrite") + args = ap.parse_args() + result = build(args.repo.resolve()) + if args.write: + with args.write.open("x") as output: + output.write(json.dumps(result, indent=2, sort_keys=True)+"\n") + print("GENERATED_QQ16_TRANSCRIPT_CAPACITY") + return + expected = read_json(args.certificate.read_bytes()) + validate(expected, result) + for change in (True, "88/7 altered"): + mutant = deepcopy(expected) + mutant["source_rank"]["defect_rank_lower_per_owner"] = change + reject(lambda: validate(mutant, result), "complete receipt mismatch") + print(MARKER + " defect>=88|G|/7 q<=12_excluded full_R2_X_insufficient") + + +if __name__ == "__main__": + main()