diff --git a/research/seven-source-duo-21-calls/CERTIFICATE.json b/research/seven-source-duo-21-calls/CERTIFICATE.json new file mode 100644 index 0000000000..bd26ecafff --- /dev/null +++ b/research/seven-source-duo-21-calls/CERTIFICATE.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "model": "Seven-source restored singleton+DUO connector of research/connector-seven-source-duo: a step s in 1..127 of Hamming weight 1 is one singleton call z += B_j x_j; weight 2 is one charged DUO call z += B_j x_j + B_k x_k. A word is universal when its prefix states P satisfy P+P = F2^7.", + "words": { + "k21_W24": { + "prefix_states": [0, 1, 33, 36, 38, 102, 100, 96, 98, 114, 82, 83, 115, 123, 120, 88, 89, 9, 41, 40, 8], + "k": 21, + "duo_calls": 3, + "W": 24, + "queries_all_127_rows": 275, + "adds_all_127_rows": 278 + }, + "k20_W26": { + "prefix_states": [0, 2, 16, 112, 120, 88, 92, 60, 61, 29, 21, 85, 81, 115, 123, 59, 58, 26, 14, 12], + "k": 20, + "duo_calls": 6, + "W": 26, + "queries_all_127_rows": 274, + "adds_all_127_rows": 280 + } + }, + "search_failures_not_exclusions": { + "note": "Bounded simulated-annealing runs of search/sa.c that found no universal word. These are search failures, not exclusions.", + "runs": [ + "./sa 20 24 11 10000000 20", + "./sa 20 24 99 20000000 20", + "./sa 19 W 5 10000000 10 for W in 24 26 28 30 34", + "./sa 18 W 5 10000000 10 for W in 30 36", + "./sa 21 22 3 10000000 10", + "./sa 22 22 3 10000000 10" + ] + } +} diff --git a/research/seven-source-duo-21-calls/README.md b/research/seven-source-duo-21-calls/README.md new file mode 100644 index 0000000000..ba90f61acb --- /dev/null +++ b/research/seven-source-duo-21-calls/README.md @@ -0,0 +1,113 @@ +# Seven-source singleton+DUO connectors: 21 calls at 24 adds, and 20 calls + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: finite certificate (explicit construction).** No search +exclusion, no optimality proof, no new κ, no supplier change. + +In the seven-source restored connector of Ross Richardson's +[#943](https://github.com/CrocSwap/integer-mult-bounds/pull/943), extended by +the charged pair-source DUO call `z += B_j x_j + B_k x_k` of +`research/duo-toggle-connector`, Aaron Wang's +[#2396](https://github.com/CrocSwap/integer-mult-bounds/pull/2396) +(`research/connector-seven-source-duo`) gives a universal word with +`(k, W) = (22, 24)`: 22 source calls and 24 toggle-adds. Its first open +question asks whether `(22, 24)` is the Pareto profile. It is not. This package +gives two universal words: + +| Word | Calls `k` | DUO calls | Adds `W` | Batch queries | Batch adds | +|---|---:|---:|---:|---:|---:| +| #2396 (cited) | 22 | 2 | 24 | 276 | 278 | +| **this package** | **21** | 3 | **24** | **275** | **278** | +| **this package** | **20** | 6 | 26 | **274** | 280 | + +The batch is the all-127-row batch of #2396 with two paired readouts per row +(254 readouts). The `(21, 24)` word strictly dominates `(22, 24)`: one fewer +call at the same adds, so in #2396's tariff `c_B = o + p`, `c_DUO = o + 2p`, +`c_A = o + p` the batch saves `o` for every `o > 0`, and `3o` against the +24-call singleton Gray word. The `(20, 26)` word saves one more call at two +more adds; it beats `(21, 24)` exactly when `o > 2p`. It also answers +#2396's `(20, d)` question at `d = 6`, where #2396's search reached 126/128. + +## The words + +Prefix states, with bit `j` for source `j`. Each word closes back to `0`. +A step of weight one is a singleton call, a step of weight two a DUO call. + +```text +(21,24): 0 1 33 36 38 102 100 96 98 114 82 83 115 123 120 88 89 9 41 40 8 +(20,26): 0 2 16 112 120 88 92 60 61 29 21 85 81 115 123 59 58 26 14 12 +``` + +Universality is the paired-readout criterion used by #943 and #2396: +the prefix-state set `P` satisfies `P + P = F2^7`. + +## Evidence + +[verify.py](verify.py) uses only the Python standard library and no search. +For each word it rebuilds the steps from the prefix states and checks: + +- every step has weight one or two, the word restores the connector, and every + source label has positive even multiplicity; +- all 128 masks lie in `P + P`, and a separate dual test (mask `m` is covered + when `p xor m` is in `P` for some `p` in `P`) finds no missing mask; +- `k`, the DUO count, `W` and the batch bill match [CERTIFICATE.json](CERTIFICATE.json); +- four mutations per word are rejected: a deleted call, a DUO shrunk to a + singleton, a retargeted call and a dropped call. + +It also reads #2396's pinned certificate, confirms that word is universal at +`(22, 24)`, and checks the dominance relations above. Assertions are explicit +checks, so `-O` does not skip them. + +## Reproduce + +From the repository root with CPython 3.12 (the recorded local interpreter was +`~/git/integer-mult-bounds/.venv/bin/python3.12`): + +```sh +python3.12 -B research/seven-source-duo-21-calls/verify.py +python3.12 -B scripts/research_package.py --package research/seven-source-duo-21-calls +``` + +Expected marker: +`PASS_SEVEN_SOURCE_DUO_21_CALLS k21_W24_queries=275 k20_W26_queries=274 pred_queries=276 universal=128/128 mutations_rejected=8`. + +The words came from the simulated-annealing program [search/sa.c](search/sa.c) +(`cc -O2 -o sa sa.c -lm`; arguments `K WMAX seed iterations restarts`). +`./sa 21 24 1 5000000 20` and `./sa 20 26 7 5000000 20` printed these words +on an Apple arm64 host. The search is provenance only; the verifier does not +depend on it. + +## Limitations + +- **No lower bound.** Runs at `(20, W <= 24)`, `(19, W <= 34)`, `(18, W <= 36)` + and `W = 22` at `k = 21, 22` found nothing. These are bounded search + failures listed in CERTIFICATE.json, not exclusions. +- The counting bound `C(k,2) + 1 >= 128` gives only `k >= 17`. +- Inherited from #2396 and `research/duo-toggle-connector`: no physical + supplier instance of this connector exists, so no recursive moment, frame, + compiler or κ consequence follows. With `o = 0` the `(21, 24)` word gains + nothing over `(22, 24)`. + +## Open next questions + +1. **Is 20 the minimum number of calls?** A universal 19-call word would cut + the batch to 273 queries. First step: an exact census of 19-point sets `P` + with `P + P = F2^7`, then a Hamiltonian-cycle test with edges of weight at + most two. Blocker: no exclusion argument beyond the counting bound + `k >= 17` and the parity rule `d = k mod 2`. +2. **Is 24 the minimum number of adds?** `f(7) = 24` (#3058) settles the + singleton case, but a word with DUO calls and `W = 22` is not excluded. + First step: adapt #3058's deletion argument to steps of weight two. +3. **Is `(20, 24)` attainable?** It would dominate both new words. The local + search reached no such word. + +## Credit + +Ross Richardson (#943) supplied the connector model and paired-readout +criterion. The DUO family and its pricing come from `research/duo-toggle-connector`. +Aaron Wang / navinor (#2396) supplied the `(22, 24)` word, the batch bill, +the tariff and the open Pareto question answered here. Douglas Colkitt (#1185) +supplied the Gray baseline, and conorholds (#3058) the singleton value +`f(7) = 24`. Their results are cited, not re-audited. The two new words, the +verifier and the search program are new. diff --git a/research/seven-source-duo-21-calls/SOURCES.json b/research/seven-source-duo-21-calls/SOURCES.json new file mode 100644 index 0000000000..6238e3c410 --- /dev/null +++ b/research/seven-source-duo-21-calls/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "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" + }, + { + "path": "research/connector-seven-source-duo/CERTIFICATE.json", + "usage": "input", + "git_blob": "a1de5ebffaa3a33486fd28643ccad67c60843f06", + "sha256": "6b8c5bd2d27a0b4cbeb073bc0ac224220fdf99bc94760afd9a1be79aa31c4a63" + } + ] +} diff --git a/research/seven-source-duo-21-calls/TASK.json b/research/seven-source-duo-21-calls/TASK.json new file mode 100644 index 0000000000..f788f8a861 --- /dev/null +++ b/research/seven-source-duo-21-calls/TASK.json @@ -0,0 +1,74 @@ +{ + "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": "Open next question 1 of PR #2396 (research/connector-seven-source-duo): is (k, W) = (22, 24) the Pareto profile for seven-source universal words in the singleton+DUO alphabet? Answered negatively by explicit universal words at (21, 24) and (20, 26).", + "scope_change_reason": "The card asks for one new alphabet extension. DUO is already added and charged by research/duo-toggle-connector and #2396; this package keeps that alphabet and source count and improves #2396's open Pareto profile. It is a side result on the connector interface.", + "bottleneck_link": "Side result. Connector call counts enter the recursive interface through complete-call pricing; the new words save one or two per-call overheads o on the all-127-row batch. No physical supplier instance of this connector exists, so no \u03ba follows.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified universal word with fewer than 22 calls; record unsuccessful smaller profiles as search failures, not exclusions.", + "outcome": "completed", + "evidence": "Explicit universal words (21, 24) and (20, 26), checked by research/seven-source-duo-21-calls/verify.py: weights, restoration, even label counts, 128/128 masks with a dual test, batch bill 275/278 and 274/280, dominance over #2396's pinned (22, 24) word, and eight rejected mutations.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is 20 the minimum number of calls for a seven-source singleton+DUO universal word?", + "why_it_matters": "A 19-call word would cut the all-127-row batch to 273 queries.", + "first_step": "Exactly enumerate 19-point sets P with P+P = F2^7, then test for a Hamiltonian cycle with edges of weight at most two.", + "blocked_by": "No exclusion argument beyond the counting bound k >= 17 and the parity rule d = k mod 2." + }, + { + "question": "Is 24 the minimum number of toggle-adds when DUO calls are allowed?", + "why_it_matters": "f(7) = 24 (#3058) settles only singleton words; a W = 22 DUO word would lower the batch adds.", + "first_step": "Adapt #3058's coordinate-deletion argument to weight-two steps.", + "blocked_by": "The deletion argument is written for singleton steps." + }, + { + "question": "Is (20, 24) attainable?", + "why_it_matters": "It would dominate both new words.", + "first_step": "An exact (20, 4) census as #2396 proposed.", + "blocked_by": "Local simulated annealing found no such word; that is not an exclusion." + } + ] +} diff --git a/research/seven-source-duo-21-calls/VERIFY.json b/research/seven-source-duo-21-calls/VERIFY.json new file mode 100644 index 0000000000..f802e5e78f --- /dev/null +++ b/research/seven-source-duo-21-calls/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-seven-source-duo/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Two explicit seven-source singleton+DUO universal words, (21,24) and (20,26): step weights, restoration, even label counts, 128/128 masks with an independent dual test, batch bill, dominance over the pinned #2396 (22,24) word, and eight mutation controls. Prints PASS_SEVEN_SOURCE_DUO_21_CALLS." + } + ] +} diff --git a/research/seven-source-duo-21-calls/search/sa.c b/research/seven-source-duo-21-calls/search/sa.c new file mode 100644 index 0000000000..a9091654e3 --- /dev/null +++ b/research/seven-source-duo-21-calls/search/sa.c @@ -0,0 +1,47 @@ +// SA search: closed cycle of K points in F2^N, consecutive (cyclic) Hamming distance 1 or 2, +// maximize |P+P| coverage; then report W = sum of distances. +#include +#include +#include +#include +#define N 7 +#define M (1<>7; s^=s<<17; return s; } +static inline int wt(int x){ return __builtin_popcount(x); } +int K, WMAX; int P[64]; int cnt[M]; int cov; +static int ok(int d){ int w=wt(d); return w==1||w==2; } +static int W(){ int t=0; for(int i=0;i0){ if(cnt[d]++==0) cov++; } else { if(--cnt[d]==0) cov--; } } } +int main(int argc,char**argv){ + K=atoi(argv[1]); WMAX=atoi(argv[2]); s^=strtoull(argv[3],0,10)*0x9E3779B97F4A7C15ULL; long iters=atol(argv[4]); int restarts=atoi(argv[5]); + for(int r=0;rWMAX? w-WMAX:0); + for(long it=0;itWMAX? nw-WMAX:0); + if(ns>=score || exp((ns-score)/T) > (rnd()%1000000)/1e6){ score=ns; bad=nb; w=nw; } + else { add(i,-1); P[i]=old; add(i,1); } + if(cov==M && bad==0 && w<=WMAX){ + printf("FOUND K=%d W=%d :",K,w); for(int j=0;j> j) & 1 + require(acc == 0, "word does not restore the connector") + require(all(c % 2 == 0 and c > 0 for c in counts), f"label counts {counts}") + d = sum(1 for s in steps if bin(s).count("1") == 2) + return len(steps), d, sum(bin(s).count("1") for s in steps) + + +def states_of(steps): + out, acc = [], 0 + for s in steps: + out.append(acc) + acc ^= s + return out + + +def universal(steps): + states = states_of(steps) + return len(covered(states)) == MASKS and not dual_missing(states) + + +def check_word(name, rec): + states = rec["prefix_states"] + require(states[0] == 0) + steps = steps_of(states) + k, d, w = profile(steps) + require(states_of(steps) == states) + require((k, d, w) == (rec["k"], rec["duo_calls"], rec["W"]), (name, k, d, w)) + require(len(covered(states)) == MASKS, f"{name} covers {len(covered(states))}") + require(dual_missing(states) == [], name) + require(k + READOUTS == rec["queries_all_127_rows"]) + require(w + READOUTS == rec["adds_all_127_rows"]) + return steps, k, w + + +def mutations(steps): + """Each mutation must be rejected as illegal or non-universal.""" + rejected = 0 + trials = [] + trials.append(steps[1:]) # delete a call + duo = next(i for i, s in enumerate(steps) if bin(s).count("1") == 2) + low = steps[duo] & -steps[duo] + trials.append(steps[:duo] + [low] + steps[duo + 1:]) # shrink DUO + trials.append(steps[:2] + [steps[2] ^ 64 if steps[2] ^ 64 else 1] + steps[3:]) # retarget + trials.append(steps[:-2] + [steps[-1]]) # drop the penultimate call + for t in trials: + try: + profile(t) + ok = universal(t) + except CheckError: + ok = False + rejected += not ok + require(rejected == len(trials), f"only {rejected}/{len(trials)} mutations rejected") + return rejected + + +def main(): + cert = json.loads((HERE / "CERTIFICATE.json").read_text()) + pred_bytes = PRED.read_bytes() + require(hashlib.sha256(pred_bytes).hexdigest() == PRED_SHA256, "predecessor pin") + pred = json.loads(pred_bytes)["headline_22_24"] + pk, pd, pw = profile(pred["steps"]) + require((pk, pw) == (22, 24) and universal(pred["steps"]), "predecessor control") + a_steps, ak, aw = check_word("k21_W24", cert["words"]["k21_W24"]) + b_steps, bk, bw = check_word("k20_W26", cert["words"]["k20_W26"]) + # (21,24) strictly dominates (22,24): one fewer call, same adds. + require(ak < pk and aw == pw) + # (20,26) beats (21,24) in c = q*o + a*p exactly when o > 2p. + require((bk - ak, bw - aw) == (-1, 2)) + muts = mutations(a_steps) + mutations(b_steps) + print( + "PASS_SEVEN_SOURCE_DUO_21_CALLS " + f"k21_W24_queries={ak + READOUTS} k20_W26_queries={bk + READOUTS} " + f"pred_queries={pk + READOUTS} universal=128/128 mutations_rejected={muts}" + ) + + +if __name__ == "__main__": + try: + main() + except CheckError as exc: + print(f"FAIL_SEVEN_SOURCE_DUO_21_CALLS {exc}") + sys.exit(1)