Prove the global thirteen-ADD dirty parity-fanout minimum (no κ)

research/global-thirteen-add-fanout/PROOF.md

@@ -0,0 +1,125 @@
+# The global thirteen-ADD lower bound
+
+This scoped proof was produced by Nick Petalas. New work is Apache-2.0.
+
+## Statement
+
+Let A, B, C, X_i, Y_i, Z_i for i=1,2,3, and any finite number of
+additional rows be arbitrary independent elements of F2^L, L>=1. Every
+instruction is one paid row XOR r_d <- r_d + r_s, with d != s. Sources,
+targets and additional rows may all be read or written in any order. There
+are no free operations, clean initial rows or input-dependent instructions.
+The endpoint preserves A, B, C and every additional row, and requires
+
+    X_i' = X_i + A+B,
+    Y_i' = Y_i + A+B+C,
+    Z_i' = Z_i + A+C.
+
+Every such finite program has at least thirteen instructions. Consequently
+Cinna Davis's thirteen-instruction construction in PR2271 is globally optimal
+in this larger program class. The new result is the lower bound; that
+construction and its earlier one-anchor optimality retain their original
+credit. No predecessor executable or finite certificate is used in this proof.
+
+It suffices to prove the bound at L=1. Write each current row as a formal
+binary linear combination of all original rows. These coefficient rows form
+an invertible matrix at every cut, since each instruction is an elementary
+row operation. In particular no current coefficient row is zero.
+
+## 1. Count incoming writes
+
+Let c_v count instructions whose destination is row v. Each of the nine
+targets has c_v>=1, since its prescribed change is nonzero. Every unchanged
+row has either c_v=0 or c_v>=2. Indeed, a row written exactly once has its
+original value until that instruction, which adds a nonzero coefficient row;
+its value then stays changed to the endpoint.
+
+Suppose the whole program has at most twelve instructions. There are at most
+three writes beyond the nine mandatory target writes:
+
+    sum_targets (c_v-1) + sum_unchanged c_v <= 3.                 (1)
+
+Call a target written exactly once light. At every cut a light target j is
+either its original row e_j or its final row e_j+p_j, where p_j is its
+prescribed source parity. Both have exactly the same coefficients on all
+original nonsource rows. At its sole write, the input must be exactly p_j.
+All prescribed parities have at least two source coordinates.
+
+## 2. Some original source must be written
+
+Suppose A, B and C are never written. Order them first. At every cut the
+coefficient matrix has the block form
+
+    [ I_3  0 ]
+    [  U   V ],
+
+where V is invertible. Source-to-nonsource instructions leave V unchanged;
+nonsource-to-nonsource instructions perform elementary row operations on V.
+Thus every nonsource row has a nonzero coefficient on original nonsource
+inputs. It can never equal a pure source parity. The three unchanged source
+rows are single source coordinates, so they cannot supply p_j either.
+
+By (1), at most three targets are written more than once. There is a light
+target, whose required input p_j is therefore unavailable. This contradiction
+shows that at least one original source is written.
+
+## 3. Only one source can be written
+
+By (1) and the unchanged-row rule, exactly one original source a can be
+written, and its write count m is either two or three. All additional rows
+and the other two sources are never written.
+
+If m=3, all nine targets are light. Every row other than a is either an
+unchanged original source coordinate, an unchanged additional dirty row,
+or a light target. None can equal a prescribed pure parity. Hence a must
+supply all three distinct parities A+B, A+B+C, A+C.
+
+But a starts and ends at its original single source coordinate. Three
+writes give at most two intermediate values, so a cannot supply three
+specified values distinct from its starting value. This excludes m=3.
+
+## 4. A twice-written target cannot supply the missing parity
+
+Now m=2. There is at most one non-light target t, with exactly two writes.
+If it does not exist, only a could supply pure parities, and its one
+intermediate value is insufficient. Suppose t exists.
+
+Let e_t be the coefficient of t's original dirty input. Every light target
+and unchanged row other than a has e_t coefficient zero. Only a and t can
+have that coefficient. If t ever holds a pure source value, this occurs
+between its two writes. Its first write must cancel its original e_t, so
+its input is a with e_t coefficient one.
+
+At that point at least one write into a has occurred. Both cannot already
+have occurred, because a would then have its final original source value
+and e_t coefficient zero. Thus exactly one write into a has occurred. That
+write could have acquired e_t only by reading t. Since t has not yet been
+written, it was still its bare original row e_t. Therefore
+
+    a = a_original + e_t,
+    t_after_first_write = e_t + a = a_original.                 (2)
+
+Thus the only possible pure source value of t is the original single
+source coordinate a_original. It is none of the required multi-source
+parities. This argument permits arbitrary interleavings of all light-target
+writes and does not assume a source-only tour.
+
+Only a can therefore supply a light target's prescribed input. Each parity
+class has three targets, and at most one target is non-light, so every
+class still has a light target. Row a would have to supply all three
+parities. Its two writes give only one intermediate value distinct from
+its original value. This is impossible.
+
+All programs of length at most twelve are excluded. The bound holds for
+any finite dirty workspace and arbitrary target feedback. Combining it
+with the credited thirteen-call construction proves the stated optimum.
+
+## Scope
+
+The argument is algebraic, with unit cost per whole-row XOR. It applies
+bitwise at every positive common width. It does not optimize bit gates that
+mix different coordinates inside a row. Clean initialization, arbitrary
+free linear maps, nonlinear or input-dependent instructions, native calls,
+physical layout, tape travel, precision and recursive prices are outside
+this alphabet. No multiplication theorem, new kappa or supplier admission
+follows. Independent human and formal proof-kernel review are unclaimed.

research/global-thirteen-add-fanout/README.md

@@ -0,0 +1,146 @@
+# Thirteen row ADDs are globally necessary for the PR2271 boundary
+
+This scoped mathematical proof was produced by Nick Petalas. Apache-2.0.
+
+Cinna Davis's [PR2271](https://github.com/CrocSwap/integer-mult-bounds/pull/2271)
+gives a thirteen-ADD circuit for three copies each of the source parities
+A+B, A+B+C and A+C. It proves optimality within one-anchor tours. The new
+lower bound permits arbitrary CNOT ordering, target feedback and any finite
+number of additional restored dirty rows. **Thirteen is still the minimum.**
+
+For arbitrary independent source and target rows over F2^L, L>=1, require
+
+```text
+A, B, C and every additional row return unchanged;
+X_i += A+B;   Y_i += A+B+C;   Z_i += A+C,   i=1,2,3.
+Every instruction is one paid r_d ^= r_s, d != s.
+```
+
+There are no free maps or clean initial rows. Every scalar row is an
+independent arbitrary input. The new result is an unrestricted lower bound
+inside this row-XOR alphabet. The upper construction is credited to PR2271
+and is cited without replaying its verifier or finite certificate.
+
+## Proof and evidence
+
+[PROOF.md](PROOF.md) gives the complete written argument. Nine target writes
+are mandatory. An unchanged row cannot be written exactly once. A putative
+twelve-gate circuit therefore has only three surplus writes. If no source
+changes, an invertible dirty-input block excludes every needed pure parity.
+Otherwise only one source changes, either twice or three times. The
+three-write case has too few intermediate values. In the two-write case,
+at most one target can be written twice; if that target becomes pure, its
+only possible pure value is the original single source coordinate. It
+cannot supply a missing multi-source parity. This exhausts the budget.
+
+The arbitrary-workspace conclusion is a written proof. The self-contained
+verifier corroborates its lemmas on complete, explicitly finite domains:
+
+- All 168 invertible binary three-row bases and all 1,008 single CNOT
+  transitions change their destination row.
+- All 55,987 words of length at most six on two fixed sources and two dirty
+  rows preserve the invertible dirty block, across 380,713 prefix visits.
+- All 12,288 four-write words with two writes into A and two into T, over
+  eight frozen-row source offsets. Of these, 2,720 restore A. Their eight
+  pure intermediate T values are all the original single A coordinate.
+- All 680 surplus allocations across nine targets, three sources and two
+  extra rows. The 275 allocations respecting the unchanged-row rule include
+  33 with a changed source, all in the two cases used in the proof.
+- All 219 closed pure-source itineraries with one through three writes,
+  allowing even zero as an intermediate state. None visits all three masks.
+  A four-write positive control does visit them.
+- Interpreter-domain rejections and semantic controls distinguish missing
+  source restoration, a changed source and a singular dirty block. Exact
+  executed counts are emitted by the verifier.
+
+These are new lemma checks, not a census of twelve-gate programs, a replay
+of PR2271 or a proof-kernel certificate. The program writes no files and
+prints a generated receipt binding all six package files by SHA256.
+
+## Reproduce
+
+From the repository root, with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/global-thirteen-add-fanout/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/global-thirteen-add-fanout/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/global-thirteen-add-fanout
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/global-thirteen-add-fanout --check-source-history
+```
+
+Substitute another CPython 3.12 path on other machines. The direct marker is
+`PASS_GLOBAL_THIRTEEN_ADD_LOWER_BOUND`; the registered and publication checks
+report `PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`.
+Run the last command after committing. Registered commands have independent
+120-second timeouts. Direct replay also works without Git or repository
+imports. Provenance documents are pinned historical inputs, not live
+scientific dependencies.
+
+## Scope, overlap and credit
+
+Credit Cinna Davis / 1337isnot1337 for PR2271's exact boundary, borrowed-source
+construction, complete restoration and earlier restricted optimality. Its
+retained dirty-fanout and connector lineage remains credited in the unchanged
+source. The new contribution is the incoming-write lower-bound argument,
+its arbitrary-workspace application and the independent lemma corroboration.
+Elementary binary linear algebra and CNOT circuits retain their classical
+status; no global literature-priority claim is made.
+
+Nick Petalas's older [PR4899](https://github.com/CrocSwap/integer-mult-bounds/pull/4899)
+prices weighted pair-mask tours; recent
+[PR6427](https://github.com/CrocSwap/integer-mult-bounds/pull/6427) prices
+fixed-weight tours. Both restrict the program to an anchor-tour alphabet.
+This result changes that hypothesis to arbitrary row CNOTs and proves a
+lower bound on PR2271's original boundary. It does not take another mask
+family in those restricted models.
+
+The bit-helper-contract card is explicitly changed to this local algebraic
+side result in [TASK.json](TASK.json). Canonical base is
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8.
+The selected-binding positive control passed for selected PR6030; it is
+metadata orientation, not a selected scientific replay.
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371190).
+Live PRs, recent account contributions, handoff claims, reservations,
+all-main README and merged-PR searches were checked. Sparse notes,
+unpublished work and arbitrary historical code diffs remain coverage limits.
+
+This does not supply a physical caller, bit-coordinate mixing optimum,
+native implementation, routing/tape bound, precision/stock ledger, recursive
+invoice, supplier admission, new kappa or selected-frontier change. All five
+framework assumptions remain. Clean inputs, free basis changes, nonlinear
+instructions and input-dependent programs are outside the theorem. No
+predecessor scientific suite, selected cold replay, Lean or Docker build
+was run. Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Does the minimum survive one initially clean, zero-return row? Begin with
+  this exact endpoint and charge initialization and restoration. The dirty
+  invertibility argument does not cover the changed initial condition.
+- Can an actual supplier use this boundary after complete physical costs?
+  First identify a literal common-frame occurrence, then price its source
+  references, movement, native work and restoration. No such occurrence or
+  full recursive invoice is supplied here.
+
+Structured first steps and blockers are in TASK.json. No broader search is
+needed to obtain this first strengthening.
+
+## Verifier bounds
+
+The interpreter caps rows at eight and word length at twelve. Exhaustive
+word loops have respectively at most 6^6 and 8*6*4^4 iterations. Prefix
+storage has at most thirteen states of eight coefficients. Every function
+is below sixty physical lines; there is no recursion, subprocess, network,
+dynamic execution or predecessor import. Explicit guards remain enabled
+under optimization. Source reads are capped at 256 KiB for each of six
+files. The direct command has no output-file path or mutable external state.
+Warning-strict normal/optimized execution and source compilation are the
+available Python diagnostics.
+
+Power of Ten rule 3 deviation: CPython and its standard library dynamically
+allocate arithmetic values, tuples and iterator states. Scope is this
+terminating, fixed-domain verifier. Fixed enumeration limits and one current
+word bound live data; no allocator-internals or steady-service guarantee is
+claimed. Both registered commands exercise the capacities and rejection
+controls. A fixed-allocation runtime would be needed before reusing this
+code under a no-allocation execution contract.

research/global-thirteen-add-fanout/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/borrowed-source-gray-mask-fanout-seed9b2fe133/README.md",
+      "usage": "provenance",
+      "git_blob": "32c2ea04e8e25c5a199861d8e0906127ffd9a5ce",
+      "sha256": "fb81510e09747ea2917318d23b667edaca28e09535b9a833e221672b9910f8f4"
+    }
+  ]
+}