diff --git a/research/five-source-toggle-frontier/README.md b/research/five-source-toggle-frontier/README.md new file mode 100644 index 0000000000..c8bc87cb0e --- /dev/null +++ b/research/five-source-toggle-frontier/README.md @@ -0,0 +1,179 @@ +# Five sources: no toggle alphabet beats the DUO point (72 queries, 74 additions) + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped written proof with exact finite corroboration. No new κ, no supplier, no +selected-frontier change.** It answers the open question of +[PR3321](https://github.com/CrocSwap/integer-mult-bounds/pull/3321) +(`research/quint-toggle-connector`): can two all-five toggle calls (Q5), or a mixed +Q5/DUO/TRIO alphabet, give a new priced point on the five-source, 31-output connector +batch? + +## Setting + +The interface is that of `research/universal-connector-boundary` (PR943): five read-only +sources, one arbitrarily dirty connector `z`, 31 dirty output rows, readouts +`A_m: y_m += A_m z`. Here **every nonempty source subset `S` is available as one complete +call** `T_S: z += sum_{j in S} B_j x_j`, charged one dispatch plus `|S|` source additions, +with no surcharge (the same favorable ledger as PR3321). Readouts stay singleton calls. +A schedule has `Q` dispatches and `A` elementary additions; its price is `oQ + pA` with +`o >= 0`, `p > 0`. The singleton witness is `(Q, A) = (74, 74)` and the DUO witness of +[PR1531](https://github.com/CrocSwap/integer-mult-bounds/pull/1531) is `(72, 74)`. + +## Result + +**Theorem 1.** For any set of toggle calls, used any number of times, every correct +schedule has `Q >= 72` and `A >= 74`. The DUO word attains both bounds at once, so the +minimum price is `72o + 74p` for every `o >= 0`, `p > 0`, and `(72, 74)` is the only +Pareto point. No mixture and no number of Q5 calls can improve it. + +**Theorem 2.** Every correct schedule that contains a weight-5 call has `A >= 78`, so its +price is at least `72o + 78p`, which is the DUO price plus `4p`. The bound is attained by +a word with one Q5, two DUOs and seven singletons (10 calls, 16 additions, `(72, 78)`). + +Consequences for PR3321's question: + +* One Q5 with singleton calls has no favorable point (PR3321). With DUO calls also + available, a Q5-containing schedule at `(72, 78)` **does** beat the singleton witness + `(74, 74)`, exactly when `o > 2p`. So a mixed alphabet creates a new priced point + relative to singletons plus Q5. +* It never beats the DUO point. For every `o >= 0`, `p > 0` the DUO schedule is cheaper + than any Q5-containing schedule by at least `4p`. Two or more Q5 calls give `A >= 80`. +* In the ledger that adds a surcharge `sigma` to each multi-source call, the DUO word has + two such calls and prices `72o + 74p + 2 sigma`, against `74o + 74p` for singletons. It + wins exactly when `sigma < o`. The Q5 witness has three multi-source calls and is + dominated at every `sigma >= 0`. + +## Proof + +*Reduction (PR943, specialized to identity maps with one-bit rows).* Let `q_t` be the +parity vector of the sources added after `t` calls. A schedule must restore `z`, so the +word of toggle vectors is a closed walk in `F_2^5`: `T` steps, `q_T = 0`, `W` total weight +(`W` is even). A row `m` read `r_m` times at boundaries `t_1..t_r` receives +`r_m A_m z_initial + A_m sum_i q_{t_i} . (B x)`, so correctness for dirty `z` forces `r_m` +even and `sum_i q_{t_i} = m`. Hence `r_m >= 2`, and `r_m = 2` only if `m = q_s XOR q_t` +for two boundaries. Let `D` be the set of nonzero differences of the prefix points and +`u = 31 - |D|`. Rows outside `D` need at least four readouts, so +`R >= 62 + 2u`, `Q = T + R`, `A = W + R`. + +*Lemma 1 (support).* `T + 2u >= 10`, with equality only if `T = 10`, the ten prefix +points are distinct and `u = 0`. Let `s` be the number of distinct prefix points, so +`T >= s` and `31 - u <= C(s, 2)`. No set of at most nine points of `F_2^5` has +`P + P = F_2^5` (counting for `s <= 8`; an exhaustive search for `s = 9`, below), so +`s <= 9` forces `u >= 1`. The values of `s + 2 u_min(s)` are 14 at `s = 8`, 11 at `s = 9`, +10 at `s = 10` and `s` beyond. This extends the full-coverage bound of +[PR4137](https://github.com/CrocSwap/integer-mult-bounds/pull/4137) to words that repair +missing rows with extra readouts. So `Q >= T + 62 + 2u >= 72`. + +*Lemma 2 (expansion).* Replace each call `T_S` by `|S|` consecutive singleton calls. The +result is a closed singleton word `w'` of length `W` whose boundaries include those of the +original, so `u(w') <= u(w)`. For a closed singleton word of length `L`, +`L + 2u >= 12`: a missing source leaves 16 rows uncovered; otherwise `L >= 10`; `L = 10` +means every source twice, and none of the 945 pairing words covers all 32 masks (best 31), +so `u >= 1`; `L >= 12` is immediate. Hence `A >= W + 62 + 2u(w) >= 74`. + +*Theorem 1.* Lemmas 1 and 2 give `Q >= 72` and `A >= 74`. The DUO word below attains +`(72, 74)`, which proves the price statement. Equality in `Q` forces `T = 10` and full +coverage. + +*Theorem 2.* Let a word have `k >= 1` weight-5 steps, so `W >= T + 4k`. With +`T + 2u >= 10`, `A >= W + 62 + 2u >= 72 + 4k`: this gives `A >= 80` for `k >= 2`. +For `k = 1` the same chain gives 76, and the cases below close the gap to 78. + +* `T >= 11`: `W >= T + 4 >= 15` and `W` is even, so `W >= 16`, `A >= 78`. +* `T <= 9`: `u >= 1`, `W >= 14` at `T = 9`, `A >= 14 + 62 + 2 = 78`; smaller `T` leaves + more rows uncovered (`u >= 3` at `T = 8`, giving `A >= 80`). +* `T = 10`: `W >= 16` gives 78. If `W = 14`, the other nine steps are singletons. Rotating + the closed word puts Q5 last, and closure makes every singleton count odd, so the counts + are `(5,1,1,1,1)` or `(3,3,1,1,1)`. The census below runs all 115,920 such words: at + most 27 of 31 differences, so `u >= 4` and `A >= 14 + 62 + 8 = 84`. + +The word `[1, 2, 1, 4, 2, 1, 8, 24, 10, 31]` (masks; 24 = `{3,4}`, 10 = `{1,3}`, 31 = Q5) has +ten distinct prefix points covering `F_2^5`, `W = 16`, so `(72, 78)`. It was found by an +exhaustive depth-first search over closed words with one Q5; the verifier replays it. + +## Evidence + +All counts are recomputed from the integers by `verify.py` (standard library; about 14 s): + +* **Cover numbers.** An exhaustive search with an exact waste cut finds no nine-point + cover; the affine-basis normal form (every cover contains an affine basis) agrees; the + same search finds 99,200 ten-point covers containing 0, the number recorded by + `research/duo-toggle-connector`, and the normal form finds 80. +* **Pairing census.** 945 length-ten singleton words; the coverage histogram equals the one + recorded by PR943 (`31` is the maximum, 22 words); minimum missing rows `u = 1`. +* **One weight-5 step.** 115,920 words; maximum 27 distinct nonzero differences. +* **Witnesses.** Both words build explicit 72-call schedules (62 readouts, rows at their + first boundary pair). Each is replayed twice: symbolically for arbitrary operators + (`z` and each row as formal combinations of `z_0` and `B_j x_j`) and concretely with + random binary maps and dirty data (150 trials each). The singleton 74-call word and + PR943's ten-call word with a four-readout repair pass the same replays as positive + controls; the ten-call word misses exactly mask 21, as PR943 states. +* **Tables and sanity.** The `T + 2u` table, the case checks for Theorem 2 over `T <= 40`, + 30,000 random closed words over all 31 toggles and a 6,000-step hill climb from the DUO + word, all above the floors (`Q >= 72`, `A >= 74`, `A >= 78` with a Q5). +* **Controls.** Dropped operations, a wrong row, an unclosed word, a truncated concrete + schedule, a four-step word claimed to reach 72, and a zero toggle are all rejected. + +## Reproduce + +From the repository root, CPython 3.12, standard library only: + +```sh +python3.12 -I -W error -B research/five-source-toggle-frontier/verify.py +python3.12 -I -O -W error -B research/five-source-toggle-frontier/verify.py +python3.12 -B scripts/research_package.py --package research/five-source-toggle-frontier +``` + +Expected first line: +`PASS_FIVE_SOURCE_TOGGLE_FRONTIER nine_point_covers=0 ten_point_covers=99200 ... +weight5_witness=(72,78) no_new_kappa`. + +## Limitations + +* The price model is the favorable ledger of PR3321: a multi-source call costs one + dispatch plus its additions, with no frame, routing or implementation surcharge. A real + surcharge only raises every schedule that uses such a call. No physical call, compiler + or supplier is established, and nothing here changes κ. +* The model is the binary-linear five-source, 31-row interface with singleton readouts. It + excludes joint readouts, extra connectors, mutable sources, frame changes and other + source counts. The all-alphabet claim is for source-side toggles only. +* The reduction to prefix differences is inherited from PR943 (necessity by the + identity-map specialization). The proofs are written, with finite exhaustive components + under the stated reductions. No proof assistant was run; independent human and formal + proof-kernel review are unclaimed. +* Weights 3 and 4 are not given an analogue of Theorem 2 here. +* Verifier discipline: no recursion, and every loop has an explicit finite bound. The cover + search enforces a 60,000,000-step limit against the 5,403,753 and 41,511,450 steps it + uses for nine and ten points. Python allocates integers and containers while it runs; + that managed-runtime deviation is confined to these bounded searches (explicit stacks of + depth at most 10 and a streamed 115,920-word census). + +## Open next questions + +1. What is the exact minimum price among schedules that contain a weight-3 or weight-4 + call? The expansion argument gives `A >= 74` there; existing packages bound single + TRIO and arity-four cases separately (`research/atomic-trio-connector`, the open + PR3909). A rerun of the depth-first search used for the Q5 witness, with one TRIO or + one weight-4 call and extra weight 2 to 6, would give the attained value. Nothing + blocks it. +2. Does the same single-point collapse hold for every alphabet at six sources? The open + [PR2249](https://github.com/CrocSwap/integer-mult-bounds/pull/2249) reports + `r((C2)^6) = 14` and the singleton minimum `f(6) = 16`, which would give `Q >= 140` and + `A >= 142`, attained by the six-source DUO word it cites. Rerunning the argument here with + those two invariants, and then a uniform statement for `n <= 6` from the least cover size + and the least singleton walk, is the next step. +3. Can a readout-side alphabet (joint outputs) move the 62-readout floor, which is 62 of + the 72 queries? Toggle-side extensions cannot: Theorem 1 closes them. + +## Credit + +Interface, singleton minimum 12 and the 945-pairing census: Ross Richardson, PR943 +(`research/universal-connector-boundary`). The DUO word and the ten-point cover count: navinor, +PR1531 (`research/duo-toggle-connector`). The support bound for steps of weight 1 to 5 at +full coverage: unpaidmoon, PR4137 (`research/connector-triple-query-floor`). The Q5 model, +the one-Q5 census and the question answered here: 1337isnot1337 (Cinna Davis), PR3321 +(`research/quint-toggle-connector`). All were used as cited inputs and recomputed as +controls; none was audited. New here: the partial-coverage form of the support bound, the +expansion bound `A >= 74` for every alphabet, the single-point frontier, the weight-5 +floor 78 and its attaining word. diff --git a/research/five-source-toggle-frontier/SOURCES.json b/research/five-source-toggle-frontier/SOURCES.json new file mode 100644 index 0000000000..30f2626542 --- /dev/null +++ b/research/five-source-toggle-frontier/SOURCES.json @@ -0,0 +1,72 @@ +{ + "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/connector-triple-query-floor/README.md", + "usage": "provenance", + "git_blob": "c290f6381de73f1b1868404544698ac08f72c9cd", + "sha256": "9c81c56e361bbf9e2f392dd61958493a79b194b9ec70913c548b1da501c05c81" + }, + { + "path": "research/duo-toggle-connector/CERTIFICATE.json", + "usage": "provenance", + "git_blob": "accffc014ce13993ddce723abd4256dc0c884e5b", + "sha256": "a1ad3af8bbc872a8abcf8df543267eb82cfa0ede8d581a30b6c751307bb4f267" + }, + { + "path": "research/quint-toggle-connector/README.md", + "usage": "provenance", + "git_blob": "26812fa19651f77a5ba0231d1d5e5da39e3a3f35", + "sha256": "215c3f8ef0325656c2d4fdff25f9ca1aa1263e203cbe004cf997862185563fe4" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "provenance", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ], + "mathematical_references": [ + { + "pr": 943, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/943", + "path": "research/universal-connector-boundary/README.md", + "author": "Ross Richardson", + "use": "Interface, prefix-difference reduction, singleton minimum 12 and the 945-pairing census (recomputed)." + }, + { + "pr": 1531, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1531", + "path": "research/duo-toggle-connector/CERTIFICATE.json", + "author": "navinor", + "use": "DUO word and the 99,200 ten-point covers (recomputed)." + }, + { + "pr": 4137, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4137", + "path": "research/connector-triple-query-floor/README.md", + "author": "unpaidmoon", + "use": "Support bound for steps of weight 1 to 5 at full coverage." + }, + { + "pr": 3321, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3321", + "path": "research/quint-toggle-connector/README.md", + "author": "1337isnot1337", + "use": "Q5 model, one-Q5 census (recomputed) and the open question answered here." + } + ] +} diff --git a/research/five-source-toggle-frontier/TASK.json b/research/five-source-toggle-frontier/TASK.json new file mode 100644 index 0000000000..bc1dbd137d --- /dev/null +++ b/research/five-source-toggle-frontier/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Prove that no toggle alphabet, meaning any mixture of multi-source calls used any number of times, improves on the DUO point (72 queries, 74 additions) for the five-source, 31-row connector batch, and give the exact floor of 78 additions, attained, for schedules that contain a weight-5 call.", + "scope_change_reason": "The card asks whether one explicit alphabet extension offers a favorable budget. PR3321's open question asks about two Q5 calls or a mixed Q5/DUO/TRIO alphabet. The support and expansion bounds do not depend on which toggles are available, so the question is answered here for every nonempty-subset alphabet at once.", + "bottleneck_link": "The five-source connector costs 72 or 74 calls, of which 62 are readouts. Toggle-side alphabet extensions cannot lower it below the DUO point, so a further gain at this interface must change the readout side, the source count or the interface itself.", + "budget_minutes": 60, + "stop_rule": "Stop when the all-alphabet floors and the weight-5 floor are proved with attaining words. Do not extend to six or seven sources or to readout-side extensions.", + "outcome": "negative-result", + "evidence": "Written proof in README.md. verify.py recomputes the cover numbers (no nine-point cover; 99,200 ten-point covers), the 945-pairing census, the 115,920-word weight-5 census, two attaining 72-call schedules with generic-operator and concrete replays, the inequality tables, a hill climb and nine rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact minimum price among schedules that contain a weight-3 or weight-4 call?", + "why_it_matters": "Theorem 2 fixes the weight-5 value 72o + 78p; the other arities are only bounded by separate single-call packages.", + "first_step": "Rerun the depth-first search for a closed ten-step word with one TRIO or one weight-4 call and extra weight 2 to 6.", + "blocked_by": "Nothing." + }, + { + "question": "Does the single-point collapse (least cover size, least singleton walk) hold for every alphabet at six sources?", + "why_it_matters": "The open PR2249 reports r((C2)^6) = 14 and f(6) = 16, which would give (140, 142) for every alphabet.", + "first_step": "Rerun the support and expansion arguments with those two invariants and the six-source DUO word.", + "blocked_by": "The invariants are cited from an unmerged package; a six-point-set census is heavier than the five-source scan." + }, + { + "question": "Can a readout-side alphabet move the 62-readout floor?", + "why_it_matters": "Readouts are 62 of the 72 queries, and toggle-side extensions are now closed.", + "first_step": "State a joint-readout call with its additions and redo the row-cover argument for it.", + "blocked_by": "A priced joint-readout operation is not defined in the current model." + } + ], + "predecessors": [ + { + "pr": 943, + "author": "Ross Richardson", + "relationship": "Interface, singleton minimum 12 and the 945-pairing census; recomputed as a control." + }, + { + "pr": 1531, + "author": "navinor", + "relationship": "DUO word and the ten-point cover count 99,200; recomputed as controls." + }, + { + "pr": 4137, + "author": "unpaidmoon", + "relationship": "Support bound for steps of weight 1 to 5 at full coverage, extended here to partial coverage." + }, + { + "pr": 3321, + "author": "1337isnot1337", + "relationship": "Q5 model, one-Q5 census and the open question answered here." + }, + { + "pr": 2249, + "author": "1337isnot1337", + "relationship": "Open six-source analogue; cited in the open questions only." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19383637" +} diff --git a/research/five-source-toggle-frontier/VERIFY.json b/research/five-source-toggle-frontier/VERIFY.json new file mode 100644 index 0000000000..d213c54a82 --- /dev/null +++ b/research/five-source-toggle-frontier/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": 180, + "checks": "Cover numbers (no nine-point cover, 99,200 ten-point covers), 945-pairing census, 115,920-word weight-5 census, DUO and weight-5 schedules replayed symbolically and concretely, inequality tables, hill climb and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The same checks under optimized execution (no assert statements are used)." + } + ] +} diff --git a/research/five-source-toggle-frontier/verify.py b/research/five-source-toggle-frontier/verify.py new file mode 100644 index 0000000000..13b56f595d --- /dev/null +++ b/research/five-source-toggle-frontier/verify.py @@ -0,0 +1,583 @@ +#!/usr/bin/env python3 +"""Five-source dirty connector over every toggle alphabet: exact finite checks. + +Standard library only; every loop has an explicit finite bound. The model is the +five-source, 31-output interface of research/universal-connector-boundary with +every nonempty source subset S available as one complete call T_S priced +o + |S| p. A source word is a closed walk of toggle vectors in F_2^5; two +readouts at boundaries s, t realize the row q_s XOR q_t. Lower bounds use only +that reduction (it is the L = 1, identity-map specialization of the interface). + +Checks, all exact integer arithmetic: + 1. no set of at most nine points of F_2^5 has P + P = F_2^5 (exhaustive search over + every nine-point set containing 0, and over the affine-basis normal form); + 2. the 945 label-pairing census of length-ten singleton words (max coverage 31 of 32); + 3. the census of the 115,920 closed words with one weight-5 step and nine singletons; + 4. the DUO word (price (72, 74)) and a word with one weight-5 call (price (72, 78)): + coverage, generic-operator replay and concrete random-operator replay of each + 72-call schedule; + 5. the inequality tables behind Q >= 72, A >= 74 and A >= 78 with a weight-5 call; + 6. rejection controls and a seeded hill-climb that must not undercut the bounds. +""" + +import random +import sys +import time +from itertools import combinations + +N = 5 +NMASK = (1 << N) - 1 # the 31 nonzero masks 1..31 +FULLBITS = ((1 << (NMASK + 1)) - 1) & ~1 # bit m set for every nonzero mask m +READOUT_FLOOR = 2 * NMASK # two readouts for each of the 31 rows + +# Published singleton and DUO words (research/universal-connector-boundary and +# research/duo-toggle-connector). They are inputs here, not trusted results: every +# property used below is recomputed from the integers. +SINGLETON_12 = [2, 0, 2, 1, 2, 0, 3, 1, 4, 2, 3, 4] # B2 B0 B2 B1 B2 B0 B3 B1 B4 B2 B3 B4 +SINGLETON_10_MISS21 = [0, 1, 2, 0, 3, 1, 4, 2, 3, 4] # B0 B1 B2 B0 B3 B1 B4 B2 B3 B4 +DUO_WALK = [1, 2, 8, 18, 12, 16, 1, 2, 4, 2] # step masks; 18 and 12 are DUOs +# Found here by exhaustive depth-first search (not taken from a predecessor): ten calls, one +# weight-5 call (31), two DUOs (24 = {3,4}, 10 = {1,3}) and seven singletons; W = 16. +Q5_WALK = [1, 2, 1, 4, 2, 1, 8, 24, 10, 31] + +PAIRING_HISTOGRAM = {16: 42, 19: 120, 21: 180, 22: 56, 23: 45, 24: 220, 26: 110, 28: 150, 31: 22} + + +def wt(x): + return x.bit_count() + + +def require(ok, message): + if not ok: + raise SystemExit("FAIL " + message) + + +def prefixes(steps): + q = 0 + out = [0] + for s in steps: + require(1 <= s <= NMASK, "toggle outside the nonzero masks of F_2^5: %r" % (s,)) + q ^= s + out.append(q) + return out + + +def nonzero_differences(points): + pts = sorted(set(points)) + found = set() + for i, a in enumerate(pts): + for b in pts[i + 1:]: + found.add(a ^ b) + return found + + +def missing_count(steps): + """Number u of nonzero masks that no two boundaries of the closed word realize.""" + pre = prefixes(steps) + require(pre[-1] == 0, "source word is not closed") + return NMASK - len(nonzero_differences(pre)) + + +def price_floor(steps): + """(Q, A) lower bounds for any schedule over this source word (rows read twice, plus + four readouts for each row that no boundary pair realizes).""" + u = missing_count(steps) + readouts = READOUT_FLOOR + 2 * u + return len(steps) + readouts, sum(wt(s) for s in steps) + readouts + + +# ---------------------------------------------------------------- 1. cover numbers + +COVER_SEARCH_STEP_LIMIT = 60_000_000 # measured need: 5,403,753 steps (nine points), 41,511,450 (ten) + + +def count_covers(size): + """Number of subsets P of F_2^5 with 0 in P, |P| = size and P + P = F_2^5. + + Exhaustive depth-first search with an explicit stack (no recursion), over increasing + element choices. Adding an element to a k-point set creates k new pairs; pairs that + repeat an earlier difference are 'waste'. A cover needs 31 distinct nonzero + differences, so waste can never exceed C(size, 2) - 31; the cut is exact, not heuristic.""" + allowed = size * (size - 1) // 2 - NMASK + if allowed < 0: + return 0 + covers = 0 + chosen = [0] + seen_at = [0] # differences covered by chosen[:k] + waste_at = [0] + next_try = [1] # next candidate element for the node chosen[:k] + for _ in range(COVER_SEARCH_STEP_LIMIT): + if not chosen: + return covers + k = len(chosen) + x = next_try[-1] + if k == size or x > NMASK: + if k == size and seen_at[-1] == FULLBITS: + covers += 1 + chosen.pop() + seen_at.pop() + waste_at.pop() + next_try.pop() + continue + next_try[-1] = x + 1 + fresh = 0 + for p in chosen: + bit = 1 << (x ^ p) + if not (seen_at[-1] & bit) and not (fresh & bit): + fresh |= bit + waste = waste_at[-1] + k - fresh.bit_count() + if waste <= allowed: + chosen.append(x) + seen_at.append(seen_at[-1] | fresh) + waste_at.append(waste) + next_try.append(x + 1) + raise SystemExit("FAIL cover search exceeded its step limit") + + +def affine_normal_form_counts(): + """Every cover contains an affine basis, and affine maps preserve P + P = F_2^5, so + it suffices to take P containing 0, e_0..e_4 and extra points.""" + base = [0] + [1 << j for j in range(N)] + rest = [x for x in range(1, NMASK + 1) if x not in base] + out = {} + for extra in (3, 4): + count = 0 + for add in combinations(rest, extra): + pts = base + list(add) + if len(nonzero_differences(pts)) == NMASK: + count += 1 + out[len(base) + extra] = count + return out + + +def check_cover_numbers(): + for size in range(1, 9): + require(size * (size - 1) // 2 < NMASK, "counting bound at size %d" % size) + covers9 = count_covers(9) + require(covers9 == 0, "a nine-point cover of F_2^5 exists") + normal = affine_normal_form_counts() + require(normal[9] == 0, "normal-form search found a nine-point cover") + require(normal[10] == 80, "normal-form ten-point cover count changed: %r" % (normal[10],)) + pts = prefixes(DUO_WALK)[:-1] + require(len(set(pts)) == 10 and len(nonzero_differences(pts)) == NMASK, + "the DUO prefix set is not a ten-point cover") + # Positive control for the pruned search: the same search finds the 99,200 ten-point + # covers containing 0 that research/duo-toggle-connector records from a separate scan. + covers10 = count_covers(10) + require(covers10 == 99200, "ten-point cover count %d" % covers10) + return covers9, normal[10], covers10 + + +# ---------------------------------------------------------------- 2. pairing census + +def matchings(n): + """All perfect matchings of the positions 0..n-1, each as a tuple of pairs (explicit stack).""" + stack = [((), tuple(range(n)))] + while stack: + part, rest = stack.pop() + if not rest: + yield part + continue + first = rest[0] + for i in range(1, len(rest)): + stack.append((part + ((first, rest[i]),), rest[1:i] + rest[i + 1:])) + + +def check_pairing_census(): + histogram = {} + best_missing = NMASK + total = 0 + for matching in matchings(10): + word = [0] * 10 + for label, (a, b) in enumerate(matching): + word[a] = word[b] = 1 << label + total += 1 + u = missing_count(word) + coverage = NMASK + 1 - u + histogram[coverage] = histogram.get(coverage, 0) + 1 + best_missing = min(best_missing, u) + require(total == 945, "pairing count %d" % total) + require(histogram == PAIRING_HISTOGRAM, "pairing histogram differs: %r" % (histogram,)) + require(best_missing == 1, "a length-ten singleton word covers every mask") + return total, best_missing + + +# ---------------------------------------------------------------- 3. one weight-5 step + +def multiset_words(counts): + """All distinct sequences containing label j exactly counts[j] times, in lexicographic + order, by repeated next-permutation steps (no recursion).""" + word = [j for j, c in enumerate(counts) for _ in range(c)] + n = len(word) + while True: + yield tuple(word) + i = n - 2 + while i >= 0 and word[i] >= word[i + 1]: + i -= 1 + if i < 0: + return + j = n - 1 + while word[j] <= word[i]: + j -= 1 + word[i], word[j] = word[j], word[i] + word[i + 1:] = reversed(word[i + 1:]) + + +def check_one_weight5_census(): + """Closed ten-step words with one weight-5 step and nine singleton steps. Rotating a + closed word translates its prefix set, so the weight-5 step may be last. Closure forces + every singleton count odd, so the counts are (5,1,1,1,1) or (3,3,1,1,1).""" + patterns = set() + for a in range(1, 10, 2): + for b in range(1, 10, 2): + for c in range(1, 10, 2): + for d in range(1, 10, 2): + for e in range(1, 10, 2): + if a + b + c + d + e == 9: + patterns.add(tuple(sorted((a, b, c, d, e), reverse=True))) + require(patterns == {(5, 1, 1, 1, 1), (3, 3, 1, 1, 1)}, "odd count patterns") + words = 0 + best = 0 + for pattern in sorted(patterns): + for perm_counts in sorted(_label_assignments(pattern)): + for word in multiset_words(perm_counts): + words += 1 + point = 0 + points = [0] + for j in word: + point ^= 1 << j + points.append(point) + require(point == NMASK, "closure of the weight-5 word") + count = len(nonzero_differences(points)) + if count > best: + best = count + require(words == 115920, "weight-5 census size %d" % words) + require(best == 27, "maximum distinct differences %d" % best) + return words, best + + +def _label_assignments(pattern): + # distinct arrangements of the multiset of counts over the five labels + seen = set() + stack = [()] + while stack: + part = stack.pop() + if len(part) == len(pattern): + seen.add(part) + continue + remaining = list(pattern) + for c in part: + remaining.remove(c) + for c in set(remaining): + stack.append(part + (c,)) + return seen + + +# ---------------------------------------------------------------- 4. schedules + +def build_schedule(steps): + """Readouts at the first boundary pair realizing each row, interleaved with the word. + Operations: ('T', mask) a toggle call, ('A', row) a readout.""" + pre = prefixes(steps) + first = {} + for i in range(len(pre)): + for j in range(i + 1, len(pre)): + first.setdefault(pre[i] ^ pre[j], (i, j)) + at = {b: [] for b in range(len(pre))} + extra = 0 + for m in range(1, NMASK + 1): + if m in first: + for b in first[m]: + at[b].append(m) + else: + # four readouts: two boundary pairs whose differences XOR to m + done = False + for d1, (i, j) in sorted(first.items()): + d2 = d1 ^ m + if d2 in first: + k, l = first[d2] + if len({i, j, k, l}) == 4: + for b in (i, j, k, l): + at[b].append(m) + done = True + extra += 1 + break + require(done, "no four-readout repair for mask %d" % m) + ops = [] + for b in range(len(pre)): + ops.extend(("A", m) for m in at[b]) + if b < len(steps): + ops.append(("T", steps[b])) + return ops + + +def costs(ops): + queries = len(ops) + additions = sum(wt(arg) if kind == "T" else 1 for kind, arg in ops) + return queries, additions + + +def evaluate_generic(ops): + """Exact for arbitrary operators: z is a sum of the formal symbols z0 (bit 0) and + B_j x_j (bit 1 + j); a readout adds the same formal combination, acted on by A_m, to row m. + The schedule is correct for every admissible choice of maps and dirty data iff the final + row m holds exactly the symbols B_j x_j with j in m and z has returned to z0.""" + z = 1 + rows = [0] * (NMASK + 1) + for kind, arg in ops: + if kind == "T": + for j in range(N): + if arg >> j & 1: + z ^= 1 << (1 + j) + else: + rows[arg] ^= z + if z != 1: + return False + for m in range(1, NMASK + 1): + want = 0 + for j in range(N): + if m >> j & 1: + want |= 1 << (1 + j) + if rows[m] != want: + return False + return True + + +def evaluate_concrete(ops, rng, trials, width=3): + """Run the schedule on random dirty data with random binary linear maps.""" + def apply(matrix, v): + out = 0 + for i in range(width): + if v >> i & 1: + out ^= matrix[i] + return out + + for _ in range(trials): + mats_b = [[rng.randrange(1 << width) for _ in range(width)] for _ in range(N)] + mats_a = [[rng.randrange(1 << width) for _ in range(width)] for _ in range(NMASK + 1)] + x = [rng.randrange(1 << width) for _ in range(N)] + z0 = rng.randrange(1 << width) + y0 = [rng.randrange(1 << width) for _ in range(NMASK + 1)] + z = z0 + y = list(y0) + for kind, arg in ops: + if kind == "T": + for j in range(N): + if arg >> j & 1: + z ^= apply(mats_b[j], x[j]) + else: + y[arg] ^= apply(mats_a[arg], z) + if z != z0: + return False + for m in range(1, NMASK + 1): + total = 0 + for j in range(N): + if m >> j & 1: + total ^= apply(mats_b[j], x[j]) + if y[m] != y0[m] ^ apply(mats_a[m], total): + return False + return True + + +def check_schedules(): + rng = random.Random(20261103) + duo = build_schedule(DUO_WALK) + q, a = costs(duo) + require((q, a) == (72, 74), "DUO schedule price %r" % ((q, a),)) + require(len(DUO_WALK) == 10 and sum(wt(s) for s in DUO_WALK) == 12, "DUO word profile") + require(sorted(wt(s) for s in DUO_WALK).count(2) == 2, "DUO word must use two weight-2 calls") + require(evaluate_generic(duo), "DUO schedule fails the generic-operator replay") + require(evaluate_concrete(duo, rng, 150), "DUO schedule fails the concrete replay") + + require(prefixes(Q5_WALK)[-1] == 0 and len(Q5_WALK) == 10, "weight-5 word is not a closed ten-step walk") + require(sorted(wt(t) for t in Q5_WALK) == [1] * 7 + [2, 2, 5], "weight-5 word step weights") + q5 = build_schedule(Q5_WALK) + require(costs(q5) == (72, 78), "weight-5 schedule price %r" % (costs(q5),)) + require(price_floor(Q5_WALK) == (72, 78), "weight-5 word floors") + require(evaluate_generic(q5), "weight-5 schedule fails the generic-operator replay") + require(evaluate_concrete(q5, rng, 150), "weight-5 schedule fails the concrete replay") + + single = build_schedule([1 << j for j in SINGLETON_12]) + require(costs(single) == (74, 74), "singleton schedule price") + require(evaluate_generic(single) and evaluate_concrete(single, rng, 60), + "singleton control fails") + + miss = [1 << j for j in SINGLETON_10_MISS21] + pre = prefixes(miss) + absent = set(range(1, NMASK + 1)) - nonzero_differences(pre) + require(absent == {21}, "ten-call singleton control misses %r" % sorted(absent)) + repaired = build_schedule(miss) + require(costs(repaired) == (74, 74) and evaluate_generic(repaired), + "ten-call word with a four-readout repair") + return q, a + + +# ---------------------------------------------------------------- 5. inequality tables + +def u_floor(s): + """Least number of uncovered masks when the closed word has s distinct prefix points.""" + pairs = s * (s - 1) // 2 + least = max(NMASK - pairs, 0) + if s <= 9: + least = max(least, 1) # no cover of F_2^5 has at most nine points + return least + + +def check_inequalities(): + best = None + for s in range(1, 41): + value = s + 2 * u_floor(s) # lower bound for T + 2u since T >= s + if best is None or value < best[0]: + best = (value, s) + if s != 10: + require(value >= 11, "T + 2u floor %d at s = %d" % (value, s)) + require(best == (10, 10), "minimum of T + 2u is %r" % (best,)) + # Q >= T + 62 + 2u >= 72, with equality only if T = s = 10 and u = 0. + # weight-5 step: W >= T + 4 per such step; W is even (closed walk). + for T in range(1, 41): + s_max = T + # least u over s <= T given the table above + u_least = min(u_floor(s) for s in range(1, s_max + 1)) + w_least = T + 4 + if w_least % 2: + w_least += 1 + if T == 10 and w_least == 14: + u_least = max(u_least, 1) # the weight-5 census: nine singletons never cover + a_floor = w_least + READOUT_FLOOR + 2 * u_least + require(a_floor >= 78, "weight-5 addition floor %d at T = %d" % (a_floor, T)) + # two or more weight-5 steps: W >= T + 8 and T + 2u >= 10 give A >= 80 + for T in range(1, 41): + u_least = min(u_floor(s) for s in range(1, T + 1)) + w_least = T + 8 + (T % 2) + require(w_least + READOUT_FLOOR + 2 * u_least >= 80, "two weight-5 steps at T = %d" % T) + return best + + +# ---------------------------------------------------------------- 6. controls + +def hill_climb(rng, rounds, start): + """Local search over closed words of any alphabet. The proved floors must hold at every + visited word; the search is expected to reach (72, 74) from the DUO start.""" + cur = list(start) + q, a = price_floor(cur) + best_q, best_a = q, a + seen_weight5 = [] + for _ in range(rounds): + cand = list(cur) + move = rng.randrange(4) + if move == 0 and len(cand) >= 2: + i = rng.randrange(len(cand) - 1) + cand[i] = rng.randrange(1, NMASK + 1) + x = 0 + for s in cand[:-1]: + x ^= s + cand[-1] = x + elif move == 1 and len(cand) < 14: + i = rng.randrange(len(cand) + 1) + t = rng.randrange(1, NMASK + 1) + cand.insert(i, t) + x = 0 + for s in cand[:-1]: + x ^= s + cand[-1] = x + elif move == 2 and len(cand) > 3: + del cand[rng.randrange(len(cand))] + x = 0 + for s in cand[:-1]: + x ^= s + cand[-1] = x + else: + i, j = rng.randrange(len(cand)), rng.randrange(len(cand)) + cand[i], cand[j] = cand[j], cand[i] + if len(cand) < 2 or any(not 1 <= s <= NMASK for s in cand): + continue + if prefixes(cand)[-1] != 0: + continue + cq, ca = price_floor(cand) + require(cq >= 72 and ca >= 74, "floor violated by %r -> %r" % (cand, (cq, ca))) + if 31 in cand: + require(ca >= 78, "weight-5 floor violated by %r -> %r" % (cand, (cq, ca))) + seen_weight5.append(ca) + best_q, best_a = min(best_q, cq), min(best_a, ca) + if (cq, ca) <= (q, a) or rng.random() < 0.15: + cur, (q, a) = cand, (cq, ca) + return best_q, best_a, len(seen_weight5) + + +def check_random_words(rng, samples): + seen5 = 0 + low_q = low_a = None + for _ in range(samples): + length = rng.randrange(3, 15) + steps = [rng.randrange(1, NMASK + 1) for _ in range(length - 1)] + x = 0 + for s in steps: + x ^= s + if x == 0: + continue + steps.append(x) + q, a = price_floor(steps) + require(q >= 72 and a >= 74, "random word undercuts the floors: %r" % (steps,)) + if 31 in steps: + seen5 += 1 + require(a >= 78, "random weight-5 word undercuts 78: %r" % (steps,)) + low_q = q if low_q is None else min(low_q, q) + low_a = a if low_a is None else min(low_a, a) + return seen5, low_q, low_a + + +def check_rejections(): + duo = build_schedule(DUO_WALK) + controls = 0 + for i in (0, 7, 30, 71): # drop one operation + broken = duo[:i] + duo[i + 1:] + require(not evaluate_generic(broken), "generic replay accepted a dropped operation %d" % i) + controls += 1 + wrong_row = list(duo) + first_read = next(i for i, op in enumerate(wrong_row) if op[0] == "A") + row = wrong_row[first_read][1] + wrong_row[first_read] = ("A", row + 1 if row < NMASK else 1) + require(not evaluate_generic(wrong_row), "generic replay accepted a wrong row") + controls += 1 + open_walk = [op for op in duo if op != ("T", DUO_WALK[-1])] + require(not evaluate_generic(open_walk), "generic replay accepted a word that does not restore z") + controls += 1 + require(not evaluate_concrete(duo[:-1], random.Random(7), 30), + "concrete replay accepted a truncated schedule") + controls += 1 + # a short word cannot reach 72 queries: four steps leave nearly every row uncovered + require(price_floor([1, 2, 1, 2])[0] > 72, "four-step word cannot reach 72") + controls += 1 + try: + prefixes([0]) + except SystemExit: + controls += 1 + else: + raise SystemExit("FAIL a zero toggle was accepted") + return controls + + +def main(): + t0 = time.time() + covers9, normal10, covers10 = check_cover_numbers() + pairings, best_missing = check_pairing_census() + words5, best5 = check_one_weight5_census() + q, a = check_schedules() + floor_value, floor_s = check_inequalities() + rng = random.Random(20261104) + seen5, low_q, low_a = check_random_words(rng, 30000) + require(low_q >= 72 and low_a >= 74, "random floor") + hq, ha, h5 = hill_climb(random.Random(11), 6000, DUO_WALK) + require(hq >= 72 and ha >= 74, "hill-climb floor") + controls = check_rejections() + print("PASS_FIVE_SOURCE_TOGGLE_FRONTIER nine_point_covers=%d ten_point_covers=%d " + "affine_ten_covers=%d pairings=%d singleton_min_missing=%d weight5_words=%d " + "weight5_max_diff=%d witness=(%d,%d) min_T_plus_2u=%d@s=%d random_weight5=%d " + "hill_floor=(%d,%d) controls=%d weight5_witness=(72,78) no_new_kappa" + % (covers9, covers10, normal10, pairings, best_missing, words5, best5, q, a, + floor_value, floor_s, seen5 + h5, hq, ha, controls)) + print("elapsed_seconds=%.1f" % (time.time() - t0), file=sys.stderr) + + +if __name__ == "__main__": + main()