diff --git a/research/pr4598-header-recount/README.md b/research/pr4598-header-recount/README.md new file mode 100644 index 0000000000..4920889db1 --- /dev/null +++ b/research/pr4598-header-recount/README.md @@ -0,0 +1,53 @@ +# Independent recount of #4598's five-request threshold headers + +**Task:** independent-moment (independent recount). **Base:** canonical main `f626db5c`. **No κ is claimed.** + +petalas's #4598 (head `c80f445e`) claims a count for k = 5 pairwise orthogonal rank-one requests on F₂⁶. Of all complete headers G ∈ GL₆(F₂), exactly **2,880** pass every guard; a guard asks that the leading principal minors of orders 1–5 of G P_t G⁻¹ be nonzero. The density is 1/6,999,552. This refutes the 2·k! = 240 pattern suggested at k = 3 and 4. + +This package recounts the headers **without #4598's method**. It uses no J − I decomposition, no rank or idempotence argument and no rectangle-subset search. It also imports nothing from #4598. + +## Method + +1. **Guard condition.** G P_t G⁻¹ = I − g_t h_tᵀ, where g_t is column t of G and h_t is row t of G⁻¹. So the order-j minor is 1 − Σ_{i≤j} h_t[i] g_t[i]. +2. **Headers as pairs.** Let X be the first k columns of G and Y the first k rows of G⁻¹. Headers correspond one-to-one with pairs (X, Y) satisfying YX = Σᵢ yᵢxᵢᵀ = I_k, because the last column of G is the unique nonzero vector of ker Y. +3. **Ordered convolution.** The count is therefore an ordered convolution of m = k+1 increments yᵢxᵢᵀ: + - the first k increments must have a zero diagonal; + - the total must be I_k; + - each increment is weighted by how many pairs (y, x) produce it, so the zero matrix has weight 2·2^k − 1. + + Zero and repeated increments are therefore counted, not excluded by argument. The convolution is evaluated exactly by meet-in-the-middle with Python integers. +4. **Failure control.** Drop the order-3 guard at k = 3 (m = 4). The convolution and the brute force over GL₄ then agree on a different count, 252. Both routes respond to the guard semantics in the same way. +5. **Cross-check.** Steps 1–3 are checked against the leading-minor definition by brute force over all of GL₃(F₂) (k = 2) and GL₄(F₂) (k = 3). The GL₄ check uses both the coordinate requests and a non-coordinate orthogonal family. + +## Result + +| k | 2 | 3 | 4 | 5 | +|---|---|---|---|---| +| passing headers (convolution) | 2 | 12 | 48 | **2,880** | +| brute force from the definition | 2 | 12 (both families) | — | — | + +- **Agreement.** Every value agrees with #4598, and with its k = 3, 4 controls (#4275, #4345). +- **Density.** |GL₆(F₂)| = 20,158,709,760 and 2,880 divides it, so the density is 1/6,999,552. +- **The 2·k! pattern fails at k = 5:** 2,880 ≠ 240. +- **Zero increments.** Setting the zero increment's weight to 0 leaves every count unchanged for k = 2 through 5. So no passing sequence contains a zero increment, which independently confirms the corresponding step of #4598's argument. +- **Independence.** The k = 5 total therefore follows from the minor condition through a different route. It does not depend on #4598's bijection or on its claim that every decomposition uses five distinct nonzero rectangles. Its zero-increment step is confirmed separately, as noted above. + +## Verify + +```text +python3 -B research/pr4598-header-recount/verify.py +``` + +The script takes about 9 s and uses the standard library only. + +## Limitations + +- **Scope.** Only #4598's stated header problem is checked: k ≤ 5, m = k+1, F₂, orthogonal kernels and complete equally weighted headers. +- **Not re-checked.** #4598's listing of the 24 subsets and its hand counterexample. +- **Brute force.** Coverage stops at GL₄. For k = 4 and 5 the result rests on the exact convolution together with the bijection derived above. + +## Open next questions + +- The same convolution gives the k = 6 (m = 7) count. Its meet-in-the-middle tables grow to roughly 3⁹ × 2^36 sums, so it needs a Walsh–Hadamard version with modular arithmetic. First step: port the convolution to a mod-p fast Walsh–Hadamard transform over 2^36 cells, or exploit the symmetric group action on coordinates to shrink the space. + +Credit: petalas (Nick Petalas) for #4598 and the #4275 threshold framing; Cinna Davis for the BIT request context. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4598-header-recount/SOURCES.json b/research/pr4598-header-recount/SOURCES.json new file mode 100644 index 0000000000..a2a5ea8bbd --- /dev/null +++ b/research/pr4598-header-recount/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/pr4598-header-recount/TASK.json b/research/pr4598-header-recount/TASK.json new file mode 100644 index 0000000000..4388d7c14f --- /dev/null +++ b/research/pr4598-header-recount/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 finite certificate (#4598) that refutes the 2 k! threshold pattern.", + "budget_minutes": 60, + "stop_rule": "Stop at k = 5 agreement.", + "outcome": "completed", + "evidence": "Exact ordered convolution over (y_i, x_i) pairs with YX = I and zero-diagonal prefixes gives 2/12/48/2880 for k = 2..5; brute force from the leading-minor definition over GL_3 and GL_4 (two orthogonal families) agrees; zero increments contribute nothing (counts unchanged at weight 0); failure control: dropping the order-3 guard gives 252 by both routes; density 1/6,999,552.", + "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": "k = 6 count.", + "why_it_matters": "Tests candidate replacement patterns for the refuted 2 k!.", + "first_step": "Mod-p Walsh-Hadamard version of the convolution over 2^36 cells or coordinate-symmetry reduction.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4598-header-recount/VERIFY.json b/research/pr4598-header-recount/VERIFY.json new file mode 100644 index 0000000000..bf569b9cb3 --- /dev/null +++ b/research/pr4598-header-recount/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": "Convolution counts 2/12/48/2880 for k = 2..5; brute-force agreement over GL_3 and GL_4 (two orthogonal families); zero-increment contribution 0; dropped-guard failure control 252 by both routes; GL_6 order and density." + } + ] +} diff --git a/research/pr4598-header-recount/verify.py b/research/pr4598-header-recount/verify.py new file mode 100644 index 0000000000..ec2638bb79 --- /dev/null +++ b/research/pr4598-header-recount/verify.py @@ -0,0 +1,150 @@ +#!/usr/bin/env python3 +"""Independent recount of PR #4598 (petalas): complete passing binary threshold headers for k requests in dimension k+1. + +Problem (from #4598/#4275): U_1..U_k pairwise orthogonal rank-one idempotents on F_2^m, m = k+1, normalized to +U_t = e_t e_t^T; P_t = I - U_t; a header G in GL_m(F_2) passes when every leading principal minor of G P_t G^-1 of +orders 1..m-1 is nonzero, for every t. #4598 claims 2,880 passing headers at k = 5 (and 12, 48 at k = 3, 4). + +Method, deliberately not #4598's (no J - I decomposition, no rank/idempotence argument, no rectangle-subset search): + * G P_t G^-1 = I - g_t h_t^T with g_t column t of G and h_t row t of G^-1, so the order-j minor is + 1 - sum_{i<=j} h_t[i] g_t[i] (matrix determinant lemma, derived here and checked by brute force below); + * headers correspond bijectively to pairs (X, Y), X the first k columns of G (rows x_i), Y the first k rows of + G^-1 (columns y_i), with Y X = sum_i y_i x_i^T = I_k: the last column is the unique nonzero vector of ker Y; + * so the count is the number of ordered sequences of m pairs (y_i, x_i) in F_2^k x F_2^k whose first k + increments y_i x_i^T have zero diagonal (supports disjoint) and whose total is I_k. Increments are weighted by + how many pairs give them (the zero matrix arises from 2*2^k - 1 pairs), so zero and repeated increments are + counted, not excluded a priori. The ordered convolution is evaluated exactly by meet-in-the-middle; + * the reformulation is cross-checked against the leading-minor definition by brute force over all of GL_4(F_2) + (k = 3) and GL_3 (k = 2), for the coordinate requests and for a non-coordinate orthogonal family. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from collections import Counter +from itertools import product +import json +import sys + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +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 convolve(table, weights): + out = Counter() + for a, wa in table.items(): + for r, wr in weights.items(): + out[a ^ r] += wa * wr + return out + + +def count_by_convolution(k, guarded=None, zero_weight=None): + """Ordered count of (y_i, x_i), i = 1..k+1, whose first `guarded` increments have zero diagonal + (default k: every guard order 1..k) and whose total is the identity.""" + guarded = k if guarded is None else guarded + 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 + need(sum(zero_diag.values()) == 3 ** k and zero_diag[0] == 2 ** (k + 1) - 1, "increment weights") + if zero_weight is not None: + zero_diag[0] = zero_weight + steps = [zero_diag] * guarded + [anything] * (k + 1 - guarded) + head, tail = Counter({0: 1}), Counter({0: 1}) + for w in steps[:(k + 1) // 2]: + head = convolve(head, w) + for w in steps[(k + 1) // 2:]: + tail = convolve(tail, w) + ident = sum(1 << (k * a + a) for a in range(k)) + return sum(w * tail.get(a ^ ident, 0) for a, w in head.items()) + + +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 leading_minors_nonzero(a, n, orders): + """Leading principal minors of orders 1..orders nonzero, by elimination without pivoting.""" + m = [row[:] for row in a] + for c in range(orders): + 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, requests, orders=None): + orders = n - 1 if orders is None else orders + passing = 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 + passing += all(leading_minors_nonzero(mat_mul(mat_mul(g, p, n), gi, n), n, orders) for p in requests) + return passing, total + + +def requests_from(q, n, k): + qi = inverse(q, n) + out = [] + for t in range(k): + p = [[int(i == j) ^ (i == t and j == t) for j in range(n)] for i in range(n)] + out.append(mat_mul(mat_mul(q, p, n), qi, n)) + return out + + +def main(): + counts = {k: count_by_convolution(k) for k in (2, 3, 4, 5)} + need(counts[3] == 12 and counts[4] == 48, "k = 3, 4 controls (#4275 / #4345)") + need(counts[5] == 2880, "#4598: 2,880 headers at k = 5") + order6 = 1 + for i in range(6): + order6 *= 64 - 2 ** i + need(order6 == 20158709760 and order6 % 2880 == 0 and order6 // 2880 == 6999552, "density 1/6,999,552") + need(counts[5] != 2 * 120, "the proposed 2 k! pattern fails at k = 5") + coordinate, gl4 = brute_force(4, requests_from([[int(i == j) for j in range(4)] for i in range(4)], 4, 3)) + q = [[1, 1, 0, 0], [0, 1, 1, 0], [1, 0, 1, 1], [0, 1, 0, 1]] + need(inverse(q, 4) is not None, "Q invertible") + other, _ = brute_force(4, requests_from(q, 4, 3)) + need(gl4 == 20160 and coordinate == counts[3] == other, "brute force over GL_4 matches the convolution at k = 3") + need(all(count_by_convolution(k, zero_weight=0) == counts[k] for k in (2, 3, 4, 5)), + "zero increments never occur in a passing sequence (counts unchanged with zero weight 0)") + dropped = count_by_convolution(3, guarded=2) + dropped_bf, _ = brute_force(4, requests_from([[int(i == j) for j in range(4)] for i in range(4)], 4, 3), orders=2) + need(dropped == dropped_bf != counts[3], "failure control: dropping the order-3 guard changes the count, both ways") + small, gl3 = brute_force(3, requests_from([[int(i == j) for j in range(3)] for i in range(3)], 3, 2)) + need(gl3 == 168 and small == counts[2], "brute force over GL_3 matches the convolution at k = 2") + print(json.dumps({"status": "PASS_PR4598_INDEPENDENT_RECOUNT", + "passing_headers_by_k": {str(k): v for k, v in counts.items()}, + "brute_force_GL4_k3": {"coordinate": coordinate, "non_coordinate_family": other, + "group_order": gl4}, + "brute_force_GL3_k2": small, + "k5_density": "1/%d" % (order6 // 2880), "two_k_factorial_at_k5": 240, + "zero_increments_contribute": 0, + "failure_control_drop_last_guard_k3": dropped, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())