Skip to content

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

Open
petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w14-1022ac-connected-xor-word-floor
Open

petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w14-1022ac-connected-xor-word-floor

Conversation

@petalas

@petalas petalas commented Oct 27, 2026 •

Copy link
Copy Markdown
Contributor

Result

Any 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, every connected restored word needs at least 2(n-1) XORs, for every n. Doubling the edges of any spanning tree attains the bound. This answers Open next question 2 of ywz65's #2455 (research/mutable-source-six-query-xor).

Claim type: scoped written mathematical proof with finite exact corroboration. No new κ. The selected frontier is unchanged.

The proof in research/connected-xor-word-floor/PROOF.md has 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 this means L >= |targets| + |sources|.
  2. Induction. If some label is only a target or only a source, delete its calls. The rest is a restored word on n-1 labels. Each component left behind needs at least two calls to or from the deleted label, because one nonzero contribution cannot cancel. Otherwise every label is both a source and a target, and step 1 gives L >= 2n.

The argument covers overlapping interactions and odd-length identities, such as the five-call commutator word on three labels. It uses no edge-count or parity argument.

Connector consequence. Assume #2455's component inequality Q >= n + c, which that package proves for five sources. Then X >= 2(n-c) >= 2(2n-Q) for n+1 <= Q <= 2n. At five sources this recovers #2455's X >= 8 at Q=6 and #2643's sharp X >= 6 at Q=7. It also gives X >= 4 at Q=8 and X >= 2 at Q=9. At Q = n+1 it gives X >= 2(n-1).

Evidence and reproduction

verify.py uses only the standard library and reads no predecessor files. It enumerates every word on one to five labels by meet-in-the-middle, keeping each frame matrix with every directed arc set that reaches it. It joins full lengths through 2, 4, 6, 8 and 8. 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 2(n-1) and that the floor is attained at every even length up to there. It also checks star and path words through 12 labels, the odd commutator identity, and six semantic controls. At five labels, the fewest components at lengths 0–8 are 5, –, 4, –, 3, 3, 2, 2, 1, and length 8 has 7,705 connected restored arc sets. Three disposable mutants were rejected: a strengthened component floor, a strengthened rank lemma, and a wrong connected minimum.

From the repository root (local CPython 3.12.15, macOS arm64):

/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

All four commands pass locally. The two registered commands each took 0.12 s, against a 120 s timeout. Any CPython 3.12 can replace the interpreter path.

Limitations

  • The all-n theorem rests on the written proof. The census covers at most five labels. No Lean or other proof-kernel check was run, and no independent human review is claimed.
  • For n != 5, the connector corollary assumes Prove eight source XORs are necessary at the six-query endpoint #2455's component inequality at that source count. That inequality is cited, not re-proved or audited.
  • Tariff optimality at other query counts, physical common-B source access, native, precision and hosting costs, and supplier admission are out of scope.
  • The extension to calls x_t += a x_s with a != 0 over any field is written-proof only.

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, and five labels were only joined through length 8.
  • Can X >= 2(2n-Q) raise Research: 7–9Q mutable-source invoices cannot beat six-query tariff 436 #2677's eight- and nine-query tariff floors? Those floors use X >= 0 in a path-lowered class. First the two results need a common model.

Related open work

No open PR studies connected restored source-XOR words or the mutable-source connector's XOR count. The merged predecessors are #2455, #2643, #2677, #1898 and #1340.

Credit

ywz65 (#2455) for the question, the X-only reduction, the component inequality and the five-label census. Arham Tahir (#1898, #1340, #1370) for the connector, the paid source-XOR alphabet and the eight-XOR construction. VictorLiwentao (#2643, #2677) for the seven-query floor and invoices. Base: canonical main 19fdb086ea96af9a9f87936a2b888e10af4ed810, priority revision 8. Advance claim: #1166 (comment)

CI notes

Head 9e8f632cd1eece10d294b10d7ee13e7ca92d26a6: all checks passed in run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40523982229. plan passed (4m40s) and replay (research/connected-xor-word-floor) passed (1m33s).

A restored F2 source-XOR word whose interaction graph has c components
on n labels has at least 2(n-c) calls. A rank lemma for products of
rank-one updates gives L >= |targets| + |sources|. Induction removes a
pure source or pure target. Doubled spanning trees attain the bound.
Under the component inequality of PR CrocSwap#2455 this gives X >= 2(2n-Q),
answering that package's all-n open question.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant