From 6a10c0eaa7e896bb5c6d297a0b9c6bbe46143498 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Tue, 13 Oct 2026 18:22:58 -0500 Subject: [PATCH] Prove local ADD minimum for R439 frame 509 --- .../EXPECTED.json | 16 ++ .../INPUT.json | 11 + .../PREDECESSORS.json | 35 +++ .../PROOF.md | 66 ++++++ .../README.md | 43 ++++ .../SELECTION.md | 43 ++++ .../SOURCES.json | 60 +++++ .../TASK.json | 60 +++++ .../VERIFY.json | 36 +++ .../test_package.py | 32 +++ .../verify.py | 216 ++++++++++++++++++ 11 files changed, 618 insertions(+) create mode 100644 research/r439-b509-local-minimality-seed06/EXPECTED.json create mode 100644 research/r439-b509-local-minimality-seed06/INPUT.json create mode 100644 research/r439-b509-local-minimality-seed06/PREDECESSORS.json create mode 100644 research/r439-b509-local-minimality-seed06/PROOF.md create mode 100644 research/r439-b509-local-minimality-seed06/README.md create mode 100644 research/r439-b509-local-minimality-seed06/SELECTION.md create mode 100644 research/r439-b509-local-minimality-seed06/SOURCES.json create mode 100644 research/r439-b509-local-minimality-seed06/TASK.json create mode 100644 research/r439-b509-local-minimality-seed06/VERIFY.json create mode 100644 research/r439-b509-local-minimality-seed06/test_package.py create mode 100644 research/r439-b509-local-minimality-seed06/verify.py diff --git a/research/r439-b509-local-minimality-seed06/EXPECTED.json b/research/r439-b509-local-minimality-seed06/EXPECTED.json new file mode 100644 index 0000000000..61c6b85a37 --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/EXPECTED.json @@ -0,0 +1,16 @@ +{ + "minimum_adds": 3, + "target_f2_rows": [1, 3, 6, 9], + "old_integer_rows": [[1, 0, 0, 0], [1, 1, 0, 0], [2, 1, 1, 0], [1, 0, 0, 1]], + "new_integer_rows": [[1, 0, 0, 0], [1, 1, 0, 0], [0, 1, 1, 0], [1, 0, 0, 1]], + "old_minus_new": [[0, 0, 0, 0], [0, 0, 0, 0], [2, 0, 0, 0], [0, 0, 0, 0]], + "distinct_maps_by_length": [1, 12, 97, 626], + "target_words_by_length": [0, 0, 0, 3], + "shortest_words": [ + "h ^= b ; b ^= a ; c ^= a", + "h ^= b ; c ^= a ; b ^= a", + "c ^= a ; h ^= b ; b ^= a" + ], + "boolean_inputs": 16, + "positive_control_target_rows": [1, 3, 4, 12] +} diff --git a/research/r439-b509-local-minimality-seed06/INPUT.json b/research/r439-b509-local-minimality-seed06/INPUT.json new file mode 100644 index 0000000000..f547683ced --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/INPUT.json @@ -0,0 +1,11 @@ +{ + "format": "r439-b509-local-minimality/1", + "predecessor_pr": 1221, + "predecessor_head": "6deda901721316fcb61c6e2a6dd6b537de183452", + "register_order": ["a", "b", "h", "c"], + "physical_registers": [33, 38, 468, 77], + "old_word": [["b", "a"], ["h", "a"], ["c", "a"], ["h", "b"]], + "new_word": [["h", "b"], ["b", "a"], ["c", "a"]], + "boolean_endpoint": ["a", "b+a", "h+b", "c+a"], + "gate_contract": "one scalar ADD writes one destination; Boolean reduction is a directed CNOT x_d ^= x_s" +} diff --git a/research/r439-b509-local-minimality-seed06/PREDECESSORS.json b/research/r439-b509-local-minimality-seed06/PREDECESSORS.json new file mode 100644 index 0000000000..cbf5a5f77f --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/PREDECESSORS.json @@ -0,0 +1,35 @@ +{ + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "pr": 1221, + "author": "Hanson Sun (@bbMisk)", + "state_at_claim": "open", + "head": "6deda901721316fcb61c6e2a6dd6b537de183452", + "parent": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "files": { + "research/r439-b509-boolean-seed05/README.md": { + "git_blob": "18030e62bc32b5983167367aa6d252dd75570848", + "sha256": "35023cb28c826c1bd019d4db36a8c260d3e1afc3065cd75c6fa171ad41226cf6" + }, + "research/r439-b509-boolean-seed05/CANDIDATE.json": { + "git_blob": "86f33af1791026ce0cf61a4cc77cd5a9c4813994", + "sha256": "66bd9ef28754b6d0925d82137c0b2b90cb21b9234ffed18c41d31ab6b4f6192c" + } + }, + "parent_circuit": { + "pr": 973, + "head": "c05dc72734c25dd069077157224d4dd30c6e8c19", + "path": "research/r439-frame509-seed08/CANDIDATE.json" + }, + "concurrent_matrix_audit": { + "pr": 1344, + "author": "1337isnot1337", + "head_at_overlap_refresh": "a42e525e9868970f3fa2d99dccca45f014aa0fd3", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1344", + "scope_added_here": "local one-destination ADD lower bound and exact four-register shortest-word census; PR #1344 does not claim a circuit minimum" + }, + "selected_bit": { + "pr": 589, + "head": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "path_at_base": "research/e8-bit-p111-tuned/tune/EXPECTED.json" + } +} diff --git a/research/r439-b509-local-minimality-seed06/PROOF.md b/research/r439-b509-local-minimality-seed06/PROOF.md new file mode 100644 index 0000000000..d533faa604 --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/PROOF.md @@ -0,0 +1,66 @@ +# Exact local minimum for the R439 frame-509 Boolean endpoint + +## Theorem + +Fix the four named coordinates `(a,b,h,c)=(33,38,468,77)` at the frame-509 block boundary. In the scalar one-destination ADD model, the Boolean map + +```text +(a,b,h,c) -> (a, b+a, h+b, c+a) over F2 +``` + +requires at least three ADDs, and three suffice. In the directed four-register CNOT alphabet (one gate `x_d ^= x_s`, `d != s`), exactly three ordered length-three words realize the map. + +## Lower bound and witness + +The endpoint changes three distinct destination coordinates, `b`, `h`, and `c`. A scalar ADD writes only one destination, so a word of fewer than three ADDs cannot change all three outputs. This argument allows any register as a source, including dirty helpers outside these four coordinates; it depends only on the one-destination gate contract. + +PR #1221 supplies the attaining word: + +```text +h ^= b +b ^= a +c ^= a +``` + +The older four-ADD word is: + +```text +b ^= a +h ^= a +c ^= a +h ^= b +``` + +Both realize the stated endpoint for every Boolean input. The three length-three words found by the fixed four-register census are: + +```text +h ^= b ; b ^= a ; c ^= a +h ^= b ; c ^= a ; b ^= a +c ^= a ; h ^= b ; b ^= a +``` + +They differ only by the position of the independent `c ^= a` gate. The census is a finite exact cross-check; the support-independent destination argument establishes the lower bound. + +## Integer transfer distinction + +Interpreting each gate as integer addition, the old word has rows + +```text +[[1,0,0,0], [1,1,0,0], [2,1,1,0], [1,0,0,1]] +``` + +and the new word has rows + +```text +[[1,0,0,0], [1,1,0,0], [0,1,1,0], [1,0,0,1]]. +``` + +Thus `old - new` is exactly `2 e_h e_a^T`, not zero over the integers. The rewrite is justified by its characteristic-two endpoint inside PR #1221's fully checked splice; this package does not assert integer-map equality or independently replay that splice. + +## Exact finite replay + +The verifier uses integer row matrices for the two transfers and bit rows for the Boolean circuit. It evaluates all 16 four-bit assignments, checks the old/new Boolean equality and exact integer difference, then enumerates all ordered words of lengths 0 through 3 over the 12 directed CNOTs. It records both word counts and distinct endpoint counts, checks that the target first appears at length three, and verifies the three realizing words. Positive and negative controls exercise a known two-output two-gate target and a two-gate prefix that cannot equal the three-output target. + +## Limits + +This is a local minimum for one Boolean block endpoint in the scalar ADD model. It is not a shortest-factorization theorem for the original 31-ADD frame-509 block or its 20-ADD post-splice replacement, does not certify a different frame path or boundary map, and does not recheck the complete supplier. No paid recursive profile or κ changes. diff --git a/research/r439-b509-local-minimality-seed06/README.md b/research/r439-b509-local-minimality-seed06/README.md new file mode 100644 index 0000000000..aa2fcbe99f --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/README.md @@ -0,0 +1,43 @@ +# R439 frame 509: exact local ADD minimum + +**Scoped optimality proof; no new κ.** For the fixed four-register Boolean endpoint used by Hanson's PR #1221, the minimum is exactly three scalar ADDs in the one-destination model. The PR #1221 witness attains the lower bound. Concurrent PR #1344 independently verifies the same maps and full splice, but does not claim local minimality. This package adds only the local minimum and shortest-word classification; it does not duplicate that splice replay, certify the minimum cost of the full frame-509 block, or change the selected supplier. + +The destination lower bound is support-independent: the block endpoint changes three distinct output registers, while each scalar ADD writes one destination. An exact four-register census gives a separate reproducible check: among the 12 directed CNOT gates there are 1, 12, 97 and 626 distinct maps at lengths 0, 1, 2 and 3, respectively; the target has no representative below length 3 and exactly three length-3 words. + +## Reproduce + +From the repository root, with Python 3.12 or later and the standard library: + +```sh +python3 -I -O -B research/r439-b509-local-minimality-seed06/verify.py +python3 -I -O -B research/r439-b509-local-minimality-seed06/test_package.py -v +``` + +Expected verifier marker: + +```text +PASS_R439_B509_LOCAL_MINIMALITY minimum=3 length3_words=3 maps=1,12,97,626 boolean_inputs=16 integer_delta=2e_h_e_a no_new_kappa +``` + +The registered package check is: + +```sh +python3 scripts/research_package.py --package research/r439-b509-local-minimality-seed06 --check-only +``` + +Expected: `PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)`. Local replay used Python 3.14.7. The package's registered Python 3.12 replay was not run locally because Python 3.12 is not installed in this environment. + +The proof and exact scope are in [PROOF.md](PROOF.md). [TASK.json](TASK.json) records the catalogue scope change; [SELECTION.md](SELECTION.md) records the three alternatives and live overlap decision. Base inputs are pinned in [SOURCES.json](SOURCES.json); the open predecessor is pinned separately in [PREDECESSORS.json](PREDECESSORS.json). + +The package does not replay PR #1221's full word, rerun the selected cold replay, or claim H1–H5 admission, hosted adoption, a changed paid profile or a new κ. The current selected conditional result remains κ = `836330098538459/500000000000000000`; the complex supplier binds. + +## Open next questions + +- **Question:** Is the full post-splice 20-ADD frame-509 block minimum under the original 11-register integer-add model? +- **Why it matters:** That would distinguish a local Boolean cancellation floor from a lower bound on further improvements to the selected bit word's full block. +- **First step:** Extract and pin the exact 11-by-11 integer block map, then prove a destination/support lower bound before considering a bounded factorization search. +- **Blocked by:** The four-register endpoint proved here does not cover rewrites that change other block coordinates or use a different boundary map. + +## Credit and disclosure + +Credit Hanson Sun (@bbMisk), PR #1221, for the three-ADD witness; Cinna Davis (@1337isnot1337), PR #973, for the 21-ADD parent; DreamingOfClouds, PR #589; and eumemic, PR #555, for the selected R439 supplier. This package was prepared with substantial OpenAI Codex assistance; no human independent review is claimed. New work is Apache-2.0. diff --git a/research/r439-b509-local-minimality-seed06/SELECTION.md b/research/r439-b509-local-minimality-seed06/SELECTION.md new file mode 100644 index 0000000000..6cf72aa7a4 --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/SELECTION.md @@ -0,0 +1,43 @@ +# Task card: local ADD minimality for R439 frame 509 + +## Assignment and base + +- OS assignment seed: **6** (Bit supplier track). +- Base commit: `bce54fb3f895cbe5cd4c0eb477c3afeed100190f` (`origin/main` at fetch). +- Selected conditional baseline: κ = `836330098538459/500000000000000000`. +- Bit supplier ancestry: PR589 on PR555; selected-source record pins PR589 head `a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46`. + +## Three candidate tasks and selection + +1. **A larger/nonabelian bit register model.** The seed-6 catalogue suggestion was checked against live coordination. Discussion #1317 completed as PR #1333, so this route is already claimed and completed. +2. **A replacement H2/K helper-star interface.** The catalogue's second suggestion overlaps the exact dirty-target relaxation in PR #1306 and the semantic-D bridge in PR #1311, as well as the existing helper-star packages. The broad interface question is not a useful unclaimed scope here. +3. **A local lower bound for the open R439 frame-509 rewrite in PR #1221.** Selected. PR #1221 gives a three-ADD Boolean replacement and explicitly disclaims circuit minimality. At the final overlap refresh, PR #1344 independently replayed the same matrices and full splice but still made no minimum claim. This task independently certifies the exact local minimum under the standard scalar-add gate model and classifies the shortest four-register words. It adds an optimality statement; it does not repeat PR #1344's splice replay or re-review the full supplier. + +The overlap helper also returned PR #1284, a three-ADD direct-target cost in a distinct rational triangle-observation model; it uses a different object and operation alphabet, so it does not cover this R439 bit block. + +## Exact question and method + +For the fixed frame-509 Boolean endpoint on `(a,b,h,c)=(33,38,468,77)`, prove the minimum number of scalar ADDs is exactly three when each ADD has one destination and the local boundary labels are fixed. The endpoint is + +```text +(a,b,h,c) -> (a, b+a, h+b, c+a) over F2. +``` + +The lower bound is destination-based: the endpoint changes three distinct destination coordinates (`b`, `h`, `c`), and one scalar ADD writes only one destination. The three-ADD witness in PR #1221 attains this bound. Independently execute both the four-ADD and three-ADD words over every Boolean input, check the integer transfer difference `2 e_468 e_33^T`, and enumerate all 4-register CNOT words through length three as a reproducible finite cross-check. + +## Scope, overlap, and stop rule + +- PR #1221 is intentionally acknowledged: its construction is the witness being independently classified, and its README explicitly says minimum is outside its claim. +- The result is only the minimum for this fixed local Boolean endpoint in the scalar one-destination ADD model. It does not prove a minimum for the full 31-gate frame block, any altered frame path or boundary map, hosted adoption, a paid recursive profile, or κ. +- Check for a new exact frame-509 minimality claim immediately before posting. If one exists, release this scope or identify a distinct missing claim before continuing. +- Stop after the exact finite replay and focused package checks; do not run the selected frontier cold replay. + +## Deliverable and provenance + +Expected package: `research/r439-b509-local-minimality-seed06/` with proof note, standard-library verifier, exact input references and tests. Predecessors: Hanson Sun (@bbMisk), PR #1221, for the 20-ADD witness; Cinna Davis (@1337isnot1337), PR #973, for the 21-ADD parent; DreamingOfClouds, PR #589, and eumemic, PR #555, for the selected R439 word. + +Prepared with substantial OpenAI Codex assistance; no human independent review is claimed. Apache-2.0. + +## Coordination claim + +Posted to the pinned start-here discussion at 2026-10-13 23:08:59 UTC: https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18911102 diff --git a/research/r439-b509-local-minimality-seed06/SOURCES.json b/research/r439-b509-local-minimality-seed06/SOURCES.json new file mode 100644 index 0000000000..20760d7cc4 --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "CONTRIBUTING.md", + "usage": "provenance", + "git_blob": "e51435543687f1bd88ab22248082dc689ce8b853", + "sha256": "df5b5646602f42cb5da5844f04ac925182ddcd0f627b9de1c96a5095bb7a277a" + }, + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "docs/research/current-status.md", + "usage": "provenance", + "git_blob": "aa3cf49715cd367ad8c4e63ab28856fc0d19794f", + "sha256": "1f59d648763c77d574d18dc59ea8bf62d2ee74aaed3c202c9c8cfa4f901badbd" + }, + { + "path": "docs/research/pr-ledger.md", + "usage": "provenance", + "git_blob": "4331ba3175b3418f70fb5cf7ee9689b3505c0678", + "sha256": "8030b58f708e40aee4e40f950a20a0b0ccef3f92b08e6e089fe35db82ec027e6" + }, + { + "path": "docs/research/research-priority-log.md", + "usage": "provenance", + "git_blob": "346488a890884cf64f5cc69b03cb4f9a52d83c01", + "sha256": "fd7f3a15beec0b0df0d164b0f5be03867358b42d426aab9c2b5538764f541768" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + } + ] +} diff --git a/research/r439-b509-local-minimality-seed06/TASK.json b/research/r439-b509-local-minimality-seed06/TASK.json new file mode 100644 index 0000000000..1ce0d2d677 --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently certify the exact minimum scalar ADD count for the fixed R439 frame-509 Boolean endpoint in PR #1221 and enumerate all shortest words on its four named registers.", + "scope_change_reason": "The original H2/K helper-star route overlaps the exact dirty-target relaxation in PR #1306 and semantic-D bridge work in PR #1311. This contribution changes the object to the open PR #1221 frame-509 block. Concurrent PR #1344 independently verifies its matrices and splice but explicitly makes no minimum claim; this package supplies only that distinct local optimality statement and shortest-word classification.", + "bottleneck_link": "This is a bit-supplier circuit result, but the selected recursive bound remains complex-limited; it provides a certified local floor for one bit-block rewrite and does not change the paid moment.", + "budget_minutes": 60, + "stop_rule": "Stop after verifying the fixed Boolean endpoint, integer transfer difference, complete four-register CNOT census through length three, and failure controls; do not search for a full-block factorization or rerun the selected construction.", + "outcome": "completed", + "evidence": "The exact endpoint changes three distinct destinations, so every scalar one-destination ADD word needs at least three operations; PR #1221's word attains three. The standard-library verifier checks all 16 Boolean inputs, the exact integer matrix difference 2 e_h e_a^T, and all 1+12+144+1728 four-register CNOT words through length three. The target has no shorter realization and exactly three length-three realizations. PR #1344's matrix and splice replay is credited but not repeated.", + "author": "OpenAI Codex", + "ai_assistance": "Substantial OpenAI Codex assistance in source review, task selection, proof formalization, implementation, verification, and writing; no human independent review is claimed.", + "open_questions": [ + { + "question": "Is the full post-splice 20-ADD frame-509 block minimum under the original 11-register integer-add model?", + "why_it_matters": "This would determine whether more savings remain in the selected bit word's full block, beyond the local Boolean cancellation audited here.", + "first_step": "Extract and pin the exact 11-by-11 integer block map, then prove a destination/support lower bound before considering a bounded factorization search.", + "blocked_by": "This result covers one fixed four-register Boolean endpoint only; full-block rewrites may change other coordinates or use a different boundary map." + } + ] +} diff --git a/research/r439-b509-local-minimality-seed06/VERIFY.json b/research/r439-b509-local-minimality-seed06/VERIFY.json new file mode 100644 index 0000000000..ca5ad39e7c --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Checks source pins, both Boolean endpoints on all 16 inputs, exact integer transfer difference, all four-register CNOT maps through length 3, three shortest realizations, and positive/negative controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py", + "-v" + ], + "timeout_seconds": 30, + "checks": "Runs four focused tests including wrong-source, incomplete two-gate, positive two-gate, and complete-certificate controls." + } + ] +} diff --git a/research/r439-b509-local-minimality-seed06/test_package.py b/research/r439-b509-local-minimality-seed06/test_package.py new file mode 100644 index 0000000000..44da2f8c0a --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/test_package.py @@ -0,0 +1,32 @@ +#!/usr/bin/env python3 +"""Failure and positive controls for the scoped verifier.""" + +import importlib.util +from pathlib import Path +import unittest + + +PACKAGE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("r439_b509_minimality", PACKAGE / "verify.py") +VERIFY = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(VERIFY) + + +class LocalMinimumTests(unittest.TestCase): + def test_full_certificate(self): + result = VERIFY.verify() + self.assertEqual(result["minimum"], 3) + self.assertEqual(result["length3_words"], 3) + + def test_wrong_source_is_rejected(self): + self.assertNotEqual(VERIFY.f2_rows(VERIFY.BAD_SOURCE_CONTROL), VERIFY.TARGET_ROWS) + + def test_two_gate_prefix_is_rejected(self): + self.assertNotEqual(VERIFY.f2_rows(VERIFY.TWO_GATE_CONTROL), VERIFY.TARGET_ROWS) + + def test_two_gate_positive_control(self): + self.assertEqual(VERIFY.f2_rows(VERIFY.POSITIVE_CONTROL), VERIFY.POSITIVE_CONTROL_ROWS) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/r439-b509-local-minimality-seed06/verify.py b/research/r439-b509-local-minimality-seed06/verify.py new file mode 100644 index 0000000000..94ef41a09c --- /dev/null +++ b/research/r439-b509-local-minimality-seed06/verify.py @@ -0,0 +1,216 @@ +#!/usr/bin/env python3 +"""Exact local F2 circuit minimum and integer transfer check.""" + +from itertools import product +import json +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +NAMES = ("a", "b", "h", "c") +INDEX = {name: i for i, name in enumerate(NAMES)} +PHYSICAL = (33, 38, 468, 77) +OLD = ((1, 0), (2, 0), (3, 0), (2, 1)) +NEW = ((2, 1), (1, 0), (3, 0)) +TARGET_ROWS = (0b0001, 0b0011, 0b0110, 0b1001) +OLD_INTEGER = ( + (1, 0, 0, 0), + (1, 1, 0, 0), + (2, 1, 1, 0), + (1, 0, 0, 1), +) +NEW_INTEGER = ( + (1, 0, 0, 0), + (1, 1, 0, 0), + (0, 1, 1, 0), + (1, 0, 0, 1), +) +DELTA = ( + (0, 0, 0, 0), + (0, 0, 0, 0), + (2, 0, 0, 0), + (0, 0, 0, 0), +) +DISTINCT_MAPS = (1, 12, 97, 626) +TARGET_WORDS_BY_LENGTH = (0, 0, 0, 3) +SHORTEST_WORDS = ( + "h ^= b ; b ^= a ; c ^= a", + "h ^= b ; c ^= a ; b ^= a", + "c ^= a ; h ^= b ; b ^= a", +) +POSITIVE_CONTROL = ((1, 0), (3, 2)) +POSITIVE_CONTROL_ROWS = (0b0001, 0b0011, 0b0100, 0b1100) +BAD_SOURCE_CONTROL = ((2, 0), (1, 0), (3, 0)) +TWO_GATE_CONTROL = ((2, 1), (1, 0)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def f2_rows(word): + rows = [1 << i for i in range(4)] + for destination, source in word: + rows[destination] ^= rows[source] + return tuple(rows) + + +def integer_rows(word): + rows = [[int(i == j) for j in range(4)] for i in range(4)] + for destination, source in word: + rows[destination] = [ + left + right for left, right in zip(rows[destination], rows[source]) + ] + return tuple(tuple(row) for row in rows) + + +def run_boolean(word, value): + state = list(value) + for destination, source in word: + state[destination] ^= state[source] + return tuple(state) + + +def word_text(word): + return " ; ".join( + f"{NAMES[destination]} ^= {NAMES[source]}" + for destination, source in word + ) + + +def named_word(value): + require(isinstance(value, list), "word must be a JSON array") + result = [] + for gate in value: + require(isinstance(gate, list) and len(gate) == 2, "malformed gate") + destination, source = gate + require(destination in INDEX and source in INDEX, "unknown local register") + require(destination != source, "self-add is outside the CNOT alphabet") + result.append((INDEX[destination], INDEX[source])) + return tuple(result) + + +def enumerate_cnot_words(): + operations = tuple( + (destination, source) + for destination in range(4) + for source in range(4) + if destination != source + ) + distinct_counts = [] + target_words = [] + target_counts = [] + for length in range(4): + maps = {} + matches = [] + for word in product(operations, repeat=length): + rows = f2_rows(word) + maps[rows] = maps.get(rows, 0) + 1 + if rows == TARGET_ROWS: + matches.append(word) + distinct_counts.append(len(maps)) + target_counts.append(len(matches)) + target_words.append(matches) + return tuple(distinct_counts), tuple(target_counts), tuple(target_words) + + +def expected_certificate(): + return { + "minimum_adds": 3, + "target_f2_rows": list(TARGET_ROWS), + "old_integer_rows": [list(row) for row in OLD_INTEGER], + "new_integer_rows": [list(row) for row in NEW_INTEGER], + "old_minus_new": [list(row) for row in DELTA], + "distinct_maps_by_length": list(DISTINCT_MAPS), + "target_words_by_length": list(TARGET_WORDS_BY_LENGTH), + "shortest_words": list(SHORTEST_WORDS), + "boolean_inputs": 16, + "positive_control_target_rows": list(POSITIVE_CONTROL_ROWS), + } + + +def verify(): + source = json.loads((PACKAGE / "INPUT.json").read_text()) + expected = json.loads((PACKAGE / "EXPECTED.json").read_text()) + predecessor = json.loads((PACKAGE / "PREDECESSORS.json").read_text()) + + require(source["format"] == "r439-b509-local-minimality/1", "wrong input format") + require(source["predecessor_pr"] == 1221, "wrong predecessor PR") + require(source["predecessor_head"] == "6deda901721316fcb61c6e2a6dd6b537de183452", + "predecessor head changed") + require(tuple(source["register_order"]) == NAMES, "register order changed") + require(tuple(source["physical_registers"]) == PHYSICAL, "physical labels changed") + require(named_word(source["old_word"]) == OLD, "old source word changed") + require(named_word(source["new_word"]) == NEW, "new witness word changed") + require(source["boolean_endpoint"] == ["a", "b+a", "h+b", "c+a"], + "endpoint statement changed") + require(source["gate_contract"].startswith("one scalar ADD writes one destination"), + "gate contract changed") + require(predecessor["head"] == source["predecessor_head"], + "predecessor manifest does not match the input pin") + require(predecessor["pr"] == 1221 and predecessor["state_at_claim"] == "open", + "predecessor metadata changed") + concurrent = predecessor["concurrent_matrix_audit"] + require(concurrent["pr"] == 1344 + and concurrent["head_at_overlap_refresh"] + == "a42e525e9868970f3fa2d99dccca45f014aa0fd3", + "concurrent matrix-audit pin changed") + require("does not claim a circuit minimum" in concurrent["scope_added_here"], + "overlap distinction changed") + + require(f2_rows(OLD) == TARGET_ROWS, "old word misses the target endpoint") + require(f2_rows(NEW) == TARGET_ROWS, "new word misses the target endpoint") + require(integer_rows(OLD) == OLD_INTEGER, "old integer transfer changed") + require(integer_rows(NEW) == NEW_INTEGER, "new integer transfer changed") + difference = tuple( + tuple(left - right for left, right in zip(old_row, new_row)) + for old_row, new_row in zip(integer_rows(OLD), integer_rows(NEW)) + ) + require(difference == DELTA, "integer transfer difference changed") + + # Check the complete local truth table, including all dirty inputs. + for value in product((0, 1), repeat=4): + a, b, h, c = value + target = (a, b ^ a, h ^ b, c ^ a) + require(run_boolean(OLD, value) == target, "old word fails an input") + require(run_boolean(NEW, value) == target, "new word fails an input") + + counts, target_counts, words = enumerate_cnot_words() + require(counts == DISTINCT_MAPS, "distinct-map census changed") + require(target_counts == TARGET_WORDS_BY_LENGTH, "target word count changed") + require(tuple(map(word_text, words[3])) == SHORTEST_WORDS, + "length-three realization census changed") + require(len(NEW) == 3, "attaining word is not length three") + + # Failure controls: a wrong source and a two-gate prefix must miss the target. + require(f2_rows(BAD_SOURCE_CONTROL) != TARGET_ROWS, + "wrong-source negative control unexpectedly passes") + require(f2_rows(TWO_GATE_CONTROL) != TARGET_ROWS, + "two-gate negative control unexpectedly passes") + require(f2_rows(POSITIVE_CONTROL) == POSITIVE_CONTROL_ROWS, + "positive two-gate enumeration control failed") + + require(expected == expected_certificate(), "EXPECTED.json does not match replay") + return { + "minimum": 3, + "length3_words": len(words[3]), + "maps": counts, + "boolean_inputs": 16, + "integer_delta": difference, + } + + +def main(): + result = verify() + print( + "PASS_R439_B509_LOCAL_MINIMALITY " + f"minimum={result['minimum']} length3_words={result['length3_words']} " + f"maps={','.join(map(str, result['maps']))} " + f"boolean_inputs={result['boolean_inputs']} " + "integer_delta=2e_h_e_a no_new_kappa" + ) + + +if __name__ == "__main__": + main()