From 752c83ddaff26003c4c7e15f51804dc946cd6696 Mon Sep 17 00:00:00 2001
From: zxv <zxv@zxv>
Date: Tue, 27 Oct 2026 23:19:14 -0400
Subject: [PATCH 1/3] Align current CI navigation with selected PR6030

---
 docs/ci-verification.md         | 19 ++++++++++++++++++-
 docs/research/current-status.md |  2 +-
 2 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/docs/ci-verification.md b/docs/ci-verification.md
index 006bf5a3d5..63ba3e9aa8 100644
--- a/docs/ci-verification.md
+++ b/docs/ci-verification.md
@@ -1,6 +1,23 @@
 # CI verification
 
-## Current selected-family replay: #5599
+## Current selected-family replay: #6030
+
+The [selected record](../certificates/selected-result.json) binds conditional
+κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md),
+[validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json),
+and [explicit source closure](../certificates/frontier6030-source.json).
+`make frontier6030-verify` follows that source-bound selected replay. The review
+separates retained normal primary macOS/Linux evidence from fresh independent
+word/invoice/native, original caller, adapted caller and optimized primary checks.
+Consult its receipts for exact commands, source heads and limits; the #5599
+checkpoint below retains its own historical replay details.
+
+The five inherited framework assumptions remain. Neither the full uniform word
+nor a complete rounded multiplier is materialized. A source/metadata check is
+not an operator replay or a formal theorem proof. Routine research submissions
+do not need to rerun this selected-family replay.
+
+## Historical selected-family replay: #5599
 
 The [selected record](../certificates/selected-result.json) binds conditional
 κ = 0.00310045 to the [proof review](research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md)
diff --git a/docs/research/current-status.md b/docs/research/current-status.md
index a84ac12213..c49a245adc 100644
--- a/docs/research/current-status.md
+++ b/docs/research/current-status.md
@@ -1,6 +1,6 @@
 # Current reviewed status
 
-Selected conditional κ: **0.003125804 = 781451/250000000**, DreamingOfClouds'
+Selected conditional κ: **0.003125804** = 781451/250000000, DreamingOfClouds'
 PR6030 on the cumulative P104 construction. The complete caller counts 13,444
 productive fields and 66,834 paid calls. The saving is about 0.81775% above the
 preceding selected PR5599 claim 0.00310045.

From 25969a548a6862fd4e40a1b3b658868066e0f986 Mon Sep 17 00:00:00 2001
From: zxv <zxv@zxv>
Date: Wed, 28 Oct 2026 00:07:13 -0400
Subject: [PATCH 2/3] Prove sharp two-channel gains from each added dyadic cut
 coordinate

---
 research/dyadic-cut-enlargement/README.md    | 188 +++++++++++++++++++
 research/dyadic-cut-enlargement/SOURCES.json |  36 ++++
 research/dyadic-cut-enlargement/TASK.json    |  79 ++++++++
 research/dyadic-cut-enlargement/VERIFY.json  |  34 ++++
 research/dyadic-cut-enlargement/verify.py    | 115 ++++++++++++
 5 files changed, 452 insertions(+)
 create mode 100644 research/dyadic-cut-enlargement/README.md
 create mode 100644 research/dyadic-cut-enlargement/SOURCES.json
 create mode 100644 research/dyadic-cut-enlargement/TASK.json
 create mode 100644 research/dyadic-cut-enlargement/VERIFY.json
 create mode 100644 research/dyadic-cut-enlargement/verify.py

diff --git a/research/dyadic-cut-enlargement/README.md b/research/dyadic-cut-enlargement/README.md
new file mode 100644
index 0000000000..8a5c62d729
--- /dev/null
+++ b/research/dyadic-cut-enlargement/README.md
@@ -0,0 +1,188 @@
+# One extra cut coordinate can restore two dyadic helper channels
+
+In the fixed-prefix dyadic helper interface of
+[Ali Romman](https://github.com/aliromman)'s
+[PR #5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615), enlarging
+the eligible cut by $d$ scalar coordinates changes its unit-channel capacity by
+at most $2d$. The bound is sharp for every positive integer $d$.
+One added coordinate can therefore unlock **two** channels, not just one.
+
+The attaining example is source-relative: the exact three-coordinate causal
+fixture already present in #5615 has capacity zero on its restricted two-coordinate
+cut and capacity two when its third coordinate becomes eligible. No prefix,
+suffix or helper target is changed. Its complete arbitrary-dirty identity word
+costs 12 signed scalar ADDs. Repeating independent blocks attains the $2d$ gain
+with $d$ extra eligible coordinates and a full cost of $12d$ ADDs.
+
+This is a scoped cut-module theorem and calibration construction, not a native
+P104 realization, productive-target split, selected-frontier change or new κ.
+Eligibility is a changed contract; permitting the third coordinate at a physical
+common chart and delivering its channels remain separate obligations.
+
+## Fixed contract and sharp bound
+
+Let $D=\mathbb{Z}[1/2]$. Keep the prefix $A$, suffix $B$, helper input/output
+support $G$, and complete endpoint fixed. Let $E$ be the dyadic row module
+whose prefix image has support in $G$, and let $H$ be the corresponding suffix
+column module. For eligible coordinate supports $F\subseteq F'$, define
+
+$$
+L=F\cap E,\qquad L'=F'\cap E,
+\qquad R=F\cap H,\qquad R'=F'\cap H.
+$$
+
+The row/column copies of a coordinate module are identified in this notation.
+Suppose $F'/F$ has rank $d$. With full dyadic bases, form the old and new
+pairings $K$ and $K'$. Let $c(K)$ be the largest $t$ for which dyadic matrices
+$X,Y$ satisfy $XKY=I_t$. Then
+
+$$
+\boxed{0\leq c(K')-c(K)\leq2d.}
+$$
+
+**Proof.** The quotient $L'/L$ injects into $F'/F$: its kernel consists precisely
+of those eligible rows already in $F$. It is therefore a free $D$-module of rank
+$a\leq d$. The short exact sequence splits, so every full basis of $L$ extends
+to one of $L'$. Likewise a full basis of $R$ extends by $b\leq d$ columns.
+Thus compatible choices of full bases put $K$ in the upper-left block of $K'$.
+
+Padding old $X,Y$ with zeros shows $c(K')\geq c(K)$. By #5615's single-cut
+criterion, some odd prime $p$ attains $c(K)$ as the rank of $K$ modulo $p$.
+Adding $a$ rows and $b$ columns can raise rank by at most $a+b$. Consequently
+
+$$
+c(K')\leq r_p(K')\leq r_p(K)+a+b\leq c(K)+2d,
+$$
+
+where $r_p$ denotes rank modulo $p$. This proves the bound. The argument does
+not require the added channels to be simple tensors or to use coordinate bases
+inside the eligible modules. ∎
+
+The proof requires a **fixed** prefix, suffix, helper support and embedding of
+the old cut into the new one. A different program or helper endpoint need not
+contain the old pairing block. The theorem then supplies no capacity bound.
+
+## Exact source fixture: zero becomes two
+
+The retained fixture has prefix and inverse suffix
+
+$$
+A=\begin{pmatrix}1&0&1\\0&1&2\\1&2&6\end{pmatrix},
+\qquad
+B=\begin{pmatrix}2&2&-1\\2&5&-2\\-1&-2&1\end{pmatrix}.
+$$
+
+Take helper support $G$ on the first two original coordinates. On the old cut
+$F$, also supported on the first two physical coordinates, the full eligible
+row and column bases are both $(-2,1)$. Their pairing is $[5]$, with rational
+rank one but zero dyadic unit capacity: reduction modulo five has rank zero.
+
+Now allow the third physical coordinate, so $F'$ is the whole ambient space.
+Full eligible bases are the first two rows of $B$ and the first two columns
+of $A$. Their pairing is $I_2$, since $BA=I_3$. The new capacity is exactly two.
+These are full module bases: invertibility over $D$ identifies them with all
+helper-supported rows and columns. No clean-input assumption is used. In bases
+that extend the old ones, the enlarged pairing is
+
+$$
+K'=\begin{pmatrix}5&-2\\-2&1\end{pmatrix},
+\qquad 5\cdot1-(-2)^2=1.
+$$
+
+Its old upper-left block is still $[5]$, while the whole block is a unit.
+
+The exact prefix, in current-value semantics, is
+
+```text
+x0 += z
+x1 += z
+x1 += z
+z  += x0
+z  += x1
+z  += x1
+```
+
+The suffix executes these instructions in reverse order with minus signs.
+All three independent dirty inputs are restored. The complete word has 12
+signed ADDs and uses the same three coordinates before and after changing the
+eligible support. No allocation or basis conversion is silently added to this
+calibration word. Realizing the changed eligibility and channel delivery in a
+native supplier is not provided or priced as zero.
+
+For $d$ independent blocks, the old pairing is $5I_d$ and the enlarged pairing
+is $I_{2d}$. Adding all $d$ third coordinates therefore attains the bound $2d$.
+If only $s$ third coordinates become eligible, the exact capacity is $2s$.
+This also gives every intermediate even gain in the family.
+
+## A necessary size for a nonproduct rescue
+
+[Nick Petalas](https://github.com/petalas)'s
+[PR #5882](https://github.com/CrocSwap/integer-mult-bounds/pull/5882) proves that
+an algebraic repeated pairing $K$ has tensor capacity $c(K)^f$ and rational
+rank $r(K)^f$. Suppose an actual product cut has this exact pairing. Any
+fixed-prefix enlargement that raises its capacity to at least $r(K)^f$ must add
+
+$$
+d\geq\left\lceil\frac{r(K)^f-c(K)^f}{2}\right\rceil
+$$
+
+eligible scalar coordinates. This follows by applying the sharp bound to the
+whole tensor cut. It does not assume that the enlarged cut itself factors.
+This is a coordinate-availability requirement, not a paid-job or storage tariff:
+newly eligible coordinates may already exist. Their native charts, timing and
+delivery still require a separate source-bound bill.
+
+## Evidence and reproduction
+
+```
+python3.12 -B scripts/research_package.py --package research/dyadic-cut-enlargement
+python3.12 -B scripts/check_research_commit.py --package research/dyadic-cut-enlargement
+```
+
+The verifier authenticates the unchanged #5615 kernel/capacity source and the
+#5882 proof. It reconstructs every ADD of the scalar words, independently solves
+the complete row/column eligibility constraints, and checks all partial support
+enlargements of one through six independent blocks. It verifies literal full
+unit-block witnesses and modular upper bounds, including odd and dyadic-scaled
+coefficient controls. A separate small bordered-matrix census corroborates the
+rank bound. Wrong cut supports, a nonsaturated basis, false one-channel gain
+bounds and a changed prefix are rejected. Normal and optimized replays use
+explicit checks and write no package files.
+
+Canonical main was refreshed on 2026-10-28 UTC at
+721c03822c421b7f7fcbb2598993b947c4d88419, priority 8. The navigation repair
+from [PR #6050](https://github.com/CrocSwap/integer-mult-bounds/pull/6050) is
+included; frozen packages and the selected record are unchanged. No selected
+cold replay ran. The optional full-history preflight is unavailable in this
+shallow checkout; all declared pins use its reachable base.
+
+## Significance for researchers
+
+A zero-capacity restricted cut need not remain useless after one legal support
+change. Conversely, each extra eligible coordinate can recover at most two
+channels while the program is fixed. This supplies a sharp optimistic resource
+screen for nonproduct support changes beyond
+[PR #6054](https://github.com/CrocSwap/integer-mult-bounds/pull/6054)'s product-cut
+obstruction. It does not grant the physical common-chart or consumer contract.
+
+## Open next questions
+
+Can one actual native helper cut make an outside coordinate eligible at a paid
+cost that its additional channels can fund? First extract the fixed prefix,
+suffix and complete support embedding, then prove legal chart/timing and delivery.
+The scalar fixture alone does not supply those conditions.
+
+Can changed prefixes or helper endpoints beat the fixed-program two-per-coordinate
+bound at a favorable complete invoice? First name the changed map and preserve
+all independent dirty inputs. Such changes lie outside this theorem.
+
+## Credit
+
+Prepared by [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance.
+[Ali Romman](https://github.com/aliromman) supplies the single-cut theorem,
+source fixture and unchanged saturated-kernel code in #5615.
+[Nick Petalas](https://github.com/petalas) supplies #5882's tensor formula.
+Their methods and prior attribution remain intact. Module splitting over a PID
+and bordered-matrix rank bounds are classical. The contribution is their sharp
+fixed-cut enlargement implication and the source-relative attaining family.
+No independent human or proof-assistant review is claimed. Apache-2.0.
diff --git a/research/dyadic-cut-enlargement/SOURCES.json b/research/dyadic-cut-enlargement/SOURCES.json
new file mode 100644
index 0000000000..19559ccffb
--- /dev/null
+++ b/research/dyadic-cut-enlargement/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "752c83ddaff26003c4c7e15f51804dc946cd6696",
+  "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/dyadic-helper-channel-capacity/PROOF.md",
+      "usage": "input",
+      "git_blob": "c97a6edce3070414c81f0ef6e6c099ebb17f3a90",
+      "sha256": "b258a217f2cd0fc48461285fe8ae24de26b0c5963668d9d8f0955fc6e759e929"
+    },
+    {
+      "path": "research/dyadic-helper-channel-capacity/capacity.py",
+      "usage": "input",
+      "git_blob": "d882eb6d049125c67d4c0d47dced60bf0e181268",
+      "sha256": "1cd82b0beab7983d955cfc1d1e562af490f90bcaad6e3ec7d07e0c5a33608834"
+    },
+    {
+      "path": "research/tensor-helper-capacity/PROOF.md",
+      "usage": "input",
+      "git_blob": "09f921ccdc6fbd289d46e1d7d9620b20fd72c0d7",
+      "sha256": "4621e2a382ce0b077aa70a392b5e0b2cdec14e550a369558d795431e14e17262"
+    }
+  ]
+}
diff --git a/research/dyadic-cut-enlargement/TASK.json b/research/dyadic-cut-enlargement/TASK.json
new file mode 100644
index 0000000000..c55a60ca84
--- /dev/null
+++ b/research/dyadic-cut-enlargement/TASK.json
@@ -0,0 +1,79 @@
+{
+  "schema_version": 1,
+  "task_id": "coverage-law-change",
+  "priority_revision": 8,
+  "base_commit": "752c83ddaff26003c4c7e15f51804dc946cd6696",
+  "original_card": {
+    "id": "coverage-law-change",
+    "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "target credit",
+      "helper split",
+      "coverage law"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp two-per-coordinate bound for dyadic cut enlargement at a fixed prefix/suffix, with the source K=[5] calibration attaining every even partial gain.",
+  "scope_change_reason": "Broader lateral research changes cut eligibility beyond the prior product-support model. This is a module/coordinate screen, not a physical productive-target construction.",
+  "bottleneck_link": "Quantifies both a genuine support escape and the number of newly eligible coordinates a fixed-program tensor rescue needs.",
+  "budget_minutes": 15,
+  "stop_rule": "Stop after the sharp module theorem and complete scalar calibration; no native implementation campaign.",
+  "outcome": "completed",
+  "evidence": "README.md proof; verify.py exact full words, saturated kernels, unit blocks and modular upper bounds.",
+  "author": "zxv (https://github.com/zxv), with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "Can a native cut legally admit one outside coordinate at an affordable complete bill?",
+      "why_it_matters": "Needed to turn the algebraic two-channel gain into productive supplier credit.",
+      "first_step": "Extract fixed prefix/suffix and support embedding, then price chart/timing/delivery.",
+      "blocked_by": "No native carrier or consumer is provided."
+    },
+    {
+      "question": "Can a changed prefix beat the fixed-program bound economically?",
+      "why_it_matters": "A different prefix is a distinct reopening condition.",
+      "first_step": "Name one changed map and check arbitrary-dirty endpoints before pricing it.",
+      "blocked_by": "The theorem fixes both prefix and suffix."
+    }
+  ]
+}
diff --git a/research/dyadic-cut-enlargement/VERIFY.json b/research/dyadic-cut-enlargement/VERIFY.json
new file mode 100644
index 0000000000..6cacbe3dc5
--- /dev/null
+++ b/research/dyadic-cut-enlargement/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/dyadic-helper-channel-capacity/PROOF.md",
+    "research/dyadic-helper-channel-capacity/capacity.py",
+    "research/tensor-helper-capacity/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Full arbitrary-dirty scalar words, every partial cut through six blocks, saturated kernels, unit witnesses, modular rank census and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Identical exact checks with assertions disabled."
+    }
+  ]
+}
diff --git a/research/dyadic-cut-enlargement/verify.py b/research/dyadic-cut-enlargement/verify.py
new file mode 100644
index 0000000000..0aecfd654e
--- /dev/null
+++ b/research/dyadic-cut-enlargement/verify.py
@@ -0,0 +1,115 @@
+"""Sharp fixed-cut capacity enlargement; exact finite corroboration. Apache-2.0."""
+from fractions import Fraction as Q
+from itertools import product as words
+from pathlib import Path
+import hashlib
+import importlib.util
+import json
+
+HERE=Path(__file__).resolve().parent
+ROOT=HERE.parents[1]
+
+
+def need(ok,msg):
+    if not ok:raise ValueError(msg)
+
+
+def eye(n):return [[int(i==j) for j in range(n)] for i in range(n)]
+def tr(a):return [list(x) for x in zip(*a)]
+def mm(a,b):return [[sum(x*y for x,y in zip(row,col)) for col in zip(*b)] for row in a]
+
+
+def rank_mod(a,p):
+    a=[[int(x)%p for x in row] for row in a]
+    m=len(a);n=len(a[0]) if m else 0;i=0
+    for j in range(n):
+        k=next((k for k in range(i,m) if a[k][j]),None)
+        if k is None:continue
+        a[i],a[k]=a[k],a[i];u=pow(a[i][j],-1,p)
+        a[i]=[x*u%p for x in a[i]]
+        for k in range(m):
+            if k!=i:
+                u=a[k][j];a[k]=[(x-u*y)%p for x,y in zip(a[k],a[i])]
+        i+=1
+        if i==m:break
+    return i
+
+
+def full_word(d):
+    n=3*d;a=eye(n);events=[]
+    for block in range(d):
+        x,y,z=range(3*block,3*block+3)
+        events.extend([(x,z,1),(y,z,1),(y,z,1),(z,x,1),(z,y,1),(z,y,1)])
+    for dst,src,c in events:a[dst]=[x+c*y for x,y in zip(a[dst],a[src])]
+    b=eye(n)
+    for dst,src,c in reversed(events):b[dst]=[x-c*y for x,y in zip(b[dst],b[src])]
+    need(mm(a,b)==mm(b,a)==eye(n),'full arbitrary-dirty restoration')
+    need(2*len(events)==12*d,'full signed ADD bill')
+    return a,b
+
+
+def pairing(a,b,f,g,kernel):
+    out=[j for j in range(len(a)) if j not in g]
+    l=tr(kernel([[a[i][j] for i in f] for j in out],len(f)))
+    r=kernel([[b[j][i] for i in f] for j in out],len(f))
+    return mm(l,r),l,r
+
+
+def rejected(fn):
+    try:fn()
+    except ValueError:return
+    raise ValueError('negative control accepted')
+
+
+def main():
+    pins=json.loads((HERE/'SOURCES.json').read_text())
+    for row in pins['files']:
+        if row['usage']=='input':
+            need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'source bytes')
+    path=ROOT/'research/dyadic-helper-channel-capacity/capacity.py'
+    spec=importlib.util.spec_from_file_location('retained_capacity',path)
+    old=importlib.util.module_from_spec(spec);spec.loader.exec_module(old)
+    subsets=0
+    for d in range(1,7):
+        a,b=full_word(d);g=[j for j in range(3*d) if j%3!=2]
+        k,l,r=pairing(a,b,g,g,old.kernel)
+        need(k==[[5*int(i==j) for j in range(d)] for i in range(d)],'old full pairing')
+        need(rank_mod(k,5)==old.capacity(k)['capacity']==0,'zero old capacity')
+        for bits in words((0,1),repeat=d):
+            added=[3*i+2 for i,x in enumerate(bits) if x]
+            f=sorted(g+added);s=sum(bits)
+            k,l,r=pairing(a,b,f,g,old.kernel);c=old.capacity(k)
+            need(c['capacity']==2*s,'exact partial enlargement')
+            need(c['rational_rank']==d+s,'full kernel dimensions')
+            need(rank_mod(k,5)==2*s,'modular upper bound')
+            if s:need(mm(mm(c['left'],k),c['right'])==eye(2*s),'literal unit block')
+            subsets+=1
+    # Independent field-rank census of every 2x2 bordering of a 1x1 block.
+    bordered=0
+    for p in (3,5):
+        for entries in words(range(p),repeat=4):
+            a=[[entries[0],entries[1]],[entries[2],entries[3]]]
+            need(0<=rank_mod(a,p)-int(entries[0]!=0)<=2,'bordered rank bound')
+            bordered+=1
+    a,b=full_word(1)
+    need(a==[[1,0,1],[0,1,2],[1,2,6]],'source literal prefix')
+    need(b==[[2,2,-1],[2,5,-2],[-1,-2,1]],'source literal suffix')
+    l=[b[0],b[1]];r=[[a[i][0],a[i][1]] for i in range(3)]
+    need(mm(l,r)==eye(2),'full-cut source witness')
+    u=[[-2,1],[1,0]]
+    need(mm(mm(u,mm(l,r)),u)==[[5,-2],[-2,1]],'compatible bordered bases')
+    need(old.capacity([[5,-2],[-2,1]])['capacity']==2,'sharp bordered unit')
+    need(old.capacity([[Q(5,8)]])['capacity']==0,'dyadic scaling cannot invert five')
+    need(old.capacity([[1,0],[0,5]])['capacity']==1,'mixed unit/nonunit control')
+    rejected(lambda:need(2<=1,'false one-channel-per-coordinate bound'))
+    rejected(lambda:need(old.capacity([[15]])['capacity']==1,'odd scaling false unit'))
+    rejected(lambda:old.capacity([[Q(1,3)]]))
+    bad=[row[:] for row in a];bad[0][0]+=1
+    rejected(lambda:need(mm(bad,b)==eye(3),'changed prefix'))
+    rejected(lambda:need(mm([[3*x for x in row] for row in l],r)==eye(2),'nonsaturated basis'))
+    print(json.dumps(dict(status='PASS_DYADIC_CUT_ENLARGEMENT',support_enlargements=subsets,
+                         bordered_matrices=bordered,sharp_gain_per_coordinate=2,
+                         scope='fixed-prefix module theorem and scalar calibration; no new kappa'),sort_keys=True))
+
+
+if __name__=='__main__':main()

From 5fd1fdedddf32307db31416958a1f03a8a67aa16 Mon Sep 17 00:00:00 2001
From: zxv <zxv@zxv>
Date: Wed, 28 Oct 2026 00:36:37 -0400
Subject: [PATCH 3/3] Clarify reuse of the retained saturated-kernel
 implementation

---
 research/dyadic-cut-enlargement/README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/research/dyadic-cut-enlargement/README.md b/research/dyadic-cut-enlargement/README.md
index 8a5c62d729..312b56bc97 100644
--- a/research/dyadic-cut-enlargement/README.md
+++ b/research/dyadic-cut-enlargement/README.md
@@ -140,8 +140,8 @@ python3.12 -B scripts/check_research_commit.py --package research/dyadic-cut-enl
 ```
 
 The verifier authenticates the unchanged #5615 kernel/capacity source and the
-#5882 proof. It reconstructs every ADD of the scalar words, independently solves
-the complete row/column eligibility constraints, and checks all partial support
+#5882 proof. It reconstructs every ADD of the scalar words, solves the complete row/column eligibility constraints with the retained kernel
+routine, and checks all partial support
 enlargements of one through six independent blocks. It verifies literal full
 unit-block witnesses and modular upper bounds, including odd and dyadic-scaled
 coefficient controls. A separate small bordered-matrix census corroborates the