diff --git a/research/r420-block4-short-word/README.md b/research/r420-block4-short-word/README.md new file mode 100644 index 0000000000..7c99cfb448 --- /dev/null +++ b/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. diff --git a/research/r420-block4-short-word/SOURCES.json b/research/r420-block4-short-word/SOURCES.json new file mode 100644 index 0000000000..c3afaa9e6e --- /dev/null +++ b/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" + } + ] +} diff --git a/research/r420-block4-short-word/TASK.json b/research/r420-block4-short-word/TASK.json new file mode 100644 index 0000000000..9d93be64b7 --- /dev/null +++ b/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" + } +} diff --git a/research/r420-block4-short-word/VERIFY.json b/research/r420-block4-short-word/VERIFY.json new file mode 100644 index 0000000000..06c378bf1e --- /dev/null +++ b/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." + } + ] +} diff --git a/research/r420-block4-short-word/verify.py b/research/r420-block4-short-word/verify.py new file mode 100644 index 0000000000..ea5134e61c --- /dev/null +++ b/research/r420-block4-short-word/verify.py @@ -0,0 +1,196 @@ +"""Construct and check a 29-XOR realization of the fixed R420 block-4 map. + +The target and wire order are the specification from Cinna Davis's PR1383. +The new word and its bidirectional reduction are produced by Nick Petalas. +Apache-2.0. No predecessor program is imported or replayed. +""" + +import hashlib +import json +import random + + +WIDTH = 12 +TARGET = (4092, 4085, 3951, 3967, 511, 1535, + 2559, 3326, 3743, 3855, 4080, 4059) +INPUT_WIRES = (23, 110, 102, 28, 46, 38, 87, 92, 55, 60, 78, 70) +WORD = ((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)) +OUTPUT_TO_WIRE = (3, 2, 5, 4, 0, 10, 11, 8, 7, 1, 9, 6) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate(word, assignment, target): + require(len(target) == WIDTH, "target width") + require(all(type(x) is int and 0 <= x < 1 << WIDTH for x in target), + "target entry") + require(len(assignment) == WIDTH, "assignment width") + require(all(type(x) is int for x in assignment), "assignment type") + require(sorted(assignment) == list(range(WIDTH)), "assignment permutation") + require(0 < len(word) <= 150, "word length") + for gate in word: + require(len(gate) == 2, "gate arity") + require(all(type(x) is int and 0 <= x < WIDTH for x in gate), + "gate index") + require(gate[0] != gate[1], "self addition") + + +def columns(rows): + return [sum(((rows[i] >> j) & 1) << i for i in range(WIDTH)) + for j in range(WIDTH)] + + +def next_move(rows, seen, rng): + best = -WIDTH + moves = [] + for side, vectors in enumerate((rows, columns(rows))): + for dest in range(WIDTH): + for source in range(WIDTH): + if dest == source: + continue + gain = vectors[dest].bit_count() + gain -= (vectors[dest] ^ vectors[source]).bit_count() + if gain > best: + best, moves = gain, [(side, dest, source)] + elif gain == best: + moves.append((side, dest, source)) + rng.shuffle(moves) + for side, dest, source in moves: + changed = list(rows) + if side == 0: + changed[dest] ^= changed[source] + else: + for i in range(WIDTH): + changed[i] ^= ((changed[i] >> source) & 1) << dest + if tuple(changed) not in seen: + return side, dest, source, changed + raise ValueError("no unseen best move") + + +def construct(): + """Replay only the first trajectory, with at most 150 reduction moves.""" + rows = list(TARGET) + left, right, seen = [], [], set() + rng = random.Random(0) + for _ in range(151): + if sum(x.bit_count() for x in rows) == WIDTH: + assignment = tuple(x.bit_length() - 1 for x in rows) + require(sorted(assignment) == list(range(WIDTH)), "not a permutation") + word = right + [(assignment[d], assignment[s]) + for d, s in reversed(left)] + require(len(word) <= 150, "construction budget") + return tuple(word), assignment + require(len(left) + len(right) < 150, "construction exhausted") + side, dest, source, rows = next_move(rows, seen, rng) + seen.add(tuple(rows)) + if side == 0: + left.append((dest, source)) + else: + right.append((source, dest)) + raise ValueError("construction exhausted") + + +def matrix_rows(word, assignment): + rows = [1 << i for i in range(WIDTH)] + for dest, source in word: + rows[dest] ^= rows[source] + return tuple(rows[i] for i in assignment) + + +def boolean_run(bits, word): + state = list(bits) + for dest, source in word: + state[dest] = (state[dest] + state[source]) % 2 + return state + + +def exhaustive_inputs(): + checked = 0 + for mask in range(1 << WIDTH): + bits = [(mask >> i) & 1 for i in range(WIDTH)] + expected = [sum(bits[j] for j in range(WIDTH) if (row >> j) & 1) % 2 + for row in TARGET] + state = boolean_run(bits, WORD) + actual = [state[i] for i in OUTPUT_TO_WIRE] + require(actual == expected, f"Boolean endpoint {mask}") + # Load logical outputs on their assigned physical wires before inversion. + inverse_input = [0] * WIDTH + for i, wire in enumerate(OUTPUT_TO_WIRE): + inverse_input[wire] = expected[i] + require(boolean_run(inverse_input, reversed(WORD)) == bits, + f"inverse endpoint {mask}") + checked += 1 + return checked + + +def corruption_controls(): + deletions = reversals = 0 + for i, (dest, source) in enumerate(WORD): + omitted = WORD[:i] + WORD[i + 1:] + require(matrix_rows(omitted, OUTPUT_TO_WIRE) != TARGET, "deleted gate") + deletions += 1 + reversed_gate = WORD[:i] + ((source, dest),) + WORD[i + 1:] + require(matrix_rows(reversed_gate, OUTPUT_TO_WIRE) != TARGET, + "reversed gate") + reversals += 1 + identity_assignment = tuple(range(WIDTH)) + require(matrix_rows(WORD, identity_assignment) != TARGET, "missing assignment") + changed = TARGET[:-1] + (TARGET[-1] ^ 1,) + require(matrix_rows(WORD, OUTPUT_TO_WIRE) != changed, "changed target") + return deletions, reversals, 2 + + +def malformed_controls(): + cases = ( + ((), OUTPUT_TO_WIRE, TARGET), + (WORD * 6, OUTPUT_TO_WIRE, TARGET), + (((0,),), OUTPUT_TO_WIRE, TARGET), + (((True, 1),), OUTPUT_TO_WIRE, TARGET), + (((0, WIDTH),), OUTPUT_TO_WIRE, TARGET), + (((1, 1),), OUTPUT_TO_WIRE, TARGET), + (WORD, OUTPUT_TO_WIRE[:-1], TARGET), + (WORD, (0,) * WIDTH, TARGET), + (WORD, (True,) + OUTPUT_TO_WIRE[1:], TARGET), + (WORD, OUTPUT_TO_WIRE, TARGET[:-1]), + (WORD, OUTPUT_TO_WIRE, (1 << WIDTH,) + TARGET[1:]), + ) + rejected = 0 + for word, assignment, target in cases: + try: + validate(word, assignment, target) + except ValueError: + rejected += 1 + else: + raise ValueError("malformed fixture accepted") + return rejected + + +def main(): + validate(WORD, OUTPUT_TO_WIRE, TARGET) + word, assignment = construct() + require((word, assignment) == (WORD, OUTPUT_TO_WIRE), "construction drift") + require(len(WORD) == 29 and len(WORD) < 51, "strict shortening") + require(matrix_rows(WORD, OUTPUT_TO_WIRE) == TARGET, "matrix endpoint") + checked = exhaustive_inputs() + deletions, reversals, endpoint_controls = corruption_controls() + malformed = malformed_controls() + payload = {"target_rows": TARGET, "input_wires": INPUT_WIRES, + "operations": WORD, "output_to_wire": OUTPUT_TO_WIRE} + digest = hashlib.sha256(json.dumps(payload, sort_keys=True).encode()).hexdigest() + print("PASS_R420_BLOCK4_SHORT_WORD") + print(f"gates={len(WORD)} cited_predecessor=51 local_saving={51 - len(WORD)} " + f"inputs={checked} inverses={checked} workspace=0") + print(f"deletions_rejected={deletions} directions_rejected={reversals} " + f"endpoint_controls={endpoint_controls} malformed_rejected={malformed}") + print(f"witness_sha256={digest} no_new_kappa") + + +if __name__ == "__main__": + main()