diff --git a/research/qq16-b2-observation-kernel/README.md b/research/qq16-b2-observation-kernel/README.md new file mode 100644 index 0000000000..15f6707f8c --- /dev/null +++ b/research/qq16-b2-observation-kernel/README.md @@ -0,0 +1,276 @@ +# A QQ16 kernel invisible to every nonzero-chart source query + +## Result and relevance + +For the actual QQ16 first `F0/B1` pair and retained ordinary schedule, adding +an exact pre-`F0` observation **`B2 X_U` does not suffice to recover the original +selected A input**. A three-port input has + +``` +B1 h = B2 h = 0, B0 h != 0. +``` + +All selected endpoints, all completed-X descendants, all five forward-query +histories, and the added `B2 X_U` observation agree with the zero input. The +required original `X_A` does not. This is an exact indistinguishability result, +not a failed search. Even an arbitrary decoder cannot distinguish these inputs +from that observation set. + +In fact this same `h` has `B_s h=0` for **every `1 <= s <= 8`**. Granting every +nonzero-chart pre-read of this ordinary source still leaves the obstruction. +The eight chart queries are different from eight scalar output coordinates of +one query. Neither statement rules out an old-chart `B0` read, a different +observation, or a change to the first pair. + +This addresses revision 4's concrete missing controller interface without +repeating a selected-root computation. It provides no complete QQ16 supplier, +new exponent, native read implementation, or formal-kernel theorem. + +## What is new relative to the sources + +Ali Romman's [PR1969](https://github.com/CrocSwap/integer-mult-bounds/pull/1969), +retained in [`research/joint-query`](../joint-query/README.md), supplies the +ordered local maps, actual routes, and native local invoices. Its +[selected witness](../joint-query/evidence/QQ16-SELECTED-WITNESS.md) and +[independent rational review](../joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md) +already give eight missing directions with `B1 h=0` and `B2 h!=0`. Their +selected-only obstruction is not claimed as new here. + +[Cinna Davis / PR2079](https://github.com/CrocSwap/integer-mult-bounds/pull/2079), +head `49df8190b158e3028e702b2c6b798117006f7249`, formalizes the +[discussion 2074](https://github.com/CrocSwap/integer-mult-bounds/discussions/2074) +proposal `B2 X_U` and tests it against those eight directions. Its +[pinned proof](https://github.com/CrocSwap/integer-mult-bounds/blob/49df8190b158e3028e702b2c6b798117006f7249/research/joint-query-extra-b2-observation-seed3e62/README.md) +explicitly leaves full-controller injectivity open. Detecting that family is not +the same as recovering all initial selected inputs. The new witness instead +lies in the kernel of the **expanded** observation set and loses initial **A**, +not the predecessor's initial T. It answers PR2079's second open question for +this fixed first pair, without contradicting its restricted detection result. + +Existing scalar/native/ordered reviews are reused as source contracts, not +called independent by importing their checkers. This verifier imports no +predecessor Python code. It reconstructs R from original scalar operations, +reconstructs the owner routes from the actual phase axes, applies the ordered +maps to explicit functions on owners, and replays the source template's tail. + +## Actual source and observation model + +Use the actual 8-by-112 centre matrix R, with + +``` +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). +``` + +For owner `d`, let `rho_s(p)` be the actual stage-s owner involution at port +p; stage zero is the identity. The ordinary query is + +``` +(B_s h)(d) = sum_(p in U) r_p h_p(d rho_s(p)), +``` + +where `r_p` is column p of R. The eight local chart axes `b_(p,i)` lie in the +initial 9-dimensional block. The phase source explicitly gives + +``` +rho_s(p) b_(p,i) = e_(9 + 8(s-1) + i), 1 <= s <= 8. +``` + +These are **owner routes**, not payload permutations. Inputs below are +constant in every payload coordinate but vary with the owner. They are valid +at every positive tensor size. Native payload translations and endpoint line +operators fix these constant payloads; this is not an assumption that the +owner array is constant. + +The first pair and ordinary schedule are fixed. Subsequent homogeneous +selected-only linear controls may be arbitrary, including cross-bank, +port and cover maps. They do not read ordinary banks. The extra observation +is retained as a record; it does not rewrite the first pair. Later controls +may use it, because it is zero on the entire counterexample trajectory. + +## Explicit three-port witness + +The reconstructed columns satisfy + +``` +r_2 = (1, 1, 0, 0, 0, 0, 1, -1) +r_8 = (0, 1, 0, -1, 1, 0, 1, 0) +r_85 = (1, 0, 0, 1, -1, 0, 0, -1) +r_2 = r_8 + r_85. +``` + +The actual first local axes, as binary masks, are + +``` +b_(2,0)=37, b_(8,0)=38, b_(85,0)=506. +``` + +Let `f_v(d)=bit_0(d v)`, with the binary bit interpreted as the integer zero +or one. Define + +``` +h_2(d) = -f_37(d), +h_8(d) = f_38(d), +h_85(d) = f_506(d), +h_p(d) = 0 otherwise. +``` + +For every owner d and every `s=1,...,8`, the common-axis identity gives + +``` +(B_s h)(d) = (-r_2+r_8+r_85) bit_0(d e_(9+8(s-1))) = 0. +``` + +This is an all-owner algebraic identity; it is not an enumeration of a few +cover representatives. At the identity owner, only mask 37 has low bit one, +so + +``` +(B0 h)(I) = -r_2 = (-1,-1,0,0,0,0,-1,1) != 0. +``` + +The formal sparse-function representation used by the checker need not assume +that all `f_v` are linearly independent on the cover. Cancellation of the +formal sum is sufficient for zero; evaluation at the actual identity owner +is sufficient for nonzero. + +## Ordered first-pair trajectory + +Let `P_(s,A)` be the actual selected section, so +`ell_(s,A) P_(s,A)=I`. Set every bank except pair zero to zero and set + +``` +X_U=h, Y_U=0, +X_A=-P_(0,A) B0 h, Y_A=-X_A, +X_T=0, Y_T=0. +``` + +Both selected pair sums are zero. At the identity owner the required initial +A values, in the displayed A order, are + +``` +(1/2, 0, 1/2, 1/2, 0, -1/2, 0, 0). +``` + +The initial full query is `f0=B0h+ell_(0,A)X_A=0`. The exact forward map +therefore yields + +``` +X_U=Y_U=h, X_A=Y_A=X_T=Y_T=0. +``` + +The backward future query is `q2=B2h=0`, so its systematic future logger +leaves `u=(h,0,0)`. The old T driver is `a=0`, and `b=B1h=0`. Substituting in +the conserved backward formulas gives + +``` +Y_0,U=h, every other field zero. +``` + +No operator factors have been commuted. The extra pre-`F0` read was +`B2 X_U=B2h=0`, so the new record is identical to the zero-input record. + +## All remaining observations + +The retained positive ordinary bridge `(dst,src)=(0,1)` places `-h` in +`Y_1,U`. `F2` acts on pair zero with zero X source and does not change the +state. The negative bridge removes `-h` before `B3`. Every subsequent active +pair is zero. The final three bridges leave only `Y_0,U=h`. All five forward +queries `f0,f2,f4,f6,f8` are zero. + +All selected states after the first pair are zero. Every later homogeneous +selected-only map, including maps that use the added zero record, preserves +that fact. Thus the argument does not depend on a particular selected-only +controller. + +The terminal signed exchange moves h to **named final `X_0,U`, with the +old-Y native type**. It is not a completed-X descendant. Every completed-X +descendant is zero. Mistaking the named final X array for an available +completed-X observation would invalidate the observation contract; a +negative control deliberately makes that mistake and rejects it. + +The checker reconstructs the original template's `recipe` and binds its +stage/pair/orientation records to the hosted calls. It replays its ordinary +bridges and the actual ordered F/B formulas, and matches the complete retained +witness tail receipt. Ignored idle/frame sweeps preserve logical contents; +all payload operations fix the constant payloads used here. A new full native +supplier replay is not claimed. + +## Complete favorable budget and stopping decision + +This is a functionality obstruction, not a native-cost lower bound. Before +synthesis, grant the proposed B2 extraction, eight output coordinates, source +access, owner/address maps, storage, restoration, endpoint conversion, +chronological hosting and precision **zero added cost**. Even that favorable +completed observation model cannot recover the required A input. + +For orientation, the retained local F and B words have rank masses 5530 and +5546, respectively. Their first-pair mass is 11076. If an additional rank-8 +record were separately charged, those local masses would become 5554 for B +and 11084 for the pair, before any other nonnegative costs. This is a +hypothetical output charge, not a demonstrated native read or a physical +lower bound. No completed recursive moment exists for the failed recovery +proposal, so there is no justified new moment root to compute. More payment +for the same observation cannot remove its information kernel. Feedback +that changes the first pair is outside this test. + +## Reproduction and evidence + +Standard-library CPython 3.12, no network and no predecessor imports: + +```sh +uv run --python 3.12 --no-project python -I -O -B research/qq16-b2-observation-kernel/verify.py +uv run --python 3.12 --no-project python -B scripts/research_package.py --package research/qq16-b2-observation-kernel +``` + +The direct command requires the committed `RESULT.json`, regenerates every +proof-relevant result in memory, and compares the complete canonical JSON +payload. It authenticates all source bytes before parsing the archive or +certificate. `--emit-result NEW_PATH` explicitly creates an external receipt +and refuses to overwrite an existing file. Compression/container hashes are +only immutable-source authentication, not regenerated mathematical equality. + +Expected status: `PASS_QQ16_B2_OBSERVATION_KERNEL`. Eight controls reject changed +dependency coefficients, a changed chart axis, omitted A cancellation, a +missing negative bridge, endpoint type confusion, replacement of the new +read by a detecting B0 read, payload-only routing and altered source bytes. +The B0 control confirms an escape for this witness, not sufficiency of B0 +for the whole controller. + +`SELECTION.json` preserves the single independent chooser draw, seed +`20e7cbb51ab8b49eac12de2f825e100a`, track `independent-verification`. +Scientific base: `564148b82ae9df72163f22106f15e73efca8aff2`, priority revision 4. +Exact input Git blobs and SHA256 pins are in `SOURCES.json`; archive member +pins and the full observation trajectory are in `RESULT.json`. The selected +record and all frozen predecessors are unchanged. The required binding-only +working example passed; this does not imply a selected full cold replay. + +## Open next questions + +1. **Does B0 together with B2 and the retained observations recover the full + fixed-pair selected-input kernel?** This witness proves that B0 detects one + missing component, not a complete repair. First derive the entire ordered + kernel and compare the augmented observation map. Actual native frame access + and a complete physical invoice remain blockers. +2. **Can a changed first pair retain both old-chart components cheaply?** Write + its arbitrary-input identity and fully priced output/restoration contract + before synthesis. The present first pair is fixed; the result is not a + universal obstruction to changed controllers or other ordinary reads. + +## Attribution and limits + +Ali Romman and the credited supplier lineage provide PR1969's local QQ16 +maps, actual routes, retained tail and independent reviews. The selected +gauge44/t16 sources retain icekylinx's contributions, chafreaky's frame work +and their earlier supplier lineage; see the unchanged +[source notices](../joint-query/NOTICE.md). Cinna Davis / `1337isnot1337` +supplies PR2079's explicit B2 pre-read +and bounded old-witness separation result; this audit answers its stated +full-kernel question. + +The new three-port kernel, expanded-observation proof and independent checker +were prepared for Adam Gall with substantial OpenAI Codex assistance. +Apache-2.0. No independent human review, formal-kernel run, complete physical +read, all-size compiler admission, selected supplier replay, hosted-CI pass, +or literature-priority guarantee is claimed. diff --git a/research/qq16-b2-observation-kernel/RESULT.json b/research/qq16-b2-observation-kernel/RESULT.json new file mode 100644 index 0000000000..4f4770072f --- /dev/null +++ b/research/qq16-b2-observation-kernel/RESULT.json @@ -0,0 +1,344 @@ +{ + "archive_members": { + "slots/local/CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "slots/local/LOCAL-PROGRAMS.json.gz": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "observation_audit": { + "B0_h_at_identity": [ + "-1", + "-1", + "0", + "0", + "0", + "0", + "-1", + "1" + ], + "required_initial_X_A_at_identity": [ + "1/2", + "0", + "1/2", + "1/2", + "0", + "-1/2", + "0", + "0" + ], + "surviving_unobserved_endpoint": "final X0_U=h, with old-Y native type", + "tail_trajectory": [ + { + "coefficient": 1, + "dst": 0, + "kind": "bridge", + "ordinary": [ + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 0 + ], + "src": 1 + }, + { + "kind": "local", + "ordinary": [ + 0, + 1, + 0, + -1, + 0, + 0, + 0, + 0 + ], + "stage": 2 + }, + { + "coefficient": -1, + "dst": 0, + "kind": "bridge", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "src": 1 + }, + { + "kind": "local", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 3 + }, + { + "coefficient": 1, + "dst": 1, + "kind": "bridge", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "src": 2 + }, + { + "kind": "local", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 4 + }, + { + "coefficient": -1, + "dst": 1, + "kind": "bridge", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "src": 2 + }, + { + "kind": "local", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 5 + }, + { + "coefficient": 1, + "dst": 2, + "kind": "bridge", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "src": 3 + }, + { + "kind": "local", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 6 + }, + { + "coefficient": -1, + "dst": 2, + "kind": "bridge", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "src": 3 + }, + { + "kind": "local", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 7 + }, + { + "kind": "local", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "stage": 8 + }, + { + "coefficient": 1, + "dst": 3, + "kind": "bridge", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "src": 2 + }, + { + "coefficient": 1, + "dst": 2, + "kind": "bridge", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "src": 1 + }, + { + "coefficient": 1, + "dst": 1, + "kind": "bridge", + "ordinary": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "src": 0 + }, + { + "kind": "terminal", + "ordinary": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + ], + "zero_observations": [ + "all selected endpoints", + "all completed-X descendants", + "f0", + "f2", + "f4", + "f6", + "f8", + "pre-F0 B2 X_U" + ] + }, + "proof_inputs": { + "research/community-frontier1042-audit/selected-replay.tar.gz": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "research/joint-query/certificate.json.gz": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/joint-query/evidence/BRIDGE-REVIEW.md": "d01b5f4959f7c91f835496d050dfae3eeab9dee2f581571c316a42571eaa1cd3", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75", + "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md": "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md": "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc" + }, + "rejecting_controls": [ + "changed dependency coefficient", + "changed chart axis", + "missing initial A cancellation", + "missing first negative bridge", + "old-Y endpoint mislabeled as completed-X", + "B0 observation detects this witness", + "owner action replaced by payload-only action", + "source-byte mutation" + ], + "schema": "qq16-b2-observation-kernel-v1", + "scope": "Fixed first pair and ordinary schedule; exact B2 pre-read added. No changed feedback, native read, supplier, new kappa, or formal-kernel claim.", + "source_R_sha256": "70055070e6f0465dcb9f99773769809f032043e7a1cba4f0c0fe5e5c365f0213", + "status": "PASS_QQ16_B2_OBSERVATION_KERNEL", + "witness": { + "axes": { + "2": 37, + "8": 38, + "85": 506 + }, + "coefficients": { + "2": -1, + "8": 1, + "85": 1 + }, + "definition": "h_p(d)=c_p bit_0(d b_(p,0)), constant in every payload coordinate", + "vanishing_stages": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ] + } +} diff --git a/research/qq16-b2-observation-kernel/SELECTION.json b/research/qq16-b2-observation-kernel/SELECTION.json new file mode 100644 index 0000000000..6d514b9455 --- /dev/null +++ b/research/qq16-b2-observation-kernel/SELECTION.json @@ -0,0 +1,60 @@ +{ + "seed": "20e7cbb51ab8b49eac12de2f825e100a", + "track": "independent-verification", + "suggestions": [ + { + "task_id": "independent-moment", + "scope_key": "c6f2494b197df3bc3591", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "method": "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "starting_points": ["certificates/selected-result.json"], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": ["python3", "-B", "scripts/research_baseline.py"], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "List the existing independent checks for the exact selected or candidate sources. Pick a new changed input, missing binding or distinct failure mode; stop with a handoff if the proposed arithmetic check is already covered.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": ["Reconstruct either a source ledger or a numeric enclosure with a different method."], + "scope_change_triggers": ["Importing the primary function and calling its output independent verification."], + "overlap_terms": ["independent moment", "rank histogram", "exact enclosure"], + "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": "formal-interface-lemma", + "scope_key": "e3ffea67887eeb4c396c", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "method": "Audit a formal theorem-to-certificate binding independently.", + "starting_points": ["certificates/selected-result.json", "research/hyperplane-end-lean/PROOF.md"], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": ["python3", "-B", "scripts/research_baseline.py"], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": ["Narrow to one formal lemma or one theorem-to-certificate binding."], + "scope_change_triggers": ["Formalizing already-covered arithmetic and claiming the full multiplication theorem."], + "overlap_terms": ["hyperplane end", "formal interface", "Lean binding"], + "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-b2-observation-kernel/SOURCES.json b/research/qq16-b2-observation-kernel/SOURCES.json new file mode 100644 index 0000000000..50d83b201a --- /dev/null +++ b/research/qq16-b2-observation-kernel/SOURCES.json @@ -0,0 +1,60 @@ +{ + "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/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "usage": "input", + "git_blob": "c6ecf75654a084a9cc001bd62663f341976bae7a", + "sha256": "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "usage": "input", + "git_blob": "307650f45e37c28d14fe913958efa4fb429242b7", + "sha256": "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "usage": "input", + "git_blob": "5082d791d0b993492cbc5bf61ac3b69e82c96f3f", + "sha256": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4" + }, + { + "path": "research/joint-query/evidence/BRIDGE-REVIEW.md", + "usage": "input", + "git_blob": "86139908c418235588045324f0873de6ac9f9707", + "sha256": "d01b5f4959f7c91f835496d050dfae3eeab9dee2f581571c316a42571eaa1cd3" + } + ] +} diff --git a/research/qq16-b2-observation-kernel/TASK.json b/research/qq16-b2-observation-kernel/TASK.json new file mode 100644 index 0000000000..1076993922 --- /dev/null +++ b/research/qq16-b2-observation-kernel/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 4, + "base_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "List the existing independent checks for the exact selected or candidate sources. Pick a new changed input, missing binding or distinct failure mode; stop with a handoff if the proposed arithmetic check is already covered.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "changed", + "actual_scope": "At the fixed QQ16 F0/B1 cut, grant the exact pre-F0 read B2 X_U in addition to all selected outputs, completed-X descendants and five forward-query histories. Determine whether this expanded observation set restores BOTH initial selected blocks. Seek an explicit actual-route kernel with B1 h=B2 h=0 but B0 h nonzero; do not repeat the predecessor's already checked eight B2 directions.", + "scope_change_reason": "Priority revision 4 names changed QQ16 observations as a central missing interface. This independent-verification assignment changes from rank-ledger or root arithmetic to the unproved implication that detecting the old B2 witness repairs selected-input recovery. Existing QQ16 scalar, native and rational-observation reviews do not audit this expanded observation set. Cinna Davis's PR2079, exact head49df8190b158e3028e702b2c6b798117006f7249, proposes B2 X_U and tests the old eight directions while explicitly leaving full injectivity open; this audit supplies a new kernel answering that open question for the fixed first pair.", + "bottleneck_link": "A controller that detects one known witness may still discard other required selected data. An exact expanded-observation counterexample stops an incomplete paid query from being promoted to a supplier, before spending effort on native hosting.", + "budget_minutes": 60, + "stop_rule": "Finish one explicit source-bound kernel or exact reconstruction, verify the ordered first pair and retained tail, and stop before synthesizing another controller. Do not claim a universal obstruction, a complete native read, a supplier or a new exponent.", + "outcome": "negative-result", + "result": "Exact expanded-observation obstruction: the three ports 2,8,85 have coefficients -1,1,1 and first local axes 37,38,506. Their common-axis query images cancel in every nonzero chart, but B0 at the identity is -r2, giving a nonzero original selected A input and zero expanded observations.", + "evidence": "verify.py independently reconstructs R, all actual owner routes and the full ordered trajectory from authenticated sources; RESULT.json is a canonical replay receipt with eight rejecting controls. README.md gives the all-owner proof. Required research_baseline.py first working example passed.", + "author": "Adam Gall with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in research, proof, implementation and verification; no independent human or formal-kernel review claimed.", + "seed": "20e7cbb51ab8b49eac12de2f825e100a", + "track": "independent-verification", + "method": "Reconstruct actual R from original scalar operations and local axes from DATA-PHASES. Use h_p(d)=c_p bit_0(d b_(p,0)) with Rc=0. Actual routes send b_(p,0) to a stage-specific common axis independently of p, proving all eight nonzero-stage queries vanish at every owner. Evaluate B0 at the identity to certify nonzero. Independently replay the ordered first pair and original hosted-template tail.", + "domain": "Actual 112-port QQ16 source, the fixed 16 selected ports and 96 ordinary ports, exact integer/rational coefficients, arbitrary regular-cover values constant in payload coordinates, fixed F0/B1 and ordinary tail, arbitrary later homogeneous selected-only linear maps. The added B2 read is retained as an external observation, not fed back to change the first pair.", + "optimistic_complete_bill": "For this sufficiency audit grant B2 extraction, all eight output coordinates, read maps, temporary storage, restoration, endpoints, hosting and precision at zero additional cost. Even this maximally favorable complete observation budget must pass functionality. Retained B1 native mass is 5546; an optimistic separately paid rank-8 record would make 5554 before nonnegative physical charges, but no physical realization or improved moment is assumed. Stop on a kernel witness independently of cost.", + "source_scope": "Scientific main 564148b82ae9df72163f22106f15e73efca8aff2, priority4; merged Ali Romman PR1969 and its selected source archive. Pending PR2079 is read at immutable head49df8190b158e3028e702b2c6b798117006f7249, but its code is neither imported nor used as a theorem premise. No posts or comments.", + "freshness": { + "checked_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "checked_priority_revision": 4, + "shared_overlap_checked_at": "2026-10-14T19:02:09Z", + "coverage": "Complete parent-refreshed snapshot of 353 open PRs including drafts, 738 discussion/comment/reply records, and 1536 local records. Targeted live PR2079 and immutable README read; head confirmed49df8190b158e3028e702b2c6b798117006f7249. New main changes guidance only; catalogue and scientific inputs unchanged. Updated guidance was read and the original scientific base retained. No absence/novelty guarantee." + }, + "open_questions": [ + { + "question": "Does a B0 observation, together with B2 and the retained observations, recover the full fixed-pair selected-input kernel?", + "why_it_matters": "A replacement controller needs recovery of every required selected input, not just detection of one witness.", + "first_step": "Derive the full first-pair kernel and compare it with the augmented B0/B2 observation map before native synthesis.", + "blocked_by": "Actual-route kernel characterization and a fully paid implementation remain separate obligations." + }, + { + "question": "Can a changed first pair preserve both independent old-chart query components at favorable cost?", + "why_it_matters": "The present audit keeps the first pair fixed and therefore cannot decide changed-controller viability.", + "first_step": "Write the ordered first-pair identity and complete optimistic invoice, including helper and endpoint restoration.", + "blocked_by": "No changed first-pair word or hosting certificate is supplied here." + } + ] +} diff --git a/research/qq16-b2-observation-kernel/VERIFY.json b/research/qq16-b2-observation-kernel/VERIFY.json new file mode 100644 index 0000000000..c0ff595870 --- /dev/null +++ b/research/qq16-b2-observation-kernel/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "research/joint-query/evidence/BRIDGE-REVIEW.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate original sources; reconstruct R, actual owner routes and the three-port kernel; replay every ordered local call and ordinary tail event; compare canonical receipt; reject eight semantic/source controls." + } + ] +} diff --git a/research/qq16-b2-observation-kernel/verify.py b/research/qq16-b2-observation-kernel/verify.py new file mode 100755 index 0000000000..bc07d47ddf --- /dev/null +++ b/research/qq16-b2-observation-kernel/verify.py @@ -0,0 +1,403 @@ +#!/usr/bin/env python3 +"""Exact, producer-independent QQ16 expanded-observation counterexample. + +Sparse functions represent finite sums of f_v(d) = bit_0(d v). A zero +formal sum is zero at every owner; nonzeroness is witnessed at d = I. +No predecessor Python code is imported or executed. Apache-2.0. +Prepared for Adam Gall with substantial OpenAI Codex assistance. +""" + +import argparse +from fractions import Fraction as Q +import gzip +from hashlib import sha256 +from io import BytesIO +import json +from pathlib import Path +import tarfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +CERTIFICATE = "research/joint-query/certificate.json.gz" +EVIDENCE = "research/joint-query/evidence/" +INPUTS = { + ARCHIVE: "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + CERTIFICATE: "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + EVIDENCE + "JOINT-QUERY-TRANSFER.md": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75", + EVIDENCE + "QQ16-RATIONAL-OBSERVATION-REVIEW.md": "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49", + EVIDENCE + "QQ16-SELECTED-WITNESS.md": "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc", + EVIDENCE + "QQ16-SELECTED-WITNESS.json": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4", + EVIDENCE + "BRIDGE-REVIEW.md": "d01b5f4959f7c91f835496d050dfae3eeab9dee2f581571c316a42571eaa1cd3", +} +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", + "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", +} +A = (0, 7, 20, 27, 36, 46, 57, 111) +T = (21, 37, 47, 76, 81, 87, 92, 110) +U = tuple(p for p in range(112) if p not in A + T) +COEFFICIENTS = {2: -1, 8: 1, 85: 1} +AXES = tuple(1 << j for j in range(73)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(raw, expected, name): + require(sha256(raw).hexdigest() == expected, "source hash: " + name) + return raw + + +def load_sources(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + require({row["path"]: row["sha256"] for row in manifest["files"] + if row["usage"] == "input"} == INPUTS, "manifest input pins") + raw = {name: authenticate((ROOT / name).read_bytes(), pin, name) + for name, pin in INPUTS.items()} + members = {} + with tarfile.open(fileobj=BytesIO(raw[ARCHIVE]), mode="r:gz") as archive: + for name, pin in MEMBERS.items(): + matches = [m for m in archive.getmembers() if m.name == name] + require(len(matches) == 1 and matches[0].isfile(), "unique member: " + name) + payload = authenticate(archive.extractfile(matches[0]).read(), pin, name) + if name.endswith(".gz"): + payload = gzip.decompress(payload) + members[name.rsplit("/", 1)[-1]] = json.loads(payload) + certificate = json.loads(gzip.decompress(raw[CERTIFICATE])) + previous = json.loads(raw[EVIDENCE + "QQ16-SELECTED-WITNESS.json"]) + return members, certificate, previous + + +def linear(*terms): + """Exact sum of (scalar, sparse row/function) terms, with zero removal.""" + result = {} + for coefficient, row in terms: + for key, value in row.items(): + result[key] = result.get(key, Q(0)) + coefficient * value + return {key: value for key, value in result.items() if value} + + +def reconstruct_R(word, programs): + require((word["v"], word["R"], word["h"]) == (112, 480, 9), "selected geometry") + # Project the original scalar operations to the 112 source input columns. + rows = [{p: Q(1)} if p < 112 else {} for p in range(712)] + reached = False + for event in programs["forward"]: + if event == ["phase", "centers"]: + reached = True + break + if event[0] != "scalar": + continue + op = event[1] + target = op[1][1] + (704 if op[1][0] == "C" else 0) + if op[0] == "clear": + rows[target] = {} + elif op[0] == "scale": + rows[target] = linear((Q(op[2], op[3]), rows[target])) + else: + require(op[0] in ("add", "copy"), "original scalar alphabet") + source = op[2][1] + (704 if op[2][0] == "C" else 0) + rows[target] = (rows[source].copy() if op[0] == "copy" else + linear((1, rows[target]), (Q(op[3], op[4]), rows[source]))) + require(reached, "source centre cut") + return [[rows[c].get(p, Q(0)) for p in range(112)] for c in word["centers"]] + + +def inverse(matrix): + n = len(matrix) + rows = [list(row) + [Q(i == j) for j in range(n)] for i, row in enumerate(matrix)] + for col in range(n): + pivot = next((i for i in range(col, n) if rows[i][col]), None) + require(pivot is not None, "selected minor invertibility") + rows[col], rows[pivot] = rows[pivot], rows[col] + divisor = rows[col][col] + rows[col] = [x / divisor for x in rows[col]] + for i in range(n): + if i != col: + factor = rows[i][col] + rows[i] = [x - factor * y for x, y in zip(rows[i], rows[col])] + return [row[n:] for row in rows] + + +def binary_action(columns, vector): + result = 0 + while vector: + bit = vector & -vector + result ^= columns[bit.bit_length() - 1] + vector ^= bit + return result + + +def route_axis(basis, stage, vector): + if stage == 0: + return vector + for i, axis in enumerate(basis): + swap = axis ^ AXES[9 + 8 * (stage - 1) + i] + if (vector & swap).bit_count() % 2: + vector ^= swap + return vector + + +class Model: + def __init__(self, R, phases, ignore_owner=False): + self.R = R + self.bases = [tuple(row["idle_children"][0]["orthogonal_axes"][:8]) + for row in phases["recipes"]] + self.inverses = {ports: inverse([[R[k][p] for p in ports] for k in range(8)]) + for ports in (A, T)} + self.routes = [] + require(phases["m"] == 73 and len(self.bases) == 112, "actual phase geometry") + for p, (basis, record) in enumerate(zip(self.bases, phases["recipes"])): + local = (record["q"],) + basis + require(record["port"] == p and all(0 < v < (1 << 9) for v in local), + "actual first-block chart") + require(all((local[i] & local[j]).bit_count() % 2 == (i == j) + for i in range(9) for j in range(9)), "orthonormal chart") + routes = [] + for stage in range(9): + columns = tuple(route_axis(basis, stage, v) for v in AXES) + require(all(binary_action(columns, column) == AXES[i] + for i, column in enumerate(columns)), "route involution") + if stage: + require(all(binary_action(columns, basis[i]) == AXES[9 + 8 * (stage - 1) + i] + for i in range(8)), "actual common-axis image") + routes.append(AXES if ignore_owner else columns) + self.routes.append(routes) + + def move(self, stage, port, function): + return linear(*((value, {binary_action(self.routes[port][stage], axis): Q(1)}) + for axis, value in function.items())) + + def query(self, stage, fields, ports=tuple(range(112))): + return [linear(*((self.R[k][p], self.move(stage, p, fields[p])) for p in ports)) + for k in range(8)] + + def inject(self, stage, ports, query): + result = [{} for _ in range(112)] + for i, p in enumerate(ports): + result[p] = self.move(stage, p, linear(*((self.inverses[ports][i][k], query[k]) + for k in range(8)))) + return result + + def ordinary_response(self, stage, query): + result = [{} for _ in range(112)] + for p in U: + result[p] = self.move(stage, p, linear(*((self.R[k][p] / 4, query[k]) + for k in range(8)))) + return result + + def forward(self, stage, x, y): + f = self.query(stage, x) + selected = self.query(stage, x, T) + response = self.ordinary_response(stage, f) + xa, xt = self.inject(stage, A, selected), self.inject(stage, T, f) + out_x, out_y = [{} for _ in range(112)], [{} for _ in range(112)] + for p in U: + out_x[p] = linear((1, x[p]), (-1, response[p])) + out_y[p] = linear((1, y[p]), (1, out_x[p])) + for p in A + T: + out_x[p] = xa[p] if p in A else xt[p] + out_y[p] = linear((1, x[p]), (1, y[p]), (-1, out_x[p])) + return out_x, out_y, f + + def backward(self, stage, future, x, y): + ua = self.inject(future, A, self.query(future, y)) + u = [ua[p] if p in A else y[p].copy() for p in range(112)] + a, b = self.query(stage, x, T), self.query(stage, u) + response = self.ordinary_response(stage, a) + xt = self.inject(stage, T, [linear((1, b[k]), (12, a[k])) for k in range(8)]) + subtract = self.inject(stage, T, [linear((1, b[k]), (11, a[k])) for k in range(8)]) + out_x, out_y = [{} for _ in range(112)], [{} for _ in range(112)] + for p in U: + out_x[p] = linear((1, x[p]), (-1, y[p])) + out_y[p] = linear((1, y[p]), (1, response[p])) + for p in A: + out_x[p] = linear((1, x[p]), (1, y[p]), (-1, u[p])) + out_y[p] = u[p] + for p in T: + out_x[p], out_y[p] = xt[p], linear((1, u[p]), (-1, subtract[p])) + return out_x, out_y + + +def at_identity(function): + return sum(coefficient * (axis & 1) for axis, coefficient in function.items()) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def experiment(model, template, previous, coefficients=None, axis_mutation=False, + omit_initial_correction=False, omit_minus=False, wrong_endpoint=False, + extra_stage=2): + coefficients = COEFFICIENTS if coefficients is None else coefficients + h = [{} for _ in range(112)] + for p, c in coefficients.items(): + axis_index = 1 if axis_mutation and p == 2 else 0 + h[p] = {model.bases[p][axis_index]: Q(c)} + b0 = model.query(0, h) + require(any(at_identity(row) for row in b0), "nonzero B0 at identity") + require(not any(model.query(1, h)), "B1 kernel") + require(not any(model.query(extra_stage, h)), "extra observation kernel") + initial_a = model.inject(0, A, b0) + x, y = h.copy(), [{} for _ in range(112)] + for p in A: + x[p] = {} if omit_initial_correction else linear((-1, initial_a[p])) + y[p] = linear((-1, x[p])) + required_input = [str(at_identity(x[p])) for p in A] + require(any(at_identity(x[p]) for p in A), "nonzero required original A") + x, y, f0 = model.forward(0, x, y) + require(not any(f0), "zero f0") + require(all(not x[p] and not y[p] for p in A + T), "selected zero after F0") + x, y = model.backward(1, 2, x, y) + require(not any(x) and y == h, "exact first-pair output") + banks = [[x, y]] + [[[{ } for _ in range(112)], [{ } for _ in range(112)]] for _ in range(3)] + histories = {0: f0} + trajectory = [] + recipe = template["recipe"] + require(recipe[:2] == [{"kind": "local", "pair": 0, "reverse": False, "stage": 0}, + {"kind": "local", "pair": 0, "reverse": True, "stage": 1}], + "fixed first pair") + for event in recipe[2:]: + if omit_minus and event == {"kind": "bridge", "src": 1, "dst": 0, "coefficient": -1}: + continue + kind = event["kind"] + if kind == "bridge": + src, dst, c = event["src"], event["dst"], event["coefficient"] + for p in U: + banks[dst][0][p] = linear((1, banks[dst][0][p]), (c, banks[src][0][p])) + banks[src][1][p] = linear((1, banks[src][1][p]), (-c, banks[dst][1][p])) + record = dict(event) + elif kind == "local": + stage, pair = event["stage"], event["pair"] + bx, by = banks[pair] + if event["reverse"]: + banks[pair] = list(model.backward(stage, stage + 1, bx, by)) + else: + bx, by, f = model.forward(stage, bx, by) + banks[pair] = [bx, by] + histories[stage] = f + record = {"kind": "local", "stage": stage} + else: + require(kind == "terminal", "retained schedule alphabet") + # The completed-X descendants are the pre-exchange X fields. + require(not any(row for bx, _ in banks for row in bx), "completed-X descendants") + banks = [[by, [linear((-1, row)) for row in bx]] for bx, by in banks] + record = {"kind": "terminal"} + require(not any(fields[p] for pair in banks for fields in pair for p in A + T), + "selected outputs stay zero") + # Each ordinary bank is an exact scalar multiple of the entire h field. + ordinary = [] + for pair in banks: + for fields in pair: + multiplier = next((c for c in (0, 1, -1) if all( + fields[p] == linear((c, h[p])) for p in U)), None) + require(multiplier is not None, "ordinary trajectory closure") + ordinary.append(multiplier) + record["ordinary"] = ordinary + trajectory.append(record) + require(trajectory == previous["trajectory_after_B1"], "retained full tail trajectory") + require(sorted(histories) == [0, 2, 4, 6, 8] and not any( + row for query in histories.values() for row in query), "all five forward histories") + require(banks[0][0] == h and not any(row for pair in banks[1:] for fields in pair for row in fields), + "only old-Y-typed final X0 survives") + require(not any(row for _, by in banks for row in by), "zero final completed-X descendants") + if wrong_endpoint: + require(not any(row for bx, _ in banks for row in bx), "wrong old-Y endpoint observation") + return { + "B0_h_at_identity": [str(at_identity(row)) for row in b0], + "required_initial_X_A_at_identity": required_input, + "zero_observations": ["all selected endpoints", "all completed-X descendants", + "f0", "f2", "f4", "f6", "f8", "pre-F0 B2 X_U"], + "tail_trajectory": trajectory, + "surviving_unobserved_endpoint": "final X0_U=h, with old-Y native type", + } + + +def rejecting(name, action, controls): + try: + action() + except ValueError: + controls.append(name) + else: + raise ValueError("negative control accepted: " + name) + + +def build_result(): + members, certificate, previous = load_sources() + word = members["CANONICAL-WORD.json.gz"] + R = reconstruct_R(word, members["LOCAL-PROGRAMS.json.gz"]) + require(R == [[Q(row.get(str(p), "0")) for p in range(112)] + for row in certificate["R_rows"]], "operation-derived R equals QQ16 input") + require((certificate["A_ports"], certificate["T_ports"], certificate["U_ports"]) + == (list(A), list(T), list(U)), "actual selected and ordinary ports") + require(all(sum(R[i][p] * R[j][p] for p in U) == (48 if i == j else 0) + for i in range(8) for j in range(8)), "ordinary Gram") + require(all(sum(R[k][p] * c for p, c in COEFFICIENTS.items()) == 0 for k in range(8)), + "three-column exact dependency") + phases = members["DATA-PHASES.json"] + model = Model(R, phases) + template = members["GLOBAL-TEMPLATE.json.gz"] + require(all(phases["recipes"][p]["q"] == word["ports"][p] for p in range(112)), + "phase/root binding") + recipe_calls = {(e["stage"], e["pair"], "backward" if e["reverse"] else "forward") + for e in template["recipe"] if e["kind"] == "local"} + require(recipe_calls == {(c["stage"], c["pair"], c["orientation"]) for c in template["calls"]}, + "recipe/hosted-call binding") + result = experiment(model, template, previous) + # Stronger than required: this h has zero query in all eight nonzero charts. + h = [{model.bases[p][0]: Q(COEFFICIENTS[p])} if p in COEFFICIENTS else {} for p in range(112)] + require(all(not any(model.query(s, h)) for s in range(1, 9)), "all nonzero-stage kernels") + controls = [] + cases = [ + ("changed dependency coefficient", {"coefficients": {2: -1, 8: 1, 85: -1}}), + ("changed chart axis", {"axis_mutation": True}), + ("missing initial A cancellation", {"omit_initial_correction": True}), + ("missing first negative bridge", {"omit_minus": True}), + ("old-Y endpoint mislabeled as completed-X", {"wrong_endpoint": True}), + ("B0 observation detects this witness", {"extra_stage": 0}), + ] + for name, options in cases: + rejecting(name, lambda options=options: experiment(model, template, previous, **options), controls) + rejecting("owner action replaced by payload-only action", + lambda: experiment(Model(R, phases, ignore_owner=True), template, previous), controls) + rejecting("source-byte mutation", lambda: authenticate(b"changed", INPUTS[CERTIFICATE], CERTIFICATE), controls) + return { + "schema": "qq16-b2-observation-kernel-v1", + "status": "PASS_QQ16_B2_OBSERVATION_KERNEL", + "proof_inputs": INPUTS, + "archive_members": MEMBERS, + "source_R_sha256": sha256(canonical([[str(x) for x in row] for row in R]).encode()).hexdigest(), + "witness": {"definition": "h_p(d)=c_p bit_0(d b_(p,0)), constant in every payload coordinate", + "coefficients": {str(p): c for p, c in COEFFICIENTS.items()}, + "axes": {str(p): model.bases[p][0] for p in COEFFICIENTS}, + "vanishing_stages": list(range(1, 9))}, + "observation_audit": result, + "rejecting_controls": controls, + "scope": "Fixed first pair and ordinary schedule; exact B2 pre-read added. No changed feedback, native read, supplier, new kappa, or formal-kernel claim.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-result", type=Path, help="Create a new receipt exclusively; never overwrite") + args = parser.parse_args() + result = build_result() + if args.emit_result is not None: + with args.emit_result.open("x", encoding="utf-8") as handle: + json.dump(result, handle, indent=2, sort_keys=True) + handle.write("\n") + else: + recorded = json.loads((PACKAGE / "RESULT.json").read_text()) + require(canonical(recorded) == canonical(result), "complete canonical result equality") + print(result["status"]) + print("3 ordinary ports; B1h=B2h=0; original A nonzero; 8 zero observations; 8 rejecting controls") + + +if __name__ == "__main__": + main()