diff --git a/research/connected-xor-word-floor/PROOF.md b/research/connected-xor-word-floor/PROOF.md new file mode 100644 index 0000000000..c12325a479 --- /dev/null +++ b/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. diff --git a/research/connected-xor-word-floor/README.md b/research/connected-xor-word-floor/README.md new file mode 100644 index 0000000000..2909053eaf --- /dev/null +++ b/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. diff --git a/research/connected-xor-word-floor/SOURCES.json b/research/connected-xor-word-floor/SOURCES.json new file mode 100644 index 0000000000..4acb4e09e8 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/connected-xor-word-floor/TASK.json b/research/connected-xor-word-floor/TASK.json new file mode 100644 index 0000000000..0e9a0995f9 --- /dev/null +++ b/research/connected-xor-word-floor/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "All-n lower bound for restored F2 source-XOR words: L >= 2(n - c), so a connected restored word on n labels needs at least 2(n-1) calls, with attaining words for every n; plus the connector consequence X >= 2(2n-Q) under PR #2455's component inequality.", + "scope_change_reason": "This keeps PR1340's paid source-XOR alphabet and removes the source-count restriction, which the card lists as a scope-change trigger. It answers Open next question 2 of ywz65's PR #2455, which asks for exactly this all-n theorem to settle the minimum-query source-XOR question left by PR #1898.", + "bottleneck_link": "Side result: the source-restoration bill of the mutable-source connector becomes a closed-form floor at every source and query count, before any unequal-price tariff search. No supplier, alphabet extension or physical common-B access is established.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified written theorem with attaining words and an exhaustive small-label corroboration. No tariff search or new connector construction.", + "outcome": "completed", + "evidence": "PROOF.md proves L >= |T|+|S| for restored words (rank-one product lemma) and L >= 2(n-c) by induction removing a pure source or pure target. verify.py exhaustively joins every restored word for one to five labels (through lengths 2, 4, 6, 8 and 8), checks both inequalities on every restored directed arc set, confirms the first connected length 2(n-1), and checks star/path attaining words through twelve labels.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact minimum length of a connected restored source-XOR word of odd length on n labels?", + "why_it_matters": "Odd restored words exist; their minimum decides which odd X counts can occur at the minimum query endpoint.", + "first_step": "The theorem gives at least 2n-1; the census attains it with length five on three labels and seven on four labels; five labels were joined only through length eight. Test whether 2n-1 is attained for every n >= 3.", + "blocked_by": "The proof bounds the length from below but constructs only even attaining words." + }, + { + "question": "Does the floor X >= 2(2n-Q) combine with the readout floors of PR #2677 to raise the 8- and 9-query tariff floors?", + "why_it_matters": "PR #2677 records only X >= 0 at eight and nine queries in its path-lowered class; X >= 4 and X >= 2 could raise those floors.", + "first_step": "Bind the n-source component inequality and PR #2677's readout floors to one shared model, then add the XOR term.", + "blocked_by": "The readout floors belong to a different schedule class; this package does not establish that they hold together with the XOR floor." + } + ], + "claim_type": "scoped-proof", + "coordination": { + "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19219151", + "question_source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2455", + "source_author": "ywz65" + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "selection": { + "selected_task": "connector-alphabet-change", + "first_step": "research/universal-connector-boundary/verify.py returned PASS_UNIVERSAL_CONNECTOR_BOUNDARY pairings=945 max_coverage=31; research_selected_baseline.py returned PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "overlap_scope": "Live open PR titles, account PRs, latest handoff comments; cached card search with complete remote pagination and sparse local omissions; committed README Git searches and merged PR searches for six-query XOR, connected restored shear and mutable-source terms. Arbitrary code diffs and unpublished work are not fully covered." + }, + "freshness": { + "upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "checked_at_utc": "2026-10-27T14:42:34.979227+00:00", + "decision": "Continue completed scoped theorem. Canonical main is unchanged since entry; no live PR or claim targets the all-n connected restored XOR-word floor." + } +} diff --git a/research/connected-xor-word-floor/VERIFY.json b/research/connected-xor-word-floor/VERIFY.json new file mode 100644 index 0000000000..a01d5d2196 --- /dev/null +++ b/research/connected-xor-word-floor/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": "Exhaustive restored-word census for one to five labels (lengths through 2,4,6,8,8), the rank lemma L>=|T|+|S| and floor c>=n-floor(L/2) on every restored arc set, first connected length 2(n-1), attaining star/path words through twelve labels, the odd commutator identity and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete checks with Python assertions disabled." + } + ] +} diff --git a/research/connected-xor-word-floor/verify.py b/research/connected-xor-word-floor/verify.py new file mode 100644 index 0000000000..6f5a0a6f83 --- /dev/null +++ b/research/connected-xor-word-floor/verify.py @@ -0,0 +1,177 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the connected restored XOR-word floor. + +Produced by Nick Petalas. Apache-2.0. +No predecessor executable or external scientific input is imported. +""" + +import hashlib +import json +from pathlib import Path +import sys + + +PACKAGE_FILES = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") +# Census widths and the largest full word length joined at each width. +CENSUS = ((1, 2), (2, 4), (3, 6), (4, 8), (5, 8)) +MAX_STAR_LABELS = 12 + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def arcs(n: int) -> tuple[tuple[int, int], ...]: + need(type(n) is int and 1 <= n <= MAX_STAR_LABELS, "unsupported label count") + return tuple((s, t) for t in range(n) for s in range(n) if s != t) + + +def apply(rows: tuple[int, ...], s: int, t: int) -> tuple[int, ...]: + """X_(s,t): x_t += x_s, acting on the rows of the source frame.""" + need(0 <= s < len(rows) and 0 <= t < len(rows) and s != t, "bad XOR call") + out = list(rows) + out[t] ^= rows[s] + return tuple(out) + + +def identity(n: int) -> tuple[int, ...]: + return tuple(1 << i for i in range(n)) + + +def components(n: int, arc_mask: int, table: tuple[tuple[int, int], ...]) -> int: + parent = list(range(n)) + + def root(v: int) -> int: + for _ in range(n): + if parent[v] == v: + return v + v = parent[v] + raise ValueError("union-find did not terminate") + + for k, (s, t) in enumerate(table): + if arc_mask >> k & 1: + parent[root(s)] = root(t) + return len({root(v) for v in range(n)}) + + +def endpoint_counts(arc_mask: int, table: tuple[tuple[int, int], ...]) -> tuple[int, int]: + used = [arc for k, arc in enumerate(table) if arc_mask >> k & 1] + return len({t for _, t in used}), len({s for s, _ in used}) + + +def half_layers(n: int, depth: int) -> list[dict[tuple[int, ...], set[int]]]: + """Every (frame matrix, used directed-arc set) reachable in exactly k calls.""" + table = arcs(n) + layers = [{identity(n): {0}}] + for _ in range(depth): + nxt: dict[tuple[int, ...], set[int]] = {} + for rows, masks in layers[-1].items(): + for k, (s, t) in enumerate(table): + bucket = nxt.setdefault(apply(rows, s, t), set()) + bucket.update(mask | 1 << k for mask in masks) + layers.append(nxt) + return layers + + +def census(n: int, max_length: int) -> dict[str, object]: + table = arcs(n) + layers = half_layers(n, (max_length + 1) // 2) + rows_out = [] + for length in range(max_length + 1): + left, right = layers[length // 2], layers[(length + 1) // 2] + graphs: set[int] = set() + for rows, masks in left.items(): + for other in right.get(rows, ()): + graphs.update(mask | other for mask in masks) + fewest = None + for mask in graphs: + c = components(n, mask, table) + targets, sources = endpoint_counts(mask, table) + need(length >= targets + sources, "rank lemma L >= |T|+|S| fails") + need(c >= n - length // 2, "component floor c >= n - floor(L/2) fails") + fewest = c if fewest is None else min(fewest, c) + rows_out.append({"length": length, "restored_arc_sets": len(graphs), "fewest_components": fewest}) + first_connected = next((r["length"] for r in rows_out if r["fewest_components"] == 1), None) + if n == 1: + need(first_connected == 0, "single label must be connected by the empty word") + elif max_length >= 2 * (n - 1): + need(first_connected == 2 * (n - 1), "connected minimum is not 2(n-1)") + for r in rows_out: + if r["length"] % 2 == 0 and r["length"] <= 2 * (n - 1): + need(r["fewest_components"] == n - r["length"] // 2, "even-length floor is not attained") + return { + "labels": n, + "max_length": max_length, + "half_layer_states": [sum(len(v) for v in layer.values()) for layer in layers], + "lengths": rows_out, + "first_connected_length": first_connected, + } + + +def run_word(n: int, word: list[tuple[int, int]]) -> tuple[bool, int]: + rows = identity(n) + mask = 0 + index = {arc: k for k, arc in enumerate(arcs(n))} + for s, t in word: + rows = apply(rows, s, t) + mask |= 1 << index[(s, t)] + return rows == identity(n), components(n, mask, arcs(n)) + + +def attaining_words() -> dict[str, object]: + checked = [] + for n in range(2, MAX_STAR_LABELS + 1): + star = [(0, i) for i in range(1, n) for _ in range(2)] + path = [(i, i + 1) for i in range(n - 1) for _ in range(2)] + for word in (star, path): + restored, c = run_word(n, word) + need(restored and c == 1 and len(word) == 2 * (n - 1), "attaining word fails") + checked.append(n) + commutator = [(1, 0), (2, 1), (1, 0), (2, 1), (2, 0)] + restored, c = run_word(3, commutator) + need(restored and c == 1, "odd commutator identity fails") + return {"star_and_path_labels": checked, "odd_commutator_length": len(commutator)} + + +def controls() -> int: + passed = 0 + restored, c = run_word(3, [(0, 1), (1, 2), (0, 1), (1, 2)]) + need(c == 1 and not restored, "connected nonrestored control") + passed += 1 + restored, c = run_word(3, [(0, 1), (0, 1)]) + need(restored and c == 2, "restored disconnected control") + passed += 1 + restored, c = run_word(3, [(0, 1), (1, 2), (2, 0)]) + need(not restored and c == 1, "three-cycle control") + passed += 1 + for bad in ((0, 0), (0, 3), (-1, 1)): + try: + apply(identity(3), *bad) + except ValueError: + passed += 1 + else: + raise ValueError("malformed call accepted") + return passed + + +def package_hashes() -> dict[str, str]: + root = Path(__file__).resolve().parent + return {name: hashlib.sha256((root / name).read_bytes()).hexdigest() for name in PACKAGE_FILES} + + +def main() -> int: + results = [census(n, length) for n, length in CENSUS] + receipt = { + "census": results, + "attaining": attaining_words(), + "controls_passed": controls(), + "package_sha256": package_hashes(), + } + print("PASS_CONNECTED_XOR_WORD_FLOOR") + print(json.dumps(receipt, indent=1, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + sys.exit(main())