Construct R420 block 4 in 29 XORs, saving 22 (no new κ)

research/r420-block4-short-word/README.md

@@ -0,0 +1,152 @@
+# R420 block 4 in 29 XOR additions
+
+This finite construction is produced by Nick Petalas. It realizes the fixed
+12-wire binary map of Cinna Davis's [PR #1383](https://github.com/CrocSwap/integer-mult-bounds/pull/1383)
+in **29 XOR additions**, with no workspace and an explicit output assignment.
+The [51-gate construction in PR #1363](https://github.com/CrocSwap/integer-mult-bounds/pull/1363)
+is the cited predecessor, so the new local word saves 22 additions.
+No predecessor count or program is independently audited here.
+
+Claim type: finite exact circuit certificate, with a written extension to
+arbitrary binary vector payloads. This is a local construction, without an
+optimality claim, a complete R420 replacement, or a new kappa.
+
+## Exact endpoint
+
+Let the twelve arbitrary input values be x0 through x11, in physical order
+
+```text
+(23,110,102,28,46,38,87,92,55,60,78,70).
+```
+
+The target is frame 546, phase-B block 4 of the historical R420 word. Its
+specification is taken from PR1383's pinned `CERTIFICATE.json`, specifically
+`source_target_rows` and `object.input_wires`. A row integer m denotes the
+linear form sum_j bit_j(m) x_j over F2. The ordered target rows are
+
+```text
+(4092,4085,3951,3967,511,1535,2559,3326,3743,3855,4080,4059).
+```
+
+For each pair (d,s) below, perform r[d] ^= r[s]. Start with r[j]=x_j.
+
+```text
+(5,6)  (7,8)  (1,3)  (1,2)  (6,2)  (3,0)  (1,9)
+(2,0)  (0,8)  (9,5)  (9,10) (7,4)  (0,10) (6,8)
+(0,11) (9,11) (9,7)  (8,1)  (8,9)  (1,0)  (0,8)
+(7,1)  (6,7)  (2,9)  (3,2)  (5,1)  (11,0) (10,0)
+(4,5)
+```
+
+Read logical output i from r[p_i], where
+
+```text
+p = (3,2,5,4,0,10,11,8,7,1,9,6).
+physical output wires = (28,102,38,46,23,78,70,55,92,110,60,87).
+```
+
+The output assignment is part of the endpoint contract. It is not an
+implemented physical routing operation or a claim that routing is free.
+There are exactly twelve registers throughout, all initially arbitrary.
+To invert the endpoint, load y_i on wire p_i and run the 29 gates backward.
+
+## Construction and proof
+
+The first bidirectional greedy trajectory, with tie seed zero, reduces the
+target matrix M to a permutation P. A row step left-multiplies by an
+involutory elementary matrix. A column step right-multiplies by one. Thus
+L M R = P and M = L^-1 P R^-1. Move P to the endpoint assignment. Execute
+the column-derived input gates, followed by the reversed row gates conjugated
+by P. `construct()` implements exactly this conversion and recovers the
+literal word and assignment above. It has a 150-move bound. No second
+trajectory was searched after this first strict improvement.
+
+A separate packed-row replay begins with the twelve unit rows, applies the
+29 listed gates, and reads them in order p. It gives exactly the twelve target
+rows displayed above. This proves the binary matrix identity. The independent
+list-valued Boolean interpreter then checks all 4,096 inputs and all 4,096
+inverse reconstructions. For payloads in any F2-vector space, apply the same
+matrix identity coordinate by coordinate. This extension uses linearity and
+holds at every payload width. It does not assert the same identity for real
+or integer addition.
+
+The new scope changes `centre-path-sharing` to PR1383's explicit historical
+shortening handoff. The current selected-baseline command passed its source
+binding and metadata checks before the experiment. It was not a scientific
+supplier replay. The historical local map does not establish a current
+persistent-centre contract or a complete signed-moment gain.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/r420-block4-short-word/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/r420-block4-short-word/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/r420-block4-short-word
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/r420-block4-short-word --check-source-history
+```
+
+Both direct modes print
+
+```text
+PASS_R420_BLOCK4_SHORT_WORD
+gates=29 cited_predecessor=51 local_saving=22 inputs=4096 inverses=4096 workspace=0
+deletions_rejected=29 directions_rejected=29 endpoint_controls=2 malformed_rejected=11
+```
+
+The final line gives a SHA256 digest of the full target, input wires, word and
+output assignment. Every single gate deletion and every single gate direction
+reversal fails the endpoint. Two more controls reject omission of the output
+assignment and a changed target. Eleven malformed program/specification cases
+are rejected. Explicit exceptions preserve all checks under optimized Python.
+The direct verifier reads no external files and writes nothing. `SOURCES.json`
+pins the predecessor specification and explanations as Git provenance, not
+as executable dependencies. No predecessor verifier is imported or replayed.
+
+All functions are under sixty lines. Loops have fixed bounds: 4,096 inputs,
+29 gate mutations per kind, eleven malformed cases, and at most 150 reduction
+moves, each considering 264 row/column moves. Python's managed allocation is
+a deviation from fixed preallocation: the reduction retains at most 150
+12-entry states and 264 candidate triples, while Boolean inputs are streamed
+one at a time. Every matrix entry is a twelve-bit integer. Warning-strict
+normal and optimized runs check the real endpoint and rejection paths.
+
+## Limits
+
+This word uses the binary map and explicit logical output assignment of the
+source handoff. It does not preserve the predecessor's positive integer lift,
+local norm envelope, downstream route assignment or full cleanup word. Those
+properties are not implied by binary equality. No full-word scalar saving,
+unchanged paid profile, hosted precision, native implementation, caller bill,
+supplier admission, selected-frontier update or complete multiplication
+theorem is claimed. There was no exact-depth exclusion, so 29 is an upper
+bound and optimality remains open. Independent human and formal proof-kernel
+review are unclaimed. No selected cold replay, Lean or Docker was run.
+
+## Open next questions
+
+1. Can one complete historical R420 caller use this exact output assignment
+   while rebuilding downstream routing and literal reverse cleanup? Start
+   with this one block and charge the complete changed word, its positive
+   norm envelope and payload cap. None of those source-bound obligations is
+   supplied here; the 22-addition local saving cannot be doubled automatically.
+2. Can a short invariant prove a lower bound approaching 29 for this exact
+   binary target with arbitrary output assignment and no workspace? Start
+   with a declared elementary-gate model and an independently checkable
+   bound. The present successful trajectory supplies no optimality evidence.
+
+These questions are unreserved. The structured scope and blockers are in
+`TASK.json`. Stop here at the first smaller finite word.
+
+## Credit
+
+The new word, reduction and checker were produced by Nick Petalas. Apache-2.0.
+Cinna Davis / 1337isnot1337 supplies the exact target, input order and explicit
+open question in PR1383, and the 51-gate predecessor with its separate
+whole-word route in PR1363. Credit eumemic for the retained PR543 R420 source,
+and the PR370/493 construction and checker lineage cited by those packages.
+Ali Romman's PR688 supplied predecessor whole-word replay structure, which
+is not used here. Elementary row/column XOR reduction and bidirectional linear
+circuit synthesis are classical methods; no general algorithm novelty is
+claimed. Frozen predecessor files and their credit are unchanged.

research/r420-block4-short-word/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/r420-block4-resynthesis/README.md",
+      "usage": "provenance",
+      "git_blob": "aeb50404a2fee0a69a23c73cd9af3db916da902f",
+      "sha256": "895ece279b64a171912cf982250feebefb918ef769d51d5f6ed96ff405d7a43a"
+    },
+    {
+      "path": "research/r420-block4-truth-audit-seed00/CERTIFICATE.json",
+      "usage": "provenance",
+      "git_blob": "1701079a1fd7dcd94c6a0a809b98a00d66b8c405",
+      "sha256": "f244d7c49d3bd1a5d111dba8e8d9281911dc5c8ee337fa1e3e6da796926ee2b2"
+    },
+    {
+      "path": "research/r420-block4-truth-audit-seed00/README.md",
+      "usage": "provenance",
+      "git_blob": "f1feab3c513a12964f9a6f829ce1aa37765a1c14",
+      "sha256": "174d7e9c6b3754e1df7241ad655718f60b8a34c6ec59856b7ff0c9b5e4124abc"
+    }
+  ]
+}

research/r420-block4-short-word/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "centre-path-sharing",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "centre-path-sharing",
+    "question": "Can a specified persistent boundary eliminate a repeated centre operation in the current caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Write a two-call input/output contract on the current source word, including arbitrary centre baselines and every later read. Price producer, retention, native alignment and restoration jointly. Historical 64-per-call and 1.90x figures are not current budgets. Stop if a missing consumer or restored-input obligation consumes the saving; reopen only with a changed legal boundary.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "centre path",
+      "persistent boundary",
+      "dirty recoding"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Finite 29-XOR realization of the fixed twelve-wire R420 phase-B block-4 binary map, with no workspace and an explicit output assignment.",
+  "scope_change_reason": "Take the explicit open shortening question in Cinna Davis PR1383 instead of constructing a current persistent-centre interface. This is a local historical side result.",
+  "bottleneck_link": "A smaller exact scalar block is reusable finite circuit evidence. It supplies no current signed-moment improvement or completed caller.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified word below 51 gates. Do not search further or claim a complete R420-word saving.",
+  "outcome": "completed",
+  "evidence": "The first seed-zero bidirectional reduction gives 29 gates. Exact matrix equality, 4096 Boolean endpoints and inverses, 29 deletions, 29 direction reversals, two endpoint controls and eleven malformed cases are checked.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a complete historical R420 caller use this output assignment with a smaller full word?",
+      "why_it_matters": "The local 22-addition saving does not include changed routing, cleanup or precision.",
+      "first_step": "Regenerate one complete word with the new block, downstream route assignments and literal reverse cleanup; derive its full norm and payload bill.",
+      "blocked_by": "No whole-word implementation, native replay or physical invoice is supplied."
+    },
+    {
+      "question": "What lower bound holds for this fixed binary target with arbitrary output assignment and no workspace?",
+      "why_it_matters": "The 29-gate word is an upper bound, not an exact minimum.",
+      "first_step": "Specify a bounded elementary-gate lower certificate for the displayed matrix.",
+      "blocked_by": "The successful greedy trajectory excludes no shorter words."
+    }
+  ],
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19219047",
+  "upstream_checkpoint": {
+    "commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+    "priority_revision": 8,
+    "checked_at": "2026-10-27T14:27:26Z"
+  },
+  "question_source": {
+    "pr": 1383,
+    "author": "1337isnot1337",
+    "question": "Can the fixed twelve-wire R420 block-4 target be realized in fewer than 51 XOR additions?"
+  },
+  "environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS arm64",
+    "dependencies": "standard library only"
+  }
+}

research/r420-block4-short-word/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Regenerate the first trajectory; check the new exact matrix and every Boolean input/inverse; reject 29 gate deletions, 29 direction flips, two endpoint corruptions and eleven malformed programs."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Regenerate the first trajectory; check the new exact matrix and every Boolean input/inverse; reject 29 gate deletions, 29 direction flips, two endpoint corruptions and eleven malformed programs."
+    }
+  ]
+}