From 8c5e1cf07c23d843642bf2d4c76f882669edc43f Mon Sep 17 00:00:00 2001
From: Evan McKinney <evmckinney9@gmail.com>
Date: Fri, 9 Oct 2026 09:27:01 -0400
Subject: [PATCH] Pack completed PR187 bit residuals with the PR193 complex
 supplier

---
 .../workflows/packed-source-assisted-bit.yml  |  38 +++
 research/packed-source-assisted-bit/PROOF.md  | 193 ++++++++++++
 research/packed-source-assisted-bit/README.md |  48 +++
 .../packed-source-assisted-bit/SOURCE.json    |  12 +
 .../packed-source-assisted-bit/arithmetic.py  |  95 ++++++
 research/packed-source-assisted-bit/audit.py  |  77 +++++
 .../certificate.json                          | 283 ++++++++++++++++++
 .../packed-source-assisted-bit/controls.py    |  35 +++
 .../packed-source-assisted-bit/packing.py     | 186 ++++++++++++
 research/packed-source-assisted-bit/verify.py |  69 +++++
 10 files changed, 1036 insertions(+)
 create mode 100644 .github/workflows/packed-source-assisted-bit.yml
 create mode 100644 research/packed-source-assisted-bit/PROOF.md
 create mode 100644 research/packed-source-assisted-bit/README.md
 create mode 100644 research/packed-source-assisted-bit/SOURCE.json
 create mode 100644 research/packed-source-assisted-bit/arithmetic.py
 create mode 100644 research/packed-source-assisted-bit/audit.py
 create mode 100644 research/packed-source-assisted-bit/certificate.json
 create mode 100644 research/packed-source-assisted-bit/controls.py
 create mode 100644 research/packed-source-assisted-bit/packing.py
 create mode 100644 research/packed-source-assisted-bit/verify.py

diff --git a/.github/workflows/packed-source-assisted-bit.yml b/.github/workflows/packed-source-assisted-bit.yml
new file mode 100644
index 0000000000..7c2b657ddc
--- /dev/null
+++ b/.github/workflows/packed-source-assisted-bit.yml
@@ -0,0 +1,38 @@
+name: Verify packed source-assisted bit supplier
+on:
+  pull_request:
+    paths:
+      - 'research/packed-source-assisted-bit/**'
+      - 'research/source-assisted-v4/**'
+      - 'research/source-assisted/**'
+      - 'scripts/paired_cube_assembly.py'
+      - '.github/workflows/packed-source-assisted-bit.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  full:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          repository: CrocSwap/integer-mult-bounds
+          ref: 201737a1ec4f936e166e2481fb9e88104cb2ccc7
+          path: .dependencies/pr187
+          persist-credentials: false
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          repository: CrocSwap/integer-mult-bounds
+          ref: 187e1010ac8b259af8e9b5166f68b64bc27b4b47
+          path: .dependencies/pr193
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.13'
+      - run: python -m pip install -r .dependencies/pr193/research/source-assisted/requirements-round13.txt
+      - run: python -B research/packed-source-assisted-bit/verify.py --complex-root .dependencies/pr193 --bit-root .dependencies/pr187 --full
+      - run: git diff --exit-code
diff --git a/research/packed-source-assisted-bit/PROOF.md b/research/packed-source-assisted-bit/PROOF.md
new file mode 100644
index 0000000000..295b7974b8
--- /dev/null
+++ b/research/packed-source-assisted-bit/PROOF.md
@@ -0,0 +1,193 @@
+# Completed entrance banks on the emitted PR187 bit word
+
+This applies completed-bank packing, also used in PR186, to PR187's bit
+word. It retains PR187/193's conditional all-size interfaces.
+
+## 1. Actual physical chains
+
+Use immutable PR187 commit `201737a1ec4f936e166e2481fb9e88104cb2ccc7`.
+Its unmodified full gate emits and independently checks the complete bit
+word, including source controls, target chronology, all source/target/dirty
+columns, inverse cleanup, prime coverage, and the paid child histogram.
+It has 19,348 logical auxiliary roles and 1,760 donor/recipient splices,
+hence 17,588 physical chains. There are 3,960 logical gauges:
+
+- 1,760 rank-21 gauges are recipient starts internal to the paid splices;
+- 2,200 rank-20 gauges are starts of otherwise unpaired physical chains.
+
+No donor is gauged; donors and recipients are disjoint. The checker verifies
+these properties from the emitted word. Only the second group supplies
+rank-four entrance residuals. Every other physical chain has rank-24
+residual. Interior recipient starts are not counted again as packable ends.
+All source, target, copied-center, compensated-read and internal operations
+remain in the word and in the retained histogram.
+
+## 2. Exact charts
+
+For each of the 220 distinct rank-20 gauge frames sigma=ker A in Q^24,
+use the form G=9I-J. Its G-orthogonal complement has basis obtained from
+rows a of A by 15a-(sum a)1. Put these four vectors before a basis of sigma
+as the columns of B. The checker verifies orthogonality, both inverse
+identities for B, and an independent replay of its elementary factors.
+Thus the residual projector I-P_sigma becomes diag(I_4,0) in this chart.
+A nongauged residual is I_24.
+
+All charts have at most 186 elementary factors, coefficient numerator
+magnitude at most five and denominator at most eighteen. The exact factors
+and integral inverse determinants are checked; all their nonzero integers
+are below 2^80. They remain invertible at every inherited allowed prime
+q>2^80. These are address charts, not new complex payload coefficients.
+They do not change PR193's dyadic scalar word.
+
+Embed each chart into 72 coordinates at its original tensor stage and
+permute its residual coordinates into the assigned bank interval. This
+uses at most 71 coordinate transpositions in addition to the chart factors.
+Explicitly, take H=Pi B^-1, with the identity on the other tensor coordinates.
+Then H P H^-1=E for the original residual projector P and the assigned
+coordinate projector E. The routing below uses this direction of H.
+
+## 3. Banks and legal scheduling
+
+Take three full copies of the three-stage construction. Each physical
+chain occurs nine times. Partition its residual occurrences into
+
+- 3,300 banks of six rank-four and two rank-24 items;
+- 43,964 banks of three rank-24 items.
+
+Every bank has rank 72. The inventories are exact:
+
+    6 * 3300 = 9 * 2200,
+    2 * 3300 + 3 * 43964 = 9 * (17588-2200).
+
+The physical-chain/bank bipartite multigraph has degree nine on every
+chain and at most eight at every bank. A deterministic two-color-swap
+algorithm supplies a proper nine-edge-coloring. An independent check
+verifies all 158,292 incidences at both endpoints. A duplicate color at a
+chain is rejected. Color 3j+b denotes stage j and copy b. Thus every
+invocation receives every physical chain exactly once, no bank is used
+twice within a color batch, and each data copy retains its original stage
+order. No incomplete invocation is shared.
+
+For an item chart H and cover index g, connect bank (c,g) to its physical
+chain in core (color,gH). Right multiplication by H is a bijection of the
+full local-ring GL cover. Every core receives all required chains, and the
+data wiring is unchanged. This uses the inherited completed-core contract:
+the data map is independent of arbitrary initial scratch and the completed
+scratch endpoint separates the residual of each physical chain. PR187's
+internal source controls and compensated splices remain inside that core.
+
+## 4. Bank endpoint and arbitrary dirty data
+
+After the chart changes, a bank's residual projectors E_i have disjoint
+coordinate intervals and sum to I_72. Let D_P be the ordinary partial-swap
+involution associated with a projector P. For disjoint projectors,
+
+    D_P D_Q = D_(P+Q) = D_Q D_P.
+
+Conjugation by a common cover representative and by the common weighted
+address map preserves products. Hence the bank's weighted residual
+involutions commute and multiply to the required full weighted endpoint.
+The inherited ancestor weights are independent of the fresh selector
+fields changed by g -> gH; those ancestor fields remain spectators.
+This is an operator identity on arbitrary bank contents, not an assumption
+of zero-initialized scratch. The reverse order gives the same endpoint.
+
+Controls check both bank patterns on all 144 formal columns over Z/9,
+Z/25 and Z/125, with nonconstant unit weights in both orders. They reject
+omitted and repeated blocks. These checks support the identity above;
+they do not simulate the full cover or prove the inherited Clifford interface.
+
+## 5. Complete histogram and routing
+
+There are 47,264 banks and 3*3,520 data roles, giving W=57,824 and m=72.
+Take three copies of PR187's independently recounted histogram and remove
+exactly its 6,600 exterior children of rank 60. Every remaining child is
+retained. The bank endpoints already equal the required full endpoint,
+which justifies removing those exterior corrections.
+
+The resulting rank mass is 4,157,520, deficit 72W-mass=5,808, and maximum
+child rank 22. Dividing by three gives normalized W=57,824/3 and deficit
+1,936. The full integer profile is used for verification.
+
+Every retained edge still averages over a complete GL cover under a fixed
+bijection. Retain the bad-class allowance 10^-16 and 32m² fallback children
+per edge. No simultaneous good-class intersection is assumed.
+
+Routing is paid through the inherited ordinary selector, not treated as a
+unit tape instruction. For g=g_0+qX, right multiplication by each fixed H
+is a finite low-type permutation and an affine map of X, with carry fixed
+by g_0. Preserve complete spectators and restore all borrowed rows.
+Extending the injective allocation to a permutation and routing out and
+back gives the conservative additional selector-call bound
+
+    18 * ((57824-1) + 17588 * 72 * (186+71))
+      = 5,859,111,150.
+
+All original scalar work, source controls, readouts, data routing and
+cleanup remain paid. The extra calls cost O(K V w^(1-a_old)); they are not
+added as small recursive children. K is fixed independently of atom width.
+With w=ceil(e^c), this is at most O(K V e^c). The strictly positive gap
+c<1-a_ordinary absorbs it into the existing row/adapter toll, changing a
+fixed stopping constant rather than the exponent.
+
+W<q for q>2^80, and the maximum child ratio 22/72 is below one half.
+The GL stock and internally borrowed digits therefore keep the inherited
+O(w log e) digit order. There is no new external polynomial row reserve.
+The completed old ordinary selector used for the additional routes is the
+same leaf interface used by PR185/187's finite composition. Its all-size,
+weighted, restored-row and fixed-tape guarantees remain assumptions here.
+
+## 6. Exact moments and finite leaf composition
+
+For a profile H, certify the sufficient paid moment
+
+    sum_r H_r (r/m)^(1-c) / W
+      + 10^-16 * 32m * (#edges) * m^c / W < 1.
+
+Under the inherited recurrence, substituting a width power 1-c makes
+a rank-r child contribute (r/m)^(1-c). Division by W normalizes the
+parent stock. A strict moment below one gives contraction of the recursive
+term; the separate ordinary-leaf and routing tolls must still satisfy the
+strict inequalities below. The finite moment alone is not an all-size proof.
+
+The packed coarse saving is 676537710350481/10^18. The next 10^-18 grid
+point fails. A second, independent rational logarithm/exponential enclosure
+checks both sides of this exclusion and reproduces the original supplier's
+coarse saving. Packing strictly improves the paid moment at that original
+saving as well.
+
+Start from PR187's already completed ordinary supplier of saving a_0.
+Apply exactly three finite stopped-leaf levels using the packed coarse
+construction, atom exponent c, and the previous level for ordinary leaves,
+routing and high-part exchange:
+
+    a_j = (1-c)c+c a_(j-1) = c-c^j(c-a_0), j=1,2,3.
+
+This is an acyclic composition. All gaps a_j<c<1-a_j are positive fixed
+rationals. Each completed leaf restores its own borrowed rows and keeps
+outer fields as spectators. The old external leaf reserve remains unused
+slack, as in PR185's written proof; no new external stock or growing-depth
+program is assumed. This package does not substitute the unattained limit c.
+
+## 7. Assembly, comparison and limits
+
+Use PR193 commit `187e1010ac8b259af8e9b5166f68b64bc27b4b47` for the complex
+supplier. Its unchanged histogram has certified saving
+700918443859411/10^18 under the finer rational enclosure, above a_3.
+Keep its finite scalar/router and external-row bridge. The additional bit
+address routes are covered by the ordinary toll above. Set eta=beta=10^-24
+in the same 47-constraint balanced assembly. It certifies
+
+    kappa = 135216063303877/200000000000000000
+          = 0.000676080316519385.
+
+The next final 10^-18 grid point fails for these fixed supplies and
+parameters. The independent audit recomputes the finite leaf recurrence,
+all supplier moments and the final controlling margin. The inherited
+assembly recomputes all 47 strict inequalities and seven margins.
+
+No all-size compiler, analytic, precision, restored-row or fixed-tape
+hypothesis is proved here. PR193 retains its disclosed lack of a globally
+renumbered complex word and full Clifford/router replay. This is a
+conditional finite construction and composition, not an unconditional
+multiplication theorem or a practical speedup claim.
diff --git a/research/packed-source-assisted-bit/README.md b/research/packed-source-assisted-bit/README.md
new file mode 100644
index 0000000000..f138331020
--- /dev/null
+++ b/research/packed-source-assisted-bit/README.md
@@ -0,0 +1,48 @@
+# Packed source-assisted bit supplier
+
+Pack PR187's completed rank-4/rank-24 scratch residuals and combine the
+result with PR193's complex supplier:
+
+| Construction | Conditional kappa |
+|---|---:|
+| PR194 as published | 0.0006674324 |
+| PR193 complex + PR187 bit | 0.000670450176035363 |
+| Same suppliers, with packing | **0.000676080316519385** |
+
+Packing contributes **0.8398%**. The **1.2957%** gain over PR194 also includes
+supplier and arithmetic choices. [PROOF.md](PROOF.md) gives the construction,
+routing costs and inherited assumptions; [SOURCE.json](SOURCE.json) pins inputs.
+
+## Reproduce
+
+From the repository root, create the pinned dependency checkouts and run:
+
+```sh
+git fetch https://github.com/CrocSwap/integer-mult-bounds 201737a1ec4f936e166e2481fb9e88104cb2ccc7
+git worktree add --detach ../packed-bit-pr187 201737a1ec4f936e166e2481fb9e88104cb2ccc7
+git fetch https://github.com/CrocSwap/integer-mult-bounds 187e1010ac8b259af8e9b5166f68b64bc27b4b47
+git worktree add --detach ../packed-complex-pr193 187e1010ac8b259af8e9b5166f68b64bc27b4b47
+python3.13 -m pip install -r ../packed-complex-pr193/research/source-assisted/requirements-round13.txt
+python3.13 -B research/packed-source-assisted-bit/verify.py --complex-root ../packed-complex-pr193 --bit-root ../packed-bit-pr187 --full
+```
+
+This runs both unchanged upstream verifiers, regenerates charts and incidence
+assignments, and checks two exact moment engines, finite leaf composition,
+all 47 assembly inequalities, seven margins and corruption controls. The
+certificate stores the minimum constraint slack instead of all 47 slacks;
+every inequality is still recomputed. Add `--write` to regenerate it.
+Without `--full`, the checker uses the saved physical receipt and needs only
+Python 3.11+ and its standard library. Full regeneration uses Python 3.13
+to match the inherited complex verifier's gzip encoding.
+
+## Credit and scope
+
+Credit Avi Eisenberg for PR193; Rohan Arun for PR187; icekylinx for the
+source-assisted method and paired-cube framework; eumemic for PR168;
+and the preceding frame, reuse, balanced-layout and arithmetic contributors.
+Finite leaf composition follows PR185/187. Related completed banks appear
+in PR186; no new general packing mechanism is claimed. Original notices
+remain in the pinned checkouts. The full multiplication theorem remains
+conditional on the interfaces listed in the proof.
+
+Prepared with substantial OpenAI Codex assistance. Apache-2.0.
diff --git a/research/packed-source-assisted-bit/SOURCE.json b/research/packed-source-assisted-bit/SOURCE.json
new file mode 100644
index 0000000000..4b09a72293
--- /dev/null
+++ b/research/packed-source-assisted-bit/SOURCE.json
@@ -0,0 +1,12 @@
+{
+  "complex_commit": "187e1010ac8b259af8e9b5166f68b64bc27b4b47",
+  "bit_commit": "201737a1ec4f936e166e2481fb9e88104cb2ccc7",
+  "comparison_pr194_commit": "a8c87783785be6fe20c4a8bb2ac4b3eec295a179",
+  "files": {
+    "research/source-assisted-v4/certificate.json": "d84406d2fcc6990deba2b135509e6d86600e57123d88f9b21f7b7240e1aeb513",
+    "research/source-assisted-v4/SOURCE.json": "99024e5c8296ad03b6e499c3c4e1e9e879bf6a5954d8558cc39abd557edf79d6",
+    "scripts/paired_cube_assembly.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c",
+    "research/source-assisted/global/FINITE_BRIDGE.txt": "66d8f4ea8752abd89952d6674a636575a0db16e18b1c16e293f48f64242f0c46"
+  },
+  "bit_manifest_sha256": "265dad47ee7bbc1a555ff02810e94b15d76cc362acf1518ed05f8b60a7d1b489"
+}
diff --git a/research/packed-source-assisted-bit/arithmetic.py b/research/packed-source-assisted-bit/arithmetic.py
new file mode 100644
index 0000000000..7a25587798
--- /dev/null
+++ b/research/packed-source-assisted-bit/arithmetic.py
@@ -0,0 +1,95 @@
+"""Exact paid moments and finite ordinary-leaf composition.
+
+PR185/187 finite bootstrap and PR193 balanced bridge are inherited.
+Apache-2.0. Prepared with substantial OpenAI Codex assistance.
+"""
+from fractions import Fraction as Q
+from pathlib import Path
+import importlib.util,json
+
+def load(name,path):
+ s=importlib.util.spec_from_file_location(name,path);m=importlib.util.module_from_spec(s);s.loader.exec_module(m);return m
+
+def build(ROOT,BIT,physical):
+    im=load('interval_moment',BIT/'research/paired-cube-local-bit-168/arithmetic/interval_moment.py')
+    assembly=load('frontier_assembly',ROOT/'scripts/paired_cube_assembly.py')
+    p=physical
+    c191=json.loads((ROOT/'research/source-assisted-v4/certificate.json').read_text())
+    b187=json.loads((BIT/'research/source-assisted-bit-bootstrap/certificate.json').read_text())
+
+    def profile(m,W,H,delta):
+     H={int(r):int(n) for r,n in H.items()}
+     return dict(m=m,W=W,child_multiplicities=H,N=delta,L=0,total_rank=sum(r*n for r,n in H.items()),maxchild=max(H))
+    cp=c191['complex_profile'];cp=profile(cp['m'],cp['W_per_vertex'],cp['child_histogram'],cp['deficit_per_vertex'])
+    unpacked=b187['profile'];unpacked['child_multiplicities']={int(r):n for r,n in unpacked['child_multiplicities'].items()}
+    packed=profile(72,p['W'],p['child_histogram'],p['deficit'])
+
+    def paid(row,a,bit):
+     result=im.moment(row,a)
+     if bit:
+      l,u=im.log_interval(Q(row['m']));e,f=im.exp_interval(a*l,a*u)
+      w=Q(1,10**16)*Q(32*row['m']*sum(row['child_multiplicities'].values()),row['W'])
+      result.update(lower=result['lower']+w*e,upper=result['upper']+w*f)
+     return result
+
+    def certify(row,bit):
+     den=10**18;lo=0;hi=den//100
+     assert paid(row,Q(lo,den),bit)['upper']<1<paid(row,Q(hi,den),bit)['lower']
+     while hi-lo>1:
+      mid=(lo+hi)//2;v=paid(row,Q(mid,den),bit)
+      if v['upper']<1:lo=mid
+      elif v['lower']>1:hi=mid
+      else:raise AssertionError('Interval inconclusive')
+     a=Q(lo,den);b=Q(hi,den)
+     return dict(saving=a,accepted=paid(row,a,bit),next_excluded=paid(row,b,bit))
+
+    complex_cert=certify(cp,False)
+    original=certify(unpacked,True);new=certify(packed,True)
+    assert original['saving']==Q(b187['coarse'])
+    assert new['saving']>original['saving']
+    assert paid(packed,original['saving'],True)['upper']<paid(unpacked,original['saving'],True)['lower']
+    # Finite-depth ordinary supplier composition, as in PR185/187.
+    old=Q(b187['ordinary_chain'][-1]);coarse=new['saving'];chain=[old]
+    for _ in range(3):
+     a=(1-coarse)*coarse+coarse*chain[-1]
+     assert chain[-1]<a<coarse<1-a
+     chain.append(a)
+    assert 0<p['conservative_selector_calls']<2**40
+    # Additional chart/router calls are fixed, executed with the inherited ordinary
+    # selector; their exponent is <=atom exponent coarse and is below 1-ordinary.
+    assert coarse<1-chain[-1]
+    bridge=c191['assembly']['finite_bridge'];bridge['rows']['degree_gap']=Q(bridge['rows']['degree_gap'])
+    beta=eta=Q(1,10**24);weak=Q(1,10**30);den=10**18
+
+    def assemble(bit_saving):
+     b=complex_cert['saving'];a=min(bit_saving,(1-beta)*b-weak)
+     q=a*(1-2*eta);bound=(1-eta)*q/(1+q);z=bound*den
+     k=Q((z.numerator-1)//z.denominator,den)
+     out=assembly.assembly(a,b,bridge,k,eta=eta,beta=beta)
+     assert len(out['strict_constraints'])==47 and len(out['margins'])==7
+     try:assembly.assembly(a,b,bridge,k+Q(1,den),eta=eta,beta=beta)
+     except AssertionError:pass
+     else:raise AssertionError('Next final grid accepted')
+     constraints=out.pop('strict_constraints')
+     out['strict_constraint_count']=len(constraints)
+     out['minimum_constraint']=min(constraints.values())
+     return dict(kappa=k,assembly=out,binding='complex' if a==(1-beta)*b-weak else 'bit')
+    before=assemble(old);after=assemble(chain[-1])
+    del before['assembly']  # Recomputed and checked above; do not duplicate its full record.
+    assert before['kappa']<after['kappa']
+    controls=[]
+    bad=dict(packed,total_rank=packed['total_rank']+1)
+    try:paid(bad,coarse,True)
+    except ValueError:controls.append('changed rank mass')
+    else:raise AssertionError('Corrupt mass accepted')
+
+    out=dict(scope='Conditional composition; physical and finite bridge proof dependencies are separate',
+     source_commits=dict(complex='187e1010ac8b259af8e9b5166f68b64bc27b4b47',bit='201737a1ec4f936e166e2481fb9e88104cb2ccc7'),
+     complex_profile=cp,packed_profile=packed,complex=complex_cert,bit_before=original,bit_after=new,
+     bit_coarse_relative_gain=new['saving']/original['saving']-1,
+     stock_relative_reduction=1-Q(p['W'],3*unpacked['W']),ordinary_chain=chain,
+     extra_selector_calls=p['conservative_selector_calls'],selector_toll_gap=1-chain[-1]-coarse,
+     published_parent_kappa=c191['kappa'],comparison_pr194_kappa='1668581/2500000000',before_packing=before,after_packing=after,
+     kappa_gain_from_packing=after['kappa']-before['kappa'],controls=controls)
+
+    return out
diff --git a/research/packed-source-assisted-bit/audit.py b/research/packed-source-assisted-bit/audit.py
new file mode 100644
index 0000000000..0bf3613d7c
--- /dev/null
+++ b/research/packed-source-assisted-bit/audit.py
@@ -0,0 +1,77 @@
+"""Independent exact moment and finite-leaf audit; no optimizer imports."""
+from fractions import Fraction as Q
+from functools import lru_cache
+from math import factorial
+ROUND=2**192
+
+def lower(value):
+    return Q((value * ROUND).numerator // (value * ROUND).denominator, ROUND)
+
+def upper(value):
+    x = value * ROUND
+    return Q(-((-x.numerator) // x.denominator), ROUND)
+
+@lru_cache(None)
+def logarithm(x):
+    """Independent base-two reduction, 64 atanh terms and geometric remainder."""
+    assert x >= 1
+    power = 0
+    while x >= 2:
+        x /= 2
+        power += 1
+    def small(y):
+        z = (y - 1) / (y + 1)
+        s = 2 * sum((z**(2*j+1) / (2*j+1) for j in range(64)), Q(0))
+        return s, s + 2*z**129 / (129*(1-z*z))
+    l, u = small(x)
+    l2, u2 = small(Q(2))
+    return lower(l + power*l2), upper(u + power*u2)
+
+def exponential(l, u):
+    assert 0 <= l <= u < Q(1, 4)
+    def polynomial(x):
+        return sum((x**j / factorial(j) for j in range(17)), Q(0))
+    tail = u**17 / (factorial(17)*(1-u/18))
+    return lower(polynomial(l)), upper(polynomial(u) + tail)
+
+
+def moment(row,a,bit):
+    m,W=row['m'],row['W'];H={int(r):n for r,n in row['child_multiplicities'].items()}
+    assert sum(r*n for r,n in H.items())==row['total_rank']==m*W-row['N']
+    lo=hi=Q(0)
+    for r,n in H.items():
+        l,u=logarithm(Q(m,r));e,f=exponential(a*l,a*u)
+        lo+=Q(r*n,m*W)*e;hi+=Q(r*n,m*W)*f
+    if bit:
+        l,u=logarithm(Q(m));e,f=exponential(a*l,a*u)
+        weight=Q(32*m*sum(H.values()),10**16*W)
+        lo+=weight*e;hi+=weight*f
+    return lo,hi
+
+
+def run(record,original):
+    original=dict(original,child_multiplicities={int(r):n for r,n in original['child_multiplicities'].items()})
+    intervals={}
+    for name,row,bit in (('complex',record['complex_profile'],False),('bit_before',original,True),('bit_after',record['packed_profile'],True)):
+        a=Q(record[name]['saving']);lo,hi=moment(row,a,bit);next_lo,next_hi=moment(row,a+Q(1,10**18),bit)
+        assert hi<1<next_lo
+        intervals[name]=dict(accepted_lower=lo,accepted_upper=hi,next_lower=next_lo,next_upper=next_hi)
+    H={int(r):3*n for r,n in original['child_multiplicities'].items()}
+    assert H.pop(60)==6600
+    packed=record['packed_profile']
+    assert H=={int(r):n for r,n in packed['child_multiplicities'].items()}
+    assert packed['W']==3*original['W']-5500==57824
+    assert packed['N']==3*original['N']==5808
+    c=Q(record['bit_after']['saving']);chain=list(map(Q,record['ordinary_chain']))
+    assert len(chain)==4
+    for j,a in enumerate(chain[1:],1):
+        assert a==(1-c)*c+c*chain[j-1]==c-c**j*(c-chain[0])
+        assert chain[j-1]<a<c<1-a
+    b=Q(record['complex']['saving']);beta=eta=Q(1,10**24)
+    for name,saving in (('before_packing',chain[0]),('after_packing',chain[-1])):
+        a=min(saving,(1-beta)*b-Q(1,10**30));q=a*(1-2*eta);ceiling=(1-eta)*q/(1+q)
+        k=Q(record[name]['kappa'])
+        assert k<ceiling<=k+Q(1,10**18)
+        assert a==saving<b
+    assert Q(record['after_packing']['kappa'])>Q(record['comparison_pr194_kappa'])
+    return dict(status='PASS',moment_intervals=intervals,finite_leaf_levels=3,adjacent_final_grids_checked=2)
diff --git a/research/packed-source-assisted-bit/certificate.json b/research/packed-source-assisted-bit/certificate.json
new file mode 100644
index 0000000000..0f9f621f97
--- /dev/null
+++ b/research/packed-source-assisted-bit/certificate.json
@@ -0,0 +1,283 @@
+{
+  "arithmetic": {
+    "after_packing": {
+      "assembly": {
+        "absorption_gap": "187650353208934737181123742870437912940949995045313888226518464938967487270856700842041821731319938636561692714643181933741611144530007126046466744153457796400215954019595072229/488611590678881218387328874576807331136570134250515107904773869020042872913440211179005663339249011225418425020698808191034912055269862358356142442926411901474639569927771000000000000000000000000",
+        "margins": {
+          "Gaussian_arithmetic": "528545086209949419726491961301050937293827471949595840307053861934346146396433112540041299925504520458301027454753856644633870006759074561636873770203772497064955741990673588098525360430072229/781778545086209949419726199322891729818512214800824172647638190432068596661504337886409061342798417960669480033118093105655859288431779773369827908682259042359423311884433600000000000000000000000",
+          "balanced_prefix": "330340678881218387329362858057331136570134250515107904773869020042872913440211179005663339249011225418425020698808191034912055269862358356142442926411901474639569927771/488611590678881218387328874576807331136570134250515107904773869020042872913440211179005663339249011225418425020698808191034912055269862358356142442926411901474639569927771",
+          "bulk_exposure": "660681357762436774657750474977377798013817816531165764303334067721378889211950964679462121255800874738779400321858893671573588098525360430072229/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+          "compact_phase_layer": "330340678881218387328874246466652255351746921640531097442732449908622398332306405136643296376097785207246015035468942023686636844841659547951408014356631612281213785328073588098525360430072229/488611590678881218387328874576807331136570134250515107904773869020042872913440211179005663339249011225418425020698808191034912055269862358356142442926411901474639569927771000000000000000000000000",
+          "coordinate_movement": "660681357762436774657750474977377798013817816531165764303334067721378889211950964679462121255800874738779400321858893671573588098525360430072229/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+          "dimension": "488281249999999999999999511718750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000/488611590678881218387328874576807331136570134250515107904773869020042872913440211179005663339249011225418425020698808191034912055269862358356142442926411901474639569927771",
+          "scalar_work": "2642725431049747098634414252867970211342686675246286430859815590208732792413784658176286671119176363136221159927126279268071023733878168040948508499239941934758203279725073588098525360430072229/3908892725431049747098630996614458649092561074004120863238190952160342983307521689432045306713992089803347400165590465528279296442158898866849139543411295211797116559422168000000000000000000000000"
+        },
+        "minimum_constraint": "660681357762436774657750474977377798013817816531165764303334067721378889211950964679462121255800874738779400321858893671573588098525360430072229/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "minimum_margin": "330340678881218387328874246466652255351746921640531097442732449908622398332306405136643296376097785207246015035468942023686636844841659547951408014356631612281213785328073588098525360430072229/488611590678881218387328874576807331136570134250515107904773869020042872913440211179005663339249011225418425020698808191034912055269862358356142442926411901474639569927771000000000000000000000000",
+        "parameters": {
+          "C0": {
+            "base": 2,
+            "exponent": 210000
+          },
+          "C1": 1,
+          "a_bit": "660681357762436774657750474977377798013817816531165764303334067721378889211950964679462121255800874738779400321858893671573588098525360430072229/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+          "a_complex": "700918443859411/1000000000000000000",
+          "alpha_squared_power": "660681357762436774658237104523983391921881172155639002216601469951495311772517584142306635625109010625671035734277133058598692114704017904093850940768533086920783713099073588098525360430072229/977223181357762436774657749153614662273140268501030215809547738040085745826880422358011326678498022450836850041397616382069824110539724716712284885852823802949279139855542000000000000000000000000",
+          "beta": "1/1000000000000000000000000",
+          "c": "330340678881218387328996647119831136570134250515107904773869020042872913440211179005663339249011225418425020698808191034912055269862358356142442926411901474639569927771/488281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+          "delta": "1/8000000000000000000000000",
+          "epsilon": "488281249999999999999999511718750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000/488611590678881218387328874576807331136570134250515107904773869020042872913440211179005663339249011225418425020698808191034912055269862358356142442926411901474639569927771",
+          "eta": "1/1000000000000000000000000",
+          "kappa": "135216063303877/200000000000000000",
+          "lambda_": "975901818642237563225342250185703979964422956841219309213074463946096437641953813338654605600123088337212185279140262362129301150680874961428821442573588098525360430072229/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+          "lambda_prime": "487950909321118781612671125423192668863429865749484892095226130979957127086559788820994336660750988774581574979301191808965087944730137641643857557073588098525360430072229/488281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+          "q": "330340678881218387328874576807331136570134250515107904773869020042872913440211179005663339249011225418425020698808191034912055269862358356142442926411901474639569927771/488281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+          "sigma": "999299081556140589/1000000000000000000",
+          "tau": "975901818642237563225342249525022622201986182183468834235696665932278621110788049035320537878744199125261220599678141106328426411901474639569927771/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+        },
+        "recurrence": {
+          "internal": "975901818642237563225342249525022622201986182183468834235696665932278621110788049035320537878744199125261220599678141106328426411901474639569927771/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+          "leaf": "999299081556140589000000000700918443859411/1000000000000000000000000000000000000000000",
+          "reservations": "487950909321118781612671003352880168863429865749484892095226130979957127086559788820994336660750988774581574979301191808965087944730137641643857557073588098525360430072229/488281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+        },
+        "strict_constraint_count": 47
+      },
+      "binding": "bit",
+      "kappa": "135216063303877/200000000000000000"
+    },
+    "before_packing": {
+      "binding": "bit",
+      "kappa": "670450176035363/1000000000000000000"
+    },
+    "bit_after": {
+      "accepted": {
+        "lower": "677624999999999999657399605509035322101598190079690160033232817/677625000000000000000000000000000000000000000000000000000000000",
+        "saving": "676537710350481/1000000000000000000",
+        "strict_gap_lower": "303030165592899211041645670279812486649/86736000000000000000000000000000000000000000000000",
+        "upper": "16940624999999999991434990137725883052539955032869207135332167/16940625000000000000000000000000000000000000000000000000000000"
+      },
+      "next_excluded": {
+        "lower": "338812500000000000527954367608485199993671032009844206302895179/338812500000000000000000000000000000000000000000000000000000000",
+        "saving": "338268855175241/500000000000000000",
+        "strict_gap_lower": "404039982111640812962552474122098050579/115648000000000000000000000000000000000000000000000",
+        "upper": "225875000000000000351969578405656799995780691751588845995281407/225875000000000000000000000000000000000000000000000000000000000"
+      },
+      "saving": "676537710350481/1000000000000000000"
+    },
+    "bit_before": {
+      "accepted": {
+        "lower": "82453124999999999989205572896937038584170512932039742846004063/82453125000000000000000000000000000000000000000000000000000000",
+        "saving": "167724995262213/250000000000000000",
+        "strict_gap_lower": "4523116177218361504761889534314884837/1407200000000000000000000000000000000000000000000",
+        "upper": "27484374999999999996401857632312346194723504686885643461352837/27484375000000000000000000000000000000000000000000000000000000"
+      },
+      "next_excluded": {
+        "lower": "247359375000000000437697138375814169267365282480510092612153899/247359375000000000000000000000000000000000000000000000000000000",
+        "saving": "670899981048853/1000000000000000000",
+        "strict_gap_lower": "610620322902716487671930671872838275917/189972000000000000000000000000000000000000000000000",
+        "upper": "742078125000000001313091415127442507802095857661807621928951729/742078125000000000000000000000000000000000000000000000000000000"
+      },
+      "saving": "167724995262213/250000000000000000"
+    },
+    "bit_coarse_relative_gain": "1879243100543/223633327016284",
+    "comparison_pr194_kappa": "1668581/2500000000",
+    "complex": {
+      "accepted": {
+        "lower": "265143999999999999505356323836919762528275607173151/265144000000000000000000000000000000000000000000000",
+        "saving": "700918443859411/1000000000000000000",
+        "strict_gap_lower": "44967606923916385224702216933483/24104000000000000000000000000000000000000000000000",
+        "upper": "24103999999999999955032393076083614775297783066517/24104000000000000000000000000000000000000000000000"
+      },
+      "next_excluded": {
+        "lower": "66286000000000000033428585232057842908390904631703/66286000000000000000000000000000000000000000000000",
+        "saving": "175229610964853/250000000000000000",
+        "strict_gap_lower": "-1162733399375924970726640217937/2305600000000000000000000000000000000000000000000",
+        "upper": "2305600000000000001162733399375924970726640217937/2305600000000000000000000000000000000000000000000"
+      },
+      "saving": "700918443859411/1000000000000000000"
+    },
+    "complex_profile": {
+      "L": 0,
+      "N": 1320,
+      "W": 12052,
+      "child_multiplicities": {
+        "1": 87534,
+        "10": 2790,
+        "11": 1062,
+        "12": 3591,
+        "13": 381,
+        "14": 2226,
+        "15": 5637,
+        "16": 264,
+        "17": 243,
+        "18": 7959,
+        "19": 501,
+        "2": 39834,
+        "20": 66,
+        "3": 29769,
+        "4": 12627,
+        "5": 5850,
+        "6": 4815,
+        "7": 2118,
+        "8": 4593,
+        "9": 1287
+      },
+      "m": 66,
+      "maxchild": 20,
+      "total_rank": 794112
+    },
+    "controls": [
+      "changed rank mass"
+    ],
+    "extra_selector_calls": 5859111150,
+    "kappa_gain_from_packing": "2815070242011/500000000000000000",
+    "ordinary_chain": [
+      "655175762739997625388892048465518856359612684797421550872147594576395840411339259699702069/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "660677633021489850195699555709117768852581594816555572803312176338987944423020142711333538320522333270845189/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "660681355244212736301851286128921676374944322184490562027244992313907172742513022152383123305699174315199029401817676282685909/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "660681357762436774657750474977377798013817816531165764303334067721378889211950964679462121255800874738779400321858893671573588098525360430072229/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+    ],
+    "packed_profile": {
+      "L": 0,
+      "N": 5808,
+      "W": 57824,
+      "child_multiplicities": {
+        "1": 360504,
+        "10": 7524,
+        "11": 3474,
+        "12": 12960,
+        "13": 4770,
+        "14": 9702,
+        "15": 3690,
+        "16": 9648,
+        "17": 3492,
+        "18": 3996,
+        "19": 2754,
+        "2": 192684,
+        "20": 15840,
+        "21": 33480,
+        "22": 35856,
+        "3": 88848,
+        "4": 26910,
+        "5": 23400,
+        "6": 10980,
+        "7": 9936,
+        "8": 8406,
+        "9": 5436
+      },
+      "m": 72,
+      "maxchild": 22,
+      "total_rank": 4157520
+    },
+    "published_parent_kappa": "103873/156250000",
+    "scope": "Conditional composition; physical and finite bridge proof dependencies are separate",
+    "selector_toll_gap": "975241137284473421623779749525022622201986182183468834235696665932278621110788049035320537878744199125261220599678141106328426411901474639569927771/976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "source_commits": {
+      "bit": "201737a1ec4f936e166e2481fb9e88104cb2ccc7",
+      "complex": "187e1010ac8b259af8e9b5166f68b64bc27b4b47"
+    },
+    "stock_relative_reduction": "1375/15831"
+  },
+  "bank_controls": {
+    "formal_columns_per_case": 144,
+    "rejected": [
+      "repeated block mod 9",
+      "omitted block mod 9",
+      "repeated block mod 25",
+      "omitted block mod 25",
+      "repeated block mod 125",
+      "omitted block mod 125"
+    ],
+    "weighted_partition_cases": 12
+  },
+  "immutable_bit_files": 1734,
+  "independent": {
+    "adjacent_final_grids_checked": 2,
+    "finite_leaf_levels": 3,
+    "moment_intervals": {
+      "bit_after": {
+        "accepted_lower": "1063380265860349887610922319274424787879843879342729678618060364779583768997/1063380265860349888148556701975273738802839652013735346700288000000000000000",
+        "accepted_upper": "708920177240233258407281546182949858586562586228486452412162802431181632859/708920177240233258765704467983515825868559768009156897800192000000000000000",
+        "next_lower": "35446008862011662993518944684512458755751066352922710458582079319188746721/35446008862011662938285223399175791293427988400457844890009600000000000000",
+        "next_upper": "2126760531720699779611136681070747525345063981175362627515292436885702163843/2126760531720699776297113403950547477605679304027470693400576000000000000000"
+      },
+      "bit_before": {
+        "accepted_lower": "145565621444687319080969092786203211049137332137254931463250615537521283577/145565621444687319100025950720899268115209554259731636289536000000000000000",
+        "accepted_upper": "4658099886229994210591010969158502753572394628392157806824878181575688209673/4658099886229994211200830423068776579686705736311412361265152000000000000000",
+        "next_lower": "388174990519166184953603235307216531909307483891106061822184641295075931077/388174990519166184266735868589064714973892144692617696772096000000000000000",
+        "next_upper": "465809988622999421944323882368659838291168980669327274186701550413466592973/465809988622999421120083042306877657968670573631141236126515200000000000000"
+      },
+      "complex": {
+        "accepted_lower": "151303260229760552849231624798695928011617003747957445895984727/151303260229760553131497868256997591293731175633361087898845184",
+        "accepted_upper": "1664335862527366081341547872785655208127787041227531904856155057/1664335862527366084446476550826973504231042931966971966887297024",
+        "next_lower": "1664335862527366085285815072313660921079442613294059590682498373/1664335862527366084446476550826973504231042931966971966887297024",
+        "next_upper": "72362428805537655881991959665811344394758374491046069160122671/72362428805537655845498980470737978444827953563781389864665088"
+      }
+    },
+    "status": "PASS"
+  },
+  "physical": {
+    "W": 57824,
+    "banks": 47264,
+    "chart_sha256": "24ad4add234c38be945378df5748ea4c4f054780e3a617c2b7be12e5049ad553",
+    "child_histogram": {
+      "1": 360504,
+      "10": 7524,
+      "11": 3474,
+      "12": 12960,
+      "13": 4770,
+      "14": 9702,
+      "15": 3690,
+      "16": 9648,
+      "17": 3492,
+      "18": 3996,
+      "19": 2754,
+      "2": 192684,
+      "20": 15840,
+      "21": 33480,
+      "22": 35856,
+      "3": 88848,
+      "4": 26910,
+      "5": 23400,
+      "6": 10980,
+      "7": 9936,
+      "8": 8406,
+      "9": 5436
+    },
+    "color_stats": {
+      "longest_swapped_path": 11,
+      "swaps": 733
+    },
+    "conflicting_assignment_rejected": true,
+    "conservative_selector_calls": 5859111150,
+    "copies": 3,
+    "deficit": 5808,
+    "distinct_gauges": 220,
+    "gauge_roles": 2200,
+    "incidence_sha256": "310591cedba5a950c1e44d9adf686c9df104c07ba03d04c50db87c22b44e3ef6",
+    "incidences": 158292,
+    "interior_splices": 1760,
+    "m": 72,
+    "max_chart_factors": 186,
+    "max_den": 18,
+    "max_num": 5,
+    "maxchild": 22,
+    "patterns": [
+      {
+        "count": 3300,
+        "rank24": 2,
+        "rank4": 6
+      },
+      {
+        "count": 43964,
+        "rank24": 3,
+        "rank4": 0
+      }
+    ],
+    "physical_roles": 17588,
+    "rank_mass": 4157520,
+    "source_commit": "201737a1ec4f936e166e2481fb9e88104cb2ccc7",
+    "status": "PASS exact actual-chain chart and incidence checks",
+    "word_sha256": "3c188c2527b3b96443e241f2f0d07c120feb1e784c2ff7f49c3e1e10eaea5f0b"
+  }
+}
diff --git a/research/packed-source-assisted-bit/controls.py b/research/packed-source-assisted-bit/controls.py
new file mode 100644
index 0000000000..5123541528
--- /dev/null
+++ b/research/packed-source-assisted-bit/controls.py
@@ -0,0 +1,35 @@
+"""Independent weighted completed-bank endpoint checks on arbitrary formal data."""
+from math import gcd
+
+
+def run():
+    m=72;cases=0;rejected=[]
+    patterns=([4]*6+[24]*2,[24]*3)
+    def apply(parts,modulus,reverse=False,repeat_first=False):
+        rows=[{i:1} for i in range(2*m)]
+        intervals=[];offset=0
+        for width in parts:intervals.append(range(offset,offset+width));offset+=width
+        if repeat_first:intervals.append(intervals[0])
+        if reverse:intervals.reverse()
+        for interval in intervals:
+            for i in interval:
+                weight=(1,2,4)[i%3];assert gcd(weight,modulus)==1
+                a,b=rows[i],rows[2*m-1-i]
+                rows[i]={j:weight*x%modulus for j,x in b.items()}
+                rows[2*m-1-i]={j:pow(weight,-1,modulus)*x%modulus for j,x in a.items()}
+        return rows
+    def expected(modulus):
+        return [{2*m-1-i:(1,2,4)[i%3]} for i in range(m)]+[
+            {m-1-i:pow((1,2,4)[(m-1-i)%3],-1,modulus)} for i in range(m)]
+    for modulus in (9,25,125):
+        for pattern in patterns:
+            for reverse in (False,True):
+                assert apply(pattern,modulus,reverse)==expected(modulus)
+                cases+=1
+        try:assert apply(patterns[0],modulus,repeat_first=True)==expected(modulus)
+        except AssertionError:rejected.append('repeated block mod '+str(modulus))
+        else:raise AssertionError('Repeated block accepted')
+        try:assert apply(patterns[0][:-1],modulus)==expected(modulus)
+        except AssertionError:rejected.append('omitted block mod '+str(modulus))
+        else:raise AssertionError('Omitted block accepted')
+    return dict(formal_columns_per_case=2*m,weighted_partition_cases=cases,rejected=rejected)
diff --git a/research/packed-source-assisted-bit/packing.py b/research/packed-source-assisted-bit/packing.py
new file mode 100644
index 0000000000..b7e31dc08a
--- /dev/null
+++ b/research/packed-source-assisted-bit/packing.py
@@ -0,0 +1,186 @@
+"""Exact gauge charts and completed-residual bank allocation.
+
+Apache-2.0. Prepared with substantial OpenAI Codex assistance.
+"""
+from array import array
+from collections import Counter
+from fractions import Fraction as Q
+from math import gcd
+from pathlib import Path
+import hashlib,json,sys
+
+def inverse_integer(a):
+    """Fraction-free Gauss-Jordan; return integral C,d with a C = d I."""
+    n=len(a)
+    m=[list(row)+[int(i==j) for j in range(n)] for i,row in enumerate(a)]
+    previous=1
+    factors=[]
+    for k in range(n):
+        pivot=next((i for i in range(k,n) if m[i][k]),None)
+        if pivot is None:
+            raise ValueError('Singular basis')
+        m[k],m[pivot]=m[pivot],m[k]
+        if pivot != k:factors.append(('swap',k,pivot,1,1))
+        p=m[k][k]
+        if p != previous:
+            ratio=Q(previous,p)
+            factors.append(('scale',k,k,ratio.numerator,ratio.denominator))
+        for i in range(n):
+            if i==k:continue
+            u=m[i][k]
+            if u:
+                ratio=Q(-u,previous)
+                factors.append(('add',i,k,ratio.numerator,ratio.denominator))
+            for j in range(2*n):
+                if j==k:continue
+                value=p*m[i][j]-u*m[k][j]
+                assert value % previous==0
+                m[i][j]=value//previous
+            m[i][k]=0
+        previous=p
+    d=m[0][0]
+    assert d and all(m[i][j]==d*int(i==j) for i in range(n) for j in range(n))
+    c=[row[n:] for row in m]
+    common=abs(d)
+    for row in c:
+        for x in row:common=gcd(common,x)
+    d//=common
+    c=[[x//common for x in row] for row in c]
+    if d<0:d=-d;c=[[-x for x in row] for row in c]
+    return c,d,factors
+
+def color_incidence(left,right,nleft,nright,colors):
+    """Incremental two-color swaps; parallel edges are identified separately."""
+    assert len(left)==len(right)
+    full=(1<<colors)-1
+    lf=[full]*nleft;rf=[full]*nright
+    lc=[array('i',[-1])*colors for _ in range(nleft)]
+    rc=[{} for _ in range(nright)]
+    labels=array('i',[-1])*len(left)
+    swaps=longest=0
+    def remove(e):
+        u,v,c=left[e],right[e],labels[e]
+        assert lc[u][c]==e and rc[v][c]==e
+        lc[u][c]=-1;del rc[v][c]
+        lf[u]|=1<<c;rf[v]|=1<<c
+    def add(e,c):
+        u,v=left[e],right[e]
+        assert lf[u]&(1<<c) and rf[v]&(1<<c)
+        labels[e]=c;lc[u][c]=e;rc[v][c]=e
+        lf[u]&=~(1<<c);rf[v]&=~(1<<c)
+    for e,(u,v) in enumerate(zip(left,right)):
+        common=lf[u]&rf[v]
+        if common:
+            add(e,(common&-common).bit_length()-1)
+            continue
+        assert lf[u] and rf[v]
+        a=(lf[u]&-lf[u]).bit_length()-1
+        b=(rf[v]&-rf[v]).bit_length()-1
+        path=[];r=u
+        while True:
+            edge=lc[r][b]
+            if edge<0:break
+            path.append(edge);bank=right[edge]
+            assert bank!=v
+            edge=rc[bank].get(a,-1)
+            if edge<0:break
+            path.append(edge);r=left[edge]
+        changes=[(edge,b if labels[edge]==a else a) for edge in path]
+        for edge,_ in changes:remove(edge)
+        for edge,c in changes:add(edge,c)
+        add(e,b)
+        swaps+=1;longest=max(longest,len(path))
+    return labels,{'swaps':swaps,'longest_swapped_path':longest}
+
+def check_coloring(left,right,labels,nleft,nright,colors,full_left=False):
+    assert len(left)==len(right)==len(labels)
+    lm=[0]*nleft;rm=[0]*nright
+    for u,v,c in zip(left,right,labels):
+        assert 0<=u<nleft and 0<=v<nright and 0<=c<colors
+        bit=1<<c
+        assert not lm[u]&bit and not rm[v]&bit
+        lm[u]|=bit;rm[v]|=bit
+    if full_left:assert all(mask==(1<<colors)-1 for mask in lm)
+
+def build(BIT):
+    sys.path.insert(0,str(BIT/'scripts'))
+    import paired_cube_bit_physical as P
+    chk=P.loaded();chk.frames()
+    wordpath=BIT/'build/source-assisted-bit-bootstrap/emitted-word.json'
+    w=json.loads(wordpath.read_text())
+    receipt=json.loads((BIT/'build/source-assisted-bit-bootstrap/emitted-physical.json').read_text())
+    assert hashlib.sha256(wordpath.read_bytes()).hexdigest()==receipt['word_sha256']
+    R=w['R'];donors={a for a,b in w['pairs']};recipients={b for a,b in w['pairs']};gauges={z['role']:z for z in w['gauges']}
+    assert len(donors)==len(recipients)==len(w['pairs'])==1760
+    assert not donors&recipients and not donors&gauges.keys() and recipients<=gauges.keys()
+    physical=sorted(set(range(R))-recipients);ren={r:i for i,r in enumerate(physical)}
+    assert len(physical)==receipt['physical_R']==17588
+    selected=set(gauges)-recipients
+    assert len(selected)==2200 and {gauges[r]['dim'] for r in selected}=={20}
+    assert {gauges[r]['dim'] for r in recipients}=={21}
+    # Interior rank-21 recipient starts are already paid splices, not entrance residuals.
+    inventory=Counter(gauges[r]['frame'] for r in selected)
+    digest=hashlib.sha256();maxops=maxnum=maxden=0
+    for f,count in sorted(inventory.items()):
+     A=chk.A[f];source=chk.B[f];assert len(A)==4 and len(source)==20
+     residual=[]
+     for a in A:
+      row=[15*x-sum(a) for x in a];d=gcd(*row);residual.append([x//d for x in row])
+     assert all(9*sum(x*y for x,y in zip(a,b))-sum(a)*sum(b)==0 for a in residual for b in source)
+     B=list(map(list,zip(*(residual+source))))
+     C,d,ops=inverse_integer(B)
+     for left,right in ((B,C),(C,B)):
+      assert all(sum(x*y for x,y in zip(row,col))==d*int(i==j) for i,row in enumerate(left) for j,col in enumerate(zip(*right)))
+     replay=[list(map(Q,row)) for row in B]
+     for op,i,j,num,den in ops:
+      if op=='swap':replay[i],replay[j]=replay[j],replay[i]
+      elif op=='scale':replay[i]=[Q(num,den)*x for x in replay[i]]
+      else:
+       assert op=='add';replay[i]=[x+Q(num,den)*y for x,y in zip(replay[i],replay[j])]
+     assert all(x==int(i==j) for i,row in enumerate(replay) for j,x in enumerate(row))
+     maxops=max(maxops,len(ops));maxnum=max(maxnum,max(abs(op[3]) for op in ops));maxden=max(maxden,d,max(op[4] for op in ops))
+     digest.update(json.dumps([f,count,B,C,d,ops],separators=(',',':')).encode())
+    assert max(maxnum,maxden)<2**80
+    families={4:sorted(selected),24:sorted(set(physical)-selected)}
+    degree=9;copies=3;small=degree*len(selected)//6
+    assert 6*small==degree*len(selected)
+    large=(degree*len(families[24])-2*small)//3
+    assert 3*large+2*small==degree*len(families[24])
+    left=[];right=[];offsets=[];counts=Counter();bank=0
+    for pattern,n in (({4:6,24:2},small),({24:3},large)):
+     for _ in range(n):
+      offset=0
+      for rank,mult in sorted(pattern.items()):
+       for _ in range(mult):
+        role=families[rank][counts[rank]//degree]
+        left.append(ren[role]);right.append(bank);offsets.append(offset);counts[rank]+=1;offset+=rank
+      assert offset==72
+      bank+=1
+    assert all(counts[r]==degree*len(rs) for r,rs in families.items())
+    labels,stats=color_incidence(left,right,len(physical),bank,degree)
+    check_coloring(left,right,labels,len(physical),bank,degree,full_left=True)
+    first={};rejected=False
+    for e,r in enumerate(left):
+     if r not in first:first[r]=e;continue
+     old=labels[e];labels[e]=labels[first[r]]
+     try:check_coloring(left,right,labels,len(physical),bank,degree,full_left=True)
+     except AssertionError:rejected=True
+     finally:labels[e]=old
+     break
+    assert rejected
+    incidence=hashlib.sha256()
+    for r,b,c,o in zip(left,right,labels,offsets):incidence.update(f'{r},{b},{c},{o}\n'.encode())
+    H=Counter({int(r):copies*n for r,n in receipt['child_histogram'].items()})
+    assert H.pop(60)==copies*len(selected)
+    assert not any(r>22 for r in H)
+    W=2*w['v']*copies+bank;mass=sum(r*n for r,n in H.items())
+    assert 72*W-mass==copies*receipt['deficit_per_vertex']==5808
+    K=18*((W-1)+len(physical)*72*(maxops+71))
+    record=dict(status='PASS exact actual-chain chart and incidence checks',source_commit='201737a1ec4f936e166e2481fb9e88104cb2ccc7',
+     word_sha256=receipt['word_sha256'],physical_roles=len(physical),interior_splices=len(recipients),gauge_roles=len(selected),
+     distinct_gauges=len(inventory),copies=copies,banks=bank,patterns=[dict(rank4=6,rank24=2,count=small),dict(rank4=0,rank24=3,count=large)],
+     incidences=len(left),W=W,m=72,rank_mass=mass,deficit=5808,maxchild=max(H),child_histogram=dict(sorted(H.items())),
+     chart_sha256=digest.hexdigest(),incidence_sha256=incidence.hexdigest(),max_chart_factors=maxops,max_num=maxnum,max_den=maxden,
+     conservative_selector_calls=K,color_stats=stats,conflicting_assignment_rejected=rejected)
+
+    return record
diff --git a/research/packed-source-assisted-bit/verify.py b/research/packed-source-assisted-bit/verify.py
new file mode 100644
index 0000000000..3a59cd6ca9
--- /dev/null
+++ b/research/packed-source-assisted-bit/verify.py
@@ -0,0 +1,69 @@
+#!/usr/bin/env python3
+"""Verify the packed PR187 bit supplier with PR193's complex supplier, offline."""
+from pathlib import Path
+from fractions import Fraction as Q
+import argparse,hashlib,json,os,subprocess,sys
+if sys.flags.optimize:raise SystemExit('Assertions required')
+sys.set_int_max_str_digits(0)
+HERE=Path(__file__).resolve().parent
+import packing,arithmetic,audit,controls
+
+
+def serial(value):
+    if isinstance(value,Q):return str(value)
+    if isinstance(value,dict):return {str(k):serial(v) for k,v in value.items()}
+    if isinstance(value,(list,tuple)):return [serial(v) for v in value]
+    return value
+
+
+def run(root,script,*args):
+    subprocess.run([sys.executable,'-B',str(root/script),*args],cwd=root,check=True,
+                   env=dict(os.environ,PYTHONDONTWRITEBYTECODE='1'))
+
+
+def main():
+    parser=argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--complex-root',type=Path,required=True,help='Checkout of the pinned PR193 commit')
+    parser.add_argument('--bit-root',type=Path,required=True,help='Checkout of the pinned PR187 commit')
+    parser.add_argument('--full',action='store_true',help='Regenerate both suppliers and actual packing')
+    parser.add_argument('--write',action='store_true',help='Regenerate certificate; requires --full')
+    args=parser.parse_args();assert not args.write or args.full
+    ROOT=args.complex_root.resolve()
+    source=json.loads((HERE/'SOURCE.json').read_text())
+    head=subprocess.check_output(['git','-C',str(ROOT),'rev-parse','HEAD'],text=True).strip()
+    assert head==source['complex_commit'],'Wrong complex checkout commit'
+    for name,expected in source['files'].items():
+        assert hashlib.sha256((ROOT/name).read_bytes()).hexdigest()==expected,('Changed source',name)
+    inherited=json.loads((ROOT/'research/source-assisted-v4/SOURCE.json').read_text())
+    for name,expected in inherited['files'].items():
+        assert hashlib.sha256((ROOT/name).read_bytes()).hexdigest()==expected,('Changed complex dependency',name)
+    bit=args.bit_root.resolve()
+    head=subprocess.check_output(['git','-C',str(bit),'rev-parse','HEAD'],text=True).strip()
+    assert head==source['bit_commit'],'Wrong bit checkout commit'
+    manifest_path=bit/'research/source-assisted-bit-bootstrap/SOURCE.json'
+    assert hashlib.sha256(manifest_path.read_bytes()).hexdigest()==source['bit_manifest_sha256']
+    manifest=json.loads(manifest_path.read_text())
+    inventory=dict(manifest['repository_files'])
+    inventory.update({'research/source-assisted-bit-bootstrap/'+name:sha
+                      for name,sha in manifest['package_files'].items()})
+    for name,expected in inventory.items():
+        assert hashlib.sha256((bit/name).read_bytes()).hexdigest()==expected,('Changed bit dependency',name)
+    if args.full:
+        run(ROOT,'research/source-assisted-v4/verify.py')
+        run(bit,'research/source-assisted-bit-bootstrap/verify.py','--full')
+        physical=packing.build(bit)
+    else:
+        physical=json.loads((HERE/'certificate.json').read_text())['physical']
+    result=arithmetic.build(ROOT,bit,physical)
+    baseline=json.loads((bit/'research/source-assisted-bit-bootstrap/certificate.json').read_text())
+    independent=audit.run(result,baseline['profile'])
+    record=dict(physical=physical,arithmetic=result,independent=independent,
+                bank_controls=controls.run(),immutable_bit_files=len(inventory)+1)
+    out=serial(record)
+    if args.write:(HERE/'certificate.json').write_text(json.dumps(out,indent=2,sort_keys=True)+'\n')
+    else:assert out==json.loads((HERE/'certificate.json').read_text()),'Certificate differs'
+    print('PASS exact packed profile, two moment engines, finite leaf composition, 47 constraints and seven margins')
+    print('conditional kappa = '+out['arithmetic']['after_packing']['kappa'])
+
+
+if __name__=='__main__':main()