From 4bdc574da394a39f955e8cf4637075649c43a632 Mon Sep 17 00:00:00 2001 From: ross Date: Thu, 15 Oct 2026 06:23:47 +1100 Subject: [PATCH] Quantify QQ16 residual information after an extra B2 query --- .../qq16-extra-query-residual/ORACLE.json | 1483 +++++++++++++++++ research/qq16-extra-query-residual/PROOF.md | 336 ++++ research/qq16-extra-query-residual/README.md | 154 ++ .../qq16-extra-query-residual/RESULT.json | 785 +++++++++ .../qq16-extra-query-residual/REVIEW.json | 48 + .../qq16-extra-query-residual/SOURCES.json | 100 ++ research/qq16-extra-query-residual/TASK.json | 135 ++ .../qq16-extra-query-residual/VERIFY.json | 40 + .../qq16-extra-query-residual/independent.py | 424 +++++ .../qq16-extra-query-residual/test_package.py | 162 ++ research/qq16-extra-query-residual/verify.py | 295 ++++ 11 files changed, 3962 insertions(+) create mode 100644 research/qq16-extra-query-residual/ORACLE.json create mode 100644 research/qq16-extra-query-residual/PROOF.md create mode 100644 research/qq16-extra-query-residual/README.md create mode 100644 research/qq16-extra-query-residual/RESULT.json create mode 100644 research/qq16-extra-query-residual/REVIEW.json create mode 100644 research/qq16-extra-query-residual/SOURCES.json create mode 100644 research/qq16-extra-query-residual/TASK.json create mode 100644 research/qq16-extra-query-residual/VERIFY.json create mode 100644 research/qq16-extra-query-residual/independent.py create mode 100644 research/qq16-extra-query-residual/test_package.py create mode 100644 research/qq16-extra-query-residual/verify.py diff --git a/research/qq16-extra-query-residual/ORACLE.json b/research/qq16-extra-query-residual/ORACLE.json new file mode 100644 index 0000000000..7354eda14c --- /dev/null +++ b/research/qq16-extra-query-residual/ORACLE.json @@ -0,0 +1,1483 @@ +{ + "controls": { + "coefficient_change": "REJECT: ordinary column Gram", + "port_reordering_and_whole_column_signs": "PASS", + "reversed_noncommuting_route_product": { + "basis_axis": 0, + "correct_image": 1179667, + "port": 1, + "reversed_image": 4627, + "status": "REJECT: ordered route product" + }, + "route_collision": { + "distinct_routes": 95, + "identity_coefficient_trace": 1544, + "named_distinctness_check": "REJECT" + }, + "source_payload_mutation": "REJECT: source digest" + }, + "reconstruction": { + "A_ports": [ + 0, + 7, + 20, + 27, + 36, + 46, + 57, + 111 + ], + "R_dense": [ + [ + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 1, + 1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + -1, + 1, + -1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + -1, + 1, + 0, + 0, + -1, + 1, + 1, + 1, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 0, + 1, + 0, + 1, + -1, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 0, + 0, + 0, + 1, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + -1, + 0, + 0 + ], + [ + 0, + -1, + 0, + -1, + 0, + 0, + 1, + 0, + 1, + 0, + -1, + -1, + 1, + 0, + 1, + 1, + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + -1, + 0, + -1, + 0, + -1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + 1, + 1, + -1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + 0, + 1, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + -1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + -1, + 0, + -1, + 0, + 0, + 1, + 0, + 1, + 0, + 0, + -1, + -1, + 0, + -1, + 0, + -1, + -1, + 0, + 1, + 0, + 1, + 0, + 0, + 1, + 0, + 1, + 0, + 0, + 1, + 0, + -1, + -1, + 1, + 0, + 0, + 1, + 1 + ], + [ + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + -1, + 1, + 0, + 0, + 1, + -1, + -1, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + -1, + 1, + 0, + 1, + -1, + 0, + -1, + 1, + 1, + -1, + 0, + 0, + 0, + -1, + 1, + 0, + 1, + -1, + 0, + 1, + -1, + 1, + -1, + 0, + 0, + 0, + 1, + -1, + 0, + -1, + 1, + 1, + -1, + 0, + 0, + 1, + -1, + 1, + -1, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + -1, + 0, + 1, + -1, + -1, + 1 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 1, + -1, + -1, + 0, + -1, + -1, + 0, + 0, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + -1, + -1, + 0, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + 0, + 0, + -1, + 1, + -1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 1, + 1, + -1, + -1 + ], + [ + 0, + -1, + -1, + 0, + -1, + -1, + 1, + 0, + 0, + -1, + 0, + 0, + 0, + 1, + 0, + 0, + -1, + 0, + 1, + 1, + -1, + -1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 0, + -1, + 1, + 1, + 0, + -1, + -1, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + -1, + 0, + 0, + -1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + 0, + 0, + 1, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + 0, + 1, + 0, + 0, + -1, + 1, + 0, + 0, + -1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + 0, + 0, + 0, + 1, + -1, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 0, + -1, + 0, + 0, + -1, + 0, + 0, + -1, + -1 + ] + ], + "R_dense_sha256": "4766159d79608cc4e943b59d971f37763835ceb07f39e5a8319f5ebc4fcad91f", + "R_rows_integer_json_sha256": "4766159d79608cc4e943b59d971f37763835ceb07f39e5a8319f5ebc4fcad91f", + "T_ports": [ + 21, + 37, + 47, + 76, + 81, + 87, + 92, + 110 + ], + "U_column_squared_norm_histogram": { + "4": 96 + }, + "U_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, + 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, + 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 + ], + "centre_output_registers": [ + 92, + 57, + 81, + 224, + 11, + 240, + 9, + 256 + ], + "method_R": "reverse covectors on all 712 independent input positions, then source projection", + "method_routes": "orthonormal chart/stage coordinate swaps; 73 binary columns per route", + "retained_helper_dependencies_per_row": [ + 55, + 50, + 54, + 51, + 48, + 49, + 47, + 50 + ], + "routes_U96_stage_major_sha256": "f55db68178127a8ba23820eba933e1417b3db3d8eaa2bce2a343d14907a48c2b", + "scalar_prefix_event_count": 12550, + "stage_0_1_2_route_columns_sha256": "6b5e3e9f6037b242625eeb14d32cd392da2035ee95d57c7b940c68b909890203" + }, + "same_stage_gram": [ + [ + 48, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 48, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 48, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 48, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 48, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 48, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 48, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 48 + ] + ], + "scope": { + "collision_rule": "sum over each relative-route bucket K_g of K_g K_g^T", + "finite_coverage": "112 actual R columns and stage 0/1/2 routes; all 96 ordinary columns and all three pairs", + "matrix_convention": "GF(2) matrices stored as columns; product(g,h) maps x to g(h(x)); D_gD_h=D_(gh)", + "not_checked": [ + "full regular cover enumeration", + "QQ16 chronological trajectory", + "native phase replay", + "precision or physical routing costs", + "complete supplier", + "new kappa" + ], + "representation": "finite regular right cover action, payload-constant fields; arbitrary cover values" + }, + "source": { + "archive_path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "member_sha256_and_payload_sha256": { + "slots/local/CANONICAL-WORD.json.gz": [ + "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c" + ], + "slots/local/LOCAL-PROGRAMS.json.gz": [ + "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "9f41d53659e9be84e20c661560c5687abbf5cd0660cdecbe01ad5eb29e6b8ee3" + ], + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": [ + "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + ] + } + }, + "stage_pairs": { + "0,1": { + "distinct_relative_routes": 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 + ] + ], + "identity_coefficient_trace": 1536, + "operator": "B_s B_t* B_t B_s*", + "relative_route_columns_sha256": "3ab11c32aa2a2fe41cfcd48af4156bfdab95d1dccdc0a52cec01ff9544b5e8fa", + "relative_route_order": "rho_s(p) rho_t(p)^-1", + "route_multiplicity_histogram": { + "1": 96 + } + }, + "0,2": { + "distinct_relative_routes": 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 + ] + ], + "identity_coefficient_trace": 1536, + "operator": "B_s B_t* B_t B_s*", + "relative_route_columns_sha256": "a071cc6f2fdd1335103470d6092a9ad86ec37f43534621dd4b4de7319e0edbd5", + "relative_route_order": "rho_s(p) rho_t(p)^-1", + "route_multiplicity_histogram": { + "1": 96 + } + }, + "1,2": { + "distinct_relative_routes": 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 + ] + ], + "identity_coefficient_trace": 1536, + "operator": "B_s B_t* B_t B_s*", + "relative_route_columns_sha256": "57c975bc42b34a7130779c11944eda6d3ad3ff82ee46af1de94ae4b3d7828c4d", + "relative_route_order": "rho_s(p) rho_t(p)^-1", + "route_multiplicity_histogram": { + "1": 96 + } + } + }, + "status": "PASS_INDEPENDENT_QQ16_THREE_QUERY_TRACE", + "trace_coefficients_per_regular_cover_order": { + "rank_B0_restricted_to_joint_kernel_B1_B2_lower_bound": "32/7", + "stacked_Gram_square_trace": 64512, + "stacked_Gram_trace": 1152, + "stacked_query_rank_lower_bound": "144/7" + } +} diff --git a/research/qq16-extra-query-residual/PROOF.md b/research/qq16-extra-query-residual/PROOF.md new file mode 100644 index 0000000000..388bca8797 --- /dev/null +++ b/research/qq16-extra-query-residual/PROOF.md @@ -0,0 +1,336 @@ +# Residual selected information after a free pre-F0 ordinary query + +The fixed QQ16 `F0/B1` pair and retained ordinary bank schedule still +cannot restore every original selected input after the complete value +`B2 X_U` is supplied immediately before `F0`. This statement grants that +query exact, free, read-only access and indefinite retention. There are +at least `ceil(32 |G| / 7)` independent missing selected-input directions +on a finite regular cover `G`. This is an information-space dimension, +not a paid recursive-child rank or a native operation count. + +This note addresses Cinna Davis's proposed extra query in +[PR #2079](https://github.com/CrocSwap/integer-mult-bounds/pull/2079), +head `49df8190b158e3028e702b2c6b798117006f7249`, and +[discussion #2074](https://github.com/CrocSwap/integer-mult-bounds/discussions/2074). +The source checkout is `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. +The predecessor identifies a real observation absent from the old +witness. The new result is that supplying that particular observation +does not suffice for this fixed controller. + +## Exact model and source obligations + +Use the sets and ordered maps in +[`CONSERVED-QQ16.md`](../joint-query/evidence/CONSERVED-QQ16.md) and +[`JOINT-QUERY-TRANSFER.md`](../joint-query/evidence/JOINT-QUERY-TRANSFER.md): + +```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), |U| = 96. +``` + +Write `R_s = R D_s`, `B_s = R_s iota_U`, and +`ell_(s,A) = R_A pi_A D_s`. The selected section `P_(s,A)` satisfies +`ell_(s,A) P_(s,A) = I` and is supported on A. Define the analogous T +section and query. All selected sections are dyadic units between the +eight selected coordinate fields and the eight query coordinate fields. +Stage zero has `D_0 = I`. + +Let `G` be the finite cover group, or a finite subgroup containing all +routes used below, with its regular right action. Put `N=|G|` and work +over `Q`. For a cover route `g`, write + +```text +(Q_g f)(d) = f(d g), Q_g Q_h = Q_(g h), +Q_g* = Q_(g^-1), tr(Q_g) = N if g=1, else 0. +``` + +The last equality requires this regular action. Distinct abstract route +labels in a nonfaithful quotient representation would not suffice. +The actual routes are finite binary invertible matrices; the subgroup +they generate is finite. A larger cover splits into orbits `dH` of +the subgroup H's right action, so the calculation applies per orbit. + +For `p in U`, let `r_p` be column p of R and `g_(s,p)` the actual +stage-s route. On logical fields constant in every payload coordinate, + +```text +B_s = [ r_p Q_(g_(s,p)) ]_(p in U). +``` + +This restriction keeps arbitrary independent cover values. It does +not identify cover owners. The full cover action is +`f(d,z_1,...,z_lambda) -> f(d g,z_1+d delta,...,z_lambda+d delta)`; +payload translations act trivially on these constant logical fields. +Thus they form an invariant subspace of the routed logical maps at +every positive tensor size. The proof uses the inherited invertible +endpoint-frame conventions, including their phases, as bound by +[`BRIDGE-REVIEW.md`](../joint-query/evidence/BRIDGE-REVIEW.md), sections +1--4. Converting the logical initial state to physical input coordinates +is an invertible frame change, as is converting each output endpoint. +Zero observations remain zero, and a nonzero required selected value +remains nonzero. No new assertion that a native frame fixes the constant +function is needed for the rank argument. + +The finite, source-bound checking obligations are precisely: + +1. `r_p^T r_p=4` for every `p in U`, and + `sum_(p in U) r_p r_p^T = 48 I_8`. +2. For each separate pair `(s,t)=(0,1),(0,2),(1,2)`, the 96 labels + `g_(s,p) g_(t,p)^-1`, as p ranges over U, are distinct. + +Labels need only be distinct within each pair, not across the union +of all three lists. The companion exact route check discharges these +finite obligations using the actual source columns and route matrices. +The proof below does not enumerate G, compute its size, or expand a +full regular-representation matrix. + +## Three-query rank bound + +Each query is a scaled coisometry: + +```text +B_s B_s* = sum_p r_p r_p^T tensor I_G = 48 I_(8N). +``` + +For `s != t` set `C_st=B_s B_t*`. If +`a_p=g_(s,p) g_(t,p)^-1`, then + +```text +C_st = sum_p r_p r_p^T tensor Q_(a_p). +``` + +In `C_st C_st*`, a term has identity route exactly when `a_p=a_q`. +Pairwise route injectivity forces `p=q`. Its identity coefficient is + +```text +sum_p (r_p r_p^T)^2 + = sum_p (r_p^T r_p) r_p r_p^T + = 4 sum_p r_p r_p^T + = 192 I_8. +``` + +Nonidentity routes have zero regular trace. Consequently + +```text +tr(C_st C_st*) = 1536 N, s != t, +tr((B_s B_s*)^2) = 18432 N. +``` + +Stack the three maps as `S=[B0; B1; B2]`, and put `K=S* S`. Then + +```text +tr(K) = 3 (8)(48) N = 1152 N, +tr(K^2) = 3 (18432) N + 6 (1536) N = 64512 N. +``` + +The real symmetric matrix K is positive semidefinite. Cauchy--Schwarz +on its nonzero eigenvalues gives + +```text +rank(S) = rank(K) >= tr(K)^2 / tr(K^2) = (144/7) N. +``` + +All entries are rational, so rational and real matrix ranks agree. +Let `Q=[B1; B2]` and `V=ker Q`. Projection from the image of S onto +the image of Q is surjective; its kernel is +`{(B0 h,0,0): h in V}`. Thus + +```text +rank(B0 restricted to V) = rank(S) - rank(Q) + >= (144/7) N - 16 N + = (32/7) N. +``` + +In particular, + +```text +dim_Q B0(ker B1 intersect ker B2) >= ceil(32 N / 7) > 0. (1) +``` + +No assertion that `rank(Q)=16N` is needed. + +## Rational, integer, and dyadic inputs + +Equation (1) supplies an h with + +```text +B1 h = B2 h = 0, B0 h != 0. (2) +``` + +This can be chosen rational: a rational nullspace basis for Q spans +its real kernel, and B0 cannot annihilate every vector in that basis. +Clearing the finitely many denominators gives an integer h satisfying +(2). All selected sections are dyadic, so the initial logical data +below are dyadic. Multiplying h by a further common power of two also +makes those finitely many initial selected values integer. Conversely, +division of the complete input by a sufficiently large power of two +fits any prescribed positive magnitude bound without losing (2). + +For each fixed tensor size, the inherited frames and their inverses +are finite products of native lines and translations with +Gaussian-dyadic coefficients. The physical pullback is therefore an +admitted exact complex dyadic input. The rational and integer +statements above concern logical coordinates; the obstruction does +not require a general frame to preserve real-valued physical arrays. + +This is an exact existence proof on each finite regular cover. It does +not exhibit a compactly supported formula for h independent of N, +bound the denominator or bit length needed for a chosen magnitude +bound, or provide a recursive precision implementation. + +## Ordered trajectory through the fixed first two calls + +Set all other pairs, helpers, and private fields initially to zero. +In pair 0 take + +```text +X_U = h, Y_U = 0, +X_A = -P_(0,A) B0 h, Y_A = P_(0,A) B0 h, +X_T = 0, Y_T = 0. (3) +``` + +Zero helper values are permitted under an arbitrary-input contract; +failure on this subspace already precludes universal restoration. +The two selected pair sums vanish. Also `X_A != 0`, because +`ell_(0,A) P_(0,A)=I` and `B0 h != 0`. The added pre-F0 observation is +exactly + +```text +q_extra = B2 X_U = B2 h = 0. (4) +``` + +The forward map at chart 0 is + +```text +f0 = B0 X_U + ell_(0,A) X_A + ell_(0,T) X_T, +X'_U = X_U - K_(0,U) f0, +X'_A = P_(0,A) ell_(0,T) X_T, +X'_T = P_(0,T) f0, +Y'_U = Y_U + X'_U, +Y'_S = X_S + Y_S - X'_S, S=A union T. +``` + +Substitution of (3) gives `f0=B0 h-B0 h=0`, so after F0, + +```text +X_U=Y_U=h, X_A=Y_A=X_T=Y_T=0. (5) +``` + +For the backward call B1 with future chart 2, define + +```text +E2 = I + P_(2,A)(R2-ell_(2,A)), +u = E2 Y, a1=ell_(1,T) X, b1=R1 u. +``` + +On (5), the full future query `R2 Y` equals `B2 h=0` and the +selected A baseline is zero. Therefore `u=Y`, `a1=0`, and +`b1=B1 h=0`. The conserved backward formulas are + +```text +Y'_A=u_A, +Y'_U=Y_U+K_(1,U) a1, +Y'_T=u_T-P_(1,T)(b1+11a1), +X'_U=X_U-Y_U, +X'_A=X_A+Y_A-u_A, +X'_T=P_(1,T)(b1+12a1). +``` + +They leave exactly + +```text +Y_(0,U)=h; all other ordinary and selected fields are zero. (6) +``` + +Every cancellation uses the displayed order of operators. No two +chart routes, selected sections, or query operators are commuted. + +## Retained observations and restoration obstruction + +State (6) is exactly the post-B1 state used by the predecessor +[`selected-output witness`](../joint-query/evidence/QQ16-SELECTED-WITNESS.md) +and its +[`rational observation review`](../joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md). +We retain that ordinary bank schedule and its source-bound tail +statement. The positive `(0,1)` bridge places `-h` in `Y_(1,U)`. +F2 has zero X source and makes no change. The negative bridge removes +that `-h` before B3. Later active ordinary pairs have zero inputs. +The last three ordinary bridges leave only `Y_(0,U)=h`, and the +terminal moves it to named `X_(0,U)` with the former-Y native type. +Every completed-X descendant is zero. The predecessor's independent +tail receipt also includes the control that omitting the first +negative bridge fails at B3. + +The first two calls remain exactly the fixed F0/B1 pair derived above; +the observation grant does not insert a changed controller between +them. All selected fields are already zero after F0 and remain zero +after B1. Subsequent homogeneous selected-only linear operations +therefore keep them zero, including cross-bank, port, cover and +selected-terminal maps. They must not read ordinary data. All five +forward query histories +`f0,f2,f4,f6,f8` are zero. Equation (4) adds another zero observation. +Thus the entire allowed record + +```text +all selected output endpoints from F0 onward, +all completed-X descendants at the retained output endpoint, +all five forward-query histories, +the complete pre-F0 value B2 X_U +``` + +is identical for (3) and the zero input, while the required original +selected value `X_(0,A)=-P_(0,A) B0h` differs. No decoder determined +only by that record can restore all original selected inputs. This +indistinguishability argument is stronger than a restriction to +rational-linear decoder coefficients. The record does not include +an intermediate ordinary read of `X_U=h` immediately after F0. +Granting the selected F0 output as an additional read-only observation +does not authorize changing the fixed first pair. + +More quantitatively, varying h over V gives an invisible family whose +original selected A values have dimension `rank(B0|V)`. By (1) that +dimension is at least `ceil(32N/7)`. Any additional *linear* observation +map that restores every such selected value must have at least this +rank on that family: its kernel there must be contained in the kernel +of the required selected-value map. This remains a statement about +information dimension, with no conversion to native or recursive cost. + +As a positive distinction, a retained initial observation `B0 X_U` +detects every member of this family with nonzero selected defect, +because the required A value is exactly `-P_(0,A) B0 X_U`. +This does not prove that adding B0 repairs other inputs or closes the +whole controller. + +## Covered domain and remaining obligations + +The theorem covers these exact F0/B1 maps, the retained ordinary tail, +restoration on arbitrary rational or dyadic logical inputs, regular +cover action, every positive payload tensor size, and the specified +side-effect-free ordinary query `B2 X_U`. The chosen witness is dyadic +and has an admitted complex dyadic physical pullback. The same finite +source obligations imply the dimension theorem for every finite +regular cover containing the distinct route labels. + +The full original query `R2 X` is a different observation: on (3) it +equals `-ell_(2,A) P_(0,A) B0 h` and need not vanish. Neither the old +selected witness nor this note silently substitutes it for `B2 X_U`. +Changes to the first local pair, ordinary-to-selected access, source +mutations, extra observations, or a different ordinary schedule require +a new analysis. Restoring only the conserved selected pair sums is also +a weaker task than restoring the arbitrary original selected inputs. + +The new rank and first-two-call arguments are written all-parameter +linear-algebra proofs. Actual column and route premises are finite exact +checks. The later bank schedule is an explicitly inherited, +source-bound predecessor obligation, not a newly derived general +scheduling theorem. No formal-kernel proof is claimed. Native address +access, precision bounds, paid recursive costs, complete supplier +admission, and a multiplication-exponent improvement remain outside +this result. + +The QQ16 maps, cover semantics, old witness, and retained schedule are +credited to the contributors recorded in `research/joint-query/NOTICE.md`. +Cinna Davis proposed the additional ordinary query being tested here. +This residual proof and its checking used substantial OpenAI Codex +assistance. New material is Apache-2.0. diff --git a/research/qq16-extra-query-residual/README.md b/research/qq16-extra-query-residual/README.md new file mode 100644 index 0000000000..891a305995 --- /dev/null +++ b/research/qq16-extra-query-residual/README.md @@ -0,0 +1,154 @@ +# QQ16 residual A-input dimension after one extra query + +**Scoped obstruction; no new supplier or kappa.** Even granting the complete +read-only pre-F0 value `B2 X_U` free of charge, the fixed QQ16 F0/B1 controller +cannot restore every original selected input from its retained observations. +There are at least `ceil(32 |G| / 7)` independent missing A-input directions +on the finite regular cover G: at least four sevenths of its `8|G|`-dimensional +A-input space. This is information dimension, not a paid recursive rank or a +physical cost estimate. + +The contribution is a **quantitative dimension bound and independent trace +method**. The final overlap refresh found Adam Gall's concurrent +[PR2093](https://github.com/CrocSwap/integer-mult-bounds/pull/2093), exact head +`8b21a900eb520e4f11ea177b310f66316f8e8983`, which already proves the qualitative +obstruction using an explicit three-port witness invisible to *all* nonzero +charts. We credit that result rather than claim priority for insufficiency. +Our bound measures the size of the missing A space for the B2-only repair; +it does not establish that bound for observing all eight nonzero-chart queries. + +Both results address the arbitrary-input question left open by Cinna Davis's +[PR2079](https://github.com/CrocSwap/integer-mult-bounds/pull/2079). That +contribution correctly separates the eight previously exhibited directions. +The residual family lies in both `ker B1` and `ker B2`, with nonzero `B0 h`. + +## Argument and exact scope + +The [written proof](PROOF.md) uses the actual U96 query columns and the stage +0, 1 and 2 cover routes. For each of the three stage pairs, all 96 relative +routes are distinct. With `S=[B0;B1;B2]` and `K=S* S`, the exact regular traces +are + +```text +tr K = 1152 |G|, +tr K^2 = 64512 |G|, +rank S >= (tr K)^2 / tr K^2 = (144/7) |G|. +``` + +Since `[B1;B2]` has at most `16|G|` output coordinates, +`dim B0(ker B1 intersect ker B2) >= ceil(32|G|/7)`. +Choose a rational, then denominator-cleared integer, h in this joint kernel +with `B0 h != 0`. Initialize only pair 0 as + +```text +X_U=h, Y_U=0, +X_A=-P_(0,A) B0 h, Y_A=-X_A, +X_T=Y_T=0. +``` + +The unchanged F0/B1 pair leaves only `Y_(0,U)=h`. The inherited ordinary tail +has zero selected outputs, zero completed-X descendants and all five F-query +histories zero. The added observation `B2 X_U` is also zero, although the +original A input is nonzero. Thus no decoder determined only by these records +can restore all original selected inputs. + +The result retains the local pair, ordinary tail, regular cover action and +native endpoint interpretation. It permits homogeneous selected-only controls +after B1. It grants the complete extra observation with no source mutation and +free indefinite retention. Logical payload-constant inputs retain arbitrary +cover values and apply at every positive tensor size under the inherited +invertible endpoint frames. Fixed finite-precision implementation is not proved. + +The full initial `R2 X` is a different observation; it need not vanish here. +Changing a first-pair map, adding another ordinary read, or changing the tail +requires a new argument. An initial `B0 X_U` observation detects the constructed +missing A values, but is not proved to repair the whole controller. + +## Evidence and reproduction + +Run from a Git checkout with the pinned source history and Python 3.12: + +```sh +python3.12 -I -B scripts/research_package.py --package research/qq16-extra-query-residual +``` + +Expected: `PASS_QQ16_EXTRA_QUERY_RESIDUAL`, six passing behavioral groups, and +`PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=negative-result`. No network or +third-party Python packages are needed. Direct verification is +`python3.12 -I -O -B research/qq16-extra-query-residual/verify.py`. + +- The primary checker reads the frozen R certificate and reconstructs binary + routes by transvections. It computes collision-aware matrix coefficients, + the exact trace bound and the inherited tail's formal h trajectory. +- The code-disjoint oracle reconstructs R by backward covectors through all + 712 independent source/helper positions, then projects the source columns. + It constructs routes by orthonormal axis swaps. The full R and U96 route + hashes, all three coefficient matrices and both trace moments agree. +- Fixed [RESULT.json](RESULT.json) and [ORACLE.json](ORACLE.json) are consumed, + not regenerated during acceptance. A complete C3xC3 regular example supplies + an explicit residual witness and exact matrix ranks 25 and 17. This small + example illustrates the argument; it does not replace the actual source check. +- Controls detect changed coefficients, route collisions, reversed noncommuting + route products, an omitted cancelling bridge, source drift, typed and + trace-preserving receipt corruption, missing receipts and overwritten + generation outputs. Actual removal of the oracle's distinctness and Gram + guards makes its control suite fail. Port permutation and whole-column signs + are accepted; normal and optimized relocated checks preserve the receipts. +- [REVIEW.json](REVIEW.json) records an independent agent's mathematical review + and hashes of the proof, both checkers, source manifest and primary receipt. + +This is a written all-parameter rank/existence argument with finite exact +source checks. It does not enumerate the cover, construct an explicit basis +for the dimension bound, reprove the inherited native tail, replay the complete supplier, +or establish precision, physical costs, supplier admission or a formal-kernel +multiplication theorem. The zero-cost favorable relaxation already fails the +restoration obligation, so no moment screen or native implementation is claimed. + +## Provenance and overlap + +Scientific base `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +Selected-record SHA256 is +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +Exact Git and SHA256 pins are in [SOURCES.json](SOURCES.json). Original immutable +archive bytes are used directly; no source archive is copied or modified. +[TASK.json](TASK.json) records selection, scope refinement and overlap. + +The selector's recursive-interface allocation was refined to revision 4's +central `joint-query-controller` handoff. Work continues in +[Discussion2074](https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18932289). +Adam Gall's adjacent [PR2086](https://github.com/CrocSwap/integer-mult-bounds/pull/2086) +changes the first A logger without retaining an extra observation; it does not +require the simultaneous `B1 h=B2 h=0` used here. Neither result is a universal +barrier to changed QQ16 interfaces. + +## Open next questions + +1. Does one properly priced **full** initial `R2 X` read or an additional + `B0 X_U` read remove all missing selected information? It would change the + observation contract tested here. First compute the joint kernel of the + entire retained record, checking both A and T restoration, before native + synthesis. The full-controller kernel and legal final frame access remain + unresolved; detecting this family alone is insufficient. +2. Can a changed T record, ordinary response or backward first call avoid + losing these initial values without another transcript? First apply the + erased-state test and a favorable complete cost bound to one precise map. + Global ordinary scheduling, endpoint access, hosting and precision remain + blockers. Repeating the same fixed-pair B2-only observation is unnecessary. + +## Credit + +Prepared for Ross Richardson with substantial OpenAI Codex assistance, including +the `math-recursive-interfaces` proof specialist and code-disjoint +`math-exact-circuit-verification` oracle/reviewer. No independent human review +is claimed. New material is Apache-2.0. + +Ali Romman's [PR1969](https://github.com/CrocSwap/integer-mult-bounds/pull/1969) +and its credited centre-encoding contributors supply the QQ16 maps, native +contracts, original observation witness and retained tail. Cinna Davis's PR2079 +poses the extra observation and establishes its eight-direction separation. +Adam Gall's PR2086 supplies adjacent first-forward logger analysis, and his +concurrent PR2093 supplies the explicit all-nonzero-chart witness for the +same qualitative obstruction. PR2093's pinned proof was inspected; its +executable was not imported or rerun by this package. The +[upstream notices](../joint-query/NOTICE.md) retain all geometry, gauge44/t16, +compiler and selected-supplier attribution and source licenses. diff --git a/research/qq16-extra-query-residual/RESULT.json b/research/qq16-extra-query-residual/RESULT.json new file mode 100644 index 0000000000..ec7a9d603f --- /dev/null +++ b/research/qq16-extra-query-residual/RESULT.json @@ -0,0 +1,785 @@ +{ + "finite_fixture": { + "B0_h": [ + 9, + -9, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "B1_h": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "B2_h": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "F0_query": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "after_B1_only_YU": true, + "cover_size": 9, + "exact_missing_dimension": 8, + "explicit_h": [ + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "group": "C3xC3", + "initial_A": [ + -9, + 9, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_shape": [ + 27, + 81 + ], + "rank_bound": "243/11", + "square_trace": 2673, + "stacked_rank": 25, + "trace": 243, + "two_query_rank": 17 + }, + "negative_controls": [ + "changed_column", + "collapsed_route", + "omitted_cancelling_bridge" + ], + "route_audit": { + "R_dense_sha256": "4766159d79608cc4e943b59d971f37763835ceb07f39e5a8319f5ebc4fcad91f", + "missing_A_dimension_lower_per_cover_owner": "32/7", + "ordinary_column_norms": { + "4": 96 + }, + "ordinary_gram": [ + [ + 48, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 48, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 48, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 48, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 48, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 48, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 48, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 48 + ] + ], + "pairs": { + "0,1": { + "distinct_routes": 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 + ] + ], + "normalized_trace": 1536 + }, + "0,2": { + "distinct_routes": 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 + ] + ], + "normalized_trace": 1536 + }, + "1,2": { + "distinct_routes": 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 + ] + ], + "normalized_trace": 1536 + } + }, + "routes_U96_stage_major_sha256": "f55db68178127a8ba23820eba933e1417b3db3d8eaa2bce2a343d14907a48c2b", + "square_trace_per_cover_owner": 64512, + "stacked_rank_lower_per_cover_owner": "144/7", + "trace_per_cover_owner": 1152 + }, + "schema": 1, + "scope": "Fixed F0/B1 and retained observations plus side-effect-free B2 X_U; written rank/existence theorem and finite source checks; no native tariff, full controller or new kappa.", + "source_sha256": { + "research/community-frontier1042-audit/selected-replay.tar.gz": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "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-COVER-ACTION-ADDENDUM.md": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb", + "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_EXTRA_QUERY_RESIDUAL", + "tail": [ + { + "kind": "bridge", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + -1, + 0, + 0 + ] + }, + { + "kind": "local", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + -1, + 0, + 0 + ] + }, + { + "kind": "bridge", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "local", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "bridge", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "local", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "bridge", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "local", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "bridge", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "local", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "bridge", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "local", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "local", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "bridge", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "bridge", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "bridge", + "x": [ + 0, + 0, + 0, + 0 + ], + "y": [ + 1, + 0, + 0, + 0 + ] + }, + { + "kind": "terminal", + "x": [ + 1, + 0, + 0, + 0 + ], + "y": [ + 0, + 0, + 0, + 0 + ] + } + ] +} diff --git a/research/qq16-extra-query-residual/REVIEW.json b/research/qq16-extra-query-residual/REVIEW.json new file mode 100644 index 0000000000..136afc365e --- /dev/null +++ b/research/qq16-extra-query-residual/REVIEW.json @@ -0,0 +1,48 @@ +{ + "checks": [ + { + "command": "python3 -I -B research/qq16-extra-query-residual/verify.py", + "exit_code": 0, + "stdout": "PASS_QQ16_EXTRA_QUERY_RESIDUAL rank_stack>=144|G|/7 missing_A>=ceil(32|G|/7) no_new_kappa" + }, + { + "command": "python3 -I -O -B research/qq16-extra-query-residual/verify.py", + "exit_code": 0, + "stdout": "PASS_QQ16_EXTRA_QUERY_RESIDUAL rank_stack>=144|G|/7 missing_A>=ceil(32|G|/7) no_new_kappa" + }, + { + "command": "python3 -I -O -B research/qq16-extra-query-residual/independent.py", + "exit_code": 0, + "status": "PASS_INDEPENDENT_QQ16_THREE_QUERY_TRACE" + } + ], + "defects_requiring_repair": [], + "primary_independent_exact_agreement": { + "R_dense_sha256": "4766159d79608cc4e943b59d971f37763835ceb07f39e5a8319f5ebc4fcad91f", + "all_three_identity_coefficient_matrices_equal": true, + "routes_U96_stage_major_sha256": "f55db68178127a8ba23820eba933e1417b3db3d8eaa2bce2a343d14907a48c2b" + }, + "remaining_obligations": [ + "Inherited QQ16 native/endpoint and tail source premises are consumed, not fully re-proved.", + "No full-cover enumeration, compact witness formula independent of cover size, recursive precision, physical routing tariff, complete supplier or kappa claim." + ], + "review_conclusions": { + "extra_observation": "The complete read-only pre-F0 B2 XU is zero. The full query R2 X is different and is explicitly excluded; the fixed first two calls are not changed by the observation grant.", + "finite_fixture": "C3xC3 fixture is correctly labelled illustrative. Its complete ranks 25 and 17 and witness do not replace actual QQ16 source/route checks.", + "observation_scope": "All selected endpoints from F0 onward, completed-X descendants at the retained output endpoint, five forward histories and pre-F0 B2 XU coincide with zero input; original XA differs. Indistinguishability excludes any decoder determined only by this record. Later controller operations are homogeneous selected-only with no ordinary read.", + "ordered_F0_B1": "Correct source-matching formulas. With XU=h, YU=0, XA=-P0A B0h, YA=P0A B0h, XT=YT=0 and B1h=B2h=0, F0 yields XU=YU=h and all selected zero; B1 yields only Y0U=h. No operators commute in these substitutions.", + "rational_existence": "Correct over finite regular covers. Rational matrices give a rational witness; clearing denominators gives integer logical h, and dyadic selected sections admit dyadic logical inputs. No constructive uniform precision bound follows.", + "regular_representation": "Correct requirement: distinct actual matrix routes act in a finite regular right cover, so only identity has nonzero trace. Payload-constant logical fields retain arbitrary cover values; inherited invertible Gaussian-dyadic endpoint frames preserve the zero/nonzero observation distinction.", + "retained_tail": "The pinned trajectory_after_B1 is replayed exactly on its one formal h coefficient, including all stages 2 through 8 and terminal. The omitted first cancelling bridge fails at B3. Native tail interpretation and completed-X versus old-Y endpoint typing remain explicitly inherited from the pinned predecessor proof, not newly verified native semantics.", + "trace_rank": "Correct: tr K=1152N, tr K^2=64512N; rank S>=144N/7 and rank B0|ker(B1,B2)>=32N/7 by exact image projection identity, without assuming rank[B1;B2]=16N." + }, + "review_scope": "Written all-parameter proof plus independent finite source audit and actual primary receipt replay; not a formal-kernel proof.", + "reviewed_file_sha256": { + "PROOF.md": "9c2ad4600d65dd3354db4bae5ac78d13fedf2da6e500224fafaeed596846c887", + "RESULT.json": "f70f11e360d75f43fdd9ed6f9968b00c7955ce9e2dbd67066c84a8ec41e6e3bd", + "SOURCES.json": "f6b4d07ad33578999bbe858b34f0200eeae7f56aeddc8d217b0897808a14c969", + "independent.py": "41331f2a7fbd3752beb1d6e8b57f0f555dffccb523e953198eaf8f4790031b17", + "verify.py": "68e3c1c8c044a9b7ae245b189ef2154b6cfe6c96faca87349cd336ebf731fd2e" + }, + "status": "PASS_INDEPENDENT_QQ16_RESIDUAL_MATHEMATICAL_REVIEW" +} diff --git a/research/qq16-extra-query-residual/SOURCES.json b/research/qq16-extra-query-residual/SOURCES.json new file mode 100644 index 0000000000..4373b30160 --- /dev/null +++ b/research/qq16-extra-query-residual/SOURCES.json @@ -0,0 +1,100 @@ +{ + "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/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-COVER-ACTION-ADDENDUM.md", + "usage": "input", + "git_blob": "3dd1a990d7b9d57cfb20cf8e8dd45548f043a944", + "sha256": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb" + }, + { + "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, + "author": "Ali Romman", + "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "role": "original QQ16 local maps, cover action and observation witness" + }, + { + "pr": 2079, + "author": "Cinna Davis", + "head": "49df8190b158e3028e702b2c6b798117006f7249", + "path": "research/joint-query-extra-b2-observation-seed3e62/README.md", + "sha256": "22044da27cc22b6387aa72b53cefd2f9f1e73c3147308533ef9d4445fc01f03f", + "role": "proposed side-effect-free added B2 X_U observation; public contextual source, no executable dependency" + }, + { + "pr": 2086, + "author": "Adam Gall", + "head": "68dcf180ce3918a9ee1998bfc5455f42516c6009", + "role": "adjacent changed-A-logger obstruction without added observations; distinct premise, no executable dependency" + } + ] +} diff --git a/research/qq16-extra-query-residual/TASK.json b/research/qq16-extra-query-residual/TASK.json new file mode 100644 index 0000000000..0b9e546b60 --- /dev/null +++ b/research/qq16-extra-query-residual/TASK.json @@ -0,0 +1,135 @@ +{ + "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": "For fixed QQ16 F0/B1 and retained ordinary tail, prove or falsify restoration from original selected endpoints/completed-X descendants/five F histories plus complete read-only pre-F0 B2 X_U. Exact actual stage0/1/2 route trace bound and joint-kernel residual dimension.", + "scope_change_reason": "Take revision-4 central handoff PR2079 after recursive-interfaces allocation; test arbitrary-input sufficiency of its one paid observation, granting it free, rather than repeat old connector exclusions.", + "bottleneck_link": "Resolves whether a specific proposed ordinary query repairs the missing controller interface. A zero-cost information relaxation fails, so full native synthesis of this unchanged B2-only repair is unwarranted.", + "budget_minutes": 60, + "stop_rule": "Stop if actual three-query trace bound does not exceed16|G| or source routes fail; no larger search. Budget about60 minutes with final quarter reserved for verification and handoff.", + "outcome": "negative-result", + "evidence": "PROOF.md written trace/rank/existence theorem; RESULT.json exact source/route/tail and finite C3xC3 checks; ORACLE.json code-disjoint reverse-covector and coordinate-swap audit; REVIEW.json independent agent review. Six behavioral groups including removed guards. No new kappa.", + "author": "Ross Richardson", + "ai_assistance": "Substantial OpenAI Codex assistance in task selection, rank derivation, coding, verification, writing and publication. math-recursive-interfaces proof specialist and math-exact-circuit-verification code-disjoint oracle/reviewer; no independent human review.", + "open_questions": [ + { + "question": "Does a full initial R2X read or an additional B0X_U observation restore all arbitrary selected inputs?", + "why_it_matters": "B2X_U alone fails despite exposing the predecessor eight-direction family.", + "first_step": "Compute the complete observation kernel and both A/T restoration obligations before native synthesis.", + "blocked_by": "No complete corrected controller; legal native access, retention, precision and complete paid bill remain missing." + }, + { + "question": "Can one changed T record, ordinary response or B1 map avoid the erased selected state?", + "why_it_matters": "The fixed pair loses initial data even with this free extra record.", + "first_step": "Specify one changed ordered first-pair map and test its kernel before a fully charged favorable budget.", + "blocked_by": "Changed-map inverse and global scheduling, endpoint, hosting and precision obligations." + } + ], + "selection_nonce": "4ded8151ee3f650a1a7da9212a67da24", + "selection_track": "recursive-interfaces", + "selection_override": "Revision4 explicitly prioritizes a live central handoff within the drawn track; second open question of PR2079, complementary to PR2086.", + "scope_key": "qq16-fixed-f0-b1-free-pre-f0-b2xu-three-query-residual", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18932289", + "entry_overlap": { + "open_prs": 359, + "discussions": 740, + "complete_pagination": true, + "fetched_between_utc": [ + "2026-10-14T19:07:15Z", + "2026-10-14T19:09:32Z" + ], + "direct_open_prs_followup": 362, + "nearest": [ + { + "pr": 1969, + "role": "original maps and witness" + }, + { + "pr": 2079, + "head": "49df8190b158e3028e702b2c6b798117006f7249", + "role": "exact extra query being audited" + }, + { + "pr": 2086, + "head": "68dcf180ce3918a9ee1998bfc5455f42516c6009", + "role": "different changed-A-logger premise, no added record" + } + ], + "limitations": "Text/local-metadata search is not code-diff exhaustion or a novelty certificate. Default cache write failed; successful refresh used this run writable scratch cache." + }, + "final_overlap": { + "searched_at": "2026-10-14T19:22:02.797930+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T19:19:42.224310+00:00", + "complete_pagination": true, + "records": 369 + }, + "discussions": { + "fetched_at": "2026-10-14T19:22:02.738211+00:00", + "complete_pagination": true, + "records": 753 + } + }, + "warnings": [], + "matches_total": 10, + "decision": "Continue completed proof as independent quantitative corroboration. Concurrent PR2093 establishes the qualitative obstruction with an explicit all-nonzero-chart witness; this package adds ceil(32|G|/7) residual A-image dimension for B2-only observation, using a different trace method. No novelty guarantee." + }, + "concurrent_result": { + "pr": 2093, + "author": "Adam Gall", + "head": "8b21a900eb520e4f11ea177b310f66316f8e8983", + "readme_sha256": "a4a7eb47ba7f619836c5a7ca7e20e8c05686a16f1fffc0370c6c189f4153b5dc", + "status": "Pinned public proof inspected; executable not rerun; not a runtime dependency." + }, + "submission_checkpoint": { + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "utc": "2026-10-14T19:19:42Z", + "relevant_source_changes": false + } +} diff --git a/research/qq16-extra-query-residual/VERIFY.json b/research/qq16-extra-query-residual/VERIFY.json new file mode 100644 index 0000000000..24dbb3b720 --- /dev/null +++ b/research/qq16-extra-query-residual/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "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-COVER-ACTION-ADDENDUM.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": "Actual finite route and Gram premises, fixed exact receipt, trace rank bound and inherited restricted tail." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 180, + "checks": "Independent source derivation/receipt agreement, semantic and typed corruption, source drift, missing/no-overwrite evidence, actual removed guards, normal/optimized package relocation." + } + ] +} diff --git a/research/qq16-extra-query-residual/independent.py b/research/qq16-extra-query-residual/independent.py new file mode 100644 index 0000000000..1df8c91bf4 --- /dev/null +++ b/research/qq16-extra-query-residual/independent.py @@ -0,0 +1,424 @@ +#!/usr/bin/env python3 +"""Independent, source-derived QQ16 three-query trace audit. + +No research-package module is imported. The query rows are reconstructed by +reverse covector propagation; native routes are constructed by swapping two +orthonormal coordinate blocks. Output is deterministic exact JSON. The +finite audit does not enumerate the cover and is not a supplier admission. + +Apache-2.0. Substantial mathematical and implementation assistance: OpenAI +Codex. Original scalar programs and native charts retain their source credits. +""" + +import argparse +from collections import Counter +from fractions import Fraction +import gzip +import hashlib +import io +import json +from pathlib import Path +import subprocess +import tarfile + + +SOURCE_BASE = "bce54fb3f895cbe5cd4c0eb477c3afeed100190f" +ARCHIVE_PATH = "research/community-frontier1042-audit/selected-replay.tar.gz" +ARCHIVE_SHA = "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" +MEMBERS = { + "slots/local/CANONICAL-WORD.json.gz": ( + "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c"), + "slots/local/LOCAL-PROGRAMS.json.gz": ( + "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "9f41d53659e9be84e20c661560c5687abbf5cd0660cdecbe01ad5eb29e6b8ee3"), + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": ( + "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa"), +} +A = (0, 7, 20, 27, 36, 46, 57, 111) +T = (21, 37, 47, 76, 81, 87, 92, 110) +U = tuple(p for p in range(112) if p not in A + T) +DIMENSION = 73 +IDENTITY = tuple(1 << j for j in range(DIMENSION)) + + +class AuditError(ValueError): + pass + + +def require(ok, reason): + if not ok: + raise AuditError(reason) + + +def digest(raw): + return hashlib.sha256(raw).hexdigest() + + +def pinned(raw, expected, name): + require(digest(raw) == expected, "source digest: " + name) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def exact_json(value): + if isinstance(value, Fraction): + return value.numerator if value.denominator == 1 else str(value) + if isinstance(value, (list, tuple)): + return [exact_json(x) for x in value] + if isinstance(value, dict): + return {str(k): exact_json(v) for k, v in value.items()} + return value + + +def read_sources(repo): + raw = subprocess.check_output( + ["git", "show", SOURCE_BASE + ":" + ARCHIVE_PATH], cwd=repo) + pinned(raw, ARCHIVE_SHA, ARCHIVE_PATH) + decoded = {} + with tarfile.open(fileobj=io.BytesIO(raw), mode="r:gz") as archive: + for name, (compressed_sha, payload_sha) in MEMBERS.items(): + matches = [m for m in archive.getmembers() if m.name == name] + require(len(matches) == 1 and matches[0].isfile(), + "exactly one regular archive member: " + name) + member = archive.extractfile(matches[0]).read() + pinned(member, compressed_sha, name) + payload = gzip.decompress(member) if name.endswith(".gz") else member + pinned(payload, payload_sha, name + " payload") + decoded[name.rsplit("/", 1)[1]] = json.loads(payload) + return decoded + + +def register(token): + kind, at = token + require(kind in ("L", "C"), "declared register kind") + require(0 <= at < (704 if kind == "L" else 8), "declared register index") + return at + (704 if kind == "C" else 0) + + +def query_by_reverse_covectors(word, programs): + """Pull each centre output row back through the scalar prefix. + + For x_t <- x_t+c*x_s, a covector coefficient w_t contributes c*w_t + to w_s. All 712 input positions remain distinct until the final + projection onto the 112 source coordinates; no clean-input assumption + is used to discard dependencies during the propagation. + """ + require((word["v"], word["R"], word["h"]) == (112, 480, 9), + "source geometry") + program = programs["forward"] + cuts = [i for i, e in enumerate(program) if e == ["phase", "centers"]] + require(len(cuts) == 1, "unique centre boundary") + require(len(set(word["centers"])) == 8, "eight distinct centre outputs") + rows, nuisance = [], [] + for centre in word["centers"]: + covector = {centre: Fraction(1)} + for event in reversed(program[:cuts[0]]): + if event[0] != "scalar": + continue + op = event[1] + kind, target = op[0], register(op[1]) + require(kind in ("clear", "scale", "copy", "add"), + "known scalar operation") + weight = covector.get(target, Fraction(0)) + if not weight: + continue + if kind == "clear": + del covector[target] + elif kind == "scale": + covector[target] = weight * Fraction(op[2], op[3]) + else: + source = register(op[2]) + require(target != source, "distinct scalar operands") + if kind == "copy": + del covector[target] + amount = weight + else: + amount = weight * Fraction(op[3], op[4]) + total = covector.get(source, Fraction(0)) + amount + if total: + covector[source] = total + else: + covector.pop(source, None) + require(not any(112 <= p < 224 or p >= 704 for p in covector), + "centre source/helper decomposition") + rows.append([covector.get(p, Fraction(0)) for p in range(112)]) + nuisance.append({p: x for p, x in covector.items() if p >= 224}) + require(all(x.denominator == 1 for row in rows for x in row), + "integer source query") + return rows, nuisance, cuts[0] + + +def gf2_apply(columns, vector): + require(0 <= vector < 1 << len(columns), "binary vector domain") + result = 0 + for j, column in enumerate(columns): + if vector & (1 << j): + result ^= column + return result + + +def gf2_product(left, right): + """Columns of left*right: right acts first on a column vector.""" + require(len(left) == len(right) == DIMENSION, "route dimensions") + return tuple(gf2_apply(left, x) for x in right) + + +def gf2_transpose(columns): + return tuple(sum(((columns[j] >> i) & 1) << j for j in range(DIMENSION)) + for i in range(DIMENSION)) + + +def route_by_coordinate_swap(chart, stage): + """Fix q and swap b_1,...,b_8 with the stage's eight spare axes. + + This is an orthonormal-basis coordinate calculation, rather than the + native verifier's transvection construction. + """ + if stage == 0: + return IDENTITY + columns = [] + for x in IDENTITY: + y = x + for k, b in enumerate(chart[1:]): + spare = 1 << (9 + 8 * (stage - 1) + k) + if (x & b).bit_count() % 2: + y ^= b ^ spare + if x & spare: + y ^= spare ^ b + columns.append(y) + return tuple(columns) + + +def native_routes(word, phases): + require(phases["m"] == DIMENSION and len(phases["recipes"]) == 112, + "source native dimension and port count") + routes = [[], [], []] + for p, record in enumerate(phases["recipes"]): + require(record["port"] == p and record["q"] == word["ports"][p], + "source port binding") + chart = [record["q"]] + record["idle_children"][0]["orthogonal_axes"][:8] + require(len(chart) == 9 and all(0 < x < 512 for x in chart), + "nine local binary chart axes") + require(all((chart[i] & chart[j]).bit_count() % 2 == int(i == j) + for i in range(9) for j in range(9)), "orthonormal chart") + beta = sum((((b.bit_count() - 1) // 2) % 2) << k + for k, b in enumerate(chart[1:])) + beta_chart = 0 + for k, b in enumerate(chart[1:]): + if beta & (1 << k): + beta_chart ^= b + for stage in range(3): + g = route_by_coordinate_swap(chart, stage) + require(gf2_product(g, g) == IDENTITY, "route involution") + require(gf2_transpose(g) == g, "route orthogonality") + require(gf2_apply(g, chart[0]) == chart[0], "route fixes port normal") + if stage: + for k, b in enumerate(chart[1:]): + spare = 1 << (9 + 8 * (stage - 1) + k) + require(gf2_apply(g, b) == spare and gf2_apply(g, spare) == b, + "route swaps the actual chart and stage axes") + entry = chart[0] ^ beta_chart + exit_value = beta_chart ^ (beta << (9 + 8 * (stage - 1))) + else: + entry = exit_value = 0 + require(record["stage_alignment"][stage] == { + "entry_X": entry, "entry_Y": entry, + "exit_X": exit_value, "exit_Y": exit_value}, + "source stage-alignment binding") + routes[stage].append(g) + return routes + + +def zero(size=8): + return [[Fraction(0) for _ in range(size)] for _ in range(size)] + + +def transpose(matrix): + return list(map(list, zip(*matrix))) + + +def matmul(left, right): + rt = transpose(right) + return [[sum(a * b for a, b in zip(row, column)) for column in rt] + for row in left] + + +def trace(matrix): + return sum(matrix[i][i] for i in range(len(matrix))) + + +def gram(columns): + return [[sum(c[i] * c[j] for c in columns) for j in range(8)] + for i in range(8)] + + +def scalar_identity(value): + return [[Fraction(value * (i == j)) for j in range(8)] for i in range(8)] + + +def cross_identity_coefficient(columns, relative_routes): + """Compute [e] C C* with C=B_s B_t*, retaining every collision. + + Write C=sum_g K_g D_g, K_g=sum_{p:g_p=g} r_p r_p^T. + Since D_g D_h*=D_(g h^-1), [e] C C*=sum_g K_g K_g^T. + No port-index distinctness is assumed by this computation. + """ + require(len(columns) == len(relative_routes), "one route per column") + buckets = {} + multiplicity = Counter(relative_routes) + for column, g in zip(columns, relative_routes): + block = buckets.setdefault(g, zero()) + for i in range(8): + for j in range(8): + block[i][j] += column[i] * column[j] + coefficient = zero() + for block in buckets.values(): + square = matmul(block, transpose(block)) + for i in range(8): + for j in range(8): + coefficient[i][j] += square[i][j] + return coefficient, dict(sorted(Counter(multiplicity.values()).items())) + + +def require_distinct(relative_routes): + require(len(relative_routes) == len(set(relative_routes)) == 96, + "96 distinct relative routes") + + +def require_column_gram(columns): + require(gram(columns) == scalar_identity(48), "ordinary column Gram") + + +def expect_rejection(action, reason): + try: + action() + except AuditError as exc: + require(str(exc) == reason, "negative control rejected by wrong check") + return + raise AuditError("negative control unexpectedly accepted: " + reason) + + +def controls(columns, routes, relatives, source_payload): + # The first two actual U columns have inner product two, so their + # forced collision contributes a visible off-diagonal port term. + collision = relatives.copy() + collision[1] = collision[0] + expect_rejection(lambda: require_distinct(collision), "96 distinct relative routes") + collided, histogram = cross_identity_coefficient(columns, collision) + require(trace(collided) == 1544, "collision-aware cross-term control") + require(histogram == {1: 94, 2: 1}, "collision histogram control") + bad_columns = [c.copy() for c in columns] + bad_columns[0][0] += 1 + expect_rejection(lambda: require_column_gram(bad_columns), "ordinary column Gram") + # The algebra must admit a harmless port reordering and independent + # signs of whole source columns. + transformed = [[-x for x in c] for c in reversed(columns)] + transformed_relatives = list(reversed(relatives)) + require(cross_identity_coefficient(transformed, transformed_relatives)[0] + == scalar_identity(192), "reordering/sign positive control") + require_column_gram(transformed) + expected_sha = digest(source_payload) + expect_rejection(lambda: pinned(source_payload + b" ", expected_sha, "control"), + "source digest: control") + # Orientation cannot be checked by the trace alone: the actual stage + # routes do not commute, even though reversing every relative route + # leaves the Gram trace unchanged. Check their ordered action itself. + g, h = routes[1][U[0]], routes[2][U[0]] + gh, hg = gf2_product(g, h), gf2_product(h, g) + witness = next(j for j in range(DIMENSION) if gh[j] != hg[j]) + x = 1 << witness + require(gh[witness] == gf2_apply(g, gf2_apply(h, x)), "ordered route product") + expect_rejection(lambda: require(hg[witness] == gf2_apply(g, gf2_apply(h, x)), + "ordered route product"), + "ordered route product") + return { + "route_collision": {"distinct_routes": 95, "identity_coefficient_trace": 1544, + "named_distinctness_check": "REJECT"}, + "coefficient_change": "REJECT: ordinary column Gram", + "port_reordering_and_whole_column_signs": "PASS", + "source_payload_mutation": "REJECT: source digest", + "reversed_noncommuting_route_product": { + "status": "REJECT: ordered route product", "port": U[0], + "basis_axis": witness, "correct_image": gh[witness], "reversed_image": hg[witness]}, + } + + +def audit(repo): + source = read_sources(repo) + word = source["CANONICAL-WORD.json.gz"] + rows, nuisance, cut = query_by_reverse_covectors(word, source["LOCAL-PROGRAMS.json.gz"]) + routes = native_routes(word, source["DATA-PHASES.json"]) + columns = [[row[p] for row in rows] for p in U] + require(all(sum(x*x for x in c) == 4 for c in columns), "96 column norms") + require_column_gram(columns) + same = gram(columns) + results, relatives = {}, {} + for s, t in ((0, 1), (0, 2), (1, 2)): + # B_s B_t*: rho_s followed in the right regular action by rho_t^-1. + relative = [gf2_product(routes[s][p], gf2_transpose(routes[t][p])) for p in U] + coefficient, multiplicities = cross_identity_coefficient(columns, relative) + require_distinct(relative) + require(coefficient == scalar_identity(192), "cross identity coefficient") + key = str(s) + "," + str(t) + relatives[key] = relative + results[key] = { + "operator": "B_s B_t* B_t B_s*", "relative_route_order": "rho_s(p) rho_t(p)^-1", + "distinct_relative_routes": len(set(relative)), + "route_multiplicity_histogram": multiplicities, + "relative_route_columns_sha256": digest(canonical(relative)), + "identity_coefficient": coefficient, "identity_coefficient_trace": trace(coefficient), + } + tr = 3 * trace(same) + tr_square = 3 * trace(matmul(same, same)) + 2 * sum( + item["identity_coefficient_trace"] for item in results.values()) + rank_lower = tr * tr / tr_square + residual_lower = rank_lower - 16 + return exact_json({ + "status": "PASS_INDEPENDENT_QQ16_THREE_QUERY_TRACE", + "source": {"base": SOURCE_BASE, "archive_path": ARCHIVE_PATH, + "archive_sha256": ARCHIVE_SHA, + "member_sha256_and_payload_sha256": MEMBERS}, + "reconstruction": { + "method_R": "reverse covectors on all 712 independent input positions, then source projection", + "method_routes": "orthonormal chart/stage coordinate swaps; 73 binary columns per route", + "scalar_prefix_event_count": cut, "centre_output_registers": word["centers"], + "retained_helper_dependencies_per_row": [len(row) for row in nuisance], + "R_dense": exact_json(rows), + "R_dense_sha256": digest(canonical(exact_json(rows))), + "R_rows_integer_json_sha256": digest(canonical(exact_json(rows))), + "routes_U96_stage_major_sha256": digest(canonical( + [routes[stage][port] for stage in range(3) for port in U])), + "stage_0_1_2_route_columns_sha256": digest(canonical(routes)), + "A_ports": A, "T_ports": T, "U_ports": U, + "U_column_squared_norm_histogram": {"4": len(U)}, + }, + "same_stage_gram": same, "stage_pairs": results, + "trace_coefficients_per_regular_cover_order": { + "stacked_Gram_trace": tr, "stacked_Gram_square_trace": tr_square, + "stacked_query_rank_lower_bound": rank_lower, + "rank_B0_restricted_to_joint_kernel_B1_B2_lower_bound": residual_lower, + }, + "controls": controls(columns, routes, relatives["1,2"], canonical(exact_json(rows))), + "scope": { + "finite_coverage": "112 actual R columns and stage 0/1/2 routes; all 96 ordinary columns and all three pairs", + "representation": "finite regular right cover action, payload-constant fields; arbitrary cover values", + "matrix_convention": "GF(2) matrices stored as columns; product(g,h) maps x to g(h(x)); D_gD_h=D_(gh)", + "collision_rule": "sum over each relative-route bucket K_g of K_g K_g^T", + "not_checked": ["full regular cover enumeration", "QQ16 chronological trajectory", "native phase replay", "precision or physical routing costs", "complete supplier", "new kappa"], + }, + }) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=Path(__file__).resolve().parents[2]) + args = parser.parse_args() + print(json.dumps(audit(args.repo), indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/qq16-extra-query-residual/test_package.py b/research/qq16-extra-query-residual/test_package.py new file mode 100644 index 0000000000..75b656412a --- /dev/null +++ b/research/qq16-extra-query-residual/test_package.py @@ -0,0 +1,162 @@ +#!/usr/bin/env python3 +"""Behavioral controls for the fixed receipts and independent mathematics. + +Apache-2.0; substantial OpenAI Codex assistance. Tests never rewrite evidence. +""" +from copy import deepcopy +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import types +import unittest +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +primary = load("qq16_primary", HERE / "verify.py") +oracle = load("qq16_oracle", HERE / "independent.py") + + +class PackageTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.actual = primary.build(REPO) + cls.receipt = json.loads((HERE / "RESULT.json").read_text()) + + def test_fixed_receipts_and_independent_source_derivation(self): + primary.validate(self.receipt, self.actual) + other = oracle.audit(REPO) + expected = json.loads((HERE / "ORACLE.json").read_text()) + self.assertEqual(oracle.canonical(other), oracle.canonical(expected)) + first = self.actual["route_audit"] + for key in ("R_dense_sha256", "routes_U96_stage_major_sha256"): + self.assertEqual(first[key], other["reconstruction"][key]) + self.assertEqual(first["ordinary_gram"], other["same_stage_gram"]) + for key, pair in first["pairs"].items(): + self.assertEqual(pair["identity_coefficient"], other["stage_pairs"][key]["identity_coefficient"]) + self.assertEqual(pair["distinct_routes"], other["stage_pairs"][key]["distinct_relative_routes"]) + bounds = other["trace_coefficients_per_regular_cover_order"] + self.assertEqual(first["trace_per_cover_owner"], bounds["stacked_Gram_trace"]) + self.assertEqual(first["square_trace_per_cover_owner"], bounds["stacked_Gram_square_trace"]) + self.assertEqual(first["stacked_rank_lower_per_cover_owner"], bounds["stacked_query_rank_lower_bound"]) + self.assertEqual(first["missing_A_dimension_lower_per_cover_owner"], + bounds["rank_B0_restricted_to_joint_kernel_B1_B2_lower_bound"]) + + def test_complete_receipt_rejects_semantic_and_typed_corruption(self): + mutants = [] + bad = deepcopy(self.receipt) + bad["route_audit"]["missing_A_dimension_lower_per_cover_owner"] = "33/7" + mutants.append(bad) + bad = deepcopy(self.receipt) + bad["route_audit"]["pairs"]["0,1"]["identity_coefficient"][0][0] -= 1 + bad["route_audit"]["pairs"]["0,1"]["identity_coefficient"][1][1] += 1 + mutants.append(bad) # same trace, different matrix + bad = deepcopy(self.receipt) + del bad["tail"][2] + mutants.append(bad) + bad = deepcopy(self.receipt) + bad["finite_fixture"]["after_B1_only_YU"] = 1 + mutants.append(bad) # bool and integer must remain distinct + bad = deepcopy(self.receipt) + bad["unpriced_native_gain"] = True + mutants.append(bad) + for bad in mutants: + with self.subTest(change=str(bad)[:60]): + with self.assertRaisesRegex(primary.CheckError, "complete fixed receipt"): + primary.validate(bad, self.actual) + # Formatting/key order is intentionally not a semantic difference. + reformatted = json.loads(json.dumps(self.receipt, sort_keys=True, indent=4)) + primary.validate(reformatted, self.actual) + + def test_missing_receipts_and_no_overwrite(self): + before = (HERE / "RESULT.json").read_bytes() + with tempfile.TemporaryDirectory(prefix="qq16-receipts-") as tmp: + missing = Path(tmp) / "missing.json" + run = subprocess.run([sys.executable, "-I", "-B", str(HERE / "verify.py"), + "--repo", str(REPO), "--certificate", str(missing)], + text=True, capture_output=True) + self.assertNotEqual(run.returncode, 0) + self.assertIn("FileNotFoundError", run.stderr) + self.assertFalse(missing.exists()) + run = subprocess.run([sys.executable, "-I", "-B", str(HERE / "verify.py"), + "--repo", str(REPO), "--write", str(HERE / "RESULT.json")], + text=True, capture_output=True) + self.assertNotEqual(run.returncode, 0) + self.assertIn("FileExistsError", run.stderr) + self.assertEqual(before, (HERE / "RESULT.json").read_bytes()) + + def test_live_source_drift(self): + # A small shadow of live input paths tests byte drift without editing + # frozen sources or making another Git checkout. Git reads use REPO. + sources = json.loads((HERE / "SOURCES.json").read_text())["files"] + with tempfile.TemporaryDirectory(prefix="qq16-source-") as tmp: + root = Path(tmp) + for item in sources: + if item["usage"] != "input": + continue + target = root / item["path"] + target.parent.mkdir(parents=True, exist_ok=True) + target.symlink_to(REPO / item["path"]) + name = "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md" + target = root / name + target.unlink() + target.write_bytes((REPO / name).read_bytes() + b"\nchanged source\n") + command = primary.subprocess.check_output + def git_read(args, **kwargs): + kwargs["cwd"] = REPO + return command(args, **kwargs) + with patch.object(primary.subprocess, "check_output", side_effect=git_read): + with self.assertRaisesRegex(primary.CheckError, "live source: " + name): + primary.authenticate(root) + + def test_independent_controls_fail_when_named_guards_are_removed(self): + source = (HERE / "independent.py").read_text() + guards = [ + 'require(len(relative_routes) == len(set(relative_routes)) == 96,\n "96 distinct relative routes")', + 'require(gram(columns) == scalar_identity(48), "ordinary column Gram")', + ] + for guard in guards: + self.assertEqual(source.count(guard), 1) + mutant = types.ModuleType("qq16_guard_removed") + mutant.__file__ = str(HERE / "independent.py") + exec(compile(source.replace(guard, "pass"), mutant.__file__, "exec"), mutant.__dict__) + with self.assertRaisesRegex(mutant.AuditError, "negative control unexpectedly accepted"): + mutant.audit(REPO) + + def test_normal_optimized_and_relocated_verification_preserve_artifacts(self): + # Package relocation uses an explicitly supplied original Git repo. + # This is not a source-export or full copied-repository cold replay. + names = ["RESULT.json", "ORACLE.json", "SOURCES.json"] + before = {name: (HERE / name).read_bytes() for name in names} + with tempfile.TemporaryDirectory(prefix="qq16-relocated-") as tmp: + moved = Path(tmp) / "package" + shutil.copytree(HERE, moved, ignore=shutil.ignore_patterns("__pycache__")) + outputs = [] + for optimize in ([], ["-O"]): + run = subprocess.run([sys.executable, "-I", *optimize, "-B", str(moved / "verify.py"), + "--repo", str(REPO)], cwd=tmp, text=True, capture_output=True) + self.assertEqual(run.returncode, 0, run.stderr) + outputs.append(run.stdout) + self.assertEqual(outputs[0], outputs[1]) + self.assertIn("PASS_QQ16_EXTRA_QUERY_RESIDUAL", outputs[0]) + for name in names: + self.assertEqual((moved / name).read_bytes(), before[name]) + for name in names: + self.assertEqual((HERE / name).read_bytes(), before[name]) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/qq16-extra-query-residual/verify.py b/research/qq16-extra-query-residual/verify.py new file mode 100644 index 0000000000..0705f968dd --- /dev/null +++ b/research/qq16-extra-query-residual/verify.py @@ -0,0 +1,295 @@ +#!/usr/bin/env python3 +"""Exact QQ16 residual audit: retained R certificate and transvection routes. + +No predecessor executable is imported. The independent oracle instead uses +reverse covectors and chart-axis swaps. Apache-2.0; OpenAI Codex assistance. +""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +import io +import json +from pathlib import Path +import subprocess +import tarfile + +HERE = Path(__file__).resolve().parent +BASE = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +PHASE_MEMBER = "t16/global/base/work/complex-nine-native/DATA-PHASES.json" +PHASE_SHA = "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" +PACKET = "research/joint-query/certificate.json.gz" +TAIL = "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json" +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 << k for k in range(73)) + +class CheckError(ValueError): + pass + +def require(ok, why): + if not ok: + raise CheckError(why) + +def digest(raw): + return hashlib.sha256(raw).hexdigest() + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + +def authenticate(repo): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + require(manifest["base_commit"] == BASE, "source base") + sources = {} + for entry in manifest["files"]: + path = entry["path"] + raw = subprocess.check_output(["git", "show", BASE + ":" + path], cwd=repo) + blob = subprocess.check_output(["git", "rev-parse", BASE + ":" + path], cwd=repo).decode().strip() + require(digest(raw) == entry["sha256"] and blob == entry["git_blob"], "provenance: " + path) + if entry["usage"] == "input": + require((repo / path).read_bytes() == raw, "live source: " + path) + sources[path] = raw + require({ARCHIVE, PACKET, TAIL} <= sources.keys(), "required source inventory") + return sources + +def load_inputs(sources): + packet = json.loads(gzip.decompress(sources[PACKET])) + require((packet["A_ports"], packet["T_ports"], packet["U_ports"]) == (A, T, U), "selected port partition") + require(len(packet["R_rows"]) == 8, "eight query rows") + R = [[Q(row.get(str(p), 0)) for p in range(112)] for row in packet["R_rows"]] + require(all(x.denominator == 1 for row in R for x in row), "integer R") + R = [[int(x) for x in row] for row in R] + with tarfile.open(fileobj=io.BytesIO(sources[ARCHIVE]), mode="r:gz") as archive: + members = [m for m in archive.getmembers() if m.name == PHASE_MEMBER] + require(len(members) == 1 and members[0].isfile(), "unique phase member") + raw = archive.extractfile(members[0]).read() + require(digest(raw) == PHASE_SHA, "phase member digest") + phases = json.loads(raw) + return R, phases, json.loads(sources[TAIL]) + +def apply(columns, x): + y = 0 + while x: + bit = x & -x + y ^= columns[bit.bit_length() - 1] + x ^= bit + return y + +def compose(left, right): + return tuple(apply(left, c) for c in right) + +def routes_from_transvections(phases): + require(phases["m"] == 73 and len(phases["recipes"]) == 112, "phase dimensions") + routes = [[], [], []] + for p, record in enumerate(phases["recipes"]): + require(record["port"] == p, "phase port order") + chart = [record["q"]] + record["idle_children"][0]["orthogonal_axes"][:8] + require(len(chart) == 9 and all(0 < c < 512 for c in chart), "local chart support") + require(all((x & y).bit_count() % 2 == int(i == j) + for i, x in enumerate(chart) for j, y in enumerate(chart)), "chart orthogonality") + routes[0].append(AXES) + for stage in (1, 2): + normals = [chart[i + 1] ^ AXES[9 + 8 * (stage - 1) + i] for i in range(8)] + matrix = tuple(x ^ apply(normals, sum(((x & n).bit_count() % 2) << i + for i, n in enumerate(normals))) for x in AXES) + require(compose(matrix, matrix) == AXES, "route inverse") + require(all((x & y).bit_count() % 2 == int(i == j) + for i, x in enumerate(matrix) for j, y in enumerate(matrix)), "route orthogonality") + routes[stage].append(matrix) + return routes + +def gram(R, ports): + return [[sum(R[i][p] * R[j][p] for p in ports) for j in range(8)] for i in range(8)] + +def diagonal(k): + return [[k * int(i == j) for j in range(8)] for i in range(8)] + +def cross_coefficient(R, routes, s, t, ports=U): + """Group equal relative routes, then compute sum_g C_g C_g^T exactly.""" + grouped = {} + for p in ports: + g = compose(routes[s][p], routes[t][p]) # checked involutions + matrix = grouped.setdefault(g, diagonal(0)) + for i in range(8): + for j in range(8): + matrix[i][j] += R[i][p] * R[j][p] + result = [[sum(sum(C[i][k] * C[j][k] for k in range(8)) for C in grouped.values()) + for j in range(8)] for i in range(8)] + return len(grouped), result + +def route_report(R, routes): + norms = [sum(row[p] ** 2 for row in R) for p in U] + require(norms == [4] * 96, "ordinary column norms") + require(gram(R, U) == diagonal(48), "ordinary Gram") + require(gram(R, A) == gram(R, T) == diagonal(4), "selected dyadic unit minors") + pairs = {} + for s, t in ((0, 1), (0, 2), (1, 2)): + count, coefficient = cross_coefficient(R, routes, s, t) + require(count == 96, "distinct relative routes") + require(coefficient == diagonal(192), "cross identity coefficient") + pairs[f"{s},{t}"] = {"distinct_routes": count, "identity_coefficient": coefficient, + "normalized_trace": sum(coefficient[i][i] for i in range(8))} + 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) + 2 * sum(p["normalized_trace"] for p in pairs.values()) + bound = Q(trace * trace, square) + require(bound > 16, "positive residual rank") + return {"R_dense_sha256": digest(canonical(R)), + "routes_U96_stage_major_sha256": digest(canonical([routes[s][p] for s in range(3) for p in U])), + "ordinary_column_norms": dict(sorted(Counter(map(str, norms)).items())), + "ordinary_gram": gram(R, U), "pairs": pairs, + "trace_per_cover_owner": trace, "square_trace_per_cover_owner": square, + "stacked_rank_lower_per_cover_owner": str(bound), + "missing_A_dimension_lower_per_cover_owner": str(bound - 16)} + +def tail_trace(events): + """Recompute the inherited tail on its one formal ordinary vector h.""" + x, y = [0]*4, [1, 0, 0, 0] + result, stages = [], [] + for event in events: + kind = event["kind"] + if kind == "bridge": + src, dst, c = event["src"], event["dst"], event["coefficient"] + require(0 <= src < 4 and 0 <= dst < 4 and src != dst and c in (-1, 1), "bridge domain") + x[dst] += c * x[src] + y[src] -= c * y[dst] + elif kind == "local": + s = event["stage"] + require(s in range(2, 9), "tail stage") + bank = (s // 2) % 4 + require((x if s % 2 == 0 else y)[bank] == 0, "active tail source is zero") + stages.append(s) + else: + require(kind == "terminal", "tail event kind") + x, y = y, [-v for v in x] + result.append({"kind": kind, "x": x.copy(), "y": y.copy()}) + require(stages == list(range(2, 9)), "complete tail stage coverage") + require(x == [1, 0, 0, 0] and y == [0]*4, "tail endpoint") + return result + +def matrix_rank(matrix): + a = [list(map(Q, row)) for row in matrix] + rank = 0 + for col in range(len(a[0])): + pivot = next((i for i in range(rank, len(a)) if a[i][col]), None) + if pivot is None: + continue + a[rank], a[pivot] = a[pivot], a[rank] + scale = a[rank][col] + a[rank] = [x / scale for x in a[rank]] + for i in range(rank + 1, len(a)): + if a[i][col]: + scale = a[i][col] + a[i] = [x - scale*y for x, y in zip(a[i], a[rank])] + rank += 1 + if rank == len(a): + break + return rank + +def finite_regular_fixture(): + """Complete C3xC3 regular example, not a claim about the actual cover. + + One centre coordinate, nine ordinary ports, route s*p for B_s. Taking + the same mean-zero field in every port gives an explicit hidden h. + """ + points = [(i, j) for i in range(3) for j in range(3)] + index = {g: i for i, g in enumerate(points)} + B = [] + for s in range(3): + rows = [] + for g in points: + row = [0]*81 + for p, point in enumerate(points): + at = ((g[0]+s*point[0]) % 3, (g[1]+s*point[1]) % 3) + row[9*p+index[at]] = 1 + rows.append(row) + B.append(rows) + e, h = [1, -1]+[0]*7, ([1, -1]+[0]*7)*9 + query = lambda s, v: [sum(a*b for a,b in zip(row,v)) for row in B[s]] + require(query(1,h) == query(2,h) == [0]*9, "fixture hidden queries") + require(query(0,h) == [9*v for v in e], "fixture old query") + stack = sum(B, []) + actual_rank, old_rank = matrix_rank(stack), matrix_rank(B[1]+B[2]) + require((actual_rank,old_rank) == (25,17), "fixture complete ranks") + H = [[sum(a*b for a,b in zip(x,y)) for y in stack] for x in stack] + trace, square = sum(H[i][i] for i in range(27)), sum(x*x for row in H for x in row) + lower = Q(trace*trace,square) + require(actual_rank >= lower > 18, "fixture trace bound") + # Selected sections are identities in this illustrative model. The + # general ordered proof supplies the arbitrary-chart assertion. + xa, ya = [-v for v in query(0,h)], query(0,h) + f0 = [u+v for u,v in zip(query(0,h),xa)] + require(f0 == [0]*9 and any(xa), "fixture initial A and F query") + selected_after_f0 = [a+b for a,b in zip(xa,ya)] + require(selected_after_f0 == [0]*9, "fixture selected F endpoint") + q2, b1 = query(2,h), query(1,h) + require(q2 == b1 == [0]*9, "fixture B query cancellation") + require([a-b for a,b in zip(h,h)] == [0]*81, "fixture ordinary B endpoint") + return {"group":"C3xC3", "cover_size":9, "matrix_shape":[27,81], + "stacked_rank":actual_rank, "two_query_rank":old_rank, + "exact_missing_dimension":actual_rank-old_rank, "trace":trace, + "square_trace":square, "rank_bound":str(lower), "explicit_h":h, + "B0_h":query(0,h), "B1_h":b1, "B2_h":q2, "initial_A":xa, + "F0_query":f0, "after_B1_only_YU":True} + +def rejected(call, message): + try: + call() + except CheckError as error: + require(message in str(error), "wrong rejection: " + str(error)) + else: + raise CheckError("negative control unexpectedly accepted: " + message) + +def controls(R, routes, events): + bad_R = deepcopy(R) + bad_R[0][U[0]] += 1 + rejected(lambda: route_report(bad_R,routes), "ordinary column norms") + bad_routes = deepcopy(routes) + bad_routes[1][U[1]] = bad_routes[1][U[0]] + rejected(lambda: route_report(R,bad_routes), "distinct relative routes") + bad_events = deepcopy(events) + minus = next(i for i,e in enumerate(bad_events) if e["kind"] == "bridge" and e["coefficient"] == -1) + del bad_events[minus] + rejected(lambda: tail_trace(bad_events), "active tail source is zero") + return ["changed_column", "collapsed_route", "omitted_cancelling_bridge"] + +def build(repo): + sources = authenticate(repo) + R, phases, witness = load_inputs(sources) + routes = routes_from_transvections(phases) + report = route_report(R,routes) + events = witness["trajectory_after_B1"] + trace = tail_trace(events) + for event,state in zip(events,trace): + require(event["ordinary"] == [z for pair in zip(state["x"],state["y"]) for z in pair], "inherited tail receipt") + return {"schema":1, "status":"PASS_QQ16_EXTRA_QUERY_RESIDUAL", "route_audit":report, + "tail":trace, "finite_fixture":finite_regular_fixture(), + "negative_controls":controls(R,routes,events), + "source_sha256":{k:digest(v) for k,v in sorted(sources.items())}, + "scope":"Fixed F0/B1 and retained observations plus side-effect-free B2 X_U; written rank/existence theorem and finite source checks; no native tariff, full controller or new kappa."} + +def validate(receipt,actual): + require(type(receipt) is dict and canonical(receipt) == canonical(actual), "complete fixed receipt") + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo",type=Path,default=HERE.parents[1]) + parser.add_argument("--write",type=Path,help="explicitly generate a NEW receipt; refuses overwrite") + parser.add_argument("--certificate",type=Path,default=HERE / "RESULT.json") + args = parser.parse_args() + actual = build(args.repo.resolve()) + if args.write: + with args.write.open("x") as file: + json.dump(actual,file,indent=2,sort_keys=True) + file.write("\n") + print("GENERATED_QQ16_EXTRA_QUERY_RESIDUAL " + str(args.write)) + return + receipt = json.loads(args.certificate.read_text()) + validate(receipt,actual) + print(actual["status"] + " rank_stack>=144|G|/7 missing_A>=ceil(32|G|/7) no_new_kappa") + +if __name__ == "__main__": + main()