diff --git a/research/homogeneous-gcd-width/PROOF.md b/research/homogeneous-gcd-width/PROOF.md
new file mode 100644
index 0000000000..87caadb392
--- /dev/null
+++ b/research/homogeneous-gcd-width/PROOF.md
@@ -0,0 +1,172 @@
+# Exact cancellation in a homogeneous chronological compiler
+
+This scoped written proof was produced by Nick Petalas. It specializes
+codyw912's PR4638 arbitrary-height forest and Mihir Srivastava's PR4507
+chronological batching policy. Their validity and native contracts are cited
+premises. No predecessor result is re-audited here.
+
+## Hypotheses
+
+Fix integers m>=2 and W,P>=1. A raw unit has W distinguishable productive
+positions, all of rank m, and P distinguishable chronological paid positions,
+all of rank 1. Use precisely the arbitrary-height forest in PR4638. At
+ambient integer rank n>=m its cutoff is C=floor(n/m), and its height G(n)
+is any specified nonnegative finite integer. Different ranks may have
+different heights. Set B_j=1 for 0<=j<m.
+
+The W targets are separate arbitrary inputs. No productive role is silently
+identified with another. Separate paid paths and positions retain separate
+chronological cuts. The interpretation as a physical supplier requires the
+predecessor's native, whole-job, ownership and closure hypotheses. This proof
+does not construct a native unit with this symbolic inventory.
+
+For every n>=m define
+
+```text
+H(n) = floor(log_m n),
+k(n) = min(G(n)+1,H(n)),
+d(n) = G(n)+1-k(n),
+s(n) = m^k(n),
+S(n) = P^d(n) W^k(n).
+```
+
+All logarithms here define integer floors by power comparison. Since
+floor(log_m floor(n/m))=H(n)-1, the first present depth of the forest is
+d(n). In particular 1<=k(n)<=H(n), m<=s(n)<=n, and n-s(n)<n.
+
+## Lemma 1. The complete source and cut lists
+
+At depth d a class is indexed by a distinguishable paid path of length d.
+There are P^d such classes. A unit is indexed by an ordered target word of
+length G-d. All these words have column m^(G-d), independently of their
+letters. Consequently either the entire class is present or it is empty.
+It is present exactly when m^(G-d)<=C, which is equivalent to d>=d(n).
+
+For a nonleaf present parent, its W^(G-d) paid outputs at one position
+match the child's target demands bijectively. Split a parent word into its
+first letter and remaining word. Both have the same column/rank contract,
+and the child is present whenever its parent is. Thus no present class has
+an unmatched nonleaf exit. This is matching within one actual paid cut,
+with no pooling between paths or positions.
+
+If d(n)=0, the root demands W^(G+1) source jobs of rank m^(G+1).
+If d(n)>0, the classes through depth d(n)-1 are empty. At the first present
+depth d(n), each of the P^d(n) classes demands W^(G-d(n)+1) fresh source
+jobs, all of rank m^(G-d(n)+1). No later class needs a fresh source because
+its present parent supplies it. These two cases give the same source list
+
+```text
+one rank s(n), with total multiplicity S(n).
+```
+
+Every depth-G class contains the single empty target word. Each of its P
+paid positions therefore exits with one rank-one job. The complete exit
+list has P^(G+1) separate cuts, each (rank 1, multiplicity 1). Its length
+is an algebraic count; a general-height forest is not emitted by this proof.
+There are no boundary exits. This also proves nonemptiness, including when
+the root class is empty.
+
+As a consistency identity, its unit-column mass V is
+
+```text
+V = sum_(d=d(n)..G) P^d (Wm)^(G-d),
+S(n) s(n) - P^(G+1) = (Wm-P) V.
+```
+
+This is a telescoping finite geometric sum, valid also at Wm=P. No positive
+surplus or favorable moment is assumed merely to count the forest.
+
+## Theorem 2. Exact least-LCM width at every height
+
+The source complement is one upfront batch
+(n-s(n),S(n)). All the separate exits use B_1=1 and impose no replication
+constraint. Applying the cited local batching lemma gives
+
+```text
+a_n = B_(n-s(n)) / gcd(B_(n-s(n)),S(n)),
+B_n = S(n) a_n = lcm(S(n),B_(n-s(n))).                 (1)
+```
+
+This is the recursively least library under that fixed common-replication
+policy. Local minimality is inherited from PR4507; no optimality over other
+policies or physical programs is claimed.
+
+Starting at n_0=n, set n_(i+1)=n_i-s(n_i) until n_t<m. Each step decreases
+the rank by at least m, so t<=floor(n/m). Repeated application of (1) gives
+the exact closed expression
+
+```text
+B_n = lcm_(0<=i<t) [P^d(n_i) W^k(n_i)].              (2)
+```
+
+The empty LCM is 1. This expression retains the actual gcd cancellations;
+replacing the LCM by multiplication or by numerical maximum is invalid.
+
+## Corollary 3. Exact default width
+
+For the default height G(n)=floor(log_m floor(n/m))=H(n)-1,
+one has d(n)=0, s(n)=m^H(n), S(n)=W^H(n). Along the decreasing chain every
+later H is at most the initial H. Every later source total therefore divides
+the first. Equation (2) proves, for all n>=m,
+
+```text
+B_n = W^floor(log_m n).                              (3)
+```
+
+At n=m^h, this is exactly W^h, so its polynomial order cannot be reduced
+when W>1. P affects exits and cost, but not this default productive width.
+
+For comparison define the specific gcd-free recurrence
+U_j=1 for j<m and U_n=S(n) U_(n-s(n)). Writing n=sum a_j m^j in base m
+gives U_n=W^(sum_(j>=1) j a_j), because each subtraction removes one largest
+power. At n=m^(h+1)-1 its exponent is (m-1)h(h+1)/2. Hence retaining gcd
+cancellation changes this particular upper construction from worst-shell
+exp(Theta((log n)^2)) to polynomial width when W>1. This comparator is
+defined here; it is not alleged to be a predecessor's optimal width.
+
+## Corollary 4. Polynomial adaptive widths, including empty roots
+
+Put G_*(N)=max_(m<=j<=N) G(j), with N>=m. Every source in the chain for
+any n<=N divides W^H(N) P^G_*(N), since k(j)<=H(N) and d(j)<=G(j).
+This remains true when W and P have shared prime factors. Thus
+
+```text
+B_n divides W^H(N) P^G_*(N),  m<=n<=N.               (4)
+```
+
+In particular, fix M>=2 and integer g>=1 and use the predecessor's height
+G(n)=g floor(log_M floor(n/m)). This is monotone, so (4) at N=n gives
+
+```text
+B_n divides W^floor(log_m n) P^(g floor(log_M floor(n/m))),
+B_n <= n^(log_m W + g log_M P).                     (5)
+```
+
+This proves polynomial width even when m^g<M, where the general adaptive
+envelope in PR4638 has a subexponential factor. Equation (5) need not be
+sharp. No lower bound or universal polynomial width theorem for mixed rank
+alphabets follows. The hypothesis that every paid rank is one is essential
+to the cut reduction used above.
+
+## Scope and attribution
+
+The new results are the exact homogeneous source/cut reduction, chain-LCM
+solution, default closed form and polynomial adaptive divisor. The question
+comes from PR4638's request to retain actual gcd savings. PR5962's independent
+prime-coordinate projection and PR6086's shell counting retain a different
+mechanism and are not audited or extended here. This proof does not tighten
+their generic semigroup estimates.
+
+Credit Jacob Alan Sussman's integer compiler; zxv's PR4436/4483 chronological
+forest; Mihir Srivastava's PR4507 local gcd/LCM policy; codyw912's PR4638
+arbitrary-height transfer and width question; and Cinna Davis and Ryanson
+Jonathan for the retained native/flow lineage. LCM arithmetic, positional
+notation and finite geometric sums are classical. No literature-wide
+priority is claimed for those tools.
+
+This is a conditional mathematical specialization. It supplies no physical
+native inventory, storage/tape cost, numerical precision, stock constant,
+outer consumer, new kappa or complete multiplication theorem. In particular,
+polynomial productive width does not bound the cost of generating every
+smaller program. The five selected framework assumptions remain.
+Independent human and formal proof-kernel review are unclaimed.
diff --git a/research/homogeneous-gcd-width/README.md b/research/homogeneous-gcd-width/README.md
new file mode 100644
index 0000000000..81b8e074a2
--- /dev/null
+++ b/research/homogeneous-gcd-width/README.md
@@ -0,0 +1,129 @@
+# Exact polynomial widths from chronological gcd cancellation
+
+This scoped written proof was produced by Nick Petalas. For a symbolic native
+rule with W distinguishable rank-m productive targets and P distinguishable
+rank-one paid positions, the least chronological compiler widths have the
+exact default-height formula
+
+```text
+B_n = W^floor(log_m n),  n>=m;       B_n=1, 0<=n<m.
+```
+
+At an arbitrary finite height G(n), put H=floor(log_m n), k=min(G(n)+1,H),
+s=m^k and S=P^(G(n)+1-k) W^k. The complete cut inventory gives
+
+```text
+B_n = lcm(S,B_(n-s)).
+```
+
+Thus B_n is exactly the LCM of source totals along one decreasing rank chain.
+At adaptive height G(n)=g floor(log_M floor(n/m)), for fixed M>=2 and g>=1,
+
+```text
+B_n divides W^floor(log_m n) P^(g floor(log_M floor(n/m))),
+B_n <= n^(log_m W + g log_M P).
+```
+
+This is a polynomial bound, including parameter ranges where PR4638's general
+adaptive envelope is subexponential. The new step retains actual gcd
+cancellation. It supplies a concrete positive answer to that package's
+gcd-savings opening, without improving its generic semigroup count.
+[PROOF.md](PROOF.md) gives all quantifiers, the complete specialized cuts and
+the comparison with a separately defined gcd-free recurrence.
+
+At m=2,W=2,P=3,n=1023, the least width is 512. Omitting gcd cancellation in
+that recurrence gives 2^45. At fixed height two, the actual rank-10 chain has
+source totals 8 and 18 and needs width 72; replacing LCM by maximum fails.
+These are compiler widths, not runtime measurements or a new kappa.
+
+## Evidence and reproduction
+
+The standalone checker imports no predecessor code and writes no files. It
+enumerates 2,052 forests, including 1,422 empty-root cases, and 139,536 literal
+leaf cuts. Distinguishable paid paths and ordered target words independently
+recover the claimed source/cut and unit-column formula. Exact rank invoices
+also agree. A separate literal-batch compiler checks 27 default width tables.
+The recurrence and chain formula agree at 121,440 coordinates in 480 tables
+across default, fixed and adaptive rules. Twelve domain rejections and seven
+semantic control groups retain explicit checks under optimization.
+Four capacity controls exercise the declared logarithm, closed-form, chain
+and width-table limits. Three disposable optimized-code mutations reject an
+omitted empty-root depth, omitted paid-path multiplicity and omitted gcd.
+
+The finite domains corroborate the written proof. They do not establish its
+unbounded quantifiers or certify a physical native supplier. The receipt is
+generated on stdout and binds all six package files by SHA256; no receipt is
+hand-written or committed.
+
+From the worktree root, with the local CPython 3.12 interpreter:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/homogeneous-gcd-width/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/homogeneous-gcd-width/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/homogeneous-gcd-width
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/homogeneous-gcd-width --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. Only the standard
+library is required. Expected markers are PASS_HOMOGENEOUS_GCD_WIDTH,
+PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. Source pins
+are provenance only, so the standalone six-file replay also works without Git.
+
+## Scope, credit and overlap
+
+The source question is codyw912 / [PR4638](https://github.com/CrocSwap/integer-mult-bounds/pull/4638),
+Open next question 2 of research/adaptive-chronological-batching. Credit Mihir
+Srivastava / [PR4507](https://github.com/CrocSwap/integer-mult-bounds/pull/4507)
+for least chronological batching; zxv / PR4436 and PR4483 for the default and
+arbitrary-height forests; Jacob Alan Sussman for integer compilation; and
+Cinna Davis and Ryanson Jonathan for their retained native and flow lineage.
+LCM arithmetic and positional notation are classical. No literature-wide
+priority claim is made.
+
+Nick Petalas / PR5962 improves semigroup counting, and JoyboyBrian / PR6086
+improves adaptive shell counting. This proof uses a different mechanism,
+retaining exact cancellation in source multiplicities. The source results
+and their numbers are cited premises, not audit or replay deliverables.
+
+Canonical base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8,
+selected PR6030. The selected mixed-rank inventory is outside this theorem.
+Live open PRs, active Discussions, recent account work, local reservations and
+main/merged object and general-form searches were checked. Cached overlap
+reported complete pagination for 555 open PRs and 6,599 discussion records;
+sparse local notes, arbitrary historical diffs and unpublished work remain
+coverage limits. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373389)
+records the exact scope. Structured metadata is in [TASK.json](TASK.json).
+
+No physical realization of the homogeneous rule, finite generation-time bound,
+practical cutoff, storage extent, precision, stock, outer consumer, supplier
+admission or complete multiplication theorem is supplied. All-column native
+semantics, ownership/erasure, compiler realization, precision/tape and analytic
+recovery remain conditional obligations. Independent human and formal
+proof-kernel review are unclaimed. The selected cold replay, Lean and Docker
+were not run. New work is Apache-2.0; frozen predecessor files are unchanged.
+
+## Open next questions
+
+- Bind one physically realized native word to this inventory and price its
+  complete caller. A useful physical inventory is missing; polynomial width
+  alone does not improve the selected exponent.
+- Find a valuation invariant retaining gcd savings for one mixed-rank physical
+  profile. The one-complement and rank-one-exit reduction fails there, so this
+  proof supplies no mixed-rank polynomial width claim.
+
+## Verifier constraints
+
+All functions are at most 45 lines. Loops and iterator products have explicit
+finite domains; there is no recursion, subprocess, network, dynamic code
+execution, callback or output-file creation. Explicit guards remain active
+under optimized Python. Registered replay uses warnings as errors.
+
+Power-of-ten rule 3 deviation: CPython allocates managed integers, sets and
+containers during checking. The literal oracle bounds m<=6, W,P<=3, n<=512
+and height<=5. Each target-word set has at most 243 members and each paid-path
+iterator has at most 243 members; a leaf sweep has at most 729 cuts. Width
+tables have at most 1,025 entries. The closed formula caps height at 256 and
+rank at 2^256. Package reads are bounded by two MiB per file. These controls
+bound live memory in this one-shot verifier; they do not provide an
+allocation-free runtime. An embedded fixed-allocation port would need a
+separate implementation and capacity review.
diff --git a/research/homogeneous-gcd-width/SOURCES.json b/research/homogeneous-gcd-width/SOURCES.json
new file mode 100644
index 0000000000..dce9c877be
--- /dev/null
+++ b/research/homogeneous-gcd-width/SOURCES.json
@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/adaptive-chronological-batching/README.md",
+      "usage": "provenance",
+      "git_blob": "d8cb94c3f4e9210060da425d882fde9d2b03e6c1",
+      "sha256": "3943b7e0dabc0486d566f2070518a28f1429e9cce9b578dd4b3a2a00dc7f4cf4"
+    },
+    {
+      "path": "research/adaptive-chronological-batching/WIDTH.md",
+      "usage": "provenance",
+      "git_blob": "4c637ac8968ffd5268ef39bf136e140afec11f6e",
+      "sha256": "63ddab206587d72abb9e155fd2f3532ca6c1b3a822a5e426a829f31bcfa535f8"
+    },
+    {
+      "path": "research/adaptive-chronological-batching/batching.py",
+      "usage": "provenance",
+      "git_blob": "0347e94fec541a373807d5536e164d8ba617be77",
+      "sha256": "e443972cc4b4a5247b90a6b042f61db8171080c7499b416fbaad56059ef3f369"
+    },
+    {
+      "path": "research/chronological-batch-width/README.md",
+      "usage": "provenance",
+      "git_blob": "c85304a601f858774f425d5f3869ac0a6f85ec29",
+      "sha256": "0cf276c77016a98a0dabba822d27bb9cb94c0bf86ec353a16499fe85e6032c20"
+    }
+  ]
+}
diff --git a/research/homogeneous-gcd-width/TASK.json b/research/homogeneous-gcd-width/TASK.json
new file mode 100644
index 0000000000..a383ce7abe
--- /dev/null
+++ b/research/homogeneous-gcd-width/TASK.json
@@ -0,0 +1,110 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact homogeneous chronological source/cut reduction, chain-LCM widths, default closed form and polynomial logarithmic-height adaptive bound.",
+  "scope_change_reason": "The interface card changes to PR4638 Open next question 2 about actual gcd cancellation. A symbolic one-target-rank, rank-one-paid specialization admits an exact solution; native realization is not supplied.",
+  "bottleneck_link": "Compiler productive width is one finite-resource obligation. This specialization proves that actual cancellation can remove generic quasipolynomial or subexponential width envelopes, without claiming applicability to the mixed selected supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved homogeneous width formula and bounded independent finite corroboration. Do not extend the native model or claim a new kappa.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; standalone literal-forest, chronological-batch and chain-LCM comparisons in verify.py.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does a physically realized native rule admit this homogeneous rank inventory with a useful complete moment?",
+      "why_it_matters": "The polynomial width theorem alone does not supply a supplier or improve the selected exponent.",
+      "first_step": "Bind one literal native word to W full-rank productive jobs and P rank-one paid positions, then price its entire caller.",
+      "blocked_by": "No such physical inventory or complete bill is supplied here."
+    },
+    {
+      "question": "Can actual gcd cancellation yield a smaller bound for one mixed-rank physical profile?",
+      "why_it_matters": "The selected supplier has multiple productive and paid ranks outside the theorem.",
+      "first_step": "Identify a changed invariant controlling valuations on its actual separate chronological cuts.",
+      "blocked_by": "The one-complement and rank-one-exit reduction fails for general mixed ranks."
+    }
+  ],
+  "coordination": {
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373389",
+    "source_pr": 4638,
+    "source_author": "codyw912",
+    "predecessor_author": "codyw912",
+    "upstream_checked_at": "2026-11-03T12:07:00Z",
+    "upstream_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "overlap_limits": "Complete open/discussion cached pagination; targeted merged/main searches. Sparse local notes, arbitrary historical diffs and unpublished work remain outside coverage."
+  }
+}
diff --git a/research/homogeneous-gcd-width/VERIFY.json b/research/homogeneous-gcd-width/VERIFY.json
new file mode 100644
index 0000000000..fbd8a0ec69
--- /dev/null
+++ b/research/homogeneous-gcd-width/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Literal distinguishable forests, complete specialized cut reduction, exact default and adaptive width identities and semantic/domain controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same exact checks with optimization; explicit guards remain active."
+    }
+  ]
+}
diff --git a/research/homogeneous-gcd-width/verify.py b/research/homogeneous-gcd-width/verify.py
new file mode 100644
index 0000000000..8e6c032e8a
--- /dev/null
+++ b/research/homogeneous-gcd-width/verify.py
@@ -0,0 +1,272 @@
+#!/usr/bin/env python3
+"""Exact finite corroboration of homogeneous chronological width cancellation.
+
+Produced by Nick Petalas. Apache-2.0.
+The universal statements are proved in PROOF.md; this checker imports no
+predecessor implementation and writes no files.
+"""
+from collections import Counter
+from hashlib import sha256
+from itertools import product
+import json
+from math import gcd, lcm
+from pathlib import Path
+
+
+FILES = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py")
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def integer(value, low, high):
+    need(type(value) is int and low <= value <= high, "integer domain")
+
+
+def floor_log(value, base):
+    integer(value, 1, 2**256)
+    integer(base, 2, 2**16)
+    for exponent in range(257):
+        if value < base:
+            return exponent
+        value //= base
+    raise ValueError("logarithm capacity")
+
+
+def closed_flow(m, w, p, n, height):
+    """New source/cut formula, on an explicitly bounded executable domain."""
+    integer(m, 2, 16)
+    integer(w, 1, 16)
+    integer(p, 1, 16)
+    integer(n, m, 2**256)
+    integer(height, 0, 256)
+    shell = floor_log(n, m)
+    letters = min(height + 1, shell)
+    start = height + 1 - letters
+    rank = m**letters
+    sources = p**start * w**letters
+    need(1 <= rank <= n and start >= 0, "strict complement descent")
+    columns = Counter()
+    for depth in range(start, height + 1):
+        columns[m**(height - depth)] += p**depth * w**(height - depth)
+    return {"sources": {rank: sources}, "columns": dict(columns),
+            "leaf_cuts": p**(height + 1), "boundary_cuts": 0,
+            "source_depth": start}
+
+
+def literal_flow(m, w, p, n, height):
+    """Enumerate distinguishable paid paths and ordered target words.
+
+    This does not use closed_flow, a multinomial formula, or compressed path
+    occurrences. Each paid position retains its own chronological cut.
+    """
+    integer(m, 2, 6)
+    integer(w, 1, 3)
+    integer(p, 1, 3)
+    integer(n, m, 512)
+    integer(height, 0, 5)
+    cap = n // m
+    sources, columns = Counter(), Counter()
+    leaf_cuts, boundary_cuts, first_source = 0, 0, None
+    for depth in range(height + 1):
+        degree = height - depth
+        here = set(product(range(w), repeat=degree)) if m**degree <= cap else set()
+        if depth == 0:
+            for word in here:
+                for letter in range(w):
+                    sources[m**(len(word) + 1)] += 1
+                    first_source = 0
+        below = set()
+        if degree and m**(degree - 1) <= cap:
+            for tail in product(range(w), repeat=degree - 1):
+                for letter in range(w):
+                    below.add((letter,) + tail)
+        for path in product(range(p), repeat=depth):
+            need(len(path) == depth, "literal paid path")
+            for word in here:
+                columns[m**len(word)] += 1
+            for paid_position in range(p):
+                need(0 <= paid_position < p, "literal paid position")
+                if depth == height:
+                    need(here == {()}, "leaf unit exists")
+                    leaf_cuts += 1
+                else:
+                    boundary_cuts += bool(here - below)
+                    for word in below - here:
+                        sources[m**len(word)] += 1
+                        if first_source is None:
+                            first_source = depth + 1
+    return {"sources": dict(sources), "columns": dict(columns),
+            "leaf_cuts": leaf_cuts, "boundary_cuts": boundary_cuts,
+            "source_depth": first_source}
+
+
+def height_at(n, m, rule):
+    kind, base, multiplier = rule
+    if kind == "default":
+        return floor_log(n // m, m)
+    if kind == "fixed":
+        return multiplier
+    need(kind == "adaptive", "height rule")
+    return multiplier * floor_log(n // m, base)
+
+
+def width_table(m, w, p, maximum, rule, literal=False):
+    integer(maximum, m, 1024)
+    widths = [1] * (maximum + 1)
+    for n in range(m, maximum + 1):
+        height = height_at(n, m, rule)
+        flow = literal_flow(m, w, p, n, height) if literal else closed_flow(m, w, p, n, height)
+        need(len(flow["sources"]) == 1, "one source rank")
+        (source_rank, count), = flow["sources"].items()
+        complement = n - source_rank
+        replication = widths[complement] // gcd(widths[complement], count)
+        # Every leaf is a separate (rank 1, count 1) batch; B_1=1.
+        need(widths[1] == 1 and flow["boundary_cuts"] == 0, "complete cut reduction")
+        widths[n] = count * replication
+        need(replication * count % widths[complement] == 0, "whole complement batch")
+        need(widths[n] == lcm(count, widths[complement]), "gcd cancellation")
+    return widths
+
+
+def chain_width(m, w, p, n, rule):
+    """Evaluate the new decreasing-chain LCM, without a table of widths."""
+    integer(n, 0, 1024)
+    result, remaining = 1, n
+    for _ in range(n // m + 1):
+        if remaining < m:
+            return result
+        flow = closed_flow(m, w, p, remaining, height_at(remaining, m, rule))
+        (rank, count), = flow["sources"].items()
+        result = lcm(result, count)
+        remaining -= rank
+    raise ValueError("subtraction chain capacity")
+
+
+def check_flows():
+    fixtures, literal_leaves, empty_roots = 0, 0, 0
+    for m, w, p in product(range(2, 7), range(1, 4), range(1, 4)):
+        ranks = {m, m + 1, 2 * m - 1, m*m - 1, m*m, m*m + 1, 63, 127}
+        for n, height in product(sorted(ranks), range(6)):
+            actual = literal_flow(m, w, p, n, height)
+            predicted = closed_flow(m, w, p, n, height)
+            need(actual == predicted, "literal forest agrees with new formula")
+            source_mass = sum(rank * count for rank, count in actual["sources"].items())
+            column_mass = sum(rank * count for rank, count in actual["columns"].items())
+            need(source_mass - actual["leaf_cuts"] == (m*w - p)*column_mass,
+                 "exact rank invoice")
+            fixtures += 1
+            literal_leaves += actual["leaf_cuts"]
+            empty_roots += actual["source_depth"] > 0
+    return {"forest_fixtures": fixtures, "enumerated_leaf_cuts": literal_leaves,
+            "empty_root_fixtures": empty_roots}
+
+
+def check_widths():
+    fixtures, coordinates, literal_tables, strict = 0, 0, 0, 0
+    rules = [("default", 0, 0), ("fixed", 0, 0), ("fixed", 0, 4),
+             ("adaptive", 2, 2), ("adaptive", 3, 3), ("adaptive", 8, 4)]
+    for m, w, p, rule in product(range(2, 7), range(1, 5), range(1, 5), rules):
+        widths = width_table(m, w, p, 256, rule)
+        for n in range(m, 257):
+            need(widths[n] == chain_width(m, w, p, n, rule), "exact chain LCM")
+            if rule[0] == "default":
+                need(widths[n] == w**floor_log(n, m), "default closed form")
+            divisor = w**floor_log(n, m) * p**height_at(n, m, rule)
+            need(divisor % widths[n] == 0, "polynomial divisor")
+            coordinates += 1
+        fixtures += 1
+    for m, w, p in product(range(2, 5), range(1, 4), range(1, 4)):
+        literal = width_table(m, w, p, 63, ("default", 0, 0), literal=True)
+        formula = width_table(m, w, p, 63, ("default", 0, 0))
+        need(literal == formula, "independent literal-batch widths")
+        literal_tables += 1
+        strict += sum(width > 1 for width in literal)
+    return {"width_tables": fixtures, "width_coordinates": coordinates,
+            "literal_width_tables": literal_tables,
+            "nonunit_literal_widths": strict}
+
+
+def expect_rejection(values):
+    try:
+        closed_flow(*values)
+    except ValueError as error:
+        need(str(error) == "integer domain", "specific domain rejection")
+        return
+    raise ValueError("invalid input accepted")
+
+
+def check_controls():
+    invalid = [(1,2,3,8,2), (True,2,3,8,2), (17,2,3,32,2),
+               (2,0,3,8,2), (2,17,3,8,2), (2,2,False,8,2),
+               (2,2,0,8,2), (2,2,17,8,2), (2,2,3,1,2),
+               (2,2,3,2**257,2), (2,2,3,8,-1), (2,2,3,8,257)]
+    for values in invalid:
+        expect_rejection(values)
+    empty = literal_flow(2, 2, 3, 2, 3)
+    widths = width_table(2, 2, 3, 8, ("default", 0, 0))
+    fixed = width_table(2, 2, 3, 10, ("fixed", 0, 2))
+    first = closed_flow(2, 2, 3, 8, 0)
+    second = closed_flow(2, 2, 3, 6, 3)
+    controls = [
+        (empty["sources"] == {2:54} and empty["source_depth"] == 3,
+         "empty parents cannot be pruned"),
+        (empty["leaf_cuts"] == 81, "occurrences are distinct cuts"),
+        (closed_flow(2, 2, 3, 8, 2)["sources"] == {8:8}, "target multiplicity"),
+        (widths[6] == 4 and 4*widths[2] == 8, "omitted gcd overpays"),
+        (chain_width(2, 2, 3, 8, ("fixed", 0, 0)) == 2 != widths[8],
+         "height is part of the contract"),
+        (fixed[10] == 72 and max(8, 18) == 18, "LCM is not maximum"),
+        (first["sources"] == {2:2} and second["sources"] == {4:36}
+         and 2 * (36 // gcd(36, 2)) == 36, "arbitrary-height cancellation")]
+    for condition, message in controls:
+        need(condition, message)
+    return {"invalid_input_rejections": len(invalid),
+            "semantic_control_groups": len(controls)}
+
+
+def check_capacities():
+    large = closed_flow(2, 16, 16, 2**256, 256)
+    controls = [
+        (floor_log(2**256, 2) == 256, "maximum logarithm"),
+        (large["sources"] == {2**256:16**257}
+         and len(large["columns"]) == 256, "maximum closed formula"),
+        (chain_width(2, 2, 3, 1024, ("fixed", 0, 0)) == 2,
+         "maximum subtraction chain"),
+        (len(width_table(2, 1, 1, 1024, ("fixed", 0, 0))) == 1025,
+         "maximum width table")]
+    for condition, message in controls:
+        need(condition, message)
+    return {"capacity_controls": len(controls)}
+
+
+def file_hashes():
+    folder = Path(__file__).resolve().parent
+    hashes = {}
+    for name in FILES:
+        with (folder / name).open("rb") as source:
+            raw = source.read(2**21 + 1)
+        need(len(raw) <= 2**21, "package file capacity")
+        hashes[name] = sha256(raw).hexdigest()
+    return hashes
+
+
+def main():
+    receipt = {"claim_type": "scoped written proof with exact finite corroboration"}
+    receipt.update(check_flows())
+    receipt.update(check_widths())
+    receipt.update(check_controls())
+    receipt.update(check_capacities())
+    default = chain_width(2, 2, 3, 1023, ("default", 0, 0))
+    need(default == 512, "default numerical example")
+    receipt["example"] = {"m":2, "W":2, "P":3, "rank":1023,
+                          "least_width":default, "gcd_free_width":2**45}
+    receipt["package_sha256"] = file_hashes()
+    print(json.dumps(receipt, sort_keys=True, indent=2))
+    print("PASS_HOMOGENEOUS_GCD_WIDTH")
+
+
+if __name__ == "__main__":
+    main()