Prove the five-request binary full-guard product inequality for every m>=5 (k=5 of #4275 OQ2; no new κ)

research/five-event-guard-correlation/PROOF.md

@@ -0,0 +1,137 @@
+# Five binary full-guard events lie below the product of their marginals
+
+Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. This is successor work to petalas's
+#4275, which supplies the character law, and #4599, which settles k = 4. It follows the same method.
+
+## Statement
+
+**Setting.**
+
+- U_1, …, U_5 are pairwise orthogonal rank-one idempotents on F_2^m, with m ≥ 5.
+- P_t = I − U_t, and G is uniform on GL_m(F_2).
+- E_t is the event that every leading principal minor of G P_t G⁻¹, of orders 1 to m−1, is nonzero.
+- n = m − 1, X = 2^m, s_m = 3ⁿ/((X−1)2ⁿ), and ρ_m = Pr(E_1 ∩ … ∩ E_5)/s_m⁵.
+
+**Theorem.** For every m ≥ 5,
+
+```text
+Pr(E_1 ∩ … ∩ E_5) < s_m^5,     1 − ρ_m = 20 (7/9)^n + O((19/21)^n (7/9)^n).
+```
+
+This answers k = 5 of Open next question 2 in #4275. The claim is a scoped counting proof with an exact finite
+component. No negative association is asserted for other functions, other event families or k ≥ 6.
+
+## 1. Reduction to a walk
+
+A basis change takes U_t to e_t e_tᵀ. This only permutes headers, so it does not change any probability.
+
+**The guard as a sum.** Let g_t be column t of G and h_t row t of G⁻¹. Then G P_t G⁻¹ = I − g_t h_tᵀ, and by the
+matrix determinant lemma its order-j leading minor is
+
+```text
+1 − Σ_{i≤j} h_t[i] g_t[i].
+```
+
+**Headers as pairs.** Let x_i be the first five coordinates of row i of G, and y_i the first five coordinates of
+column i of G⁻¹. Write A_j = Σ_{i≤j} y_i x_iᵀ for the prefix sums. Then every guard passes exactly when A_1, …, A_n
+all have zero diagonal. Two facts follow:
+
+- each increment y_i x_iᵀ with i ≤ n has disjoint factor supports;
+- A_m = YX = I_5, so the last increment is I_5 − A_n. This has unit diagonal and rank at most one, so it is J and
+  its pair is forced to be all ones. Hence A_n = E := J − I_5.
+
+**Counting headers.** Each pair (X, Y) with YX = I_5 extends to exactly |GL_{m−5}| headers, because the remaining
+columns of G form an ordered basis of ker Y. Let D_n(E) be the number of ordered sequences of n factor pairs with
+disjoint supports whose rank-one increments sum to E. Then
+
+```text
+Pr(E_1 ∩ … ∩ E_5) = D_n(E) |GL_{m−5}| / |GL_m| = D_n(E) / (2^{5n−20} (X−1)(X−2)(X−4)(X−8)(X−16)).
+```
+
+**The ratio.** Put N_n = 2^20 D_n(E). Then
+
+```text
+ρ_m = (N_n / 243^n) · H(X),     H(X) = (X−1)^4 / ((X−2)(X−4)(X−8)(X−16)) > 1.        (1)
+```
+
+## 2. The signed spectrum
+
+The increments live in the group of zero-diagonal 5×5 binary matrices, F_2^20. Let w be the weight of each element,
+meaning the number of disjoint-support pairs that produce it. Its total is 3⁵ = 243, of which the zero matrix has
+weight 63; there are 181 distinct increments. Let ŵ be the Walsh–Hadamard transform. Then
+
+```text
+N_n = Σ_c (−1)^{|c|} ŵ(c)^n,
+```
+
+because the character c evaluated at E is (−1)^{|c|}. The verifier computes ŵ exactly on all 2^20 characters and
+collects N_n = Σ_z b_z zⁿ. The result has 62 bases, all of them positive. The leading terms are
+
+```text
+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.     (2)
+```
+
+This agrees with #4275's description of the second eigenvalue: 7·3^{k−2} = 189, with sign −1 and multiplicity
+k(k−1) = 20.
+
+**Cross-checks of the table.** These do not use characters.
+
+- **Direct counts.** Meet-in-the-middle convolution gives D_n(E) for n = 4, 5 and 6, and 2^20 D_n(E) equals
+  Σ_z b_z zⁿ in each case. In particular D_4(E) = 0.
+- **m = 6.** The formula gives exactly 2,880 complete headers. This matches #4598 and my independent recount in #4605.
+- **Marginal law.** At k = 1 the same reduction reproduces the marginal s_m.
+- **Brute force.** The reduction matches a brute force from the leading-minor definition over GL_3 and GL_4, for
+  k = 1, 3 and 4.
+- **Failure control.** Changing one multiplicity by one unit is detected.
+
+## 3. Large dimensions (n ≥ 117)
+
+Put x = (7/9)ⁿ. The bases below 189 satisfy |R_n| ≤ 1,048,555·171ⁿ. Since 1,048,555·171^117 ≤ 9·189^117 and
+171/189 < 1, every n ≥ 117 gives
+
+```text
+N_n / 243^n ≤ 1 − 20x + 9x = 1 − 11x.                                   (3)
+```
+
+**Bounding H.** The numerator minus the denominator of H is 26X³ − 274X² + 956X − 1023. This is at most 26X³ for
+X ≥ 4. For X ≥ 32 the denominator is at least (15/16)(7/8)(3/4)(1/2)X⁴ = (315/1024)X⁴. Since 26·1024 < 85·315,
+
+```text
+H(X) − 1 < 85/X = 42.5/2^n ≤ x     (85·9^117 ≤ 2·14^117, then monotone).   (4)
+```
+
+**Conclusion.** Also 11·7^117 < 9^117, so 1 − 11x > 0. N_n ≥ 0 because it counts sequences, so (1), (3) and (4)
+give
+
+```text
+ρ_m ≤ (1 − 11x)(1 + x) = 1 − 10x − 11x² < 1     for every m ≥ 118.
+```
+
+## 4. Remaining dimensions (5 ≤ m ≤ 118)
+
+The verifier checks the strict rational inequality Pr(E_1 ∩ … ∩ E_5) < s_m⁵ exactly at each of these 114
+dimensions.
+
+- **m = 5:** the joint probability is 0.
+- **m = 6:** it is 2,880/|GL_6|, and ρ_6 ≈ 0.0056.
+- **m = 7:** it is 39/225,763,328.
+
+## 5. Leading deficit
+
+By (2), N_n/243ⁿ = 1 − 20x + O((171/243)ⁿ), and 171/243 = (19/21)(7/9). By (4), H = 1 + O(2⁻ⁿ), and 1/2 < 171/243.
+Multiplying the two gives the asserted deficit. The computed ratio (1−ρ_m)/x is 18.97 at m = 40, 19.98 at m = 80 and
+19.9995 at m = 118.
+
+## Scope
+
+**Covered.** Exactly five fixed, pairwise orthogonal rank-one requests over F_2, with complete headers weighted
+equally.
+
+**Not settled.** k ≥ 6, odd characteristic, restricted header families and nonorthogonal kernels.
+
+**Not claimed.**
+
+- A physical saving: producer, header selection, emission, dispatch, dirty restoration, stock and precision are
+  all unpriced.
+- A supplier or a new κ.
+- Formal proof-kernel review.

research/five-event-guard-correlation/README.md

@@ -0,0 +1,52 @@
+# Five binary full-guard events are strictly below independent marginals
+
+**Task:** independent-moment (original successor result). **Base:** canonical main `f626db5c`. **No κ is claimed.**
+
+**Claim type:** scoped counting proof with an exact finite component. [PROOF.md](PROOF.md) has the argument.
+
+For five pairwise orthogonal rank-one requests on F₂ᵐ and a uniform header in GL_m(F₂), let E_t be the event that every leading-minor guard of G P_t G⁻¹ through order m−1 passes. Then, for every m ≥ 5,
+
+```text
+Pr(E_1 ∩ … ∩ E_5) < s_m^5,   s_m = 3^(m−1)/((2^m−1) 2^(m−1)),
+1 − ρ_m = 20 (7/9)^(m−1) + O((19/21)^(m−1) (7/9)^(m−1)).
+```
+
+This answers k = 5 of Open next question 2 in #4275. #4599 settles k = 4.
+
+## Evidence
+
+- **Exact signed spectrum.** It is computed over all 2²⁰ characters of the zero-diagonal 5×5 binary matrices. There are 62 bases, all positive, led by 243ⁿ − 20·189ⁿ + 60·171ⁿ.
+- **Independent cross-checks of the table.**
+  - direct meet-in-the-middle counts at n = 4, 5, 6;
+  - the 2,880 complete headers at m = 6, matching #4598 and #4605;
+  - the marginal law at k = 1;
+  - the pair reduction against a brute force over GL₃ and GL₄ (k = 1, 3, 4);
+  - a positive control of k = 4 below the product (#4599);
+  - a one-unit table mutation is detected.
+- **Two ranges.** For 5 ≤ m ≤ 118 there are exact rational comparisons. For m ≥ 118 a uniform tail bound from exact integer inequalities applies, with no unchecked interval.
+- **Values.**
+
+  | m | 6 | 8 | 20 | 40 | 118 |
+  |---|---|---|---|---|---|
+  | ρ_m | 0.0056 | 0.078 | 0.881 | 0.99895 | 1 − 3×10⁻¹² |
+
+  The deficit ratio (1−ρ)/(7/9)ⁿ reaches 19.9995 at m = 118.
+
+## Verify
+
+```text
+python3 -B research/five-event-guard-correlation/verify.py
+```
+
+It takes about 5 s and uses the standard library only.
+
+## Limitations
+
+- **Scope.** Only k = 5 is covered, with orthogonal kernels, F₂ and complete equally weighted headers. No all-k statement is made.
+- **Not claimed.** A producer, selection, emission, dispatch, dirty restoration, stock, precision, a supplier or a κ change. Independent human or proof-kernel review has not been done.
+
+## Open next questions
+
+- **All k ≥ 4.** Bound the remaining negative spectrum uniformly in k. The second base 7·3^{k−2} carries sign −1 and multiplicity k(k−1). The third base is 19·3^{k−3} with sign +, which is 57 at k = 4 and 171 at k = 5. First step: tabulate the spectrum at k = 6, which has 2³⁰ characters and needs a vectorised or symmetry-reduced transform.
+
+Credit: petalas (Nick Petalas) for #4275's character law and threshold framing, #4599's k = 4 method and #4598's m = 6 count. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.

research/five-event-guard-correlation/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/corankone-triple-header-law/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8",
+      "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f"
+    },
+    {
+      "path": "research/corankone-triple-header-law/README.md",
+      "usage": "provenance",
+      "git_blob": "830650a2a4f954d0170e138c17eed5967d21a824",
+      "sha256": "b7a6cf666e30a4ef135aa7190fe545dd7203cd1ffcc175138bd3dda7484155f2"
+    }
+  ]
+}

research/five-event-guard-correlation/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "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_status": "unchanged",
+  "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+  "scope_change_reason": null,
+  "bottleneck_link": "Settles k = 5 of #4275 OQ2 (binary multi-request header guard correlation), extending #4599's k = 4.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the k = 5 theorem and leading deficit.",
+  "outcome": "completed",
+  "evidence": "Exact 2^20-character signed spectrum (62 bases; 243^n - 20*189^n + 60*171^n ...), cross-checked by direct counts n=4,5,6, the 2,880 headers at m=6, marginal law, brute force GL_3/GL_4, k=4 control and table mutation; exact comparisons 5<=m<=118; uniform bound for m>=118; deficit ratio 19.9995 at m=118.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Product inequality for all k >= 4.",
+      "why_it_matters": "Completes #4275 OQ2.",
+      "first_step": "Tabulate the k = 6 spectrum (2^30 characters) with a vectorised or symmetry-reduced transform.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/five-event-guard-correlation/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "docs/research/agent-task-catalog.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact signed spectrum over 2^20 characters; cross-checks (direct counts n=4..6, m=6 headers 2880, marginal law, brute force GL_3/GL_4, k=4 control, mutation); exact inequality 5<=m<=118; uniform-range integer inequalities; deficit."
+    }
+  ]
+}