From 66d43a6c84bd13a93a9c2050de8b90eb75aa98ea Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 21:14:31 +0000 Subject: [PATCH] feat(research): decide the seven-event full-guard product inequality Compute the exact signed spectrum of all 2^42 seven-vertex characters with an orbit-reduced extension enumerator (493 entries), check the product inequality exactly for 6 <= n <= 400 and close every larger m with an integer tail bound. Scoped proof resting on a finite certificate; no kappa change. --- .../seven-event-guard-correlation/PROOF.md | 184 +++++++ .../seven-event-guard-correlation/README.md | 107 ++++ .../SOURCES.json | 42 ++ .../SPECTRUM_K7.txt | 493 ++++++++++++++++++ .../seven-event-guard-correlation/TASK.json | 111 ++++ .../seven-event-guard-correlation/VERIFY.json | 35 ++ .../seven-event-guard-correlation/spectrum.c | 274 ++++++++++ .../seven-event-guard-correlation/verify.py | 428 +++++++++++++++ 8 files changed, 1674 insertions(+) create mode 100644 research/seven-event-guard-correlation/PROOF.md create mode 100644 research/seven-event-guard-correlation/README.md create mode 100644 research/seven-event-guard-correlation/SOURCES.json create mode 100644 research/seven-event-guard-correlation/SPECTRUM_K7.txt create mode 100644 research/seven-event-guard-correlation/TASK.json create mode 100644 research/seven-event-guard-correlation/VERIFY.json create mode 100644 research/seven-event-guard-correlation/spectrum.c create mode 100644 research/seven-event-guard-correlation/verify.py diff --git a/research/seven-event-guard-correlation/PROOF.md b/research/seven-event-guard-correlation/PROOF.md new file mode 100644 index 0000000000..092a463a70 --- /dev/null +++ b/research/seven-event-guard-correlation/PROOF.md @@ -0,0 +1,184 @@ +# Seven orthogonal full-guard events lie below the product of their marginals + +This contribution was produced by Nick Petalas. Apache-2.0. Independent human +and formal proof-kernel review are unclaimed. + +**Claim type: scoped counting proof resting on an exact finite certificate.** +The all-dimension step is a written argument. Its single computational input is +the exact signed spectrum of all 2^42 seven-vertex characters, produced by +`spectrum.c`, committed in `SPECTRUM_K7.txt` and regenerated by `verify.py`. + +## Statement + +Let U_1, ..., U_7 be pairwise orthogonal rank-one idempotents on F_2^m, m >= 7, +and let G be uniform in GL_m(F_2). Event E_t says that every leading principal +minor of orders 1 through m-1 of G(I-U_t)G^-1 is nonzero. Write n = m-1, +X = 2^m and s_m = 3^n / ((X-1) 2^n), the probability of one event. + +**Theorem.** For every integer m >= 7, Pr(E_1 ∩ ... ∩ E_7) < s_m^7. + +At m = 7 the joint probability is 0. At m = 8 it is 29/5201587077120, about +5.575e-12, against s_8^7 of about 6.063e-9. The ratio rho_m = Pr / s_m^7 +tends to 1 from below, with 1 - rho_m = 42 (7/9)^(m-1) (1 + O((19/21)^(m-1))). + +This is the k = 7 case of the product inequality that PR6515 proves for k = 6, +PR4607 for k = 5 and PR4599 for k = 4. Those proofs, and the k = 6 spectrum, are +not used below. + +## 1. Inputs from the character law (cited, not re-proved) + +PR4275 (`research/corankone-triple-header-law`) proves, for k pairwise +orthogonal rank-one requests over F_2 and n = m-1: + +* Theorem 2: the number of passing headers is C |GL_(m-k)(F_2)| with + C = 2^(-k(k-1)) N_n, where N_n = sum over zero-diagonal binary k x k matrices c + of (-1)^|c| Z(c)^n, and Z(c) is the three-state sum + sum over sigma in {0,1,2}^k of (-1)^(sum of c_ij with sigma_i = 1, sigma_j = 2). +* Theorem 1: the fraction of passing headers is C / D with + D = 2^(k(m-k)) prod_(i= k + 1. + +Dividing, Pr_k(m) = N_n / (2^(kn) prod_(i= 6 (m >= 7, where X > 64). Summing out the label-2 coordinates gives the subset form + + Z(c) = sum over A subset of [k] such that every j outside A has even + incoming parity sum_(i in A) c_ij, of 2^(k-|A|). + +Group the characters by their value: H[z] = sum over c with Z(c) = z of (-1)^|c|, +so that N_n = sum_z H[z] z^n. + +## 2. The spectrum of all 2^42 characters + +A Gray-code walk over 2^42 matrices would take days. `spectrum.c` instead uses +two facts. + +**Relabelling.** Z(c) is unchanged by renaming the vertices. Fix the first five +vertices. The 2^20 digraphs on them fall into 9,608 orbits under S_5, so it +suffices to take one representative of each orbit, weighted by its orbit size, +and to sweep every arc pattern between the representative and the last two +vertices. + +**The last vertex in two tables.** Let c' be the digraph on the first six +vertices, with rows r_i, and let u (arcs from the six into vertex 7) and v (arcs +from vertex 7 into the six) be arbitrary six-bit sets. For A' a subset of the +six, let r[A'] be the xor of its rows. The condition defining Z(c) reads: + +* A = A' (vertex 7 outside A): r[A'] vanishes outside A', and |u ∩ A'| is even; + the weight is 2^(7-|A'|). +* A = A' + {7}: r[A'] xor v vanishes outside A'; the weight is 2^(6-|A'|). + +Hence Z(c) = F1(u) + F2(v), with + + F1(u) = sum over A' with r[A'] outside A' empty and |u ∩ A'| even of 2^(7-|A'|), + F2(v) = sum over A' with (r[A'] xor v) outside A' empty of 2^(6-|A'|). + +F1 is a Walsh-Hadamard transform of 64 numbers and F2 is a pass over the v that +agree with r[A'] outside A'. All 2^12 patterns of the last vertex then cost two +tables of 64 entries and 4,096 histogram updates, each carrying the sign +(-1)^(|u|+|v|) and the orbit weight. In all, 9,608 orbits times 2^10 patterns of +vertex 6 give 9.8 million sweeps. One process finishes in about 40 seconds. + +**Result** (`SPECTRUM_K7.txt`, 493 lines "z H[z]"): + +| fact | value | +|---|---| +| nonzero entries | 493 (247 positive, 246 negative); every z is odd | +| sum of H[z] | 0 | +| sum of abs(H[z]) | 2^42, so no value of Z carries both signs | +| top levels | H[2187] = 1, H[1701] = -42, H[1539] = 210 | +| next level | H[1485] = -280, then H[1467] = 210, H[1461] = -84 | +| below 1539 | largest z is 1485; sum of abs(H[z]) is A = 2^42 - 253 = 4,398,046,510,851 | +| N_n for n = 0..6 | 0 | +| N_7 / 2^42 | 29,816,640 = 7! * 5916 | + +The top levels are the single arcs (7*6 = 42, Z = 7*3^5 = 1701, odd, so sign -1) +and the two-arrow stars (7*6*5 = 210, Z = 19*3^4 = 1539), matching the equality +classification of PR6440 and the bound of PR5146. + +**Why this table is trusted.** The checks that `verify.py` runs, none of which +uses the answer: + +1. The enumerator equals labelled brute force over all matrices at k = 3, 4, 5, + and (`--brute6`) over all 2^30 matrices at k = 6. +2. At k = 3 and 4 it equals the literal three-state definition, and the subset + form equals the definition on every matrix at k = 3, 4 and on random samples + at k = 5, 6, 7. +3. Its k = 3 spectrum is the closed form of PR4275, and its k = 4 and k = 5 + leading coefficients and remainder bounds are those printed in PR4599 and + PR4607 (statements checked in the pinned files). +4. At k = 7, N_0 = ... = N_6 = 0, which is Theorem 3 of PR4275 (a header needs + n >= k); N_7 is divisible by 7!, as it must be, because a decomposition with + exactly k nonzero distinct rectangles can be ordered in k! ways; the counts + add to 2^42 characters; and a one-unit change to any top coefficient breaks the + vanishing moments (a control). +5. `--labelled7` repeats the k = 7 computation without the orbit reduction + (every labelled five-vertex digraph, weight one) and gets the same table. + +## 3. Dimensions m <= 401 + +For every 6 <= n <= 400 `verify.py` evaluates both sides of (R) with exact +integers from the full table and checks the strict inequality. At n = 6 (m = 7) +the left side is 0. For n < 6 the factors X - 2^j are not all positive and (R) is +not asserted. The ratio rho_m is about 0.00091954 at m = 8, 0.0107257 at +m = 9, 0.0961028 at m = 11, 0.264821 at m = 13, 0.617156 at m = 17, +0.827536 at m = 21, 0.981491 at m = 31 and 0.999858 at m = 51. + +## 4. Every larger dimension + +Let A be as above. Every z below 1539 is at most 1485, so for every n + + N_n <= 2187^n - 42*1701^n + 210*1539^n + A*1485^n + = 2187^n - 3*1701^n - L(n), + L(n) = 39*1701^n - 210*1539^n - A*1485^n. + +The integers give L(187) < 0 and L(188) > 0. Also + + L(n+1) - 1701 L(n) = 210*162*1539^n + 216*A*1485^n > 0, + +so L(n) > 0 for every n >= 188, and therefore + + N_n <= 2187^n - 3*1701^n for every n >= 188. (1) + +For X >= 64 put a_j = (2^j - 1)/(X-1), which lies in [0,1]. Then +X - 2^j = (X-1)(1 - a_j), and the inequality prod(1 - a_j) >= 1 - sum a_j +together with sum_(j=1..6) (2^j - 1) = 120 gives + + (X-2)(X-4)(X-8)(X-16)(X-32)(X-64) >= (X-1)^5 (X-121). (2) + +By (2), (R) follows from N_n (X-1) < 2187^n (X-121). By (1) this holds as soon as +120 * 2187^n < 3 * 1701^n (X-1), that is + + 40 * 9^n < 7^n (2^(n+1) - 1). (3) + +At n = 7 it reads 191,318,760 < 210,003,465. Write f(n) = 7^n (2^(n+1)-1) / 9^n. +Then f(n+1) / f(n) = 7(2^(n+2)-1) / (9(2^(n+1)-1)) exceeds 1, because +7(2^(n+2)-1) - 9(2^(n+1)-1) = 10*2^n + 2 > 0. So f(n) > 40 and (3) holds for +every n >= 7, hence (R) holds for every n >= 188. Section 3 covers 6 <= n <= 400. +Together they cover every m >= 7. `verify.py` checks L(187) < 0, L(188) > 0, +the growth identity, (1) for 188 <= n < 1000 directly from the table, (2) and +the step in (3) for 7 <= n < 400, and (3) at n = 7. QED. + +## 5. Rate + +From the top three levels, N_n / 2187^n = 1 - 42 (7/9)^n + 210 (19/27)^n + O((55/81)^n), +and (X-1)^6 / prod(X - 2^j) = 1 + O(2^-n), where 2^-n and (19/27)^n are both +smaller than (7/9)^n by exponential factors. This gives the stated rate. The exact +ratios at n = 100 and n = 400 agree with 42 (7/9)^n to within 0.1%. + +## Scope + +**Covered.** Exactly seven fixed, pairwise orthogonal rank-one requests over F_2, +complete uniform headers, every m >= 7. + +**Not settled.** k >= 8; odd characteristic; nonorthogonal or restricted request +families; negative association of six or seven indicators (a stronger statement +than the product inequality, with its own open questions in PR5860 and PR6515); +a human-checkable derivation of the spectrum, which rests on the program. + +**Not claimed.** A physical saving, a supplier, a new κ, a selected-frontier +change, or proof-kernel review of the C program. diff --git a/research/seven-event-guard-correlation/README.md b/research/seven-event-guard-correlation/README.md new file mode 100644 index 0000000000..58bbe1ff1d --- /dev/null +++ b/research/seven-event-guard-correlation/README.md @@ -0,0 +1,107 @@ +# Seven orthogonal full-guard events lie below the product of their marginals + +This contribution was produced by Nick Petalas. Apache-2.0. Independent human +and formal proof-kernel review are unclaimed. + +**Claim type: scoped counting proof resting on an exact finite certificate. No κ.** + +Over F_2, let U_1, ..., U_7 be pairwise orthogonal rank-one idempotents on F_2^m +and let G be uniform in GL_m(F_2). Event E_t says every leading principal minor of +orders 1 through m-1 of G(I-U_t)G^-1 is nonzero. With n = m-1, X = 2^m and +s_m = 3^n / ((X-1) 2^n) the probability of one event: + +```text +for every m >= 7: Pr(E_1 ∩ ... ∩ E_7) < s_m^7 +``` + +At m = 7 the joint probability is 0 (a passing header needs m >= k+1). At m = 8 it +is 29/5201587077120, about 5.575e-12, against s_8^7 of about 6.063e-9. The ratio +tends to 1 from below: 1 - rho_m = 42 (7/9)^(m-1) (1 + O((19/21)^(m-1))). + +This answers open next question 1 of unpaidmoon's [PR6515](https://github.com/CrocSwap/integer-mult-bounds/pull/6515) +(`research/six-event-guard-correlation`): the same inequality for seven events, +inside the strip 8 <= m <= 344 that it leaves open. The proof uses Nick Petalas's +character law (PR4275) as a cited premise and does not use the k = 6 theorem of +PR6515, the remainder bound of PR5146 or the k = 4, 5 theorems. + +## New step + +The signed spectrum of all 2^42 seven-vertex characters is computed exactly, in +about 40 seconds on one core, instead of by a 2^42 Gray-code walk. `spectrum.c` +(i) reduces the first five vertices to their 9,608 orbits under S_5, and +(ii) evaluates all 2^12 arc patterns of the last vertex from two 64-entry tables, +because Z(c) = F1(u) + F2(v) there ([PROOF.md](PROOF.md) section 2). The table +`SPECTRUM_K7.txt` has 493 entries; N_0 = ... = N_6 = 0 and N_7 / 2^42 = 29,816,640 = +7! * 5916. Strict inequality is checked with exact integers for every 6 <= n <= 400, and +an integer tail bound (L(187) < 0 < L(188)) closes every larger m. + +## Evidence + +From the repository root; a C compiler (`cc`, `gcc` or `clang`) is required. + +```sh +python3.12 -I -B research/seven-event-guard-correlation/verify.py # PASS_SEVEN_EVENT_GUARD_CORRELATION +python3.12 -I -B research/seven-event-guard-correlation/verify.py --brute6 # PASS_SEVEN_EVENT_GUARD_BRUTE6 +python3.12 -B scripts/research_package.py --package research/seven-event-guard-correlation +python3.12 -B scripts/check_research_commit.py --package research/seven-event-guard-correlation --check-source-history +``` + +The default replay regenerates the k = 7 spectrum and compares it byte for byte with +`SPECTRUM_K7.txt`; validates the enumerator against labelled brute force at k = 3, 4, +5, against the literal three-state definition at k = 3, 4, and against the spectra +printed in the pinned PR4275, PR4599 and PR4607 files; checks the subset form +against the definition on random characters at k = 5, 6, 7; checks the spectrum +facts, the exact range, the tail bound, the closing inequalities and the rate; and +runs six rejection controls (a one-unit change to a top coefficient, a doubled top +coefficient, a shifted subset weight, a doctored k = 4 spectrum, an altered pinned +statement, a wrong tail threshold). `--brute6` checks the orbit-reduced k = 6 +spectrum against labelled brute force over all 2^30 matrices. It also reproduces the +k = 6 figures reported in PR6515 (176 entries; 1, -30, 120 at 729, 567, 513) as a +by-product. `--labelled7` (not registered; about 7 minutes on 18 cores) repeats the +k = 7 run over every labelled five-vertex digraph with weight one and no orbit +reduction; it covers all 2^42 characters and gives the same 493-entry table. + +Local runs (CPython 3.12.15, macOS arm64, 18 cores, compiler `-std=c11 -O2 -Wall +-Wextra -Wpedantic -Werror`): the default replay takes 13.3 s wall (46 CPU-seconds, +four shards; one shard needs 37 s for the k = 7 table alone), also with `-O`; `--brute6` +takes 31.6 s (125 CPU-seconds). These are check durations, not a speed comparison. + +## Limitations + +* The spectrum is a finite computation by a program. It is validated as listed above + but not re-derived by hand, and no independent re-implementation is supplied. +* Covered: exactly seven pairwise orthogonal rank-one requests over F_2, complete + uniform headers, every m >= 7. +* Not settled: k >= 8, odd characteristic, nonorthogonal or restricted request + families, negative association of six or seven indicators (a stronger statement), + any physical sampling, selection or restoration cost. No supplier, κ or selected + frontier change. Lean, Docker and the selected cold replay were not run. + +## Open next questions + +Structured copies are in [TASK.json](TASK.json). + +1. **k = 8.** Does the inequality hold for every m >= 9? *First step:* extend + `spectrum.c` to eight vertices (a 30-bit base mask with 1,540,944 orbits under + S_6, and 128 x 128 sweeps), compressing the two tables to value histograms. + An extrapolation from the k = 7 timing gives roughly 30 core-hours (not run). + *Blocker:* compute time, not mathematics. +2. **All k.** The computed tables show levels 3^k, 7*3^(k-2), 19*3^(k-3), 55*3^(k-4) + with coefficients 1, -k(k-1), k(k-1)(k-2), -8*C(k,4) for k = 4..7 (checked by + `verify.py`, not proved), every Z odd and one sign per Z value. *First step:* + combine PR6440's third-level classification with a uniform bound on the remainder. + *Blocker:* no all-k bound on characters below the first levels. +3. **Shared kernel directions** (PR6515 open question 2). *First step:* test whether + PR4240's joint law for nonorthogonal rank-one requests extends to several requests + with one shared direction. *Blocker:* not examined here. + +## Credit + +Nick Petalas (PR4275) supplies the character law, the transfer and the binary +threshold; Nick Petalas (PR4599) the four-event inequality; Ryanson Jonathan +(PR4607) the five-event inequality and spectrum; Nick Petalas (PR5146) the remainder +bound; Nick Petalas (PR6440) the equality classification of the third level; +unpaidmoon (PR6515) the six-event inequality, the open question and the +enumeration-plus-tail method adapted here. The orbit reduction, the two-table sweep +and the k = 7 table are new in this package. The Weierstrass product inequality and +Walsh-Hadamard transform are classical. Predecessor packages are unchanged. diff --git a/research/seven-event-guard-correlation/SOURCES.json b/research/seven-event-guard-correlation/SOURCES.json new file mode 100644 index 0000000000..9bcef859c9 --- /dev/null +++ b/research/seven-event-guard-correlation/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/binary-character-remainder-gap/README.md", + "usage": "input", + "git_blob": "26dfd91cd1076ceae1732a8340daa70c746969a5", + "sha256": "d333054883ff2d9a5f8414d188b0e51c418d14de21f1f3ba927f5546c2d6661d" + }, + { + "path": "research/corankone-four-correlation/PROOF.md", + "usage": "input", + "git_blob": "6309eb879c93a3270a0912b40275c5678185b2a8", + "sha256": "c8966a14b9151ce0b94ee0c512dc81ba8cd537f01bd0c8fd6c1f27c97f275951" + }, + { + "path": "research/corankone-triple-header-law/PROOF.md", + "usage": "input", + "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8", + "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f" + }, + { + "path": "research/five-event-guard-correlation/PROOF.md", + "usage": "input", + "git_blob": "a84e5696ab202dfef0296e02d9cf26e85923eb3c", + "sha256": "a46e1d5ede453b996f545f29fa8ed50f9fc05b829192ee81d41ff0424301fc0a" + } + ] +} diff --git a/research/seven-event-guard-correlation/SPECTRUM_K7.txt b/research/seven-event-guard-correlation/SPECTRUM_K7.txt new file mode 100644 index 0000000000..91d42fd80b --- /dev/null +++ b/research/seven-event-guard-correlation/SPECTRUM_K7.txt @@ -0,0 +1,493 @@ +129 -720 +131 10080 +133 -40320 +135 110880 +137 -292320 +139 630000 +141 -1238328 +143 2343600 +145 -4433940 +147 8033760 +149 -14340480 +151 26861520 +153 -43591380 +155 67762800 +157 -107735880 +159 165337368 +161 -250204668 +163 374583636 +165 -553148232 +167 793206120 +169 -1124700360 +171 1570171560 +173 -2158074240 +175 2950680600 +177 -3950368800 +179 5235478108 +181 -6860557844 +183 8797412596 +185 -11163810384 +187 13978033020 +189 -17188853304 +191 20909121100 +193 -25081720160 +195 29590939420 +197 -34461233520 +199 39604057080 +201 -44921472848 +203 50299626580 +205 -55718670196 +207 61034950620 +209 -66120294240 +211 71095953026 +213 -75768195012 +215 80092945716 +217 -84027198850 +219 87515842960 +221 -90496696584 +223 93028693156 +225 -95197704574 +227 96683788536 +229 -97819136436 +231 98571462976 +233 -98836293570 +235 98772158520 +237 -98249238500 +239 97459230960 +241 -96284567700 +243 94933815466 +245 -93327540768 +247 91320333678 +249 -89336955540 +251 87097733730 +253 -84790306440 +255 82510834800 +257 -79833591880 +259 77338151660 +261 -74851073080 +263 72115697010 +265 -69655811316 +267 67145612478 +269 -64482885180 +271 61910741970 +273 -59613986376 +275 57152914350 +277 -54712247100 +279 52647576660 +281 -50165111430 +283 48033410880 +285 -46253619258 +287 43921642716 +289 -41949532506 +291 40269980562 +293 -38225226984 +295 36494720262 +297 -34915980078 +299 32960027961 +301 -31341365328 +303 30077245170 +305 -28432907160 +307 26860793400 +309 -25768336188 +311 24257137890 +313 -22939036260 +315 22189065402 +317 -20695752700 +319 19593787920 +321 -18926232360 +323 17592488970 +325 -16733198670 +327 16117274180 +329 -14971655846 +331 14170999850 +333 -13767903170 +335 12779750970 +337 -11999374380 +339 11733529020 +341 -10767360100 +343 10165824970 +345 -10072777960 +347 9111024720 +349 -8599238130 +351 8494741836 +353 -7706112080 +355 7326375070 +357 -7217535472 +359 6520917340 +361 -6141353330 +363 6144258225 +365 -5527049010 +367 5176802960 +369 -5234261760 +371 4635386952 +373 -4381427036 +375 4505077556 +377 -3937492020 +379 3725298528 +381 -3824756936 +383 3327003680 +385 -3181139780 +387 3274423054 +389 -2813098610 +391 2655836820 +393 -2786887740 +395 2399874330 +397 -2230737180 +399 2370551162 +401 -2006385360 +403 1889330940 +405 -2052063860 +407 1673786170 +409 -1582335510 +411 1716328320 +413 -1413842360 +415 1357746880 +417 -1460879000 +419 1192032800 +421 -1131687900 +423 1264136580 +425 -1028213130 +427 967456770 +429 -1074059070 +431 849344300 +433 -814989980 +435 934901100 +437 -723520980 +439 688898420 +441 -795507412 +443 609407750 +445 -593832050 +447 673468320 +449 -513642780 +451 496967520 +453 -590270520 +455 456727950 +457 -419043450 +459 513456090 +461 -371764260 +463 354989250 +465 -456035300 +467 317698150 +469 -305058320 +471 388034640 +473 -271305300 +475 261462810 +477 -337958544 +479 228871230 +481 -220755570 +483 293087760 +485 -197948730 +487 183355620 +489 -248066532 +491 162595272 +493 -152416460 +495 226406600 +497 -142746240 +499 134120280 +501 -187813710 +503 115423980 +505 -115872330 +507 163437330 +509 -98870940 +511 96201000 +513 -145412820 +515 86701440 +517 -81490500 +519 124964280 +521 -71005620 +523 67151070 +525 -112164570 +527 61440330 +529 -57556800 +531 96601680 +533 -52502310 +535 51677220 +537 -81995760 +539 43502970 +541 -41316870 +543 69805680 +545 -38726940 +547 37147530 +549 -66775170 +551 31954860 +553 -31896060 +555 58024470 +557 -27225240 +559 27257580 +561 -47693450 +563 22472380 +565 -22539300 +567 46686192 +569 -20185480 +571 19376420 +573 -38022670 +575 18088280 +577 -16835280 +579 32926320 +581 -15004500 +583 13653570 +585 -33770940 +587 12840275 +589 -12370960 +591 25489030 +593 -10610460 +595 11729690 +597 -23127440 +599 9723420 +601 -9424660 +603 21333060 +605 -8504160 +607 8285550 +609 -17882172 +611 7037772 +613 -7030604 +615 17083878 +617 -6149780 +619 6022940 +621 -14783020 +623 5809650 +625 -5062680 +627 11548670 +629 -4073580 +631 4022760 +633 -11145120 +635 4078620 +637 -3908940 +639 10381560 +641 -3105760 +643 3008320 +645 -8444800 +647 2533860 +649 -2766050 +651 7661570 +653 -2534490 +655 2444820 +657 -6941550 +659 2156700 +661 -1829730 +663 5446980 +665 -1981560 +667 1883910 +669 -5172020 +671 1479030 +673 -1426740 +675 5991930 +677 -1425480 +679 1413300 +681 -4192440 +683 908670 +685 -1201200 +687 3826200 +689 -945630 +691 833070 +693 -4264890 +695 834540 +697 -678510 +699 2488080 +701 -555240 +703 772380 +705 -2878680 +707 641970 +709 -530460 +711 3173100 +713 -561120 +715 499380 +717 -1821120 +719 406560 +721 -517860 +723 1484700 +725 -270480 +727 336840 +729 -2054710 +731 309862 +733 -293874 +735 1397172 +737 -213780 +739 232470 +741 -1005270 +743 206080 +745 -200200 +747 1306830 +749 -299040 +751 156240 +753 -706440 +755 160020 +757 -237160 +759 794220 +761 -141960 +763 216510 +765 -1261680 +767 151830 +769 -134540 +771 595140 +773 -115780 +775 170520 +777 -658140 +779 214200 +781 -158760 +783 859320 +785 -126000 +787 149100 +789 -493920 +791 116340 +793 -94080 +795 431340 +797 -70840 +799 66220 +801 -547680 +803 76440 +805 -80640 +807 302400 +809 -27160 +811 62160 +813 -367500 +815 98280 +817 -79800 +819 563430 +821 -49560 +823 49840 +825 -313600 +827 34230 +829 -33600 +831 254730 +833 -44100 +835 16800 +837 -392280 +839 18480 +841 -15120 +843 190890 +845 -15960 +847 28560 +849 -153720 +851 18942 +853 -28014 +855 319536 +857 -26124 +859 26124 +861 -132342 +863 10920 +865 -31080 +867 114450 +869 -17640 +871 7560 +873 -207060 +875 22680 +877 -13860 +879 72660 +881 -6720 +883 18900 +885 -68040 +887 11760 +889 -12600 +891 176400 +893 -19320 +895 6720 +897 -77700 +899 3570 +901 -4620 +903 51240 +905 -2520 +907 5040 +909 -103320 +915 20160 +917 -6300 +919 5040 +921 -32760 +923 3780 +925 -5040 +927 76440 +929 -1680 +931 7140 +933 -19740 +935 1680 +939 25200 +941 -840 +945 -73500 +947 2520 +949 -840 +951 11760 +955 1680 +957 -18480 +959 1680 +963 34020 +965 -840 +969 -5040 +973 -3024 +975 15246 +977 -882 +979 840 +981 -39270 +983 1680 +985 -840 +987 17430 +991 1680 +993 -6720 +995 2520 +997 -2520 +999 36960 +1001 -840 +1005 -11760 +1007 1260 +1009 -1260 +1011 4620 +1017 -16380 +1019 840 +1027 1680 +1029 -9660 +1031 1680 +1033 -1680 +1035 22680 +1037 -840 +1041 -5040 +1043 840 +1045 -1680 +1047 5040 +1053 -26670 +1055 420 +1059 4620 +1061 -420 +1071 9240 +1077 -2940 +1083 2520 +1089 -2520 +1095 22 +1097 -42 +1099 252 +1101 -294 +1103 210 +1107 8526 +1109 -280 +1111 420 +1113 -840 +1119 630 +1121 -140 +1125 -2940 +1135 700 +1137 -3220 +1139 630 +1141 -420 +1143 5880 +1147 70 +1149 -2520 +1155 1680 +1161 -4900 +1173 -140 +1179 3150 +1197 -2520 +1215 3248 +1217 -84 +1219 42 +1221 -420 +1227 210 +1233 -840 +1251 420 +1269 -1680 +1323 630 +1377 -210 +1459 14 +1461 -84 +1467 210 +1485 -280 +1539 210 +1701 -42 +2187 1 diff --git a/research/seven-event-guard-correlation/TASK.json b/research/seven-event-guard-correlation/TASK.json new file mode 100644 index 0000000000..4ed4f9dac6 --- /dev/null +++ b/research/seven-event-guard-correlation/TASK.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "The k = 7 case of the binary full-guard product inequality for pairwise orthogonal rank-one requests: for every m >= 7, Pr(E_1 ... E_7) < s_m^7 under a uniform GL_m(F_2) header, from the exact signed spectrum of all 2^42 characters.", + "scope_change_reason": "The pinned card asks whether a serialized target/paid invoice independently supports a claimed improvement. This package contains no invoice. It answers open question 1 of PR6515 (research/six-event-guard-correlation): the same inequality for seven events, which PR6515 proves for six. The proved statement is a signed comparison of header probabilities.", + "bottleneck_link": "Side result. Full-guard header probabilities say how often one uniform header satisfies several BIT requests at once; the product inequality says joint success is rarer than independence predicts. It changes no supplier, invoice or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop when the k = 7 inequality is decided for every m >= 7: a proof from the exact spectrum, or the first violating m. Do not claim k >= 8, negative association, odd characteristic, nonorthogonal kernels or any physical consequence.", + "outcome": "completed", + "evidence": "python3 -I -B research/seven-event-guard-correlation/verify.py prints PASS_SEVEN_EVENT_GUARD_CORRELATION: the orbit-reduced enumerator regenerates the 493-entry k = 7 spectrum equal to SPECTRUM_K7.txt, agrees with labelled brute force at k <= 5 and with the published k = 3, 4, 5 spectra, the strict inequality holds exactly for n = 6..400, and the integer tail bound from n = 188 closes every larger m. --brute6 prints PASS_SEVEN_EVENT_GUARD_BRUTE6 (labelled brute force over 2^30 matrices at k = 6).", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the product inequality hold for k = 8 at every m >= 9?", + "why_it_matters": "It would extend the sequence k = 4 (PR4599), 5 (PR4607), 6 (PR6515) and 7 (this package), and shows whether the exact-spectrum method scales.", + "first_step": "Raise the vertex limit of spectrum.c to 8: the base is six vertices (1,540,944 orbits under S_6, a 30-bit arc mask, so four lookup chunks) and each sweep has 128 x 128 patterns; compress the two 128-entry tables to value histograms before convolving them. Extrapolating the k = 7 timing gives roughly 30 core-hours (an estimate, not run).", + "blocked_by": "Compute time, not mathematics; the tail argument of PROOF.md carries over once the spectrum is known." + }, + { + "question": "Is there an all-k proof of the product inequality?", + "why_it_matters": "Each k so far needs its own finite spectrum. The computed tables show regular structure: every Z is odd, no Z value carries both signs, and the top levels are 3^k, -k(k-1) at 7*3^(k-2), +k(k-1)(k-2) at 19*3^(k-3).", + "first_step": "Use the observation (checked for k = 4..7, not proved) that the fourth level is -8*C(k,4) at 55*3^(k-4), together with PR6440's third-level classification, to bound the remainder below the top levels uniformly in k.", + "blocked_by": "No all-k bound on the characters below the first levels; PR5146 bounds only the second and third modes." + }, + { + "question": "Does the inequality survive when two request kernels share a direction (PR6515 open question 2)?", + "why_it_matters": "The orthogonal-kernel law does not describe overlapping requests, and PR6515 asks whether a six-event ratio can reach 1 at m = 7 with one shared direction.", + "first_step": "Read PR4240's joint header law for nonorthogonal rank-one requests and test whether it extends to several requests with one shared direction.", + "blocked_by": "Not examined here; the character law used by this package needs pairwise orthogonal kernels." + } + ] +} diff --git a/research/seven-event-guard-correlation/VERIFY.json b/research/seven-event-guard-correlation/VERIFY.json new file mode 100644 index 0000000000..f5c1f53ccd --- /dev/null +++ b/research/seven-event-guard-correlation/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/binary-character-remainder-gap/README.md", + "research/corankone-four-correlation/PROOF.md", + "research/corankone-triple-header-law/PROOF.md", + "research/five-event-guard-correlation/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Regenerates the exact signed k = 7 spectrum with spectrum.c (compiled with -Wall -Wextra -Wpedantic -Werror) and compares it with SPECTRUM_K7.txt; enumerator versus labelled brute force at k = 3, 4, 5, versus the three-state definition at k = 3, 4 and versus the published k = 3, 4, 5 spectra in the pinned files; subset form versus definition on samples; spectrum facts (493 entries, sums, vanishing N_0..N_6, N_7 divisible by 7!); exact strict inequality for n = 6..400; the integer tail bound from n = 188; the closing elementary inequalities; the asymptotic rate; and six rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--brute6" + ], + "timeout_seconds": 600, + "checks": "Labelled brute force over all 2^30 six-vertex matrices equals the orbit-reduced k = 6 spectrum (176 entries)." + } + ] +} diff --git a/research/seven-event-guard-correlation/spectrum.c b/research/seven-event-guard-correlation/spectrum.c new file mode 100644 index 0000000000..3ba22e4f0d --- /dev/null +++ b/research/seven-event-guard-correlation/spectrum.c @@ -0,0 +1,274 @@ +/* + * Signed spectrum of the binary full-guard character sum, for K <= 7 vertices. + * + * Over F_2 let c range over zero-diagonal K x K matrices (K*(K-1) free bits), + * let |c| be its number of ones, and define + * + * Z(c) = sum over A subset of [K] such that every j not in A satisfies + * sum_{i in A} c_ij = 0 (mod 2), of 2^(K-|A|). + * + * This subset form equals the three-state sum + * sum_{sigma in {0,1,2}^K} (-1)^{sum_ij c_ij [sigma_i=1][sigma_j=2]} + * (sum out the label-2 coordinates). The program prints, for every z with + * H[z] != 0, the line "z H[z]" where H[z] = sum_{c : Z(c)=z} (-1)^{|c|}. + * + * Modes (argv[2]): + * ext orbit representatives of the K-2 base vertices under their + * symmetric group, all arcs of vertex K-2 to and from the base, and a + * table sweep over every arc pattern of the last vertex. Z of the + * last vertex's 2^(2(K-1)) patterns is F1[u] + F2[v]: see sweep(). + * labelled the same sweep with every labelled base matrix, weight one + * (no symmetry reduction; a control for the orbit weights). + * brute every labelled K x K matrix, K <= 6 (a control that shares neither + * the orbit reduction nor the table sweep). + * + * usage: spectrum K [ext|labelled|brute] [shard nshards] + * Shards split the base representatives (or the matrices) round-robin; the + * caller adds the printed counts of all shards. Diagnostics go to stderr. + */ +#include +#include +#include +#include +#include + +typedef int64_t i64; + +enum { + MAXK = 7, /* vertices */ + MAXBASE = MAXK - 2, + MAXPERM = 120, /* 5! */ + MAXSUB = 64, /* subsets of the K-1 earlier vertices */ + MAXZ = 2188 /* 3^7 + 1 */ +}; + +typedef struct { + int K; + int zmax; /* 3^K, the largest possible Z */ + i64 hist[MAXZ]; + i64 characters; /* number of labelled characters accounted for */ +} Spectrum; + +typedef struct { + int b; /* base vertices, K - 2 */ + int nbits; /* arcs among base vertices, b(b-1) */ + int pos[MAXBASE][MAXBASE]; /* bit index of arc (i,j), i != j */ + int nperm; + int perm[MAXPERM][MAXBASE]; + uint32_t chunk[MAXPERM][3][256]; /* image of each 8-bit chunk of an arc mask */ +} Base; + +static int popc(uint32_t x) { return __builtin_popcount(x); } + +static i64 pow3(int k) { + i64 r = 1; + for (int i = 0; i < k; i++) r *= 3; + return r; +} + +static void spectrum_add(Spectrum *s, int z, i64 amount) { + assert(z >= 1 && z <= s->zmax); + s->hist[z] += amount; +} + +/* ------------------------------------------------------------ brute mode */ + +static void run_brute(Spectrum *s, int shard, int nshards) { + int K = s->K, nbits = K * (K - 1), pos[MAXK][MAXK], t = 0; + for (int i = 0; i < K; i++) + for (int j = 0; j < K; j++) + if (i != j) pos[i][j] = t++; + assert(t == nbits && K <= 6); + uint32_t nsub = 1u << K; + uint64_t total = 1ull << nbits; + for (uint64_t m = (uint64_t)shard; m < total; m += (uint64_t)nshards) { + uint32_t rows[MAXK], r[1u << 6]; + for (int i = 0; i < K; i++) { + rows[i] = 0; + for (int j = 0; j < K; j++) + if (i != j && ((m >> pos[i][j]) & 1u)) rows[i] |= 1u << j; + } + int z = 1 << K; /* A = empty set */ + r[0] = 0; + for (uint32_t a = 1; a < nsub; a++) { + r[a] = r[a & (a - 1)] ^ rows[__builtin_ctz(a)]; + if ((r[a] & ~a & (nsub - 1)) == 0) z += 1 << (K - popc(a)); + } + int sign = (popc((uint32_t)(m & 0xffffffffu)) + popc((uint32_t)(m >> 32))) & 1 ? -1 : 1; + spectrum_add(s, z, sign); + s->characters++; + } +} + +/* ------------------------------------------------------------ ext modes */ + +/* Next permutation in lexicographic order; returns 0 after the last one. */ +static int next_permutation(int *a, int n) { + int i = n - 2; + while (i >= 0 && a[i] > a[i + 1]) i--; + if (i < 0) return 0; + int j = n - 1; + while (a[j] < a[i]) j--; + int tmp = a[i]; a[i] = a[j]; a[j] = tmp; + for (int lo = i + 1, hi = n - 1; lo < hi; lo++, hi--) { + tmp = a[lo]; a[lo] = a[hi]; a[hi] = tmp; + } + return 1; +} + +static void base_init(Base *B, int K) { + int b = K - 2, t = 0; + assert(b >= 1 && b <= MAXBASE); + memset(B, 0, sizeof *B); + B->b = b; + for (int i = 0; i < b; i++) + for (int j = 0; j < b; j++) + if (i != j) B->pos[i][j] = t++; + B->nbits = t; + assert(t <= 24); /* three 8-bit chunks */ + int a[MAXBASE]; + for (int i = 0; i < b; i++) a[i] = i; + do { + assert(B->nperm < MAXPERM); + memcpy(B->perm[B->nperm++], a, sizeof(int) * (size_t)b); + } while (next_permutation(a, b)); + for (int p = 0; p < B->nperm; p++) { + int image[24]; + for (int i = 0; i < b; i++) + for (int j = 0; j < b; j++) + if (i != j) image[B->pos[i][j]] = B->pos[B->perm[p][i]][B->perm[p][j]]; + for (int c = 0; c < 3; c++) + for (int v = 0; v < 256; v++) { + uint32_t out = 0; + for (int q = 0; q < 8; q++) + if (c * 8 + q < B->nbits && ((v >> q) & 1)) out |= 1u << image[c * 8 + q]; + B->chunk[p][c][v] = out; + } + } +} + +/* Orbit size of x if x is the least element of its orbit, else 0. */ +static int base_orbit_size(const Base *B, uint32_t x) { + int fixed = 0; + for (int p = 0; p < B->nperm; p++) { + uint32_t y = B->chunk[p][0][x & 255] | B->chunk[p][1][(x >> 8) & 255] | B->chunk[p][2][(x >> 16) & 255]; + if (y < x) return 0; + if (y == x) fixed++; + } + assert(fixed >= 1 && B->nperm % fixed == 0); + return B->nperm / fixed; +} + +/* + * Add every arc pattern of the last vertex to the digraph on the K-1 earlier + * vertices whose adjacency rows are rows[0..K-2] (bit j of rows[i] is c_ij). + * Let u be the set of earlier vertices with an arc into the last vertex and v + * the set it points to. For A' a subset of the earlier vertices let + * r[A'] be the xor of its rows. Subsets A not containing the last vertex + * need r[A'] to vanish outside A' and an even overlap |u & A'|; subsets + * A' + {last} need r[A'] xor v to vanish outside A'. Hence + * Z = F1[u] + F2[v] with + * F1[u] = sum over A' with r[A'] & ~A' = 0 and parity(u & A') = 0 of 2^(K-|A'|), + * F2[v] = sum over A' with (r[A'] ^ v) & ~A' = 0 of 2^(K-|A'|-1). + * F1 comes from a Walsh-Hadamard transform and F2 from enumerating the v + * that agree with r[A'] outside A'. The sign of the last vertex's 2(K-1) + * arcs is (-1)^(|u|+|v|); `signed_weight` carries the sign and orbit weight + * of the rest. + */ +static void sweep(Spectrum *s, const uint32_t rows[], i64 signed_weight) { + int K = s->K, B1 = K - 1; + uint32_t nsub = 1u << B1, full = nsub - 1; + uint32_t r[MAXSUB]; + int g[MAXSUB], f2[MAXSUB], wsum = 0; + r[0] = 0; + for (uint32_t a = 0; a < nsub; a++) { + if (a) r[a] = r[a & (a - 1)] ^ rows[__builtin_ctz(a)]; + g[a] = ((r[a] & ~a & full) == 0) ? (1 << (K - popc(a))) : 0; + wsum += g[a]; + f2[a] = 0; + } + for (uint32_t len = 1; len < nsub; len <<= 1) /* Walsh-Hadamard transform of g */ + for (uint32_t i = 0; i < nsub; i += 2 * len) + for (uint32_t j = i; j < i + len; j++) { + int x = g[j], y = g[j + len]; + g[j] = x + y; + g[j + len] = x - y; + } + for (uint32_t a = 0; a < nsub; a++) { + uint32_t target = r[a] & ~a & full, sub = a; + int weight = 1 << (K - popc(a) - 1); + for (;;) { + f2[target | sub] += weight; + if (sub == 0) break; + sub = (sub - 1) & a; + } + } + for (uint32_t u = 0; u < nsub; u++) { + assert(((wsum + g[u]) & 1) == 0); + int f1 = (wsum + g[u]) / 2; + i64 su = (popc(u) & 1) ? -signed_weight : signed_weight; + for (uint32_t v = 0; v < nsub; v++) spectrum_add(s, f1 + f2[v], (popc(v) & 1) ? -su : su); + } + s->characters += (i64)nsub * (i64)nsub * (signed_weight < 0 ? -signed_weight : signed_weight); +} + +/* Extend one base matrix x (weight w) by the arcs of vertex b and sweep. */ +static void expand_base(Spectrum *s, const Base *B, uint32_t x, int w) { + int b = B->b; + uint32_t rows[MAXBASE + 1]; + for (int i = 0; i < b; i++) { + rows[i] = 0; + for (int j = 0; j < b; j++) + if (i != j && ((x >> B->pos[i][j]) & 1u)) rows[i] |= 1u << j; + } + for (uint32_t ext = 0; ext < (1u << (2 * b)); ext++) { + uint32_t into = ext & ((1u << b) - 1), out_of = ext >> b, full[MAXBASE + 1]; + for (int i = 0; i < b; i++) full[i] = rows[i] | (((into >> i) & 1u) << b); + full[b] = out_of; + i64 sw = ((popc(x) + popc(ext)) & 1) ? -(i64)w : (i64)w; + sweep(s, full, sw); + } +} + +static void run_ext(Spectrum *s, int labelled, int shard, int nshards) { + static Base B; + base_init(&B, s->K); + uint64_t total = 1ull << B.nbits, index = 0; + i64 reps = 0, orbit_total = 0; + for (uint64_t x = 0; x < total; x++) { + int w = labelled ? 1 : base_orbit_size(&B, (uint32_t)x); + if (w == 0) continue; + reps++; + orbit_total += w; + if ((int)(index++ % (uint64_t)nshards) == shard) expand_base(s, &B, (uint32_t)x, w); + } + assert(orbit_total == (i64)total); + fprintf(stderr, "base_matrices=%lld orbit_total=%lld\n", (long long)reps, (long long)orbit_total); +} + +int main(int argc, char **argv) { + if (argc < 2 || (argc != 2 && argc != 3 && argc != 5)) { + fprintf(stderr, "usage: spectrum K [ext|labelled|brute] [shard nshards]\n"); + return 2; + } + static Spectrum S; + S.K = atoi(argv[1]); + S.zmax = S.K >= 3 && S.K <= MAXK ? (int)pow3(S.K) : 0; + const char *mode = argc >= 3 ? argv[2] : "ext"; + int shard = argc == 5 ? atoi(argv[3]) : 0, nshards = argc == 5 ? atoi(argv[4]) : 1; + if (S.K < 3 || S.K > MAXK || shard < 0 || nshards < 1 || shard >= nshards) { + fprintf(stderr, "bad arguments\n"); + return 2; + } + if (strcmp(mode, "brute") == 0 && S.K <= 6) run_brute(&S, shard, nshards); + else if (strcmp(mode, "ext") == 0) run_ext(&S, 0, shard, nshards); + else if (strcmp(mode, "labelled") == 0) run_ext(&S, 1, shard, nshards); + else { + fprintf(stderr, "unknown mode or K too large for brute\n"); + return 2; + } + for (int z = 0; z < MAXZ; z++) + if (S.hist[z] != 0 && printf("%d %lld\n", z, (long long)S.hist[z]) < 0) return 1; + fprintf(stderr, "characters=%lld\n", (long long)S.characters); + return fflush(stdout) == 0 ? 0 : 1; +} diff --git a/research/seven-event-guard-correlation/verify.py b/research/seven-event-guard-correlation/verify.py new file mode 100644 index 0000000000..1e360cb938 --- /dev/null +++ b/research/seven-event-guard-correlation/verify.py @@ -0,0 +1,428 @@ +#!/usr/bin/env python3 +"""Seven orthogonal binary full-guard events lie below the product of their marginals. + +Over F_2, let U_1..U_7 be pairwise orthogonal rank-one idempotents on F_2^m and +G uniform in GL_m(F_2). E_t says every leading principal minor of order 1..m-1 +of G(I-U_t)G^-1 is nonzero. With n = m-1 and X = 2^m, Nick Petalas's PR4275 +character law gives the joint probability + + Pr(E_1 ... E_k) = N_n / (2^(kn) prod_{i= 7, + + N_n (X-1)^6 < 3^(7n) prod_{j=1..6} (X - 2^j) (n = m - 1) + +from the exact signed spectrum H of all 2^42 characters. The spectrum is +regenerated by spectrum.c (orbit-reduced extension enumerator) and compared with +SPECTRUM_K7.txt; the enumerator is validated against labelled brute force +(k <= 5 always, k = 6 with --brute6), the three-state definition, and the +spectra published in the pinned predecessor files for k = 3, 4, 5. + +Standard library only; every check raises an explicit exception, so `python -O` +keeps all of them. A C compiler (cc, gcc or clang) is required. + + python3 verify.py # full default replay + python3 verify.py --brute6 # k = 6 labelled brute-force control (2^30 matrices) + python3 verify.py --labelled7 # k = 7 without orbit reduction (about 4000 core-seconds) +""" +import argparse +import itertools +import math +import os +import pathlib +import random +import re +import shutil +import subprocess +import sys +import tempfile +import time +from fractions import Fraction + +PACKAGE = pathlib.Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +K = 7 +EXACT_N_MIN = 6 # m = 7 is the first dimension holding seven orthogonal requests +EXACT_N_MAX = 400 # exact big-integer comparison for n = EXACT_N_MIN .. EXACT_N_MAX +TAIL_N_MAX = 1000 # bound on the search for the tail threshold +MAX_SHARDS = 4 +PINNED = { + "law": "research/corankone-triple-header-law/PROOF.md", + "five": "research/five-event-guard-correlation/PROOF.md", + "four": "research/corankone-four-correlation/PROOF.md", +} + + +class Failure(Exception): + """A verification step failed.""" + + +def require(condition, message): + if not condition: + raise Failure(message) + + +def expect_failure(label, function, *args): + """A control: `function` must raise Failure on the doctored input.""" + try: + function(*args) + except Failure: + return + raise Failure("control did not reject: " + label) + + +# ---------------------------------------------------------------- spectrum IO + + +def parse_spectrum(text): + """Parse lines 'z count' with strictly increasing z and nonzero counts.""" + spectrum, previous = {}, 0 + for line in text.splitlines(): + fields = line.split(" ") + require(len(fields) == 2, "malformed spectrum line: %r" % line) + z, count = int(fields[0]), int(fields[1]) + require(z > previous and count != 0, "spectrum lines must increase with nonzero counts") + spectrum[z] = count + previous = z + return spectrum + + +def moment(spectrum, n): + return sum(count * z**n for z, count in spectrum.items()) + + +# ------------------------------------------------- the definition and subsets + + +def z_literal(arcs, k): + """Three-state sum over sigma in {0,1,2}^k of (-1)^{arcs from label 1 to label 2}.""" + total = 0 + for sigma in itertools.product(range(3), repeat=k): + parity = sum(1 for (i, j) in arcs if sigma[i] == 1 and sigma[j] == 2) & 1 + total += -1 if parity else 1 + return total + + +def z_subset(arcs, k): + """Subset form: A with even incoming parity outside A, weight 2^(k-|A|).""" + rows = [0] * k + for (i, j) in arcs: + rows[i] |= 1 << j + mask, total = (1 << k) - 1, 0 + for a in range(1 << k): + r = 0 + for i in range(k): + if (a >> i) & 1: + r ^= rows[i] + if (r & ~a & mask) == 0: + total += 1 << (k - bin(a).count("1")) + return total + + +def all_arcs(k): + return [(i, j) for i in range(k) for j in range(k) if i != j] + + +def definition_spectrum(k): + """Signed spectrum from the literal three-state definition; also compares the subset form.""" + arcs_all, spectrum = all_arcs(k), {} + for mask in range(1 << len(arcs_all)): + arcs = [arcs_all[b] for b in range(len(arcs_all)) if (mask >> b) & 1] + z = z_literal(arcs, k) + require(z == z_subset(arcs, k), "subset form differs from the definition at k=%d" % k) + spectrum[z] = spectrum.get(z, 0) + (-1 if len(arcs) & 1 else 1) + return {z: v for z, v in sorted(spectrum.items()) if v} + + +def sampled_definition_check(k, samples, seed): + """The subset form equals the three-state definition on random characters.""" + rng, arcs_all = random.Random(seed), all_arcs(k) + for _ in range(samples): + arcs = [a for a in arcs_all if rng.random() < rng.choice((0.1, 0.3, 0.5))] + require(z_literal(arcs, k) == z_subset(arcs, k), "subset form differs at k=%d" % k) + + +# ------------------------------------------------------------ the C enumerator + + +def find_compiler(): + for name in ("cc", "gcc", "clang"): + path = shutil.which(name) + if path: + return path + raise Failure("no C compiler (cc, gcc or clang) on PATH") + + +def build(workdir): + exe = pathlib.Path(workdir) / "spectrum" + flags = ["-std=c11", "-O2", "-Wall", "-Wextra", "-Wpedantic", "-Werror"] + done = subprocess.run([find_compiler()] + flags + ["-o", str(exe), str(PACKAGE / "spectrum.c")], + capture_output=True, text=True, timeout=300) + require(done.returncode == 0, "spectrum.c failed to compile:\n" + done.stderr) + return exe + + +def run_spectrum(exe, k, mode, shards=1): + """Run the enumerator on `shards` processes and add their counts.""" + require(1 <= shards <= 64, "bad shard count") + procs = [subprocess.Popen([str(exe), str(k), mode, str(s), str(shards)], + stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True) + for s in range(shards)] + spectrum, characters = {}, 0 + for proc in procs: + out, err = proc.communicate(timeout=3600) + require(proc.returncode == 0, "spectrum %d %s failed: %s" % (k, mode, err)) + found = re.search(r"characters=(\d+)", err) + require(found is not None, "spectrum printed no character count") + characters += int(found.group(1)) + for z, count in parse_pairs(out): + spectrum[z] = spectrum.get(z, 0) + count + require(characters == 2 ** (k * (k - 1)), "enumerator did not cover every character") + return {z: v for z, v in sorted(spectrum.items()) if v} + + +def parse_pairs(text): + for line in text.splitlines(): + z, count = line.split(" ") + yield int(z), int(count) + + +def format_spectrum(spectrum): + return "".join("%d %d\n" % (z, v) for z, v in sorted(spectrum.items())) + + +# ---------------------------------------------- published spectra (pinned text) + + +def pinned_text(key): + return " ".join((ROOT / PINNED[key]).read_text(encoding="utf-8").split()) + + +def check_pinned_statements(texts): + """The pinned predecessor files state the facts used as controls.""" + needles = { + "law": ["C(2,m,k) = 2^(-k(k-1)) sum_c (-1)^(|c|) Z(c)^n", + "(27^n - 6*21^n + 6*19^n - 6*17^n + 16*15^n - 18*13^n + 9*11^n - 2*9^n) / 64", + "exists if and only if m >= k + 1"], + "five": ["N_n = 243^n − 20·189^n + 60·171^n − 40·165^n", + "Σ_{z<189} |b_z| = 1,048,555", "max_{z<189} z = 171"], + "four": ["N_n = 81^n - 12*63^n + R_n", "|R_n| <= 4083*57^n"], + } + for key, items in needles.items(): + for needle in items: + require(needle in texts[key], "pinned %s file lacks: %s" % (key, needle)) + + +def check_published_spectra(spectra): + """k = 3, 4, 5 spectra against the closed forms in the pinned files.""" + three = {27: 1, 21: -6, 19: 6, 17: -6, 15: 16, 13: -18, 11: 9, 9: -2} + require(spectra[3] == three, "k=3 spectrum differs from the published closed form") + h4 = spectra[4] + below = {z: v for z, v in h4.items() if z < 63} + require(h4[81] == 1 and h4[63] == -12 and h4[57] == 24, "k=4 top coefficients differ") + require(sum(abs(v) for v in below.values()) == 4083 and max(below) == 57, "k=4 remainder differs") + h5 = spectra[5] + below = {z: v for z, v in h5.items() if z < 189} + require([h5[z] for z in (243, 189, 171, 165)] == [1, -20, 60, -40], "k=5 top coefficients differ") + require(sum(abs(v) for v in below.values()) == 1048555 and max(below) == 171, "k=5 remainder differs") + + +# --------------------------------------------------------- the k = 7 theorem + + +def check_spectrum_facts(h): + """Structural facts of the k = 7 spectrum, all read from the table.""" + require(len(h) == 493, "expected 493 nonzero spectrum entries") + require(sum(h.values()) == 0, "signed multiplicities must sum to zero") + require(sum(abs(v) for v in h.values()) == 2**42, "absolute multiplicities must sum to 2^42") + require(h[2187] == 1 and h[1701] == -42 and h[1539] == 210, "top three levels differ") + rest = {z: v for z, v in h.items() if z < 1539} + require(max(rest) == 1485 and sum(abs(v) for v in rest.values()) == 2**42 - 253, + "remainder bounds differ") + for n in range(7): + require(moment(h, n) == 0, "N_%d must vanish (binary threshold m >= k+1)" % n) + walks = moment(h, 7) + require(walks > 0 and walks % (2**42 * math.factorial(7)) == 0, + "N_7 must be a positive multiple of 2^42 * 7!") + return walks // 2**42 + + +def inequality_sides(h, n, k=K): + x = 2 ** (n + 1) + right = 3 ** (k * n) + for j in range(1, k): + right *= x - 2**j + return moment(h, n) * (x - 1) ** (k - 1), right + + +def check_exact_range(h): + """N_n (X-1)^6 < 3^(7n) prod (X - 2^j) for every EXACT_N_MIN <= n <= EXACT_N_MAX.""" + worst = (0, 1, 0) + for n in range(EXACT_N_MIN, EXACT_N_MAX + 1): + left, right = inequality_sides(h, n) + require(0 <= left < right, "inequality fails at n=%d (m=%d)" % (n, n + 1)) + if left * worst[1] > worst[0] * right: + worst = (left, right, n) + return worst + + +def tail_lemma(h): + """Constants of the integer tail bound, and the facts it needs.""" + big_a = sum(abs(v) for z, v in h.items() if z < 1539) + + def lam(n): + return 39 * 1701**n - 210 * 1539**n - big_a * 1485**n + + first = next((n for n in range(1, TAIL_N_MAX) if lam(n) >= 0), None) + require(first == 188 and lam(187) < 0, "tail threshold is not 188") + for n in range(first, TAIL_N_MAX): + require(lam(n) >= 0, "tail lemma lambda(n) < 0 at n=%d" % n) + for n in range(60): + gap = lam(n + 1) - 1701 * lam(n) + require(gap == 210 * 162 * 1539**n + 216 * big_a * 1485**n, "growth identity fails") + for n in range(first, TAIL_N_MAX): + bound = 2187**n - 3 * 1701**n + require(moment(h, n) <= bound, "N_n exceeds 2187^n - 3*1701^n at n=%d" % n) + return first + + +def check_closing_inequalities(): + """The two elementary inequalities that finish the tail argument.""" + require((2**8 - 1) * 7**7 > 40 * 9**7, "(2^(n+1)-1)(7/9)^n > 40 fails at n=7") + for n in range(7, 400): + require((2 ** (n + 2) - 1) * 7 > 9 * (2 ** (n + 1) - 1), "monotonicity fails at n=%d" % n) + x = 2 ** (n + 1) + product = math.prod(x - 2**j for j in range(1, 7)) + require(product >= (x - 1) ** 5 * (x - 121), "Weierstrass bound fails at n=%d" % n) + + +def check_top_levels(spectra): + """Observed for k = 4..7: levels 3^k, 7*3^(k-2), 19*3^(k-3), 55*3^(k-4) with + coefficients 1, -k(k-1), k(k-1)(k-2), -8*C(k,4). A finite observation, not a theorem.""" + for k in range(4, 8): + h, top = spectra[k], sorted(spectra[k], reverse=True)[:4] + levels = [3**k, 7 * 3 ** (k - 2), 19 * 3 ** (k - 3), 55 * 3 ** (k - 4)] + counts = [1, -k * (k - 1), k * (k - 1) * (k - 2), -8 * math.comb(k, 4)] + require(top == levels and [h[z] for z in top] == counts, "top levels differ at k=%d" % k) + + +def asymptotic_check(h): + """1 - rho_m = 42 (7/9)^(m-1) (1 + O((19/21)^(m-1))) shows in the exact ratios.""" + for n in (100, 400): + left, right = inequality_sides(h, n) + gap = Fraction(right - left, right) + predicted = 42 * Fraction(7, 9) ** n + require(abs(gap - predicted) * 1000 < predicted, "asymptotic form fails at n=%d" % n) + + +# --------------------------------------------------------------- the controls + + +def run_controls(h, spectra): + bumped = dict(h) + bumped[1701] += 1 + expect_failure("one-unit arc coefficient", check_spectrum_facts, bumped) + doubled = dict(h) + doubled[2187] = 2 + expect_failure("doubled top coefficient", check_exact_range, doubled) + expect_failure("shifted subset form", lambda: require( + all(z_subset(a, 3) + 1 == z_literal(a, 3) for a in ([], [(0, 1)], [(0, 1), (1, 2)])), + "shifted subset form")) + doctored = dict(spectra[4]) + doctored[57] += 1 + expect_failure("doctored k=4 spectrum", check_published_spectra, {**spectra, 4: doctored}) + texts = {key: pinned_text(key) for key in PINNED} + texts["five"] = texts["five"].replace("243^n", "244^n") + expect_failure("altered pinned statement", check_pinned_statements, texts) + expect_failure("wrong tail threshold", lambda: require( + (39 * 1701**187 - 210 * 1539**187 - (2**42 - 253) * 1485**187) >= 0, "threshold")) + + +# ------------------------------------------------------------------- drivers + + +def shard_count(): + return max(1, min(MAX_SHARDS, os.cpu_count() or 1)) + + +def replay_default(): + started = time.time() + committed = parse_spectrum((PACKAGE / "SPECTRUM_K7.txt").read_text(encoding="utf-8")) + texts = {key: pinned_text(key) for key in PINNED} + check_pinned_statements(texts) + definition = {k: definition_spectrum(k) for k in (3, 4)} + for k, samples in ((5, 60), (6, 40), (7, 20)): + sampled_definition_check(k, samples, seed=k) + with tempfile.TemporaryDirectory() as workdir: + exe = build(workdir) + spectra = {k: run_spectrum(exe, k, "ext") for k in (3, 4, 5, 6)} + for k in (3, 4, 5): + require(run_spectrum(exe, k, "brute") == spectra[k], "ext differs from brute at k=%d" % k) + for k in (3, 4): + require(definition[k] == spectra[k], "ext differs from the definition at k=%d" % k) + check_published_spectra(spectra) + h7 = run_spectrum(exe, K, "ext", shards=shard_count()) + require(h7 == committed, "regenerated k=7 spectrum differs from SPECTRUM_K7.txt") + walks = check_spectrum_facts(committed) + worst = check_exact_range(committed) + first = tail_lemma(committed) + check_closing_inequalities() + asymptotic_check(committed) + check_top_levels({**spectra, K: committed}) + run_controls(committed, spectra) + print("k=3..6 spectra: %s nonzero entries; ext equals brute at k<=5, definition at k<=4" + % "/".join(str(len(spectra[k])) for k in (3, 4, 5, 6))) + print("k=7 spectrum: 493 entries regenerated and equal to SPECTRUM_K7.txt; N_7/2^42 = %d = 7! * %d" + % (walks, walks // math.factorial(7))) + print("top four levels checked for k=4..7 (observation, not a theorem)") + print("exact range n=%d..%d: strict inequality; tightest n=%d, 1 - rho = %.3e" + % (EXACT_N_MIN, EXACT_N_MAX, worst[2], float(Fraction(worst[1] - worst[0], worst[1])))) + print("tail: lambda(n) >= 0 from n=%d, so N_n <= 2187^n - 3*1701^n for n >= %d" % (first, first)) + print("elapsed %.1f s" % (time.time() - started)) + print("PASS_SEVEN_EVENT_GUARD_CORRELATION") + + +def replay_brute6(): + with tempfile.TemporaryDirectory() as workdir: + exe = build(workdir) + brute = run_spectrum(exe, 6, "brute", shards=shard_count()) + require(brute == run_spectrum(exe, 6, "ext"), "ext differs from labelled brute force at k=6") + require(len(brute) == 176 and brute[729] == 1 and brute[567] == -30 and brute[513] == 120, + "k=6 spectrum shape differs") + print("k=6: labelled brute force over 2^30 matrices equals the orbit-reduced spectrum (176 entries)") + print("PASS_SEVEN_EVENT_GUARD_BRUTE6") + + +def replay_labelled7(): + committed = parse_spectrum((PACKAGE / "SPECTRUM_K7.txt").read_text(encoding="utf-8")) + with tempfile.TemporaryDirectory() as workdir: + exe = build(workdir) + labelled = run_spectrum(exe, K, "labelled", shards=max(1, os.cpu_count() or 1)) + require(labelled == committed, "labelled k=7 spectrum differs from SPECTRUM_K7.txt") + print("k=7: unreduced labelled base matrices give the committed spectrum") + print("PASS_SEVEN_EVENT_GUARD_LABELLED7") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__.split("\n")[0]) + group = parser.add_mutually_exclusive_group() + group.add_argument("--brute6", action="store_true", help="k=6 labelled brute-force control") + group.add_argument("--labelled7", action="store_true", help="k=7 control without orbit reduction") + args = parser.parse_args() + try: + if args.brute6: + replay_brute6() + elif args.labelled7: + replay_labelled7() + else: + replay_default() + except Failure as error: + print("FAIL: %s" % error, file=sys.stderr) + return 1 + return 0 + + +if __name__ == "__main__": + sys.exit(main())