From d043a58aa43d21e2da6c6405127ec49412078815 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 21:59:12 +0100 Subject: [PATCH 1/2] feat(research): exclude the seven-source F3 connector floor Two independent enumerators check every restored 21-event source path up to rotation and relabelling; none serves all 127 masks with readout triples. With the 405-call word and deletion lemma of #4232, the seven-source optimum is 405 and the floor is attained exactly for n <= 6. --- .../CERTIFICATE.json | 165 +++++++++++ .../f3-seven-source-connector-floor/README.md | 139 ++++++++++ .../SOURCES.json | 18 ++ .../f3-seven-source-connector-floor/TASK.json | 86 ++++++ .../VERIFY.json | 60 ++++ .../engine/independent.c | 63 +++++ .../engine/reduced.c | 116 ++++++++ .../f3-seven-source-connector-floor/verify.py | 259 ++++++++++++++++++ 8 files changed, 906 insertions(+) create mode 100644 research/f3-seven-source-connector-floor/CERTIFICATE.json create mode 100644 research/f3-seven-source-connector-floor/README.md create mode 100644 research/f3-seven-source-connector-floor/SOURCES.json create mode 100644 research/f3-seven-source-connector-floor/TASK.json create mode 100644 research/f3-seven-source-connector-floor/VERIFY.json create mode 100644 research/f3-seven-source-connector-floor/engine/independent.c create mode 100644 research/f3-seven-source-connector-floor/engine/reduced.c create mode 100644 research/f3-seven-source-connector-floor/verify.py diff --git a/research/f3-seven-source-connector-floor/CERTIFICATE.json b/research/f3-seven-source-connector-floor/CERTIFICATE.json new file mode 100644 index 0000000000..777ba68ef9 --- /dev/null +++ b/research/f3-seven-source-connector-floor/CERTIFICATE.json @@ -0,0 +1,165 @@ +{ + "schema_version": 1, + "field": "F3", + "model": "restored source path of length 3n, each source three times; a mask is served when it equals q_a+q_b+q_c over prefix boundaries a<=b<=c (PR4232 section 3)", + "calibration": { + "1": { + "reduced": [ + 1, + 1 + ], + "all_paths": [ + 1, + 1 + ] + }, + "2": { + "reduced": [ + 5, + 5 + ], + "independent": [ + 6, + 6 + ], + "all_paths": [ + 20, + 20 + ] + }, + "3": { + "reduced": [ + 79, + 79 + ], + "independent": [ + 210, + 210 + ], + "all_paths": [ + 1680, + 1680 + ] + }, + "4": { + "reduced": [ + 3165, + 2257 + ], + "independent": [ + 12600, + 10227 + ], + "all_paths": [ + 369600, + 291120 + ] + }, + "5": { + "reduced": [ + 227174, + 32317 + ], + "independent": [ + 1201200, + 216666 + ] + }, + "6": { + "reduced": [ + 25518500, + 2678 + ], + "independent": [ + 168168000, + 13575 + ] + } + }, + "n7": { + "reduced": { + "shards": 18, + "leaves": [ + 239023495, + 255665689, + 250908027, + 235822986, + 212179804, + 205285672, + 215970227, + 219525116, + 227294598, + 241218002, + 213212613, + 214258909, + 239615884, + 250575668, + 257508926, + 222676889, + 209091877, + 220389458 + ], + "total_leaves": 4130223840, + "solutions": 0 + }, + "independent": { + "shards": 18, + "leaves": [ + 1381780400, + 1598088800, + 1682511600, + 1452220000, + 1958495000, + 1934655800, + 2203170200, + 2150117200, + 2049770800, + 2271145800, + 2044504000, + 2104086600, + 1626886800, + 1666310800, + 1696972200, + 1584429000, + 1436789200, + 1749024200 + ], + "total_leaves": 32590958400, + "solutions": 0 + } + }, + "seven_source_upper_from_pr4232": { + "path": [ + 6, + 0, + 5, + 5, + 4, + 0, + 0, + 3, + 4, + 4, + 2, + 3, + 3, + 1, + 2, + 2, + 6, + 1, + 1, + 5, + 6 + ], + "six_readout_boundaries": [ + 0, + 0, + 1, + 2, + 8, + 14 + ], + "calls": 405 + } +} diff --git a/research/f3-seven-source-connector-floor/README.md b/research/f3-seven-source-connector-floor/README.md new file mode 100644 index 0000000000..fe4c4d598b --- /dev/null +++ b/research/f3-seven-source-connector-floor/README.md @@ -0,0 +1,139 @@ +# Unsigned F3 connector: the floor fails at seven sources + +For seven immutable sources, all 127 nonzero binary-mask outputs and one +arbitrarily dirty restored connector over F3, no word attains the 402-call +floor. Combined with the 405-call word of +[#4232](https://github.com/CrocSwap/integer-mult-bounds/pull/4232), the exact +seven-source optimum is **405 calls**. By #4232's deletion lemma, the floor +3(n + 2^n − 1) is attained **exactly for n ≤ 6** and fails for every n ≥ 7. + +This answers #4232's open question 1. The claim is a scoped proof whose +exhaustive step is a finite computer census, run by two separately written +enumerators that use different arithmetic and different symmetry reductions. +There is no new κ, no selected-frontier change and no multiplication theorem. + +## 1. Interface and reduction (from predecessors) + +The interface is #4232's: rows are n read-only sources x_j, 2^n − 1 outputs +y_m and one borrowed dirty connector z. The only calls are unsigned +`B_j: z += B_j x_j` and `A_m: y_m += A_m z` with arbitrary F3-linear maps. The +word must add `sum_(j in m) A_m B_j x_j` to every y_m and restore x and z. + +Two facts are taken from #4232 (head `86ad339efc9f817846479431d8cc0f04edf95fb9`), +which extends #4225's mod-three count argument: + +- every call count is a positive multiple of three, so the floor is + 3(n + 2^n − 1) and any word that misses it has at least three more calls; +- a floor word is a restored source path of length 3n, each source three times, + with three readouts per mask, and it is correct exactly when every binary + mask equals q_a + q_b + q_c for prefix boundaries a ≤ b ≤ c. Here q_t ∈ F3^n + counts source events modulo three after t steps. + +#4232 also supplies the seven-source 405-call word (masks 1..126 by readout +triples, mask 127 by six readouts) and the deletion lemma. This package +re-runs the 405-word check as a cheap self-contained step. The new content is +the exclusion in section 2. + +## 2. No seven-source floor path exists + +**Rotation invariance.** Because each source occurs three times, q_{3n} = 0 = +q_0, so the boundaries form a cycle of 3n points. Rotating the path to start +at position r replaces every q_t by q_{t+r} − q_r. A readout triple sum changes +by −3q_r = 0. The set of served masks is therefore invariant under cyclic +rotation, and also under relabelling the sources, since the mask set is +closed under coordinate permutations. + +**Census.** A floor path for n = 7 exists exactly when some path in either +reduced family below serves all 127 masks: + +| Engine | Reduction | Paths checked | Floor paths | +|---|---|---:|---:| +| `engine/reduced.c` | labels by first occurrence; rotated so position 0 is an event whose gap to the same source's next event is the path's minimum cyclic gap | 4,130,223,840 | 0 | +| `engine/independent.c` | labels by first occurrence; rotated so the last event differs from the first | 32,590,958,400 | 0 | + +Each family meets every rotation-and-relabelling orbit. For the first, rotate +any minimum-gap event to position 0. For the second, pick r with +s_(r−1) ≠ s_r, which exists because n ≥ 2. The engines also differ in +arithmetic. The first packs F3 vectors as two bit masks and uses a bitwise +adder. The second uses base-3 integers and digit-wise tables. Both mark the +pair sums q_a + q_b and accept mask m when m − q_c is a marked pair for some c. + +**Calibration.** For n = 1..6 both engines find floor paths, and their counts +are recorded in [CERTIFICATE.json](CERTIFICATE.json). For n ≤ 4 a pure-Python +brute force over every path, with no symmetry and a direct triple-sum test, +matches both engines. It confirms that each reduced solution list meets every +solution orbit and contains only solutions. + +## 3. Consequences + +- The seven-source optimum is 405: no 402-call word exists, and every call + count is a multiple of three, so 405 is the next possible value, attained + by #4232's word. +- The floor-attaining set is exactly {1, …, 6}. The deletion lemma says a + floor word at n gives one at n − 1, so failure at 7 propagates to every + n ≥ 7. This replaces #4232's interval 6 ≤ N ≤ 13 with N = 6. +- For every n ≥ 7 the optimum is at least 3(n + 2^n − 1) + 3. Exact values for + n ≥ 8 remain open. +- Open PR [#4248](https://github.com/CrocSwap/integer-mult-bounds/pull/4248) + (head `e7df122403cfc2febfb6799abb821487d8d1ee49`) reaches the unsigned floor + for k ≤ 2c sources in characteristic c. At c = 3 that gives k ≤ 6, so with + this exclusion its range is exactly the attaining set in characteristic three. + +## 4. Reproduction + +From the repository root (a C11 compiler `cc` is required): + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/f3-seven-source-connector-floor/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/f3-seven-source-connector-floor/verify.py --n7-shards 0,1 +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/f3-seven-source-connector-floor/verify.py --n7-all +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/f3-seven-source-connector-floor/verify.py --n7-independent +``` + +The default mode runs the calibration, brute-force cross-checks, the 405-word +check and controls (marker `PASS_F3_SEVEN_SOURCE_CALIBRATION`). `--n7-shards` +replays named shards of the reduced census and compares their leaf counts with +the certificate (marker `PASS_F3_SEVEN_SOURCE_SHARDS`). `--n7-all` and +`--n7-independent` replay the whole census for one engine (marker +`PASS_F3_SEVEN_SOURCE_CENSUS`). They use every available core. Measured +locally on an 18-core Apple machine: about 25 CPU minutes (2.5 minutes wall) for the +reduced engine and about 12.5 minutes wall, all 18 cores busy, for the +independent one. The independent leaf count equals the closed form +((3n)!/6^n − n(3n−2)!/6^(n−1))/n!, which the default mode checks for n = 2..7. +[VERIFY.json](VERIFY.json) registers the calibration and six of the 18 +reduced shards (0, 1, 8, 9, 16, 17), the most the 1200 s package replay cap +holds. The complete reduced census (`--n7-all`) and the independent census +(`--n7-independent`) are opt-in. Their per-shard leaf counts are in the +certificate. + +## 5. Limitations + +- The exclusion is a computer census, not a written proof. CI replays only six + of the 18 reduced shards; the full censuses of both engines were run locally + and are reproducible with the opt-in commands. No proof-kernel + check, SAT certificate or independent human review is claimed. The two + engines share the reduction to boundary triples from #4232, so a flaw in + that reduction would affect both. +- The result covers only the unsigned, immutable-source, complete-call + interface over F3. Admission, coefficient preparation, dispatch and physical + costs are additional and unknown. No consumer is instantiated. + +## Open next questions + +1. What is the exact optimum for n = 8..13? The floor fails, so each optimum + is at least the floor plus three. Is it exactly the floor plus three, as for + n = 7? +2. What is the largest number of masks a 21-event seven-source path serves with + triples? #4232's annealing reached 126; the census here could also record + the maximum, which would bound how many masks need longer readout lists. +3. Can the n = 7 exclusion be given a short written argument, for example from + the window form of #4232 applied to the all-ones mask and the weight-six + masks? + +## Credit + +Produced by Nick Petalas. The interface, readout criterion, deletion lemma and +405-call seven-source word are from #4232. The mod-three count argument and the +five-source word come from #4225. The F3 alphabet and one-source handoff are +Riquelme Soares's #4189. The connector interface and prefix-readout criterion +originate in Ross Richardson's #943. Apache-2.0. diff --git a/research/f3-seven-source-connector-floor/SOURCES.json b/research/f3-seven-source-connector-floor/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/f3-seven-source-connector-floor/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/f3-seven-source-connector-floor/TASK.json b/research/f3-seven-source-connector-floor/TASK.json new file mode 100644 index 0000000000..fc1d38b100 --- /dev/null +++ b/research/f3-seven-source-connector-floor/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "Decide whether the unsigned F3 seven-source connector (seven immutable sources, all 127 nonzero binary-mask outputs, one arbitrarily dirty restored connector) attains the 402-call floor of three calls per operator.", + "scope_change_reason": "Keeps the F3 alphabet and answers PR4232's open question 1, a source-count question the card lists as a scope-change trigger. With PR4232's deletion lemma it fixes the exact batch size up to which an F3 connector pays three calls per operator.", + "bottleneck_link": "Bounds the largest batch at which an F3 connector consumer can pay exactly three calls per operator: six sources. No physical consumer, admission or transfer is supplied, so no kappa change follows.", + "budget_minutes": 60, + "stop_rule": "Stop after the exhaustive n=7 census with two engines and the n<=6 and brute-force calibrations. Exact optima for n>=8 are left open.", + "outcome": "completed", + "evidence": "Two separately written C enumerators check every restored 21-event path up to rotation and relabelling; neither finds a path serving all 127 masks. CERTIFICATE.json records per-shard leaf counts and n<=6 calibration counts; verify.py cross-checks both reductions against a pure-Python brute force for n<=4 and re-checks PR4232's 405-call word.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact optimum for each n=8..13?", + "why_it_matters": "A consumer of a larger F3 batch needs the exact surcharge; only floor+3 is known as a lower bound.", + "first_step": "Search for words whose source path serves all but a few masks with triples and pays six readouts for the rest, then bound the number of triple-served masks.", + "blocked_by": "No upper or lower bound beyond floor+3 is proved for n>=8." + }, + { + "question": "What is the maximum number of masks a seven-source 21-event path serves with readout triples?", + "why_it_matters": "It bounds how many outputs need longer readout lists in any near-floor word.", + "first_step": "Extend reduced.c to record the maximum served count instead of exiting at the first unserved mask.", + "blocked_by": "The census exits early and records only the decision." + }, + { + "question": "Is there a short written proof that no seven-source floor path exists?", + "why_it_matters": "It would replace a 4e9-path census and might explain where the threshold sits.", + "first_step": "Apply PR4232's window form to the all-ones mask and the seven weight-six masks.", + "blocked_by": "No structural argument is known." + } + ], + "predecessor_handoff": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4232", + "head": "86ad339efc9f817846479431d8cc0f04edf95fb9", + "author": "Nick Petalas", + "usage": "Interface, boundary-triple reduction, deletion lemma and 405-call seven-source word; open question 1 answered here. No executable dependency." + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19081034", + "upstream_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "overlap_scope": "100 live open PR titles, 60 recent account PRs, last 30 handoff comments, find_overlap helper, and merged README grep for seven-source F3 terms. Only PR4232 studies the n-source unsigned F3 floor; a concurrent characteristic-four claim is a separate question.", + "family_decision": "Local interface result; stop. No construction round is justified without a consumer." + } +} diff --git a/research/f3-seven-source-connector-floor/VERIFY.json b/research/f3-seven-source-connector-floor/VERIFY.json new file mode 100644 index 0000000000..8e6dd5d6b0 --- /dev/null +++ b/research/f3-seven-source-connector-floor/VERIFY.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Compile both C engines; replay n=1..6 calibration counts for both; pure-Python brute force for n<=4 matching both engines, with every solution orbit met by the reduced census; PR4232's 405-call seven-source word; positive, negative and shard-partition controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--n7-shards", + "0,1" + ], + "timeout_seconds": 320, + "checks": "Reduced-engine n=7 census shards 0,1 of 18: zero floor paths and leaf counts equal to CERTIFICATE.json. A sample of the census; the complete census is the opt-in --n7-all replay." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--n7-shards", + "8,9" + ], + "timeout_seconds": 320, + "checks": "Reduced-engine n=7 census shards 8,9 of 18: zero floor paths and leaf counts equal to CERTIFICATE.json. A sample of the census; the complete census is the opt-in --n7-all replay." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--n7-shards", + "16,17" + ], + "timeout_seconds": 320, + "checks": "Reduced-engine n=7 census shards 16,17 of 18: zero floor paths and leaf counts equal to CERTIFICATE.json. A sample of the census; the complete census is the opt-in --n7-all replay." + } + ], + "notes": "Requires a C11 compiler named cc. The 1200 s package replay cap holds six of the 18 reduced-engine shards. The complete reduced census (about 1350 CPU seconds; {python} -B {package}/verify.py --n7-all) and the independent-engine census (about 12.5 minutes wall on 18 cores; --n7-independent) are opt-in and compare against the per-shard leaf counts in CERTIFICATE.json." +} diff --git a/research/f3-seven-source-connector-floor/engine/independent.c b/research/f3-seven-source-connector-floor/engine/independent.c new file mode 100644 index 0000000000..1f36c99d81 --- /dev/null +++ b/research/f3-seven-source-connector-floor/engine/independent.c @@ -0,0 +1,63 @@ +/* Independent second enumerator (different arithmetic and symmetry). + Points are base-3 integers; addition uses a digit-wise table. Pair sums + are marked; a mask is served when mask - q_c is a marked pair sum. + Symmetry: labels in first-occurrence order, and the path is rotated so + that its last event differs from its first (always possible for n >= 2). + Sharding splits at depth 8, so it needs 3n > 8. + Usage: independent n nshards shard */ +#include +#include +#include +static int n, L, NS, SH, P3, path[24], cnt[8], used; +static uint64_t leaves, sols, ctr; +static int add_tab[2187][2187]; +static int pw[8], binmask3[256]; +static int addv(int a, int b) { + int r = 0; + for (int j = 0; j < n; j++) r += ((a / pw[j] % 3 + b / pw[j] % 3) % 3) * pw[j]; + return r; +} +static int sub_tab[2187][2187]; +static uint32_t stampv[2187], gen; +static int order[128]; +static int check(void) { + int q[24]; q[0] = 0; + for (int t = 1; t < L; t++) q[t] = add_tab[q[t - 1]][pw[path[t - 1]]]; + gen++; + for (int a = 0; a < L; a++) + for (int b = a; b < L; b++) stampv[add_tab[q[a]][q[b]]] = gen; + for (int k = 0; k < (1 << n) - 1; k++) { /* mask = q_a + q_b + q_c iff mask - q_c is a pair sum */ + int m = binmask3[order[k]], ok = 0; + for (int c = 0; c < L && !ok; c++) ok = stampv[sub_tab[m][q[c]]] == gen; + if (!ok) return 0; + } + return 1; +} +static void rec(int t) { + if (t == 8 && (ctr++ % NS) != (uint64_t)SH) return; + if (t == L) { + if (path[L - 1] == path[0]) return; + leaves++; + if (check()) { sols++; if (sols <= 5) { printf("SOLUTION"); for (int i = 0; i < L; i++) printf(" %d", path[i]); printf("\n"); } } + return; + } + int top = used < n ? used + 1 : n; + for (int s = 0; s < top; s++) { + if (cnt[s] == 3) continue; + int ou = used; if (s == used) used++; + cnt[s]++; path[t] = s; rec(t + 1); cnt[s]--; used = ou; + } +} +int main(int argc, char **argv) { + if (argc != 4) { fprintf(stderr, "usage: independent n nshards shard\n"); return 2; } + n = atoi(argv[1]); NS = atoi(argv[2]); SH = atoi(argv[3]); L = 3 * n; + if (n < 2 || n > 7 || NS < 1 || SH < 0 || SH >= NS) return 2; + P3 = 1; for (int j = 0; j < n; j++) { pw[j] = P3; P3 *= 3; } + for (int a = 0; a < P3; a++) for (int b = 0; b < P3; b++) add_tab[a][b] = addv(a, b); + for (int a = 0; a < P3; a++) for (int b = 0; b < P3; b++) sub_tab[addv(a, b)][b] = a; + { int k = 0; for (int w = n; w >= 1; w--) for (int m = 1; m < (1 << n); m++) if (__builtin_popcount(m) == w) order[k++] = m; } + for (int m = 0; m < (1 << n); m++) { int r = 0; for (int j = 0; j < n; j++) if (m >> j & 1) r += pw[j]; binmask3[m] = r; } + rec(0); + printf("RESULT n=%d shard=%d/%d leaves=%llu solutions=%llu\n", n, SH, NS, (unsigned long long)leaves, (unsigned long long)sols); + return 0; +} diff --git a/research/f3-seven-source-connector-floor/engine/reduced.c b/research/f3-seven-source-connector-floor/engine/reduced.c new file mode 100644 index 0000000000..7c2f78f9f8 --- /dev/null +++ b/research/f3-seven-source-connector-floor/engine/reduced.c @@ -0,0 +1,116 @@ +/* Enumerate restored unsigned F3 connector source paths (n sources, each used + three times) and decide whether one readout triple serves every nonzero + binary mask. Usage: reduced n nshards shard sym(0|1) [print_limit] + sym=1: labels in first-occurrence order, source 0 at position 0, and the + first gap of source 0 equal to the minimum cyclic gap of the path. + sym=0: every path (no reduction), for cross-validation. */ +#include +#include +#include + +#define MAXN 8 +#define MAXL (3 * MAXN) + +static int n, L, nshards, shard, sym, print_limit; +static int path[MAXL], cnt[MAXN], first[MAXN], last[MAXN]; +static int used_labels, g0; +static uint64_t leaves, solutions, prefix_counter; +static uint32_t stamp[1 << (2 * MAXN)]; +static uint32_t gen; +static int mask_order[1 << MAXN]; +static int split_depth; + +static inline void add3(int alo, int ahi, int blo, int bhi, int *clo, int *chi) { + int an = ~(alo | ahi), bn = ~(blo | bhi); + *clo = (alo & bn) | (blo & an) | (ahi & bhi); + *chi = (ahi & bn) | (bhi & an) | (alo & blo); +} + +static int check(void) { + int lo[MAXL], hi[MAXL], full = (1 << n) - 1; + lo[0] = hi[0] = 0; + for (int t = 1; t < L; t++) { /* q_t = q_{t-1} + e_{path[t-1]} */ + int b = 1 << path[t - 1]; + add3(lo[t - 1], hi[t - 1], b, 0, &lo[t], &hi[t]); + lo[t] &= full; hi[t] &= full; + } + gen++; + if (gen == 0) { for (int i = 0; i < (1 << (2 * n)); i++) stamp[i] = 0; gen = 1; } + for (int i = 0; i < L; i++) + for (int j = i; j < L; j++) { + int sl, sh; + add3(lo[i], hi[i], lo[j], hi[j], &sl, &sh); + stamp[(sl & full) | ((sh & full) << n)] = gen; + } + for (int k = 0; k < full; k++) { + int m = mask_order[k], ok = 0; + for (int c = 0; c < L && !ok; c++) { + int dl, dh; /* m - q_c = m + (-q_c) */ + add3(m, 0, hi[c], lo[c], &dl, &dh); + if (stamp[(dl & full) | ((dh & full) << n)] == gen) ok = 1; + } + if (!ok) return 0; + } + return 1; +} + +static void rec(int t) { + if (t == split_depth) { + if ((prefix_counter++ % nshards) != (uint64_t)shard) return; + } + if (t == L) { + leaves++; + if (check()) { + solutions++; + if (solutions <= (uint64_t)print_limit) { + printf("SOLUTION"); + for (int i = 0; i < L; i++) printf(" %d", path[i]); + printf("\n"); + } + } + return; + } + int top = sym ? (used_labels < n ? used_labels + 1 : n) : n; + for (int s = 0; s < top; s++) { + if (cnt[s] == 3) continue; + if (sym) { + if (t < g0 && s == 0 && t != 0) continue; /* source 0 waits */ + if (t == g0 && s != 0) continue; /* second 0 at g0 */ + if (cnt[s] > 0 && t - last[s] < g0) continue; + if (cnt[s] == 2 && L - t + first[s] < g0) continue; + } + int ol = last[s], of = first[s], ou = used_labels; + if (cnt[s] == 0) { first[s] = t; if (s == used_labels) used_labels++; } + last[s] = t; cnt[s]++; path[t] = s; + rec(t + 1); + cnt[s]--; last[s] = ol; first[s] = of; used_labels = ou; + } +} + +int main(int argc, char **argv) { + if (argc < 5) { fprintf(stderr, "usage: reduced n nshards shard sym [print_limit]\n"); return 2; } + n = atoi(argv[1]); nshards = atoi(argv[2]); shard = atoi(argv[3]); sym = atoi(argv[4]); + print_limit = argc > 5 ? atoi(argv[5]) : 5; + if (n < 1 || n > MAXN || nshards < 1 || shard < 0 || shard >= nshards) return 2; + L = 3 * n; + split_depth = L < 9 ? L : 9; + /* hardest masks first: by descending weight */ + int k = 0; + for (int w = n; w >= 1; w--) + for (int m = 1; m < (1 << n); m++) + if (__builtin_popcount(m) == w) mask_order[k++] = m; + if (sym) { + for (g0 = 1; 3 * g0 <= L; g0++) { + prefix_counter = 0; + for (int s = 0; s < n; s++) cnt[s] = 0; + used_labels = 0; + rec(0); + } + } else { + prefix_counter = 0; used_labels = n; + rec(0); + } + printf("RESULT n=%d sym=%d shard=%d/%d leaves=%llu solutions=%llu\n", n, sym, shard, nshards, + (unsigned long long)leaves, (unsigned long long)solutions); + return 0; +} diff --git a/research/f3-seven-source-connector-floor/verify.py b/research/f3-seven-source-connector-floor/verify.py new file mode 100644 index 0000000000..c36a949389 --- /dev/null +++ b/research/f3-seven-source-connector-floor/verify.py @@ -0,0 +1,259 @@ +"""Verify the seven-source unsigned F3 connector floor exclusion. + +Default mode: compile both C engines, replay their n <= 6 calibration counts +against CERTIFICATE.json, cross-check the engines and both symmetry +reductions against a pure-Python brute force for n <= 4, check the 405-call +seven-source word cited from PR4232, and run rejection controls. + +--n7-shards K,... replay those reduced-engine shards of the n = 7 census. +--n7-all replay all 18 reduced-engine shards (about 25 CPU minutes). +--n7-independent replay all 18 independent-engine shards (about 12.5 minutes + wall on 18 cores). The last two are opt-in. +""" + +import argparse +import concurrent.futures +import hashlib +import itertools +import json +import math +import os +import pathlib +import re +import subprocess +import sys +import tempfile + +HERE = pathlib.Path(__file__).resolve().parent +PACKAGE_FILES = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "CERTIFICATE.json", "verify.py", "engine/reduced.c", + "engine/independent.c") +RESULT_RE = re.compile(r"^RESULT n=(\d+) .*leaves=(\d+) solutions=(\d+)$", re.M) +SOLUTION_RE = re.compile(r"^SOLUTION((?: \d+)+)$", re.M) + + +def require(cond, message): + if not cond: + raise SystemExit("FAIL: " + message) + + +def compile_engines(workdir): + binaries = {} + for name in ("reduced", "independent"): + out = workdir / name + subprocess.run(["cc", "-O3", "-std=c11", "-Wall", "-Wextra", "-Werror", + "-o", str(out), str(HERE / "engine" / (name + ".c"))], + check=True, capture_output=True, text=True) + binaries[name] = out + return binaries + + +def run_engine(binary, args): + proc = subprocess.run([str(binary)] + [str(a) for a in args], + capture_output=True, text=True, check=True) + found = RESULT_RE.findall(proc.stdout) + require(len(found) == 1, f"one RESULT line expected from {binary.name} {args}") + paths = [tuple(map(int, s.split())) for s in SOLUTION_RE.findall(proc.stdout)] + return int(found[0][1]), int(found[0][2]), paths + + +# ---- pure-Python model ------------------------------------------------- + +def prefix_points(path, n): + q = [(0,) * n] + for s in path: + v = list(q[-1]) + v[s] = (v[s] + 1) % 3 + q.append(tuple(v)) + return q + + +def served_masks(path, n): + """Binary masks equal to q_a + q_b + q_c for boundaries a <= b <= c.""" + q = prefix_points(path, n) + sums = {tuple((x + y + z) % 3 for x, y, z in zip(q[a], q[b], q[c])) + for a, b, c in itertools.combinations_with_replacement(range(len(q)), 3)} + return {m for m in range(1, 1 << n) + if tuple((m >> j) & 1 for j in range(n)) in sums} + + +def all_paths(n): + """Every arrangement of the multiset {0^3, ..., (n-1)^3}.""" + def rec(prefix, counts): + if len(prefix) == 3 * n: + yield tuple(prefix) + return + for s in range(n): + if counts[s] < 3: + counts[s] += 1 + prefix.append(s) + yield from rec(prefix, counts) + prefix.pop() + counts[s] -= 1 + yield from rec([], [0] * n) + + +def relabel(path): + lab = {} + for s in path: + lab.setdefault(s, len(lab)) + return tuple(lab[s] for s in path) + + +def cyclic_gaps(path): + L = len(path) + gap = {} + for s in set(path): + pos = [i for i, x in enumerate(path) if x == s] + for k in range(3): + gap[pos[k]] = (pos[(k + 1) % 3] - pos[k]) % L + return gap + + +def reduced_forms(path): + """Rotations starting at a minimum-gap event, relabelled.""" + gap = cyclic_gaps(path) + g = min(gap.values()) + return {relabel(path[r:] + path[:r]) for r in gap if gap[r] == g} + + +# ---- checks -------------------------------------------------------------- + +def check_calibration(cert, binaries): + for key, rec in cert["calibration"].items(): + n = int(key) + leaves, sols, _ = run_engine(binaries["reduced"], [n, 1, 0, 1, 0]) + require([leaves, sols] == rec["reduced"], f"reduced engine n={n}: {leaves},{sols}") + if n >= 2: + leaves, sols, _ = run_engine(binaries["independent"], [n, 1, 0]) + require([leaves, sols] == rec["independent"], + f"independent engine n={n}: {leaves},{sols}") + print("calibration n=1..6 reduced and independent counts match") + + +def independent_family_size(n): + """Relabelled paths whose last event differs from the first, in closed form.""" + L = 3 * n + arrangements = math.factorial(L) // 6 ** n + same_ends = n * math.factorial(L - 2) // 6 ** (n - 1) + return (arrangements - same_ends) // math.factorial(n) + + +def check_independent_sizes(cert): + for key, rec in cert["calibration"].items(): + if "independent" in rec: + require(rec["independent"][0] == independent_family_size(int(key)), + f"independent family size n={key}") + require(cert["n7"]["independent"]["total_leaves"] == independent_family_size(7), + "independent n=7 census size") + print("independent engine leaf counts equal the closed-form family size for n=2..7") + + +def check_brute_force(cert, binaries): + for n in (2, 3, 4): + paths = list(all_paths(n)) + good = [p for p in paths if len(served_masks(p, n)) == (1 << n) - 1] + rec = cert["calibration"][str(n)] + require([len(paths), len(good)] == rec["all_paths"], f"brute force n={n}") + # Independent engine: relabelled paths whose last event differs from the first. + canon = {relabel(p) for p in good if p[-1] != p[0]} + require(len(canon) == rec["independent"][1], f"independent symmetry n={n}") + # Reduced engine: its solution list must meet every orbit and contain only solutions. + _, _, red = run_engine(binaries["reduced"], [n, 1, 0, 1, 10 ** 6]) + red = set(red) + require(len(red) == rec["reduced"][1], f"reduced list n={n}") + require(all(len(served_masks(p, n)) == (1 << n) - 1 for p in red), + f"reduced engine reports a non-solution at n={n}") + require(all(reduced_forms(p) & red for p in good), + f"a solution orbit is missing from the reduced census at n={n}") + print(f"brute force n={n}: {len(paths)} paths, {len(good)} solutions; " + "both reductions meet every solution orbit") + + +def check_seven_upper(cert): + w = cert["seven_source_upper_from_pr4232"] + path, n = w["path"], 7 + require(sorted(path) == sorted(list(range(n)) * 3), "seven-source path counts") + served = served_masks(path, n) + require(served == set(range(1, 127)), "PR4232 path serves masks 1..126") + q = prefix_points(path, n) + total = [sum(q[b][j] for b in w["six_readout_boundaries"]) % 3 for j in range(n)] + require(total == [1] * n, "six readouts serve mask 127") + calls = len(path) + 3 * 126 + 6 + require(calls == w["calls"] == 405, "405 calls") + require(3 * (n + 2 ** n - 1) == 402, "floor 402") + print("seven-source 405-call word from PR4232: masks 1..126 by triples, 127 by six readouts") + + +def check_controls(binaries): + # A floor path at n = 6 is found (positive control); a sorted path fails. + _, sols, paths = run_engine(binaries["reduced"], [6, 1, 0, 1, 1]) + require(sols > 0 and len(served_masks(paths[0], 6)) == 63, "n=6 positive control") + require(len(served_masks(tuple(s for s in range(6) for _ in range(3)), 6)) < 63, + "sorted six-source path must fail") + # Shards partition the census: n = 6 reduced leaves add up over 7 shards. + whole, _, _ = run_engine(binaries["reduced"], [6, 1, 0, 1, 0]) + parts = sum(run_engine(binaries["reduced"], [6, 7, k, 1, 0])[0] for k in range(7)) + require(parts == whole, "shard partition control") + print("controls rejected/accepted as expected; shards partition n=6") + + +def run_n7(cert, binaries, engine, shards): + rec = cert["n7"][engine] + nshards = rec["shards"] + args = {k: ([7, nshards, k, 1, 0] if engine == "reduced" else [7, nshards, k]) + for k in shards} + workers = max(1, min(len(shards), os.cpu_count() or 1)) + with concurrent.futures.ThreadPoolExecutor(workers) as pool: + results = dict(zip(shards, pool.map(lambda k: run_engine(binaries[engine], args[k]), + shards))) + for k in shards: + leaves, sols, _ = results[k] + require(sols == 0, f"{engine} shard {k} found a floor path") + require(leaves == rec["leaves"][k], f"{engine} shard {k} leaves {leaves}") + print(f"n=7 {engine} shards {shards}: 0 floor paths, leaf counts match") + if sorted(shards) == list(range(nshards)): + require(sum(rec["leaves"]) == rec["total_leaves"], "total leaves") + print(f"n=7 {engine} census complete: {rec['total_leaves']} paths, none attains 402") + + +def receipt(): + h = hashlib.sha256() + for name in PACKAGE_FILES: + data = (HERE / name).read_bytes() + h.update(name.encode() + b"\0" + hashlib.sha256(data).hexdigest().encode() + b"\n") + return h.hexdigest() + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--n7-shards", default="") + ap.add_argument("--n7-all", action="store_true") + ap.add_argument("--n7-independent", action="store_true") + opts = ap.parse_args() + cert = json.loads((HERE / "CERTIFICATE.json").read_text()) + with tempfile.TemporaryDirectory() as tmp: + binaries = compile_engines(pathlib.Path(tmp)) + if opts.n7_shards: + run_n7(cert, binaries, "reduced", [int(k) for k in opts.n7_shards.split(",")]) + marker = "PASS_F3_SEVEN_SOURCE_SHARDS" + elif opts.n7_all or opts.n7_independent: + if opts.n7_all: + run_n7(cert, binaries, "reduced", list(range(cert["n7"]["reduced"]["shards"]))) + if opts.n7_independent: + run_n7(cert, binaries, "independent", + list(range(cert["n7"]["independent"]["shards"]))) + marker = "PASS_F3_SEVEN_SOURCE_CENSUS" + else: + check_calibration(cert, binaries) + check_brute_force(cert, binaries) + check_independent_sizes(cert) + check_seven_upper(cert) + check_controls(binaries) + marker = "PASS_F3_SEVEN_SOURCE_CALIBRATION" + print("receipt_sha256", receipt()) + print(marker) + + +if __name__ == "__main__": + sys.exit(main()) From aa61e1746f8c12807bed59cd169591bd82320bc6 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 22:12:10 +0100 Subject: [PATCH 2/2] fix(research): fit the seven-source calibration in the CI replay budget The hosted runner timed out the default mode at 240 s. Use a pair-sum brute force, move the independent n=6 calibration to the opt-in mode, and give each registered command 300 s. --- .../f3-seven-source-connector-floor/README.md | 7 ++--- .../VERIFY.json | 12 ++++----- .../f3-seven-source-connector-floor/verify.py | 26 ++++++++++++------- 3 files changed, 26 insertions(+), 19 deletions(-) diff --git a/research/f3-seven-source-connector-floor/README.md b/research/f3-seven-source-connector-floor/README.md index fe4c4d598b..3bc0fb800a 100644 --- a/research/f3-seven-source-connector-floor/README.md +++ b/research/f3-seven-source-connector-floor/README.md @@ -90,12 +90,13 @@ From the repository root (a C11 compiler `cc` is required): ~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/f3-seven-source-connector-floor/verify.py --n7-independent ``` -The default mode runs the calibration, brute-force cross-checks, the 405-word -check and controls (marker `PASS_F3_SEVEN_SOURCE_CALIBRATION`). `--n7-shards` +The default mode runs the calibration (reduced engine n ≤ 6, independent +engine n ≤ 5), brute-force cross-checks, the 405-word check and controls (marker `PASS_F3_SEVEN_SOURCE_CALIBRATION`). `--n7-shards` replays named shards of the reduced census and compares their leaf counts with the certificate (marker `PASS_F3_SEVEN_SOURCE_SHARDS`). `--n7-all` and `--n7-independent` replay the whole census for one engine (marker -`PASS_F3_SEVEN_SOURCE_CENSUS`). They use every available core. Measured +`PASS_F3_SEVEN_SOURCE_CENSUS`); `--n7-independent` also replays the +independent engine's n = 6 calibration. They use every available core. Measured locally on an 18-core Apple machine: about 25 CPU minutes (2.5 minutes wall) for the reduced engine and about 12.5 minutes wall, all 18 cores busy, for the independent one. The independent leaf count equals the closed form diff --git a/research/f3-seven-source-connector-floor/VERIFY.json b/research/f3-seven-source-connector-floor/VERIFY.json index 8e6dd5d6b0..206d9c829f 100644 --- a/research/f3-seven-source-connector-floor/VERIFY.json +++ b/research/f3-seven-source-connector-floor/VERIFY.json @@ -13,8 +13,8 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 240, - "checks": "Compile both C engines; replay n=1..6 calibration counts for both; pure-Python brute force for n<=4 matching both engines, with every solution orbit met by the reduced census; PR4232's 405-call seven-source word; positive, negative and shard-partition controls." + "timeout_seconds": 300, + "checks": "Compile both C engines; replay reduced n=1..6 and independent n=2..5 calibration counts; pure-Python brute force for n<=4 matching both engines, with every solution orbit met by the reduced census; PR4232's 405-call seven-source word; positive, negative and shard-partition controls." }, { "argv": [ @@ -26,7 +26,7 @@ "--n7-shards", "0,1" ], - "timeout_seconds": 320, + "timeout_seconds": 300, "checks": "Reduced-engine n=7 census shards 0,1 of 18: zero floor paths and leaf counts equal to CERTIFICATE.json. A sample of the census; the complete census is the opt-in --n7-all replay." }, { @@ -39,7 +39,7 @@ "--n7-shards", "8,9" ], - "timeout_seconds": 320, + "timeout_seconds": 300, "checks": "Reduced-engine n=7 census shards 8,9 of 18: zero floor paths and leaf counts equal to CERTIFICATE.json. A sample of the census; the complete census is the opt-in --n7-all replay." }, { @@ -52,9 +52,9 @@ "--n7-shards", "16,17" ], - "timeout_seconds": 320, + "timeout_seconds": 300, "checks": "Reduced-engine n=7 census shards 16,17 of 18: zero floor paths and leaf counts equal to CERTIFICATE.json. A sample of the census; the complete census is the opt-in --n7-all replay." } ], - "notes": "Requires a C11 compiler named cc. The 1200 s package replay cap holds six of the 18 reduced-engine shards. The complete reduced census (about 1350 CPU seconds; {python} -B {package}/verify.py --n7-all) and the independent-engine census (about 12.5 minutes wall on 18 cores; --n7-independent) are opt-in and compare against the per-shard leaf counts in CERTIFICATE.json." + "notes": "Requires a C11 compiler named cc. The 1200 s package replay cap holds six of the 18 reduced-engine shards. The complete reduced census (about 1350 CPU seconds; {python} -B {package}/verify.py --n7-all) and the independent-engine census (about 12.5 minutes wall on 18 cores; --n7-independent) are opt-in (--n7-independent also replays the independent n=6 calibration) and compare against the per-shard leaf counts in CERTIFICATE.json." } diff --git a/research/f3-seven-source-connector-floor/verify.py b/research/f3-seven-source-connector-floor/verify.py index c36a949389..1b2dfebcce 100644 --- a/research/f3-seven-source-connector-floor/verify.py +++ b/research/f3-seven-source-connector-floor/verify.py @@ -1,7 +1,8 @@ """Verify the seven-source unsigned F3 connector floor exclusion. -Default mode: compile both C engines, replay their n <= 6 calibration counts -against CERTIFICATE.json, cross-check the engines and both symmetry +Default mode: compile both C engines, replay their calibration counts against +CERTIFICATE.json (reduced n <= 6, independent n <= 5; --n7-independent adds +the independent n = 6 count), cross-check the engines and both symmetry reductions against a pure-Python brute force for n <= 4, check the 405-call seven-source word cited from PR4232, and run rejection controls. @@ -71,10 +72,14 @@ def prefix_points(path, n): def served_masks(path, n): """Binary masks equal to q_a + q_b + q_c for boundaries a <= b <= c.""" q = prefix_points(path, n) - sums = {tuple((x + y + z) % 3 for x, y, z in zip(q[a], q[b], q[c])) - for a, b, c in itertools.combinations_with_replacement(range(len(q)), 3)} - return {m for m in range(1, 1 << n) - if tuple((m >> j) & 1 for j in range(n)) in sums} + pairs = {tuple((x + y) % 3 for x, y in zip(q[a], q[b])) + for a, b in itertools.combinations_with_replacement(range(len(q)), 2)} + served = set() + for m in range(1, 1 << n): + bits = [(m >> j) & 1 for j in range(n)] + if any(tuple((b - x) % 3 for b, x in zip(bits, qc)) in pairs for qc in q): + served.add(m) + return served def all_paths(n): @@ -119,16 +124,16 @@ def reduced_forms(path): # ---- checks -------------------------------------------------------------- -def check_calibration(cert, binaries): +def check_calibration(cert, binaries, max_independent): for key, rec in cert["calibration"].items(): n = int(key) leaves, sols, _ = run_engine(binaries["reduced"], [n, 1, 0, 1, 0]) require([leaves, sols] == rec["reduced"], f"reduced engine n={n}: {leaves},{sols}") - if n >= 2: + if 2 <= n <= max_independent: leaves, sols, _ = run_engine(binaries["independent"], [n, 1, 0]) require([leaves, sols] == rec["independent"], f"independent engine n={n}: {leaves},{sols}") - print("calibration n=1..6 reduced and independent counts match") + print(f"calibration: reduced n=1..6 and independent n=2..{max_independent} counts match") def independent_family_size(n): @@ -241,11 +246,12 @@ def main(): if opts.n7_all: run_n7(cert, binaries, "reduced", list(range(cert["n7"]["reduced"]["shards"]))) if opts.n7_independent: + check_calibration(cert, binaries, 6) run_n7(cert, binaries, "independent", list(range(cert["n7"]["independent"]["shards"]))) marker = "PASS_F3_SEVEN_SOURCE_CENSUS" else: - check_calibration(cert, binaries) + check_calibration(cert, binaries, 5) check_brute_force(cert, binaries) check_independent_sizes(cert) check_seven_upper(cert)