diff --git a/research/qq16-shear-native-frame-audit/README.md b/research/qq16-shear-native-frame-audit/README.md new file mode 100644 index 0000000000..99ff1c857e --- /dev/null +++ b/research/qq16-shear-native-frame-audit/README.md @@ -0,0 +1,124 @@ +# Native frame audit of the QQ16 identity shear + +Status: independent verification and a scoped correction; no new kappa. +This package audits the native implementation claim in [PR2216](https://github.com/CrocSwap/integer-mult-bounds/pull/2216). +The payload-constant rank certificate remains outside the correction. + +## Precise claim and inherited boundary + +Fix the retained QQ16 interface and the coordinate pairing below. +Keep the F0 output boundary and B1 input boundary unchanged. +The proposed insertion uses only the sixteen bare scalar updates shown here. + +```text +A = [0, 7, 20, 27, 36, 46, 57, 111] +T = [21, 37, 47, 76, 81, 87, 92, 110] +X_T[j] += X_A[j] +Y_T[j] -= X_A[j] (j = 0,...,7) +``` + +For every listed pair, its Y update fails to implement the stated logical subtraction on arbitrary payloads. +Its X update has equal source and target frames. +The claim concerns this insertion at the retained boundary, with no intervening conversion or changed boundary convention. + +Let F=completed(0). The inherited boundary encodes logical values x and y as follows: + +```text +physical X_p = F x_p +physical Y_p = F C_(q_p)^-1 y_p +C_q = ((1+i) I + (1-i) T_q)/2, (T_q f)(z) = f(z XOR q) +``` + +This boundary is explicit in [CONSERVED-QQ16](../joint-query/evidence/CONSERVED-QQ16.md#cover-action-and-native-phases). +The [native review](../joint-query/evidence/NATIVE-REVIEW.md) states that B1 first converts X_T to the Y type. +The `boundary(stage)` function in [verify_native.py](../joint-query/verify_native.py) gives the same types. +We inherit the retained core's output contract; we do not replay or prove that complete core here. +The packet check confirms that F0's wrappers preserve the selected X types and never write Y_T. +It also checks B1's first eight normalizations against the corresponding Y types. + +## Complete counterexample argument + +Start with logical Y_T[j]=0 and X_A[j]=x. +A bare physical subtraction writes -F x. +The desired logical subtraction requires -F C_q^-1 x. +Since F is invertible, these outputs agree exactly when C_q x=x. +All translation lines commute here, so interpretation in the Y frame gives -C_q x instead of -x. +The two bare updates change the logical T sum by (I-C_q)x. + +Each selected label q is nonzero in the first nine binary coordinates. +Choose w with q dot w=1 over F2, and set chi_w(z)=(-1)^(w dot z). +Then T_q chi_w=-chi_w, hence C_q chi_w=i chi_w and C_q^-1 chi_w=-i chi_w. +Thus the two outputs differ for every selected pair. +The logical sum changes by (1-i)chi_w instead of zero. + +The witness sits at the identity-owner fiber with one nonconstant payload layer. +Keep the other payload layers and spectator coordinates constant. +This also gives a counterexample for every positive tensor length under the inherited tensor convention. +We retain the full owner cover. + +For port 21, q=289 and w=1. Then F chi_w=i chi_w. +At address zero, the bare and desired outputs are -i and -1, respectively. +[RESULT.json](RESULT.json) records all eight exact witnesses. + +PR2216's [cost paragraph](https://github.com/CrocSwap/integer-mult-bounds/blob/b80e9ba43367fb8b20877a97da1cb677c34f9264/research/qq16-f0-b1-shear-seedccce426/PROOF.md#cost-and-remaining-obligations) describes all data frames as common. +Its preceding experiment keeps each payload block constant. +On that restricted subspace every C_q acts as identity, so its test cannot detect the frame mismatch. +Sixteen bare additions do realize the shear on that subspace. +This audit does not replay or refute the reported rank-eight minor on that subspace. + +## Independent checks and limits + +The verifier authenticates four retained inputs and checks the relevant literal wrapper events. +It evaluates stored Z4 coefficient polynomials on all 512 active characters for each target. +A separate physical implementation applies Gaussian-integer C-line convolutions to eight 512-entry character arrays. +That implementation does not evaluate or generate phase polynomials and imports no predecessor executable. +Its outputs match the polynomial prediction and reject each bare subtraction. + +Inverse-line adaptation passes; the positive-line sign fails. +Physical decoding also checks the nonzero logical sum change. +Constant payloads pass both paths and expose the restricted test's blind spot. + +The complete argument above proves failure of the unrestricted scalar identity. +The finite checks bind its eight labels and witnesses to the pinned source. +They do not independently validate the full retained traversal, its native core, hosting, or the multiplication theorem. +The X count records eight equal-frame updates, rather than eight separate full-circuit tests. + +## Cost boundary and contribution + +A native implementation for arbitrary payloads needs an explicit typed adaptation or a fusion proof. +The semantic inverse-line control is not a free primitive or a hosted construction. +This audit proves no lower bound on additional children for a redesigned word. +It does not rule out reusing B1's existing operations. +The correction prevents an unrestricted controller from inheriting the sixteen-addition invoice without a typed implementation. +It changes no selected frontier or supplier certificate. + +## Reproduce + +From the repository root, run: + +```sh +python3 -I -O -B research/qq16-shear-native-frame-audit/verify.py +``` + +Expected: `PASS_QQ16_SHEAR_NATIVE_FRAME_AUDIT rejected_Y_adds=8 same_frame_X_updates=8 character_phases=4096 physical_vectors=8`. +Research verification uses CPython 3.15.0 through the Math research-python wrapper. +The generic package replay also passes in its required environment, CPython 3.12.12. +That second run is an explicit compatibility exception, not independent mathematical verification. + +## Open next questions + +Can a typed rewrite fuse the missing conversion into B1's existing native operations? +First emit that complete word and compare every arbitrary input and helper output. +Then price its children, maps, storage, restoration, precision, and hosting. +The current audit does not supply that construction. + +## Credit and provenance + +Ali Romman and the retained QQ16 lineage supply the maps, native words, and reviews. +Cinna Davis supplies the shear in PR2216, head b80e9ba43367fb8b20877a97da1cb677c34f9264. +The audit uses base 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2. +See [SOURCES.json](SOURCES.json) for exact input hashes and Git blobs. +PR2093's separate surviving A-defect concerns full-controller information, not this frame correction. + +Prepared for Charles Bethin with substantial OpenAI Codex assistance. Apache-2.0. +No independent human review or formal-kernel proof occurs here. diff --git a/research/qq16-shear-native-frame-audit/RESULT.json b/research/qq16-shear-native-frame-audit/RESULT.json new file mode 100644 index 0000000000..d6318b4920 --- /dev/null +++ b/research/qq16-shear-native-frame-audit/RESULT.json @@ -0,0 +1,229 @@ +{ + "literal_shear_scalar_additions": 16, + "owner": "identity", + "phase_characters_checked": 4096, + "physical_character_vectors": 8, + "receipts": [ + { + "A_port": 0, + "T_port": 21, + "X_T_add_legal": true, + "X_frame": "f1", + "Y_T_add_legal": false, + "Y_frame": "f23", + "bare_target": [ + 0, + -1 + ], + "desired_target": [ + -1, + 0 + ], + "frequency_mask": 1, + "inverse_line_semantic_control": "PASS", + "logical_sum_change_at_witness": [ + 1, + -1 + ], + "physical_counterexample_index": 0, + "positive_line_control": "REJECTED", + "q": 289, + "source_phase_Z4": 1, + "target_phase_Z4": 0 + }, + { + "A_port": 7, + "T_port": 37, + "X_T_add_legal": true, + "X_frame": "f1", + "Y_T_add_legal": false, + "Y_frame": "f39", + "bare_target": [ + 0, + -1 + ], + "desired_target": [ + -1, + 0 + ], + "frequency_mask": 2, + "inverse_line_semantic_control": "PASS", + "logical_sum_change_at_witness": [ + 1, + -1 + ], + "physical_counterexample_index": 0, + "positive_line_control": "REJECTED", + "q": 274, + "source_phase_Z4": 1, + "target_phase_Z4": 0 + }, + { + "A_port": 20, + "T_port": 47, + "X_T_add_legal": true, + "X_frame": "f1", + "Y_T_add_legal": false, + "Y_frame": "f49", + "bare_target": [ + 0, + -1 + ], + "desired_target": [ + -1, + 0 + ], + "frequency_mask": 4, + "inverse_line_semantic_control": "PASS", + "logical_sum_change_at_witness": [ + 1, + -1 + ], + "physical_counterexample_index": 0, + "positive_line_control": "REJECTED", + "q": 268, + "source_phase_Z4": 1, + "target_phase_Z4": 0 + }, + { + "A_port": 27, + "T_port": 76, + "X_T_add_legal": true, + "X_frame": "f1", + "Y_T_add_legal": false, + "Y_frame": "f78", + "bare_target": [ + 0, + -1 + ], + "desired_target": [ + -1, + 0 + ], + "frequency_mask": 64, + "inverse_line_semantic_control": "PASS", + "logical_sum_change_at_witness": [ + 1, + -1 + ], + "physical_counterexample_index": 0, + "positive_line_control": "REJECTED", + "q": 448, + "source_phase_Z4": 1, + "target_phase_Z4": 0 + }, + { + "A_port": 36, + "T_port": 81, + "X_T_add_legal": true, + "X_frame": "f1", + "Y_T_add_legal": false, + "Y_frame": "f83", + "bare_target": [ + 0, + -1 + ], + "desired_target": [ + -1, + 0 + ], + "frequency_mask": 2, + "inverse_line_semantic_control": "PASS", + "logical_sum_change_at_witness": [ + 1, + -1 + ], + "physical_counterexample_index": 0, + "positive_line_control": "REJECTED", + "q": 478, + "source_phase_Z4": 1, + "target_phase_Z4": 0 + }, + { + "A_port": 46, + "T_port": 87, + "X_T_add_legal": true, + "X_frame": "f1", + "Y_T_add_legal": false, + "Y_frame": "f89", + "bare_target": [ + 0, + -1 + ], + "desired_target": [ + -1, + 0 + ], + "frequency_mask": 1, + "inverse_line_semantic_control": "PASS", + "logical_sum_change_at_witness": [ + 1, + -1 + ], + "physical_counterexample_index": 0, + "positive_line_control": "REJECTED", + "q": 493, + "source_phase_Z4": 1, + "target_phase_Z4": 0 + }, + { + "A_port": 57, + "T_port": 92, + "X_T_add_legal": true, + "X_frame": "f1", + "Y_T_add_legal": false, + "Y_frame": "f94", + "bare_target": [ + 0, + -1 + ], + "desired_target": [ + -1, + 0 + ], + "frequency_mask": 1, + "inverse_line_semantic_control": "PASS", + "logical_sum_change_at_witness": [ + 1, + -1 + ], + "physical_counterexample_index": 0, + "positive_line_control": "REJECTED", + "q": 499, + "source_phase_Z4": 1, + "target_phase_Z4": 0 + }, + { + "A_port": 111, + "T_port": 110, + "X_T_add_legal": true, + "X_frame": "f1", + "Y_T_add_legal": false, + "Y_frame": "f112", + "bare_target": [ + 0, + -1 + ], + "desired_target": [ + -1, + 0 + ], + "frequency_mask": 1, + "inverse_line_semantic_control": "PASS", + "logical_sum_change_at_witness": [ + 1, + -1 + ], + "physical_counterexample_index": 0, + "positive_line_control": "REJECTED", + "q": 319, + "source_phase_Z4": 1, + "target_phase_Z4": 0 + } + ], + "same_frame_X_additions": 8, + "scope": "Counterexamples to the literal sixteen-scalar native implementation on arbitrary payloads. PR2216 logical payload-constant rank result is not refuted. Fused or redesigned implementations remain open; no child-count lower bound or new kappa.", + "status": "PASS_QQ16_SHEAR_NATIVE_FRAME_AUDIT", + "tensor_payload_layers": 1, + "unadapted_Y_additions_rejected": 8 +} diff --git a/research/qq16-shear-native-frame-audit/SOURCES.json b/research/qq16-shear-native-frame-audit/SOURCES.json new file mode 100644 index 0000000000..b2425cc735 --- /dev/null +++ b/research/qq16-shear-native-frame-audit/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/CONSERVED-QQ16.md", + "usage": "input", + "git_blob": "4639583c1be02c2fb60ed8a8072c9969ef1569ce", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + }, + { + "path": "research/joint-query/evidence/NATIVE-REVIEW.md", + "usage": "input", + "git_blob": "525b38dbdefed0e8192a9c5165e802136cc05034", + "sha256": "2247e3cbe73f3f0da55c647ffae15f98dd9445b2366ba9e255b9bebc9f742b70" + }, + { + "path": "research/joint-query/verify_native.py", + "usage": "input", + "git_blob": "ede9e7e42744dd0c96790516a9acdfe07d180018", + "sha256": "1c58e7b6e8e1cde4df455c2129601c145ed763fc63a3ab427eb1058d1fc08bd2" + } + ] +} diff --git a/research/qq16-shear-native-frame-audit/TASK.json b/research/qq16-shear-native-frame-audit/TASK.json new file mode 100644 index 0000000000..7bbafcedfc --- /dev/null +++ b/research/qq16-shear-native-frame-audit/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "joint-query-controller", + "question": "Can one explicitly changed QQ16 interface recover the missing chart query and close a two-call controller within a favorable full budget?", + "starting_points": [ + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Add one explicitly priced ordinary-to-selected observation and derive the ordered two-call map and inverse.", + "Change the first local pair or retained state, then test the existing lost-observation witness and price all new operations." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the fixed-first-pair QQ16 witness before designing a controller. The checked #1969 local words do not evade that witness or supply global placement.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Apply the existing witness to one proposed extra observation or changed first pair. If it still loses the required record, stop. Otherwise derive one ordered two-call identity and charge the added read, chart maps and restoration before extending to more stages.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969" + ] + }, + "scope_status": "refined", + "actual_scope": "Audit the literal PR2216 sixteen-scalar shear against the retained native F0 output frames.", + "scope_change_reason": "One evidence-driven pivot from a successful logical transfer proof after the cost review exposed different X and Y frames.", + "bottleneck_link": "The recursive-interface mechanism cannot use a zero-adaptation invoice until its typed word is established.", + "budget_minutes": 45, + "stop_rule": "Stop after exact counterexamples for all eight Y updates; do not infer a lower bound for fused implementations.", + "outcome": "completed", + "evidence": "RESULT.json: 4096 phase characters, eight independent physical convolution witnesses, and explicit failure of logical sum conservation.", + "author": "Charles Bethin", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, code, audit and writing.", + "open_questions": [ + { + "question": "Can B1 reuse its existing lines to implement the shear?", + "why_it_matters": "This decides whether the logical mechanism has a favorable native cost.", + "first_step": "Emit a typed complete word and verify arbitrary data and helper inputs.", + "blocked_by": "No such implementation is supplied." + } + ], + "sprint_seed": 53, + "task_identifier": "01a1335e-7a24-73c3-a549-9bcb5496a363", + "publication_status": "prepared for independent maintainer review", + "reviewed_pr_head": "b80e9ba43367fb8b20877a97da1cb677c34f9264", + "continuation_started_at": "2026-10-15T02:03:35Z", + "verification_scope": "Native boundary contract is inherited. Exact selected wrapper bindings, phase polynomials, and independent physical convolution are checked; no complete native core or traversal replay.", + "reviewed_pr_proof_sha256": "a46cd4b87c9f9f5b6ba4a88ba7d9e065531782c5ac2e1afafb6d657498957431", + "reviewed_pr_proof_path": "research/qq16-f0-b1-shear-seedccce426/PROOF.md" +} diff --git a/research/qq16-shear-native-frame-audit/VERIFY.json b/research/qq16-shear-native-frame-audit/VERIFY.json new file mode 100644 index 0000000000..3c376e481f --- /dev/null +++ b/research/qq16-shear-native-frame-audit/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/joint-query/evidence/NATIVE-REVIEW.md", + "research/joint-query/verify_native.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact native phase mismatch, independent Gaussian convolution, inverse/sign and constant-payload controls." + } + ] +} diff --git a/research/qq16-shear-native-frame-audit/verify.py b/research/qq16-shear-native-frame-audit/verify.py new file mode 100644 index 0000000000..d537e734ea --- /dev/null +++ b/research/qq16-shear-native-frame-audit/verify.py @@ -0,0 +1,247 @@ +#!/usr/bin/env python3 +"""Audit the literal QQ16 F0/B1 scalar shear against native endpoint types. + +Apache-2.0. Prepared for Charles Bethin with substantial OpenAI Codex +assistance. Ali Romman supplies the retained QQ16 maps; Cinna Davis supplies +PR2216's logical shear. No predecessor executable is imported. +""" + +import argparse +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +A = [0, 7, 20, 27, 36, 46, 57, 111] +T = [21, 37, 47, 76, 81, 87, 92, 110] +MARKER = "PASS_QQ16_SHEAR_NATIVE_FRAME_AUDIT" + + +def need(value, message): + # Remain active under -O and -OO. + if not value: + raise ValueError(message) + + +def terms_key(terms): + out = {} + for axis, coefficient in terms: + out[axis] = (out.get(axis, 0) + coefficient) % 4 + return tuple(sorted((axis, c) for axis, c in out.items() if c)) + + +def phase(polynomial, frequency): + """Evaluate stored coefficients without importing their generator.""" + result = sum( + c for i, c in enumerate(polynomial["linear_Z4"]) + if (frequency >> i) & 1 + ) + for i, row in enumerate(polynomial["quadratic_rows"]): + if (frequency >> i) & 1: + result += 2 * (row & frequency).bit_count() + return result % 4 + + +def neg(vector): + return [(-a, -b) for a, b in vector] + + +def line(vector, label, sign): + """Physical Gaussian-integer convolution, with no phase-polynomial input. + + Apply ((1 + sign*i) I + (1 - sign*i) T_label)/2. + These character fixtures stay in the Gaussian integers at every step. + """ + result = [] + for z, (a, b) in enumerate(vector): + c, d = vector[z ^ label] + real = a - sign * b + c + sign * d + imag = sign * a + b - sign * c + d + need(real % 2 == imag % 2 == 0, "nonintegral Gaussian fixture") + result.append((real // 2, imag // 2)) + return result + + +def walk(events): + """Visit only the literal retained wrapper; no core expansion is claimed.""" + for event in events: + if event[0] in ("cover_sweep", "private_sweep"): + yield from walk(event[2]) + else: + yield event + + +def bind_boundary(packet, full_id): + """Bind the inherited core boundary to the relevant literal wrappers.""" + forward = packet["programs"]["F_0"] + need(forward[0][:3] == ["retained_core", "forward", 0], "F0 core boundary") + untouched_y = {112 + p for p in T} + for event in walk(forward[1:]): + if event[0] == "scalar": + target = event[1][1] + elif event[0] in ("cover_map", "native_line"): + target = event[1] + else: + raise ValueError("unexpected F0 wrapper event " + str(event[0])) + need( + not (target[0] == "L" and target[1] in untouched_y), + "F0 wrapper changes a Y_T field", + ) + if target[0] == "L" and target[1] in A + T: + need( + event[0] == "scalar" and event[2] == full_id, + "F0 preserves selected X frame", + ) + + # B1 explicitly converts these X_T fields into their corresponding Y types. + normalizations = {} + for target, event in zip(T, packet["programs"]["B_1_2"][:8], strict=True): + need( + event[:3] == ["native_line", ["L", target], "inverse_" + str(target)], + "initial B1 normalization order", + ) + normalizations[target] = event + return normalizations + + +def run(root): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for record in manifest["files"]: + if record["usage"] == "input": + actual = hashlib.sha256((root / record["path"]).read_bytes()).hexdigest() + need(actual == record["sha256"], "source pin " + record["path"]) + + packet = json.loads(gzip.decompress( + (root / "research/joint-query/certificate.json.gz").read_bytes() + )) + need(packet["A_ports"] == A and packet["T_ports"] == T, "selected partition") + frames = packet["native_frame_registry"] + lines = packet["native_line_recipes"] + full = tuple((1 << j, 1) for j in range(9)) + frame_keys = {terms_key(v["line_terms_Z4"]): k for k, v in frames.items()} + full_id = frame_keys[full] + normalizations = bind_boundary(packet, full_id) + receipts = [] + + for source, target in zip(A, T, strict=True): + native = lines["inverse_" + str(target)] + q = native["label"] + need( + native["port"] == target and native["sign"] == -1 and 0 < q < 512, + "actual inverse native line", + ) + y_id = frame_keys[terms_key(list(full) + [(q, -1)])] + need( + normalizations[target][3:] == [full_id, y_id], + "B1 X_T normalization binds the corresponding Y_T type", + ) + w = q & -q # A concrete binary frequency with q dot w = 1. + source_phase = phase(frames[full_id], w) + target_phase = phase(frames[y_id], w) + need((target_phase - source_phase) % 4 == 3, "inverse-line phase mismatch") + need( + phase(frames[full_id], 0) == phase(frames[y_id], 0) == 0, + "constant payload blind spot", + ) + need( + all( + (phase(frames[y_id], v) - phase(frames[full_id], v)) % 4 + == (-((q & v).bit_count() % 2)) % 4 + for v in range(512) + ), + "all active-character phase differences", + ) + + # Independently apply the nine physical lines to an explicit array. + character = [(-1 if (w & z).bit_count() % 2 else 1, 0) for z in range(512)] + physical = character + for axis in range(9): + physical = line(physical, 1 << axis, 1) + units = [(1, 0), (0, 1), (-1, 0), (0, -1)] + rx, ix = units[source_phase] + ry, iy = units[target_phase] + need( + physical == [(rx * c, ix * c) for c, _ in character], + "physical F0 source versus stored polynomial", + ) + desired = [(-ry * c, -iy * c) for c, _ in character] + bare = neg(physical) + need(bare != desired, "bare subtraction must differ from logical subtraction") + mismatch = next(i for i in range(512) if bare[i] != desired[i]) + + # This source adaptation is a semantic control, not a free native primitive. + adapted = neg(line(physical, q, -1)) + wrong_sign = neg(line(physical, q, 1)) + need(adapted == desired, "inverse-line semantic positive control") + need(wrong_sign != desired, "positive-line sign negative control") + # Decode the bare Y result physically, using (F C_q^-1)^-1 = C_q F^-1. + decoded_y = bare + for axis in reversed(range(9)): + decoded_y = line(decoded_y, 1 << axis, -1) + decoded_y = line(decoded_y, q, 1) + sum_change = [(c + a, b) for (c, _), (a, b) in zip(character, decoded_y)] + need( + sum_change == [(c, -c) for c, _ in character], + "bare paired updates violate logical sum conservation", + ) + constant = [(1, 0)] * 512 + need(line(constant, q, -1) == constant, "constant-payload control") + + receipts.append({ + "A_port": source, + "T_port": target, + "q": q, + "X_frame": full_id, + "Y_frame": y_id, + "frequency_mask": w, + "source_phase_Z4": source_phase, + "target_phase_Z4": target_phase, + "physical_counterexample_index": mismatch, + "bare_target": list(bare[mismatch]), + "desired_target": list(desired[mismatch]), + "logical_sum_change_at_witness": list(sum_change[mismatch]), + "X_T_add_legal": True, + "Y_T_add_legal": False, + "inverse_line_semantic_control": "PASS", + "positive_line_control": "REJECTED", + }) + + return { + "status": MARKER, + "literal_shear_scalar_additions": 16, + "same_frame_X_additions": 8, + "unadapted_Y_additions_rejected": 8, + "phase_characters_checked": 4096, + "physical_character_vectors": 8, + "owner": "identity", + "tensor_payload_layers": 1, + "receipts": receipts, + "scope": ( + "Counterexamples to the literal sixteen-scalar native implementation " + "on arbitrary payloads. PR2216 logical payload-constant rank result " + "is not refuted. Fused or redesigned implementations remain open; " + "no child-count lower bound or new kappa." + ), + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + result = run(ROOT) + path = HERE / "RESULT.json" + if args.write_result: + path.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + need(json.loads(path.read_text()) == result, "frozen complete receipt differs") + print( + MARKER + " rejected_Y_adds=8 same_frame_X_updates=8" + " character_phases=4096 physical_vectors=8" + ) + + +if __name__ == "__main__": + main()