From 68dcf180ce3918a9ee1998bfc5455f42516c6009 Mon Sep 17 00:00:00 2001 From: Adam Gall Date: Wed, 14 Oct 2026 15:05:04 -0400 Subject: [PATCH] Prove QQ16 first-forward A logger obstruction --- .../qq16-forward-logger-obstruction/README.md | 272 +++++++++++ .../RESULT.json | 158 +++++++ .../SELECTION.json | 134 ++++++ .../SOURCES.json | 78 ++++ .../qq16-forward-logger-obstruction/TASK.json | 136 ++++++ .../VERIFY.json | 41 ++ .../qq16-forward-logger-obstruction/verify.py | 425 ++++++++++++++++++ 7 files changed, 1244 insertions(+) create mode 100644 research/qq16-forward-logger-obstruction/README.md create mode 100644 research/qq16-forward-logger-obstruction/RESULT.json create mode 100644 research/qq16-forward-logger-obstruction/SELECTION.json create mode 100644 research/qq16-forward-logger-obstruction/SOURCES.json create mode 100644 research/qq16-forward-logger-obstruction/TASK.json create mode 100644 research/qq16-forward-logger-obstruction/VERIFY.json create mode 100755 research/qq16-forward-logger-obstruction/verify.py diff --git a/research/qq16-forward-logger-obstruction/README.md b/research/qq16-forward-logger-obstruction/README.md new file mode 100644 index 0000000000..722d283cec --- /dev/null +++ b/research/qq16-forward-logger-obstruction/README.md @@ -0,0 +1,272 @@ +# Changing the first QQ16 A logger is insufficient + +**Scoped negative result; no new supplier or κ.** Changing the first forward +QQ16 source encoder cannot restore the initial selected inputs if it preserves +the full-query T output, the ordinary response and selected pair sums, while +B1, the ordinary tail and the allowed final observations stay fixed. The A +logger may change arbitrarily, including reads of ordinary inputs within F0. +The obstruction survives even if the entire changed encoder is granted for free. + +This is a changed-first-forward theorem, not a repetition of the fixed-F0 +witness and not an obstruction to every changed first pair. The proof below +quantifies over every invertible homogeneous source encoder with the displayed +outputs; the finite fixtures do not establish that quantifier. + +## Exact interface and predecessors + +Ali Romman's [PR1969](https://github.com/CrocSwap/integer-mult-bounds/pull/1969), +head `a6e6ad3936f67b8f63b5b68c5e75d540610a65e7`, supplies the +[ordered QQ16 maps](../joint-query/evidence/JOINT-QUERY-TRANSFER.md), native +local words and the [fixed-pair witness](../joint-query/evidence/QQ16-SELECTED-WITNESS.md). +Its [independent observation review](../joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md) +proves eight missing B2 directions for fixed F0/B1. Those results are credited +inputs, not new claims here. + +Retain its disjoint sets + +``` +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). +``` + +Use the actual routed centre queries R_s, their ordinary restrictions B_s, +and the two-sided selected sections P_(s,A), P_(s,T). For the first source +write z=X_U, a=ell_(0,A)X, c=ell_(0,T)X, and f=B0 z+a+c. +Let **G be any invertible homogeneous linear source map** satisfying + +``` +X'_U = z - K_(0,U) f, +X'_T = P_(0,T) f. +``` + +There is no further restriction on X'_A. In particular, G may read ordinary +inputs to compute its A output. Complete the pair by + +``` +Y'_U = Y_U + X'_U, +Y'_S = X_S + Y_S - X'_S, S=A union T. +``` + +G acts on X alone. No input-dependent transcript, extra output or unrestored +helper is retained. Its full pair extension is invertible: invert G, then use +the last two equations to recover Y. Arbitrary initial Y is allowed, not cleared. + +After this first call, retain **the original B_1_2**, the original ordinary +bank schedule and its terminal types. Later homogeneous selected-only linear +controls may change arbitrarily but may not read ordinary fields. Allowed +observations are all selected endpoints, all completed-X descendants and all +five forward query histories. The final named X0 ordinary field has the old-Y +native type, so it is not one of the completed-X descendants. This distinction +is essential, exactly as in the predecessor witness. + +## 1. An actual B0/B1 witness + +Let * transpose the real coefficient matrix and invert the cover route. +The source columns r_p satisfy + +``` +||r_p||^2 = 4, sum_(p in U) r_p r_p^T = 48 I. +``` + +Stage zero has identity routes. The 96 actual stage-one ordinary routes g_p +are distinct involutions. Consequently B0 B0*=B1 B1*=48I. For e_k supported +at the identity cover element, define + +``` +h_k = (48 I - B1* B1) B0* e_k. (1) +``` + +Then B1 h_k=0. Since g_p^-1 g_q is identity exactly when p=q, the identity +coefficient of B0 B1* B1 B0* is + +``` +sum_p (r_p r_p^T)^2 = 4 sum_p r_p r_p^T = 192 I. +``` + +Thus the identity coefficient of B0 h_k is + +``` +48^2 I - 192 I = 2112 I. (2) +``` + +The eight h_k are independent and have integer coefficients. The checker +reconstructs R from the selected scalar prefix, derives the 112 stage-one +routes from the actual phase recipes, constructs every group-ring coefficient +of all eight h_k, and checks the **entire** B1 h=0, not only its identity term. +The 17-coordinate route representation is faithful: stage one acts on the nine +local and eight first-stage coordinates and fixes the other 56 coordinates. +It is not an abelian or cover-invariant quotient. + +These are valid witnesses at every positive tensor size: take the fields +constant in payload coordinates, while leaving cover values arbitrary. Payload +translations act trivially on this subspace. Exact logical frame conventions +and their native meaning remain inherited from the predecessor, not removed by +an approximation. No division by 3, 11 or 13 is used in (1). + +## 2. Pull back the erased state through any changed logger + +Fix one h=h_k and prescribe the state immediately after G: + +``` +X'_U=Y'_U=h, +X'_A=P_(2,A) B2 h, Y'_A=-P_(2,A) B2 h, +X'_T=Y'_T=0. +``` + +All other banks are zero. Since G is surjective, this X' has a unique original +source X. The conserved sums determine Y_S=-X_S, and Y_U=0. The two fixed +source output equations imply, in order, + +``` +f=0, z=h, a+c=-B0 h. (3) +``` + +Equation (2) makes (3) nonzero. Hence **at least one of the original selected +A or T inputs is nonzero**, regardless of what G writes into A. The proof does +not claim that the original T alone must be nonzero for every changed logger. + +Now run the unchanged B_1_2. Its future query is +`q2=B2 h+ell_(2,A)Y'_A=0`; the future logger E2 makes its A source zero. +Its T source and old selected-X driver are zero. The remaining current query +is `b1=B1 h=0`. Substitution into the credited ordered backward equations +therefore leaves exactly + +``` +Y_0,U=h; all other ordinary and selected fields zero. +``` + +This is the same post-B1 state as the predecessor's witness, although the +preimage and its missing query are different. The inherited ordinary tail +therefore gives zero selected observations, zero completed-X descendants and +zero f2,f4,f6,f8; f0=0 was already established. Its only terminal ordinary +value is h in old-Y-typed X0. Homogeneous selected-only operations preserve +the all-zero selected state. The zero initial input has identical allowed +observations but different required selected data. No decoder from those +observations alone, even a nonlinear decoder, can restore both inputs. + +**This is the new implication:** an arbitrary rewrite of the A logger cannot +help while the two other source outputs and the downstream interface are fixed. +The old proof with its fixed preimage did not itself quantify over these G. + +### Ordered description of the whole linear logger family + +In normalized coordinates write the remaining output as +`d=alpha a+beta c+L z`. Here alpha and beta are arbitrary query operators and +L may read every ordinary source coordinate. Put D=beta-alpha. If D has a +two-sided inverse, the exact source inverse is + +``` +z = w + K_(0,U) f, +sigma = f - B0 z, +c = D^-1 (d - alpha sigma - L z), +a = sigma - c. +``` + +Factors are not commuted. Eliminating z and sigma reduces source invertibility +to invertibility of D on the query space. This also shows the admitted family +is nonempty and substantially larger than the original logger `d=c`. +For the erased state, every member still has `a+c=-B0h`. The checker includes +all 500 invertible scalar loggers over F5 with two ordinary coordinates and a +rational two-coordinate example with noncommuting alpha and beta. These are +regressions of the ordered calculation, not a substitute for the proof. + +## Complete favorable accounting and stop decision + +The credited original local pair has native rank mass **11076**, real scalar +primitive bound **426196**, **528** added full-cover maps and **64** native +wrapper maps. Those local counts are read from the pinned native invoice; +map counts are not physical address costs. They are context, not a lower bound +on a resynthesized G and not a whole-controller bill. + +Before synthesis, grant the changed G **zero total cost**, and grant zero costs +for every extra read internal to it, source/target adapters, owner/helper hosting, +precision, routing and restoration work. Keep the required endpoint and +observation contract. Even this favorable completion is impossible by (3). +Adding nonnegative charges cannot fix its information loss. Accordingly no +moment root, child profile improvement, native synthesis or supplier claim is +made. A separately retained observation changes the interface and is not +silently assigned zero cost here. + +## Evidence and reproduction + +Base `564148b82ae9df72163f22106f15e73efca8aff2`, priority revision 4; +selection seed `e86c305e59ee045687c6d1ab7d3956e0`, recursive-interfaces, +`joint-query-controller`. [SELECTION.json](SELECTION.json) is the unchanged +one-shot draw. [TASK.json](TASK.json) records the hypothesis, pre-computation +screen, overlap scope and next questions. [SOURCES.json](SOURCES.json) pins +live inputs and historical provenance. No predecessor executable is imported +and no source archive is copied or changed. +The submission checkpoint read main +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`: guidance changed, but priority +revision, catalogue, selected record and scientific inputs did not. The original +scientific base and source pins are intentionally retained. + +From the repository root, standard-library CPython 3.12: + +```sh +uv run --python 3.12 --no-project python -I -B research/qq16-forward-logger-obstruction/verify.py +uv run --python 3.12 --no-project python scripts/research_package.py --package research/qq16-forward-logger-obstruction +``` + +The registered replay also runs under `-O`; all checks use explicit exceptions. +It compares the complete canonical JSON result with [RESULT.json](RESULT.json). +To regenerate evidence without overwriting the committed receipt, use +`verify.py --emit /tmp/qq16-forward-logger-result.json` with a fresh path. + +Observed on CPython 3.12.12: `PASS_QQ16_FORWARD_LOGGER_OBSTRUCTION` in the +scientific generation and both registered modes, followed by +`PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=negative-result`. +The receipt records 4320 nonzero ordinary-field/group terms, complete B1h=0, +eight independent missing directions, 500 changed loggers, 8000 dirty pair-basis +inverse checks and the noncommuting rational fixture. An initial registration +attempt rejected a combined next-questions heading; the corrected heading passed. + +Semantic controls remove the projector term, change 48 to 47, collapse all +routes, corrupt a query column and omit the first cancelling ordinary bridge. +An extra B0 observation detects the witness, delimiting the result. The finite +logger check tests both inverse orders on every dirty pair-state basis column. +The tail replay is only the restricted h-coefficient trajectory from the pinned +witness and independent review receipts; **it is not a replay of the absent +full controller program or the native supplier**. + +## Overlap and limits + +The final shared overlap snapshot covers 353 open PRs and 738 discussion records, +with complete pagination at 2026-10-14 19:00:33/19:02:09 UTC. The targeted offline +search at 19:03:45 also covered 1538 local records (including this package). +Targeted reading included merged PR1969, the exact local sources and +[PR2079](https://github.com/CrocSwap/integer-mult-bounds/pull/2079) at +`49df8190b158e3028e702b2c6b798117006f7249` (Cinna Davis), following +[discussion2074](https://github.com/CrocSwap/integer-mult-bounds/discussions/2074). +That concurrent work separates the original eight-direction witness using a +separately retained pre-F0 B2 observation, and explicitly leaves full-controller +injectivity open. This result instead changes the first A logger without adding +an observation. +Cached searches and absence of a matching title are not novelty proofs. + +This does not exclude changing B1, changing the full-query T output or ordinary +response, retaining an extra transcript, reading ordinary old-Y output later, +nonhomogeneous control, changing selected conservation or changing the ordinary +schedule. No physical lower bound, all-size supplier admission, stronger κ, +complete cold replay or formal proof-assistant verification is claimed. + +## Open next questions + +- **Change an actually necessary premise.** Specify one different first T + record or ordinary response and apply the same post-F0 state first. A legal + native realization and complete paid bill remain the blockers. +- **Price a separately retained observation.** Test restoration of both initial + selected inputs, not only one old B2 witness. Read access, storage lifetime, + native types, restoration and recursive pricing remain obligations. + +## Attribution + +Prepared for Adam Gall with substantial OpenAI Codex assistance. New material +uses Apache-2.0. Ali Romman and the credited centre-encoding contributors supply +QQ16, its source loader/reconstruction method, native routes and the original +witness and review. The gauge44/t16 geometry, compiler and selected-supplier +lineage retain their full [source notices](../joint-query/NOTICE.md). The new +contribution is the changed-logger pullback theorem, B0/B1 integer witness and +its checker, not those inherited constructions. No independent human or formal +kernel review is asserted. diff --git a/research/qq16-forward-logger-obstruction/RESULT.json b/research/qq16-forward-logger-obstruction/RESULT.json new file mode 100644 index 0000000000..8d896cce98 --- /dev/null +++ b/research/qq16-forward-logger-obstruction/RESULT.json @@ -0,0 +1,158 @@ +{ + "finite_logger_fixture": { + "changed_logger_witnesses": 500, + "field": 5, + "loggers": 500, + "two_sided_dirty_basis_checks": 8000 + }, + "limits": [ + "No arbitrary-first-pair obstruction", + "No lower bound on paid ordinary reads", + "No native logger synthesis or supplier admission", + "No new kappa or formal-kernel proof" + ], + "ordered_fixture": { + "centre_dimension": 2, + "noncommuting_M_N": true, + "ordinary_dimension": 4, + "two_sided_source_basis_checks": 16, + "witnesses": 2 + }, + "query": { + "columns": 112, + "distinct_ordinary_routes": 96, + "gram": 48, + "ordinary_columns": 96, + "query_columns_sha256": "38664b168db7ae1158c3c4cbd56622d5cf0ff22911e02c2c4aed323316566d82", + "source_scalar_prefix_operations": 10851, + "stage_one_routes_sha256": "f60e780fc1a7ee97bb64d314bc2b89aa3936da7a3905adce3cf05f35ed0ddf46" + }, + "result": "Every invertible source F0 logger with fixed U/T outputs and conserved selected pair sums fails selected restoration under fixed B1 and the retained observation/tail contract, even with zero added logger cost.", + "retained_pair_bill": { + "added_cover_maps": 528, + "native_mass": 11076, + "real_scalar_bound": 426196, + "wrapper_maps": 64 + }, + "semantic_controls": { + "collapsed_routes_zero_witness": true, + "corrupted_query_gram": true, + "extra_B0_observation_detects_witness": true, + "omitted_projector_term": true, + "wrong_gram_coefficient": true + }, + "status": "PASS_QQ16_FORWARD_LOGGER_OBSTRUCTION", + "tail": { + "events": 17, + "final_X_coefficients": [ + 1, + 0, + 0, + 0 + ], + "final_Y_coefficients": [ + 0, + 0, + 0, + 0 + ], + "forward_queries_zero": [ + 0, + 2, + 4, + 6, + 8 + ], + "scope": "Restricted inherited h trajectory; not a full controller/native replay" + }, + "witness": { + "B0_h_group_terms": 4225, + "B0_h_identity_coefficient": [ + [ + 2112, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 2112, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 2112, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2112, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2112, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2112, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2112, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2112 + ] + ], + "B1_h_nonzero_terms": 0, + "canonical_group_ring_sha256": "9a23ea4cf582f9c4a345dd6491f4918ece98308f7dce63a7a6ad5ce57e1d259c", + "definition": "(48I-B1*B1)B0*e_k", + "independent_directions": 8, + "ordinary_field_group_terms": 4320 + } +} diff --git a/research/qq16-forward-logger-obstruction/SELECTION.json b/research/qq16-forward-logger-obstruction/SELECTION.json new file mode 100644 index 0000000000..fac3afb43c --- /dev/null +++ b/research/qq16-forward-logger-obstruction/SELECTION.json @@ -0,0 +1,134 @@ +{ + "seed": "e86c305e59ee045687c6d1ab7d3956e0", + "track": "recursive-interfaces", + "suggestions": [ + { + "task_id": "connector-alphabet-change", + "scope_key": "ff4f5113ed2256ab19ed", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "method": "Construct and charge a legal extra operation on a minimal instance.", + "starting_points": [ + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "joint-query-controller", + "scope_key": "0e34adbc1dd119161c3a", + "question": "Can one explicitly changed QQ16 interface recover the missing chart query and close a two-call controller within a favorable full budget?", + "method": "Change the first local pair or retained state, then test the existing lost-observation witness and price all new operations.", + "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" + ], + "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_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "coverage-law-change", + "scope_key": "225dda4a25bdcb8e3086", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "method": "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "catalog_assessed_on": "2026-10-14", + "priority_revision": 4, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/qq16-forward-logger-obstruction/SOURCES.json b/research/qq16-forward-logger-obstruction/SOURCES.json new file mode 100644 index 0000000000..3e1a85ddb9 --- /dev/null +++ b/research/qq16-forward-logger-obstruction/SOURCES.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "base_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "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/evidence/CONSERVED-QQ16.json", + "usage": "input", + "git_blob": "7a155a27dcf7f1ccd48e40d57a2c5d2724016e9b", + "sha256": "b91eb8599c403db55c889bb225a1cd93f46fdb83eb339f101d18843d52b1c920" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.json", + "usage": "input", + "git_blob": "e649641e9b44af2fff9742df51d439890c1a19cc", + "sha256": "588a3ce4593576ae921e97c6ced6a050f88736f29708cfee117385b254cd358f" + }, + { + "path": "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "usage": "input", + "git_blob": "c6ecf75654a084a9cc001bd62663f341976bae7a", + "sha256": "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "usage": "input", + "git_blob": "5082d791d0b993492cbc5bf61ac3b69e82c96f3f", + "sha256": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "usage": "input", + "git_blob": "307650f45e37c28d14fe913958efa4fb429242b7", + "sha256": "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc" + }, + { + "path": "research/joint-query/source_data.py", + "usage": "input", + "git_blob": "c9d465ed47500304bef65fcb588befe356c5cf09", + "sha256": "d23924511e3aed41e5e64511ca70126a636d91c8aa02e656cb61d6ceca1fe0a0" + }, + { + "path": "research/joint-query/verify_native.py", + "usage": "input", + "git_blob": "ede9e7e42744dd0c96790516a9acdfe07d180018", + "sha256": "1c58e7b6e8e1cde4df455c2129601c145ed763fc63a3ab427eb1058d1fc08bd2" + } + ] +} diff --git a/research/qq16-forward-logger-obstruction/TASK.json b/research/qq16-forward-logger-obstruction/TASK.json new file mode 100644 index 0000000000..4d7dfed85e --- /dev/null +++ b/research/qq16-forward-logger-obstruction/TASK.json @@ -0,0 +1,136 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 4, + "base_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "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": "Change the first forward selected A logger arbitrarily, retaining the full R0 source query in T, the ordinary J response, selected pair sums, fixed B1 and the retained ordinary tail. Determine whether any invertible source-only logger can restore the arbitrary initial selected data from selected endpoints, completed-X descendants and all five forward queries.", + "scope_change_reason": "The predecessor fixes F0 and B1; this investigation changes F0 and quantifies over every invertible selected A encoding with the stated unchanged output equations, including ordinary reads inside F0. It does not add an independently retained observation or change B1.", + "bottleneck_link": "Identifies which first-pair premise must actually change to evade the central QQ16 lost-query obstruction, rather than resynthesizing a forward logger that cannot close its controller.", + "budget_minutes": 60, + "stop_rule": "Stop synthesis if the integer B0/B1 witness survives every first-forward logger under the stated equations; otherwise identify exactly which lemma fails before any larger controller search.", + "outcome": "negative-result", + "evidence": "README ordered pullback proof and RESULT.json: PASS_QQ16_FORWARD_LOGGER_OBSTRUCTION; full group-ring B1h=0 for eight B0/B1 witnesses, B0h identity coefficient 2112I, 96 distinct routes, 4320 witness field/group terms, 500 changed F5 loggers and 8000 dirty inverse-basis checks, noncommuting rational fixture, 17-event inherited restricted tail and semantic controls.", + "author": "Adam Gall", + "ai_assistance": "Substantial OpenAI Codex assistance in research, implementation, and verification.", + "selection_seed": "e86c305e59ee045687c6d1ab7d3956e0", + "selection_scope_key": "0e34adbc1dd119161c3a", + "domain": { + "coefficients": "Rational or complex cover fields; payload-constant finite-support witnesses at every positive tensor size.", + "retained_observation": "All selected outputs, completed-X descendants, and the five ordinary forward query histories. No extra retained ordinary query or scratch transcript.", + "changed_premise": "Arbitrary invertible homogeneous source F0 map satisfying only fixed U and T output equations; selected Y outputs are fixed by conserved pair sums." + }, + "method": "Build h=(48I-B1*B1)B0*e. Check actual stage-one routes distinct and Grams so B1h=0 and the identity coefficient of B0h is 2112e. Use arbitrary F0 surjectivity to pull back a B1-erased post-forward state and force nonzero original normalized A+T from f0=0.", + "optimistic_completed_bill": { + "retained_local_pair": { + "F0_native_mass": 5530, + "B1_native_mass": 5546, + "total_native_mass": 11076, + "F0_real_scalar_bound": 211210, + "B1_real_scalar_bound": 214986, + "total_real_scalar_bound": 426196, + "B1_added_cover_maps": 528, + "native_wrapper_maps": 64 + }, + "favorable_relaxation": "Grant the entire changed source encoder zero total cost, including all internal ordinary reads, adapters, owner/helper hosting, precision, routing and restoration. Still require exact endpoint restoration and the stated observation interface. Failure even in this relaxation rules out every nonnegative completed bill in this class; retained original pair counts are context, not a lower bound for a resynthesized logger. No moment root or universal native pricing lower bound is claimed.", + "stop_before_synthesis": true + }, + "predecessors": [ + { + "pr": 1969, + "author": "Ali Romman", + "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "scope": "Fixed F0/B1 witness, ordered QQ16 maps and native invoices; all remain credited predecessor results." + }, + { + "pr": 2079, + "author": "Cinna Davis", + "head": "49df8190b158e3028e702b2c6b798117006f7249", + "scope": "Concurrent extra B2 observation separates the original eight-direction witness but explicitly does not establish full-controller injectivity. Unlike this theorem it adds a separately retained observation; its profile-only screen is not used as a proof input." + }, + { + "discussion": 2074, + "author": "1337isnot1337", + "scope": "Concurrent paid pre-F0 B2 read; distinct because that adds an independent retained observation, which this theorem excludes." + } + ], + "freshness": { + "upstream_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "priority_revision": 4, + "submission_upstream_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "submission_guidance_read": "Read refreshed autoresearch 286-348 and priority-log 316-347; catalogue, selected record and scientific sources unchanged. Original scientific base intentionally retained.", + "open_prs_fetched_at": "2026-10-14T19:00:33.696741+00:00", + "open_prs_records": 353, + "discussions_fetched_at": "2026-10-14T19:02:09.707625+00:00", + "discussion_records": 738, + "complete_pagination": true, + "local_records": 1538, + "targeted_predecessor_read_at": "2026-10-14T18:53:56.170003+00:00", + "targeted_pr2079_head": "49df8190b158e3028e702b2c6b798117006f7249", + "final_targeted_search_at": "2026-10-14T19:03:45.771313+00:00", + "limitations": "Offline shared-cache search plus targeted live PR1969, PR2079, discussion2074 and local merged sources. Offline warnings remain explicit; search absence is not a novelty proof. No public discussion posts authorized." + }, + "validation": { + "runtime": "CPython 3.12.12, standard library, macOS arm64", + "scientific_emit": "PASS_QQ16_FORWARD_LOGGER_OBSTRUCTION", + "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE research/qq16-forward-logger-obstruction outcome=negative-result", + "optimized_replay": "PASS_QQ16_FORWARD_LOGGER_OBSTRUCTION under -I -O -B", + "initial_metadata_attempt": "Rejected a combined Open next questions heading; corrected to the required exact heading before successful registered replay. No mathematical check failed." + }, + "open_questions": [ + { + "question": "Can changing the T query record or ordinary response in the first pair escape the obstruction?", + "why_it_matters": "Those are now explicit surviving first-forward design directions.", + "first_step": "Specify one different T output or ordinary response and test the same post-F0 state before synthesizing native words.", + "blocked_by": "A legal native implementation and full paid bill remain required." + }, + { + "question": "Can a separately retained ordinary query restore the missing initial selected data?", + "why_it_matters": "An extra observation is outside this obstruction and may recover lost information.", + "first_step": "Follow the paid-query work and test the full selected restoration, not only one B2 witness.", + "blocked_by": "Independent query access, lifetime, endpoint restoration and physical charges." + } + ] +} diff --git a/research/qq16-forward-logger-obstruction/VERIFY.json b/research/qq16-forward-logger-obstruction/VERIFY.json new file mode 100644 index 0000000000..a1e101c43d --- /dev/null +++ b/research/qq16-forward-logger-obstruction/VERIFY.json @@ -0,0 +1,41 @@ +{ + "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/evidence/CONSERVED-QQ16.json", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.json", + "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/source_data.py", + "research/joint-query/verify_native.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Authenticate all inputs; reconstruct actual R and all stage-one routes; evaluate all eight full group-ring witnesses; exhaustive F5 changed loggers, noncommuting rational inverse, restricted inherited tail and semantic controls; compare complete canonical RESULT." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same complete exact mathematical replay with Python assertions disabled." + } + ] +} diff --git a/research/qq16-forward-logger-obstruction/verify.py b/research/qq16-forward-logger-obstruction/verify.py new file mode 100755 index 0000000000..9c4d180486 --- /dev/null +++ b/research/qq16-forward-logger-obstruction/verify.py @@ -0,0 +1,425 @@ +#!/usr/bin/env python3 +"""Exact source-bound evidence for the QQ16 first-forward logger obstruction. + +Adam Gall, with substantial OpenAI Codex assistance. Apache-2.0. +No predecessor executable is imported. The universal claim is proved in README. +""" +import argparse +from fractions import Fraction as Q +from functools import lru_cache +import gzip +from hashlib import sha256 +from io import BytesIO +import json +from pathlib import Path +import tarfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +MEMBERS = { + "slots/local/CANONICAL-WORD.json.gz": + "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "slots/local/LOCAL-PROGRAMS.json.gz": + "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": + "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", +} +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] +ID = tuple(1 << i for i in range(17)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(value): + return sha256(canonical(value)).hexdigest() + + +def authenticate(root): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + data = {} + for entry in manifest["files"]: + if entry["usage"] != "input": + continue + raw = (root / entry["path"]).read_bytes() + need(sha256(raw).hexdigest() == entry["sha256"], + "Source pin differs: " + entry["path"]) + data[entry["path"]] = raw + return data + + +def archive_data(raw): + result = {} + with tarfile.open(fileobj=BytesIO(raw), mode="r:gz") as archive: + for path, pin in MEMBERS.items(): + entries = [e for e in archive.getmembers() if e.name == path] + need(len(entries) == 1 and entries[0].isfile(), "Unique regular archive member") + body = archive.extractfile(entries[0]).read() + need(sha256(body).hexdigest() == pin, "Archive member pin: " + path) + result[path.rsplit("/", 1)[1]] = json.loads( + gzip.decompress(body) if path.endswith(".gz") else body) + return result + + +def query_columns(local): + word = local["CANONICAL-WORD.json.gz"] + need((word["v"], word["R"], word["h"]) == (112, 480, 9), "Selected dimensions") + # Propagate only derivatives with respect to X. Helpers/Y are independent + # columns with zero X derivative, not assumed initialized in the theorem. + rows = [{i: Q(1)} if i < 112 else {} for i in range(712)] + operations = 0 + for event in local["LOCAL-PROGRAMS.json.gz"]["forward"]: + if event == ["phase", "centers"]: + break + if event[0] != "scalar": + continue + gate = event[1] + reg = lambda token: token[1] + (704 if token[0] == "C" else 0) + target = reg(gate[1]) + op = gate[0] + operations += 1 + if op == "clear": + rows[target] = {} + elif op == "copy": + rows[target] = rows[reg(gate[2])].copy() + elif op == "scale": + rows[target] = {j: v * Q(gate[2], gate[3]) for j, v in rows[target].items()} + else: + need(op == "add", "Known scalar prefix operation") + for j, v in rows[reg(gate[2])].items(): + value = rows[target].get(j, 0) + Q(gate[3], gate[4]) * v + if value: + rows[target][j] = value + else: + rows[target].pop(j, None) + else: + raise ValueError("Missing centre cut") + R = [[rows[c].get(p, Q(0)) for p in range(112)] for c in word["centers"]] + need(len(R) == 8 and all(v.denominator == 1 for row in R for v in row), "Integer R") + columns = [tuple(int(R[k][p]) for k in range(8)) for p in range(112)] + check_grams(columns) + return columns, operations + + +def gram(columns): + return [[sum(v[i] * v[j] for v in columns) for j in range(8)] for i in range(8)] + + +def diagonal(value): + return [[value * int(i == j) for j in range(8)] for i in range(8)] + + +def check_grams(columns): + need(len(columns) == 112 and all(sum(v*v for v in c) == 4 for c in columns), "Norm-four ports") + need(gram(columns) == diagonal(56), "Full Gram 56I") + need(gram([columns[p] for p in A]) == diagonal(4), "A dyadic section") + need(gram([columns[p] for p in T]) == diagonal(4), "T dyadic section") + need(gram([columns[p] for p in U]) == diagonal(48), "Ordinary Gram 48I") + + +def act(columns, value): + result = 0 + while value: + low = value & -value + result ^= columns[low.bit_length() - 1] + value ^= low + return result + + +@lru_cache(maxsize=30000) +def multiply(left, right): + return tuple(act(left, column) for column in right) + + +def routes(local): + phases = local["DATA-PHASES.json"] + word = local["CANONICAL-WORD.json.gz"] + need(phases["m"] == 73 and len(phases["recipes"]) == 112, "Actual phase dimensions") + result = [] + for p, recipe in enumerate(phases["recipes"]): + basis = [recipe["q"]] + recipe["idle_children"][0]["orthogonal_axes"][:8] + need(recipe["port"] == p and basis[0] == word["ports"][p], "Port source binding") + need(all(0 < vector < 512 for vector in basis), "Local basis stays in nine coordinates") + need(all(((basis[i] & basis[j]).bit_count() % 2) == int(i == j) + for i in range(9) for j in range(9)), "Orthonormal local basis") + # Swap each local basis vector with its stage-one external axis. + # All remaining 56 coordinates are fixed, so this is the full map's + # faithful 17-coordinate restriction, not a quotient representation. + columns = [] + for axis in ID: + value = axis + for i, vector in enumerate(basis[1:]): + external = 1 << (9 + i) + if ((axis & vector).bit_count() + bool(axis & external)) % 2: + value ^= vector ^ external + columns.append(value) + route = tuple(columns) + need(multiply(route, route) == ID, "Actual route involution") + need(act(route, recipe["q"]) == recipe["q"], "Route fixes port normal") + need(all(act(route, basis[i + 1]) == 1 << (9 + i) for i in range(8)), "Exact stage-one exchange") + result.append(route) + need(len({result[p] for p in U}) == 96, "All ordinary stage-one routes distinct") + return result + + +def add_vector(table, key, values, scale=1): + row = table.setdefault(key, [0] * len(values)) + for i, value in enumerate(values): + row[i] += scale * value + + +def clean(table): + return {key: tuple(value) for key, value in table.items() if any(value)} + + +def witness(columns, route, coefficient=48, omit_projection=False): + # All eight e_k columns at once. Coefficients live in the actual finite + # matrix-group algebra; no enumeration of the enormous regular cover. + result = [] + for p in U: + row = {} + add_vector(row, ID, columns[p], coefficient) + if not omit_projection: + for q in U: + dot = sum(a*b for a, b in zip(columns[p], columns[q])) + if dot: + add_vector(row, multiply(route[p], route[q]), columns[q], -dot) + result.append(clean(row)) + return result + + +def apply_query(h, columns, route=None): + out = {} + for p, field in zip(U, h): + for owner, row in field.items(): + label = multiply(route[p], owner) if route is not None else owner + values = [columns[p][i] * row[k] for i in range(8) for k in range(8)] + add_vector(out, label, values) + return clean(out) + + +def rejected(action): + try: + action() + except ValueError: + return True + return False + + +def finite_loggers(): + """Every scalar A logger over F5 with two ordinary inputs: 500 cases.""" + prime, count, inverse_columns = 5, 0, 0 + for m in range(prime): + for n in range(prime): + if m == n: + continue + for l0 in range(prime): + for l1 in range(prime): + def source(x, inverse=False): + z0, z1, a, c = x + if not inverse: + f = z0 + a + c + return [(z0 - 12*f) % prime, z1, + (m*a + n*c + l0*z0 + l1*z1) % prime, f % prime] + w0, w1, d, f = x + z0, z1 = (w0 + 12*f) % prime, w1 + total = f - z0 + c = ((d - m*total - l0*z0 - l1*z1) * pow(n-m, -1, prime)) % prime + return [z0, z1, (total-c) % prime, c] + + def pair(state, inverse=False): + x, y = state[:4], state[4:] + output = source(x, inverse) + if inverse: + target = [(y[0]-x[0]) % prime, (y[1]-x[1]) % prime, + (x[2]+y[2]-output[2]) % prime, (x[3]+y[3]-output[3]) % prime] + else: + target = [(y[0]+output[0]) % prime, (y[1]+output[1]) % prime, + (x[2]+y[2]-output[2]) % prime, (x[3]+y[3]-output[3]) % prime] + return output + target + + for j in range(8): + basis = [int(i == j) for i in range(8)] + need(pair(pair(basis), True) == basis, "F5 left inverse on dirty data") + need(pair(pair(basis, True)) == basis, "F5 right inverse on dirty data") + inverse_columns += 2 + # B0=[1,0], B1=[0,1], B2=[1,1], h=(1,0). + post = [1, 0, 1, 0, 1, 0, -1 % prime, 0] + original = pair(post, True) + need(pair(original) == post, "Changed first logger pullback") + need((original[2]+original[3]) % prime == -1 % prime, "Required initial A+T nonzero") + need(original[4:6] == [0, 0], "Initial ordinary Y zero") + # Fixed conserved B1, future logger E2, all selected sections + # identity in this toy model. This is not a native fixture. + x, y = post[:4], post[4:] + q2 = sum(y) % prime + b1 = (y[1] + q2 + y[3]) % prime + driver = x[3] + yp = [y[0], (y[1]+12*driver) % prime, q2, + (y[3]-b1-11*driver) % prime] + xp = [(x[0]-y[0]) % prime, (x[1]-y[1]) % prime, + (x[2]+y[2]-yp[2]) % prime, (x[3]+y[3]-yp[3]) % prime] + need(xp+yp == [0, 0, 0, 0, 1, 0, 0, 0], "Fixed B1 erases every changed logger witness") + count += 1 + need(count == 500, "Complete F5 logger domain") + return {"field": 5, "loggers": count, "two_sided_dirty_basis_checks": inverse_columns, + "changed_logger_witnesses": count} + + +def matvec(matrix, vector): + return [sum((a*b for a, b in zip(row, vector)), Q(0)) for row in matrix] + + +def plus(*vectors): + return [sum(values, Q(0)) for values in zip(*vectors)] + + +def negative(vector): + return [-v for v in vector] + + +def ordered_fixture(): + # M,N do not commute. D=N-M has a two-sided rational inverse. + M = [[Q(1), Q(1)], [Q(0), Q(1)]] + N = [[Q(2), Q(1)], [Q(1), Q(3)]] + Dinv = [[Q(1), Q(0)], [Q(-1, 2), Q(1, 2)]] + L = [[Q(1), Q(2), Q(0), Q(-1)], [Q(0), Q(1), Q(3), Q(2)]] + need(matvec(M, matvec(N, [1, 0])) != matvec(N, matvec(M, [1, 0])), "Noncommuting fixture") + + def source(x, inverse=False): + z, a, c = x[:4], x[4:6], x[6:] + if not inverse: + f = plus(z[:2], a, c) + w = plus(z, [-12*f[0], -12*f[1], 0, 0]) + d = plus(matvec(M, a), matvec(N, c), matvec(L, z)) + return w+d+f + w, d, f = z, a, c + z = plus(w, [12*f[0], 12*f[1], 0, 0]) + total = plus(f, negative(z[:2])) + c = matvec(Dinv, plus(d, negative(matvec(M, total)), negative(matvec(L, z)))) + return z+plus(total, negative(c))+c + + for j in range(8): + e = [Q(int(i == j)) for i in range(8)] + need(source(source(e), True) == e, "Ordered logger left inverse") + need(source(source(e, True)) == e, "Ordered logger right inverse") + for k in range(2): + h = [Q(int(i == k)) for i in range(4)] + post = h+h[:2]+[Q(0), Q(0)] + old = source(post, True) + need(source(old) == post, "Noncommuting pullback") + need(plus(old[4:6], old[6:]) == negative(h[:2]), "Noncommuting initial selected sum") + return {"centre_dimension": 2, "ordinary_dimension": 4, + "noncommuting_M_N": True, "two_sided_source_basis_checks": 16, + "witnesses": 2} + + +def tail_receipt(data): + source = json.loads(data["research/joint-query/evidence/QQ16-SELECTED-WITNESS.json"]) + review = json.loads(data["research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.json"]) + # Replay only the restricted ordinary h-coefficient trajectory stated by + # the pinned witness, not the absent full controller or native bank program. + def run(omit_first_negative=False): + x, y, trace = [0]*4, [1, 0, 0, 0], [] + for event in source["trajectory_after_B1"]: + kind = event["kind"] + if kind == "bridge": + d, s, c = event["dst"], event["src"], event["coefficient"] + if not (omit_first_negative and d == 0 and s == 1 and c == -1): + x[d] += c*x[s] + y[s] -= c*y[d] + elif kind == "local": + stage = event["stage"] + if stage % 2 == 0: + need(not any(x), "Later F query source zero") + else: + need(y[stage//2] == 0, "Later B source zero") + else: + need(kind == "terminal", "Known tail event") + x, y = y, [-v for v in x] + combined = [v for pair in zip(x, y) for v in pair] + need(combined == event["ordinary"], "Inherited trajectory agreement") + trace.append({"kind": kind, "x_coefficients": x[:], "y_coefficients": y[:]}) + return trace + trace = run() + need(trace == review["tail_trace"], "Independent receipt agreement") + need(rejected(lambda: run(True)), "Missing cancelling bridge rejected") + return {"events": len(trace), "forward_queries_zero": [0, 2, 4, 6, 8], + "final_X_coefficients": trace[-1]["x_coefficients"], + "final_Y_coefficients": trace[-1]["y_coefficients"], + "scope": "Restricted inherited h trajectory; not a full controller/native replay"} + + +def verify(root): + data = authenticate(root) + local = archive_data(data[ARCHIVE]) + columns, scalar_prefix = query_columns(local) + route = routes(local) + h = witness(columns, route) + b1 = apply_query(h, columns, route) + b0 = apply_query(h, columns) + need(not b1, "Full group-ring B1 h vanishes") + need(b0[ID] == tuple(v for row in diagonal(2112) for v in row), "Full identity coefficient 2112I") + serialized = [[[list(g), list(v)] for g, v in sorted(field.items())] for field in h] + controls = {} + controls["omitted_projector_term"] = bool(apply_query(witness(columns, route, omit_projection=True), columns, route)) + controls["wrong_gram_coefficient"] = bool(apply_query(witness(columns, route, coefficient=47), columns, route)) + collapsed = [ID]*112 + controls["collapsed_routes_zero_witness"] = not any(witness(columns, collapsed)) + changed = columns[:] + changed[U[0]] = tuple(v + int(i == 0) for i, v in enumerate(changed[U[0]])) + controls["corrupted_query_gram"] = rejected(lambda: check_grams(changed)) + controls["extra_B0_observation_detects_witness"] = bool(b0) + need(all(controls.values()), "Every semantic control must discriminate") + invoice = json.loads(data["research/joint-query/evidence/CONSERVED-QQ16.json"]) + local_bill = {"native_mass": sum(invoice["invoices"][key]["native_mass"] for key in ("F", "B")), + "real_scalar_bound": sum(invoice["invoices"][key]["complete_scalar"]["real_primitives"] for key in ("F", "B")), + "added_cover_maps": invoice["native_cases"]["B_1_2"]["explicit_cover_maps"] + invoice["native_cases"]["F_0"]["explicit_cover_maps"], + "wrapper_maps": invoice["native_cases"]["B_1_2"]["native_wrapper_maps"] + invoice["native_cases"]["F_0"]["native_wrapper_maps"]} + need(local_bill == {"native_mass": 11076, "real_scalar_bound": 426196, + "added_cover_maps": 528, "wrapper_maps": 64}, "Retained pair invoice") + return {"status": "PASS_QQ16_FORWARD_LOGGER_OBSTRUCTION", + "query": {"source_scalar_prefix_operations": scalar_prefix, + "columns": 112, "ordinary_columns": 96, "gram": 48, + "query_columns_sha256": digest(columns), "stage_one_routes_sha256": digest(route), + "distinct_ordinary_routes": len({route[p] for p in U})}, + "witness": {"definition": "(48I-B1*B1)B0*e_k", "independent_directions": 8, + "ordinary_field_group_terms": sum(map(len, h)), + "canonical_group_ring_sha256": digest(serialized), + "B1_h_nonzero_terms": len(b1), "B0_h_group_terms": len(b0), + "B0_h_identity_coefficient": diagonal(2112)}, + "finite_logger_fixture": finite_loggers(), "ordered_fixture": ordered_fixture(), + "tail": tail_receipt(data), "semantic_controls": controls, + "retained_pair_bill": local_bill, + "result": "Every invertible source F0 logger with fixed U/T outputs and conserved selected pair sums fails selected restoration under fixed B1 and the retained observation/tail contract, even with zero added logger cost.", + "limits": ["No arbitrary-first-pair obstruction", "No lower bound on paid ordinary reads", + "No native logger synthesis or supplier admission", "No new kappa or formal-kernel proof"]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=ROOT) + parser.add_argument("--emit", type=Path, help="Write a fresh result; refuses existing paths") + args = parser.parse_args() + result = verify(args.repo.resolve()) + if args.emit: + with args.emit.open("x") as output: + json.dump(result, output, indent=2, sort_keys=True) + output.write("\n") + else: + need(canonical(result) == canonical(json.loads((PACKAGE / "RESULT.json").read_text())), "Complete canonical RESULT mismatch") + print(result["status"]) + print("96 distinct routes; 8 B0/B1 witnesses; 500 changed loggers; no new kappa") + + +if __name__ == "__main__": + main()