Prove seven orthogonal binary full-guard events lie below the product of their marginals (no κ)

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) (2^m - 2^i).
+* Theorem 3: a passing header exists if and only if m >= k + 1.
+
+Dividing, Pr_k(m) = N_n / (2^(kn) prod_(i<k) (X - 2^i)). For k = 1,
+N_n = 3^n and Pr_1(m) = s_m. Dividing Pr_7(m) by s_m^7, the factors 2^(7n)
+and X-1 cancel, and the theorem is equivalent to
+
+    N_n (X-1)^6 < 3^(7n) (X-2)(X-4)(X-8)(X-16)(X-32)(X-64)          (R)
+
+for every n >= 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.

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.

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"
+    }
+  ]
+}