diff --git a/research/chronological-width-growth/.gitattributes b/research/chronological-width-growth/.gitattributes
new file mode 100644
index 0000000000..fa1385d99a
--- /dev/null
+++ b/research/chronological-width-growth/.gitattributes
@@ -0,0 +1 @@
+* -text
diff --git a/research/chronological-width-growth/README.md b/research/chronological-width-growth/README.md
new file mode 100644
index 0000000000..006711acd6
--- /dev/null
+++ b/research/chronological-width-growth/README.md
@@ -0,0 +1,293 @@
+# A quasipolynomial upper bound for chronological batch widths
+
+**Result:** for every fixed integer rule in #4436's default-height flow,
+the chronological gcd/LCM widths constructed in #4507 satisfy
+
+\[
+\log B_N=O((1+\log N)^{d+2}),\qquad
+B_N=\exp(O((1+\log N)^{d+2})),
+\]
+
+where `d` is the number of distinct primes dividing the target or paid
+**ranks**, and the hidden constant depends on the fixed rule. This answers
+the all-rank upper-bound part of [#4507's handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/4503).
+It improves the inherited `exp(O(N log N))` upper bound for that already
+constructed width sequence. It does not assert a matching lower bound,
+polynomial width, or a finite-rank improvement beyond #4507.
+
+For the retained raw p7 rule, `d=7`, so this gives
+`B_N = exp(O((1+log N)^9))`. The normalized leaf recurrence and all paid
+operations are unchanged. **No new kappa or native admission is claimed.**
+
+## 1. Exact scope and predecessor result
+
+Fix positive integer multiplicities `W_k` on target ranks and `P_r` on paid
+ranks, with `2 <= k_min <= m=max(k)` and `1 <= r_max < m`. The paid positions
+retain their chronological order. At rank `n>=m`, use precisely #4436's
+height `G(n)=floor(log_(k_min)(floor(n/m)))` and its source census `S_s(n)`.
+Write `S(n)=sum_s S_s(n)`. The base widths are `B_e=1` for `0<=e<m`.
+
+Keep #4507's batching policy: source complements are batched before the
+flow; unmatched exits finish separately at their actual parent-round cut.
+If `J_n` is this finite list of `(e,q)` rank/count constraints, its formula is
+
+\[
+B_n=S(n)\mathop{\mathrm{lcm}}_{(e,q)\in J_n}
+       \frac{B_e}{\gcd(B_e,q)}. \tag{1}
+\]
+
+Separate occurrences must not multiply the per-cut `q`. #4507 already
+proves (1) admissible and locally minimal for its prescribed smaller
+library, and proves that normalized leaf cost is unchanged. Those are
+predecessor results. This package proves an all-rank bound on (1).
+
+The source hypotheses still include an all-column arbitrary-input native
+word, disjoint splitting, priced whole-job adapters, and finite-program
+closure with owned initialization/erasure. We use the source's counting
+construction; we do not supply or re-audit those physical contracts.
+
+## 2. A depth envelope for every prime valuation
+
+Put `a=(m-1)/m`. Define the integer function
+
+```text
+D(n)=0                         if 0<=n<m,
+D(n)=1+D(floor(a*n))            if n>=m.
+```
+
+Every recursive rank in `J_n` is at most `floor(a*n)`. Indeed, source
+complements have `e=n-s` with `s>n/m`, and actual exits have
+`e<=r_max*n/m< n`. Since `r_max<=m-1`, both bounds imply the claim.
+This uses the actual source and exit inequalities of #4436 section 2,
+including its premature exits. Mere strict descent `e<n` would not suffice
+for the logarithmic-depth conclusion.
+
+The map `n -> floor(a*n)` is increasing. Its hitting time `D` is therefore
+nondecreasing, and each recursive edge satisfies `D(e)<=D(n)-1`.
+Also, iteration is at most `a^j*n`; hence for `n>=m`,
+
+\[
+D(n)\le 1+\left\lfloor
+  \frac{\log(n/m)}{\log(m/(m-1))}\right\rfloor=O(1+\log n). \tag{2}
+\]
+
+For fixed `N>=m`, let `L_N=lcm{S(j): m<=j<=N}`. For **any prime** `ell`,
+the exact valuation of (1) is
+
+\[
+v_\ell(B_n)=v_\ell(S(n))+
+ \max_{(e,q)\in J_n}\max(0,v_\ell(B_e)-v_\ell(q)). \tag{3}
+\]
+
+Strong induction, starting with zero valuations of the base widths, gives
+
+\[
+v_\ell(B_n)\le D(n)v_\ell(L_N),\quad
+B_n\mid L_N^{D(n)}\quad(0\le n\le N). \tag{4}
+\]
+
+The induction step bounds every child valuation by
+`(D(n)-1)*v_ell(L_N)` and the added source valuation by `v_ell(L_N)`.
+Taking maxima never adds sibling valuations. This is the benefit of the
+LCM recurrence. No monotonicity or nesting of `B_n` is assumed.
+
+## 3. Only polynomially many logarithmic-scale source states
+
+Let `Pi` contain every prime dividing a rank in either fixed alphabet,
+and put `d=|Pi|`, `M=floor(N/m)`. A positive integer is called
+`Pi-smooth` here if all its prime divisors lie in `Pi`; 1 is included.
+Let `H(M)` be the set of such integers at most `M`.
+
+**Source-state lemma.** For any `n>=m`, put `c=floor(n/m)` and let `t`
+be the largest `Pi-smooth` integer at most `c`. The complete unreplicated
+flow, and in particular `S(n)`, agrees with the flow at ambient rank `m*t`.
+This statement concerns the flow before adding the rank-`n-s` complements;
+those complement ranks can still change as `n` changes.
+
+**Proof.** The flow's predicates use the cutoff `c` and height `G` only.
+Height changes at powers `k_min^j`, all in `H`. Within one height, each
+class has an ordered paid path with product `rho`, and each target point
+has product `c(b)`. Presence is the predicate
+`rho*c(b)<=c`. Child presence has the same form, with one more paid factor
+and one fewer target factor. Every threshold is thus an integer product of
+target and paid ranks, hence is `Pi-smooth`. Target multiplicities,
+ordered-path multiplicities and Pascal matching counts are fixed between
+these thresholds. The root sources, absent-parent sources, matched jobs,
+unmatched exits and their counts are consequently unchanged. Pruning an
+empty class introduces no new threshold. There is no threshold between
+`t` and `c`, and height agrees too. This proves the lemma. QED.
+
+We use a superset of the actual thresholds: not every smooth number must
+occur as a flow threshold. In particular,
+
+\[
+\{S(j):m\le j\le N\}=\{S(mt):t\in H(M)\},\qquad
+|H(M)|\le\prod_{p\in\Pi}(1+\lfloor\log_p M\rfloor). \tag{5}
+\]
+
+The cardinality bound simply counts nonnegative prime-exponent vectors
+and drops their joint product constraint. It needs no prime-distribution
+estimate. **Rank primes are not width primes.** Source counts can have new
+prime factors; (3)-(4) apply to all of them through `L_N`.
+
+## 4. Explicit all-rank bound
+
+Let `W=sum W_k`, `P=sum P_r`, `h=G(N)`, and
+
+```text
+C_N = W*(W+P+1)^(h+1),
+K_N = product_(p in Pi) (1+floor(log_p(floor(N/m)))).
+```
+
+The source's untruncated unit census gives
+`U(n)<=sum_(j=0..G(n)) P^j W^(G(n)-j)` and `S(n)<=W*U(n)`.
+Therefore `1<=S(n)<=C_N` for `m<=n<=N`. Combining (4)-(5),
+
+\[
+B_N\mid L_N^{D(N)},\qquad
+L_N\le\prod_{t\in H(M)}S(mt)\le C_N^{|H(M)|}\le C_N^{K_N},
+\]
+\[
+\boxed{B_N\le C_N^{D(N)K_N}
+       \le 2^{D(N)K_N\lceil\log_2 C_N\rceil}.} \tag{6}
+\]
+
+For a **fixed** rule, `D(N)=O(1+log N)`, `log C_N=O(1+log N)` and
+`K_N=O((1+log N)^d)`. Equation (6) proves the announced bound. The
+constants and `d` are not uniform over rules whose ranks or multiplicities
+grow with `N`. The theorem is a sharper asymptotic upper bound, not a proof
+that the actual width has this growth order.
+
+For raw p7, the rank primes are `{2,3,5,7,11,19,41}`. At `N=1000`,
+the conservative binary exponent in (6) is 303,840; the actual width has
+2,524 bits, as already reported by #4507. The new bound is deliberately
+loose and does not improve that finite witness. Its value is its all-rank
+growth guarantee. Base ranks below `m` have width 1 separately.
+
+## 5. Exact evidence and controls
+
+The written argument proves the universal conclusion. Finite checks test
+its source binding and failure modes; they do not extrapolate a theorem.
+
+`verify.py` executes the authenticated, unmodified #4507 `batches.py` to
+obtain the actual source flows and width sequence. It does not call that
+reuse an independent flow implementation. The new `growth.py` separately
+computes prime valuations, prime-product intervals and the depth envelope.
+All comparisons use integers; every retained RESULT.json field is compared.
+
+| Fixed flow | Maximum compiled rank | Rank primes | Actual width bits | All-rank conclusion |
+| --- | ---: | --- | ---: | --- |
+| `{2:1,5:1} <- {1:2,4:1}` | 100 | 2, 5 | 42 | `log B_N=O((1+log N)^4)` |
+| `{2:4,3:1} <- {1:6,2:2}` | 100 | 2, 3 | 88 | `log B_N=O((1+log N)^4)` |
+| Raw p7 | 1,000 | 2, 3, 5, 7, 11, 19, 41 | 2,524 | `log B_N=O((1+log N)^9)` |
+
+The replay covers 1,074 nonbase ranks and 49,474 actual batch constraints:
+the valuation recurrence equals the existing width at every rank; all
+children satisfy the stronger fractional rank descent; every valuation is
+within (4); and sampling the prime products gives exactly the source LCM
+obtained from all ranks. Final width hashes reproduce the pinned receipt.
+
+There are 832 cutoff cases: both toys and p7 through cutoff 256, and a
+paid-prime fixture through 64. Complete flow records agree at the first
+and last ambient rank of each floor-cutoff interval and with the previous
+smooth representative. Of these, 642 compare a cutoff with a **strictly
+smaller** smooth representative, so the check is not only identity cases.
+
+Ten rejection controls include these concrete failures:
+
+- Omitting paid prime 3 for targets `{2:1,5:1}`, paid `{1:2,3:1}` wrongly
+  identifies cutoffs 2 and 3. Their source counts are 4 and 5 respectively.
+- Restricting width primes to rank primes fails immediately: the `{2,3}`
+  target fixture has `B_3=5`.
+- Dropping depth from (4) fails at `n=7` in the first toy: `B_7=4` but
+  the source LCM through rank 7 is 2.
+- Omitting gcd cancellation changes that toy's exact `B_22` from 896 to
+  1,792. This would remain a looser upper bound, but is not equation (3).
+
+Other controls reject noncontracting child ranks, zero batch counts,
+out-of-contract rules, a composite claimed prime, and omission of the
+source multiplier. No input-validator control is a substitute for the proof.
+
+## 6. Reproduction and provenance
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python -B scripts/research_package.py --package research/chronological-width-growth
+python -I -O -B research/chronological-width-growth/verify.py
+python -B scripts/check_research_commit.py --package research/chronological-width-growth --check-source-history
+```
+
+Normal and optimized registered replays are declared in VERIFY.json.
+Direct replay is self-contained and needs no Git or network. `--write` is
+an authoring command only; registered replay never rewrites the receipt.
+The five exported predecessor files are authenticated by Git blob and
+SHA256 before execution. VENDOR.json binds them to canonical main
+`f626db5c3a3d781d8f7695038776c621651f75e1`; SOURCES.json pins that main's
+catalogue, selected record and original files as historical provenance.
+No frozen predecessor is changed.
+
+This takes the explicit #4507 handoff, changing the `independent-moment`
+card from invoice audit to all-rank compiler width. The scope is recorded
+in TASK.json. #4519 already independently recounts the finite widths;
+#4476 checks the older nested construction, and #4521 its expanded counts.
+#4483 changes the height and convergence policy. None is represented here
+as missing finite coverage or as a premise establishing this new bound.
+Canonical coordination is the [claim in #4503](https://github.com/CrocSwap/integer-mult-bounds/discussions/4503#discussioncomment-19117802).
+
+Initial overlap covered all 5,860 tracked top-level note paths after sparse
+materialization, 355 open PRs, and 3,470 Discussion records, with reported
+complete remote pagination at 07:48-07:50 UTC on October 22, 2026.
+Closed PRs were covered only by local notes/ledger and targeted GitHub
+search. This is bounded text coverage, not every historical diff or proof
+of novelty. Submission freshness is recorded in TASK.json.
+
+The orientation-only baseline stopped on sparse-omitted
+`research/kappa-rebuild/CLAIM.json`; no baseline PASS is claimed. Package
+validation is separate. On CPython 3.12.0 / Windows, the registered ordinary
+and optimized replays pass (about 12 seconds together). An isolated copy
+passes with `-I -O -B`, Git absent from PATH and socket creation disabled;
+its files remain unchanged. Separate source-byte and receipt corruptions
+reject, as do mutations omitting paid breakpoint primes or collapsing the
+depth factor. The committed 14-file export also passes integrity checking
+and an isolated optimized replay with Git unavailable, socket creation
+disabled and unchanged bytes. Committed-byte preflight passes. The optional
+source-history preflight requires full Git history and did not run in this
+shallow checkout; all source pins are at this branch's canonical-main base.
+These are author-side tests, not an independent reviewer. No full selected
+cold replay, formal proof kernel, independent human review or
+native/physical/outer admission is claimed.
+
+## Open next questions
+
+1. **Can actual source valuations improve the exponent `d+2` or the finite
+   constants?** This would improve resource estimates beyond a loose
+   existence bound. Start with `v_ell(S(mt))` on actual transition points,
+   retaining repeated visits along contraction paths. A uniform argument
+   and a matching lower bound remain absent; merely extending finite
+   plots cannot establish the answer.
+2. **Does a comparable source-state argument apply to #4483's changed-height
+   compiler?** That would connect the width estimate to its stronger leaf
+   theorem. First pin its height rule and inventory and identify every
+   rank-dependent predicate. This package does not verify that different
+   policy, so it supplies no transferred bound for it.
+
+Neither question authorizes an automatic search campaign. Stop at the
+bounded source-state/valuation obligation. A width bound is not a bound on
+the time to generate every smaller program; native realization, complete
+storage, precision and tape costs still require their own evidence.
+
+## Credit
+
+Jacob Alan Sussman supplied the integer lockstep compiler. zxv supplied
+#4436's overlapping direct flow, rank bounds, source-count ceiling and
+original LCM freedom. Mihir Srivastava's #4507 supplied the chronological
+gcd/LCM policy and smaller finite width construction. Cinna Davis /
+1337isnot1337 supplied the raw p7 rule. Ryanson Jonathan / pinterbanget
+supplied #4456, #4476 and #4519's independent checks; the retained native
+and outer lineage remains credited in the exported source notes.
+
+Prepared for **Mihir Srivastava / mihir-s-05 with substantial OpenAI Codex
+assistance** in proof development, implementation, verification and writing.
+No subagents or independently launched reviewer were used. New work is
+Apache-2.0; exported sources retain their original notices.
diff --git a/research/chronological-width-growth/RESULT.json b/research/chronological-width-growth/RESULT.json
new file mode 100644
index 0000000000..fc14ed6582
--- /dev/null
+++ b/research/chronological-width-growth/RESULT.json
@@ -0,0 +1,231 @@
+{
+  "breakpoints": [
+    {
+      "cap": 256,
+      "change_points_sha256": "b4d086ac85f9a511f4d508d97c4850314c0e4332d447068c2e3123ed9a55aeb3",
+      "nontrivial_constant_comparisons": 235,
+      "rank_primes": [
+        2,
+        5
+      ],
+      "rule": "strict-overlap",
+      "smooth_products": 21,
+      "source_count_changes": 20
+    },
+    {
+      "cap": 256,
+      "change_points_sha256": "99a34ed2e921a1b577d77ade6e826814aaf409c0d52dfefbabda80c10d333a01",
+      "nontrivial_constant_comparisons": 228,
+      "rank_primes": [
+        2,
+        3
+      ],
+      "rule": "source-open-equality",
+      "smooth_products": 28,
+      "source_count_changes": 27
+    },
+    {
+      "cap": 256,
+      "change_points_sha256": "57f0884719161944b3a926e0e4f3d8a888c1b67717311e202310c1c451b9a311",
+      "nontrivial_constant_comparisons": 142,
+      "rank_primes": [
+        2,
+        3,
+        5,
+        7,
+        11,
+        19,
+        41
+      ],
+      "rule": "raw-p7",
+      "smooth_products": 114,
+      "source_count_changes": 69
+    },
+    {
+      "cap": 64,
+      "change_points_sha256": "eae974eee809c82a022291816e6f494db07e687d8e7d9e2ba7b72a86bef0c773",
+      "nontrivial_constant_comparisons": 37,
+      "rank_primes": [
+        2,
+        3,
+        5
+      ],
+      "rule": "paid-prime-control",
+      "smooth_products": 27,
+      "source_count_changes": 26
+    }
+  ],
+  "claim_type": "all-rank conditional width upper bound with finite exact checks",
+  "compilations": [
+    {
+      "all_rank_valuation_sha256": "ebd33196e325a55f197b58c28d92ad906c00b0b1e58a95e5ddf22a0ac9c6354e",
+      "batch_constraints": 1045,
+      "compiled_ranks": 96,
+      "first_denominator_needed": {
+        "n": 22,
+        "width": 896,
+        "without_gcd": 1792
+      },
+      "first_depth_needed": {
+        "n": 7,
+        "source_lcm": 2,
+        "width": 4
+      },
+      "maximum": 100,
+      "parameters": {
+        "cap": 20,
+        "d": 2,
+        "depth": 13,
+        "height": 4,
+        "log_degree": 4,
+        "power_of_two_exponent": 1820,
+        "prime_box_count": 10,
+        "rank_primes": [
+          2,
+          5
+        ],
+        "source_ceiling": 15552
+      },
+      "rule": "strict-overlap",
+      "source_lcm": {
+        "bits": 19,
+        "unsigned_big_endian_sha256": "55ad2189ba8d2e22fecd8ddb7569436790f224bce6e6aea7c6ebc30c7279542d"
+      },
+      "source_values": 8,
+      "width": {
+        "bits": 42,
+        "unsigned_big_endian_sha256": "a61817c96be89d11dec54f0b0ef5da6a27a6bea836b240cb170c488a1123c77c"
+      }
+    },
+    {
+      "all_rank_valuation_sha256": "90d85720de9c43bb7bbe35abb56ffba8a13d0c539915b554306385579830a157",
+      "batch_constraints": 1349,
+      "compiled_ranks": 98,
+      "first_denominator_needed": {
+        "n": 10,
+        "width": 875,
+        "without_gcd": 3500
+      },
+      "first_depth_needed": {
+        "n": 5,
+        "source_lcm": 5,
+        "width": 25
+      },
+      "maximum": 100,
+      "parameters": {
+        "cap": 33,
+        "d": 2,
+        "depth": 9,
+        "height": 5,
+        "log_degree": 4,
+        "power_of_two_exponent": 5616,
+        "prime_box_count": 24,
+        "rank_primes": [
+          2,
+          3
+        ],
+        "source_ceiling": 37647680
+      },
+      "rule": "source-open-equality",
+      "source_lcm": {
+        "bits": 94,
+        "unsigned_big_endian_sha256": "36d9b7760bacb4cbe202acbfbdd954cb6f7a0da7a452f2662134a2f5c8a84a2e"
+      },
+      "source_values": 13,
+      "width": {
+        "bits": 88,
+        "unsigned_big_endian_sha256": "b5cdb894bc41c24d0a3c8f74c29fa83624cd11cf51de04af408918b25707924b"
+      }
+    },
+    {
+      "all_rank_valuation_sha256": "217f79c7eff5258d4a8551e6825e0b8c724f1dbd6f9ad72966406f7f34a08e20",
+      "batch_constraints": 47080,
+      "compiled_ranks": 880,
+      "first_denominator_needed": {
+        "n": 126,
+        "width": 14776336,
+        "without_gcd": 59105344
+      },
+      "first_depth_needed": {
+        "n": 126,
+        "source_lcm": 7688,
+        "width": 14776336
+      },
+      "maximum": 1000,
+      "parameters": {
+        "cap": 8,
+        "d": 7,
+        "depth": 211,
+        "height": 1,
+        "log_degree": 9,
+        "power_of_two_exponent": 303840,
+        "prime_box_count": 32,
+        "rank_primes": [
+          2,
+          3,
+          5,
+          7,
+          11,
+          19,
+          41
+        ],
+        "source_ceiling": 31182789153672
+      },
+      "rule": "raw-p7",
+      "source_lcm": {
+        "bits": 107,
+        "unsigned_big_endian_sha256": "2ec0aa4350d6a9846884cc545404103785ba6297786b355865cd0eb06f056b5a"
+      },
+      "source_values": 5,
+      "width": {
+        "bits": 2524,
+        "unsigned_big_endian_sha256": "ca0f674261f498b58f82a629dee69b8b02950ac608eed62b85c279e56792a96c"
+      }
+    }
+  ],
+  "controls": {
+    "depth_counterexample": {
+      "n": 7,
+      "source_lcm": 2,
+      "width": 4
+    },
+    "gcd_counterexample": {
+      "n": 22,
+      "width": 896,
+      "without_gcd": 1792
+    },
+    "new_width_prime": {
+      "first_width": 5,
+      "rank_primes": [
+        2,
+        3
+      ]
+    },
+    "paid_prime_counterexample": {
+      "n_after": 15,
+      "n_before": 10,
+      "paid": {
+        "1": 2,
+        "3": 1
+      },
+      "source_total_after": 5,
+      "source_total_before": 4,
+      "targets": {
+        "2": 1,
+        "5": 1
+      }
+    },
+    "rejections": [
+      "paid rank reaches ambient",
+      "target rank one",
+      "noncontracting batch",
+      "zero batch count",
+      "nonprime breakpoint alphabet",
+      "omit paid breakpoint prime",
+      "confuse width primes with rank primes",
+      "drop recursive depth factor",
+      "omit gcd cancellation in exact recurrence",
+      "omit source multiplier"
+    ]
+  }
+}
diff --git a/research/chronological-width-growth/SOURCES.json b/research/chronological-width-growth/SOURCES.json
new file mode 100644
index 0000000000..d7c62ba457
--- /dev/null
+++ b/research/chronological-width-growth/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "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/chronological-batch-width/README.md",
+      "usage": "provenance",
+      "git_blob": "c85304a601f858774f425d5f3869ac0a6f85ec29",
+      "sha256": "0cf276c77016a98a0dabba822d27bb9cb94c0bf86ec353a16499fe85e6032c20"
+    },
+    {
+      "path": "research/chronological-batch-width/RESULT.json",
+      "usage": "provenance",
+      "git_blob": "2dd0cda6507acf81f72603151de62826a90a4fe5",
+      "sha256": "2750ea29f5d9d40aac5d97f1c4aa6482b5315003a9b50d1a21afae81b86d739a"
+    },
+    {
+      "path": "research/chronological-batch-width/batches.py",
+      "usage": "provenance",
+      "git_blob": "98feaef4156223829971089765bd483518c3b754",
+      "sha256": "73e7ab4a1925ee7d412d0f2b5d28b70f3a9e43e427c2ec6f6d89f193b84655ef"
+    },
+    {
+      "path": "research/chronological-batch-width/vendor/p7-RESULT.json",
+      "usage": "provenance",
+      "git_blob": "ebb30a9b3b94fb159a316350f7da57bde4a30c25",
+      "sha256": "9b814be97e3b45fcc28eafa8a65694897a7387f71a14d44796c6aadf303d7fab"
+    },
+    {
+      "path": "research/direct-mixed-flow/README.md",
+      "usage": "provenance",
+      "git_blob": "3be00f754b9ffa23e64b3eafe7706e3ac139993a",
+      "sha256": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8"
+    }
+  ]
+}
diff --git a/research/chronological-width-growth/TASK.json b/research/chronological-width-growth/TASK.json
new file mode 100644
index 0000000000..1a1d28aea7
--- /dev/null
+++ b/research/chronological-width-growth/TASK.json
@@ -0,0 +1,163 @@
+{
+  "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": "changed",
+  "actual_scope": "Prove an all-rank prime-valuation and multiplicative-breakpoint width bound for the fixed default-height chronological compiler of PR4436/4507.",
+  "scope_change_reason": "Taking the explicit unclaimed all-rank width handoff in Discussion 4503 and PR4507. The original independent-moment card concerns invoice coverage; this contribution bounds the existing chronological width sequence instead. PR4519 already checks its finite widths.",
+  "bottleneck_link": "Constructive productive width controls finite compiler resources. This supplies a quasipolynomial upper bound in place of the inherited exp(O(N log N)) envelope without changing normalized leaf cost or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "One fixed-rule default-height source-state and valuation theorem, exact checks on two toys and raw p7, then handoff. No changed-height application or native/physical expansion in this session.",
+  "outcome": "completed",
+  "evidence": "README.md all-rank proof; RESULT.json with 1074 compiled ranks, 49474 actual constraints, 832 cutoff cases, and 10 rejection controls. Universal conclusion is from the proof, not finite extrapolation. Registered normal/optimized and exported checks recorded at submission.",
+  "author": "Mihir Srivastava / mihir-s-05",
+  "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, checking and writing. No subagents, independently launched reviewer, human review or formal proof kernel.",
+  "open_questions": [
+    {
+      "question": "Can actual source valuations sharpen d+2 or the finite constants?",
+      "why_it_matters": "The present general bound is loose and gives no matching lower bound.",
+      "first_step": "Study valuations of S(mt) on actual transition points with contraction-depth multiplicities retained.",
+      "blocked_by": "No uniform valuation cancellation or matching lower-bound argument is established."
+    },
+    {
+      "question": "Does a source-state bound apply to PR4483 changed-height flow?",
+      "why_it_matters": "That flow has a stronger leaf-count theorem.",
+      "first_step": "Pin its height rule and inventories and enumerate every rank-dependent predicate before deriving a breakpoint bound.",
+      "blocked_by": "The new height policy and its source-state structure were not audited here."
+    }
+  ],
+  "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4503#discussioncomment-19117802",
+  "predecessors": [
+    {
+      "pr": 4436,
+      "commit": "56003680aee2871773de408e5f01cc5dd46b144c"
+    },
+    {
+      "pr": 4507,
+      "commit": "98b9f9e1b96940c0c405638afa974e378436fc55"
+    },
+    {
+      "pr": 4519,
+      "commit": "915b94b890cde927fba98e02db32ae2864f6bf05"
+    }
+  ],
+  "submission_refresh": {
+    "canonical_main": "f626db5c3a3d781d8f7695038776c621651f75e1",
+    "priority_revision": 7,
+    "checked_at_utc": "2026-10-22T08:08:17.094644+00:00",
+    "main_changed": false,
+    "local_tracked_notes": 5860,
+    "complete_local_head_inventory": true,
+    "open_prs": {
+      "fetched_at": "2026-10-22T08:07:00.575019+00:00",
+      "complete_pagination": true,
+      "records": 357
+    },
+    "discussions": {
+      "fetched_at": "2026-10-22T08:08:16.751958+00:00",
+      "complete_pagination": true,
+      "records": 3489
+    },
+    "scope": "Open PR bodies, Discussion records, all tracked top-level local notes. No exhaustive closed-PR or diff coverage. Nearest overlaps remain 4507/4519/4521; claim is unique in this text coverage."
+  },
+  "validation": {
+    "environment": "CPython 3.12.0, Windows AMD64, standard library only",
+    "registered_normal_and_optimized": "passed",
+    "committed_bytes": "passed for all 14 package files",
+    "official_export": "14-file integrity check and isolated optimized replay passed; Git unavailable, socket creation disabled, bytes unchanged",
+    "optional_source_history_preflight": "not run: the helper requires full Git history; this checkout is shallow; every pin is at the canonical-main base",
+    "isolated_copy": "passed with -I -O -B, Git absent from PATH, socket creation disabled, bytes preserved",
+    "external_controls": [
+      "changed-source rejected",
+      "changed-receipt rejected",
+      "omitted-paid-primes mutation rejected",
+      "collapsed-depth mutation rejected"
+    ],
+    "baseline_orientation": "stopped on sparse-omitted research/kappa-rebuild/CLAIM.json; not a PASS",
+    "not_checked": [
+      "full selected cold replay",
+      "native or physical admission",
+      "changed-height compiler applicability",
+      "formal proof kernel",
+      "independent human review",
+      "hosted CI"
+    ]
+  }
+}
diff --git a/research/chronological-width-growth/VENDOR.json b/research/chronological-width-growth/VENDOR.json
new file mode 100644
index 0000000000..662b54fbc4
--- /dev/null
+++ b/research/chronological-width-growth/VENDOR.json
@@ -0,0 +1,42 @@
+[
+  {
+    "path": "vendor/batches.py",
+    "source_path": "research/chronological-batch-width/batches.py",
+    "commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+    "git_blob": "98feaef4156223829971089765bd483518c3b754",
+    "sha256": "73e7ab4a1925ee7d412d0f2b5d28b70f3a9e43e427c2ec6f6d89f193b84655ef",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/f626db5c3a3d781d8f7695038776c621651f75e1/research/chronological-batch-width/batches.py"
+  },
+  {
+    "path": "vendor/batch-README.md",
+    "source_path": "research/chronological-batch-width/README.md",
+    "commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+    "git_blob": "c85304a601f858774f425d5f3869ac0a6f85ec29",
+    "sha256": "0cf276c77016a98a0dabba822d27bb9cb94c0bf86ec353a16499fe85e6032c20",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/f626db5c3a3d781d8f7695038776c621651f75e1/research/chronological-batch-width/README.md"
+  },
+  {
+    "path": "vendor/batch-RESULT.json",
+    "source_path": "research/chronological-batch-width/RESULT.json",
+    "commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+    "git_blob": "2dd0cda6507acf81f72603151de62826a90a4fe5",
+    "sha256": "2750ea29f5d9d40aac5d97f1c4aa6482b5315003a9b50d1a21afae81b86d739a",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/f626db5c3a3d781d8f7695038776c621651f75e1/research/chronological-batch-width/RESULT.json"
+  },
+  {
+    "path": "vendor/p7-RESULT.json",
+    "source_path": "research/chronological-batch-width/vendor/p7-RESULT.json",
+    "commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+    "git_blob": "ebb30a9b3b94fb159a316350f7da57bde4a30c25",
+    "sha256": "9b814be97e3b45fcc28eafa8a65694897a7387f71a14d44796c6aadf303d7fab",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/f626db5c3a3d781d8f7695038776c621651f75e1/research/chronological-batch-width/vendor/p7-RESULT.json"
+  },
+  {
+    "path": "vendor/flow-README.md",
+    "source_path": "research/direct-mixed-flow/README.md",
+    "commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+    "git_blob": "3be00f754b9ffa23e64b3eafe7706e3ac139993a",
+    "sha256": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/f626db5c3a3d781d8f7695038776c621651f75e1/research/direct-mixed-flow/README.md"
+  }
+]
diff --git a/research/chronological-width-growth/VERIFY.json b/research/chronological-width-growth/VERIFY.json
new file mode 100644
index 0000000000..f813873a1b
--- /dev/null
+++ b/research/chronological-width-growth/VERIFY.json
@@ -0,0 +1,28 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticate sources; recompute exact prime valuations, source-state intervals, contraction and width envelopes; compare all receipt fields; 10 rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same scientific checks with assertions disabled."
+    }
+  ]
+}
diff --git a/research/chronological-width-growth/growth.py b/research/chronological-width-growth/growth.py
new file mode 100644
index 0000000000..b60f0296dd
--- /dev/null
+++ b/research/chronological-width-growth/growth.py
@@ -0,0 +1,133 @@
+#!/usr/bin/env python3
+"""Integer envelopes for #4507's fixed-rule chronological widths.
+
+Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0.
+The universal result is proved in README.md; this module has no flow evaluator.
+"""
+from math import prod
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def factor(value):
+    require(type(value) is int and value >= 1, 'positive factor input')
+    result = {}
+    divisor = 2
+    while divisor * divisor <= value:
+        while value % divisor == 0:
+            result[divisor] = result.get(divisor, 0) + 1
+            value //= divisor
+        divisor = 3 if divisor == 2 else divisor + 2
+    if value > 1:
+        result[value] = result.get(value, 0) + 1
+    return result
+
+
+def valuation(value, prime):
+    require(value > 0 and prime >= 2, 'valuation domain')
+    result = 0
+    while value % prime == 0:
+        value //= prime
+        result += 1
+    return result
+
+
+def rank_primes(targets, paid):
+    require(bool(targets) and bool(paid), 'nonempty fixed rule')
+    require(all(type(k) is int and type(v) is int and v > 0
+                for hist in (targets, paid) for k, v in hist.items()), 'integer rule')
+    require(min(targets) >= 2 and min(paid) >= 1
+            and max(paid) < max(targets), 'strict rank contract')
+    return sorted({p for rank in targets.keys() | paid.keys() for p in factor(rank)})
+
+
+def smooth_numbers(primes, cap):
+    """All products of the supplied distinct primes up to cap, including 1."""
+    require(type(cap) is int and cap >= 1, 'positive cap')
+    require(primes == sorted(set(primes))
+            and all(factor(p) == {p: 1} for p in primes), 'distinct ordered primes')
+    values = [1]
+    for prime in primes:
+        following = []
+        for old in values:
+            value = old
+            while value <= cap:
+                following.append(value)
+                value *= prime
+        values = following
+    return sorted(values)
+
+
+def floor_log(base, value):
+    require(base >= 2 and value >= 1, 'integer logarithm domain')
+    count, power = 0, 1
+    while power <= value // base:
+        power *= base
+        count += 1
+    return count
+
+
+def depth_bound(n, m):
+    require(type(n) is int and n >= 0 and type(m) is int and m >= 2, 'depth domain')
+    depth = 0
+    while n >= m:
+        n = (m - 1) * n // m
+        depth += 1
+    return depth
+
+
+def check_descent(rows, n, m):
+    require(n >= m >= 2 and bool(rows), 'nonbase batches')
+    require(all(type(e) is int and 0 <= e <= (m-1)*n//m
+                and type(q) is int and q > 0 for e, q in rows),
+            'uniform rank contraction')
+
+
+def next_valuations(previous, rows, source_factors):
+    """Independent max-plus evaluation of v_p(S*lcm(B_e/gcd(B_e,q)))."""
+    repayment = {}
+    for e, count in rows:
+        require(0 <= e < len(previous) and count > 0, 'smaller positive batch')
+        for prime, exponent in previous[e].items():
+            need = max(0, exponent - valuation(count, prime))
+            repayment[prime] = max(repayment.get(prime, 0), need)
+    for prime, exponent in source_factors.items():
+        repayment[prime] = repayment.get(prime, 0) + exponent
+    return {p: e for p, e in repayment.items() if e}
+
+
+def from_valuations(powers):
+    return prod(p ** e for p, e in powers.items())
+
+
+def join_valuations(*maps):
+    result = {}
+    for powers in maps:
+        for prime, exponent in powers.items():
+            result[prime] = max(result.get(prime, 0), exponent)
+    return result
+
+
+def check_envelope(powers, source_lcm, depth):
+    require(all(e <= depth * source_lcm.get(p, 0) for p, e in powers.items()),
+            'source LCM depth envelope')
+
+
+def universal_parameters(targets, paid, maximum):
+    primes = rank_primes(targets, paid)
+    m, kmin = max(targets), min(targets)
+    require(maximum >= m, 'nonbase maximum')
+    cap = maximum // m
+    height = floor_log(kmin, cap)
+    W, P = sum(targets.values()), sum(paid.values())
+    ceiling = W * (W + P + 1) ** (height + 1)
+    grid = prod(1 + floor_log(p, cap) for p in primes)
+    depth = depth_bound(maximum, m)
+    ceiling_log2 = (ceiling - 1).bit_length()
+    return {'rank_primes': primes, 'd': len(primes), 'log_degree': len(primes)+2,
+            'cap': cap, 'height': height, 'source_ceiling': ceiling,
+            'prime_box_count': grid, 'depth': depth,
+            'power_of_two_exponent': depth * grid * ceiling_log2}
diff --git a/research/chronological-width-growth/vendor/batch-README.md b/research/chronological-width-growth/vendor/batch-README.md
new file mode 100644
index 0000000000..c85304a601
--- /dev/null
+++ b/research/chronological-width-growth/vendor/batch-README.md
@@ -0,0 +1,265 @@
+# Chronological batch divisibility in the direct mixed compiler
+
+**Result:** the fixed chronological flow in [PR #4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436)
+admits a smaller, explicitly computable productive width. For prescribed smaller
+supplier widths, the formula below gives the **least common replication factor
+under the stated batching policy**. A histogram-only relaxation can fail: an
+actual rank-12 toy flow accepts multiplier 175 in aggregate but needs 700 at
+one parent-round cut.
+
+At raw p7 rank 1,000, the new productive width has **2,524 bits**, versus
+**17,504 bits** for #4436's nested construction. The old width is an integer
+multiple of the new one; the reduction factor has 14,981 bits. The normalized
+rank-one leaf cost is exactly unchanged at every checked rank. This is a
+conditional batching lemma and finite accounting result, **with no new kappa**.
+It does not establish a smaller asymptotic width order or a practical algorithm.
+
+## 1. Source and the missing question
+
+The audited source is zxv's #4436 at
+`56003680aee2871773de408e5f01cc5dd46b144c`, sections 2–3 and open question 3.
+It realizes Sussman's integer lockstep construction with overlapping ranks,
+pays unmatched exits, and chooses `a_n = B_(n-1)`, `B_n = a_n S_n` so every
+smaller width divides the replication factor. Its original LCM freedom is
+explicit predecessor work. The addition here is the exact batch-by-batch
+gcd/LCM criterion, its chronological counterexample and a source-bound finite
+construction using it recursively.
+
+All target ranks are at least 2; `m` is their maximum; every paid rank is
+positive and below `m`. Keep the source's default height
+`G = floor(log_(k_min)(floor(n/m)))`, complete source census, native word and
+parent-round order. Only the replication factor changes. The input profile
+is the frozen p7 native invoice, not a new audit of its physical correctness.
+`VENDOR.json` binds four exact source files by URL, commit, Git blob and SHA256.
+They are retained locally for Git-free replay; no unmerged Git object or
+network is needed by the scientific verifier.
+
+The all-column, arbitrary-input, spectator, whole-job adapter, routing and
+owned-state contracts of the source remain hypotheses. Equal ranks alone
+do not implement a physical adapter. Native work and physical routing remain
+paid under those contracts.
+
+## 2. Batching policy and least replication factor
+
+Let `S_s` be the source-job count at rank `s`, and `S = sum_s S_s` the total
+source count at ambient rank `n`. The prescribed completed program of each
+smaller rank `e` has productive width `B_e > 0`. Put `B_0 = 1` and give a
+zero-rank complement zero cost.
+
+The allowed batching policy is:
+
+1. Before the flow, group **all source complements** by rank `n-s`. These
+   act on distinct original arrays before any enters the chronological flow.
+   Each group has `a S_s` arrays after common replication by `a`.
+2. At **one parent-round cut in one path class**, group equal-rank unmatched
+   exits across that class's units. Complete every group before returning
+   from that cut. A cut with `q` exits of rank `e` has `a q` arrays.
+   Separate paths or paid positions are separate cuts, even when their
+   ranks and multipliers agree.
+3. Match and resume native calls exactly as in #4436. Replicated copies of
+   a given class run in lockstep. No unfinished job is pooled with a later
+   cut; no extra productive input is credited.
+
+Record batches `(e,q)`: complements have `(n-s,S_s)` and exits have their
+**per-cut** counts. For this finite list define
+
+```text
+a_n = lcm over batches (e,q) of B_e / gcd(B_e,q),
+B_n = S * a_n.
+```
+
+**Lemma.** These widths are valid under the inherited source contracts, and
+`a_n` is the least positive replication factor for this policy and the
+prescribed smaller widths.
+
+**Proof.** A whole rank-`e` supplier invocation handles `B_e` arrays.
+Partitioning `a q` arrays into whole invocations is possible exactly when
+`B_e | a q`. With `g = gcd(B_e,q)`, coprimality of `B_e/g` and `q/g`
+makes this equivalent to `(B_e/g) | a`. All conditions hold exactly when
+their LCM divides `a`, proving necessity, sufficiency and minimality.
+Every recursive rank is below `n`: the source proves `0 < s <= n` and
+`0 < e < n`. Strong induction therefore supplies every invoked program.
+Complements run first; every exit finishes before its parent resumes.
+The same disjoint inputs, owners, adapters and completed endpoints as
+the source give a full rank-`n` transform on `a_n S` productive arrays.
+No fractional invocation is used. QED.
+
+Minimality is **local to this policy and the chosen smaller library**.
+It does not optimize earlier libraries jointly, permit fractional suppliers,
+vary replication independently between classes, or optimize every schedule
+and physical implementation. New widths need not be nested or monotone.
+
+## 3. Counting the chronological cuts
+
+`batches.py` is a new multiplicative-polynomial implementation. Let `F_h(c)`
+count ordered target words of length `h` with product `c`, with `W_k`
+distinguishable copies of target rank `k`. Then
+
+```text
+F_0(1) = 1,
+F_h(c) = sum_k W_k F_(h-1)(c/k),
+```
+
+where noninteger quotients contribute zero. This equals the sum of the
+source's multinomial counts over exponent vectors with the same product.
+Product collisions are summed. Only products at most `floor(n/m)` need
+storage, since all target factors are at least 2.
+
+At depth `d` and path multiplier `rho`, a present parent supplies
+`F_(G-d)(c)` units when `m rho c <= n`. At a rank-`r` paid position the
+child demands the subset of Pascal terms with `m rho r c/k <= n`. For
+a present parent, demand is at most supply. A positive difference is the
+per-cut batch at rank `rho r c`; an absent parent is supplied by new sources.
+At depth `G`, each present class contains one unit, so each paid position
+has a **single** exit before replication.
+
+Equal-`rho` paths may be compressed for counting. The stored `copies` field
+counts occurrences, including repeated paid positions. It multiplies the
+total exit and cost census but **never the per-cut batch size** in the LCM.
+The checker independently enumerates literal ordered target words and paid
+positions in 101 fixtures, comparing complete source/exit counts and the
+multiset of cuts. Target ranks 2, 4 and 8 exercise product collisions.
+
+## 4. Cost preservation and inherited width bound
+
+Write `P_e` for the complete rank-one leaf count of a width-`B_e` supplier.
+Complement groups contribute `sum_s (a S_s/B_(n-s)) P_(n-s)` leaves;
+exit groups contribute `sum_cuts (a q/B_e) P_e`, with all occurrences
+retained. Dividing by `B_n = a S` gives the predecessor's exact recurrence:
+
+```text
+L(n) = [sum_s S_s L(n-s) + sum_e E_e L(e)] / S.
+```
+
+The factor `a` cancels. With the same base `B_e=1, P_e=e` for `e<m`,
+induction proves identical normalized leaf costs at every rank. Batching
+therefore supplies no new exponent saving.
+
+For the all-rank width comparison, suppose `B'_e | B_e` at every smaller
+rank, where unprimed widths are the old nested construction. Each modulus
+`B'_e/gcd(B'_e,q)` divides `B_e`, which divides `B_(n-1)` by old nesting.
+Their LCM `a'_n` divides `B_(n-1)`. Multiplying by the same `S` gives
+`B'_n | B_n`. Equal bases complete the induction. The new construction
+inherits `exp(O(N log N))`; finite reductions do not prove a better order.
+
+## 5. Counterexample to pooling across cuts
+
+Use the source equality fixture `targets = {2:4, 3:1}`,
+`paid = {1:6, 2:2}` at `n=12`. The new recursive widths through rank 11 are
+
+```text
+e:    0  1  2  3  4   5    6    7    8    9   10    11
+B_e:  1  1  1  5  5  25  140  140  700  625  875  4375
+```
+
+Sources are `{6:60, 8:64, 9:6, 12:28}`; aggregate exits are
+`{1:216, 2:216, 4:72, 8:8}`. Clearing complements and aggregate exits gives
+multiplier **175** and every aggregate division is integral. But eight
+separate rank-8 leaf cuts each contain one job: depth 2, path multiplier 4,
+final paid rank 2. Each needs `700 | a`. At `a=175`, the individual batch
+has only 175 arrays; the parent cannot complete it with the prescribed
+width-700 supplier while waiting for other cuts. The least valid multiplier
+is **700**, giving `B_12=110600`.
+
+This refutes this specific pooled divisibility relaxation. The original
+#4436 nested construction is valid and is not alleged to contain this bug.
+A different schedule or smaller-rank library needs its own argument.
+
+## 6. Exact finite evidence
+
+| Fixed flow | Final rank | Nested width bits | New width bits | Ranks with strict reduction |
+| --- | ---: | ---: | ---: | ---: |
+| `{2:1,5:1} <- {1:2,4:1}` | 100 | 433 | 42 | 95 of 96 |
+| `{2:4,3:1} <- {1:6,2:2}` | 100 | 1,002 | 88 | 97 of 98 |
+| Raw p7 | 1,000 | 17,504 | 2,524 | 879 of 880 |
+
+The p7 reduction factor lies in `[2^14980,2^14981)`. These are bit lengths
+of enormous integer widths, not physical runtime measurements. `RESULT.json`
+records unsigned-big-endian integer hashes, all-rank witness hashes and the
+full small counterexample. Standard-library checks cover:
+
+- all nine frozen #4436 source/exit/column/matching receipts;
+- 101 independent literal cut fixtures and 2,304 brute-force multiplier cases;
+- 1,074 nonbase compiled ranks with **49,474** batch constraints;
+- integral batches, divisibility into old width, and unchanged normalized
+  leaf costs at every rank, also against a separate rational recurrence;
+- frozen nested width and leaf-count hashes for both toys and raw p7;
+- twelve rejection controls: pooling across cuts, merging repeated paths
+  and paid positions, reducing replication, deleting premature exits and
+  malformed rank/count contracts.
+
+No predecessor evaluator is imported or executed. `vendor/flow.py` is a
+source reference only. Frozen receipt matches authenticate the comparison;
+they do not independently validate the native supplier.
+
+## 7. Reproduction, coordination and limitations
+
+Python 3.12, no dependencies, from the repository root:
+
+```sh
+python -B scripts/research_package.py --package research/chronological-batch-width --check-only
+python -B scripts/research_package.py --package research/chronological-batch-width
+python -B scripts/check_research_commit.py --package research/chronological-batch-width --check-source-history
+```
+
+A Git-free copy of this package can run `python -I -O -B verify.py`.
+`--write` regenerates the receipt for authoring; default replay compares
+the fresh result with the committed receipt. Explicit exceptions keep all
+checks active in optimized Python.
+
+Local validation used CPython 3.12.0 on Windows. The metadata/pin check,
+registered ordinary and optimized replays, and a fresh Git-free isolated
+optimized replay passed. In that separate copy, altered source bytes and
+an altered receipt both rejected. Two code mutations also rejected: pooling
+repeated chronological calls into one batch, and omitting their repeated
+leaf cost. These checks are author-side evidence, not independent review.
+
+Base: canonical main `2a13eb1827784206202db90e5dc8327cf8a250db`, priority
+revision 7. The `independent-moment` card is explicitly changed to
+chronological batching and width, following #4436's open question 3.
+[Discussion #4503](https://github.com/CrocSwap/integer-mult-bounds/discussions/4503)
+is canonical. Initial overlap covered all 5,731 tracked local note paths,
+354 open PRs, 3,379 Discussion records and 3,787 closed PRs, with complete
+reported pagination at 02:29–02:31 UTC on October 22. This is bounded text
+coverage, not exhaustive diff review or a novelty certificate.
+
+Submission refresh: canonical main was unchanged. The final snapshot covered
+355 open PRs, 3,381 Discussion records and 3,787 closed PRs at 02:39–02:41
+UTC, with complete reported pagination and all tracked local notes searched.
+
+#4456 recounts the flow; #4476 checks its original nested widths and routing.
+This adds the least per-cut multiplier and smaller actual width witnesses.
+#4467's default-height analysis and #4483's changed-height convergence
+theorem are separate. No claim is made that the old exponent question
+remains generally open after #4483, whose compiler is not audited here.
+
+The historical baseline orientation command stopped on the sparse-omitted
+`research/kappa-rebuild/CLAIM.json`; it is not claimed as passing. No selected
+cold replay, native/physical admission, formal-kernel proof, independent
+human review or new kappa is claimed. The selected frontier is unchanged.
+
+## Open next questions
+
+1. **Can the width sequence be bounded more sharply in all ranks?** This
+   decides whether the finite improvement changes growth order. Start with
+   prime valuations of `B_e/gcd(B_e,q)` on actual chronological cuts. A
+   uniform valuation argument and global optimization over earlier libraries
+   remain unresolved.
+2. **Does the policy reduce widths for #4483's changed-height flow?** Its
+   smaller ambient-rank result motivates this application. First pin its
+   cut inventories and verify rank descent and batching boundaries. Only
+   #4436's default flow is instantiated here; numerical transfer is unproved.
+
+## Credit
+
+Jacob Alan Sussman supplied the multinomial integer compiler and original
+unseparated question. zxv supplied #4436's chronological overlapping flow,
+nested width theorem and source export, building on #4359's native bridge.
+Cinna Davis / 1337isnot1337 supplied #4416's p7 construction; native lineage
+remains credited in the frozen receipt and predecessor note. Ryanson
+Jonathan / pinterbanget supplied #4456's independent flow check and #4476's
+width/routing evidence. Those results are not new here.
+
+Prepared for **Mihir Srivastava / mihir-s-05 with substantial OpenAI Codex
+assistance** in derivation, implementation, verification and writing.
+No subagents. New material is Apache-2.0; retained sources keep their notices.
diff --git a/research/chronological-width-growth/vendor/batch-RESULT.json b/research/chronological-width-growth/vendor/batch-RESULT.json
new file mode 100644
index 0000000000..2dd0cda650
--- /dev/null
+++ b/research/chronological-width-growth/vendor/batch-RESULT.json
@@ -0,0 +1,166 @@
+{
+  "brute_force_minimality_cases": 2304,
+  "chronology_counterexample": {
+    "aggregate_exits": {
+      "1": 216,
+      "2": 216,
+      "4": 72,
+      "8": 8
+    },
+    "aggregate_sources": {
+      "12": 28,
+      "6": 60,
+      "8": 64,
+      "9": 6
+    },
+    "child_width": 700,
+    "chronological_multiplier": 700,
+    "cut": {
+      "copies": 8,
+      "count": 1,
+      "depth": 2,
+      "paid_rank": 2,
+      "rank": 8,
+      "rho": 4
+    },
+    "n": 12,
+    "pooled_multiplier": 175,
+    "repeated_cut_multiplier": 175,
+    "widths_through_12": [
+      1,
+      1,
+      1,
+      5,
+      5,
+      25,
+      140,
+      140,
+      700,
+      625,
+      875,
+      4375,
+      110600
+    ]
+  },
+  "claim_type": "conditional batching lemma and exact finite accounting",
+  "compilations": [
+    {
+      "all_rank_receipt_sha256": "055b2ea1bf5acd0ad272ab635fd63e85d3ce2999478d759e526a25110fdefbeb",
+      "batch_constraints": 1045,
+      "compiled_ranks": 96,
+      "first_pooled_failure": null,
+      "leaves": {
+        "bits": 48,
+        "unsigned_big_endian_sha256": "c9d453fd813fb29900634e22ca2b8410ac5686f3a6e296ddbc3f65ad1cd3c465"
+      },
+      "maximum": 100,
+      "nested_width": {
+        "bits": 433,
+        "unsigned_big_endian_sha256": "35f12bcc6000b703565e2f120e8077641f744909e8ec163921775b2b0c139254"
+      },
+      "new_width_divides_nested_at_every_rank": true,
+      "normalized_leaf_cost_unchanged": true,
+      "rule": "strict-overlap",
+      "strict_width_gains": 95,
+      "width": {
+        "bits": 42,
+        "unsigned_big_endian_sha256": "a61817c96be89d11dec54f0b0ef5da6a27a6bea836b240cb170c488a1123c77c"
+      },
+      "width_reduction_factor": {
+        "bits": 392,
+        "unsigned_big_endian_sha256": "b541c94d850e2956af1018e1de0c74b23b9213930064a476fe7b3957924e751a"
+      }
+    },
+    {
+      "all_rank_receipt_sha256": "2aed41bf23db7277f992de0a8f477ff23a0249c41085a15ee199e9c0eaaf961c",
+      "batch_constraints": 1349,
+      "compiled_ranks": 98,
+      "first_pooled_failure": {
+        "child_width": 700,
+        "chronological_multiplier": 700,
+        "cut": {
+          "copies": 8,
+          "count": 1,
+          "depth": 2,
+          "paid_rank": 2,
+          "rank": 8,
+          "rho": 4
+        },
+        "n": 12,
+        "pooled_multiplier": 175
+      },
+      "leaves": {
+        "bits": 94,
+        "unsigned_big_endian_sha256": "c7f005e5c0009d618eda5abc42bf07177df79485b72251ad081209322a7a24dd"
+      },
+      "maximum": 100,
+      "nested_width": {
+        "bits": 1002,
+        "unsigned_big_endian_sha256": "398043f007044ec4c1ba14eda89bf66b48733ce7a22bb855a3bc17a4665b5952"
+      },
+      "new_width_divides_nested_at_every_rank": true,
+      "normalized_leaf_cost_unchanged": true,
+      "rule": "source-open-equality",
+      "strict_width_gains": 97,
+      "width": {
+        "bits": 88,
+        "unsigned_big_endian_sha256": "b5cdb894bc41c24d0a3c8f74c29fa83624cd11cf51de04af408918b25707924b"
+      },
+      "width_reduction_factor": {
+        "bits": 915,
+        "unsigned_big_endian_sha256": "e9003186d9235c2584d11eed5bf0a7992a90e8d350065bd1ed10dc14cadeef5d"
+      }
+    },
+    {
+      "all_rank_receipt_sha256": "415c7c449a41ca80768f71a9fde03b3b6fe73e309046ece0ae51d61d411da930",
+      "batch_constraints": 47080,
+      "compiled_ranks": 880,
+      "first_pooled_failure": null,
+      "leaves": {
+        "bits": 2534,
+        "unsigned_big_endian_sha256": "a39d58e845fbaf80f347345e6435afbdd4d24ebfb5dc82a235d2e1885ec12d5a"
+      },
+      "maximum": 1000,
+      "nested_width": {
+        "bits": 17504,
+        "unsigned_big_endian_sha256": "49727d4435d62a4a84b79cf2451d374a5bb98234cbe460ec0b0ef3da77c8c9e6"
+      },
+      "new_width_divides_nested_at_every_rank": true,
+      "normalized_leaf_cost_unchanged": true,
+      "rule": "raw-p7",
+      "strict_width_gains": 879,
+      "width": {
+        "bits": 2524,
+        "unsigned_big_endian_sha256": "ca0f674261f498b58f82a629dee69b8b02950ac608eed62b85c279e56792a96c"
+      },
+      "width_reduction_factor": {
+        "bits": 14981,
+        "unsigned_big_endian_sha256": "a0c23802a822d865510e67a12ee0d788c4f719b69c831c3e1178c51daad570b0"
+      }
+    }
+  ],
+  "frozen_flows_matched": 9,
+  "independent_literal_cut_fixtures": 101,
+  "no_new_kappa": true,
+  "rejected_controls": [
+    "pooled exit multiplier at actual cut",
+    "drop a factor from least multiplier",
+    "zero replication",
+    "zero supplier width",
+    "zero job count",
+    "negative job count",
+    "boolean job count",
+    "future rank",
+    "paid rank equal to ambient",
+    "noninteger target multiplicity",
+    "delete premature exits",
+    "merge repeated parent paths and paid positions"
+  ],
+  "schema": "chronological-batch-width/v1",
+  "source_sha256": {
+    "vendor/direct-flow-README.md": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8",
+    "vendor/direct-flow-RESULT.json": "da04256f6f2ef61530f1d642ff1137a2274fd642782a72ef4bf3f1b65395c270",
+    "vendor/flow.py": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a",
+    "vendor/p7-RESULT.json": "9b814be97e3b45fcc28eafa8a65694897a7387f71a14d44796c6aadf303d7fab"
+  }
+}
diff --git a/research/chronological-width-growth/vendor/batches.py b/research/chronological-width-growth/vendor/batches.py
new file mode 100644
index 0000000000..98feaef415
--- /dev/null
+++ b/research/chronological-width-growth/vendor/batches.py
@@ -0,0 +1,181 @@
+#!/usr/bin/env python3
+"""Exact batching for the fixed #4436 direct flow; no native admission.
+
+Independent multiplicative-polynomial implementation of the flow's counts.
+The chronological/Pascal construction is due to Sussman and zxv.
+Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+from collections import Counter
+from math import gcd, lcm
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def validate(targets, paid, n):
+    for histogram in (targets, paid):
+        require(bool(histogram), 'nonempty histogram')
+        require(all(type(k) is int and type(v) is int and k > 0 and v > 0
+                    for k, v in histogram.items()), 'positive integer histogram')
+    require(type(n) is int and 2 <= min(targets) <= max(targets) <= n
+            and max(paid) < max(targets), 'strict rank contract')
+
+
+def polynomial_layers(targets, cap, height):
+    """Coefficient of each product in an ordered target word of length h."""
+    layers = [{1: 1}]
+    for _ in range(height):
+        following = Counter()
+        for c, count in layers[-1].items():
+            for k, multiplicity in targets.items():
+                if c*k <= cap:
+                    following[c*k] += count*multiplicity
+        layers.append(dict(following))
+    return layers
+
+
+def direct_flow(targets, paid, n):
+    validate(targets, paid, n)
+    m, kmin = max(targets), min(targets)
+    cap, height, least = n//m, 0, 1
+    while least*kmin <= cap:
+        height += 1
+        least *= kmin
+    layers = polynomial_layers(targets, cap, height)
+
+    def units(depth, rho):
+        return {c: q for c, q in layers[height-depth].items() if rho*c <= cap}
+
+    def demand(depth, rho):
+        result = Counter()
+        for c, q in units(depth, rho).items():
+            for k, w in targets.items():
+                result[c*k] += w*q
+        return result
+
+    sources = Counter(demand(0, 1))
+    exits, boundary = Counter(), Counter()
+    cuts = []
+    paths = {1: 1}
+    unit_count = column_mass = matched = 0
+    for depth in range(height+1):
+        next_paths = Counter()
+        for rho, path_count in sorted(paths.items()):
+            supply = units(depth, rho)
+            unit_count += path_count*sum(supply.values())
+            column_mass += path_count*sum(rho*c*q for c, q in supply.items())
+            for r, occurrences in sorted(paid.items()):
+                child_rho = rho*r
+                copies = path_count*occurrences
+                if depth == height:
+                    local = Counter({child_rho: supply.get(1, 0)})
+                else:
+                    child = demand(depth+1, child_rho)
+                    local = Counter()
+                    for c in supply.keys() | child.keys():
+                        have, want = supply.get(c, 0), child.get(c, 0)
+                        if have:
+                            require(want <= have, 'Pascal containment')
+                        matched += copies*min(have, want)
+                        if have > want:
+                            local[child_rho*c] += have-want
+                            boundary[child_rho*c] += copies*(have-want)
+                        elif want > have:
+                            sources[child_rho*c] += copies*(want-have)
+                    if child_rho <= cap:
+                        next_paths[child_rho] += copies
+                for e, q in sorted(local.items()):
+                    if q:
+                        # copies counts separate chronological calls. It MUST
+                        # NOT multiply q in the divisibility constraint.
+                        cuts.append({'depth': depth, 'rho': rho, 'paid_rank': r,
+                                     'rank': e, 'count': q, 'copies': copies})
+                        exits[e] += copies*q
+        paths = next_paths
+    sources, exits, boundary = +sources, +exits, +boundary
+    require(sources and all(n < m*s <= m*n for s in sources), 'source bounds')
+    require(all(0 < e < n for e in exits), 'strict exit descent')
+    mass = lambda h: sum(k*q for k, q in h.items())
+    require(mass(sources)-mass(exits) == (mass(targets)-mass(paid))*column_mass,
+            'rank-one conservation')
+    return {'sources': sources, 'exits': exits, 'boundary_exits': boundary,
+            'cuts': cuts, 'height': height, 'units': unit_count,
+            'column_mass': column_mass, 'matched_jobs': matched}
+
+
+def requirements(flow, n, pooled_exits=False):
+    """Rank/count batches: all complements first, then one exit per cut."""
+    rows = [(n-s, count) for s, count in flow['sources'].items()]
+    if pooled_exits:
+        rows += list(flow['exits'].items())
+    else:
+        rows += [(c['rank'], c['count']) for c in flow['cuts']]
+    return rows
+
+
+def multiplier(widths, rows):
+    result = 1
+    for rank, count in rows:
+        require(type(rank) is int and 0 <= rank < len(widths), 'smaller rank')
+        require(type(count) is int and count > 0, 'positive batch count')
+        width = widths[rank]
+        require(type(width) is int and width > 0, 'positive supplier width')
+        result = lcm(result, width//gcd(width, count))
+    return result
+
+
+def check_batches(widths, rows, replication):
+    require(type(replication) is int and replication > 0, 'positive replication')
+    require(all(replication*q % widths[r] == 0 for r, q in rows),
+            'whole chronological batch')
+
+
+def compile_widths(targets, paid, maximum):
+    """Compare least cut-feasible widths with #4436's nested construction."""
+    m = max(targets)
+    widths, nested = [1]*m, [1]*m
+    leaves, old_leaves = list(range(m)), list(range(m))
+    counters = {'compiled_ranks': 0, 'batch_constraints': 0, 'strict_width_gains': 0}
+    first_pooled_failure = None
+    rows_out = []
+    prior_cap, flow = None, None
+    for n in range(m, maximum+1):
+        if n//m != prior_cap:
+            flow = direct_flow(targets, paid, n)
+            prior_cap = n//m
+        rows = requirements(flow, n)
+        a = multiplier(widths, rows)
+        check_batches(widths, rows, a)
+        source_count = sum(flow['sources'].values())
+        width, old_width = a*source_count, nested[-1]*source_count
+        require(old_width % width == 0, 'new width divides old nested width')
+        # The exact same cut constraints are enforced for the old construction.
+        check_batches(nested, rows, nested[-1])
+        # rows contains one representative of each repeated exit cut; leaf
+        # accounting must retain all of those repetitions.
+        total = sum(a*q//widths[n-s]*leaves[n-s] for s, q in flow['sources'].items())
+        total += sum(a*c['count']//widths[c['rank']]*leaves[c['rank']]*c['copies']
+                     for c in flow['cuts'])
+        old_a = nested[-1]
+        old_total = sum(old_a*q//nested[n-s]*old_leaves[n-s]
+                        for s, q in flow['sources'].items())
+        old_total += sum(old_a*c['count']//nested[c['rank']]*old_leaves[c['rank']]*c['copies']
+                         for c in flow['cuts'])
+        require(total*old_width == old_total*width, 'unchanged normalized leaf cost')
+        pooled_a = multiplier(widths, requirements(flow, n, pooled_exits=True))
+        if pooled_a < a and first_pooled_failure is None:
+            bad = next(c for c in flow['cuts'] if pooled_a*c['count'] % widths[c['rank']])
+            first_pooled_failure = {'n': n, 'pooled_multiplier': pooled_a,
+                                    'chronological_multiplier': a,
+                                    'cut': bad, 'child_width': widths[bad['rank']]}
+        widths.append(width); nested.append(old_width)
+        leaves.append(total); old_leaves.append(old_total)
+        counters['compiled_ranks'] += 1
+        counters['batch_constraints'] += len(rows)
+        counters['strict_width_gains'] += width < old_width
+        rows_out.append((n, a, width, total))
+    return {'widths': widths, 'nested_widths': nested, 'leaves': leaves,
+            'nested_leaves': old_leaves, 'counters': counters,
+            'first_pooled_failure': first_pooled_failure, 'rows': rows_out}
diff --git a/research/chronological-width-growth/vendor/flow-README.md b/research/chronological-width-growth/vendor/flow-README.md
new file mode 100644
index 0000000000..3be00f754b
--- /dev/null
+++ b/research/chronological-width-growth/vendor/flow-README.md
@@ -0,0 +1,496 @@
+# Direct mixed flow and explicit compiler size: a partial research checkpoint
+
+**Publication authorized by the user on October 21, 2026.** This is a partial
+compiler/resource checkpoint; the direct exponent gate remains open.
+
+The target is a structural successor to
+[PR4433](https://github.com/CrocSwap/integer-mult-bounds/pull/4433): remove the
+tensor/padding step needed by overlapping ranks and control the complete
+finite compiler's size. The user requested a significance target twice the
+previous contribution. That is an ambitious scope target, not a numerical
+measurement or a claim that it has been achieved.
+
+Two results are established under the source native-word hypotheses:
+
+1. A **finite chronological integer flow** works when paid ranks overlap
+   target ranks, provided `max paid < ambient`. It retains and pays every
+   unmatched job as an exit. All recursive ranks decrease. This gives a
+   finite uniform compiler, **without a proved near-root saving**.
+2. Choosing **nested divisible widths** gives `B_N <= exp(O(N log N))`.
+   Exact rank-one accounting also bounds raw instances, owned centers,
+   routing slots and the source finite-constant envelopes. This batching
+   choice preserves the normalized leaf cost and therefore applies to the
+   already supported PR4433 supplier.
+
+The main exponent target remains open. Exact compilation at rank 1,000 on
+the raw p7 profile fails the desired saving. That finite failure is not an
+asymptotic obstruction, and it does not invalidate PR4433's separated recipe.
+No new κ, selected frontier, native admission or physical runtime is claimed.
+
+## 1. Source boundary and decision
+
+The starting point is Jacob Alan Sussman's multinomial lockstep construction,
+retained by PR4359. Its separated proof requires `r_max < k_min` so every
+parent output is consumed. PR4416 and PR4433 instead repair the raw p7
+overlap by chronological products, paid completion and splitting.
+
+Retain the four native hypotheses of
+[FINITE-PRECOMPILATION.md](vendor/FINITE-PRECOMPILATION.md): a correct
+all-column arbitrary-input word, disjoint splitting with complete spectators,
+permitted and priced whole-job adapters, and finite-program closure with
+owned initialization/erasure. Equal rank alone does not supply an adapter.
+Changed finite combinatorics do not independently admit those hypotheses.
+
+**Continue, with two separate gates.** The finite-flow gate is now proved and
+checked. The exponent gate requires a new uniform estimate on the complete
+complement-plus-exit recurrence. Do not expand a search solely because a
+moment root is favorable. The size theorem is useful independently, since
+the predecessor leaves productive width and owned-instance counts implicit.
+
+| Obligation | Evidence / remaining work |
+| --- | --- |
+| Integer matching with overlapping ranks | Proved below; literal and merged replays agree |
+| Chronological return and strictly smaller exits | Proved under `r_max < m`; no cross-round matching |
+| Source complements and full uniform output | Source integer-batch induction, with nested divisible widths |
+| Direct near-root saving | **Open**; rank 1,000 fails; no global conclusion |
+| Productive width, rank-one leaves, raw instances, owned centers | Explicit bounds below, with exact finite controls |
+| Routing slots, encoded records and source finite-constant envelopes | Counted below in the stated grammar; physical implementations retain their own tariffs |
+| Native all-column, physical, analytic, precision and recovery premises | Inherited; no full replay or new admission |
+
+## 2. Partially matched integer lockstep flow
+
+Let positive integer target multiplicities be W_k, chronological paid rounds
+have ranks r_j, and let
+
+```
+2 <= k_min <= m=max(k),   1 <= r_max < m.
+```
+
+The paid word may have `r_max >= k_min`. At a fixed integer top rank n>=m,
+put
+
+```
+c(a) = product_k k^a_k,
+u(a) = multinomial(|a|;a) product_k W_k^a_k,
+R(rho) = {a : m*rho*c(a) <= n},
+G = floor(log_(k_min)(floor(n/m))).
+```
+
+For every paid-round path s of length d<=G with multiplier rho_s, instantiate
+u(a) units at column rho_s*c(a), for every point a in R(rho_s) of degree
+G−d. This is the source class construction. For a parent class with
+multiplier rho, its rank-r round supplies u(b) jobs at point b when b is
+present. The child demand at that point is
+
+```
+D(b) = sum over eligible (b−e_k) of W_k*u(b−e_k).
+```
+
+The complete Pascal sum is u(b). Therefore:
+
+- If the parent point b exists, `0 <= D(b) <= u(b)`. Route D(b) of the
+  **whole** issued jobs to the child. Complete the remaining u(b)−D(b)
+  jobs as paid exits, at their actual rank `e=r*rho*c(b)`.
+- If the parent point is absent, supply the child demand with new distinct
+  top input arrays. These are source jobs, not copies of issued data.
+- At depth G, every point has degree zero; all paid jobs are exits.
+
+No fractional jobs, cloned productive inputs or uncharged discarded requests
+are introduced. Within each point, choose a fixed enumeration of parent
+jobs and target slots and match their first D(b) elements. The rest have
+explicit endpoints and remain on their actual owners.
+
+### Sources and exits
+
+At the root, every demanded point has degree G+1, so it is outside R(1).
+Its rank s is in `(n/m,n]`. A non-root source has no parent point, hence
+`m*rho_parent*c(b)>n`; its rank is `r*rho_parent*c(b)>r*n/m>=n/m`.
+Its eligible child target ensures s<=n. Thus every source is a positive
+job in `(n/m,n]`.
+
+Every exit belongs to an actual parent unit, so
+
+```
+e <= r_max*n/m < n.
+```
+
+This holds for the new premature exits as well as leaf exits. A premature
+exit has at least one omitted Pascal term, with
+`m*r*rho*c(b)/k > n`; consequently `e > k_min*n/m`. These are large exits
+near the upper boundary. They cannot be assigned the old bound
+`r_max*(n/m)^theta` with theta<1. That lost estimate is the exponent issue.
+
+### Chronology and arbitrary inputs
+
+Run all scalar steps of a class in their specified order. At paid position
+j, issue that position for every unit, partition its whole issued jobs into
+matched and unmatched slots, finish all unmatched exits and the entire child
+class, restore adapters, and only then resume position j+1. The child takes
+incoming jobs from this one parent round plus its new top sources. It never
+waits for a later round of a suspended parent. The finite class depth is G;
+all complement and exit calls have rank below n, so their uniform programs
+are already available by strong induction.
+
+Distinct slots in one class have distinct physical fields. Routing fewer
+parent slots than the original full-Pascal construction preserves this
+property. Arbitrary-input native correctness permits correlated values,
+including current owned-center contents; it does not permit field aliasing
+or extra productive credit. Each unit has its own owned identities and
+retains them until its word clears them. These requirements are unchanged.
+
+### Exact potential and count identities
+
+Let S_s and E_e be integer source and exit inventories, U the unit count,
+and Qcol the sum of the units' positive integer column multiplicities.
+Cancellation of matched jobs gives, exactly at rank one,
+
+```
+sum_s S_s*s − sum_e E_e*e = Delta * Qcol,
+Delta = sum_k W_k*k − sum_j r_j.
+```
+
+At any real exponent t, the corresponding identity is
+
+```
+sum_s S_s*s^t − sum_e E_e*e^t
+    = (T_t−P_t) * sum_units column^t.
+```
+
+Thus a favorable raw t-moment survives as a superpotential. It does **not**
+by itself pay the source complements. Writing W=sum W_k and P=number of
+paid rounds, complete untruncated layer counts give
+
+```
+U <= sum_(d=0..G) P^d W^(G−d) <= (W+P+1)^(G+1),
+S := sum_s S_s <= W*U,
+sum_e E_e <= P*U.
+```
+
+The source package's separated case is unchanged: no premature exits occur.
+The verifier compares it with the byte-identical predecessor literal replay.
+
+## 3. Nested divisible widths and complete count bounds
+
+Use the ordinary base B_n=1, P_n=n below m, with B_0=1 and P_0=0. For n>=m
+choose the replication factor and productive width
+
+```
+a_n = B_(n−1),    B_n = a_n*S_n.
+```
+
+Every earlier width B_e divides B_(n−1), by induction. Therefore every
+source-complement batch and exit batch is an integer number of smaller
+uniform programs. This is a concrete choice within the source compiler's
+existing denominator-clearing freedom; no optimum is claimed. Its previous
+option to use an LCM is retained as predecessor context.
+
+As in the source compiler, each of the a_n*S_n original arrays first gets
+its disjoint complementary job, then its one source job through the flow.
+All exits are completed by smaller uniform programs. The result is a full
+rank-n transform on every original array. Owned storage is excluded from B_n.
+
+The normalized leaf count satisfies the **same exact recurrence** for any
+valid replication choice:
+
+```
+L(n) = (1/S_n) * [sum_s S_s L(n−s) + sum_e E_e L(e)].
+```
+
+Changing the replication factors changes width and total counts equally.
+It does not spend supplier saving or alter any outer parameter.
+
+For a fixed final N and h=G(N), all n<=N satisfy
+
+```
+S_n <= C_N := W*(W+P+1)^(h+1),
+B_N = product_(n=m..N) S_n <= C_N^N.
+```
+
+Since h=O(log N), **log B_N=O(N log N)** for a fixed mixed rule. Repeatedly
+multiplying all previous widths is unnecessary. This bounds one explicit
+realization; the original compiler did not require that inefficient choice.
+
+If Delta>0, telescope rank-one mass over the fully expanded uniform program:
+
+```
+B_N*N − P_N = Delta * Qcol_N,
+U_N <= Qcol_N <= B_N*N/Delta.
+```
+
+All raw columns are positive integers, which gives the middle inequality.
+Thus paid leaves and raw instances have the same `exp(O(N log N))` bound.
+With one owned center per raw unit, the center count is at most U_N. A rule
+with O_local distinct owned banks per invocation instead gets O_local*U_N.
+Extra router scratch must be counted separately.
+
+### Routing and word description
+
+Count one routing slot for every source, every exit, every unit target slot
+and every unit paid position. At one flow its count is at most
+`2*(W+P)*U`. The same bound telescopes over all recursive calls, because
+each call contributes its own local unit instances. Exact compilation checks
+this identity alongside widths and leaves.
+
+In the macro grammar that records a whole-job adapter, inverse adapter or
+whole-field move as one record, a slot can be handled with at most sixteen
+records: up to two whole-job conjugations and their inverses, park/load/
+return/reorder moves, and explicit scratch initialization and erasure.
+Allocate separate owned scratch for those moves when needed; no zero-cost
+routing or free copying is assumed. Let A bound the fixed unit's complete
+nonrecursive record count, owned operations and scalar coefficient heights.
+The final weighted record allowance satisfies the conservative bound
+
+```
+R_bar <= A*U_N + 32*(W+P)*U_N + P_N
+      <= (A+32*(W+P)+1)*B_N*N,  for Delta>=1.
+```
+
+R_bar bounds both the macro count and the sum of scalar-height and native
+record allowances. Every owned bank has an explicit initialization record,
+so total allocated owned banks can also be bounded by R_bar; the sharper
+raw-center bound remains separate. This is a **description/record bound**,
+not a new tariff for executing a
+general matrix or permutation. A Gaussian monomial adapter's dense binary
+address matrix and quadratic phase have O(N^2) descriptor bits. Explicit role indices add O(log B_N)
+bits. Thus an encoding of this finite word still has
+`exp(O(N log N))` bits for a fixed unit and its finite coefficient alphabet.
+If physical expansion of one adapter needs F(N) native records, multiply
+the routing term by its actual F(N). That physical implementation, coefficient
+heights and tape costs remain separately priced native obligations. They
+are not set to zero by the macro bound.
+
+## 4. Applying the size result to PR4433
+
+The new nested widths may be used in the separated compiler of PR4433.
+Its normalized L(n), ambient N, uniform saving and outer ledger remain
+unchanged. Therefore this application does not need the still-open direct
+exponent lemma.
+
+With `v=150`, `H=349300000000`, `N=2^H`, the completed mixed rule has
+
+```
+W = 7688^150 < 2^1950,
+P <= 131115^150 + 7688^150*15^150 < 2^2701,
+W+P+1 < 2^2702.
+```
+
+The bound on P counts every original and completion call by its positive
+rank mass; splitting preserves that mass. Since k_min>=2, h<=H. Set
+
+```
+D = 1950 + 2702*(H+1) = 943808600004652.
+```
+
+There is consequently a realization of the same proposed conditional
+κ=0.00268647 supplier satisfying
+
+```
+B_N < 2^(D * 2^H),
+P_N < B_N * 2^H.
+```
+
+More finely, after expanding every product, padding, split and compiler call
+back to the raw p7 word, that word has surplus 608. Product/completion/split
+boundaries cancel, so
+
+```
+B_N*N − P_N = 608 * sum_raw_p7_instances column,
+U_raw <= (B_N*N − P_N)/608.
+```
+
+This is also an explicit bound on raw p7 center banks under the safe
+one-center-per-instance allocation. These are large upper bounds, not
+emitted words, smallest widths or practical precision estimates. They replace
+one implicit part of the source finite-constant prescription. The native
+adapter bodies, analytic transfer and physical costs retain their original
+conditions; a closed bound for the source's finite-constant prescription is
+given next, without a new physical runtime or exact-recovery threshold.
+
+### A closed envelope for the source finite constants
+
+The exported THREE-base native word has exactly 22,633 records in each
+orientation. Source-bound counting retains all 15 copies, the literal p7
+controller, scalar allowance 2,490,856, every productive/paid/contact/helper/
+idle slot, and all routing and owned operations. A raw macro allowance is
+
+```
+A_raw = 15*8*(decompressed native JSON bytes)
+      + 8*(literal controller JSON bytes)
+      + 32*(2490856 + all declared slots + 15*22633) < 2^40.
+```
+
+The payload-bit terms overcount the coefficient literals and full local
+descriptors, including both orientations. The 32-per-slot term overcounts
+whole-job normalizers and inverses, field movements, initialization and
+erasure. It is a bound on the declared source word in this grammar, not
+independent verification of its functional correctness or physical tariffs.
+
+For the chronological v-fold product, its number of raw p7 invocations is
+
+```
+U_v = sum_(i=0..v−1) 7688^(v−1−i)*55998^i < 2^2392.
+```
+
+At every product level retain the whole-job matching wrappers. A conservative
+product allowance is
+
+```
+A_product <= (2^40 + 32*v*(7688+55998+1))*U_v + 32*v*55998^v.
+```
+
+Add 32 records for every final paid call, completion role and original paid
+position. Counting paid calls by their rank mass gives
+
+```
+A_completed <= A_product
+    + 32*(131115^v + 7688^v*15^v + 7688^v + 55998^v).
+```
+
+A dense local binary map/quadratic phase and role index fit in
+`64*(121^v)^2` bits per such record. The verifier checks the integer bound
+`A_completed * 64*(121^v)^2 < 2^5000`. Thus **A=2^5000** is a valid weighted
+record/description allowance for this fixed completed unit. It includes all
+source coefficients and owned operations, with a large deliberate overcount.
+No instruction list of the completed product is emitted.
+
+Since `A+32*(W+P)+1 < 2^5001`, use the envelope
+
+```
+R_bar < 2^(D*2^H + H + 5001).
+```
+
+Apply the existing source finite-constant prescription to the **newly expanded
+word**. With Z=B_N+owned banks, G its scalar coefficient envelope, and P_N
+its rank-one leaves, we have `Z<=2*R_bar`, `G<=8*R_bar`, `P_N<=R_bar` and
+`N<=R_bar`. Therefore
+
+```
+E = 64*(Z+N+P_N+G+1)^3
+  < 2^(3*D*2^H + 3*H + 15021),
+B_constant = P_N+E,
+C0 = 32*N*B_constant^2
+   < 2^(6*D*2^H + 7*H + 30049)
+   < 2^(8*D*2^H).
+```
+
+The last comparison uses `2^H>=H+1` and an exact polynomial integer check
+on D and H. These are explicit, very loose upper bounds for the inherited
+semantic precision/stock constants, conditional on that source prescription
+and its admitted native record implementations. The exact numerical outer
+input threshold, prime exclusions and physical tape costs remain separate.
+
+## 5. Exact finite checks and the open exponent gate
+
+The verifier uses no floating-point acceptance tests. It checks:
+
+- Nine literal/merged flows at ranks 20, 40 and 80: a separated control,
+  strict overlap `{2:1,5:1} <- {1:2,4:1}`, and Sussman's open equality
+  example `{2:4,3:1} <- {1:6,2:2}`. Every whole input and exit agrees.
+- The separated control agrees with the unchanged Sussman literal replay.
+- Complete nested-width compilations through rank 100 on both overlap
+  examples, checking every recursive batch, routing count and rank identity.
+- Raw p7 through rank 1,000: **880 exact nonbase compilations**. B_1000 has
+  17,504 bits; the saved receipt binds all large computed integers by their
+  unsigned big-endian hashes, avoiding enormous decimal dumps.
+- Removing premature exits violates mass conservation. Removing batch
+  replication fails integer divisibility. Allowing a paid rank equal to
+  the ambient rank is rejected because strict rank descent is unavailable.
+
+For raw p7 at rank 1,000, exact arithmetic gives
+
+```
+L(1000) > 990 > 1000^(1−0.00268647).
+```
+
+The second comparison is elementary and exact: `ln(2)>2/3` from its first
+atanh term and `1000>2^9` give `ln(1000)>6`. Then
+`1000^κ > 1+6κ > 100/99`. No log approximation is used in this rejection.
+This checks one finite failure and keeps it distinct from the infinite-rank
+question.
+
+The missing lemma is a uniform bound on the **whole** recurrence. For some
+fixed p and sufficiently large n, one would need, for example,
+
+```
+sum_e E_e e^t (1+log2(e))^p
+ + sum_s S_s (n−s)^t (1+log2(n−s))^p
+ <= S_n n^t (1+log2(n))^p,
+```
+
+with zero-rank terms defined separately and a correctly funded base range.
+The premature exits have rank proportional to n. Their logarithmic factors
+cannot use the old fixed theta<1 power contraction. A raw moment advantage
+alone does not prove this inequality.
+
+Exploratory `approximate_leaves` in flow.py evaluates the recurrence in
+floating point and is deliberately excluded from verification. A bounded
+run through 20,000 ranks found saving about 0.000827 for the default height;
+varying the height did not approach 0.00268647 there. This is local search
+evidence, not a lower bound or a reason to enlarge the same scan. A better
+boundary estimate or a changed flow is the next research obligation.
+
+## 6. Reproduction and provenance
+
+Python 3.12, standard library only:
+
+```sh
+python3.12 -B research/direct-mixed-flow/verify.py
+python3.12 -B scripts/research_package.py --package research/direct-mixed-flow --check-only
+python3.12 -B scripts/research_package.py --package research/direct-mixed-flow
+```
+
+Use `verify.py --out /absolute/new/result.json` for a fresh receipt.
+[RESULT.json](RESULT.json) contains exact flows, integer compilation hashes,
+symbolic size bounds and negative controls. `flow.py` is the new algorithm;
+the verifier independently compares its merged and literal traversal outputs.
+Those are two internal implementations, not an independent mathematical review.
+
+Canonical base is `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority revision
+7. SOURCES.json pins orientation metadata. VENDOR.json separately binds eleven
+unchanged exports by commit, full path, Git blob and SHA256. Their bytes and
+notices are preserved; direct replay needs no foreign Git objects. The source
+theorem and earlier finite compiler remain attributed hypotheses, not new work.
+
+Local validation used Python 3.12.8 on macOS arm64. The registered replay,
+metadata/pin check and committed-byte preflight passed. A separate Git-free
+copy passed with `python3.12 -I -O -B verify.py`; changed-native-source and
+changed-receipt controls both rejected. Replay uses exact integer arithmetic
+and source hashes, with no network or foreign Git objects. The repository is
+shallow, so a full source-history preflight was not attempted. No Lean, Docker,
+full native/all-column admission, physical adapter expansion or historical
+suite was run. Independent mathematical acceptance remains open.
+
+The overlap refresh at 18:48 UTC covered 538 open PR bodies and 3,280
+discussion/comment records, with complete reported pagination. Specific
+searches for direct overlapping-rank compilers, Pascal matching and nested
+widths found no matching public item in that scope; this is not a novelty
+certificate. Existing PR4433 supplies the fixed-rank application, and the
+source theorem explicitly leaves the unseparated exponent open. No Discussion
+claim or PR has been posted for this partial checkpoint.
+
+## Open next questions
+
+1. **Close or refute the direct exponent gate for this capped flow.** Start
+   with a proved bound on premature-exit potential relative to the actual
+   complement capacity. This decides whether the flow can replace the
+   tensor/padding layer. A larger rank scan is not a uniform proof.
+2. **Independently admit the physical expansions and precision prescription.**
+   Audit the conservative A allowance against the actual native caller and
+   bind every adapter's physical implementation, row movements and recovery
+   exclusions. The encoded constants above use the inherited semantics;
+   description size is not a physical execution tariff.
+3. **Tighten the constructive width.** The nested product is an explicit
+   upper bound, not an optimized LCM. A useful next step would control prime
+   valuations of the actual source counts; another arbitrary batching choice
+   would not by itself establish a smaller physical supplier.
+
+Prepared by zxv with substantial OpenAI Codex assistance in research, code
+and writing. No subagents or independent human mathematical review were
+used. New material is Apache-2.0. The integer lockstep/Pascal construction
+and original open unseparated question are Jacob Alan Sussman's work, retained
+at upstream `wht-power-saving-lean` commit
+`563b4e6e913625637f36ba7869bf5fcd0dd4975a`; its LICENSE and NOTICE are included.
+PR4359 supplies the native finite-precompilation bridge and p7 predecessor
+lineage. PR4416's p7 product/padding is @1337isnot1337's work. PR4433 supplies
+the unchanged sufficient rank. Their original contributor credit remains
+in the authenticated exports.
diff --git a/research/chronological-width-growth/vendor/p7-RESULT.json b/research/chronological-width-growth/vendor/p7-RESULT.json
new file mode 100644
index 0000000000..ebb30a9b3b
--- /dev/null
+++ b/research/chronological-width-growth/vendor/p7-RESULT.json
@@ -0,0 +1,296 @@
+{
+  "endpoint": {
+    "compiler": {
+      "H0": 4307773805920,
+      "H1": 16201843136005340321,
+      "N_encoding": "2^16201843136005340321",
+      "delta": "1/1400000000",
+      "exit_coefficient_log2_upper": "26640",
+      "final_strict_power_gap": "1/1400000000",
+      "h": "1/26",
+      "materialized_tensor_rule_or_uniform_word": false,
+      "negative_log2_eta_upper": "147931769/1250000",
+      "paid_max_bound_encoding": "10^6240",
+      "rank_one_induction": "131723^n > 131115^n; target padding adds equal paid and target rank, and splitting preserves rank",
+      "t": "12466419/12500000",
+      "target_max_encoding": "121^6240",
+      "target_min_encoding": "11^6240",
+      "tensor_power": 6240,
+      "theta_upper": "25/26",
+      "z": "139623893/140000000",
+      "z0": "1396238929/1400000000"
+    },
+    "gain_over_PR4359": "38647/100000000",
+    "gain_over_PR4405": "19069/50000000",
+    "gain_over_PR4414": "33/5000000",
+    "gain_over_allfresh_p3": "5223/25000000",
+    "kappa": "268647/100000000",
+    "ledger_source_sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15",
+    "minimum_outer_margin": "524529867/122500000000000000",
+    "negative_controls": {
+      "closed_epsilon": {
+        "actual_logarithmic_gamma_guard": "0",
+        "epsilon_below_one": "0",
+        "gaussian_above_main": "-1410399/122500000000000000",
+        "global_gamma_power_slack": "-1/7000000000",
+        "new_semantic_guard_with_C1_one": "0",
+        "source_axis_superpolynomial": "0"
+      },
+      "closed_uniform_gap": {
+        "new_complex_uniform_saving_above_b": "0"
+      },
+      "insufficient_BIT": {
+        "actual_bit_above_effective": "-270533/700000000"
+      },
+      "unfunded_outer_point": {
+        "boundary_algebraic_matrix_above_kappa": "-525470133/122500000000000000",
+        "fused_gaussian_above_kappa": "-526410399/122500000000000000",
+        "global_coordinate_router_above_kappa": "-3/700000000",
+        "group_bit_router_above_kappa": "-1405641599/490000000000000000",
+        "main_transform_above_kappa": "-700470133/122500000000000000"
+      }
+    },
+    "outer": {
+      "functional_checks": {
+        "fixed_halo_explicit_metadata_branch": "13475000001/175000000",
+        "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000",
+        "new_semantic_group_guard": "3/700000000"
+      },
+      "margins": {
+        "boundary_algebraic_matrix": "329093274529867/122500000000000000",
+        "fused_gaussian": "329093273589601/122500000000000000",
+        "global_coordinate_router": "1880533/700000000",
+        "group_bit_router": "1316373794358401/490000000000000000",
+        "group_scans": "349999999/350000000",
+        "main_transform": "329093099529867/122500000000000000",
+        "microbox_face_corrections": "13475000001/175000000",
+        "polynomial_products": "699999999/700000000",
+        "sparse_union_movement": "50094718274529867/122500000000000000"
+      },
+      "parameters": {
+        "a": "1880533/700000000",
+        "b": "940267/350000000",
+        "beta": "699999997/700000000",
+        "bit_saving": "27/10000",
+        "cap_xi": "111344718099529867/122500000000000000",
+        "complex_uniform_saving": "376107/140000000",
+        "d": "1/700000000",
+        "epsilon": "699999999/700000000",
+        "kappa": "268647/100000000",
+        "lambda_": "39892541/40000000",
+        "lambda_prime": "174529867/175000000",
+        "layout": "1/700000000",
+        "q": "470133/175000000",
+        "r0": "1/7000000000",
+        "stop": "1/700000000",
+        "tested_saving": "33581/12500000"
+      },
+      "strict_checks": {
+        "actual_bit_above_effective": "9467/700000000",
+        "actual_logarithmic_gamma_guard": "1/700000000",
+        "actual_logarithmic_group_guard": "11155282162970133/61250000000000000",
+        "alpha_logarithm_absorption": "1/7000000000",
+        "boundary_algebraic_matrix_above_kappa": "699529867/122500000000000000",
+        "cap_above_band": "50094718099529867/122500000000000000",
+        "cap_below_cell": "11155281725470133/122500000000000000",
+        "cap_below_phase_cell_power": "133655281900470133/122500000000000000",
+        "complex_above_effective": "1/700000000",
+        "complex_below_one_over_32": "9997233/350000000",
+        "complex_endpoint": "1/350000000",
+        "epsilon_below_one": "1/700000000",
+        "epsilon_positive": "699999999/700000000",
+        "fine_prime_halo_umbrella": "7/2",
+        "fused_gaussian_above_kappa": "698589601/122500000000000000",
+        "gaussian_above_main": "87029867/61250000000000000",
+        "global_coordinate_router_above_kappa": "1/175000000",
+        "global_gamma_power_slack": "9/7000000000",
+        "group_below_dimension": "1/350000000",
+        "group_bit_router_above_kappa": "3494358401/490000000000000000",
+        "group_gauge_power_slack": "11155282154220133/61250000000000000",
+        "group_key_fits_record": "1/350000000",
+        "group_positive": "699999997/700000000",
+        "group_scans_above_kappa": "698119469/700000000",
+        "halo_covers_generic_inverse_radius": "5",
+        "improvement_over_user_baseline": "477749790400418148631/500000000000000000000000",
+        "lambda_above_internal": "1/1400000000",
+        "lambda_above_sigma": "3/1400000000",
+        "lambda_above_tau": "1/1400000000",
+        "lambda_prime_above_lambda": "1/1400000000",
+        "lambda_prime_above_leaf": "699059733/245000000000000000",
+        "leaf_saving_above_effective": "349059733/245000000000000000",
+        "main_transform_above_kappa": "524529867/122500000000000000",
+        "membership_arithmetic_fits_record": "1/700000000",
+        "microbox_face_corrections_above_kappa": "2155924779/28000000",
+        "microbox_halo_volume": "55300000003/700000000",
+        "new_complex_uniform_saving_above_b": "1/700000000",
+        "new_semantic_guard_with_C1_one": "1/700000000",
+        "polynomial_products_above_kappa": "69811947/70000000",
+        "positive_layout_slack": "1/700000000",
+        "q_below_effective": "1/700000000",
+        "q_below_internal": "1/700000000",
+        "q_below_leaf": "699059733/245000000000000000",
+        "q_positive": "470133/175000000",
+        "short_record_fallback": "349059733/350000000",
+        "source_axis_superpolynomial": "1/700000000",
+        "sparse_union_movement_above_kappa": "49765625699529867/122500000000000000",
+        "stop_below_one": "699999999/700000000",
+        "stop_positive": "1/700000000",
+        "strassen_integer_power_gap": "1951441519231",
+        "support_router_span": "3/700000000",
+        "theta_positive_polynomial_power": "2",
+        "union_header_fits_record": "3/700000000",
+        "union_tag_work_per_visit_fits_record": "3/700000000"
+      }
+    },
+    "schema": "native-p7-padding-strictification-outer-endpoint/1",
+    "scope": "Source-bound native p7 geometry, a finite tensor recipe with target padding, exact moment and outer inequalities, and a specified finite uniform rank. Native tensor closure and the PR4359 inherited precision, storage, analytic, fixed-tape and recovery hypotheses are written premises, not a full formal theorem certificate.",
+    "status": "PASS_CONDITIONAL_P7_OUTER_POINT",
+    "strictification_source_sha256": "1f3c2a38b34d9dad7266be212ca5d0225827d8e05bda4831e6c25c5713f624f0",
+    "tested_saving": "33581/12500000"
+  },
+  "independent_interval_crosscheck": true,
+  "scope": "Conditional native construction and exact finite arithmetic. The finite word and inherited physical, precision, analytic and fixed-tape proofs are not formally verified or materialized by this checker.",
+  "source_files": 23,
+  "status": "PASS_SOURCE_BOUND_CONDITIONAL_P7_PAID_PADDING_IMPROVEMENT",
+  "strictification": {
+    "alpha_interval": {
+      "lower": "0.99999998440390797702869232902431332",
+      "upper": "0.99999998440390797702869232902431333"
+    },
+    "alpha_upper": "99999999/100000000",
+    "completion_decay_block_length": 2,
+    "controls": {
+      "one_decay_block_rejected": true,
+      "undamped_completion_rejected": true,
+      "unpadded_rank_one_tail_rejected": true
+    },
+    "cutoff_base": 10,
+    "cutoff_encoding": "10^6240",
+    "decay_block_count": 16,
+    "decay_block_length": 390,
+    "delta_interval": {
+      "lower": "0.64382470915163933966321257464784307",
+      "upper": "0.64382470915163933966321257464784308"
+    },
+    "delta_upper": "2/3",
+    "exponent": 6240,
+    "gamma_interval": {
+      "lower": "0.99819171247300624373216957625759087",
+      "upper": "0.99819171247300624373216957625759088"
+    },
+    "gamma_upper": "4991/5000",
+    "materialized_tensor_or_completed_word": false,
+    "native_inventory": {
+      "artifact_hash_encoding": "Uncompressed UTF-8 JSON, sort_keys=True, separators=(comma,colon)",
+      "artifact_sha256": "12784fff6a13e3752ea6e80018e0484c5766a8adf2e88a7e71c80cf2bb68f398",
+      "contacts": 6720,
+      "dimension": 121,
+      "factor_receipt_sha256": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598",
+      "fresh_helper_fields": 6120,
+      "keep": 232127,
+      "limits": "Finite exact physical controller admission; inherited all-column local word, tensor strictification, new full-word precision/stock and outer transfer remain written proof obligations.",
+      "main_fields": 1568,
+      "native_scalar_allowance": 2490856,
+      "native_source_gate": "PASS_ACTUAL_ARBITRARY_HELPERS_AND_COMPLETE_PHASE_CORRECT_IDLE_JOBS",
+      "negative_controls": {
+        "omitted_endpoint_translation_rejected": 784,
+        "wrong_native_orientation_rejected": true
+      },
+      "p": 7,
+      "paid": {
+        "1": 37305,
+        "16": 448,
+        "2": 10695,
+        "3": 3360,
+        "32": 448,
+        "4": 1530,
+        "48": 448,
+        "5": 300,
+        "8": 1464
+      },
+      "paid_calls": 55998,
+      "productive_fields": 7688,
+      "rank_margin": 608,
+      "scalar_allowance": 2490856,
+      "schema": "source-bound-p7-all-fresh-complete-native-controller/1",
+      "source_sha256": {
+        "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85",
+        "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa",
+        "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497",
+        "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e",
+        "research/kappa-rebuild/complex/fresh-certificates/THREE-base-HELPER-BOUNDARIES.json.gz": "f90517e395bde58c72cacd5d3481c4ea31d459fe4535384ac16547ac40460555",
+        "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6",
+        "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61",
+        "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39",
+        "research/kappa-rebuild/complex/full_identity_rebuild.py": "9af2ffbb0038c92e2a7d281081b0daaeadce75b11b566e5427845dc1af91e33d",
+        "research/kappa-rebuild/controller/P3-NATIVE-COVER.json.gz": "facfc6d6ecde151afb7e6a167776f3fdaac1c816e785a21a39f7f0bfd9140f3f",
+        "research/kappa-rebuild/controller/p3_native_cover.py": "fae71fcbbd20b9ee73b049cf6f43ea1d048217fb15feb6055a007e47da3363fe",
+        "research/kappa-rebuild/transfer-audit/p3_cover_audit.py": "a0fe9a26f77556e83b31b0c91fea909d6f3d8209d0f9f7ad4e5bc1375d33615e",
+        "research/kappa-rebuild/transfer-audit/p3_native_audit.py": "5504a55a50546418d10c522984438cdeedb44993f7c1dab7bd4aa1ae0515d902"
+      },
+      "status": "PASS_EXACT_LAURENT_ALL_MAIN_CONTACTS_ENDPOINTS_AND_FULL_IDLE_PHASES",
+      "targets": {
+        "121": 224,
+        "25": 448,
+        "41": 448,
+        "5": 420,
+        "57": 448,
+        "6": 270,
+        "7": 840,
+        "8": 1395,
+        "9": 3195
+      },
+      "whole_idle_profile": {
+        "16": 448,
+        "32": 448,
+        "48": 448,
+        "8": 1344
+      }
+    },
+    "new_max_target_encoding": "121^6240",
+    "new_min_target_encoding": "11^6240",
+    "normalized_moment_upper_rational": "10240625039/10240638976",
+    "paid": {
+      "1": 37305,
+      "16": 448,
+      "2": 10695,
+      "3": 3360,
+      "32": 448,
+      "4": 1530,
+      "48": 448,
+      "5": 300,
+      "8": 1464
+    },
+    "paid_rank_one_moment": 131115,
+    "productive_fields": 7688,
+    "rank_one_surplus_encoding": "131723^6240-131115^6240",
+    "schema": "p7-paid-target-completion-tensor-certificate/1",
+    "scope": "Exact moment bounds for the documented chronological native product, paid target completion and disjoint splitting. Native all-column, precision, storage, analytic and fixed-tape premises remain separate; no full multiplication theorem is formally verified.",
+    "source_sha256": {
+      "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a"
+    },
+    "status": "PASS_EXACT_P7_TARGET_COMPLETION_STRICTIFICATION",
+    "strict_moment_verified": true,
+    "strictification_gap": {
+      "lower": "0.00000136095023295546357907266586564",
+      "upper": "0.00000136095023295546357907266586565"
+    },
+    "strictification_gap_rational": "13937/10240638976",
+    "target_floor_base": 11,
+    "target_floor_encoding": "11^6240",
+    "target_rank_one_moment": 131723,
+    "targets": {
+      "121": 224,
+      "25": 448,
+      "41": 448,
+      "5": 420,
+      "57": 448,
+      "6": 270,
+      "7": 840,
+      "8": 1395,
+      "9": 3195
+    },
+    "tested_saving": "33581/12500000",
+    "theta_upper": "25/26"
+  }
+}
diff --git a/research/chronological-width-growth/verify.py b/research/chronological-width-growth/verify.py
new file mode 100644
index 0000000000..7aa8773fd0
--- /dev/null
+++ b/research/chronological-width-growth/verify.py
@@ -0,0 +1,210 @@
+#!/usr/bin/env python3
+"""Source-bound checks of the all-rank argument, not a new native audit.
+
+The pinned #4507 flow/width implementation supplies the object being studied.
+growth.py separately implements breakpoints, valuations and envelopes.
+Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import argparse
+from bisect import bisect_right
+from functools import lru_cache
+import hashlib
+import importlib.util
+import json
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+sys.path.insert(0, str(HERE))
+from growth import (check_descent, check_envelope, depth_bound, factor,
+                    from_valuations, join_valuations, next_valuations,
+                    rank_primes, require, smooth_numbers, universal_parameters)
+
+
+def authenticate():
+    for row in json.loads((HERE/'VENDOR.json').read_text(encoding='utf-8')):
+        raw = (HERE/row['path']).read_bytes()
+        require(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256: '+row['path'])
+        framed = b'blob '+str(len(raw)).encode()+b'\0'+raw
+        require(hashlib.sha1(framed).hexdigest() == row['git_blob'], 'source Git blob: '+row['path'])
+
+
+def load_flow():
+    spec = importlib.util.spec_from_file_location('pinned_batches', HERE/'vendor/batches.py')
+    module = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(module)
+    return module
+
+
+def integer_record(n):
+    return {'bits': n.bit_length(), 'unsigned_big_endian_sha256':
+            hashlib.sha256(n.to_bytes(max(1,(n.bit_length()+7)//8),'big')).hexdigest()}
+
+
+def receipt_hash(value):
+    return hashlib.sha256(json.dumps(value,sort_keys=True,separators=(',',':')).encode()).hexdigest()
+
+
+def breakpoints(flow, targets, paid, cap):
+    m = max(targets)
+    primes = rank_primes(targets, paid)
+    smooth = smooth_numbers(primes, cap)
+    require(len(smooth) == len(set(smooth)), 'distinct breakpoint products')
+    exhaustive = []
+    for value in range(1,cap+1):
+        rest = value
+        for prime in primes:
+            while rest % prime == 0:
+                rest //= prime
+        if rest == 1:
+            exhaustive.append(value)
+    require(smooth == exhaustive, 'complete smooth inventory')
+    prior, changes, constant_intervals = None, [], 0
+    representative = {}
+    for c in range(1,cap+1):
+        current = flow(targets,paid,m*c)
+        require(flow(targets,paid,m*c+m-1) == current, 'floor-cutoff interval')
+        t = smooth[bisect_right(smooth,c)-1]
+        if t not in representative:
+            representative[t] = flow(targets,paid,m*t)
+        require(current == representative[t], 'complete flow constant between prime products')
+        total = sum(current['sources'].values())
+        if prior is not None and total != prior:
+            require(c in smooth, 'source-count change at a prime product')
+            changes.append(c)
+        if c != t:
+            constant_intervals += 1
+        prior = total
+    params = universal_parameters(targets,paid,m*cap)
+    require(len(smooth) <= params['prime_box_count'], 'prime exponent box')
+    return {'cap':cap,'rank_primes':primes,'smooth_products':len(smooth),
+            'nontrivial_constant_comparisons':constant_intervals,
+            'source_count_changes':len(changes),'change_points_sha256':receipt_hash(changes)}
+
+
+def compile_check(module, name, targets, paid, maximum, expected):
+    compiled = module.compile_widths(targets,paid,maximum)
+    require(integer_record(compiled['widths'][-1]) == expected['width'], 'pinned final width')
+    m = max(targets)
+    params = universal_parameters(targets,paid,maximum)
+    smooth = smooth_numbers(params['rank_primes'],params['cap'])
+    flows = {}
+    def flow_at(n):
+        c = n//m
+        if c not in flows:
+            flows[c] = module.direct_flow(targets,paid,m*c)
+        return flows[c]
+    factors = lru_cache(None)(factor)
+    sampled_sources = {sum(flow_at(m*t)['sources'].values()) for t in smooth}
+    sampled_lcm = join_valuations(*(factors(s) for s in sampled_sources))
+    source_lcm, seen_sources, values, records = {}, set(), [{} for _ in range(m)], []
+    constraints = 0
+    first_depth_needed = None
+    first_denominator_needed = None
+    for n in range(m,maximum+1):
+        f = flow_at(n)
+        S = sum(f['sources'].values())
+        require(S <= params['source_ceiling'], 'polynomial source bound')
+        rows = module.requirements(f,n)
+        check_descent(rows,n,m)
+        depth = depth_bound(n,m)
+        require(all(depth_bound(e,m) < depth for e,_ in rows), 'decreasing depth envelope')
+        powers = next_valuations(values,rows,factors(S))
+        exact = from_valuations(powers)
+        require(exact == compiled['widths'][n], 'prime recurrence equals chronological width')
+        source_lcm = join_valuations(source_lcm,factors(S))
+        seen_sources.add(S)
+        check_envelope(powers,source_lcm,depth)
+        check_envelope(powers,sampled_lcm,depth)
+        if first_depth_needed is None and any(e>source_lcm.get(p,0) for p,e in powers.items()):
+            first_depth_needed = {'n':n,'width':exact,'source_lcm':from_valuations(source_lcm)}
+        without_counts = next_valuations(values,[(e,1) for e,_ in rows],factors(S))
+        if first_denominator_needed is None and without_counts != powers:
+            first_denominator_needed = {'n':n,'width':exact,'without_gcd':from_valuations(without_counts)}
+        require(exact <= 1 << params['power_of_two_exponent'], 'explicit binary upper bound')
+        values.append(powers)
+        records.append([n,sorted(powers.items()),depth])
+        constraints += len(rows)
+    require(seen_sources == sampled_sources, 'breakpoints cover every source total')
+    require(source_lcm == sampled_lcm, 'sampled and full source LCM agree')
+    return {'rule':name,'maximum':maximum,'compiled_ranks':maximum-m+1,
+            'batch_constraints':constraints,'width':integer_record(compiled['widths'][-1]),
+            'source_values':len(sampled_sources),'source_lcm':integer_record(from_valuations(sampled_lcm)),
+            'all_rank_valuation_sha256':receipt_hash(records),
+            'parameters':params,'first_depth_needed':first_depth_needed,
+            'first_denominator_needed':first_denominator_needed}
+
+
+def controls(module, compilations):
+    rejected = []
+    def reject(name, operation, message):
+        try:
+            operation()
+        except ValueError as error:
+            require(message in str(error), 'wrong rejection: '+name)
+            rejected.append(name)
+        else:
+            raise ValueError('control accepted: '+name)
+    reject('paid rank reaches ambient',lambda:rank_primes({2:1,5:1},{5:1}),'strict rank')
+    reject('target rank one',lambda:rank_primes({1:1,5:1},{2:1}),'strict rank')
+    reject('noncontracting batch',lambda:check_descent([(9,1)],10,5),'uniform rank')
+    reject('zero batch count',lambda:check_descent([(2,0)],10,5),'uniform rank')
+    reject('nonprime breakpoint alphabet',lambda:smooth_numbers([2,4],20),'ordered primes')
+    targets, paid = {2:1,5:1}, {1:2,3:1}
+    a = module.direct_flow(targets,paid,10)
+    b = module.direct_flow(targets,paid,15)
+    require(rank_primes(targets,paid)==[2,3,5], 'paid-prime positive control')
+    require(smooth_numbers([2,5],3)==[1,2], 'target-only alias')
+    reject('omit paid breakpoint prime',lambda:require(a==b,'changed flow'),'changed flow')
+    require(sum(a['sources'].values())!=sum(b['sources'].values()), 'changed source total witness')
+    rule_t, rule_p = {2:4,3:1}, {1:6,2:2}
+    first = module.compile_widths(rule_t,rule_p,3)['widths'][3]
+    require(first==5 and rank_primes(rule_t,rule_p)==[2,3], 'new width prime witness')
+    reject('confuse width primes with rank primes',lambda:check_envelope(factor(first),{2:1,3:1},1),'source LCM')
+    witness = next(r['first_depth_needed'] for r in compilations if r['first_depth_needed'])
+    reject('drop recursive depth factor',lambda:check_envelope(factor(witness['width']),factor(witness['source_lcm']),1),'source LCM')
+    denominator = next(r['first_denominator_needed'] for r in compilations if r['first_denominator_needed'])
+    reject('omit gcd cancellation in exact recurrence',lambda:require(denominator['width']==denominator['without_gcd'],'wrong exact valuation'),'wrong exact')
+    reject('omit source multiplier',lambda:require(next_valuations([{}, {}, {}],[(0,1)],{})=={5:1},'source multiplier'),'source multiplier')
+    return {'rejections':rejected,'paid_prime_counterexample':{
+            'targets':{str(k):v for k,v in targets.items()},
+            'paid':{str(k):v for k,v in paid.items()},
+            'n_before':10,'n_after':15,'source_total_before':sum(a['sources'].values()),
+            'source_total_after':sum(b['sources'].values())},
+            'new_width_prime':{'rank_primes':[2,3],'first_width':first},
+            'depth_counterexample':witness,'gcd_counterexample':denominator}
+
+
+def run():
+    authenticate()
+    module = load_flow()
+    native = json.loads((HERE/'vendor/p7-RESULT.json').read_text())['strictification']['native_inventory']
+    parse = lambda d: {int(k):v for k,v in d.items()}
+    expected = json.loads((HERE/'vendor/batch-RESULT.json').read_text())['compilations']
+    cases = [('strict-overlap',{2:1,5:1},{1:2,4:1},100),
+             ('source-open-equality',{2:4,3:1},{1:6,2:2},100),
+             ('raw-p7',parse(native['targets']),parse(native['paid']),1000)]
+    compilations = [compile_check(module,*case,ref) for case,ref in zip(cases,expected,strict=True)]
+    epochs = [dict(rule=name,**breakpoints(module.direct_flow,t,p,256)) for name,t,p,_ in cases]
+    epochs.append(dict(rule='paid-prime-control',**breakpoints(module.direct_flow,{2:1,5:1},{1:2,3:1},64)))
+    return {'claim_type':'all-rank conditional width upper bound with finite exact checks',
+            'compilations':compilations,'breakpoints':epochs,'controls':controls(module,compilations)}
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--write',action='store_true',help='authoring only: regenerate RESULT.json')
+    args = parser.parse_args()
+    result = run()
+    path = HERE/'RESULT.json'
+    if args.write:
+        path.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n',encoding='utf-8',newline='\n')
+    else:
+        require(result==json.loads(path.read_text(encoding='utf-8')), 'complete receipt mismatch')
+    print('PASS_CHRONOLOGICAL_WIDTH_GROWTH ranks='+str(sum(r['compiled_ranks'] for r in result['compilations']))
+          +' breakpoint_caps='+str(sum(r['cap'] for r in result['breakpoints']))
+          +' controls='+str(len(result['controls']['rejections'])))
+
+
+if __name__ == '__main__':
+    main()