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..3bc0fb800a --- /dev/null +++ b/research/f3-seven-source-connector-floor/README.md @@ -0,0 +1,140 @@ +# 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 (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`); `--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 +((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..206d9c829f --- /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": 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": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--n7-shards", + "0,1" + ], + "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." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--n7-shards", + "8,9" + ], + "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." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--n7-shards", + "16,17" + ], + "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 (--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/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..1b2dfebcce --- /dev/null +++ b/research/f3-seven-source-connector-floor/verify.py @@ -0,0 +1,265 @@ +"""Verify the seven-source unsigned F3 connector floor exclusion. + +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. + +--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) + 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): + """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, 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 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(f"calibration: reduced n=1..6 and independent n=2..{max_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: + 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, 5) + 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())