From 58826666fa90b5c22ab84758625ef6eb981b149f Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 2 Nov 2026 13:50:39 +0000 Subject: [PATCH 1/2] Prove the k=6 binary full-guard product inequality For every m >= 6, six pairwise orthogonal rank-one full-guard events on GL_m(F_2) are strictly rarer than the sixth power of one event. The argument is the signed 2^30 character spectrum plus an integer tail. No selected-frontier change. Prepared by unpaidmoon with substantial Cursor Grok assistance. Co-authored-by: unpaidmoon --- research/six-event-guard-correlation/PROOF.md | 175 +++++++++++ .../six-event-guard-correlation/README.md | 61 ++++ .../six-event-guard-correlation/SOURCES.json | 36 +++ .../six-event-guard-correlation/TASK.json | 105 +++++++ .../six-event-guard-correlation/VERIFY.json | 24 ++ .../six-event-guard-correlation/spectrum.c | 82 +++++ .../six-event-guard-correlation/verify.py | 284 ++++++++++++++++++ 7 files changed, 767 insertions(+) create mode 100644 research/six-event-guard-correlation/PROOF.md create mode 100644 research/six-event-guard-correlation/README.md create mode 100644 research/six-event-guard-correlation/SOURCES.json create mode 100644 research/six-event-guard-correlation/TASK.json create mode 100644 research/six-event-guard-correlation/VERIFY.json create mode 100644 research/six-event-guard-correlation/spectrum.c create mode 100644 research/six-event-guard-correlation/verify.py diff --git a/research/six-event-guard-correlation/PROOF.md b/research/six-event-guard-correlation/PROOF.md new file mode 100644 index 0000000000..6f1d124f58 --- /dev/null +++ b/research/six-event-guard-correlation/PROOF.md @@ -0,0 +1,175 @@ +# Six orthogonal full-guard events lie below the product of their marginals + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +This answers the k=6 case of the open product inequality in +[discussion comment 19144831](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144831). +Nick Petalas's #4275 supplies the character law and the m=k threshold. +Ryanson Jonathan's #4599 and #4607 settle k=4 and k=5. The 19/21 remainder +gap is Nick Petalas's #5146. No new κ is claimed. + +## Statement + +Let m ≥ 6. Let U_1, …, U_6 be pairwise orthogonal rank-one idempotents on +F_2^m, and let G be uniform in GL_m(F_2). Event E_t says that every leading +principal minor of G(I−U_t)G^{−1}, of orders 1 through m−1, is nonzero. +Write n = m−1, X = 2^m and + +```text +s_m = 3^n / ((X−1) 2^n). +``` + +**Theorem.** For every integer m ≥ 6, + +```text +Pr(E_1 ∩ ⋯ ∩ E_6) < s_m^6. +``` + +At m = 6 the joint probability is 0. The ratio tends to 1 from below. The +proof is a scoped counting argument with one exhaustive 2^30-character +spectrum and an integer tail for every larger dimension. It is not a +negative-association theorem for other events, a supplier admission, or a +selected-frontier change. + +## 1. Reduction + +A basis change takes U_t to e_t e_tᵀ and only permutes complete headers. +#4275, Theorem 2, counts the headers whose first six diagonal guards all +pass. With N_n = Σ_c (−1)^{|c|} Z(c)^n and K = 30, + +```text +Z(c) = Σ_{σ in {0,1,2}^6} (−1)^{Σ_{i≠j} c_ij [σ_i=1][σ_j=2]}, +D_n = N_n / 2^{30}, +Pr = D_n / (2^{6n−30} (X−1)(X−2)(X−4)(X−8)(X−16)(X−32)) + = N_n / (2^{6n} (X−1)(X−2)(X−4)(X−8)(X−16)(X−32)). +``` + +The same theorem gives the one-event count 3^n, hence the marginal s_m. +Dividing Pr by s_m^6 cancels 2^{6n} and one factor of X−1, and produces + +```text +ρ_m = (N_n / 729^n) · H(X), +H(X) = (X−1)^5 / ((X−2)(X−4)(X−8)(X−16)(X−32)). +``` + +The subset form used by the enumerator, + +```text +Z(c) = Σ_{S: every j∉S has even incoming parity from S} 2^{6−|S|}, +``` + +is the closed form obtained by summing the label-2 coordinates in Z(c). +The verifier checks it against the literal three-state sum on every +zero-diagonal character at k=3 and k=4, and checks that the same enumerator +reproduces #4275's published k=3 coefficients and #4607's leading k=5 +coefficients 243^n − 20·189^n + 60·171^n. + +## 2. The signed spectrum + +The enumerator walks all 2^30 edge masks by a Gray code. Each step flips +one arc and updates the incoming-parity mask of the 2^{4} source sets that +contain that arc. The resulting 176 nonzero coefficients begin + +```text +N_n = 729^n − 30·567^n + 120·513^n + R_n. +``` + +Here 567 = 7·3^4 and 513 = 19·3^3. #5146 already separates these from +every matrix with two or more entries, whose character is at most 513. +The verifier evaluates the three-state sum on all 30 single arcs and on +all 120 two-arrow stars (six orientations on each triple of vertices, +every other entry zero). Each arc has Z = 567 and odd weight. Each star +has Z = 513 and weight 2. The absolute coefficients sum to 2^30, so no +character value contains both signs. Those two evaluations are therefore +the entire levels: coefficient −30 at 567 and +120 at 513. +Every other character has Z ≤ 495, and the absolute sum of those +coefficients is A = 1,073,741,673. Thus + +```text +R_n ≤ A·495^n, N_n ≤ 729^n − 30·567^n + 120·513^n + A·495^n. +``` + +Two direct counts fall out of the same table. N_n = 0 for 0 ≤ n ≤ 5, so +there is no positive walk of length less than 6 and the joint event is +empty at m = 6. At n = 6, N_6 / 2^30 = 23,040, an exact positive header +count at m = 7. Adding one to the single-arc coefficient makes N_5 nonzero, +so that vanishing is not a rounding accident. + +## 3. Dimensions 7 ≤ m ≤ 130 + +For n from 6 through 129 the verifier compares the integers + +```text +N_n · (X−1)^5 < 729^n · (X−2)(X−4)(X−8)(X−16)(X−32). +``` + +Each comparison is strict. Floating point already rounds ρ_m to 1 at these +dimensions; the sign is carried by the integer slack. Representative exact +ratios are about 0.000270 at m = 7, 0.00996 at m = 8, 0.3767 at m = 13 and +0.9988 at m = 41. + +## 4. Every larger dimension + +Let L(n) = 27·567^n − 120·513^n − A·495^n. The spectrum bound and L(n) ≥ 0 +give + +```text +N_n ≤ 729^n − 30·567^n + 120·513^n + A·495^n = 729^n − 3·567^n − L(n) + ≤ 729^n − 3·567^n. +``` + +The verifier finds L(129) > 0, and also that 26·567^{129} does not cover +the same remainder, so three single-arc modes are what this cap leaves at +the threshold. Expanding the definition gives + +```text +L(n+1) − 567 L(n) = 120·513^n·54 + A·495^n·72 > 0, +``` + +so L(n+1) > 567 L(n) and L stays positive. + +It remains to show (729^n − 3·567^n) H(X) < 729^n. Expanding the +denominator gives the integer identity + +```text +(X−1)^5 − (X−2)(X−4)(X−8)(X−16)(X−32) + = 57X^4 − 1230X^3 + 9910X^2 − 31739X + 32767. +``` + +For X ≥ 128 the positive lower terms satisfy 9910X^2 ≤ X^4 and +32767 ≤ X^4, so the difference is at most 59X^4. Therefore it is enough +that + +```text +3·567^n · (X−1)^5 > 59 · X^4 · 729^n, X = 2^{n+1}. +``` + +The verifier checks this at n = 129, where X = 2^{130}. If P(n) and N(n) +are the two sides, the next order is 2X, so + +```text +P(n+1)/P(n) = 567·((2X−1)/(X−1))^5 > 567·32 = 18144, +N(n+1)/N(n) = 16·729 = 11664. +``` + +The fifth-power ratio is strictly larger than 2 because +(2X−1)/(X−1) = 2 + 1/(X−1). A strict gap at n = 129 therefore stays +strict at every larger n. Also 729/567 = 9/7 > 1, and the verifier finds +729^{129} > 3·567^{129}, so 729^n > 3·567^n remains true and the +comparison upper bound stays nonnegative. The degree-four majorization +was checked at X = 128, the smallest integer in its hypothesis, and both +9910 ≤ X^2 and 32767 ≤ X^4 become looser as X grows. Hence ρ_m < 1 for +every n ≥ 129. Section 3 already includes that threshold, and sections 2 +through 4 together cover every m ≥ 6. + +## Scope + +**Covered.** Exactly six fixed, pairwise orthogonal rank-one requests over +F_2, with complete headers weighted equally, at every m ≥ 6. + +**Not settled.** k ≥ 7 inside the strip k+1 ≤ m ≤ 8(k(k−1)+1), odd +characteristic, restricted header families and nonorthogonal kernels. +#5146 already supplies a loose eventual bound past that strip; this package +does not rerun it and does not improve it for k ≥ 7. + +**Not claimed.** A physical saving, a supplier, a new κ, or proof-kernel +review. Header probabilities are not an executed caller. diff --git a/research/six-event-guard-correlation/README.md b/research/six-event-guard-correlation/README.md new file mode 100644 index 0000000000..83ec7c9f99 --- /dev/null +++ b/research/six-event-guard-correlation/README.md @@ -0,0 +1,61 @@ +# Six-event binary full-guard product inequality + +**Claim type: scoped counting proof with an exhaustive finite spectrum. No new κ.** + +For every m ≥ 6, six pairwise orthogonal rank-one full-guard events on a +uniform matrix G ∈ GL_m(F_2) are strictly rarer than the sixth power of one +such event. At m = 6 the joint count is 0. At m = 7 it is exactly 23,040 +headers. The ratio then increases toward 1 and stays below it. + +This is the k = 6 case left open by JoyboyBrian's handoff +[comment 19144831](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144831). +The character law is Nick Petalas's #4275. The k = 5 theorem is Ryanson +Jonathan's #4607. The single-arc and two-star eigenvalues are the sharp +#5146 spectrum, used here only at k = 6. Selected κ stays +781451/250000000. + +## Result + +The proof enumerates all 2^30 zero-diagonal characters. Their signed +transform is + +```text +N_n = 729^n − 30·567^n + 120·513^n + R_n, R_n ≤ 1073741673·495^n. +``` + +Exact integer comparison gives the strict ratio for 7 ≤ m ≤ 130. For every +larger m, that tail fits under 27 single-arc modes. The three modes left +over dominate the degree-four gap between (X−1)^5 and the six-event GL +denominator. Details, the induction, and the limits are in `PROOF.md`. + +## Reproduce + +From the repository root, CPython 3.12 and gcc, standard library only: + +```sh +python3.12 -B research/six-event-guard-correlation/verify.py +python3.12 -B scripts/research_package.py --package research/six-event-guard-correlation +``` + +The verifier compiles `spectrum.c`, checks the three-state sum against the +subset form at k = 3 and k = 4, matches the published k = 3 and leading k = 5 +coefficients, then checks the k = 6 theorem. It prints +`PASS_SIX_EVENT_GUARD_CORRELATION`. One normal run is the certificate. The +2^30 pass takes under a minute on this host. No files are written into the +package. Lean, Docker, selected-frontier replay and an independent human +review were not run. + +## Open next questions + +1. **k ≥ 7 in the finite strip.** The same product inequality is open for + seven or more orthogonal guards below the #5146 eventual range. The first + step is a support-truncated spectrum, or an exact count of length-k + rectangle decompositions of J−I, at k = 7. The blocker is that the raw + character space has order 2^42, so the k = 6 Gray code does not extend. +2. **Nonorthogonal kernels.** A single shared direction can change both the + marginal and the joint count. The first step is one explicit pair of + nonorthogonal rank-one idempotents at m = 7 whose six-event ratio meets + or exceeds 1, or a reduction to the orthogonal case. Nothing in this + package prices that configuration. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/six-event-guard-correlation/SOURCES.json b/research/six-event-guard-correlation/SOURCES.json new file mode 100644 index 0000000000..c14075a0a2 --- /dev/null +++ b/research/six-event-guard-correlation/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/corankone-triple-header-law/PROOF.md", + "usage": "provenance", + "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8", + "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f" + }, + { + "path": "research/five-event-guard-correlation/PROOF.md", + "usage": "provenance", + "git_blob": "a84e5696ab202dfef0296e02d9cf26e85923eb3c", + "sha256": "a46e1d5ede453b996f545f29fa8ed50f9fc05b829192ee81d41ff0424301fc0a" + }, + { + "path": "research/binary-character-remainder-gap/README.md", + "usage": "provenance", + "git_blob": "26dfd91cd1076ceae1732a8340daa70c746969a5", + "sha256": "d333054883ff2d9a5f8414d188b0e51c418d14de21f1f3ba927f5546c2d6661d" + } + ] +} diff --git a/research/six-event-guard-correlation/TASK.json b/research/six-event-guard-correlation/TASK.json new file mode 100644 index 0000000000..9e13962481 --- /dev/null +++ b/research/six-event-guard-correlation/TASK.json @@ -0,0 +1,105 @@ +{ + "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": "For every m >= 6, six pairwise orthogonal rank-one full-guard events on a uniform element of GL_m(F_2) are strictly rarer than the sixth power of one such event.", + "scope_change_reason": "Discussion handoff 19144831 files the binary full-guard product inequality under this task id. The pinned card asks whether a serialized target/paid invoice independently supports a claimed improvement. The proved statement is a signed comparison of six header events, not a supplier bill, and it does not change the selected frontier.", + "bottleneck_link": "The inequality is an independent signed moment of six complete-header events. It does not audit a supplier contract, admit a physical saving, or raise kappa.", + "budget_minutes": 60, + "stop_rule": "Stop once the k=6 inequality is proved for every m >= 6. Do not open k >= 7 and do not change the selected frontier.", + "outcome": "completed", + "evidence": "Exact signed spectrum of all 2^30 zero-diagonal characters: 176 bases, N_n = 729^n - 30*567^n + 120*513^n + R_n with R_n <= 1073741673*495^n. The 30 arcs and 120 two-arrow stars are the whole 567 and 513 levels. N_n = 0 for n < 6, and N_6/2^30 = 23040 headers at m = 7. Exact integer slack is positive for n = 6..129. For every n >= 129 the remainder fits under 27 single-arc modes, and the remaining 3 modes absorb the degree-four GL gap. A one-unit change of the arc coefficient makes N_5 nonzero.", + "author": "unpaidmoon, with substantial Cursor Grok assistance", + "ai_assistance": "Substantial Cursor Grok assistance; no independent human review. Prepared by unpaidmoon with substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does the same strict product inequality hold for every k >= 7 and every m with k+1 <= m <= 8(k(k-1)+1)?", + "why_it_matters": "k = 6 was the first open width in discussion comment 19144831. The inherited #5146 bound already covers the eventual range n >= 8(k(k-1)+1), so the missing theorem is the finite strip.", + "first_step": "At k = 7, bound or enumerate the characters above a support-truncated cutoff, or count the length-7 rectangle decompositions of J-I, and compare the resulting numerator with H(X) through the end of the strip.", + "blocked_by": "The raw character space has order 2^42, so the k = 6 Gray-code enumeration does not extend." + }, + { + "question": "Can one shared direction between two rank-one kernels push the six-event ratio to 1 or above at m = 7?", + "why_it_matters": "Orthogonality is an essential hypothesis of the character reduction. A single shared direction changes both the marginal and the joint count.", + "first_step": "Exhibit one explicit pair of nonorthogonal rank-one idempotents at m = 7 whose six-event ratio meets or exceeds 1, or reduce that configuration to the orthogonal case.", + "blocked_by": "None. This package prices only pairwise orthogonal kernels." + } + ] +} diff --git a/research/six-event-guard-correlation/VERIFY.json b/research/six-event-guard-correlation/VERIFY.json new file mode 100644 index 0000000000..67459acf1e --- /dev/null +++ b/research/six-event-guard-correlation/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json", + "research/corankone-triple-header-law/PROOF.md", + "research/five-event-guard-correlation/PROOF.md", + "research/binary-character-remainder-gap/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 480, + "checks": "Signed spectrum of all 2^30 characters; three-state sum versus the subset form on every k=3 and k=4 mask and on every k=6 arc and star; published k=3 law, k=4 recount and leading k=5 coefficients; exact positive slack for n=6..129; one-unit arc-coefficient mutation; integer tail from n=129." + } + ] +} diff --git a/research/six-event-guard-correlation/spectrum.c b/research/six-event-guard-correlation/spectrum.c new file mode 100644 index 0000000000..d21065ca68 --- /dev/null +++ b/research/six-event-guard-correlation/spectrum.c @@ -0,0 +1,82 @@ +/* Signed spectrum of the zero-diagonal binary full-guard character. + + For every edge-mask of a k-by-k zero-diagonal matrix, Z is the subset + form of the three-state character sum. Output lines are "Z b" where + b is the even-weight count minus the odd-weight count. k is 3, 4, 5 or 6. +*/ +#include +#include +#include + +int main(int argc, char **argv) { + int vertices = argc > 1 ? atoi(argv[1]) : 6; + if (vertices < 3 || vertices > 6) return 2; + int edge_count = vertices * (vertices - 1); + int subsets = 1 << vertices; + int z_limit = 1; + for (int i = 0; i < vertices; i++) z_limit *= 3; + + int *weight = calloc((size_t)subsets, sizeof(int)); + int *members = calloc((size_t)edge_count * subsets, sizeof(int)); + uint8_t *bit_of = calloc((size_t)edge_count * subsets, sizeof(uint8_t)); + int *member_count = calloc((size_t)edge_count, sizeof(int)); + if (!weight || !members || !bit_of || !member_count) return 3; + for (int subset = 0; subset < subsets; subset++) + weight[subset] = 1 << (vertices - __builtin_popcount((unsigned)subset)); + + int edge = 0; + for (int tail = 0; tail < vertices; tail++) { + for (int head = 0; head < vertices; head++) { + if (tail == head) continue; + int count = 0; + for (int subset = 0; subset < subsets; subset++) { + if (((subset >> tail) & 1) && !((subset >> head) & 1)) { + members[edge * subsets + count] = subset; + bit_of[edge * subsets + count] = (uint8_t)(1u << head); + count++; + } + } + member_count[edge] = count; + edge++; + } + } + + int64_t *even = calloc((size_t)z_limit + 1, sizeof(int64_t)); + int64_t *odd = calloc((size_t)z_limit + 1, sizeof(int64_t)); + uint8_t *failed = calloc((size_t)subsets, 1); + if (!even || !odd || !failed) return 3; + int value = 0; + for (int subset = 0; subset < subsets; subset++) value += weight[subset]; + if (value != z_limit) return 4; + even[value]++; + + uint32_t limit = 1u << edge_count; + for (uint32_t step = 1; step < limit; step++) { + int flipped = __builtin_ctz(step); + int base = flipped * subsets; + int count = member_count[flipped]; + for (int index = 0; index < count; index++) { + int subset = members[base + index]; + uint8_t before = failed[subset]; + uint8_t after = (uint8_t)(before ^ bit_of[base + index]); + failed[subset] = after; + if (before == 0) value -= weight[subset]; + else if (after == 0) value += weight[subset]; + } + if ((unsigned)value > (unsigned)z_limit) return 5; + if (step & 1u) odd[value]++; + else even[value]++; + } + + int64_t total = 0; + int64_t signed_total = 0; + for (int point = 0; point <= z_limit; point++) { + total += even[point] + odd[point]; + int64_t coefficient = even[point] - odd[point]; + signed_total += coefficient; + if (coefficient) + printf("%d %lld\n", point, (long long)coefficient); + } + if (total != (1LL << edge_count) || signed_total != 0) return 6; + return 0; +} diff --git a/research/six-event-guard-correlation/verify.py b/research/six-event-guard-correlation/verify.py new file mode 100644 index 0000000000..888e0e8fdc --- /dev/null +++ b/research/six-event-guard-correlation/verify.py @@ -0,0 +1,284 @@ +"""Exact six-event full-guard product inequality over GL_m(F_2).""" + +import json +import subprocess +import tempfile +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +SOURCE = PACKAGE / "spectrum.c" +K3 = {27: 1, 21: -6, 19: 6, 17: -6, 15: 16, 13: -18, 11: 9, 9: -2} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def subset_character(rows): + width = len(rows) + full = (1 << width) - 1 + total = 0 + for left in range(1 << width): + folded = 0 + for index, row in enumerate(rows): + if left >> index & 1: + folded ^= row + if folded & (full ^ left) == 0: + total += 1 << (width - left.bit_count()) + return total + + +def literal_character(rows): + width = len(rows) + total = 0 + state_count = 3 ** width + for code in range(state_count): + states = [] + parity = 0 + for index in range(width): + state = code % 3 + code //= 3 + states.append(state) + right = 0 + for index, state in enumerate(states): + if state == 2: + right |= 1 << index + for index, state in enumerate(states): + if state == 1: + parity += (rows[index] & right).bit_count() + total += 1 if parity % 2 == 0 else -1 + return total + + +def rows_of(width, mask): + rows = [0] * width + bit = 0 + for tail in range(width): + for head in range(width): + if tail == head: + continue + if mask >> bit & 1: + rows[tail] |= 1 << head + bit += 1 + return rows + + +def signed_spectrum(width): + spectrum = {} + edge_count = width * (width - 1) + for mask in range(1 << edge_count): + value = subset_character(rows_of(width, mask)) + sign = -1 if mask.bit_count() % 2 else 1 + spectrum[value] = spectrum.get(value, 0) + sign + return {value: coeff for value, coeff in spectrum.items() if coeff} + + +def compile_spectrum(directory): + binary = Path(directory) / "spectrum" + compiled = subprocess.run( + ["gcc", "-O3", "-std=c11", "-o", str(binary), str(SOURCE)], + check=False, capture_output=True, text=True) + need(compiled.returncode == 0, "gcc failed: " + compiled.stderr[-500:]) + return binary + + +def run_spectrum(binary, width): + ran = subprocess.run( + [str(binary), str(width)], + check=False, capture_output=True, text=True) + need(ran.returncode == 0, "spectrum failed: " + ran.stderr[-500:]) + spectrum = {} + for line in ran.stdout.splitlines(): + value, coeff = line.split() + spectrum[int(value)] = int(coeff) + return spectrum + + +def gl_product(dimension): + order = 1 << (dimension + 1) + numerator = (order - 1) ** 5 + denominator = 1 + for shift in range(1, 6): + denominator *= order - (1 << shift) + return numerator, denominator + + +def difference_polynomial(order): + """(X-1)^5 - product_{j=1..5}(X-2^j), expanded once from its coefficients.""" + return (57 * order ** 4 - 1230 * order ** 3 + 9910 * order ** 2 + - 31739 * order + 32767) + + +def exact_numerator(spectrum, power): + return sum(coeff * pow(value, power) for value, coeff in spectrum.items()) + + +def edge_index(width): + index = {} + bit = 0 + for tail in range(width): + for head in range(width): + if tail == head: + continue + index[(tail, head)] = bit + bit += 1 + return index + + +def combinations(width, count): + chosen = [] + + def walk(start, rest): + if rest == 0: + yield tuple(chosen) + return + for vertex in range(start, width): + chosen.append(vertex) + yield from walk(vertex + 1, rest - 1) + chosen.pop() + + yield from walk(0, count) + + +def identify_leading(width): + """Evaluate every single arc and every two-arrow star at this width.""" + index = edge_index(width) + arc_value = 7 * 3 ** (width - 2) + star_value = 19 * 3 ** (width - 3) + for edge, bit in index.items(): + mask = 1 << bit + rows = rows_of(width, mask) + need(literal_character(rows) == subset_character(rows) == arc_value, + "single-arc character moved") + need(mask.bit_count() % 2 == 1, "single arc is not odd weight") + stars = set() + for triple in combinations(width, 3): + first, second, third = triple + patterns = ( + ((first, second), (first, third)), + ((second, first), (third, first)), + ((second, first), (second, third)), + ((first, second), (third, second)), + ((third, first), (third, second)), + ((first, third), (second, third)), + ) + for pattern in patterns: + mask = 0 + for edge in pattern: + mask |= 1 << index[edge] + rows = rows_of(width, mask) + need(literal_character(rows) == subset_character(rows) == star_value, + "two-arrow star character moved") + need(mask.bit_count() == 2, "two-arrow star does not have weight 2") + stars.add(mask) + need(len(index) == width * (width - 1), "arc count") + need(len(stars) == width * (width - 1) * (width - 2), "star count") + + +def controls(binary): + for width in (3, 4): + edge_count = width * (width - 1) + for mask in range(1 << edge_count): + rows = rows_of(width, mask) + need(literal_character(rows) == subset_character(rows), + "three-state sum disagrees with the subset form") + python_three = signed_spectrum(3) + need(python_three == K3, "k=3 subset spectrum is not the published law") + c_three = run_spectrum(binary, 3) + c_four = run_spectrum(binary, 4) + c_five = run_spectrum(binary, 5) + need(c_three == K3, "C spectrum missed the k=3 law") + need(signed_spectrum(4) == c_four, "C spectrum missed the k=4 recount") + need(c_five[243] == 1 and c_five[189] == -20 and c_five[171] == 60, + "k=5 leading coefficients moved") + need(c_four[81] == 1 and c_four[63] == -12, "k=4 empty or single-edge multiplicity moved") + identify_leading(6) + return c_five + + +def tail_bound(absolute_rest): + """Integer tail for every n >= 129. + + At the threshold the remainder exceeds 26 single-arc modes and fits under + 27, leaving 3 modes to absorb the degree-four GL gap. + """ + threshold = 129 + cover = 27 + deficit = 3 + need(cover + deficit == 30, "arc modes were not split") + remainder = (120 * pow(513, threshold) + + absolute_rest * pow(495, threshold)) + base_gap = cover * pow(567, threshold) - remainder + need(base_gap > 0, "remainder did not fall below 27 single-edge modes") + need((cover - 1) * pow(567, threshold) < remainder, + "26 modes already covered the remainder; the split moved") + step_gap = (cover * pow(567, threshold + 1) - 120 * pow(513, threshold + 1) + - absolute_rest * pow(495, threshold + 1)) + need(step_gap > 567 * base_gap, "tail recurrence failed one step") + order = 1 << (threshold + 1) + positive = deficit * pow(567, threshold) * pow(order - 1, 5) + negative = 59 * pow(order, 4) * pow(729, threshold) + need(positive > negative, "finite-GL factor was not absorbed at n=129") + need(pow(729, threshold) > deficit * pow(567, threshold), + "3-mode upper bound is negative") + need(9910 * 128 ** 2 <= 128 ** 4 and 32767 <= 128 ** 4, + "degree-four majorization failed at X=128") + sample = difference_polynomial(order) + expanded = ((1 << (threshold + 1)) - 1) ** 5 + product = 1 + for shift in range(1, 6): + product *= order - (1 << shift) + need(expanded - product == sample, "GL polynomial identity failed") + need(sample <= 59 * order ** 4, "GL difference exceeded 59 X^4") + + +def illustrated_ratio(spectrum, power): + numerator, denominator = gl_product(power) + return exact_numerator(spectrum, power) * numerator / (pow(729, power) * denominator) + + +def main(): + with tempfile.TemporaryDirectory() as directory: + binary = compile_spectrum(directory) + controls(binary) + spectrum = run_spectrum(binary, 6) + need(spectrum[729] == 1, "empty character multiplicity") + need(spectrum[567] == -30, "single-edge multiplicity") + need(spectrum[513] == 120, "two-star multiplicity") + need(max(spectrum) == 729, "character above the empty matrix") + allowed = {729, 567, 513} + unexpected = [value for value in spectrum if value > 495 and value not in allowed] + need(not unexpected, "character between the separated levels: " + str(unexpected[:6])) + below = [value for value in spectrum if value < 513] + need(below and max(below) == 495, "unexpected character above 495 and below 513") + absolute_rest = sum(abs(spectrum[value]) for value in below) + need(sum(abs(coeff) for coeff in spectrum.values()) == 1 << 30, + "signed spectrum is not a partition of the 2^30 masks") + for power in range(0, 6): + need(exact_numerator(spectrum, power) == 0, "walk count before the threshold") + count = exact_numerator(spectrum, 6) >> 30 + need(count == 23040, "m=7 header count changed") + for power in range(6, 130): + numerator, denominator = gl_product(power) + slack = denominator * pow(729, power) - exact_numerator(spectrum, power) * numerator + need(slack > 0, "ratio reached 1 at n=" + str(power)) + shifted = dict(spectrum) + shifted[567] = spectrum[567] + 1 + need(exact_numerator(shifted, 5) != 0, "n=5 vanishing ignored a multiplicity change") + tail_bound(absolute_rest) + samples = {str(power): illustrated_ratio(spectrum, power) for power in (6, 7, 12, 20, 40)} + print(json.dumps({ + "status": "PASS_SIX_EVENT_GUARD_CORRELATION", + "terms": len(spectrum), + "m7_headers": count, + "remainder_mass": absolute_rest, + "exact_through_n": 129, + "analytic_from_n": 129, + "sample_ratios": samples, + }, sort_keys=True)) + + +if __name__ == "__main__": + main() From f6cf478e2550e747074a746a4038a74b321ceb6f Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 2 Nov 2026 13:51:54 +0000 Subject: [PATCH 2/2] Name the tail range by matrix size The induction gives rho_m < 1 for every m >= 130. Section 3 already checks that threshold exactly. Co-authored-by: unpaidmoon --- research/six-event-guard-correlation/PROOF.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/research/six-event-guard-correlation/PROOF.md b/research/six-event-guard-correlation/PROOF.md index 6f1d124f58..fcc1b10217 100644 --- a/research/six-event-guard-correlation/PROOF.md +++ b/research/six-event-guard-correlation/PROOF.md @@ -158,8 +158,8 @@ strict at every larger n. Also 729/567 = 9/7 > 1, and the verifier finds comparison upper bound stays nonnegative. The degree-four majorization was checked at X = 128, the smallest integer in its hypothesis, and both 9910 ≤ X^2 and 32767 ≤ X^4 become looser as X grows. Hence ρ_m < 1 for -every n ≥ 129. Section 3 already includes that threshold, and sections 2 -through 4 together cover every m ≥ 6. +every m ≥ 130. Section 3 already includes m = 130, and sections 2 through +4 together cover every m ≥ 6. ## Scope