Cursor/six event guard correlation 891a

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 m ≥ 130. Section 3 already includes m = 130, 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.

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.

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

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