From 3bd2fdd9632841bf8d25b0baa09b81a7b8d1e8f8 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 16:35:14 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20check=20#4599's=20four-event=20?= =?UTF-8?q?product=20inequality=20by=20direct=20header=20count=20for=20eve?= =?UTF-8?q?ry=204<=3Dm<=3D85;=20its=20spectrum=20table=20matches=20at=20al?= =?UTF-8?q?l=2082=20dimensions=20(no=20new=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- research/pr4599-four-event-check/README.md | 49 ++++++ research/pr4599-four-event-check/SOURCES.json | 18 ++ research/pr4599-four-event-check/TASK.json | 100 +++++++++++ research/pr4599-four-event-check/VERIFY.json | 18 ++ research/pr4599-four-event-check/verify.py | 165 ++++++++++++++++++ 5 files changed, 350 insertions(+) create mode 100644 research/pr4599-four-event-check/README.md create mode 100644 research/pr4599-four-event-check/SOURCES.json create mode 100644 research/pr4599-four-event-check/TASK.json create mode 100644 research/pr4599-four-event-check/VERIFY.json create mode 100644 research/pr4599-four-event-check/verify.py diff --git a/research/pr4599-four-event-check/README.md b/research/pr4599-four-event-check/README.md new file mode 100644 index 0000000000..eb2c8f563e --- /dev/null +++ b/research/pr4599-four-event-check/README.md @@ -0,0 +1,49 @@ +# Independent check of #4599: four binary full-guard events lie below the product of their marginals + +**Task:** independent-moment (independent check). **Base:** canonical main `f626db5c`. **No κ is claimed.** + +## The claim + +petalas's #4599 (head `19ca650c`) concerns four pairwise orthogonal rank-one requests on F₂ᵐ and a uniform header in GL_m(F₂). It claims Pr(E₁∩E₂∩E₃∩E₄) < s_m⁴ for every m ≥ 4, where s_m = 3ⁿ/((2ᵐ−1)2ⁿ) and n = m−1. The proof has two parts: + +- **m ≥ 85:** a spectral tail bound built from a signed character spectrum, printed in its §2; +- **4 ≤ m ≤ 84:** exact comparisons. + +## Independent route + +This route uses no #4275 character law and no #4227 marginal formula. Nothing is imported from #4599. + +1. **Minor formula.** G P_t G⁻¹ = I − g_t h_tᵀ, so the order-j minor is 1 − Σ_{i≤j} h_t[i] g_t[i]. +2. **Headers as pairs.** For k requests, passing headers are counted through X, the first k columns of G, and Y, the first k rows of G⁻¹. The count runs over pairs with YX = I_k whose first m−1 prefix sums have a zero diagonal. Each such pair extends to exactly |GL_{m−k}| headers, because the remaining columns are an ordered basis of ker Y. +3. **Exact count.** A dynamic programme over zero-diagonal k×k matrices computes these counts exactly. Each step is weighted by the number of factor pairs with disjoint supports. All arithmetic uses Python integers and fractions. + +## Results (every m from 4 to 85) + +- **Marginal law.** Pr(E₁) = s_m exactly, which independently confirms the marginal law. +- **Product inequality.** Pr(E₁∩…∩E₄) < Pr(E₁)⁴ strictly at every m. At m = 4 the joint probability is 0. At m = 5 it is 1/208,320, against a marginal of 81/496. +- **Spectrum table.** The direct joint count equals #4599's formula (N_n/81ⁿ)·H(X)·s_m⁴, built from its printed signed spectrum, at all 82 dimensions. **Failure control:** changing one multiplicity by one unit is detected. +- **§3 constants.** These are re-checked from the table: + - the tail sum is 4,083 with largest base 57; + - 4083·57⁸⁴ < 63⁸⁴, 9·9⁸⁴ < 14⁸⁴, 11·7⁸⁴ < 9⁸⁴ and 11·512 < 18·315; + - H's numerator minus denominator is 11X² − 53X + 63. +- **Leading deficit.** (1−ρ_m)/(7/9)ⁿ is 9.33 at m = 20, 11.56 at m = 40 and 11.9947 at m = 85. This is consistent with the claimed limit of 12. +- **Brute-force anchor.** A brute force from the leading-minor definition over all of GL₃ and GL₄, for k = 1, 3 and 4, matches the dynamic programme. + +## Verify + +```text +python3 -B research/pr4599-four-event-check/verify.py +``` + +The check takes about 7 s and uses the standard library only. + +## Limitations + +- **Analytic range.** The m ≥ 86 range still rests on #4599's §3 argument applied to its spectrum. This package checks the spectrum's agreement with an independent direct count at 82 consecutive dimensions, and checks the §3 integer constants. It does not prove that the spectrum is the exact transfer spectrum. +- **Scope.** Only the stated setting is covered: four requests, orthogonal kernels, F₂, and complete equally weighted headers. + +## Open next questions + +- **The five-request inequality,** which is k = 5 of #4275's Open question 2. First step: run the same prefix dynamic programme with k = 5 over 2²⁰ zero-diagonal states. A vectorised or modular transform is likely needed for speed. + +Credit: petalas (Nick Petalas) for #4599, #4275 and #4227. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4599-four-event-check/SOURCES.json b/research/pr4599-four-event-check/SOURCES.json new file mode 100644 index 0000000000..a2a5ea8bbd --- /dev/null +++ b/research/pr4599-four-event-check/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/pr4599-four-event-check/TASK.json b/research/pr4599-four-event-check/TASK.json new file mode 100644 index 0000000000..217d797ca7 --- /dev/null +++ b/research/pr4599-four-event-check/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": "Independent coverage of a new counting theorem (#4599) on binary header guard correlation.", + "budget_minutes": 60, + "stop_rule": "Stop at m = 85, the first dimension of the analytic range.", + "outcome": "completed", + "evidence": "Direct exact header count (YX=I pairs, zero-diagonal prefix DP, |GL_{m-k}| extension) for 4<=m<=85: marginal equals s_m, joint < marginal^4 at every m, joint equals #4599's spectrum formula at every m (one-unit table mutation detected); section-3 integer constants re-checked; brute force over GL_3/GL_4 agrees; (1-rho)/(7/9)^n = 11.9947 at m=85.", + "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": "Five-request product inequality.", + "why_it_matters": "#4275 Open question 2 at k=5.", + "first_step": "Run the same prefix DP with k=5 over 2^20 zero-diagonal states.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4599-four-event-check/VERIFY.json b/research/pr4599-four-event-check/VERIFY.json new file mode 100644 index 0000000000..b5d260589f --- /dev/null +++ b/research/pr4599-four-event-check/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Direct exact count for 4<=m<=85: marginal law, strict product inequality, agreement with #4599 spectrum at every m, table-mutation control, section-3 constants, brute force GL_3/GL_4." + } + ] +} diff --git a/research/pr4599-four-event-check/verify.py b/research/pr4599-four-event-check/verify.py new file mode 100644 index 0000000000..73fe6cc07c --- /dev/null +++ b/research/pr4599-four-event-check/verify.py @@ -0,0 +1,165 @@ +#!/usr/bin/env python3 +"""Independent check of PR #4599 (petalas): four binary full-guard events lie below the product of their marginals. + +Setting (#4599): U_1..U_4 pairwise orthogonal rank-one idempotents on F_2^m (normalized U_t = e_t e_t^T), P_t = I - U_t, +G uniform on GL_m(F_2); E_t: every leading principal minor of G P_t G^-1 of orders 1..m-1 is nonzero. #4599 claims +Pr(E_1..E_4) < s_m^4 with s_m = 3^n/((2^m - 1) 2^n), n = m - 1, for all m >= 4, via a spectral bound for m >= 85 +and exact comparisons for 4 <= m <= 84. + +Independent route (no #4275 character law, no #4227 marginal formula, nothing imported from #4599): + * the order-j minor of G P_t G^-1 = I - g_t h_t^T is 1 - sum_{i<=j} h_t[i] g_t[i] (g_t column t of G, h_t row t + of G^-1); + * for k requests, passing headers are counted through the first k columns X and first k rows Y of G^-1: pairs with + Y X = sum_i y_i x_i^T = I_k whose first m-1 prefix sums have zero diagonal; each such pair extends to exactly + |GL_{m-k}| headers (the remaining columns are an ordered basis of ker Y); + * the ordered sequences are counted exactly by a dynamic programme over zero-diagonal k x k matrices, each step + weighted by the number of factor pairs (y, x) with disjoint supports. +This gives Pr(E_1) and Pr(E_1..E_4) for every 4 <= m <= 85 as exact fractions. The verifier then + * checks Pr(E_1) = s_m (independently confirming the marginal law) and Pr(E_1..E_4) < Pr(E_1)^4 for every m; + * compares the direct joint count with the signed spectrum printed in #4599 PROOF.md (transcribed) at every m; + * re-checks the integer constants of section 3 of #4599 (m >= 85) from that table; + * anchors the reformulation by brute force from the leading-minor definition over GL_3 and GL_4. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction +from itertools import product +import json +import sys + +M_MAX = 85 +# #4599 PROOF.md section 2: z -> signed multiplicity b_z of N_n = sum_z b_z z^n (transcribed, cited). +SPECTRUM = {81: 1, 63: -12, 57: 24, 55: -8, 51: -24, 49: 18, 47: -48, 45: 118, 43: -68, 41: 85, 39: -180, + 37: 228, 35: -336, 33: 399, 31: -444, 29: 502, 27: -548, 25: 523, 23: -332, 21: 144, 19: -48, 17: 6} + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def gl_order(n): + out = 1 + for i in range(n): + out *= 2 ** n - 2 ** i + return out + + +def outer(y, x, k): + return sum(1 << (k * a + b) for a in range(k) if y >> a & 1 for b in range(k) if x >> b & 1) + + +def pass_probabilities(k, m_max): + """{m: Pr(all k events)} for k <= m <= m_max, by the zero-diagonal prefix DP.""" + zero_diag, anything = Counter(), Counter() + for y, x in product(range(1 << k), repeat=2): + r = outer(y, x, k) + anything[r] += 1 + if y & x == 0: + zero_diag[r] += 1 + ident = sum(1 << (k * a + a) for a in range(k)) + state, out = Counter({0: 1}), {} + for m in range(1, m_max + 1): + if m >= k: + pairs = sum(w * anything.get(s ^ ident, 0) for s, w in state.items()) + out[m] = Fraction(pairs * gl_order(m - k), gl_order(m)) + nxt = Counter() + for s, ws in state.items(): + for r, wr in zero_diag.items(): + nxt[s ^ r] += ws * wr + state = nxt + return out + + +def mat_mul(a, b, n): + return [[sum(a[i][l] & b[l][j] for l in range(n)) & 1 for j in range(n)] for i in range(n)] + + +def inverse(a, n): + m = [row[:] + [int(i == j) for j in range(n)] for i, row in enumerate(a)] + for c in range(n): + p = next((r for r in range(c, n) if m[r][c]), None) + if p is None: + return None + m[c], m[p] = m[p], m[c] + for r in range(n): + if r != c and m[r][c]: + m[r] = [u ^ v for u, v in zip(m[r], m[c])] + return [row[n:] for row in m] + + +def guards_pass(a, n): + """Leading principal minors of orders 1..n-1 nonzero, by elimination without pivoting.""" + m = [row[:] for row in a] + for c in range(n - 1): + if not m[c][c]: + return False + for r in range(c + 1, n): + if m[r][c]: + m[r] = [u ^ v for u, v in zip(m[r], m[c])] + return True + + +def brute_force(n, k): + """Exact (Pr(E_1), Pr(E_1..E_k)) over GL_n from the leading-minor definition.""" + reqs = [[[int(i == j) ^ (i == t and j == t) for j in range(n)] for i in range(n)] for t in range(k)] + one = joint = total = 0 + for bits in range(1 << (n * n)): + g = [[bits >> (n * i + j) & 1 for j in range(n)] for i in range(n)] + gi = inverse(g, n) + if gi is None: + continue + total += 1 + ok = [guards_pass(mat_mul(mat_mul(g, p, n), gi, n), n) for p in reqs] + one += ok[0] + joint += all(ok) + return Fraction(one, total), Fraction(joint, total) + + +def spectral_joint(m, spectrum): + n, x = m - 1, 2 ** m + s = Fraction(3 ** n, (x - 1) * 2 ** n) + big_n = sum(b * z ** n for z, b in spectrum.items()) + h = Fraction((x - 1) ** 3, (x - 2) * (x - 4) * (x - 8)) + return Fraction(big_n, 81 ** n) * h * s ** 4 + + +def main(): + marg, joint = pass_probabilities(1, M_MAX), pass_probabilities(4, M_MAX) + rows = [] + for m in range(4, M_MAX + 1): + n = m - 1 + need(marg[m] == Fraction(3 ** n, (2 ** m - 1) * 2 ** n), "marginal law s_m at m=%d" % m) + need(joint[m] < marg[m] ** 4, "product inequality at m=%d" % m) + need(joint[m] == spectral_joint(m, SPECTRUM), "#4599 spectrum table vs direct count at m=%d" % m) + rows.append((m, joint[m] / marg[m] ** 4)) + need(joint[4] == 0 and joint[5] == Fraction(1, 208320) and marg[5] == Fraction(81, 496), "m = 4, 5 values") + deficit = {m: (1 - rho) / Fraction(7, 9) ** (m - 1) for m, rho in rows} + # 12 - deficit is dominated by the next base: |12 - d_m| <= 4083 (57/63)^n + O(2^-n) correction + need(all(abs(deficit[m] - 12) < 4100 * Fraction(57, 63) ** (m - 1) + 20 * Fraction(9, 14) ** (m - 1) + for m in range(40, M_MAX + 1)), "(1 - rho_m)/(7/9)^n approaches 12") + tail = sum(abs(b) for z, b in SPECTRUM.items() if z < 63) + need(tail == 4083 and max(z for z in SPECTRUM if z < 63) == 57, "|R_n| <= 4083 * 57^n") + need(4083 * 57 ** 84 < 63 ** 84 and 9 * 9 ** 84 < 14 ** 84 and 11 * 7 ** 84 < 9 ** 84 and 11 * 512 < 18 * 315, + "section 3 integer inequalities") + need(all((x - 1) ** 3 - (x - 2) * (x - 4) * (x - 8) == 11 * x * x - 53 * x + 63 for x in range(1, 200)), + "H numerator minus denominator") + for n_, k_ in ((3, 1), (3, 3), (4, 1), (4, 4)): + p1, pk = brute_force(n_, k_) + need(p1 == pass_probabilities(1, n_)[n_] and pk == pass_probabilities(k_, n_)[n_], + "brute force GL_%d, k=%d" % (n_, k_)) + mutated = dict(SPECTRUM) + mutated[17] += 1 + need(any(joint[m] != spectral_joint(m, mutated) for m in range(4, M_MAX + 1)), + "failure control: a one-unit table change is detected") + print(json.dumps({"status": "PASS_PR4599_INDEPENDENT_CHECK", + "dimensions_checked": [4, M_MAX], "marginal_equals_s_m": True, + "joint_below_product_all_m": True, "spectrum_table_matches_direct_count_all_m": True, + "m5": {"joint": str(joint[5]), "marginal": str(marg[5])}, + "rho": {str(m): "%.12f" % float(r) for m, r in rows if m in (5, 6, 8, 12, 20, 40, 85)}, + "deficit_ratio": {str(m): "%.6f" % float(deficit[m]) for m in (20, 40, 85)}, + "section3_constants": True, "brute_force_GL3_GL4": True, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())