From f5b2498606dacd7919d1ee442288d4f375a082bb Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Tue, 13 Oct 2026 18:07:54 -0500 Subject: [PATCH] Add exact audit for P112 asymmetric unit --- .../CERTIFICATE.json | 317 +++++++++++++++++ .../CLAIM.md | 39 +++ .../PROOF.md | 100 ++++++ .../README.md | 80 +++++ .../SOURCES.json | 30 ++ .../TASK.json | 60 ++++ .../VERIFY.json | 23 ++ .../verify.py | 318 ++++++++++++++++++ 8 files changed, 967 insertions(+) create mode 100644 research/p112-off-pattern-unit-audit-seed52/CERTIFICATE.json create mode 100644 research/p112-off-pattern-unit-audit-seed52/CLAIM.md create mode 100644 research/p112-off-pattern-unit-audit-seed52/PROOF.md create mode 100644 research/p112-off-pattern-unit-audit-seed52/README.md create mode 100644 research/p112-off-pattern-unit-audit-seed52/SOURCES.json create mode 100644 research/p112-off-pattern-unit-audit-seed52/TASK.json create mode 100644 research/p112-off-pattern-unit-audit-seed52/VERIFY.json create mode 100644 research/p112-off-pattern-unit-audit-seed52/verify.py diff --git a/research/p112-off-pattern-unit-audit-seed52/CERTIFICATE.json b/research/p112-off-pattern-unit-audit-seed52/CERTIFICATE.json new file mode 100644 index 0000000000..d45ca5dd87 --- /dev/null +++ b/research/p112-off-pattern-unit-audit-seed52/CERTIFICATE.json @@ -0,0 +1,317 @@ +{ + "assignment": { + "os_random_integer": 3423301012, + "seed": 52, + "track": "structural decoder" + }, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "canonical_matrix_sha256": { + "decoder_rows_fraction_strings": "4e026e93981ff1de687279c65ceabb074445a508a2bc25833c06a3d658db888c", + "pairing_rows_little_column_bit_order_hex": "c5ca7f3bb5bc701f4be554e6cb45bc655d4fd2aeadb1b1dd74a81aef49bb4380" + }, + "checks": { + "coordinate_copy_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "coordinate_row_correction_global_source_ids": { + "75": [ + 8, + 10, + 12, + 14, + 17, + 19, + 20, + 22, + 26, + 27, + 28, + 29, + 33, + 35, + 36, + 38, + 42, + 43, + 44, + 45, + 56, + 59, + 60, + 63, + 64, + 65, + 66, + 67, + 73, + 74, + 76, + 79, + 81, + 83, + 85, + 87, + 90, + 91, + 94, + 95, + 97, + 99, + 101, + 103, + 106, + 107, + 110, + 111, + 112, + 114, + 116, + 118 + ], + "76": [ + 8, + 10, + 12, + 14, + 17, + 19, + 20, + 22, + 26, + 27, + 28, + 29, + 33, + 35, + 36, + 38, + 42, + 43, + 44, + 45, + 56, + 59, + 60, + 63, + 68, + 69, + 70, + 71, + 72, + 75, + 77, + 78, + 80, + 82, + 84, + 86, + 88, + 89, + 92, + 93, + 96, + 98, + 100, + 102, + 104, + 105, + 108, + 109, + 113, + 115, + 117, + 119 + ] + }, + "coordinate_row_correction_supports": [ + 52, + 52 + ], + "exact_diagonal_support": true, + "extra_total_copy_rank": 1, + "negative_controls_fail": [ + "sink label 329->328", + "target 75 mu -1->0" + ], + "relaxed_row_correction_global_source_ids": { + "75": [ + 64, + 65, + 66, + 67, + 73, + 74, + 76, + 79, + 81, + 83, + 85, + 87, + 90, + 91, + 94, + 95, + 97, + 99, + 101, + 103, + 106, + 107, + 110, + 111, + 112, + 114, + 116, + 118 + ], + "76": [ + 68, + 69, + 70, + 71, + 72, + 75, + 77, + 78, + 80, + 82, + 84, + 86, + 88, + 89, + 92, + 93, + 96, + 98, + 100, + 102, + 104, + 105, + 108, + 109, + 113, + 115, + 117, + 119 + ] + }, + "relaxed_row_correction_supports": [ + 28, + 28 + ], + "sink_source_window_rank": 9, + "total_copy_rank_cost": 65 + }, + "domain": { + "global_line_ids": [ + 8, + 119 + ], + "matrix_entries": 12544, + "rows": 112 + }, + "geometry": { + "d0_line_id": 76, + "d0_vector": [ + 1, + 0, + 0, + -1, + 1, + 0, + 0, + 1 + ], + "e_line_id": 0, + "e_vector": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "predecessor": "research/format-limits/README.md C.6; PR595 / PR717 model", + "schema_version": 1, + "scope": "Exact finite witness audit only; no completed supplier invoice and no new kappa.", + "source_sha256": { + "research/format-limits/scripts/c6_asym.py": "a9e17c1cf50a8403734a0e35863776a5ec7e60b44e9556f7b0206163c7f18cd0", + "research/format-limits/scripts/e8units.py": "3134443d8327d0bf2a8a66c26327cf5268cec6b7ffd85dde750b7e197ce63ef1" + }, + "witness": { + "extra_total_coefficients": { + "10": -2, + "12": -2, + "14": -2, + "17": 2, + "19": 2, + "20": -2, + "22": -2, + "26": 2, + "27": 2, + "28": -2, + "29": -2, + "33": 2, + "35": 2, + "36": -2, + "38": -2, + "42": 2, + "43": 2, + "44": -2, + "45": -2, + "56": -2, + "59": 2, + "60": -2, + "63": 2, + "8": -2 + }, + "relaxed_target_line_ids": [ + 75, + 76 + ], + "row_coefficients_mu": { + "75": "-1", + "76": "0" + }, + "shared_extra_source_line_ids": [ + 8, + 10, + 12, + 14, + 17, + 19, + 20, + 22, + 26, + 27, + 28, + 29, + 33, + 35, + 36, + 38, + 42, + 43, + 44, + 45, + 56, + 59, + 60, + 63 + ], + "sink_labels": { + "75": 329, + "76": 438 + } + } +} diff --git a/research/p112-off-pattern-unit-audit-seed52/CLAIM.md b/research/p112-off-pattern-unit-audit-seed52/CLAIM.md new file mode 100644 index 0000000000..f21e422054 --- /dev/null +++ b/research/p112-off-pattern-unit-audit-seed52/CLAIM.md @@ -0,0 +1,39 @@ +# Sprint assignment and overlap record + +- OS random integer: `3423301012`. +- Assignment seed: `52` (`3423301012 mod 60`); structural decoder track. +- Exact base: `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. +- Narrow question: independently replay the `d0=76` P112 asymmetric two-sink + witness in `research/format-limits` C.6, including all matrix entries, COPY + ranks, and correction supports. +- Method: a standard-library implementation of the E8/Hamming line geometry, + exact rational row construction, and bit-packed `F_2` elimination; no SAT + search. Seed 52 chooses `d0=76` from the predecessor's three cases + `{75,76,77}` by the middle-index rule (`52 mod 3 = 1`). +- Expected artifact: an independently runnable verifier, exact certificate, + scope note, source pins, and negative controls. No new supplier or κ claim. +- Expected finish in the posted claim: 2026-10-13 23:35 UTC; claim expiry: + 2026-10-14 00:56 UTC. +- Claim posted to the pinned coordination discussion: + https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18910869 + +## Candidate tasks considered + +1. **Selected:** independently check the off-pattern P112 asymmetric unit in + C.6, fixing the seed-selected `d0=76` pencil. The fresh overlap helper + reported zero direct matches across all 818 open PRs and 68 discussions + for the exact witness/audit terms. This is not a novelty certificate: the + local C.6 source is the predecessor being checked. +2. **Declined for overlap:** lower the P112 co-star/root-star COPY threshold + under support trims. Same-day open work includes PRs #1320, #1323 and #1325, + with claims/discussions #1267, #1301 and #1330 on adjacent pieces. +3. **Declined for overlap:** classify masked rank-eight complex decoders over + all P104 frame-pair punctures. The recent claim in discussion #1275 and PR + #1292 cover that object; PR #1212 also covers a neighbouring rank-eight + decoder rigidity question. + +The overlap helper used complete paginated snapshots (818 open PRs, 68 +discussions; no warnings). It searches titles, bodies, comments, local package +readmes/task metadata and the PR ledger, but not arbitrary code diffs or every +closed PR. The direct PR inventory and these local predecessors were also +checked by name. Recheck live metadata before submission. diff --git a/research/p112-off-pattern-unit-audit-seed52/PROOF.md b/research/p112-off-pattern-unit-audit-seed52/PROOF.md new file mode 100644 index 0000000000..d919dc72e2 --- /dev/null +++ b/research/p112-off-pattern-unit-audit-seed52/PROOF.md @@ -0,0 +1,100 @@ +# Exact audit of one P112 asymmetric pairing + +## Statement + +The `d0=76` witness from `research/format-limits` C.6 satisfies the stated +decoder support identity on the full P112 port set. Its pairing matrix has +rank 9. Its eight coordinate read blocks have rank 8 each, and one shared +extra-total read block has rank 1, for copy-rank sum 65. The two altered +decoder rows have 28 nonzero off-diagonal positions each; the corresponding +coordinate rows have 52 each. + +This is an independent finite replay of one supplied witness. It is not a +classification of all P112 decoders and it does not show that the unit has a +cheaper complete recursive cost. + +## Definitions and witness + +Let `L_i` be the 120 integer vectors generated from the extended binary +Hamming `[8,4,4]` code, in the predecessor's order: coordinate vectors +`2 e_0,...,2 e_7`, followed by the signed representatives of the 14 +weight-four code supports. Set + +\[ +G_{ij}=\frac{L_i\cdot L_j}{2},\qquad +M_{ij}=1+G_{ij}\pmod 2. +\] + +The independent checker factors `M=UU^T` over `F_2` using a nine-dimensional +orthonormal basis derived from the Gram block of greedily selected independent +rows. P112 is the ordered set `P={8,...,119}`. Every label row is represented +as a 9-bit integer with the same coordinate order as the predecessor. + +For P112, let `u_s` be the generated source label and `w_t` the sink label. +Use the predecessor's exact witness: + +- distinguished root vectors `e=L_0`, `d_0=L_76`; +- changed target rows `t=75,76`, with sink labels `329,438`; +- coefficients `mu_75=-1`, `mu_76=0`; +- shared extra-source set `Q`, recomputed from the paired sink labels and + orthogonality to `e` and `d_0` (24 source lines in total). + +The binary pairing and rational decoder entries are + +\[ +B_{ts}=\langle w_t,u_s\rangle_{F_2}, +\quad N_{ts}=G_{ts}/2\quad(t\notin\{75,76\}), +\] + +and, for `t` in the two changed rows, + +\[ +N_{ts}=L_s\cdot(d_0+\mu_t e) + \alpha_s, +\qquad +\alpha_s=\begin{cases}-L_s\cdot d_0,&s\in Q,\\0,&s\notin Q.\end{cases} +\] + +All values are exact integers or rationals. The verifier checks, entry by +entry, that for every off-diagonal position `N_ts B_ts=0`, and on every +diagonal position `B_tt=1` and `N_tt != 0`. Thus the decoder has precisely the +required diagonal support on all 112-by-112 entries. + +## COPY-rank calculation + +The global `F_2` row rank of `B` is 9. For each coordinate `a=0,...,7`, the +coordinate read block uses rows of P112 with `L_{t,a} != 0` plus both altered +targets, and columns with `L_{s,a} != 0`; each such submatrix has rank 8. +For the shared extra total, the two changed target rows restricted to `Q` have +rank 1. The reported sum is therefore `8*8+1=65`. + +The correction-support comparison counts nonzero off-diagonal `N_ts` values +in these two rows. The modified rows each have 28; their coordinate-decoder +rows each have 52. These are support counts. They are not an implementation +invoice for scalar corrections or recursive calls. + +## Negative controls and limits + +The verifier changes sink label `329` to `328`, and separately changes the +first altered-row coefficient from `-1` to `0`. Both mutations fail the full +diagonal-support check. These controls detect a broken witness replay; they do +not prove uniqueness or a lower bound. + +The audit does not charge construction or application of the extra total, +frame changes, source access, hosting, restoration, or recursive children. +It does not rerun the predecessor's SAT searches and does not certify any +assumption in the selected multiplication construction. A complete stage +contract is required before the 48 fewer correction positions can be compared +with the extra copy-rank unit in a supplier budget. + +## Reproducibility + +The exact base is `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. The predecessor +generator and E8 geometry implementation are pinned by Git blob and SHA256 in +`SOURCES.json`; the standard-library checker verifies their working hashes. +`CERTIFICATE.json` stores the exact source set, row data parameters, all rank +and support counts, and canonical SHA256 digests of the 112 pairing rows and +112 rational decoder rows. Reproduce with: + +```sh +python3 -I -O -B research/p112-off-pattern-unit-audit-seed52/verify.py +``` diff --git a/research/p112-off-pattern-unit-audit-seed52/README.md b/research/p112-off-pattern-unit-audit-seed52/README.md new file mode 100644 index 0000000000..4169c8b2c8 --- /dev/null +++ b/research/p112-off-pattern-unit-audit-seed52/README.md @@ -0,0 +1,80 @@ +# Independent exact audit of the P112 off-pattern two-sink unit + +**Research note / independent verification. No new κ or complete supplier is claimed.** + +## Finding + +This package independently reconstructs the `d0=76` member of the asymmetric +P112 unit recorded in [`format-limits` C.6](../format-limits/README.md#c6-asymmetric-pairing-uniqueness-at-the-e8-pattern-c6_asympy). +It checks the full 112-by-112 support identity with Python's standard library: + +- the pairing window is 9; +- the shared extra total reads 24 source ports and has COPY rank 1; +- the eight coordinate totals each have COPY rank 8, so the reported total + copy-rank charge is 65; +- the two modified decoder rows each have 28 off-diagonal correction + positions, compared with 52 in the corresponding coordinate rows; +- two negative controls, changing one sink label or one row coefficient, fail + the exact support condition. + +The complete witness parameters, 24 source labels, correction and rank counts, +source pins, and canonical hashes of the exact matrices are in +[`CERTIFICATE.json`](CERTIFICATE.json). [`PROOF.md`](PROOF.md) states the +identity and the limits of this check. + +This verifies one finite decoder unit. The scalar correction-support decrease +does not by itself give a cheaper paid recursive profile: the extra total, +frames, source access, realization and restoration still need a complete +supplier contract and invoice. + +## Reproduce + +From the repository root, with Python 3.10 or later and no third-party +dependencies: + +```sh +python3 -I -O -B research/p112-off-pattern-unit-audit-seed52/verify.py +``` + +Expected final line: + +```text +PASS_P112_ASYMMETRIC_UNIT_AUDIT seed=52 d0=76 ports=112 entries=12544 window=9 extra_sources=24 copy_ranks=8x8+1 copy_cost=65 corrections=28+28 baseline=52+52 controls=2 no_new_kappa +``` + +This command checks the pinned predecessor files, regenerates the E8/Hamming +geometry and binary labels, checks all 12,544 matrix positions, recomputes the +F2 ranks and correction supports, and compares the result with the committed +certificate. It does not call the SAT solver used in the predecessor's +separate pairing-classification checks. + +## Assignment and overlap + +OS random integer: `3423301012`; assignment seed: `52`; track: structural +decoder. Seed 52 selected the middle `d0` value, 76, from the predecessor's +three recorded values 75, 76 and 77. The other considered tasks and current +overlap evidence are in [`CLAIM.md`](CLAIM.md). The claim was posted to the +pinned coordination discussion [#1163](https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18910869). + +The exact base is `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. Source hashes and +the originating task card are pinned in [`SOURCES.json`](SOURCES.json) and +[`TASK.json`](TASK.json). The selected frontier at the base remains the +conditional finite construction κ=`836330098538459/500000000000000000` from +PR #1094, with the complex supplier binding. This audit does not alter it. + +## Open next questions + +Can this two-sink unit be embedded into a legal stage with a net improvement +after charging the extra total, frame changes, source access and restoration? +The first step is to write that typed entry/exit contract and full paid profile +for one invocation. The current note provides only the decoder identity and +COPY-rank submatrix counts; no complete implementation contract is available. + +## Credit and license + +Credit DreamingOfClouds, PR #595, for the `format-limits` C.6 witness and +analysis; PR #717 for the P112 model; and PR #446 for the inherited decoder +format. The E8/Hamming construction follows the source-pinned +`research/format-limits/scripts/e8units.py`. The check and note are by Cinna +Davis with substantial OpenAI Codex assistance. New work is Apache-2.0; no +predecessor source file was modified. diff --git a/research/p112-off-pattern-unit-audit-seed52/SOURCES.json b/research/p112-off-pattern-unit-audit-seed52/SOURCES.json new file mode 100644 index 0000000000..4b6560e0d1 --- /dev/null +++ b/research/p112-off-pattern-unit-audit-seed52/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/format-limits/scripts/c6_asym.py", + "usage": "input", + "git_blob": "cf0dd587772e7821b45d0f3144d7f66cff9613cc", + "sha256": "a9e17c1cf50a8403734a0e35863776a5ec7e60b44e9556f7b0206163c7f18cd0" + }, + { + "path": "research/format-limits/scripts/e8units.py", + "usage": "input", + "git_blob": "c4c1053bd15f63f9805b6df17693a79b3d1dec66", + "sha256": "3134443d8327d0bf2a8a66c26327cf5268cec6b7ffd85dde750b7e197ce63ef1" + } + ] +} diff --git a/research/p112-off-pattern-unit-audit-seed52/TASK.json b/research/p112-off-pattern-unit-audit-seed52/TASK.json new file mode 100644 index 0000000000..8f313c4e12 --- /dev/null +++ b/research/p112-off-pattern-unit-audit-seed52/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently replay the exact d0=76 two-sink asymmetric P112 decoder recorded in format-limits C.6, checking its full support identity, COPY ranks, and correction supports.", + "scope_change_reason": "The assigned structural-decoder track and seed selected an independent audit of a specific existing witness rather than synthesis of a new decoder or a complete-moment improvement. This provides evidence about the copied-information mechanism, but does not meet the original card's supplier-budget acceptance gate.", + "bottleneck_link": "The selected construction is complex-bound, and copied-information cost constrains the complex decoder. This audit checks a non-E8-pattern witness's exact copy-rank/correction trade; its missing stage implementation and invoice prevent a supplier or kappa conclusion.", + "budget_minutes": 60, + "stop_rule": "Stop after one seed-selected d0=76 witness, full 112-by-112 exact support check, all reported rank/support values, and two mutation controls. Do not expand to the other two pencils or run the SAT classification search.", + "outcome": "completed", + "evidence": "PASS_P112_ASYMMETRIC_UNIT_AUDIT: all 12,544 support entries, window rank 9, 24 extra sources, COPY ranks 8x8+1 (sum 65), row correction counts 28+28 versus 52+52, and two negative controls.", + "author": "Cinna Davis with OpenAI Codex", + "ai_assistance": "Substantial OpenAI Codex assistance: task selection, source inspection, independent checker implementation, certificate generation, and documentation.", + "open_questions": [ + { + "question": "Can this two-sink unit be embedded into a legal stage with net improvement after charging the extra total, frames, source access, realization, and restoration?", + "why_it_matters": "The 65 copy-rank sum and 48 fewer correction positions do not determine the complete recursive moment or a kappa improvement.", + "first_step": "Write a typed entry/exit contract and full paid profile for one invocation of the unit, then compare it against the symmetric P112 unit under the same stage model.", + "blocked_by": "No complete supplier realization, frame schedule, source-access contract, or restoration invoice is included in the predecessor witness." + } + ] +} diff --git a/research/p112-off-pattern-unit-audit-seed52/VERIFY.json b/research/p112-off-pattern-unit-audit-seed52/VERIFY.json new file mode 100644 index 0000000000..ab9a3adfb7 --- /dev/null +++ b/research/p112-off-pattern-unit-audit-seed52/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/format-limits/scripts/c6_asym.py", + "research/format-limits/scripts/e8units.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned-source validation; exact E8/Hamming reconstruction and F2 labels; all 12,544 decoder support entries; copy-rank and correction counts; two negative controls; committed canonical matrix certificate" + } + ] +} diff --git a/research/p112-off-pattern-unit-audit-seed52/verify.py b/research/p112-off-pattern-unit-audit-seed52/verify.py new file mode 100644 index 0000000000..b2b58d5ead --- /dev/null +++ b/research/p112-off-pattern-unit-audit-seed52/verify.py @@ -0,0 +1,318 @@ +#!/usr/bin/env python3 +"""Independent exact replay of the d0=76 asymmetric P112 witness (stdlib only).""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path +import sys + + +ROOT = Path(__file__).resolve().parents[2] +SOURCE_HASHES = { + "research/format-limits/scripts/c6_asym.py": "a9e17c1cf50a8403734a0e35863776a5ec7e60b44e9556f7b0206163c7f18cd0", + "research/format-limits/scripts/e8units.py": "3134443d8327d0bf2a8a66c26327cf5268cec6b7ffd85dde750b7e197ce63ef1", +} + + +def need(condition, message): + if not condition: + raise SystemExit("FAIL " + message) + + +def parity(x): + return x.bit_count() & 1 + + +def gf2_rank(rows): + basis = {} + for value in rows: + value = int(value) + while value: + pivot = value.bit_length() - 1 + if pivot in basis: + value ^= basis[pivot] + else: + basis[pivot] = value + break + return len(basis) + + +def roots_e8(): + """Build the 120 representatives from the extended [8,4,4] Hamming code.""" + generators = ( + (1, 1, 1, 1, 0, 0, 0, 0), + (0, 0, 1, 1, 1, 1, 0, 0), + (0, 0, 0, 0, 1, 1, 1, 1), + (0, 1, 0, 1, 0, 1, 0, 1), + ) + code = { + tuple(sum(coeff[k] * generators[k][j] for k in range(4)) % 2 for j in range(8)) + for coeff in product((0, 1), repeat=4) + } + supports = sorted(word for word in code if sum(word) == 4) + need(len(supports) == 14, "extended Hamming code has 14 weight-four supports") + roots = [tuple(2 if j == a else 0 for j in range(8)) for a in range(8)] + for support in supports: + indexes = [j for j, bit in enumerate(support) if bit] + for signs in product((1, -1), repeat=3): + row = [0] * 8 + row[indexes[0]] = 1 + for k, sign in enumerate(signs): + row[indexes[k + 1]] = sign + roots.append(tuple(row)) + need(len(roots) == 120, "E8 line count") + gram = [[sum(a * b for a, b in zip(x, y)) // 2 for y in roots] for x in roots] + need(all(gram[i][i] == 2 for i in range(120)), "E8 diagonal Gram entries") + need(all(gram[i][j] in (-1, 0, 1) for i in range(120) for j in range(120) if i != j), + "E8 off-diagonal Gram entries") + return roots, gram + + +def orthonormal_basis(form): + """Return rows C with C form C^T = I over F2, using bit-vector elimination.""" + n = len(form) + + def dot_form(x, y): + return sum(parity(form[i] & y) for i in range(n) if (x >> i) & 1) & 1 + + def complement(known): + rows = [1 << i for i in range(n)] + for b in known: + rows = [row ^ (b if dot_form(row, b) else 0) for row in rows] + return rows + + basis = [] + residual = [1 << i for i in range(n)] + norms = [dot_form(row, row) for row in residual] + while len(basis) < n: + candidates = [i for i, q in enumerate(norms) if q] + if candidates: + b = residual[candidates[0]] + basis.append(b) + products = [dot_form(row, b) for row in residual] + residual = [row ^ (b if p else 0) for row, p in zip(residual, products)] + norms = [q ^ p for q, p in zip(norms, products)] + continue + + # The residual form is alternating. Absorb a hyperbolic pair into an + # earlier unit vector, preserving orthonormality while replacing it by + # three unit vectors. + nonzero = [row for row in residual if row] + pair = next(((x, y) for x, y in combinations(nonzero, 2) if dot_form(x, y)), None) + need(pair is not None and basis, "nondegenerate alternating residual pair") + x, y = pair + unit = basis.pop(0) + basis.extend((unit ^ x, unit ^ y, unit ^ x ^ y)) + residual = complement(basis) + norms = [dot_form(row, row) for row in residual] + + gram_out = [[dot_form(basis[i], basis[j]) for j in range(n)] for i in range(n)] + need(all(gram_out[i][j] == int(i == j) for i in range(n) for j in range(n)), "orthonormal F2 basis") + return basis + + +def labels_from_gram(gram): + """Factor M=(J+G) mod 2 as U U^T using exact F2 row operations.""" + n = len(gram) + mrows = [sum((((1 + gram[i][j]) & 1) << j) for j in range(n)) for i in range(n)] + echelon = {} + selected = [] + for i, value in enumerate(mrows): + reduced = value + while reduced: + pivot = reduced.bit_length() - 1 + if pivot in echelon: + reduced ^= echelon[pivot] + else: + echelon[pivot] = reduced + selected.append(i) + break + width = len(selected) + need(width == 9, "E8 pairing Gram rank is nine") + + form = [sum((((mrows[selected[i]] >> selected[j]) & 1) << j) for j in range(width)) + for i in range(width)] + change = orthonormal_basis(form) + labels = [] + for row in mrows: + restricted = sum((((row >> selected[j]) & 1) << j) for j in range(width)) + labels.append([parity(restricted & basis_row) for basis_row in change]) + need(all((sum(labels[i][k] * labels[j][k] for k in range(width)) & 1) + == ((1 + gram[i][j]) & 1) for i in range(n) for j in range(n)), + "all 120 x 120 label pairings") + return labels + + +def encode_label(row): + return sum(int(bit) << (8 - j) for j, bit in enumerate(row)) + + +def rank_submatrix(rows, row_ids, col_ids): + packed = [sum(((rows[i] >> col) & 1) << j for j, col in enumerate(col_ids)) for i in row_ids] + return gf2_rank(packed) + + +def build_witness(roots, gram, labels): + ports = list(range(8, 120)) + local = {global_id: i for i, global_id in enumerate(ports)} + label_values = [encode_label(labels[i]) for i in ports] + target_to_sink = {75: 329, 76: 438} + target_mu = {75: Fraction(-1), 76: Fraction(0)} + d0 = roots[76] + e = roots[0] + + # For each changed row, the extra-total support consists of source labels + # paired to its sink, excluding the target itself, whose E8 root is + # orthogonal to e and nonorthogonal to d0. + extra_sets = {} + for target, sink in target_to_sink.items(): + t = local[target] + e_set = set() + for s, global_s in enumerate(ports): + paired = parity(sink & label_values[s]) + e_perp = sum(roots[global_s][k] * e[k] for k in range(8)) == 0 + d_nonzero = sum(roots[global_s][k] * d0[k] for k in range(8)) != 0 + if paired and s != t and e_perp and d_nonzero: + e_set.add(s) + need(t not in e_set, "extra-total support excludes its target") + extra_sets[target] = e_set + extra_sources = extra_sets[75] | extra_sets[76] + need(len(extra_sources) == 24, "shared extra total has 24 source ports") + + # Baseline pairing M=(J+G) mod 2, with exactly two sink rows replaced. + b_rows = [] + for t, global_t in enumerate(ports): + sink = target_to_sink.get(global_t, label_values[t]) + b_rows.append(sum(parity(sink & label_values[s]) << s for s in range(len(ports)))) + n_rows = [[Fraction(gram[gt][gs], 2) for gs in ports] for gt in ports] + alpha = {s: -sum(roots[ports[s]][k] * d0[k] for k in range(8)) for s in extra_sources} + for global_t in (75, 76): + t = local[global_t] + mu = target_mu[global_t] + vec = [Fraction(d0[k]) + mu * Fraction(e[k]) for k in range(8)] + n_rows[t] = [sum(Fraction(roots[global_s][k]) * vec[k] for k in range(8)) + alpha.get(s, 0) + for s, global_s in enumerate(ports)] + return ports, b_rows, n_rows, extra_sources, target_to_sink, target_mu + + +def exactness(b_rows, n_rows): + for t, row in enumerate(n_rows): + if not ((b_rows[t] >> t) & 1) or row[t] == 0: + return False + for s, value in enumerate(row): + if s != t and value and ((b_rows[t] >> s) & 1): + return False + return True + + +def main(): + for path, expected in SOURCE_HASHES.items(): + actual = sha256((ROOT / path).read_bytes()).hexdigest() + need(actual == expected, "source pin " + path) + + roots, gram = roots_e8() + labels = labels_from_gram(gram) + ports, b_rows, n_rows, extra_sources, target_to_sink, target_mu = build_witness(roots, gram, labels) + need(len(ports) == 112, "P112 port count") + need(exactness(b_rows, n_rows), "N o B has exactly the diagonal support on all 112 x 112 entries") + + copy_rank = gf2_rank(b_rows) + need(copy_rank == 9, "global sink/source pairing window") + coordinate_ranks = [] + for a in range(8): + readers = [i for i, global_i in enumerate(ports) if roots[global_i][a] != 0 or global_i in target_to_sink] + sources = [i for i, global_i in enumerate(ports) if roots[global_i][a] != 0] + coordinate_ranks.append(rank_submatrix(b_rows, readers, sources)) + extra_rank = rank_submatrix(b_rows, [67, 68], sorted(extra_sources)) + copy_cost = sum(coordinate_ranks) + extra_rank + need(coordinate_ranks == [8] * 8 and extra_rank == 1 and copy_cost == 65, + "eight coordinate ranks, shared-total rank and total copy rank") + + relaxed_local = [ports.index(i) for i in (75, 76)] + corrections = [sum(s != t and value != 0 for s, value in enumerate(n_rows[t])) for t in relaxed_local] + baseline_corrections = [sum(s != t and gram[gt][gs] != 0 for s, gs in enumerate(ports)) + for t, gt in zip(relaxed_local, (75, 76))] + need(corrections == [28, 28] and baseline_corrections == [52, 52], "exact correction support counts") + correction_sources = { + str(gt): [ports[s] for s, value in enumerate(n_rows[t]) if s != t and value != 0] + for gt, t in zip((75, 76), relaxed_local) + } + baseline_sources = { + str(gt): [gs for s, gs in enumerate(ports) if s != t and gram[gt][gs] != 0] + for gt, t in zip((75, 76), relaxed_local) + } + + # Negative controls: change a sink bit, or change the d0=76 target's + # coefficient. The published witness's exact support property must fail. + bad_sink_rows = list(b_rows) + bad_sink_rows[relaxed_local[0]] = sum( + parity(328 & encode_label(labels[global_s])) << s for s, global_s in enumerate(ports) + ) + need(not exactness(bad_sink_rows, n_rows), "negative control: altered sink label") + + bad_n_rows = [list(row) for row in n_rows] + wrong_vec = [Fraction(roots[76][k]) for k in range(8)] + bad_n_rows[relaxed_local[0]] = [sum(Fraction(roots[global_s][k]) * wrong_vec[k] for k in range(8)) + + (-sum(roots[ports[s]][k] * roots[76][k] for k in range(8)) + if s in extra_sources else 0) + for s, global_s in enumerate(ports)] + need(not exactness(b_rows, bad_n_rows), "negative control: altered relaxed-row coefficient") + + # Hash canonical row encodings so the full exact matrices have a compact, + # reproducible receipt in addition to the entrywise checks above. + b_encoding = "\n".join(f"{row:028x}" for row in b_rows) + "\n" + n_encoding = "\n".join(",".join(str(value) for value in row) for row in n_rows) + "\n" + extra_global = [ports[s] for s in sorted(extra_sources)] + alpha = {str(global_s): -sum(roots[global_s][k] * roots[76][k] for k in range(8)) + for global_s in extra_global} + result = { + "schema_version": 1, + "assignment": {"os_random_integer": 3423301012, "seed": 52, "track": "structural decoder"}, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "predecessor": "research/format-limits/README.md C.6; PR595 / PR717 model", + "domain": {"global_line_ids": [8, 119], "rows": 112, "matrix_entries": 12544}, + "geometry": {"e_line_id": 0, "e_vector": list(roots[0]), "d0_line_id": 76, "d0_vector": list(roots[76])}, + "witness": { + "relaxed_target_line_ids": [75, 76], + "sink_labels": {"75": 329, "76": 438}, + "row_coefficients_mu": {"75": "-1", "76": "0"}, + "shared_extra_source_line_ids": extra_global, + "extra_total_coefficients": alpha, + }, + "checks": { + "exact_diagonal_support": True, + "sink_source_window_rank": copy_rank, + "coordinate_copy_ranks": coordinate_ranks, + "extra_total_copy_rank": extra_rank, + "total_copy_rank_cost": copy_cost, + "relaxed_row_correction_supports": corrections, + "coordinate_row_correction_supports": baseline_corrections, + "relaxed_row_correction_global_source_ids": correction_sources, + "coordinate_row_correction_global_source_ids": baseline_sources, + "negative_controls_fail": ["sink label 329->328", "target 75 mu -1->0"], + }, + "canonical_matrix_sha256": { + "pairing_rows_little_column_bit_order_hex": sha256(b_encoding.encode()).hexdigest(), + "decoder_rows_fraction_strings": sha256(n_encoding.encode()).hexdigest(), + }, + "source_sha256": SOURCE_HASHES, + "scope": "Exact finite witness audit only; no completed supplier invoice and no new kappa.", + } + cert_path = Path(__file__).resolve().with_name("CERTIFICATE.json") + if "--write-certificate" in sys.argv: + need(not cert_path.exists(), "refuse to overwrite an existing certificate") + cert_path.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print("WROTE_CERTIFICATE " + str(cert_path)) + return + need(cert_path.is_file(), "missing committed CERTIFICATE.json") + need(json.loads(cert_path.read_text()) == result, "committed exact witness certificate") + + print("PASS_P112_ASYMMETRIC_UNIT_AUDIT seed=52 d0=76 ports=112 entries=12544 " + "window=9 extra_sources=24 copy_ranks=8x8+1 copy_cost=65 " + "corrections=28+28 baseline=52+52 controls=2 no_new_kappa") + + +if __name__ == "__main__": + main()