diff --git a/research/qq16-66port-second-axis/README.md b/research/qq16-66port-second-axis/README.md new file mode 100644 index 0000000000..e22846ca7b --- /dev/null +++ b/research/qq16-66port-second-axis/README.md @@ -0,0 +1,251 @@ +# The specified QQ16 66-port read set still loses selected inputs + +**Scoped obstruction with an exact four-port witness; no new kappa.** +[PR2354](https://github.com/CrocSwap/integer-mult-bounds/pull/2354) proves that +one specified set of 66 ordinary port reads eliminates its common-first-axis +hidden-input family. Its second open question asks whether that same set +fails on other inputs. **It does:** the second local chart axis gives a +counterexample supported on unread ports **44, 49, 58 and 70**. + +The complete fixed QQ16 schedule has zero selected observations, zero +completed-X descendants, zero five forward-query histories, and zero +transcripts from all 66 specified ports, but a nonzero original A input. +The A-to-T selected shear also leaves this witness unchanged. + +This answers that exact follow-up. It does not contradict PR2354's explicitly +family-only sufficiency statement, establish a minimum tap count, or rule out +every other set of 66 ports. A dense initial old-chart read detects this +witness. Parallel PR2368 studies that dense read with a different hidden-input +family; it is separate from the fixed-coordinate set tested here. + +## Contract + +Use the actual QQ16 A/T/U partition, fixed first `F0/B_1_2` pair, nine local +stages, and ordinary 19-event recipe. All definitions and local maps are from +the retained [conserved QQ16 contract](../joint-query/evidence/CONSERVED-QQ16.md), +[ordered proof](../joint-query/evidence/JOINT-QUERY-TRANSFER.md), and +[cover action](../joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md). + +Let J be the following 30 unread ports, and S=U minus J the 66 read ports: + +```text +J = [44,45,48,49,50,51,52,53,54,55,56,58,59,60,61,62, + 63,64,65,66,67,68,69,70,71,72,73,74,75,77]. +``` + +This is precisely PR2354's attaining set: J is the set of ordinary ports +whose first local chart axis is the binary vector 2. The verifier reconstructs +that set from the frozen source, rather than assuming a similarly sized set. + +After complete F0, allow any homogeneous linear selected-field controls, +including the paired A-to-T shear, arbitrary owner mixing, and arbitrarily +many side-effect-free reads of the entire X/Y owner arrays at ports in S. +These reads may be retained for free. Granting earlier ordinary reads from S +does not help either. Keep ordinary fields and the ordinary schedule unchanged. +There is no earlier retained selected-input record, read of an unread port, +ordinary preprocessing, or additional observation of the final former-Y +endpoint. Private input-dependent records outside this contract are excluded. + +The inherited observation contract starts after B1 for completed-X +descendants. The nonzero ordinary X output immediately after F0 is **not** +granted as an additional full ordinary observation. Only its ports in S are +readable. This distinction is necessary. + +## A four-column source identity + +Write r_p for column p of the actual rational 8-by-112 matrix R and b_p for +the **second** local chart axis (array index 1, not index 0). The source gives: + +| p | coefficient c_p | b_p | r_p, in query-coordinate order | +|---|---:|---:|---| +| 44 | -1 | 25 | (0,0,1,-1,0,0,-1,1) | +| 49 | -1 | 145 | (1,0,0,1,0,1,1,0) | +| 58 | -1 | 4 | (0,1,-1,0,1,0,0,-1) | +| 70 | +1 | 4 | (1,1,0,0,1,1,0,0) | + +Thus `-r_44-r_49-r_58+r_70=0`. All other coefficients are zero. +The actual registered routes satisfy, for every port and s=1,...,8, + +```text +rho_s(p) b_p = e_(10+8(s-1)). +``` + +Coordinates here start at zero. The verifier binds all 1,008 port/stage +matrices to the native registry and checks all 7,168 positive-stage local-axis +identities, including the 32 used by this witness. + +## An identity for every cover owner + +For an owner d in the retained regular cover G define + +```text +f_v(d) = bit_0(d v), as the rational number 0 or 1; +h_p(d) = c_p f_(b_p)(d), constant in every payload coordinate. +``` + +The full cover map reads at owner `d rho_s(p)`; payload translations act +trivially on these payload-constant fields. Consequently, with +`B_s=R_s iota_U`, the checked route identities give for **every** d: + +```text +B_s h(d) = sum_p r_p c_p bit_0(d rho_s(p) b_p) + = (sum_p r_p c_p) bit_0(d e_(10+8(s-1))) + = 0, s=1,...,8. +``` + +This is an identity, not an inference from sampled owners. It requires no +independence assertion about the functions f_v. In the old chart, + +```text +H(d) = B0 h(d) = -r_44 f_25(d) - r_49 f_145(d) + + (r_70-r_58) f_4(d). +H(I) = (-1,0,-1,0,0,-1,0,-1) != 0. +``` + +Identity belongs to G, so this evaluation suffices to prove H is nonzero. +Using the first axis instead would give `H=f_2 sum_p r_p c_p=0`: that +old family has no selected defect on this coefficient vector. This is the +changed premise, not a repetition of its 66-port family threshold. + +## The ordered hidden-input trajectory + +Initialize only pair 0, with all other pair fields and helpers zero: + +```text +X_U=h, Y_U=0, +X_A=-P_(0,A) H, Y_A=+P_(0,A) H, +X_T=0, Y_T=0. +``` + +`P_(0,A)=iota_A R_A^T/4` is a section, since `R_A R_A^T=4I`. +The original selected A input is therefore nonzero. Its identity-owner +value, in A order `[0,7,20,27,36,46,57,111]`, is + +```text +(1/2,0,-1/2,0,1/2,0,1/2,0). +``` + +Every coefficient in the initialized input is integral or half-integral; +multiplying the entire witness by two gives an integral witness. +All selected pair sums vanish. The full F0 query is +`B0 h + ell_(0,A) X_A = H-H=0`, so the exact forward map gives + +```text +after F0: X_U=Y_U=h, all selected fields zero. +``` + +Every read at S is zero, since h is supported in J. Any allowed selected +controller therefore keeps selected fields zero. In particular the shear +`X_T += C X_A; Y_T -= C X_A` does nothing, for any homogeneous linear C. + +At B1 the future logger query is `B2 h=0`, the old T driver is zero, and +the current query is `B1 h=0`. The exact backward map gives + +```text +after B1: Y_(0,U)=h, every other ordinary and selected field zero. +``` + +The first positive bridge puts `-h` in Y_(1,U). F2 has zero X input and +changes nothing. The cancelling negative bridge removes that `-h`. +All remaining active local pairs are zero; the last three bridges also +leave Y_(0,U)=h alone. Terminal rotation moves it to final X_(0,U), the +former-Y native endpoint excluded by the inherited observation contract. +The [receipt](RESULT.json) records every one of the 19 events. + +At every allowed read cut, all S arrays and selected fields are identically +zero. All completed-X descendants after B1 and all five forward histories +are zero. Induction therefore covers every permitted homogeneous selected +controller, even with repeated S reads and arbitrary owner mixing. The +zero input has exactly the same permitted observations but a different +original A input. No decoder of those observations can restore both inputs. + +## Reproduction and evidence + +Python 3.12 standard library only, from the repository root: + +```sh +python3 -I -B scripts/research_package.py --package research/qq16-66port-second-axis +``` + +The registered hook runs normal and optimized exact replays plus the focused +integrity tests. Expected direct-verifier output: + +```text +PASS_QQ16_66PORT_SECOND_AXIS support=4 observed_ports=66 stages=9 controls=8 no_new_kappa +``` + +The implementation uses rational sums of bit functions and the full ordered +logical F/B formulas. It does not import predecessor Python. Equality to +zero is checked by exact cancellation of identical functions; nonzero +claims use an explicit owner evaluation. The checker authenticates six +source files and two archive members, checks the selected sections, binds +local stage/pair/orientation to the hosted template, and compares the full +typed receipt. Default replay is read-only; `--emit-result NEW_PATH` creates +a fresh receipt exclusively. + +Eight controls reject a coefficient sign error, reuse of the ineffective +first axis, a wrong initial cancellation sign, reading port 44, omitted +owner action, a missing cancelling bridge, a wrong F2 bank, and treating the +former-Y endpoint as an allowed zero observation. Positive controls show +that an extra port-44 read and a dense initial B0 query detect this witness. +The integrity tests check relocation and byte-preserving replay, reject an +on-disk receipt type change and source corruption, and reject removal of +proof-relevant receipt fields. Every mathematical check stays active under +`-O`. + +This is an author-checked scoped proof with exact finite source evidence. +It does not rerun the literal native child kernels, the selected full cold +replay, or a proof assistant. It inherits the retained local QQ16 contract. +No full-controller rank, alternative read-set optimum, physical read/retention +cost, hosting, recursive precision, all-size admission, or complete supplier +invoice is established. The selected frontier remains unchanged. Granting +all 66 reads and storage zero cost already fails this information screen, +so no favorable completed supplier budget is claimed. + +## Provenance and credit + +Base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +Task `joint-query-controller`, refined from scope key `0e34adbc1dd119161c3a`; +nonce `72c3e793ac4e1a0f869f8e219f301324`, recursive-interfaces track. +Exact source blobs and hashes are in [SOURCES.json](SOURCES.json); the +task card and overlap record are in [TASK.json](TASK.json). +Coordination uses [Discussion #2205](https://github.com/CrocSwap/integer-mult-bounds/discussions/2205). + +- **kyzer1023 / PR2354**, inspected head + `308ebc7405303bb7ed91b012bb705949c6091a16`: first-axis rank-74/defect-66 + certificate, the exact attaining read set, and this follow-up question. +- **Adam Gall / PR2093**, credited head + `8b21a900eb520e4f11ea177b310f66316f8e8983`: common-axis owner-function + witness and its A cancellation. **commdata2338 / PR2326**, credited head + `fb7d64cd4a51c49bc56920305b0aca64011a420c`: coordinate-read contract, + selected-shear/single-tap obstruction, and threshold question. Those heads + are recorded in PR2354; neither package is a runtime dependency here. +- **Ali Romman / PR1969**: retained QQ16 local maps, native packet, + cover semantics and ordinary schedule. Their existing source notices + remain at [joint-query/NOTICE.md](../joint-query/NOTICE.md). +- **Cinna Davis / PR2216 and PR2268**: selected shear and paired-tap repair. + **EdDiboi** and kyzer1023: preceding first-axis threshold investigations. + **@starship-s / [PR2368](https://github.com/CrocSwap/integer-mult-bounds/pull/2368)**, + head `e5d4d78dcfdd55d323fcbc60df477b9f25c7abff`, reports a separate + obstruction for the dense old-chart read. Its scope and next questions + were read at the final overlap check; its verifier was not replayed here. + The present witness is detected by that dense read, so it does not supply + PR2368's result or duplicate its different input family. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +OpenAI Codex (GPT-6 Astra) assisted with derivation, implementation, checking +and writing. Author-checked only; no independent human review is claimed. +New work is Apache-2.0. Frozen predecessor files are unchanged. + +## Open next questions + +1. **Which fixed ordinary read sets eliminate every local-axis family?** + This matters because a sharp threshold for one family need not repair + the controller. First form the simultaneous exact constraints from all + eight local chart axes for one proposed unread set. A surviving defect + is a falsifier; absence of one still requires testing other input families. + No new cardinality lower bound is asserted here. +The former dense-B0 follow-up has a separate reported negative answer in +PR2368 at the head credited above. Further dense-record work should start +from its changed-record or final-cut questions, not repeat the closed +old-chart experiment. No independent review of that result is claimed here. diff --git a/research/qq16-66port-second-axis/RESULT.json b/research/qq16-66port-second-axis/RESULT.json new file mode 100644 index 0000000000..0440610476 --- /dev/null +++ b/research/qq16-66port-second-axis/RESULT.json @@ -0,0 +1,642 @@ +{ + "archive_members": { + "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "coefficient_sum": [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + "common_axis_checks": 7168, + "initial_A": [ + { + "145": "1/2", + "4": "-1/2" + }, + { + "145": "1/2", + "25": "-1/2" + }, + { + "25": "-1/2", + "4": "1/2" + }, + {}, + { + "145": "1/2", + "4": "-1/2" + }, + { + "145": "-1/2", + "25": "1/2" + }, + { + "25": "1/2", + "4": "-1/2" + }, + {} + ], + "initial_A_at_identity": [ + "1/2", + "0", + "-1/2", + "0", + "1/2", + "0", + "1/2", + "0" + ], + "local_axis_zero_based": 1, + "observed_port_count": 66, + "old_chart_at_identity": [ + "-1", + "0", + "-1", + "0", + "0", + "-1", + "0", + "-1" + ], + "old_chart_query": [ + { + "145": "-1", + "4": "1" + }, + {}, + { + "25": "-1", + "4": "1" + }, + { + "145": "-1", + "25": "1" + }, + {}, + { + "145": "-1", + "4": "1" + }, + { + "145": "-1", + "25": "1" + }, + { + "25": "-1", + "4": "1" + } + ], + "positive_controls": [ + "extra port-44 read detects witness", + "dense initial B0 query detects witness" + ], + "read_ports": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 22, + 23, + 24, + 25, + 26, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 38, + 39, + 40, + 41, + 42, + 43, + 78, + 79, + 80, + 82, + 83, + 84, + 85, + 86, + 88, + 89, + 90, + 91, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109 + ], + "registered_port_stage_routes": 1008, + "rejected_controls": [ + "flip coefficient on port 70", + "reuse first axis with no original defect", + "reverse initial A cancellation sign", + "add a read of witness port 44", + "omit owner action at one source", + "omit cancelling bridge", + "wrong F2 bank binding", + "observe former-Y terminal output" + ], + "schema": "qq16-66port-second-axis-v1", + "scope": "specified read set only; no other 66-port-set or minimum-tap claim; no new kappa", + "source_sha256": { + "research/community-frontier1042-audit/selected-replay.tar.gz": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "research/joint-query/certificate.json.gz": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/joint-query/evidence/CONSERVED-QQ16.md": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75", + "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4" + }, + "status": "PASS_QQ16_66PORT_SECOND_AXIS", + "support": [ + { + "R_column": [ + "0", + "0", + "1", + "-1", + "0", + "0", + "-1", + "1" + ], + "axis": 25, + "coefficient": -1, + "port": 44 + }, + { + "R_column": [ + "1", + "0", + "0", + "1", + "0", + "1", + "1", + "0" + ], + "axis": 145, + "coefficient": -1, + "port": 49 + }, + { + "R_column": [ + "0", + "1", + "-1", + "0", + "1", + "0", + "0", + "-1" + ], + "axis": 4, + "coefficient": -1, + "port": 58 + }, + { + "R_column": [ + "1", + "1", + "0", + "0", + "1", + "1", + "0", + "0" + ], + "axis": 4, + "coefficient": 1, + "port": 70 + } + ], + "trace": [ + { + "event": { + "kind": "local", + "pair": 0, + "reverse": false, + "stage": 0 + }, + "ordinary": [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "kind": "local", + "pair": 0, + "reverse": true, + "stage": 1 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "coefficient": 1, + "dst": 0, + "kind": "bridge", + "src": 1 + }, + "ordinary": [ + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "kind": "local", + "pair": 0, + "reverse": false, + "stage": 2 + }, + "ordinary": [ + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "coefficient": -1, + "dst": 0, + "kind": "bridge", + "src": 1 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "kind": "local", + "pair": 1, + "reverse": true, + "stage": 3 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "coefficient": 1, + "dst": 1, + "kind": "bridge", + "src": 2 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "kind": "local", + "pair": 1, + "reverse": false, + "stage": 4 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "coefficient": -1, + "dst": 1, + "kind": "bridge", + "src": 2 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "kind": "local", + "pair": 2, + "reverse": true, + "stage": 5 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "coefficient": 1, + "dst": 2, + "kind": "bridge", + "src": 3 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "kind": "local", + "pair": 2, + "reverse": false, + "stage": 6 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "coefficient": -1, + "dst": 2, + "kind": "bridge", + "src": 3 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "kind": "local", + "pair": 3, + "reverse": true, + "stage": 7 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "kind": "local", + "pair": 3, + "reverse": false, + "stage": 8 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "coefficient": 1, + "dst": 3, + "kind": "bridge", + "src": 2 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "coefficient": 1, + "dst": 2, + "kind": "bridge", + "src": 1 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "coefficient": 1, + "dst": 1, + "kind": "bridge", + "src": 0 + }, + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "event": { + "kind": "terminal", + "pairs": 4 + }, + "ordinary": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + ], + "unread_ports": [ + 44, + 45, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 77 + ], + "zero_forward_histories": [ + 0, + 2, + 4, + 6, + 8 + ], + "zero_later_queries": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ] +} diff --git a/research/qq16-66port-second-axis/SOURCES.json b/research/qq16-66port-second-axis/SOURCES.json new file mode 100644 index 0000000000..18e2b59c34 --- /dev/null +++ b/research/qq16-66port-second-axis/SOURCES.json @@ -0,0 +1,54 @@ +{ + "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/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "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-COVER-ACTION-ADDENDUM.md", + "usage": "input", + "git_blob": "3dd1a990d7b9d57cfb20cf8e8dd45548f043a944", + "sha256": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "usage": "input", + "git_blob": "5082d791d0b993492cbc5bf61ac3b69e82c96f3f", + "sha256": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4" + } + ] +} diff --git a/research/qq16-66port-second-axis/TASK.json b/research/qq16-66port-second-axis/TASK.json new file mode 100644 index 0000000000..cf4ceceb52 --- /dev/null +++ b/research/qq16-66port-second-axis/TASK.json @@ -0,0 +1,161 @@ +{ + "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": "Falsify arbitrary-input restoration for the exact 66 ordinary source-port set attaining PR2354's first-axis family threshold, using a second-axis witness on its 30 unread ports through the fixed QQ16 first pair and full ordinary tail.", + "scope_change_reason": "Take PR2354 Open next question 2, a live central handoff. The specified observation set changes the selected-only witness premise; a second local-axis family changes the predecessor's first-axis restriction. This is separate from the separate dense-old-chart observation question, now reported closed by PR2368.", + "bottleneck_link": "The missing QQ16 controller must restore selected inputs. Even zero-cost access to these 66 ports fails; family-only sufficiency cannot justify building this controller.", + "budget_minutes": 60, + "stop_rule": "Stop at an exact nonzero original selected input with identically zero allowed observations; otherwise stop after axes 1..7 and report a bounded handoff. Reserve final quarter for verification.", + "outcome": "negative-result", + "evidence": "README.md gives the proof; RESULT.json records a four-port witness, 1008 registered routes, 7168 common-axis checks, all 19 ordered events, eight rejected controls and two detecting observations. verify.py and test_integrity.py provide exact replay and corruption controls.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex (GPT-6 Astra) assistance with derivation, implementation, checking and writing; author-checked only, no independent human review claimed.", + "open_questions": [ + { + "question": "Which fixed coordinate read sets eliminate every local-axis family?", + "why_it_matters": "A threshold for one family does not establish controller recovery.", + "first_step": "Form exact constraints for all eight local chart axes on one proposed unread set and test for a surviving original A defect.", + "blocked_by": "Even simultaneous family elimination leaves other input families and physical implementation unchecked." + } + ], + "selection": { + "nonce": "72c3e793ac4e1a0f869f8e219f301324", + "track": "recursive-interfaces", + "catalog_scope_key": "0e34adbc1dd119161c3a", + "refined_scope_key": "QQ16/PR2354-attaining-66-ports/unread30/second-axis-witness", + "choice": "Second suggestion, taking PR2354 Open next question 2. No reroll.", + "passed_over": { + "coverage-law-change": "Basic one-unpaid-coordinate obstruction covered by #1587; less specific than this central handoff.", + "centre-path-sharing": "Specific source-rank/native-fusion follow-ups already covered; prefer this unclaimed restoration question." + } + }, + "predecessor": { + "pr": 2354, + "head": "308ebc7405303bb7ed91b012bb705949c6091a16", + "runtime_dependency": false + }, + "overlap": { + "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2205", + "open_prs_fetched_at": "2026-10-15T06:28:56.749233+00:00", + "open_pr_count": 570, + "discussions_fetched_at": "2026-10-15T06:31:18.032505+00:00", + "discussion_records": 1082, + "complete_pagination": true, + "mode": "cached/offline; no novelty guarantee", + "queries": [ + "--task joint-query-controller", + "--task coverage-law-change", + "66-port; attaining coordinate; second-axis" + ], + "nearest": [ + "#2354 first-axis family-only sufficiency; this tests a different family on its exact read set.", + "#2326 every single-port tap; this tests its successor 66-port set.", + "#2174 two dense reads plus A output; not a coordinate-set theorem.", + "#2368 closes the separate dense-old-chart question with another hidden-input family; this witness is detected by that read." + ], + "final_refresh": { + "open_prs_fetched_at": "2026-10-15T06:55:23.240869+00:00", + "open_pr_count": 583, + "discussions_fetched_at": "2026-10-15T06:57:32.010338+00:00", + "discussion_records": 1111, + "complete_pagination": true, + "queries": [ + "--task joint-query-controller", + "66-port; second-axis; attaining coordinate" + ], + "result": "Own posted claim is visible. No duplicate fixed-set second-axis result found. PR2368 reports the separate dense-B0 obstruction, read and credited at final refresh. Concurrent adaptive-coordinate work keeps the first-axis family; this changes the input family for one fixed set." + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2205#discussioncomment-18942783" + }, + "optimistic_budget": "Grant all 66 reads, retention, owner mixing and selected shear free; a hidden selected input still defeats restoration. No native tariff or supplier bill is inferred.", + "unrun_obligations": [ + "literal native child kernels", + "selected full cold replay", + "proof-assistant formalization", + "complete arbitrary-input kernel dimension", + "other 66-port sets or minimum tap count", + "dense-query retention", + "physical read/hosting/precision/all-size supplier admission" + ], + "task_card": { + "object_and_question": "Falsify arbitrary-input restoration for the exact 66 ordinary source-port set attaining PR2354's first-axis family threshold, using a second-axis witness on its 30 unread ports through the fixed QQ16 first pair and full ordinary tail.", + "base_and_dependencies": { + "main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "question_predecessor_pr2354": "308ebc7405303bb7ed91b012bb705949c6091a16", + "runtime_inputs": "Six unchanged main files pinned by SOURCES.json; no pending-PR runtime dependency." + }, + "changed_restriction": "First-axis witness family replaced by a second-axis family on the exact unread set; ordinary fields and first pair fixed.", + "method_and_domain": "Exact rational four-column relation; actual 73-dimensional binary route matrices; payload-constant all-owner functions; every event of the fixed 19-event recipe. A brief discovery scan considered local axes 1..7; the submitted certificate fixes axis 1 and makes no other-axis completeness claim.", + "success_and_falsification": "Nonzero original A value, zero permitted observations. Coefficient/sign/route/read/schedule mutations must be detected.", + "budget": "Grant all 66 reads, retention, owner mixing and selected shear free; a hidden selected input still defeats restoration. No native tariff or supplier bill is inferred.", + "time_cap_minutes": 60, + "artifact_and_command": "python3 -I -B scripts/research_package.py --package research/qq16-66port-second-axis", + "credit": "kyzer1023, Adam Gall, commdata2338, Ali Romman, Cinna Davis, EdDiboi, and retained supplier authors." + }, + "upstream_refresh": { + "checked_at_utc": "2026-10-15T07:04:16.723217+00:00", + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "changes_since_base": "None on canonical main, guidance, selected record or consumed sources. PR2354 head unchanged. New board evidence: parallel PR2368 reports the dense-query question closed; update next-question routing only.", + "decision": "Continue and submit the scoped counterexample from the unchanged scientific base." + }, + "validation_environment": { + "python": "3.12.3", + "dependencies": "standard library only", + "platform": "Linux", + "registered_command": "python3 -I -B scripts/research_package.py --package research/qq16-66port-second-axis" + }, + "parallel_work": { + "pr2368": { + "head": "e5d4d78dcfdd55d323fcbc60df477b9f25c7abff", + "author": "starship-s", + "inspection": "README scope and next questions read; no independent replay or dependency on its theorem.", + "difference": "Dense B0 record with a different hidden-input family; the present four-port witness is detected by that record." + } + } +} diff --git a/research/qq16-66port-second-axis/VERIFY.json b/research/qq16-66port-second-axis/VERIFY.json new file mode 100644 index 0000000000..d5f513b111 --- /dev/null +++ b/research/qq16-66port-second-axis/VERIFY.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "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-COVER-ACTION-ADDENDUM.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact all-owner witness, source/route bindings, all 19 ordered events, complete typed receipt and eight mathematical controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All acceptance and mutation checks remain active under optimization." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_integrity.py", + "-v" + ], + "timeout_seconds": 240, + "checks": "Focused relocation/read-only replay, source and receipt corruption, and proof-relevant receipt field controls." + } + ] +} diff --git a/research/qq16-66port-second-axis/test_integrity.py b/research/qq16-66port-second-axis/test_integrity.py new file mode 100644 index 0000000000..f0ca793177 --- /dev/null +++ b/research/qq16-66port-second-axis/test_integrity.py @@ -0,0 +1,73 @@ +"""Relocated positive replay and proof-relevant corruption controls.""" +from copy import deepcopy +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +spec = importlib.util.spec_from_file_location("second_axis_verifier", PACKAGE / "verify.py") +verify = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verify) + + +class IntegrityTests(unittest.TestCase): + def test_typed_complete_receipt(self): + good = json.loads((PACKAGE / "RESULT.json").read_text()) + verify.equal_receipt(good, deepcopy(good)) + for field, value in (("observed_port_count", True), ("support", []), + ("zero_later_queries", [1]), ("trace", [])): + with self.subTest(field=field): + bad = deepcopy(good) + bad[field] = value + with self.assertRaisesRegex(ValueError, "typed receipt"): + verify.equal_receipt(good, bad) + + def test_relocated_replay_and_corruption(self): + # Keep disposable copies adjacent to the checkout, never alter frozen inputs. + with tempfile.TemporaryDirectory(prefix="qq16-integrity-", dir=ROOT.parent) as temp: + root = Path(temp) + package = root / "research" / PACKAGE.name + shutil.copytree(PACKAGE, package, ignore=shutil.ignore_patterns("__pycache__")) + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + target = root / row["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / row["path"], target) + + def run(): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py")], + cwd=root, capture_output=True, text=True, timeout=90) + + before = {str(p.relative_to(root)): p.read_bytes() for p in root.rglob("*") if p.is_file()} + result = run() + self.assertEqual(result.returncode, 0, result.stderr[-2000:]) + self.assertIn("PASS_QQ16_66PORT_SECOND_AXIS", result.stdout) + after = {str(p.relative_to(root)): p.read_bytes() for p in root.rglob("*") if p.is_file()} + self.assertEqual(before, after, "replay changed copied input or package bytes") + + receipt = package / "RESULT.json" + original = receipt.read_text() + bad = json.loads(original) + bad["observed_port_count"] = True + receipt.write_text(json.dumps(bad)) + result = run() + self.assertNotEqual(result.returncode, 0) + self.assertIn("typed receipt mismatch", result.stderr) + receipt.write_text(original) + + source = root / "research/joint-query/evidence/CONSERVED-QQ16.md" + source.write_bytes(source.read_bytes() + b"\ncorrupted source control\n") + result = run() + self.assertNotEqual(result.returncode, 0) + self.assertIn("source hash mismatch", result.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-66port-second-axis/verify.py b/research/qq16-66port-second-axis/verify.py new file mode 100644 index 0000000000..1b78459083 --- /dev/null +++ b/research/qq16-66port-second-axis/verify.py @@ -0,0 +1,365 @@ +#!/usr/bin/env python3 +"""QQ16 66-port counterexample; exact sums of f_v(d)=bit_0(d v). + +Empty sums prove identities; evaluation proves inequality. Independence of +the f_v is never assumed. No predecessor Python is imported. Apache-2.0. +Prepared for commdata2338 with substantial OpenAI Codex assistance. +""" +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import gzip +from hashlib import sha256 +from io import BytesIO +import json +from pathlib import Path +import tarfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +PACKET = "research/joint-query/certificate.json.gz" +PREVIOUS = "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json" +MEMBERS = { + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": + "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": + "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", +} +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] +UNREAD = [44, 45, 48, 49, 50, 51, 52, 53, 54, 55, 56, 58, 59, 60, + 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 77] +READ = [p for p in U if p not in UNREAD] +COEFFICIENTS = {44: -1, 49: -1, 58: -1, 70: 1} +IDENTITY = tuple(1 << i for i in range(73)) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def equal_receipt(actual, expected): + require(canonical(actual) == canonical(expected), "complete typed receipt mismatch") + + +def authenticate(raw, pin, label): + require(sha256(raw).hexdigest() == pin, "source hash mismatch: " + label) + return raw + + +def sources(root=ROOT): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + pins = {f["path"]: f["sha256"] for f in manifest["files"] if f["usage"] == "input"} + require(set(pins) == {ARCHIVE, PACKET, PREVIOUS, + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md"}, + "complete declared source set") + raw = {name: authenticate((root / name).read_bytes(), pin, name) + for name, pin in pins.items()} + decoded = [] + with tarfile.open(fileobj=BytesIO(raw[ARCHIVE]), mode="r:gz") as archive: + for name, pin in MEMBERS.items(): + matches = [m for m in archive.getmembers() if m.name == name] + require(len(matches) == 1 and matches[0].isfile(), "unique regular archive member") + data = authenticate(archive.extractfile(matches[0]).read(), pin, name) + decoded.append(json.loads(gzip.decompress(data) if name.endswith(".gz") else data)) + return (json.loads(gzip.decompress(raw[PACKET])), *decoded, + json.loads(raw[PREVIOUS]), pins) + + +def combination(terms): + """Rational linear combination of dictionaries representing f_v functions.""" + out = {} + for scale, function in terms: + for v, coefficient in function.items(): + value = out.get(v, Q(0)) + scale * coefficient + if value: + out[v] = value + else: + out.pop(v, None) + return out + + +def action(columns, vector): + result = 0 + for i, column in enumerate(columns): + if (vector >> i) & 1: + result ^= column + return result + + +def transport(function, columns): + return combination((coefficient, {action(columns, v): Q(1)}) + for v, coefficient in function.items()) + + +def evaluate(function, owner=IDENTITY): + return sum((c * (action(owner, v) & 1) for v, c in function.items()), Q(0)) + + +def serialize(function): + return {str(v): str(c) for v, c in sorted(function.items())} + + +def zero_bank(): + return [{} for _ in range(112)] + + +def derive_routes(packet, phases): + require(phases["m"] == 73 and len(phases["recipes"]) == 112, "source dimensions") + registered = {tuple(m["owner_right_matrix_columns"]) + for m in packet["map_registry"].values()} + bases, routes = [], {} + for p, record in enumerate(phases["recipes"]): + basis = record["idle_children"][0]["orthogonal_axes"][:8] + local = [record["q"], *basis] + require(record["port"] == p and len(local) == 9, "source port binding") + require(all(0 < v < 512 for v in local), "local chart support") + require(all(((v & w).bit_count() % 2) == int(i == j) + for i, v in enumerate(local) for j, w in enumerate(local)), + "orthonormal local chart") + bases.append(basis) + for s in range(9): + columns = list(IDENTITY) + if s: + for i, b in enumerate(basis): + delta = b ^ (1 << (9 + 8 * (s - 1) + i)) + columns = [v ^ delta if (v & delta).bit_count() % 2 else v + for v in columns] + columns = tuple(columns) + require(columns in registered, "route missing from native map registry") + require(all(action(columns, columns[i]) == IDENTITY[i] for i in range(73)), + "route inverse") + require(action(columns, record["q"]) == record["q"], "route fixes port line") + if s: + require(all(action(columns, b) == 1 << (9 + 8 * (s - 1) + i) + for i, b in enumerate(basis)), "all-axis route identity") + routes[s, p] = columns + require([p for p in U if bases[p][0] == 2] == UNREAD, + "PR2354 exact attaining unread set") + return bases, routes + + +class Model: + """Ordered logical maps from the retained conserved QQ16 contract.""" + def __init__(self, packet, routes): + require((packet["A_ports"], packet["T_ports"], packet["U_ports"]) == (A, T, U), + "QQ16 partition") + self.R = [[Q(row.get(str(p), "0")) for p in range(112)] for row in packet["R_rows"]] + require(len(self.R) == 8, "query width") + self.routes = routes + for ports, scale in ((A, 4), (T, 4), (U, 48)): + require(all(sum(self.R[i][p] * self.R[j][p] for p in ports) + == (scale if i == j else 0) for i in range(8) for j in range(8)), + "actual selected and ordinary Grams") + + def query(self, fields, stage, ports=range(112)): + return [combination((row[p], transport(fields[p], self.routes[stage, p])) + for p in ports) for row in self.R] + + def inject(self, query, stage, ports): + fields = zero_bank() + for p in ports: + value = combination((self.R[k][p] / 4, query[k]) for k in range(8)) + fields[p] = transport(value, self.routes[stage, p]) + return fields + + def forward(self, x, y, stage): + f = self.query(x, stage) + k = self.inject(f, stage, U) + old_t = self.inject(self.query(x, stage, T), stage, A) + new_t = self.inject(f, stage, T) + xx, yy = zero_bank(), zero_bank() + for p in U: + xx[p] = combination([(1, x[p]), (-1, k[p])]) + yy[p] = combination([(1, y[p]), (1, xx[p])]) + for p in A + T: + xx[p] = old_t[p] if p in A else new_t[p] + yy[p] = combination([(1, x[p]), (1, y[p]), (-1, xx[p])]) + return xx, yy, f + + def backward(self, x, y, stage, future): + q = self.query(y, future, U + T) + logger = self.inject(q, future, A) + u = [combination([(1, yy), (1, ll)]) for yy, ll in zip(y, logger)] + a = self.query(x, stage, T) + b = self.query(u, stage) + ku = self.inject(a, stage, U) + correction = self.inject([combination([(1, bb), (11, aa)]) + for aa, bb in zip(a, b)], stage, T) + target = self.inject([combination([(1, bb), (12, aa)]) + for aa, bb in zip(a, b)], stage, T) + xx, yy = zero_bank(), zero_bank() + for p in U: + xx[p] = combination([(1, x[p]), (-1, y[p])]) + yy[p] = combination([(1, y[p]), (1, ku[p])]) + for p in A: + xx[p] = combination([(1, x[p]), (1, y[p]), (-1, u[p])]) + yy[p] = u[p] + for p in T: + xx[p] = target[p] + yy[p] = combination([(1, u[p]), (-1, correction[p])]) + return xx, yy + + +def bind_schedule(recipe, calls): + require(recipe[:2] == [{"kind": "local", "pair": 0, "reverse": False, "stage": 0}, + {"kind": "local", "pair": 0, "reverse": True, "stage": 1}], + "fixed F0/B1 first pair") + scheduled = {(e["stage"], e["pair"], "backward" if e["reverse"] else "forward") + for e in recipe if e["kind"] == "local"} + require(scheduled == {(c["stage"], c["pair"], c["orientation"]) for c in calls}, + "local stage/pair/orientation differs from hosted template") + + +def replay(model, template, h, reads=READ, initial_sign=-1): + H = model.query(h, 0) + require(any(evaluate(f) for f in H), "old-chart defect is not witnessed at identity") + for stage in range(1, 9): + require(not any(model.query(h, stage)), "later query does not vanish identically") + selected = model.inject(H, 0, A) + x, y = deepcopy(h), zero_bank() + for p in A: + x[p] = combination([(initial_sign, selected[p])]) + y[p] = combination([(-initial_sign, selected[p])]) + initial_A = [x[p] for p in A] + require(any(evaluate(f) for f in initial_A), "nonzero original selected input") + banks = [[x, y]] + [[zero_bank(), zero_bank()] for _ in range(3)] + trace, histories = [], [] + bind_schedule(template["recipe"], template["calls"]) + for index, event in enumerate(template["recipe"]): + kind = event["kind"] + if kind == "local": + pair, stage = event["pair"], event["stage"] + x, y = banks[pair] + if event["reverse"]: + banks[pair] = list(model.backward(x, y, stage, stage + 1)) + else: + xx, yy, f = model.forward(x, y, stage) + require(not any(f), "forward history is nonzero") + histories.append(stage) + banks[pair] = [xx, yy] + elif kind == "bridge": + source, target, c = event["src"], event["dst"], event["coefficient"] + for p in U: + banks[target][0][p] = combination([(1, banks[target][0][p]), + (c, banks[source][0][p])]) + banks[source][1][p] = combination([(1, banks[source][1][p]), + (-c, banks[target][1][p])]) + else: + require(kind == "terminal" and index == len(template["recipe"]) - 1, + "unique final terminal") + banks = [[y, [combination([(-1, f)]) for f in x]] for x, y in banks] + require(not any(fields[p] for pair in banks for fields in pair for p in A + T), + "selected output survives") + require(not any(fields[p] for pair in banks for fields in pair for p in reads), + "ordinary read transcript is nonzero") + if index >= 1: + completed_side = 1 if kind == "terminal" else 0 + require(not any(pair[completed_side][p] for pair in banks for p in U), + "completed-X descendant is nonzero") + multipliers = [] + for pair in banks: + for fields in pair: + candidates = [c for c in (-1, 0, 1) + if all(fields[p] == combination([(c, h[p])]) for p in U)] + require(len(candidates) == 1, "ordinary trajectory not a unique h multiple") + multipliers.append(candidates[0]) + trace.append({"event": event, "ordinary": multipliers}) + require(histories == [0, 2, 4, 6, 8], "all five forward histories") + require(trace[-1]["ordinary"] == [1, 0, 0, 0, 0, 0, 0, 0], "former-Y endpoint") + return initial_A, H, trace + + +def build_result(): + packet, phases, template, previous, pins = sources() + bases, routes = derive_routes(packet, phases) + model = Model(packet, routes) + h = zero_bank() + for p, c in COEFFICIENTS.items(): + h[p] = {bases[p][1]: Q(c)} + require([bases[p][1] for p in COEFFICIENTS] == [25, 145, 4, 4], "second axes") + coefficient_sum = [sum(row[p] * c for p, c in COEFFICIENTS.items()) for row in model.R] + require(coefficient_sum == [0] * 8, "four-column rational relation") + initial_A, H, trace = replay(model, template, h) + require([entry["ordinary"] for entry in trace[2:]] == + [entry["ordinary"] for entry in previous["trajectory_after_B1"]], + "retained ordinary-tail receipt") + require([evaluate(f) for f in H] == [-1, 0, -1, 0, 0, -1, 0, -1], + "explicit nonzero old-chart value") + controls = [] + + def rejects(name, check): + try: + check() + except ValueError: + controls.append(name) + else: + raise ValueError("mutation was not rejected: " + name) + + bad_h = deepcopy(h) + bad_h[70] = {bases[70][1]: Q(-1)} + rejects("flip coefficient on port 70", lambda: replay(model, template, bad_h)) + first_h = zero_bank() + for p, c in COEFFICIENTS.items(): + first_h[p] = {bases[p][0]: Q(c)} + rejects("reuse first axis with no original defect", lambda: replay(model, template, first_h)) + rejects("reverse initial A cancellation sign", lambda: replay(model, template, h, initial_sign=1)) + rejects("add a read of witness port 44", lambda: replay(model, template, h, reads=READ + [44])) + wrong_routes = dict(routes) + wrong_routes[1, 44] = IDENTITY + rejects("omit owner action at one source", lambda: replay(Model(packet, wrong_routes), template, h)) + wrong = deepcopy(template) + wrong["recipe"] = [e for e in wrong["recipe"] if e != + {"kind": "bridge", "src": 1, "dst": 0, "coefficient": -1}] + rejects("omit cancelling bridge", lambda: replay(model, wrong, h)) + wrong = deepcopy(template) + next(e for e in wrong["recipe"] if e.get("stage") == 2)["pair"] = 1 + rejects("wrong F2 bank binding", lambda: replay(model, wrong, h)) + rejects("observe former-Y terminal output", lambda: require(not any(h), "extra final read sees h")) + require(evaluate(h[44]) == -1, "additional port-44 read detects this witness") + require(any(evaluate(f) for f in H), "dense old-chart positive detection control") + return { + "schema": "qq16-66port-second-axis-v1", "status": "PASS_QQ16_66PORT_SECOND_AXIS", + "source_sha256": pins, "archive_members": MEMBERS, + "read_ports": READ, "unread_ports": UNREAD, "observed_port_count": len(READ), + "local_axis_zero_based": 1, + "support": [{"port": p, "coefficient": c, "axis": bases[p][1], + "R_column": [str(row[p]) for row in model.R]} for p, c in COEFFICIENTS.items()], + "coefficient_sum": [str(x) for x in coefficient_sum], + "old_chart_query": [serialize(f) for f in H], + "old_chart_at_identity": [str(evaluate(f)) for f in H], + "initial_A": [serialize(f) for f in initial_A], + "initial_A_at_identity": [str(evaluate(f)) for f in initial_A], + "registered_port_stage_routes": len(routes), "common_axis_checks": 112 * 8 * 8, + "zero_later_queries": list(range(1, 9)), "zero_forward_histories": [0, 2, 4, 6, 8], + "trace": trace, "rejected_controls": controls, + "positive_controls": ["extra port-44 read detects witness", "dense initial B0 query detects witness"], + "scope": "specified read set only; no other 66-port-set or minimum-tap claim; no new kappa", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-result", type=Path, help="write a new receipt exclusively") + args = parser.parse_args() + result = build_result() + if args.emit_result: + with args.emit_result.open("x", encoding="utf-8") as output: + json.dump(result, output, indent=2, sort_keys=True) + output.write("\n") + else: + equal_receipt(result, json.loads((PACKAGE / "RESULT.json").read_text())) + print("PASS_QQ16_66PORT_SECOND_AXIS support=4 observed_ports=66 stages=9 controls=8 no_new_kappa") + + +if __name__ == "__main__": + main()