diff --git a/research/complex-ck-b-frame-seed20/CERTIFICATE.json b/research/complex-ck-b-frame-seed20/CERTIFICATE.json
new file mode 100644
index 0000000000..65ae8dc75a
--- /dev/null
+++ b/research/complex-ck-b-frame-seed20/CERTIFICATE.json
@@ -0,0 +1,156 @@
+{
+  "complete_local_histogram": [0,2596,552,304,160,70,8,0,8,0],
+  "fixed_outside_histogram": [0,1360,56,104,64,70,8,0,8,0],
+  "baseline_histogram": [
+    0,
+    1236,
+    496,
+    200,
+    96,
+    0,
+    0,
+    0,
+    0,
+    0
+  ],
+  "conditional_profiles": 2641,
+  "domain_sizes": {
+    "2": 418,
+    "5": 56
+  },
+  "evaluated": 4724,
+  "flexible_gates": 474,
+  "gates": 1930,
+  "induced_width": 5,
+  "max_conditional_frontier": 5,
+  "pinned_gates": 492,
+  "power_certificate": {
+    "baseline_power_optimal": true,
+    "exponent_interval": "0 < p < 1",
+    "largest_derivative_upper": "-21/25",
+    "strict_alternatives": 118
+  },
+  "registers": 716,
+  "source_sha256": "ae3018c0646be06f47d345bb8baf0e6ea9220096a949fa30a8f7656aa4ad6f45",
+  "final_frontier": [
+    [0,1236,496,200,96,0,0,0,0,0],
+    [0,1239,493,201,96,0,0,0,0,0],
+    [0,1242,490,202,96,0,0,0,0,0],
+    [0,1243,492,199,97,0,0,0,0,0],
+    [0,1245,487,203,96,0,0,0,0,0],
+    [0,1248,488,196,100,0,0,0,0,0],
+    [0,1251,485,197,100,0,0,0,0,0],
+    [0,1254,482,198,100,0,0,0,0,0],
+    [0,1255,484,195,101,0,0,0,0,0],
+    [0,1257,479,199,100,0,0,0,0,0],
+    [0,1260,480,192,104,0,0,0,0,0],
+    [0,1263,477,193,104,0,0,0,0,0],
+    [0,1266,474,194,104,0,0,0,0,0],
+    [0,1267,476,191,105,0,0,0,0,0],
+    [0,1269,471,195,104,0,0,0,0,0],
+    [0,1272,472,188,108,0,0,0,0,0],
+    [0,1275,469,189,108,0,0,0,0,0],
+    [0,1278,466,190,108,0,0,0,0,0],
+    [0,1279,468,187,109,0,0,0,0,0],
+    [0,1281,463,191,108,0,0,0,0,0],
+    [0,1284,464,184,112,0,0,0,0,0],
+    [0,1287,461,185,112,0,0,0,0,0],
+    [0,1290,458,186,112,0,0,0,0,0],
+    [0,1291,460,183,113,0,0,0,0,0],
+    [0,1293,455,187,112,0,0,0,0,0],
+    [0,1296,456,180,116,0,0,0,0,0],
+    [0,1299,453,181,116,0,0,0,0,0],
+    [0,1302,450,182,116,0,0,0,0,0],
+    [0,1303,452,179,117,0,0,0,0,0],
+    [0,1305,447,183,116,0,0,0,0,0],
+    [0,1308,448,176,120,0,0,0,0,0],
+    [0,1311,445,177,120,0,0,0,0,0],
+    [0,1314,442,178,120,0,0,0,0,0],
+    [0,1315,444,175,121,0,0,0,0,0],
+    [0,1317,439,179,120,0,0,0,0,0],
+    [0,1320,440,172,124,0,0,0,0,0],
+    [0,1323,437,173,124,0,0,0,0,0],
+    [0,1326,434,174,124,0,0,0,0,0],
+    [0,1327,436,171,125,0,0,0,0,0],
+    [0,1329,431,175,124,0,0,0,0,0],
+    [0,1332,432,168,128,0,0,0,0,0],
+    [0,1335,429,169,128,0,0,0,0,0],
+    [0,1338,426,170,128,0,0,0,0,0],
+    [0,1339,428,167,129,0,0,0,0,0],
+    [0,1341,423,171,128,0,0,0,0,0],
+    [0,1344,424,164,132,0,0,0,0,0],
+    [0,1347,421,165,132,0,0,0,0,0],
+    [0,1350,418,166,132,0,0,0,0,0],
+    [0,1351,420,163,133,0,0,0,0,0],
+    [0,1353,415,167,132,0,0,0,0,0],
+    [0,1356,416,160,136,0,0,0,0,0],
+    [0,1359,413,161,136,0,0,0,0,0],
+    [0,1362,410,162,136,0,0,0,0,0],
+    [0,1365,407,163,136,0,0,0,0,0],
+    [0,1368,404,164,136,0,0,0,0,0],
+    [0,1371,401,165,136,0,0,0,0,0],
+    [0,1371,408,159,137,0,0,0,0,0],
+    [0,1374,398,166,136,0,0,0,0,0],
+    [0,1374,405,160,137,0,0,0,0,0],
+    [0,1377,395,167,136,0,0,0,0,0],
+    [0,1377,402,161,137,0,0,0,0,0],
+    [0,1378,404,158,138,0,0,0,0,0],
+    [0,1380,392,168,136,0,0,0,0,0],
+    [0,1380,399,162,137,0,0,0,0,0],
+    [0,1381,402,157,139,0,0,0,0,0],
+    [0,1383,389,169,136,0,0,0,0,0],
+    [0,1383,396,163,137,0,0,0,0,0],
+    [0,1384,400,156,140,0,0,0,0,0],
+    [0,1386,386,170,136,0,0,0,0,0],
+    [0,1386,393,164,137,0,0,0,0,0],
+    [0,1387,397,157,140,0,0,0,0,0],
+    [0,1389,383,171,136,0,0,0,0,0],
+    [0,1389,390,165,137,0,0,0,0,0],
+    [0,1390,394,158,140,0,0,0,0,0],
+    [0,1392,380,172,136,0,0,0,0,0],
+    [0,1392,387,166,137,0,0,0,0,0],
+    [0,1393,391,159,140,0,0,0,0,0],
+    [0,1395,384,167,137,0,0,0,0,0],
+    [0,1396,388,160,140,0,0,0,0,0],
+    [0,1398,381,168,137,0,0,0,0,0],
+    [0,1399,385,161,140,0,0,0,0,0],
+    [0,1399,392,155,141,0,0,0,0,0],
+    [0,1401,378,169,137,0,0,0,0,0],
+    [0,1402,382,162,140,0,0,0,0,0],
+    [0,1402,389,156,141,0,0,0,0,0],
+    [0,1404,375,170,137,0,0,0,0,0],
+    [0,1405,379,163,140,0,0,0,0,0],
+    [0,1405,386,157,141,0,0,0,0,0],
+    [0,1406,388,154,142,0,0,0,0,0],
+    [0,1407,372,171,137,0,0,0,0,0],
+    [0,1408,376,164,140,0,0,0,0,0],
+    [0,1408,383,158,141,0,0,0,0,0],
+    [0,1409,386,153,143,0,0,0,0,0],
+    [0,1411,373,165,140,0,0,0,0,0],
+    [0,1411,380,159,141,0,0,0,0,0],
+    [0,1412,384,152,144,0,0,0,0,0],
+    [0,1414,370,166,140,0,0,0,0,0],
+    [0,1414,377,160,141,0,0,0,0,0],
+    [0,1415,381,153,144,0,0,0,0,0],
+    [0,1417,367,167,140,0,0,0,0,0],
+    [0,1417,374,161,141,0,0,0,0,0],
+    [0,1418,378,154,144,0,0,0,0,0],
+    [0,1420,364,168,140,0,0,0,0,0],
+    [0,1420,371,162,141,0,0,0,0,0],
+    [0,1421,375,155,144,0,0,0,0,0],
+    [0,1423,368,163,141,0,0,0,0,0],
+    [0,1424,372,156,144,0,0,0,0,0],
+    [0,1426,365,164,141,0,0,0,0,0],
+    [0,1427,369,157,144,0,0,0,0,0],
+    [0,1429,362,165,141,0,0,0,0,0],
+    [0,1430,366,158,144,0,0,0,0,0],
+    [0,1432,359,166,141,0,0,0,0,0],
+    [0,1433,363,159,144,0,0,0,0,0],
+    [0,1435,356,167,141,0,0,0,0,0],
+    [0,1436,360,160,144,0,0,0,0,0],
+    [0,1439,357,161,144,0,0,0,0,0],
+    [0,1442,354,162,144,0,0,0,0,0],
+    [0,1445,351,163,144,0,0,0,0,0],
+    [0,1448,348,164,144,0,0,0,0,0]
+  ]
+}
diff --git a/research/complex-ck-b-frame-seed20/CLAIM.json b/research/complex-ck-b-frame-seed20/CLAIM.json
new file mode 100644
index 0000000000..0aeebb54dc
--- /dev/null
+++ b/research/complex-ck-b-frame-seed20/CLAIM.json
@@ -0,0 +1,23 @@
+{
+  "track": "complex supplier",
+  "assignment_seed": 20,
+  "random_source": "Python secrets.randbelow(100), operating-system randomness",
+  "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60",
+  "object": "Selected PR626 CK provider, retained PR622 canonical word, simultaneous B-phase frame reassignment at fixed scalar gate order",
+  "method": "Exact F2 subspace lower/upper propagation and per-register rank-partition bounds on the paid recursive moment; preserve A, cut, tail, cleanup, boundaries and ownership",
+  "candidate_tasks": [
+    "Additional signed K-triangles: covered by PR646",
+    "Coordinate-total factory resynthesis: overlaps PR681 and changed-dirt factory PR645",
+    "Fixed-order CK B-phase frame retiming: selected; seed 20 modulo 2 selects CK rather than JP8"
+  ],
+  "expected_deliverable": "One finite improving frame witness or a scoped negative certificate with a reproducible checker and controls; no unsupported kappa claim",
+  "expected_finish_utc": "2026-10-13T04:33:00Z",
+  "coordination": "No pinned issues and no open sprint/coordination issue found. Local claim, with open PR overlap checks.",
+  "overlap_snapshot": "501 open PRs through #681; PR661 supplies a related bit-frame barrier, while this object has complex F2-labelled frames and fixed CK tail interfaces",
+  "status": "completed: scoped negative result, no new kappa",
+  "result": "All 474 flexible gates in the selected CK B phase were eliminated over their complete F2 subspace domains. The baseline paid histogram is optimal for every 0 < p < 1 at fixed scalar order and exact end-of-B frames. All 118 distinct retained alternatives are strictly worse.",
+  "result_link": "https://github.com/CrocSwap/integer-mult-bounds/pull/698",
+  "evidence": "README.md and CERTIFICATE.json; reproduce with python3 -B research/complex-ck-b-frame-seed20/check.py",
+  "final_overlap": "513 open PRs through #693, followed immediately by review of #694-#697. #696 lowers scalar primitives with unchanged frames; #697 changes source access and helper count. Neither overlaps this fixed-circuit frame barrier.",
+  "completed_utc": "2026-10-13T04:22:26Z"
+}
diff --git a/research/complex-ck-b-frame-seed20/README.md b/research/complex-ck-b-frame-seed20/README.md
new file mode 100644
index 0000000000..c3d9adf6e9
--- /dev/null
+++ b/research/complex-ck-b-frame-seed20/README.md
@@ -0,0 +1,213 @@
+# A fixed-boundary frame barrier for the selected CK supplier
+
+**Scoped negative result. No new kappa.** The selected CK complex supplier's
+1,930 B-phase scalar gates already minimize their paid recursive moment among
+all simultaneous frame reassignments that preserve their order, operands and
+exact end-of-B register frames. This holds for every power `0 < p < 1`, with
+cost `sum H[r] * r**p`. The allowed frames are all subspaces of `F_2^9`, including
+ones absent from the retained frame catalogue.
+
+This closes a specific optimization class. It does not claim unique frames,
+optimality after reordering or resynthesis, optimality with changed B boundaries,
+or optimality of the JP8 provider. The scalar word and every existing repository
+file remain unchanged.
+
+## Reproduce
+
+From the repository root, using Python 3.11 or later and its standard library:
+
+```sh
+python3 -B research/complex-ck-b-frame-seed20/check.py
+```
+
+The command checks the source pins, reconstructs the complete frame domains,
+recomputes [CERTIFICATE.json](CERTIFICATE.json), and runs the independent
+enumeration checks and negative controls. The core receipt prints:
+
+```text
+PASS_CK_FIXED_END_B_FRAME_BOUND gates=1930 flexible=474 profiles=119 exponent=0<p<1
+```
+
+The core checker can also be run alone as `python3 -B
+research/complex-ck-b-frame-seed20/verify.py`. Neither command writes files,
+needs a solver, or fetches data. They fail if pinned inputs or the receipt differ.
+
+## Object, accounting and boundary
+
+Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+The selected record at this base is conditional
+`kappa = 51110230636731/31250000000000000 = 0.001635527380375392`.
+Its [maintainer review](../../docs/research/community-k492-review.md) explains
+that #626 retains #622's provider definitions and changes the owner allocation.
+The input here is the freshly replayed #622 CK
+[canonical word](../community-k492-audit/pr622/replay/ck-local/CANONICAL-WORD.json.gz).
+Its decompressed hash matches the CK identity in #626's retained SPEC.
+[SOURCES.json](SOURCES.json) pins both heads and eight source files.
+
+Only B frames vary. A, the center cut, precondition, compensation, cleanup tail,
+FULL cleanup, initial/final adapters, helpers, coefficients and owners are fixed.
+The center phase acts on private copies, so A's ending live frames are B's
+starting frames. Each scalar gate uses one common frame for its operands.
+Each operand climbs monotonically to it, paying one child whose rank is the
+dimension increase. See the retained
+[emitter](../complex-k492-owner-repair/code/hpe_emit_local.py) and
+[native auditor](../complex-k492-owner-repair/code/hpe_audit_and_transport.py).
+
+For each register touched in B, its last gate is pinned to the original frame.
+There are 492 distinct pinned gates. This preserves every end-of-B frame exactly,
+including the boundary used by the cold-helper row/column cone check. All later
+climbs and all endpoint wrappers therefore stay fixed. The scalar circuit itself
+is unchanged on arbitrary input and helper columns, in either orientation.
+
+The baseline B histogram is
+
+```text
+H_B = {1:1236, 2:496, 3:200, 4:96}, rank mass = 3212.
+```
+
+The checker separately recounts the fixed A, center, tail and final climbs:
+
+```text
+H_fixed = {1:1360, 2:56, 3:104, 4:64, 5:70, 6:8, 8:8}.
+H_total = {1:2596, 2:552, 3:304, 4:160, 5:70, 6:8, 8:8}.
+```
+
+Their sum matches the canonical word's complete local profile. The native
+[moment engine](../complex-multicold/engines/moment.py) multiplies
+`sum H[r]*r**(1-a)` by the positive factor `m**(a-1)/W`. Thus the result covers
+its recursive moment for every `0 < a < 1`. No global assembly or new exponent
+is inferred from this local certificate.
+
+## Complete finite domain
+
+Forward propagation takes the join of the current operand frames. Reverse
+propagation takes their intersection. Both passes inject the exact last-gate
+pins. Induction along each register proves that every feasible frame at gate
+`i` lies between the resulting subspaces `L_i` and `U_i`.
+
+The quotient dimensions `dim(U_i/L_i)` are 0, 1 or 2. Their complete subspace
+intervals contain 1, 2 or 5 frames respectively. The checker enumerates an
+interval by repeatedly adjoining each missing vector. Every intermediate
+subspace has a basis extending the lower subspace, so this reaches all of them.
+
+| Gate domains | Number of gates |
+| --- | ---: |
+| One frame | 1,456 |
+| Two frames | 418 |
+| Five frames | 56 |
+
+The unrestricted product is `2**418 * 5**56` assignments before shared-register
+constraints. This is not a sampled search. A factor for every operand transition
+checks subspace inclusion and charges its exact rank difference. These factors
+and the pinned boundaries are equivalent to the entire monotone common-frame
+constraint in the stated class.
+
+Min-fill variable elimination exhausts that factor graph. A table entry retains
+all paid histograms not excluded by the exact dominance rule below. Eliminating
+a gate combines all incident factors and enumerates every gate-domain value for
+each separator assignment. Discarded histories have no future constraints except
+that separator, which is the usual variable-elimination invariant.
+
+The largest separator has five gates. The replay evaluates 4,724 local domain
+assignments, retains at most five histograms per conditional table entry, and
+ends with 119 profiles. This count is work after exact elimination, not the
+number of feasible full schedules. The stopping rule is elimination of every
+one of the 474 flexible gates; there is no timeout or incomplete branch.
+
+## Why the pruning and final comparison are exact
+
+For a histogram `H`, let `M(H)=sum r*H[r]` and
+`S_k(H)=sum min(r,k)*H[r]`. At a fixed separator, transition ranks telescope, so
+all alternatives have the same mass. The implementation asserts this invariant.
+It discards `G` only when another profile `H` has equal mass and
+`S_k(H) <= S_k(G)` for all integer `1 <= k <= 9`.
+
+To justify that rule, set `f(r)=r**p`, `f(0)=0`, and
+`d_k=f(k)-f(k-1)`. For `0<p<1`, the `d_k` decrease and
+
+```text
+f(r) = d_9*r + sum_{k=1}^8 (d_k-d_{k+1})*min(r,k).
+```
+
+All coefficients on the right are nonnegative. Dominance therefore holds for
+every power in the claimed interval and remains valid when adding other factors.
+Incomparable profiles are retained rather than resolved by floating arithmetic.
+
+Concave dominance alone leaves 119 profiles. One is the baseline. Every other
+profile differs only at ranks 1 through 4. Write its cost minus the baseline as
+
+```text
+D(p) = a + b*2**p + c*3**p + d*4**p.
+```
+
+The checker establishes `b<=0`, `d>=0` and `a+2*b+3*c+4*d=0` for all 118
+alternatives. Thus `D(1)=0`. It also certifies `D'(1)<0` exactly:
+
+```text
+D'(1) = (2*b+8*d)*log(2) + 3*c*log(3).
+```
+
+Eight terms of the rational atanh series, with its geometric remainder, prove
+`69/100 < log(2) < 7/10` and `109/100 < log(3) < 11/10`. Substituting the
+appropriate endpoint for each coefficient gives a strictly negative upper
+bound in every case. The largest is `-21/25`.
+
+If `c>=0`, then `D'(p)/2**p` is nondecreasing in `p`, because its nonconstant
+terms have nonnegative coefficients and bases greater than one. If `c<0`, use
+`D'(p)/3**p`: the term with coefficient `b*log(2)` has base `2/3`, so it is
+nondecreasing because `b<=0`; the `d*log(4)` term has base `4/3` and is also
+nondecreasing. The remaining term is constant. In either case `D'(1)<0` implies
+`D'(p)<0` for `p<1`. Integrating to `D(1)=0` gives `D(p)>0` for `0<p<1`.
+
+Every feasible profile is therefore no better than a retained profile, and
+every distinct retained profile is worse than the baseline. This proves weak
+optimality of the baseline paid moment in the stated finite class. It does not
+prove uniqueness of the frame assignment.
+
+## Sprint choice, provenance and limits
+
+The operating-system assignment seed was **20**, selecting the complex-supplier
+track and CK via `20 modulo 2`. The algorithm itself is deterministic. Three
+candidates and the local claim are recorded in [CLAIM.json](CLAIM.json). No
+pinned coordination issue existed. The initial overlap review covered 501 open
+PRs through #681, plus the maintainer ledger and relevant prior negative results.
+
+Related #661, by @yuj1r0, proves an all-frame barrier for the R420 **bit** B phase.
+This complex instance has coupled frame choices that its per-register argument
+does not settle. The contribution here is complete finite-domain elimination
+for CK with its cold-helper boundary, plus the four-rank derivative certificate.
+No code was imported from #661. #651 studies target hosting and raw-face sharing,
+#646 changes the K-triangle skeleton, and #681/#645 change factory circuits or
+dirty-input propagation. Those mechanisms are outside this fixed-circuit class.
+The final refresh covered 513 open PRs through #693. New #683 concerns mixed
+K/M bypass carriers and #687 enumerates one-read relocations under minimal join
+frames. Neither changes this result's fixed-order, all-frame scope or supplies
+a dependency. The pinned-issue query remained empty.
+Immediately before submission, #694 through #697 were also reviewed. #696
+lowers complex scalar primitives while preserving frames; #697 changes source
+access and helper count. Both lie outside the fixed-circuit class here.
+
+Credit goes to Jeremy Kothe's #622 K-triangle construction and schedule;
+Chafik Boukhalfa's #626 owner package; DreamingOfClouds' cold-helper, emitter and
+native-verification work; icekylinx's coordinate-total/direct-delivery lineage;
+Dominik Scholz's prefix work; the frame-coalescing, recurrence and remaining
+contributors retained in the selected review. The unchanged bit supplier is
+eumemic's #543. Their results are inputs, not new contributions of this note.
+
+Prepared for **@thakrarsagar**, with substantial **OpenAI Codex** assistance in
+research, implementation, proof development, independent checks and writing.
+New files use the repository's Apache-2.0 license. No predecessor file is copied
+or relicensed.
+
+The finite certificate does not reprove the inherited scalar construction,
+uniform compiler, common-label or mutable-basis realization, whole-call hosting,
+normalized residuals, precision/tape/exact recovery or analytic transfer.
+It is not a Lean proof or a full multiplication-theorem audit. Reordering,
+different helper/source interfaces, changed boundary frames, and JP8 remain
+outside this result. The expensive full supplier/global replay is not needed to
+establish this isolated barrier and was not rerun; the selected-record check was.
+The complete package command passed on macOS arm64 with Python 3.11.17 and
+3.14.8. [VALIDATION.json](VALIDATION.json) records the checks and their limits.
+The same command passed from a clean archive containing only this package and
+the eight pinned inputs. [PR #698](https://github.com/CrocSwap/integer-mult-bounds/pull/698)
+is the completed sprint handoff.
diff --git a/research/complex-ck-b-frame-seed20/SOURCES.json b/research/complex-ck-b-frame-seed20/SOURCES.json
new file mode 100644
index 0000000000..c3acf2846a
--- /dev/null
+++ b/research/complex-ck-b-frame-seed20/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60",
+  "reviewed_pr622_head": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6",
+  "reviewed_pr626_head": "660de893d27bb7abd1d5b01b1640207528a5c851",
+  "canonical_decompressed_sha256": "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7",
+  "related_pr661_head": "9ca7aa3ab0a3260a2f36ac86b9911a31fd88bd89",
+  "related_pr661_role": "Related bit-supplier fixed-order barrier; no imported code or result dependency",
+  "files": {
+    "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53",
+    "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47",
+    "research/complex-k492-owner-repair/data/SPEC.json": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323",
+    "research/complex-k492-owner-repair/code/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805",
+    "research/complex-k492-owner-repair/code/hpe_audit_and_transport.py": "c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3",
+    "research/complex-multicold/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482",
+    "research/community-k492-audit/pr622/replay/ck-local/CANONICAL-WORD.json.gz": "ae3018c0646be06f47d345bb8baf0e6ea9220096a949fa30a8f7656aa4ad6f45",
+    "research/community-k492-audit/pr622/replay/ck-local/SCALAR-FRAME-AUDIT.json": "9a2972bed8a6a66f3716b50a5b325095e86f0904581256ac10127ee672886f61"
+  }
+}
diff --git a/research/complex-ck-b-frame-seed20/VALIDATION.json b/research/complex-ck-b-frame-seed20/VALIDATION.json
new file mode 100644
index 0000000000..945f91f9cc
--- /dev/null
+++ b/research/complex-ck-b-frame-seed20/VALIDATION.json
@@ -0,0 +1,19 @@
+{
+  "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60",
+  "platform": "macOS 26.5.2 arm64",
+  "python_versions": ["3.11.17", "3.14.8"],
+  "reproduce": "python3 -B research/complex-ck-b-frame-seed20/check.py",
+  "checks": {
+    "complete_certificate_both_python_versions": "PASS_CK_FIXED_END_B_FRAME_BOUND gates=1930 flexible=474 profiles=119 exponent=0<p<1",
+    "direct_enumeration": {"actual_components": 100, "actual_assignments": 1544, "coupled_synthetic_assignments": 125},
+    "negative_controls": ["inferior split-jump baseline does not pass optimality", "equal-rank incomparable frames rejected by factors and independent Gaussian replay"],
+    "power_comparison": {"strict_alternatives": 118, "independent_method": "rational integral Riemann sums for logarithm brackets", "largest_derivative_upper": "-21/25"},
+    "optimized_python": "Rejected before verification with a nonzero exit and an explicit assertion-requirement error",
+    "clean_archive": "The complete package check passed with Python 3.11.17 in a fresh git archive containing only the package and its eight pinned source files, from commit ca1cbf6",
+    "selected_record": "PASS selected record, exact kappa, original source inventory and proof supplement: 51110230636731/31250000000000000",
+    "whitespace": "git diff --check passed"
+  },
+  "overlap_refresh": {"open_prs": 513, "latest_pr": 693, "immediate_followup_prs": [694, 695, 696, 697], "pinned_issues": 0, "result": "No matching CK fixed-end-B all-frame claim found; related #661, #651, #646, #681, #645, #683, #687, #696 and #697 distinguished in README"},
+  "not_run": ["make verify", "full selected supplier cold replay", "global assembly", "Linux CI", "Lean"],
+  "reason": "Only this new research package changes. Existing suppliers, generators, selected certificates, native accounting and upstream are untouched. The new finite claim has its own complete exact check."
+}
diff --git a/research/complex-ck-b-frame-seed20/check.py b/research/complex-ck-b-frame-seed20/check.py
new file mode 100644
index 0000000000..57062c1052
--- /dev/null
+++ b/research/complex-ck-b-frame-seed20/check.py
@@ -0,0 +1,185 @@
+#!/usr/bin/env python3
+"""Small exhaustive cross-checks. @thakrarsagar / OpenAI Codex, Apache-2.0."""
+import gzip
+import itertools
+import json
+import runpy
+from fractions import Fraction
+from functools import lru_cache
+
+import verify as v
+
+@lru_cache(None)
+def linear_rank(vectors):
+    """Independent Gaussian elimination, rather than log2 of a span's size."""
+    pivots = {}
+    for x in vectors:
+        while x:
+            bit = x.bit_length() - 1
+            if bit not in pivots:
+                pivots[bit] = x
+                break
+            x ^= pivots[bit]
+    return len(pivots)
+
+
+def inside(before, after):
+    return linear_rank(tuple(sorted(before | after))) == linear_rank(tuple(sorted(after)))
+
+
+def score(profile):
+    jumps = [r for r, count in enumerate(profile) for _ in range(count)]
+    return sum(jumps), tuple(sum(min(r, k) for r in jumps) for k in range(1, 10))
+
+
+def reference_frontier(profiles):
+    profiles = set(profiles)
+    scores = {p: score(p) for p in profiles}
+    return {p for p in profiles if not any(
+        q != p and scores[q][0] == scores[p][0]
+        and all(a <= b for a, b in zip(scores[q][1], scores[p][1]))
+        for q in profiles)}
+
+
+def factor_profile(factors, assignment):
+    result = [0] * 10
+    for keys, table in factors:
+        contribution = table.get(tuple(assignment[x] for x in keys))
+        if contribution is None:
+            return None
+        for r, count in enumerate(contribution):
+            result[r] += count
+    return tuple(result)
+
+
+def direct_profile(word, domains, assignment, expected_end):
+    frames = [frozenset(basis) for basis in word['frames']]
+    current = [frames[f] for f in word['start']]
+    for gate in word['A']:
+        for register in gate[1:3] if gate[0] == 'add' else gate[1:2]:
+            current[register] = frames[gate[-1]]
+    result = [0] * 10
+    for i, gate in enumerate(word['B']):
+        frame = domains[i][assignment[i]] if i in domains else frames[gate[-1]]
+        for register in gate[1:3] if gate[0] == 'add' else gate[1:2]:
+            before = current[register]
+            if not inside(before, frame):
+                return None
+            jump = linear_rank(tuple(sorted(frame))) - linear_rank(tuple(sorted(before)))
+            if jump:
+                result[jump] += 1
+            current[register] = frame
+    if not all(inside(a, b) and inside(b, a) for a, b in zip(current, expected_end)):
+        return None
+    return tuple(result)
+
+
+def exhaustive(domains, factors, word=None, end=None):
+    keys = sorted(domains)
+    profiles = set()
+    checked = 0
+    for values in itertools.product(*(range(len(domains[x])) for x in keys)):
+        assignment = dict(zip(keys, values))
+        profile = factor_profile(factors, assignment)
+        if word is not None:
+            assert profile == direct_profile(word, domains, assignment, end)
+        if profile is not None:
+            profiles.add(profile)
+        checked += 1
+    actual, _ = v.eliminate(domains, factors)
+    assert set(actual) == reference_frontier(profiles)
+    return checked, set(actual)
+
+
+def components(domains, factors):
+    neighbors = {x: set() for x in domains}
+    for keys, _ in factors:
+        for x in keys:
+            neighbors[x].update(set(keys) - {x})
+    remaining = set(domains)
+    result = []
+    while remaining:
+        component = {remaining.pop()}
+        pending = list(component)
+        while pending:
+            adjacent = neighbors[pending.pop()] & remaining
+            remaining -= adjacent
+            component |= adjacent
+            pending.extend(adjacent)
+        result.append(component)
+    return result
+
+
+def main():
+    runpy.run_path(str(v.HERE / 'verify.py'), run_name='__main__')
+    word = json.loads(gzip.decompress(v.SOURCE.read_bytes()))
+    frames, start, end, pinned, domains, factors = v.problem(word)
+    assert len(pinned) == 492 and len(domains) == 474
+    for frame in frames:
+        assert v.rank(frame) == linear_rank(tuple(sorted(frame)))
+    baseline_assignment = {i: domains[i].index(frames[word['B'][i][-1]]) for i in domains}
+    baseline = direct_profile(word, domains, baseline_assignment, end)
+    assert baseline == factor_profile(factors, baseline_assignment)
+    assert baseline == (0, 1236, 496, 200, 96, 0, 0, 0, 0, 0)
+
+    groups = components(domains, factors)
+    small = [group for group in groups if len(group) <= 3]
+    assert len(groups) == 120 and len(small) == 100
+    checked = 0
+    for group in small:
+        local_factors = [(keys, table) for keys, table in factors if set(keys) & group]
+        assert all(set(keys) <= group for keys, _ in local_factors)
+        count, _ = exhaustive({x: domains[x] for x in group}, local_factors)
+        checked += count
+
+    # Three flexible gates form a triangle, so this exercises coupled elimination.
+    toy = dict(frames=[[], [1], [2], [1, 2]], start=[0, 0, 0], A=[], B=[
+        ['add', 0, 1, 1, 1, 1], ['add', 1, 2, 1, 1, 1],
+        ['add', 0, 2, 1, 1, 3], ['add', 0, 1, 1, 1, 3],
+        ['add', 1, 2, 1, 1, 3]])
+    tf, ts, te, _, td, factors = v.problem(toy)
+    count, frontier = exhaustive(td, factors, toy, te)
+    assert count == 125 and frontier == {(0, 0, 3, 0, 0, 0, 0, 0, 0, 0)}
+    original = v.recount(toy, tf, ts, te, {})
+    assert original == (0, 6, 0, 0, 0, 0, 0, 0, 0, 0)
+    assert not any(v.dominates(original, p) for p in frontier)
+
+    # Equal ranks cannot substitute for actual subspace containment.
+    bad = {i: td[i].index(tf[3]) for i in td}
+    bad[0] = td[0].index(tf[1])
+    bad[1] = td[1].index(tf[2])
+    assert factor_profile(factors, bad) is None
+    assert direct_profile(toy, td, bad, te) is None
+    assert linear_rank((1,)) == linear_rank((2,)) and not inside(frozenset({1}), frozenset({2}))
+
+    # Independent integral bounds, rather than verify.py's atanh series.
+    for x, lo, hi in [(2, Fraction(69, 100), Fraction(7, 10)),
+                      (3, Fraction(109, 100), Fraction(11, 10))]:
+        right = sum((Fraction(x - 1, 1000 + k * (x - 1)) for k in range(1, 1001)), Fraction(0))
+        left = right + Fraction(x - 1, 1000) * (1 - Fraction(1, x))
+        assert lo < right < left < hi
+    receipt = json.loads((v.HERE / 'CERTIFICATE.json').read_text())
+    strict_bounds = []
+    for profile in receipt['final_frontier']:
+        delta = [a - b for a, b in zip(profile, receipt['baseline_histogram'])]
+        if not any(delta):
+            continue
+        assert delta[0] == 0 and not any(delta[5:])
+        a, b, c, d = delta[1:5]
+        assert b <= 0 <= d and a + 2*b + 3*c + 4*d == 0
+        coefficients = (2*b + 8*d, 3*c)
+        intervals = ((Fraction(69, 100), Fraction(7, 10)),
+                     (Fraction(109, 100), Fraction(11, 10)))
+        upper = sum(max(coefficient * endpoint for endpoint in interval)
+                    for coefficient, interval in zip(coefficients, intervals))
+        assert upper < 0
+        strict_bounds.append(upper)
+    assert len(strict_bounds) == 118 and max(strict_bounds) == Fraction(-21, 25)
+    print(json.dumps(dict(status='PASS_EXHAUSTIVE_CROSS_CHECKS',
+        actual_components=len(small), actual_assignments=checked,
+        coupled_synthetic_assignments=count, negative_controls=2,
+        strict_power_alternatives=len(strict_bounds)), sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/complex-ck-b-frame-seed20/verify.py b/research/complex-ck-b-frame-seed20/verify.py
new file mode 100644
index 0000000000..43b1a7efef
--- /dev/null
+++ b/research/complex-ck-b-frame-seed20/verify.py
@@ -0,0 +1,307 @@
+#!/usr/bin/env python3
+"""Exact finite-domain CK frame analysis. @thakrarsagar / OpenAI Codex, Apache-2.0."""
+import gzip
+import hashlib
+import itertools
+import json
+from collections import Counter
+from fractions import Fraction
+from pathlib import Path
+
+if not __debug__:
+    raise RuntimeError('Run without -O; this certificate requires assertions.')
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+SOURCE = ROOT / 'research/community-k492-audit/pr622/replay/ck-local/CANONICAL-WORD.json.gz'
+SOURCE_SHA256 = 'ae3018c0646be06f47d345bb8baf0e6ea9220096a949fa30a8f7656aa4ad6f45'
+
+
+def span(vectors):
+    result = {0}
+    for vector in vectors:
+        result |= {x ^ vector for x in result}
+    return frozenset(result)
+
+
+def rank(frame):
+    n = len(frame)
+    assert n > 0 and n & (n - 1) == 0
+    return n.bit_length() - 1
+
+
+def operands(gate):
+    assert gate[0] in ('add', 'scale')
+    return gate[1:3] if gate[0] == 'add' else gate[1:2]
+
+
+def interval(lower, upper):
+    """Enumerate the entire subspace interval, including uncatalogued frames."""
+    assert lower <= upper
+    found = {lower}
+    todo = [lower]
+    while todo:
+        frame = todo.pop()
+        for vector in sorted(upper - frame):
+            enlarged = frame | frozenset(x ^ vector for x in frame)
+            if enlarged not in found:
+                found.add(enlarged)
+                todo.append(enlarged)
+    return sorted(found, key=lambda x: (rank(x), tuple(sorted(x))))
+
+
+def histogram(ranks):
+    counts = Counter(r for r in ranks if r)
+    assert all(0 < r <= 9 for r in counts)
+    return tuple(counts[r] for r in range(10))
+
+
+ZERO = (0,) * 10
+
+
+def plus(left, right):
+    return tuple(a + b for a, b in zip(left, right))
+
+
+def dominates(left, right):
+    """Sufficient exact order for every concave power r**p, 0 < p < 1."""
+    if sum(r * n for r, n in enumerate(left)) != sum(r * n for r, n in enumerate(right)):
+        return False
+    return all(sum(min(r, k) * (a - b) for r, (a, b) in enumerate(zip(left, right))) <= 0
+               for k in range(1, 10))
+
+
+def problem(word):
+    frames = list(map(span, word['frames']))
+    gates = word['B']
+    start = [frames[f] for f in word['start']]
+    for gate in word['A']:
+        for register in operands(gate):
+            assert start[register] <= frames[gate[-1]]
+            start[register] = frames[gate[-1]]
+    end = start.copy()
+    last = {}
+    for i, gate in enumerate(gates):
+        for register in operands(gate):
+            assert end[register] <= frames[gate[-1]]
+            end[register] = frames[gate[-1]]
+            last[register] = i
+    pinned = set(last.values())
+    current = start.copy()
+    lower = []
+    for i, gate in enumerate(gates):
+        frame = frames[gate[-1]] if i in pinned else span(
+            x for register in operands(gate) for x in current[register])
+        lower.append(frame)
+        for register in operands(gate):
+            assert current[register] <= frame
+            current[register] = frame
+    current = end.copy()
+    upper = [None] * len(gates)
+    for i in reversed(range(len(gates))):
+        gate = gates[i]
+        frame = frames[gate[-1]] if i in pinned else frozenset.intersection(
+            *(current[register] for register in operands(gate)))
+        upper[i] = frame
+        for register in operands(gate):
+            assert frame <= current[register]
+            current[register] = frame
+    domains = {}
+    for i, (lo, hi) in enumerate(zip(lower, upper)):
+        assert lo <= frames[gates[i][-1]] <= hi
+        if lo != hi:
+            domains[i] = interval(lo, hi)
+    # A factor charges one register transition, with exact inclusion enforced.
+    factors = []
+    previous = [None] * len(start)
+    for i, gate in enumerate(gates):
+        for register in operands(gate):
+            j = previous[register]
+            keys = tuple(x for x in (j, i) if x in domains)
+            table = {}
+            for values in itertools.product(*(range(len(domains[x])) for x in keys)):
+                assignment = dict(zip(keys, values))
+                before = domains[j][assignment[j]] if j in domains else (
+                    frames[gates[j][-1]] if j is not None else start[register])
+                after = domains[i][assignment[i]] if i in domains else frames[gate[-1]]
+                if before <= after:
+                    table[values] = histogram([rank(after) - rank(before)])
+            assert table
+            factors.append((keys, table))
+            previous[register] = i
+    return frames, start, end, pinned, domains, factors
+
+
+def pareto(histograms):
+    """Keep every profile not excluded by exact concave dominance."""
+    kept = []
+    for candidate in sorted(set(histograms)):
+        if any(dominates(old, candidate) for old in kept):
+            continue
+        kept = [old for old in kept if not dominates(candidate, old)]
+        kept.append(candidate)
+    return tuple(kept)
+
+
+def combine(left, right):
+    return pareto(plus(a, b) for a in left for b in right)
+
+
+def eliminate(domains, initial_factors):
+    """Exact min-fill elimination retaining all incomparable paid profiles."""
+    factors = [(keys, {values: (profile,) for values, profile in table.items()})
+               for keys, table in initial_factors]
+    remaining = set(domains)
+    evaluated = width = max_frontier = 0
+    conditional_profiles = 0
+    while remaining:
+        graph = {x: set() for x in remaining}
+        for keys, table in factors:
+            for x in keys:
+                graph[x].update(set(keys) - {x})
+        def priority(x):
+            neighbors = graph[x]
+            missing = sum(b not in graph[a] for a in neighbors for b in neighbors if a < b)
+            return missing, len(neighbors), x
+        selected = min(remaining, key=priority)
+        bucket = [(keys, table) for keys, table in factors if selected in keys]
+        factors = [(keys, table) for keys, table in factors if selected not in keys]
+        separator = tuple(sorted(set().union(*(set(keys) for keys, table in bucket)) - {selected}))
+        width = max(width, len(separator))
+        reduced = {}
+        for values in itertools.product(*(range(len(domains[x])) for x in separator)):
+            assignment = dict(zip(separator, values))
+            candidates = []
+            for value in range(len(domains[selected])):
+                evaluated += 1
+                assignment[selected] = value
+                total = (ZERO,)
+                for keys, table in bucket:
+                    contribution = table.get(tuple(assignment[x] for x in keys))
+                    if contribution is None:
+                        break
+                    total = combine(total, contribution)
+                else:
+                    candidates.extend(total)
+            if not candidates:
+                continue
+            # Eliminated register ranks telescope; separators fix the mass.
+            assert len({sum(r * n for r, n in enumerate(h)) for h in candidates}) == 1
+            frontier = pareto(candidates)
+            max_frontier = max(max_frontier, len(frontier))
+            conditional_profiles += len(frontier)
+            reduced[values] = frontier
+        assert reduced
+        factors.append((separator, reduced))
+        remaining.remove(selected)
+    result = (ZERO,)
+    for keys, table in factors:
+        assert keys == () and set(table) == {()}
+        result = combine(result, table[()])
+    return result, dict(evaluated=evaluated, induced_width=width,
+                        max_conditional_frontier=max_frontier,
+                        conditional_profiles=conditional_profiles)
+
+
+def recount(word, frames, start, end, assigned):
+    current = start.copy()
+    increments = []
+    for i, gate in enumerate(word['B']):
+        frame = assigned.get(i, frames[gate[-1]])
+        for register in operands(gate):
+            assert current[register] <= frame
+            increments.append(rank(frame) - rank(current[register]))
+            current[register] = frame
+    assert current == end
+    return histogram(increments)
+
+
+def outside_profile(word, frames, end):
+    current = [frames[f] for f in word['start']]
+    increments = []
+    def climb(register, frame):
+        assert current[register] <= frame
+        increments.append(rank(frame) - rank(current[register]))
+        current[register] = frame
+    for gate in word['A']:
+        for register in operands(gate):
+            climb(register, frames[gate[-1]])
+    for register, frame_id in zip(word['centers'], word['center_frames']):
+        previous = frames[frame_id]
+        assert current[register] == previous
+        served = {word['target_levels'].get(str(gate[1] - word['v']), 0)
+                  for gate in word['cut'] if gate[2] == register}
+        for frame_id in sorted(served, key=lambda f: -rank(frames[f])):
+            frame = frames[frame_id]
+            assert frame <= previous
+            increments.append(rank(previous) - rank(frame))
+            previous = frame
+    current = end.copy()
+    for gate in word['tail']:
+        for register in operands(gate):
+            climb(register, frames[gate[-1]])
+    for register, frame_id in enumerate(word['final']):
+        climb(register, frames[frame_id])
+    return histogram(increments)
+
+
+def log_bounds(value):
+    """Eight terms of log(x)=2*atanh((x-1)/(x+1)), with geometric tail."""
+    z = Fraction(value - 1, value + 1)
+    lower = 2 * sum((z ** (2 * k + 1) / (2 * k + 1) for k in range(8)), Fraction(0))
+    upper = lower + 2 * z ** 17 / (17 * (1 - z * z))
+    return lower, upper
+
+
+def power_certificate(baseline, frontier):
+    """Certify every retained alternative is worse for all 0 < p < 1."""
+    for value, lower, upper in [(2, Fraction(69, 100), Fraction(7, 10)),
+                                (3, Fraction(109, 100), Fraction(11, 10))]:
+        lo, hi = log_bounds(value)
+        assert lower < lo < hi < upper
+    bounds = []
+    assert baseline in frontier
+    for alternative in frontier:
+        delta = tuple(a - b for a, b in zip(alternative, baseline))
+        if not any(delta):
+            continue
+        assert delta[0] == 0 and not any(delta[5:])
+        a, b, c, d = delta[1:5]
+        assert b <= 0 and d >= 0 and a + 2*b + 3*c + 4*d == 0
+        # D'(1)=(2b+8d)log(2)+3c*log(3); README proves why its sign suffices.
+        x, y = 2*b + 8*d, 3*c
+        upper = x * (Fraction(7, 10) if x > 0 else Fraction(69, 100))
+        upper += y * (Fraction(11, 10) if y > 0 else Fraction(109, 100))
+        assert upper < 0
+        bounds.append(upper)
+    return dict(strict_alternatives=len(bounds),
+                largest_derivative_upper=str(max(bounds)),
+                exponent_interval='0 < p < 1', baseline_power_optimal=True)
+
+
+def analyze(word):
+    frames, start, end, pinned, domains, factors = problem(word)
+    frontier, stats = eliminate(domains, factors)
+    baseline = recount(word, frames, start, end, {})
+    outside = outside_profile(word, frames, end)
+    full = tuple(int(word['local_profile'].get(str(r), 0)) for r in range(10))
+    assert plus(baseline, outside) == full
+    return dict(gates=len(word['B']), registers=len(start), pinned_gates=len(pinned),
+                flexible_gates=len(domains), domain_sizes=dict(sorted(Counter(map(len, domains.values())).items())),
+                baseline_histogram=baseline, final_frontier=frontier,
+                fixed_outside_histogram=outside, complete_local_histogram=full,
+                power_certificate=power_certificate(baseline, frontier),
+                **stats)
+
+
+if __name__ == '__main__':
+    pins = json.loads((HERE / 'SOURCES.json').read_text())
+    for path, expected_hash in pins['files'].items():
+        assert hashlib.sha256((ROOT / path).read_bytes()).hexdigest() == expected_hash, path
+    assert hashlib.sha256(SOURCE.read_bytes()).hexdigest() == SOURCE_SHA256, 'source pin mismatch'
+    word = json.loads(gzip.decompress(SOURCE.read_bytes()))
+    result = analyze(word)
+    result['source_sha256'] = SOURCE_SHA256
+    expected = json.loads((HERE / 'CERTIFICATE.json').read_text())
+    assert json.loads(json.dumps(result)) == expected, 'certificate mismatch'
+    print('PASS_CK_FIXED_END_B_FRAME_BOUND gates=1930 flexible=474 profiles=119 exponent=0<p<1')