Independently check #4586's width-growth lemmas with separate flow/width code (raw p7 to rank 4000): all hold (no new κ)

research/pr4586-width-growth-check/README.md

@@ -0,0 +1,40 @@
+# Independent check of #4586: quasipolynomial growth of chronological batch widths
+
+**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.**
+
+mihir-s-05's #4586 (head `aadb7bc5`) proves that #4507's chronological batch widths satisfy `log B_N = O((1+log N)^(d+2))`, where `d` is the number of primes dividing the rank alphabet. That is `exp(O((1+log N)^9))` for raw p7, replacing the inherited `exp(O(N log N))`. #4586 checks its lemmas on an authenticated copy of #4507's own generator. This package checks them with **separately written code**, `flow_widths.py`:
+- my default-height flow, written for my #4456 checks of #4436;
+- my chronological width recurrence, written when checking #4507.
+
+The raw p7 rule is bound to main's `research/higher-moment-strictification/RESULT.json` (SHA256-pinned).
+
+## Results
+
+All checked claims are confirmed through rank `N = 4000`: 3,880 ranks and 611,342 batch constraints.
+
+- **`B_1000`.** It has **2,524 bits**, as #4586 and #4507 report. `B_4000` has 5,834 bits.
+- **Rank descent.** Every recursive rank in `J_n`, both source complements `n−s` and actual exits `e`, is at most `⌊(m−1)n/m⌋` with `m = 121`.
+- **(4).** `B_n | L_N^D(n)` holds for every `n ≤ 4000`. This is checked by `D(n)` rounds of gcd stripping, with no factoring. Here `L_N` has 309 bits and `D(4000) = 373`.
+- **(2).** The depth bound `D(n) ≤ 1 + ⌊log(n/m)/log(m/(m−1))⌋` holds.
+- **Source-state lemma.** The flow's height and complete source census at `n` equal those at `m·t`, where `t` is the largest `Π`-smooth integer at most `⌊n/m⌋` and `Π = {2,3,5,7,11,19,41}` (`d = 7`). This holds for every `n ∈ [121, 4000]`, and every rank in the rule is `Π`-smooth.
+- **(5).** `|H(M)| = 27` against the bound 576 at `M = 33`.
+- **Explicit exponent.** At `N = 1000`, `D(N)·K_N·⌈log₂ C_N⌉ = 211·32·45 = 303,840`, exactly #4586's stated value.
+
+## Verify
+
+```text
+python3 -B research/pr4586-width-growth-check/verify.py
+```
+
+This runs in about 25 s with the standard library only.
+
+## Limitations
+
+- **Scope.** The written induction and counting argument are #4586's. This package checks every finite consequence above on a separate implementation, but it does not formalise the proof.
+- **Physical contracts.** These are #4507's and #4436's premises, and are out of scope.
+
+## Open next questions
+
+- A lower bound on the actual width growth, to see how loose the quasipolynomial bound is. The bound gives 303,840 bits at `N = 1000`, against 2,524 actual. First step: fit `log B_N` against `log N` over `N ≤ 4000` with the sequence computed here.
+
+Credit: mihir-s-05 (#4586), #4507's width construction and #4436's flow lineage (zxv, Jacob Alan Sussman). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.

research/pr4586-width-growth-check/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/higher-moment-strictification/RESULT.json",
+      "usage": "input",
+      "git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a",
+      "sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156"
+    }
+  ]
+}

research/pr4586-width-growth-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 the width-growth bound that shrinks the finite-word constants every compiler word must pay.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at #4586's finite consequences on raw p7 through rank 4000.",
+  "outcome": "completed",
+  "evidence": "Separate flow/width code on raw p7 through N=4000 (611,342 constraints): B_1000 = 2,524 bits; rank descent; B_n | L_N^D(n) for all n; depth bound; source-state lemma at every rank; counting bound; explicit exponent 303,840 at N=1000.",
+  "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": "How fast does the actual width grow?",
+      "why_it_matters": "The quasipolynomial bound is loose (303,840 vs 2,524 bits at N=1000).",
+      "first_step": "Fit log B_N vs log N over N <= 4000.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4586-width-growth-check/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/higher-moment-strictification/RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Separate flow/width code on raw p7 to rank 4000: B_1000 bits, rank descent, B_n | L_N^D(n), depth bound, source-state lemma, counting bound, explicit exponent 303,840."
+    }
+  ]
+}

research/pr4586-width-growth-check/flow_widths.py

@@ -0,0 +1,138 @@
+"""Separately written default-height flow (#4436) and chronological width recurrence (#4507) used by verify.py.
+
+The flow was written for my #4456 checks of #4436; the width recurrence for my check of #4507. Neither imports
+#4436's, #4507's or #4586's code. Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from fractions import Fraction as Q
+from math import factorial
+import itertools, json, sys
+def multis(n_types, size):
+    if n_types == 0:
+        if size == 0: yield ()
+        return
+    for x in range(size + 1):
+        for rest in multis(n_types - 1, size - x): yield (x,) + rest
+def flow(N, W, P):
+    ks = sorted(W); m = ks[-1]; kmin = ks[0]
+    def c(a):
+        v = 1
+        for k, x in zip(ks, a): v *= k ** x
+        return v
+    def u(a):
+        v = factorial(sum(a))
+        for k, x in zip(ks, a): v = v // factorial(x) * W[k] ** x
+        return v
+    G = 0
+    while kmin ** (G + 1) <= N // m: G += 1
+    F = [{1: 1}]
+    for d in range(1, G + 1):
+        nxt = {}
+        for rho, cnt in F[d - 1].items():
+            for r, pr in P.items():
+                if m * rho * r <= N: nxt[rho * r] = nxt.get(rho * r, 0) + cnt * pr
+        F.append(nxt)
+    S, X, BX = {}, {}, {}
+    col = units = matched = 0
+    add = lambda D, k, v: D.__setitem__(k, D.get(k, 0) + v)
+    present = lambda rho, a: m * rho * c(a) <= N
+    for d in range(G + 1):
+        for rho, cnt in F[d].items():
+            for b in multis(len(ks), G - d):
+                if not present(rho, b): continue
+                units += cnt * u(b); col += cnt * u(b) * rho * c(b)
+                for r, pr in P.items():
+                    issued = cnt * pr * u(b); rank = r * rho * c(b)
+                    if d == G:
+                        add(X, rank, issued); continue
+                    D = sum(W[k] * u(tuple(x - (i == j) for j, x in enumerate(b)))
+                            for i, k in enumerate(ks) if b[i] > 0 and present(rho * r, tuple(x - (i == j) for j, x in enumerate(b))))
+                    matched += cnt * pr * D
+                    if issued - cnt * pr * D:
+                        add(X, rank, issued - cnt * pr * D); add(BX, rank, issued - cnt * pr * D)
+    for a in multis(len(ks), G):
+        if present(1, a):
+            for k in ks: add(S, k * c(a), W[k] * u(a))
+    for d in range(1, G + 1):
+        for rho, cnt in F[d - 1].items():
+            for r, pr in P.items():
+                for a in multis(len(ks), G - d):
+                    if not present(rho * r, a): continue
+                    for i, k in enumerate(ks):
+                        b = list(a); b[i] += 1
+                        if not present(rho, tuple(b)):
+                            add(S, rho * r * c(tuple(b)), cnt * pr * u(a) * W[k])
+    return dict(G=G, S=S, X=X, BX=BX, col=col, units=units, matched=matched)
+
+
+import math, sys, time
+from math import gcd
+
+
+def lcm(a, b):
+    return a // gcd(a, b) * b
+
+
+def cuts(N, W, P):
+    """per-cut exit batches (e, q, copies) under the chronological policy, plus aggregate exits"""
+    ks = sorted(W); m = ks[-1]; kmin = ks[0]
+    G = 0
+    while kmin ** (G + 1) <= N // m:
+        G += 1
+    cap = N // m
+    Fh = [{1: 1}]
+    for h in range(1, G + 1):
+        nxt = {}
+        for c, v in Fh[-1].items():
+            for k, w in W.items():
+                if c * k <= cap:
+                    nxt[c * k] = nxt.get(c * k, 0) + w * v
+        Fh.append(nxt)
+    paths = [{1: 1}]  # depth -> rho -> multiplicity
+    for d in range(1, G + 1):
+        nxt = {}
+        for rho, mult in paths[-1].items():
+            for r, pr in P.items():
+                if m * rho * r <= N:
+                    nxt[rho * r] = nxt.get(rho * r, 0) + mult * pr
+        paths.append(nxt)
+    out, agg = [], {}
+    for d in range(G + 1):
+        h = G - d
+        for rho, mult in paths[d].items():
+            for c, units in Fh[h].items():
+                if m * rho * c > N:
+                    continue
+                for r, pr in P.items():
+                    if h == 0:
+                        q = units  # = 1: every paid job of the leaf class exits
+                    else:
+                        q = sum(w * Fh[h - 1].get(c // k, 0) for k, w in W.items()
+                                if c % k == 0 and m * rho * r * (c // k) > N)
+                    if q:
+                        e = rho * r * c
+                        out.append((e, q, mult * pr))
+                        agg[e] = agg.get(e, 0) + q * mult * pr
+    return G, out, agg
+
+
+def widths(W, P, Nmax, check_every=0):
+    m = max(W)
+    B = [1] * m  # base widths below m (B_0 = 1)
+    nested = [1] * m
+    for N in range(m, Nmax + 1):
+        R = flow(N, W, P)
+        G, cs, agg = cuts(N, W, P)
+        assert agg == {e: v for e, v in R['X'].items() if v}, (N, 'aggregate exits match the flow')
+        S = sum(R['S'].values())
+        a = 1
+        for s, cnt in R['S'].items():
+            e = N - s
+            a = lcm(a, B[e] // gcd(B[e], cnt))
+        for e, q, _ in cs:
+            a = lcm(a, B[e] // gcd(B[e], q))
+        B.append(S * a)
+        nested.append(nested[-1] * S)
+        assert nested[-1] % B[-1] == 0, (N, 'new width divides nested width')
+    return B, nested
+
+