diff --git a/research/two-short-row-coefficients/README.md b/research/two-short-row-coefficients/README.md new file mode 100644 index 0000000000..6badb16e34 --- /dev/null +++ b/research/two-short-row-coefficients/README.md @@ -0,0 +1,83 @@ +# Which coefficients admit exactly two short rows? + +**Task:** independent-moment (a complete answer, within the row model, to #4600's open question 1). **Base:** canonical main `f626db5c`. **No κ is claimed.** + +## Background + +petalas's #4600 (head `44640c4a`, open) works in #4280's row model of balanced unsigned depth-four dirty chain words with modulus m. It proves that two short rows realizing c ≠ 0 force **m | cL** for each short length L. Unit coefficients therefore need at least three short rows. It also gives the family m = 8t, c = 4t. Its open question 1 asks which nonzero coefficients admit exactly two short rows, noting that the annihilator condition is not known to be sufficient. + +The model is the following. Profiles λ (row lengths L_q), ρ and β each have m nonincreasing entries in [0, m], with B(L) = β₁ + … + β_L. A triple is correct exactly when + +```text +Σ L_q = Σ ρ_q = Σ β_p = 0, Σ ρ_q L_q = Σ B(L_q) = 0, Σ ρ_q B(L_q) = −c (mod m). +``` + +## Results + +### Theorem: gcd(c, m) = 2 is impossible, with a written proof + +If exactly two short rows realize c ≠ 0, then **gcd(c, m) ≥ 3**. + +**Proof.** Let g = gcd(c, m). By #4600, m/g divides L₁ and L₂, and L₁ + L₂ = m. If g = 2, then L₁ = L₂ = m/2, and the congruences become + +```text +(r₁ − r₂)·m/2 ≡ 0, 2·B(m/2) ≡ 0, c ≡ −(r₁ + r₂)·B(m/2) (mod m). +``` + +The first makes r₁ − r₂ even, so r₁ + r₂ is even too. The second gives B(m/2) ∈ {0, m/2}. Hence c ≡ 0 (mod m), a contradiction. ∎ + +### Exact enumeration for every m ≤ 12 + +The enumeration ranges over all nonincreasing ρ and β, and every placement of the two short rows after the full rows. It shows that **the achievable nonzero c are exactly {c : gcd(c, m) ≥ 3}**: + +| m | achievable c | allowed by m \| cL but not achievable | +|---|---|---| +| 4 | — | 2 | +| 6 | 3 | 2, 4 | +| 8 | 4 | 2, 6 | +| 9 | 3, 6 | — | +| 10 | 5 | 2, 4, 6, 8 | +| 12 | 3, 4, 6, 8, 9 | 2, 10 | +| 2, 3, 5, 7, 11 | — | — | + +- **The annihilator condition alone is not sufficient.** +- **The strengthened condition is exactly right for m ≤ 12**, and the construction below extends this to every m. + +### Theorem: gcd(c, m) ≥ 3 is sufficient for every m, with an explicit construction + +Let g = gcd(c, m) ≥ 3, d = m/g and c ≡ g·r with 0 < r < d. Take + +```text +λ = (m, m−d, d, 0, …), ρ = (m−g, g, 0, …), +β = ((g+1)^r, g^(d−r), M, 1^r, 0^(d−r)), +``` + +where M is the balanced nonincreasing sequence of length (g−2)d and sum m − 2r. Its entries lie in [1, g] because g ≥ 3. + +- **Profiles valid.** All three profiles are nonincreasing with entries in [0, m]. +- **Partial sums.** B(d) = m + r, B(m−d) = 2m − r and B(m) = 2m. +- **Congruences.** Σ L = 2m, Σ ρ = m, Σ ρL ≡ −gd ≡ 0 and Σ B(L) = 5m. The coefficient is −[(m−g)·2m + g(2m−r)] ≡ g·r = c. ∎ + +The verifier checks the construction for every pair (m, c) with m ≤ 200 and gcd(c, m) ≥ 3, which is 4,626 pairs. + +**So within #4280's row model, exactly two short rows realize c ≠ 0 if and only if gcd(c, m) ≥ 3.** +- **Family check.** #4600's family m = 8t, c = 4t is checked directly for t = 1, …, 64: valid profiles, all congruences, exactly two short rows and c = 4t. This agrees with the table, since gcd(4t, 8t) = 4t ≥ 4. + +## Verify + +```text +python3 -B research/two-short-row-coefficients/verify.py +``` + +The check takes about 3 s and uses the standard library only. + +## Limitations + +- **Inherited assumptions.** The row model and its converse (every correct triple comes from a balanced word) are inherited from #4280 and are not re-proved here. +- **Not claimed.** A call-count claim beyond #4600's, a physical caller, a supplier or κ. + +## Open next questions + +- **Beyond the balanced row model.** Every balanced word uses each call exactly m times, so every coefficient realized here costs exactly #4600's 4m calls. The open direction is unbalanced or signed depth-four words, where short-row counts and call counts can separate. First step: restate #4280's congruences for a word with one call used m + 1 times. + +Credit: petalas (Nick Petalas) for #4600 and #4280 (row model). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/two-short-row-coefficients/SOURCES.json b/research/two-short-row-coefficients/SOURCES.json new file mode 100644 index 0000000000..a2a5ea8bbd --- /dev/null +++ b/research/two-short-row-coefficients/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/two-short-row-coefficients/TASK.json b/research/two-short-row-coefficients/TASK.json new file mode 100644 index 0000000000..25cbbd2813 --- /dev/null +++ b/research/two-short-row-coefficients/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": "Partial answer to #4600 OQ1 (two-short-row coefficients in the depth-four row model).", + "budget_minutes": 30, + "stop_rule": "Stop at the exact characterization.", + "outcome": "completed", + "evidence": "Necessity proof gcd(c,m) >= 3; explicit sufficiency construction for every m (checked for all 4,626 pairs with m <= 200); exact enumeration for m <= 12 agrees; annihilator-only c exist; #4600 family t <= 64.", + "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": "Short-row versus call counts for unbalanced or signed depth-four words.", + "why_it_matters": "In the balanced model every realized coefficient costs exactly 4m calls.", + "first_step": "Restate #4280's congruences with one call used m+1 times.", + "blocked_by": "None." + } + ] +} diff --git a/research/two-short-row-coefficients/VERIFY.json b/research/two-short-row-coefficients/VERIFY.json new file mode 100644 index 0000000000..fe4c8c5de3 --- /dev/null +++ b/research/two-short-row-coefficients/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": "Exhaustive two-short-row coefficient sets for m <= 12 vs gcd(c,m) >= 3 and the annihilator condition; #4600 family t <= 64. Explicit construction for every gcd(c,m) >= 3 pair with m <= 200." + } + ] +} diff --git a/research/two-short-row-coefficients/verify.py b/research/two-short-row-coefficients/verify.py new file mode 100644 index 0000000000..bde15ec673 --- /dev/null +++ b/research/two-short-row-coefficients/verify.py @@ -0,0 +1,142 @@ +#!/usr/bin/env python3 +"""Which coefficients admit exactly two short rows? (#4600 open question 1, petalas) + +Model (#4280 row model, as restated in #4600): a balanced depth-four word with modulus m is a triple of profiles +(lambda, rho, beta), each with m entries in [0, m] and nonincreasing (lambda is the partition of row lengths L_q). +It is correct exactly when + sum L_q = sum rho_q = sum beta_p = 0, sum rho_q L_q = sum B(L_q) = 0, sum rho_q B(L_q) = -c (mod m), +with B(L) = beta_1 + ... + beta_L. A short row has 0 < L_q < m. #4600 proves: two short rows imply m | cL for each +short length L (so units need three), and gives the family m = 8t, c = 4t. + +New here: + (1) Theorem (written proof). If exactly two short rows realize c != 0 then gcd(c, m) >= 3. + Proof: by #4600, m/g | L_1, L_2 with g = gcd(c, m) and L_1 + L_2 = m. If g = 2, L_1 = L_2 = m/2. The + congruences become (r_1 - r_2) m/2 = 0, 2 B(m/2) = 0 and c = -(r_1 + r_2) B(m/2) (mod m). The first makes + r_1 - r_2, hence r_1 + r_2, even; the second gives B(m/2) in {0, m/2}; so c = 0 (mod m). Contradiction. + (2) Exact exhaustive enumeration of the profile model for every m <= 12 (all nonincreasing rho and beta, all + placements of the two short rows): the achievable nonzero c are exactly {c : gcd(c, m) >= 3}. So for m <= 12 + the strengthened condition is also sufficient, while the annihilator condition alone is not (m = 4, 6, 8, 10, 12 + have annihilator-allowed c with gcd 2 that no two-short-row word realizes). + (3) Theorem (sufficiency, every m): if g = gcd(c, m) >= 3, write d = m/g, c = g r (0 < r < d), and take + lambda = (m, m-d, d, 0...), rho = (m-g, g, 0...), beta = ((g+1)^r, g^(d-r), M, 1^r, 0^(d-r)) with M the + balanced nonincreasing sequence of length (g-2)d and sum m - 2r (entries in [1, g] since g >= 3). Then + B(d) = m + r, B(m-d) = 2m - r, B(m) = 2m, every congruence holds and the coefficient is g r = c. Checked for + every such (m, c) with m <= 200. Hence, in the row model, two short rows suffice iff gcd(c, m) >= 3. + (4) #4600's family m = 8t, c = 4t: profiles valid and all congruences hold, with exactly two short rows, t = 1..64. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from math import gcd +import json +import sys + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def profiles(m): + out = [] + + def rec(prefix, top): + if len(prefix) == m: + out.append(tuple(prefix)) + return + for v in range(top, -1, -1): + prefix.append(v) + rec(prefix, v) + prefix.pop() + rec([], m) + return out + + +def two_row_coefficients(m): + """All nonzero c realized with exactly two short rows, by exhaustive enumeration of rho and beta.""" + balanced = [p for p in profiles(m) if sum(p) % m == 0] + rho_pairs = {f: {(p[f] % m, p[f + 1] % m) for p in balanced} for f in range(m - 1)} + b_pairs = {} + for p in balanced: + pre = [0] + for v in p: + pre.append(pre[-1] + v) + for la in range((m + 1) // 2, m): + b_pairs.setdefault(la, set()).add((pre[la] % m, pre[m - la] % m)) + found = set() + for f in range(m - 1): # lambda = (m^f, L_a, L_b, 0, ...) with L_a + L_b = m + for la in range((m + 1) // 2, m): + lb = m - la + for ra, rb in rho_pairs[f]: + if (ra * la + rb * lb) % m: + continue + for x, y in b_pairs[la]: + if (x + y) % m == 0: + c = -(ra * x + rb * y) % m + if c: + need(c * la % m == 0 and c * lb % m == 0, "#4600 annihilator condition") + found.add(c) + return found + + +def family_check(t): + m = 8 * t + lam = [m, 6 * t, 2 * t] + [0] * (m - 3) + rho = [m - 4, 4] + [0] * (m - 2) + beta = [5] * t + [4] * t + [2] * (2 * t) + [1] * (3 * t) + [0] * t + for p in (lam, rho, beta): + need(len(p) == m and all(0 <= v <= m for v in p) and all(a >= b for a, b in zip(p, p[1:])), "profile") + pre = [0] + for v in beta: + pre.append(pre[-1] + v) + big_b = lambda length: pre[length] + need(sum(lam) % m == sum(rho) % m == sum(beta) % m == 0, "sums") + need(sum(r * l for r, l in zip(rho, lam)) % m == 0 and sum(big_b(l) for l in lam) % m == 0, "weighted sums") + c = -sum(r * big_b(l) for r, l in zip(rho, lam)) % m + need(c == 4 * t and sum(0 < l < m for l in lam) == 2, "c = 4t with exactly two short rows") + + +def construction(m, c): + """Explicit two-short-row profiles for any c with g = gcd(c, m) >= 3 (c = g r, 0 < r < d = m/g).""" + g = gcd(c, m) + d, r = m // g, c // g + lam = [m, m - d, d] + [0] * (m - 3) + rho = [m - g, g] + [0] * (m - 2) + mid_len, mid_sum = (g - 2) * d, m - 2 * r + q, extra = divmod(mid_sum, mid_len) + middle = [q + 1] * extra + [q] * (mid_len - extra) + beta = [g + 1] * r + [g] * (d - r) + middle + [1] * r + [0] * (d - r) + for p in (lam, rho, beta): + need(len(p) == m and all(0 <= v <= m for v in p) and all(a >= b for a, b in zip(p, p[1:])), "profile") + pre = [0] + for v in beta: + pre.append(pre[-1] + v) + need(sum(lam) % m == sum(rho) % m == sum(beta) % m == 0, "sums") + need(sum(x * l for x, l in zip(rho, lam)) % m == 0 and sum(pre[l] for l in lam) % m == 0, "weighted sums") + need(-sum(x * pre[l] for x, l in zip(rho, lam)) % m == c and sum(0 < l < m for l in lam) == 2, + "construction realizes c with exactly two short rows") + + +def main(): + table = {} + for m in range(2, 13): + found = two_row_coefficients(m) + strengthened = {c for c in range(1, m) if gcd(c, m) >= 3} + annihilator = {c for c in range(1, m) if any(c * l % m == 0 for l in range(1, m))} + need(found == strengthened, "m = %d: achievable set is exactly gcd(c, m) >= 3" % m) + need(found <= annihilator, "annihilator condition is necessary") + table[m] = {"achievable": sorted(found), "annihilator_only": sorted(annihilator - found)} + need(any(v["annihilator_only"] for v in table.values()), "annihilator condition alone is not sufficient") + for t in range(1, 65): + family_check(t) + constructed = 0 + for m in range(2, 201): + for c in range(1, m): + if gcd(c, m) >= 3: + construction(m, c) + constructed += 1 + print(json.dumps({"status": "PASS_TWO_SHORT_ROW_COEFFICIENTS", "table": table, "family_t_checked": 64, + "construction_checked_pairs_m_le_200": constructed, + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())