Prove connected restored source-XOR words need 2(n-1) calls (no new κ)

research/connected-xor-word-floor/PROOF.md

@@ -0,0 +1,143 @@
+# Proof: connected restored XOR words need 2(n-1) calls
+
+Produced by Nick Petalas. Apache-2.0.
+
+## Model
+
+Labels form a finite set `V` with `|V| = n`. Each label holds a value in a
+vector space over F2; write `x` for the column of all values. The only call is
+
+    X_(s,t):  x_t += x_s,   s != t,
+
+whose matrix is `I + e_t e_s^T`. A word `w = g_1 ... g_L` applies `g_1`
+first, so its matrix is `M(w) = G_L ... G_1`. It is **restored** when
+`M(w) = I`. Its **interaction graph** `G(w)` is the undirected multigraph on
+`V` with one edge `{s,t}` for every call, including calls whose effect later
+cancels. Write `c(w)` for its number of components, counting isolated labels.
+Call `t` a target and `s` a source of the call. Let `T(w)` and `S(w)` be the
+sets of labels that occur as a target and as a source respectively.
+
+This is the source-XOR projection used by PR #2455: Q and R calls never change
+sources, so every restored connector word has a restored X-only projection.
+
+## Lemma 1 (rank-one product identity)
+
+Over any field, let `u_k, v_k` be column vectors and suppose
+
+    (I + u_L v_L^T) ... (I + u_1 v_1^T) = I.
+
+Then `L >= rank U + rank V`, where `U = [u_1 ... u_L]` and
+`V = [v_1 ... v_L]`.
+
+*Proof.* Let `P_k` be the product of the first `k` factors. By induction,
+`P_k = I + U_k N_k V_k^T`, where `U_k` and `V_k` hold the first `k` columns
+and `N_k` is `k`-by-`k` lower triangular with unit diagonal. The case `k=0`
+is empty. For the step,
+
+    P_k = P_(k-1) + u_k v_k^T P_(k-1)
+        = I + U_(k-1) N_(k-1) V_(k-1)^T + u_k (v_k^T + v_k^T U_(k-1) N_(k-1) V_(k-1)^T),
+
+so `N_k` is `N_(k-1)` bordered by the row `v_k^T U_(k-1) N_(k-1)`, a zero
+column and a final diagonal entry one. Hence `N = N_L` is invertible and
+`U N V^T = 0`. Sylvester's rank inequality for the `L`-column `U` and the
+`L`-row `N V^T` gives
+
+    0 = rank(U N V^T) >= rank U + rank(N V^T) - L = rank U + rank V - L.  □
+
+For a restored XOR word, `u_k = e_(t_k)` and `v_k = e_(s_k)`, so
+
+    L >= |T(w)| + |S(w)|.                                             (1)
+
+## Theorem
+
+Every restored word satisfies `L >= 2(n - c(w))`. In particular, a restored
+word whose interaction graph is connected has at least `2(n-1)` calls.
+
+*Proof.* Strong induction on `n`. For `n=1` there is no call and the bound is
+`0`.
+
+**Disconnected graphs.** If `c(w) >= 2`, each call acts inside one component.
+Calls in different components act on disjoint coordinates and commute, so
+`M(w)` is block diagonal with block `M(w_i)`, where `w_i` is the subword of
+calls inside component `C_i`. Restoration of `w` is restoration of every
+`w_i`. Each `w_i` is connected on `n_i < n` labels, so by induction
+`L = sum_i |w_i| >= sum_i 2(n_i - 1) = 2(n - c(w))`.
+
+**Connected graphs, n >= 2.** Every label is an endpoint of some call, so
+`T ∪ S = V`. There are three cases.
+
+*Case A: T = S = V.* Inequality (1) gives `L >= 2n > 2(n-1)`.
+
+*Case B: some label v is not a source.* Then `v` is a target only. No call
+reads `x_v`, so deleting every call into `v` leaves a word `w'` on `V \ {v}`
+whose action on those labels equals that of `w`. Thus `w'` is restored. Let
+`C_1, ..., C_m` be the components of `G(w') = G(w) - v`. By the disconnected
+case and induction, `|w'| >= 2(n - 1 - m)`.
+
+Every call of `w'` stays inside one `C_i`, so at all times the value of any
+label in `C_i` is a linear form in the initial values of `C_i` alone. Since
+the prefix matrices are invertible, that form is nonzero. The final value of
+`x_v` is `x_v + sum_k l_k`, where `l_k` is the value of the source of the
+`k`-th call into `v` when it is made. Restoration requires `sum_k l_k = 0`.
+The coordinate spaces of distinct `C_i` are independent, so the sum over calls
+whose source lies in `C_i` vanishes for each `i`. Since `G(w)` is connected,
+each `C_i` sends at least one call into `v`. One nonzero form cannot sum to
+zero, so each `C_i` sends at least two. The degree of `v` is at least `2m`
+and
+
+    L = |w'| + deg(v) >= 2(n - 1 - m) + 2m = 2(n-1).
+
+*Case C: some label v is not a target.* Then `x_v` never changes. Order the
+coordinates as `(V \ {v}, v)`. Every call matrix has the block form
+`[[A_k, b_k], [0, 1]]`. A call `X_(v,t)` has `A_k = I` and `b_k = e_t`; every
+other call has `b_k = 0` and `A_k` equal to its matrix on `V \ {v}`. The
+product is `[[A_L ... A_1, b], [0, 1]]` with
+
+    b = sum over calls X_(v,t_k) of (A_L ... A_(k+1)) e_(t_k).
+
+Restoration therefore forces `A_L ... A_1 = I` and `b = 0`. The first
+equation says the word `w'` obtained by deleting the calls out of `v` is
+restored, so `|w'| >= 2(n - 1 - m)` as in Case B, with `C_1, ..., C_m` the
+components of `G(w) - v`. Every `A_j` is block diagonal over these components
+and `e_(t_k)` lies in the block of the component containing `t_k`. So the
+`C_i` block of `b` is a sum of the vectors `(A_L ... A_(k+1)) e_(t_k)` over
+calls with `t_k ∈ C_i`. Each such vector is nonzero, because the matrix is
+invertible. Connectivity gives at least one call from `v` into each `C_i`,
+and a vanishing block needs at least two. Again `deg(v) >= 2m` and
+`L >= 2(n-1)`.
+
+If Case A fails, some label lies outside `S` or outside `T`, so Cases A–C are
+exhaustive.  □
+
+## Sharpness and consequences
+
+The bound is attained for every `n`. The star word that applies each
+`X_(0,i)` twice, and the path word that applies each `X_(i,i+1)` twice, are
+restored, connected, and of length `2(n-1)`. Doubling the edges of any forest
+with `k <= n-1` edges gives a restored word of length `2k` with exactly
+`n - k` components, so `c >= n - floor(L/2)` is attained at every even
+`L <= 2(n-1)`.
+
+The theorem covers overlapping interactions and odd lengths. For example,
+`X_(1,0) X_(2,1) X_(1,0) X_(2,1) X_(2,0)` is the commutator identity
+`[E_01, E_12] = E_02` read as a restored connected word of length five on
+three labels. It satisfies the bound `5 >= 4`. No parity argument is used.
+
+**Corollary (connector source-XOR floor).** Assume the component inequality
+`Q >= n + c` of PR #2455 for a restored `n`-source common-B mutable-source
+connector word with `Q` queries, where `c` is the number of components of its
+source interaction graph. PR #2455 states and proves that inequality for five
+sources; it is cited here, not re-proved or audited. Then the word's source-XOR
+count satisfies
+
+    X >= 2(n - c) >= 2(2n - Q),   for n + 1 <= Q <= 2n.
+
+At `n = 5` this gives `X >= 8` at `Q = 6`, matching the census theorem of
+PR #2455, and `X >= 6` at `Q = 7`, matching the sharp floor of PR #2643. It
+also gives `X >= 4` at `Q = 8` and `X >= 2` at `Q = 9`. At the minimum query
+count `Q = n + 1`, the interaction graph is connected and `X >= 2(n-1)`.
+
+**Remark (other fields).** Lemma 1 is stated over any field. The induction
+uses only that the call coefficient is nonzero and that prefix matrices are
+invertible, so the theorem holds verbatim for calls `x_t += a x_s` with
+`a != 0` over any field. The finite verifier checks only F2.

research/connected-xor-word-floor/README.md

@@ -0,0 +1,126 @@
+# Connected restored source-XOR words need 2(n-1) calls
+
+Every restored word of source XORs `x_t += x_s` over F2 on `n` labels whose
+interaction graph has `c` components has at least `2(n-c)` calls. In
+particular, a connected restored word needs at least `2(n-1)` XORs, for every
+`n`. Doubling any spanning tree's edges attains the bound.
+
+Claim type: scoped written mathematical proof with finite exact corroboration.
+This contribution was produced by Nick Petalas. Apache-2.0. Independent human
+and formal proof-kernel review are unclaimed. No new κ is claimed.
+
+[PROOF.md](PROOF.md) gives the complete argument in two steps:
+
+1. **Rank lemma.** If a product of `L` rank-one updates `I + u_k v_k^T` is the
+   identity over any field, then `L >= rank U + rank V`. For XOR words,
+   `L >= |targets| + |sources|`. So a word in which every label is both a
+   source and a target has at least `2n` calls.
+2. **Induction.** Otherwise some label is only a target or only a source.
+   Deleting its calls leaves a restored word on `n-1` labels. Each component
+   of the remaining graph needs at least two calls to or from the deleted label,
+   because one nonzero contribution cannot cancel.
+
+The theorem covers overlapping interactions and odd-length identities. One
+example is the five-call commutator word on three labels. Neither a graph edge
+count nor a parity argument is used.
+
+## Consequence for the mutable-source connector
+
+PR #2455 shows that a restored common-B mutable-source word with `Q` queries
+has `Q >= n + c`. Here `c` is the number of components of its source
+interaction graph. PR #2455 proves this for five sources, and that result is
+cited, not audited. Under that inequality, the theorem gives
+
+    X >= 2(n - c) >= 2(2n - Q),   n + 1 <= Q <= 2n.
+
+At five sources this recovers PR #2455's `X >= 8` at six queries and
+PR #2643's sharp `X >= 6` at seven queries. It also gives `X >= 4` at eight
+queries and `X >= 2` at nine. At the minimum query count `Q = n+1`, the
+graph is connected and `X >= 2(n-1)`, which is PR #2455's Open next question 2.
+The proof also works unchanged for calls `x_t += a x_s` with `a != 0` over any
+field. That extension is written-proof only.
+
+## Evidence and reproduction
+
+The read-only standard-library verifier enumerates every word on one to five
+labels by meet-in-the-middle. It keeps each frame matrix together with every
+directed arc set that reaches it. Every generator is an involution, so a word
+`u reverse(v)` is restored exactly when `M(u) = M(v)`. Joining equal matrices
+therefore enumerates every restored arc set of each length. The verifier joins
+full lengths through 2, 4, 6, 8 and 8 for one through five labels. On every
+restored arc set it checks `L >= |T| + |S|` and `c >= n - floor(L/2)`. It
+confirms that the first connected restored length is exactly `2(n-1)`, and
+that the floor is attained at every even length up to `2(n-1)`. It also
+checks the star and path words through twelve labels, the odd commutator
+identity, and six semantic controls.
+
+The local CPython 3.12.15 run passes. At five labels, the half-layers hold
+1, 20, 280, 3,330 and 36,110 matrix/arc-set states. The joins give 7,705
+connected restored arc sets at length eight and none shorter. The fewest
+components at lengths 0 to 8 are 5, –, 4, –, 3, 3, 2, 2, 1. Each registered
+command took about 0.1 seconds locally, far below its 120-second limit.
+
+From the repository root, run:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/connected-xor-word-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/connected-xor-word-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/connected-xor-word-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/connected-xor-word-floor --check-source-history
+```
+
+Any CPython 3.12 executable may replace this installation path. A direct run
+prints `PASS_CONNECTED_XOR_WORD_FLOOR`, followed by a generated JSON receipt
+with every census count and the SHA256 of all six package files. Save stdout
+outside the checkout. No scientific receipt is handwritten. The verifier reads
+no predecessor files at runtime.
+
+## Sources, scope and stopping decision
+
+The question is Open next question 2 of ywz65's
+[PR #2455](https://github.com/CrocSwap/integer-mult-bounds/pull/2455),
+`research/mutable-source-six-query-xor`. That package supplies the X-only
+reduction, the component inequality and the five-label census through length
+seven. Arham Tahir's PR #1898 and PR #1340 supply the connector, the paid
+source-XOR alphabet and the eight-XOR construction. VictorLiwentao's PR #2643
+supplies the seven-query floor. These results are cited, not re-verified.
+Exact source blobs are pinned in SOURCES.json.
+
+The base is canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`,
+priority revision eight. The card's first-step control and the
+selected-baseline metadata control both passed. The card scope is changed:
+the alphabet is kept and the source-count restriction is removed, which the
+card lists as a scope-change trigger. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19219151)
+records this scope. The work stopped at the first verified theorem.
+
+The selected frontier is unchanged. Tariff optimality at other query counts,
+physical common-B source access, native/precision/hosting costs, supplier
+admission and the complete multiplication theorem are outside scope. The
+connector corollary for `n != 5` assumes PR #2455's component inequality at
+that source count. No Lean, Docker or historical scientific replay is run.
+
+## Open next questions
+
+- What is the minimum odd length of a connected restored word? The theorem
+  gives at least `2n-1`. The census attains it at three and four labels, with
+  lengths five and seven. Five labels were joined only through length eight.
+  First test whether `2n-1` is attained for every `n >= 3`. This matters
+  because it decides which odd X counts occur at the minimum-query endpoint.
+- Can the floor `X >= 2(2n-Q)` raise the eight- and nine-query tariff floors
+  of PR #2677? That package records only `X >= 0` there for its path-lowered
+  class. First bind the component inequality and those readout floors to one
+  shared model. This package does not establish that they hold together.
+
+Structured questions and blockers are in TASK.json.
+
+## Verifier implementation limits
+
+All loops have fixed finite domains: at most five labels in the census, at
+most twelve in the attaining-word checks, and half-length at most four. The
+largest live table has 36,110 states. Union-find has an explicit iteration
+bound, and nothing is recursive. There is no subprocess, network access or
+scientific output write. Python allocates bounded tuples, sets and dicts, so
+static allocation is unavailable. Functions are under sixty lines. Explicit
+`ValueError` checks still run under `-O`, and the registered commands treat
+warnings as errors. Package hashing reads exactly six package files.

research/connected-xor-word-floor/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "research/mutable-source-six-query-xor/README.md",
+      "usage": "provenance",
+      "git_blob": "d1db576cf0b5db76c5b5f5485938c08601548db1",
+      "sha256": "4ef8ed96b2e12f94f51f9a10f2cd894c32f9c821efd024bf26921521c513bf84"
+    },
+    {
+      "path": "research/mutable-source-six-query-xor/TASK.json",
+      "usage": "provenance",
+      "git_blob": "2088e3dc7f74b92b22db9fd0e3127ed1344c2df4",
+      "sha256": "422d07bb303f0268e53aeaf2d9499726bd5a3508ebb277ff7d24960bab70bed2"
+    },
+    {
+      "path": "research/seven-query-xor-floor/README.md",
+      "usage": "provenance",
+      "git_blob": "0f65aa7bc2019f4012dbcf8129662d118b576095",
+      "sha256": "06d772eb54cc0ed3eee796209e5938343baea3cc19e27ff3dcb4dbab5687eed2"
+    },
+    {
+      "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"
+    }
+  ]
+}