Remove two CNOTs from the selected left binary map (no κ)

research/selected-linear-cnot-cancellation/PROOF.md

@@ -0,0 +1,88 @@
+# Twenty-five CNOTs for the selected left binary map
+
+Claim type: an exact finite word certificate and a scoped all-column proof.
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Source and new step
+
+Jerry Chen / CubeJerry's [PR #7430](https://github.com/CrocSwap/integer-mult-bounds/pull/7430),
+head `39b40c465f7636a4bb6d70af28595fe8f70f4f3f`, binds the left binary
+factor of selected MOVE24472 to the matrix with row masks
+
+```text
+G = (3, 5, 9, 17, 32, 65, 129, 1, 256).
+```
+
+Bit i in a row mask is the coefficient of input coordinate i. Thus
+
+```text
+Gx = (x0+x1, x0+x2, x0+x3, x0+x4, x5,
+      x0+x6, x0+x7, x0, x8),
+```
+
+where every addition is in F2. That source's
+[MATRICES.json](https://github.com/CubeJerry/integer-mult-bounds/blob/39b40c465f7636a4bb6d70af28595fe8f70f4f3f/research/literal-selected-linear-maps/MATRICES.json)
+records a 27-gate left word. Gate pairs are `(target, control)` in temporal
+order, with action `x[target] ^= x[control]`.
+
+The new step removes its adjacent gates at zero-based positions 5 and 6.
+Both are `(1,0)`. For `E=I+e1 e0^T`, the scalar product `e0^T e1` is zero,
+so `E^2=I` over F2. The full product is therefore unchanged after removing
+this adjacent pair. This elementary involution identity is classical; the
+contribution is its application to this specified word and the shorter
+explicit certificate.
+
+The resulting 25-gate temporal word is
+
+```text
+(7,0) (6,0) (4,0) (3,0) (2,0)
+(0,1) (1,0) (2,1) (1,2) (2,1)
+(3,2) (2,3) (3,2) (4,3) (3,4)
+(4,3) (5,4) (4,5) (5,4) (6,5)
+(5,6) (6,5) (7,6) (6,7) (7,6).
+```
+
+The verifier establishes this new word's matrix identity directly by row
+addition from I, rather than relying on correctness of the predecessor's
+word. A separate explicit-coordinate oracle checks its entire address
+action. No predecessor executable is imported or replayed.
+
+## Every positive column multiplicity
+
+For any positive integer f, let each xi be an arbitrary vector in F2^f.
+Apply every gate by componentwise XOR. A gate acts independently on each
+bit column, so the new word is the direct sum of f copies of G under the
+coordinate/column regrouping. The same cancellation holds at every column.
+Consequently the map on all nine f-bit coordinates is exactly G, coordinate
+8 is fixed, and reversing the word is its inverse. Any additional untouched
+coordinates or payload indices remain fixed as well.
+
+Executing one coordinate CNOT at each column uses 25f elementary column
+CNOTs, compared with the cited 27f. This saves exactly 2f such calls. This
+is a gate-count statement, not an exact local tape instruction count.
+
+The endpoint equality also holds as a permutation of an arbitrary payload
+array indexed by these addresses: every source address has the same image.
+It does not supply a new physical staging, erasure or owner-return program.
+
+## Verification and limits
+
+The checker evaluates the new word on all 512 addresses at f=1 and all
+262,144 addresses at f=2, including the inverse and the spectator at every
+address. It also checks the exact nine-row matrix identity. Three controls
+reject an extra deletion, reversed control directions, and a purported f=2
+implementation that only updates the first bit column.
+
+The all-f statement follows from the direct-sum proof above; the finite
+censuses are corroboration. No minimum CNOT count is claimed. The right
+factor, phase recipes, offset, central native operator and the selected
+frontier are not improved here. Integrating the word into the literal tape
+compiler, executing its new graph, and measuring complete instructions and
+historical storage remain open. No physical speedup, supplier admission,
+complete multiplication theorem, or new kappa is claimed.
+
+The selected five framework assumptions remain. Independent human and
+formal proof-kernel review are unclaimed. The source's matrix/source binding,
+27-gate comparison point, and literal implementation belong to Jerry Chen /
+CubeJerry. Credit also its #3834, #5188, #6992 and retained native/compiler
+lineage. Their results are cited premises, not validation deliverables here.

research/selected-linear-cnot-cancellation/README.md

@@ -0,0 +1,89 @@
+# Remove two CNOTs from the selected left binary map
+
+**Exact finite certificate and scoped all-column proof; no new kappa.**
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+The left binary map of MOVE24472 has an explicit **25-CNOT word**, improving
+the 27-CNOT word recorded by Jerry Chen / CubeJerry in
+[PR #7430](https://github.com/CrocSwap/integer-mult-bounds/pull/7430) at
+`39b40c465f7636a4bb6d70af28595fe8f70f4f3f`. Its adjacent gates 5 and 6 are
+both `x1 ^= x0`; their composition is the identity. The shorter word is
+printed and proved in [PROOF.md](PROOF.md).
+
+Its exact matrix has rows `(3,5,9,17,32,65,129,1,256)`. The identity holds
+for every positive number f of binary columns and arbitrary payloads,
+saving exactly 2f elementary column CNOT calls. Coordinate 8 and untouched
+spectators remain fixed. This is the first strict word improvement found;
+no shortest-word or additional synthesis claim is made.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/selected-linear-cnot-cancellation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/selected-linear-cnot-cancellation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/selected-linear-cnot-cancellation
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/selected-linear-cnot-cancellation --check-source-history
+```
+
+Another CPython 3.12 path can replace the local interpreter. Direct replay
+prints `PASS_SELECTED_LINEAR_CNOT_CANCELLATION` in a generated JSON receipt
+bound to all six package source hashes. It writes nothing. It checks the
+new matrix by row addition and the complete new forward/inverse maps by a
+separate explicit-coordinate oracle: 512 addresses at f=1 and 262,144 at
+f=2. Three malformed implementations are distinguished. No predecessor
+executable or scientific suite is run.
+
+## Scope, provenance and overlap
+
+The selected baseline metadata check passed against main
+`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8, selected
+#7000. [SOURCES.json](SOURCES.json) pins that orientation context. The new
+word and target matrix are explicit package constants; replay does not
+depend on the pending predecessor commit being present in Git history.
+The cited source file fixes the comparison and target, rather than acting
+as an undeclared executable input.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19571878)
+asks for the first shorter word. Live claims, open PRs, account history,
+merged CNOT/24472 work and main README searches were checked. No overlapping
+shorter word for this matrix was found. These bounded searches do not prove
+literature novelty. Classical CNOT cancellation is not a new theorem.
+
+No literal tape graph is changed or executed here. Exact instruction counts,
+whole-call staging, owner return, precision and complete MOVE composition
+remain separate obligations. No selected frontier, recursive invoice or
+five-framework-assumption claim changes. Credit Jerry Chen / CubeJerry's
+#7430 and its #3834/#5188/#6992 native/compiler lineage. Independent human
+and formal proof-kernel review are unclaimed.
+
+## Code bounds
+
+The checker has no recursion, network, subprocess or filesystem writes.
+There are at most 27 gates and nine coordinates; the largest streamed
+address domain has 262,144 elements. Only one nine-coordinate input/output
+pair is live per iteration. Every function is under 60 physical lines.
+Exception-based checks remain enabled under optimization. The source-hash
+reader admits six fixed package files of at most 128 KiB each and assumes
+the package stays stable during replay. Normal and optimized warning-strict
+execution and AST inspection are the local diagnostics.
+
+Power-of-ten rule 3 deviation: CPython allocates integers, tuples and lists
+during this offline finite checker. Fixed gate/address/file bounds and a
+120-second registered timeout bound its work and live data. A fixed-storage
+port is required before use in a steady service. No compiler configuration
+or shared verifier code is changed. Build the Lever led to the rerunnable
+word certificate; Prove It Works led to the separate complete-address oracle.
+
+## Open next questions
+
+1. Integrate the 25-gate word into #7430's literal compiler and obtain fresh
+   graph, full-array and history receipts. First replace only its frozen left
+   word and regenerate that graph. The complete literal replay and source
+   binder remain the blockers to claiming an instruction-count improvement.
+2. Is 25 optimal for this exact matrix? First derive a gate-count lower bound
+   or run a separately budgeted bounded synthesis. This package stops at its
+   first strict improvement and supplies neither a search nor an optimum.
+
+[TASK.json](TASK.json) records the changed card and structured next questions.

research/selected-linear-cnot-cancellation/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}

research/selected-linear-cnot-cancellation/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "An explicit 25-CNOT word for the selected MOVE24472 left binary map, improving the cited 27-gate word, with a scoped all-positive-column proof.",
+  "scope_change_reason": "The formal-interface card is narrowed to a constructive finite binary-map side result. No proof assistant or all-size physical caller binding is claimed.",
+  "bottleneck_link": "The selected native monomial needs this exact binary permutation. Two adjacent identical CNOTs can be removed, reducing its elementary gate passes before physical compiler integration.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first strict verified gate-count improvement; do not extend synthesis.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py: exact matrix identity, complete forward/inverse f=1 and f=2 address censuses, three controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What exact literal tape instructions and history does the shorter word save?",
+      "why_it_matters": "Gate counts alone do not supply the complete physical bill.",
+      "first_step": "Replace the left frozen word in PR7430 and regenerate its literal graph and full-array receipts.",
+      "blocked_by": "No updated literal compiler graph or full tape execution is supplied."
+    },
+    {
+      "question": "Is the 25-CNOT word optimal for this exact matrix?",
+      "why_it_matters": "A lower bound would distinguish a strict improvement from a shortest word.",
+      "first_step": "Derive a source-specific lower bound or budget a bounded synthesis.",
+      "blocked_by": "This package stops at the first improvement and runs no optimal synthesis."
+    }
+  ]
+}

research/selected-linear-cnot-cancellation/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": 120,
+      "checks": "Exact new matrix identity; complete f=1 and f=2 address and inverse maps; spectator preservation; three rejection controls; generated source-hash receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact new matrix identity; complete f=1 and f=2 address and inverse maps; spectator preservation; three rejection controls; generated source-hash receipt."
+    }
+  ]
+}