diff --git a/research/decoder-floors-frontier-format/LICENSE b/research/decoder-floors-frontier-format/LICENSE
new file mode 100644
index 0000000000..261eeb9e9f
--- /dev/null
+++ b/research/decoder-floors-frontier-format/LICENSE
@@ -0,0 +1,201 @@
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
diff --git a/research/decoder-floors-frontier-format/MANIFEST.sha256 b/research/decoder-floors-frontier-format/MANIFEST.sha256
new file mode 100644
index 0000000000..09f74411a0
--- /dev/null
+++ b/research/decoder-floors-frontier-format/MANIFEST.sha256
@@ -0,0 +1,39 @@
+c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4  LICENSE
+95ffb286f159eaab0e1620fc860fea91b94fe14a28ed4a4da52716f52f53bc7a  NOTICE.md
+515b4fc40aa63515cda48740a16a7c87cea04384242369dac5be93e5556655b3  README.md
+888a92eab8c98345a1db302c574bddea59a534afdfb4bc83cd49053eb84e72af  SOURCES.json
+4041cfeb1bc5131b5b57cce79de13e013061566128db38707cdc50efc3333e6a  checks/c1_rigidity.py
+a24a7f0907970257cdcfeaf3d1d234c34974b64a3d7aa584283124d79e0def7a  checks/c2_support_propagation.py
+aa3c56bd79a36dd081b40e50c675064c4dc7e780aee02779813c618651cf0ad8  checks/c3_batch_premises.py
+f06d5cc4685e81f5c1b52391a6a4f7548d9da146f0891aabdab09843c260ae11  checks/c4_masked_costar.py
+359b20c67b8d4c0491a0a3b9cf5b595f5294570e6a7a98fbe900094396620790  checks/c5_attaining_decoders.py
+42e91b63e455ddf020b678700ed45dc3ad3703374ba9d063002fffe13770b981  checks/c6_block_minrank_punctures.py
+6d3e3bac50ef7054acaeaabecbc863e8f40c359655c61fc9483257184c25d6ae  checks/c7_p111_unit.py
+66d019f311fd436c7e04517349d8d3e47d75d970951a7c99e1ef523cffd405b6  data/chart_rank7.json
+33e368cad0c95cd4af1c1d06d3a7abbd28abd14900bcada084d7b7583d89a270  data/h4_F1.json
+52e1a2b0e963311eb74c1ec2bbb110497da57b606e132f784f9000603d10a306  data/p104_frames.json
+f85ac3b3c785964c04d53bcf879a74425d8d997ec3ccb92d971cce69c9c10a32  data/p104reps.json
+2b492989fd574f557533e237267bc6693d6917ce5b32e2ccdad7fa9de81a07f9  data/p111_lines.json
+b5e9f53dbdf15cb7667fd1e7d6db92f61fc773822746e895a56c2d21b6fa4612  lib/frames.py
+fc4bb6836cb34d310ca7b3275ef15ef2d5d03e511063ddb06d0eb60e7072a640  lib/report.py
+b2bdaa63376ab0c718b256e879d669f1465f4d3407b64ecc876ca0f3e6a32acd  lib/roots.py
+567df3a6f3277179f88cf17dffbe69dd40b1f6d8277baab3cb79e7332361077f  lib/satgen.py
+6872520ef5955082ab10e6f20960bb47cabfad03bdad246ebe79231007b36159  lib/solve.py
+a0883df40db120adc892aadec78ab15e6eefa7d8e7006883294ba1da62961081  lib/supprop.py
+43eed628ea4c39f5aa47945697ccfe4dc63bbfc21d91affdd8a7d698c8ccd569  lib/units.py
+71fc5fc5bbb088d340a1b3ed75348ab296154b25f3a9edc064f27bbe037b7158  requirements.txt
+8a4e7baaca75530be75d2483df1af4cbba48013c992129da5628bb2510ae0b82  sat/hitting.py
+5b72bcdf42c37cedb9cd4f60c61ac5fe884dbf2d78bf8e36939afe1c27f69358  sat/misc.py
+c748368f64c87d2842babb47f6ede23f8f16acf98bef8a48f5dd40259f3e2be1  sat/mkmisc.py
+3334ae7bd440971a6c751e8286a755cf632f0c3a325c1a27086bf6df5c0990df  sat/mkresults.py
+6d7b82565559777597a10dd65d34088ef03b65cd6789c55be59765b3ae30f89a  sat/proofs/E8_sym_h9_alt.drat.xz
+fc385861ff98a07cf9f6267d8cc169deb4262394b23a5780cf08c27567b523e6  sat/proofs/P104H4_sym_h9_alt.drat.xz
+6de05f478a04dfc97f5b66644262e2f0ac742f1b399bab775134641a9b30b04d  sat/proofs/P111_sym_h9_alt.drat.xz
+db1e4a2526ed9593f7b8444bde8da3062c37ac00a3a49faa4ae92b035d95cc7d  sat/proofs/P112_sym_h9_alt.drat.xz
+9a22571653eb87be39b4650d03e7587072f5fd6332cc4162bde629e17d872e51  sat/proofs/edge_N0_r7.drat.xz
+5f31be0fd422372d77319c45e51488bb8eb4474f4e31402715d40572b1ec2907  sat/proofs/tri_keep11.drat.xz
+d7115712b22dca41e37813ac1236a91c198210b089651f0ec5cced78f6bdf296  sat/results.jsonl
+30889985d57b5bf1139ea29d9f52f9f5c24365c036b1acc8e263878fef8f94b7  sat/results_misc.jsonl
+378f20d152d1c4c53c9bd528bd2e661fa75b68bbeaa1fecaa498af4acda9b0f9  sat/rigid.py
+a4cd33cef93721cd79ae3dfaf69556f8502b22152e363fcab33b1fa402d68d11  scripts/provenance.py
+af4002aefda1f5c703d970b4f2387f1468005f071047d91ef94839a7ab721943  verify.sh
diff --git a/research/decoder-floors-frontier-format/NOTICE.md b/research/decoder-floors-frontier-format/NOTICE.md
new file mode 100644
index 0000000000..8b1f75f7e7
--- /dev/null
+++ b/research/decoder-floors-frontier-format/NOTICE.md
@@ -0,0 +1,16 @@
+# Notice
+
+Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root).
+
+## Credits
+
+- **#446** (cost model, Theorem C), **#595**, **#1590**, **#2111**, **#2125**, **#2162**, **#2228**, **#2244**, **#2277**: the model, the dense pairing, the root-code floors (#2228 Theorem 4), Theorem 4′ and the frame-intersection certificate (#2277 §5) that this package extends. The statements "P112 ≥ 64 for every rank-8 realisation" (Theorem P), the cross-call batching bounds with `GL(9)` charts and `k ≥ 3` (Theorem B, Bk) and the every-`B` coordinate-block minrank are new here, built on those. Rigidity of the minimal-rank label table (Theorem R) is new here for E8, P112, P104 (#968's unit and class representatives), E7 and E6 only: for P111 it is prior work of **#620** (GamingPuzzled, SAT) and **#1097** (bitplane, merged, LRAT-checked in the general model), and **#1815** (jmbarrancoml) is the one-sided P112 predecessor; here P111 is re-derived on #589's lines.
+- **#968**, **#1077**, **#1180**, **#1212**, **#1213**, **#1236**, **#1744**, **#757**, **#761**, **#620**, **#1097**, **#1815**, **#1331** (Arham-Tahir64), **#1249** (bbMisk, independent check of #1236), **#717** (ours; term-cost model, frontier-word censuses): the E8 / P112 / P104 / P111 floors for 8 terms, for factors in the live root code, rigidity, and the 9-term decoder outside the root code (#1180, whose cost 65 and shape are re-derived in `c4`).
+- **#1224** (joaqcoo; the merge lemma, one-sided overcomplete structure), **#1633** (bbMisk; excess-rank budgets), **#1714** (the independent-call batch model), **#2294** (thakrarsagar; the `k = 2` / `O(9)` / Gram batching core, found independently of Theorem B and credited for priority), **#2293** (navinor; independent audit of our Lemma CR2 / Theorem B2), **#2176**, **#2206**, **#2232**, **#2240**, **#2247**, **#2137**, **#2272**, **#2267**, Discussion 1267 (philippeVV; co-star families), Discussion 1166 (1337isnot1337; child-merging screen).
+- **#589** (P111 bit word): `data/p111_lines.json` is the `lines` array of `research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz` on `main` (sha256 pinned in `SOURCES.json`).
+- Tools: kissat 4.0.4 (SAT; never CaDiCaL); `drat-trim` (Marijn Heule and Nathan Wetzler), not vendored here, optional.
+- No file is copied from another contributor. `lib/roots.py`, `lib/satgen.py`, `lib/frames.py`, `lib/report.py`, `scripts/provenance.py`, `checks/c5_attaining_decoders.py`, `data/p104_frames.json` and `LICENSE` are the author's own files from the package of #2277 (`research/overcomplete-and-realisation-floors`).
+
+## New in this package
+
+Everything under `research/decoder-floors-frontier-format/`: `README.md`, `verify.sh`, `SOURCES.json`, `MANIFEST.sha256`, `lib/*.py`, `checks/*.py`, `sat/*.py`, `scripts/provenance.py`, and the evidence files `data/*.json`, `sat/results.jsonl`, `sat/results_misc.jsonl`, `sat/proofs/` (all produced by the generators in this package; the P104 class representatives `data/p104reps.json` and `data/h4_F1.json` were exported from the author's working card `STRAYS`, and are re-verified by the checks: `c1.gauge`, `c2`).
diff --git a/research/decoder-floors-frontier-format/README.md b/research/decoder-floors-frontier-format/README.md
new file mode 100644
index 0000000000..83999445cb
--- /dev/null
+++ b/research/decoder-floors-frontier-format/README.md
@@ -0,0 +1,299 @@
+# Decoder floors are tight in the frontier format: one F2^9 label table, factors in col M of a rank-8 realisation (P112 64, E8 72, P104 (#968's unit) 56; two-call batches 128) — no κ claim
+
+> **Scope, stated first.** This package says one thing: *for decoders of the E8-family units that are hosted the way the frontier hosts them* — one global label
+> table in `F2^9` (so the admissible pairing `B` of the whole unit has `F2`-rank `≤ 9`), with the factors of every term in the column space of a minimal-rank realisation
+> (`col P ⊆ col M`, `col Q ⊆ row M`, rank `M = T = 8`; the square decoder of a *rank-9* realisation is **not** covered, OPEN §5.2 (c)), any number of terms, any number of independently batched calls — **the copy cost of the decoder cannot be lowered
+> below P112 64, E8 72, P104 56 (P104 means #968's unit, `F1 = H4`; E7 49 on its own rank-7 table), and two independent P112 calls cost at least 128**, all attained. It contains **no κ claim**, no window,
+> no supplier, no word-side (helper, transport, packing) cost. Everything outside that format is listed in §5 as **OPEN**, with what each escape would have to achieve.
+> Nothing here removes the need to price an escape; it only says where the escapes are. **Credit, stated first:** the P111 row of Theorem R (rigidity of the rank-9 fitting matrix of a P111 pattern) is prior work of #620 (GamingPuzzled; SAT) and #1097 (bitplane, merged; LRAT-checked in the general model), and #1815 (jmbarrancoml, merged) proves a one-sided P112 fitting rigidity; what is new here is Theorem R on E8, P112, P104 (#968's unit and class representatives), E7, E6, plus P111 on #589's 111 lines in the symmetric and general model with DRAT (§3.1, §3.7). Other P104 units are **not claimed** (§6, §5.6).
+>
+> **Update (overnight closures, Oct 15).** Four open items were narrowed by other working cards of the author; **nothing in rows 1–9 changed, and none of the new items is re-run by `verify.sh`** (they are RECORDED, with the card's own scope and status quoted): the bit window of 13–14 totals is CLOSED (§3.7, row 18), the `h = 10` Gram root code is RECORDED closed (688 term-query DRATs pending, 1 verified; §5.1, rows 16a/16), `p = 45` is closed for `m ≥ 8` (dense `B`, column-space factors; §5.4, rows 19a/19), and the frame-module theorem (PROVEN, proof in §3.3) is a new tool for §5.2, which stays OPEN.
+>
+> **Labels.** **PROVEN** (proof in this README, or a cited proof of a merged / open PR of the swarm); **CHECKED** (recomputed by `verify.sh`: exact integer / `Fraction` / bit
+> arithmetic, or SAT whose UNSAT verdict carries a DRAT proof that `drat-trim` verifies; kissat 4.0.4 only, never CaDiCaL); **RECORDED** (a result of the author's working
+> cards that this package does **not** re-run, stated with its exact scope and where the evidence is; nothing in §2 marked PROVEN or CHECKED depends on a RECORDED item
+> unless that is said); **OPEN**.
+
+## 0. Reading this package
+
+```sh
+bash research/decoder-floors-frontier-format/verify.sh /fresh/output/dir        # Python >= 3.11, standard library only
+DRAT_TRIM=/path/to/drat-trim KISSAT=/path/to/kissat bash research/decoder-floors-frontier-format/verify.sh /fresh/output/dir
+```
+
+Step 0 checks every file against `MANIFEST.sha256` and every pin of `SOURCES.json` (hard stop on a mismatch). Then seven check scripts print one `PASS` / `FAIL` line per
+assertion (`SKIP` for anything that needs `kissat` or `drat-trim` when it is absent: those lines are not PASS). `verify.sh` exits nonzero on any FAIL. One core;
+6-7 minutes of CPU with both tools (358 s and 417 s user in two runs on a loaded machine; the 30 rigidity instances are re-solved and the UNSAT proofs re-checked), about 20 s without them (4 SKIP lines).
+`HIT_FULL=1` additionally re-solves three slow clique-hitting instances (kissat only, no proof; §3.6).
+
+| script | what it recomputes |
+|---|---|
+| `checks/c1_rigidity.py` | Theorem R: regenerates 30 CNFs (hash, #vars, #clauses), recorded verdicts, 4 shipped DRAT proofs, and (with kissat) re-solves all 30; 16 UNSAT proofs re-checked with drat-trim, 14 SAT models decoded |
+| `checks/c2_support_propagation.py` | Lemma 1.1 census (all `2^h − 1` label classes) on D4, D6, E7, E8, P112, P104; survivors, pair ranks, exactness of the per-term rank |
+| `checks/c3_batch_premises.py` | labels of P112 in `F2^9`, normals `w_i`, `b(w_i,w_j) = 1`, `ρ(N(f_i),N(f_j)) = 8`, frame lemma, an `O(9)` chart with all 64 cross pairs of rank 7 |
+| `checks/c4_masked_costar.py` | #1180's nine-term identity (cost 65), co-star dead sets, survivor 7-cliques |
+| `checks/c5_attaining_decoders.py` | the decoders that attain the floors (E8 72, E7 49, D6 30, D4 12, P112 64, P104 56), exact `Fraction` arithmetic |
+| `checks/c6_block_minrank_punctures.py` | EDGE E1a (every admissible `B`: the block `N(f)` of P112 has minrank 8; 8 DRAT proofs) and the C4.1 clique-hitting bounds on punctures |
+| `checks/c7_p111_unit.py` | the P111 bit unit of #589's word: 111 lines of an E8 line system, `rank_F2 B_d = 9`, an 8-frame |
+
+Layout: `lib/` (E8-family units, Bron–Kerbosch, exact `F2` / `Q` linear algebra, CNF helpers; `roots.py`, `satgen.py`, `frames.py`, `report.py` are the author's own files from
+#2277's package, `units.py`, `supprop.py`, `solve.py` are new), `sat/` (generators `rigid.py`, `misc.py`, `hitting.py`; registries; recorded results
+`results.jsonl`, `results_misc.jsonl`; shipped DRAT proofs `proofs/*.drat.xz`; author tools `mkresults.py`, `mkmisc.py`), `data/` (frames, the 111 P111 lines, one chart).
+
+## 1. Setting
+
+A **unit** is a set of `v` pairwise non-proportional lines `r_t ∈ Q^8` of the E8 root system (`E8`: 120 lines, `P112 = E8 − F0`, `P104 := E8 − F0 − F1` with `F1 = H4`, the second frame of #968's unit (the swarm has other P104 units, e.g. #1399's 896 admissible ones; those are not covered here, §6 and §5.6; the 1,260 frames `F1` disjoint from `F0` fall into invariant classes by the number of live 8-frames of the unit, `759 / 767 / 801`, and `H4` lies in the 759 class), `E7`, `E6`, the bit unit `P111` of #589). A **realisation** `M` has `M_tt ≠ 0` and `M_ts = 0` for orthogonal `t ≠ s`. A **decoder** is `M = Σ_j p_j q_jᵀ`
+with an **admissible (fitting) pairing** `B ∈ F2^{v×v}`: `B_tt = 1`, `B_ts = 0` for non-orthogonal `t ≠ s`, free on orthogonal pairs. Cost `= Σ_j rank_F2 B[R_j, A_j]`, `R_j = supp p_j`,
+`A_j = supp q_j` (the copy-pairing rank sum that the invoice charges; every bound below therefore also holds for any costlier physical charge). The **dense** pairing is
+`B_d = 1` on every orthogonal pair (and the diagonal); `rank_F2 B_d = h = 9` for E8, P112, P104, P111, `7` for E7, E6.
+**Model hypothesis (the frontier format).** The registers of the word carry labels in one `F2^h`; the pairing used by every term is a block of one matrix `B = U Vᵀ`
+(or `P Pᵀ`, the physical symmetric form) with `U, V ∈ F2^{v×h}`, i.e. `rank B ≤ h`. That the frontier word hosts its decoders on a single table of dimension `h = 9` is an
+engineering fact of the word; the code that fixes it is in this repository: `research/complex-571-cold14-k492/code/construct_k_triangle.py:20` (`P=D['binary_ports'] … h=9`), `:183–187` (the centre frames are `hyper(P[frame[i]])`, so the physical pairing is `J + Gram(even parts)`, symmetric of rank `≤ 9`) and `:364` (`'ports':P[8:]`); the working card `EDGE/HOSTING.md` (not shipped) records the same reading, with the term-cost model of #717 (cost = dimension of the label span). It is **not** proved here, it is the hypothesis whose negation is §5 item 1.
+**Label classes** (as in #2277 §1): `C = col B_d` (dim `h`); a class is the support of a nonzero `w ∈ C`; `Def(R) = {w ∈ C : supp w ∩ R = ∅}`, `δ(R) = dim Def(R)`.
+**Frames.** A `T`-frame is `T` pairwise orthogonal lines (`T = 8` for E8, P112, P104, P111; 7 for E7). Every realisation has rank `≥ T` (a frame gives an invertible diagonal minor).
+
+## 2. Master table: escape class → status → certificate
+
+"Class X" = one label table with `h = 9` (`h = 7` for E7), factors in `col M / row M` of a rank-`T` realisation.
+
+| # | escape class | what is shown | status | certificate |
+|---|---|---|---|---|
+| 1 | non-dense admissible `B` of rank `≤ 9` (E8, P112, P104 = #968's unit and three class representatives, P111) or `≤ 7` (E7, E6) | every fitting `B` of that rank **equals the dense `B`**, general `UVᵀ` and symmetric `PPᵀ` | **CHECKED** (16 DRAT-verified UNSAT + 10 SAT controls + 4 non-dense witnesses) | `c1`, §3.1 (Theorem R); the P111 case is #620 / #1097's, re-derived on #589's lines |
+| 2 | factors in the E8 root code, any `m`, dense `B` | P112 ≥ 64, E8 ≥ 72, P104 (#968's) ≥ 56, E7 ≥ 49 | **PROVEN** (cited, not re-run: #2228 Thm 4; #1180) + attained (**CHECKED**, `c5`) | #2228, #1180; with row 1 this is every `B` at `h = 9` |
+| 3 | any rank-8 realisation, factors in `col M`, any `m` | **P112 ≥ 64**; P104 (#968's unit) ≥ 56; E8 ≥ 72, E7 ≥ 49 | **PROVEN** from **CHECKED** (Lemma 1.1 census) | §3.2 (Theorem P), `c2`; E8/E7/P104 also #2277 Cor. 5.3 |
+| 4 | ≤ 8 paid terms, factors anywhere | square ⇒ row 3 | **PROVEN** | §3.3 |
+| 5 | #1180's outside-code nine-term example | costs exactly 65; its shape is ≥ 64 for **every** `B` | **CHECKED** + **PROVEN** | `c4`, `c6`, §3.3 |
+| 6 | co-star nine-term masked decoders (Disc. 1267) | all 120 dead sets span in every rank-8 realisation ⇒ each is a square decoder of a rank-9 realisation (pins them to §5 item 2(c)) | **CHECKED** (`c4`) + **PROVEN** consequence | §3.3 |
+| 7 | batches: `k` independent P112 calls on one `F2^9` table, any chart, factors in `col M_c`, any `m` | `k = 2`: ≥ 128 + 3t; `k ≥ 3` (symmetric charts): ≥ 64k + 3t; attained | **PROVEN** from **CHECKED** premises | §3.4 (Thm B, Bk), `c3`; k = 2 / O(9) / Gram also swarm #2294 |
+| 8 | any `B` on a single coordinate block | `rank_F2 B[N(f), N(f)] ≥ 8` for every admissible `B`, all 8 `f` | **CHECKED** (8 DRAT) | `c6`, §3.5 (EDGE E1a) |
+| 9 | punctures of the coordinate term under any table | clique hitting: `f(2) ≥ 14`, `f(6) ≥ 46`, `f(7) ≥ 52`, `f(8) = 56`; `s/f(s) ≤ 1/7` on the computed values | **CHECKED** (s = 2, 6: DRAT; 7, 8 exact); s = 3, 4, 5 **RECORDED** (kissat UNSAT re-run with `HIT_FULL=1`, no DRAT here) | `c6`, §3.5 |
+| 10 | P111 bit unit | rigid at `h = 9` (sym + general; **prior work of #620 / #1097**, re-derived on #589's lines); word-priced set-decoders with ≤ 14 totals cost ≥ 63 | rigidity **CHECKED** (2 DRAT); ≥ 63 for ≤ 12, 13 and 14 totals **RECORDED** (card: n ≤ 13 PROVEN, n = 14 CHECKED, 735 DRAT-verified) | `c1`, `c7`, §3.7 |
+| 11 | E8 square root-code decoders for **every** `B` (no `h` cap) | ≥ 72 (4022 pair classes) | **RECORDED** (4022 DRAT verified in the working card; not re-run) | §3.8 |
+| 12 | `FL(4)`: every D4 decoder, every `B`, every `m` | ≥ 12 | **RECORDED** (support-level enumeration, 144 classes) | §3.8 |
+| 13 | E7 square maximal-normal root-code decoders, every `B` | ≥ 49 (no ≥ 5 root–root partners) | **RECORDED** (exact enumeration + independent audit in the working card) | §3.8 |
+| 14 | P104 delivery (#968's decoder) under any `F2^9` table | no helper-free nested delivery (24 DRAT) | **RECORDED** | §3.8 |
+| 15 | PUNCT2 near-miss unions `p = 25..44`, any physical table, any `m` | no decoder beats P102's 54/102 (Model C) | **RECORDED** | §3.8 |
+| 16a | `h = 10` label tables, **root code (Gram realisation)**, any `m`, any fitting `B` of rank ≤ 10 | every term ≥ 8, so P112 ≥ 64 (a rank-10 table saves nothing; break-even needed ≤ 59) | **RECORDED** (card: CHECKED; 46/46 `G`-query DRATs verified, 688 term-query UNSAT with DRAT **pending**) | §3.8, §5.1 |
+| 16 | **label tables of rank `h ≥ 10`, the rest**: non-Gram realisations at `h ≥ 10`; `h = 11` at the orthogonal dead-root term `N(f) × N(g)`; `h ≥ 12` | non-dense fitting tables exist (row 1, witnesses); `h = 11` needs cost ≤ 55 to tie; `h ≥ 12` not attempted | **OPEN** | §5.1 |
+| 17 | **factors outside `col M`, `m ≥ 9`** | `m = 9`: `ρ ∈ {8, 9}`; (b) `ρ = 8` one outside factor, (c) `ρ = 9` square rank-9, (d) `m ≥ 10`; tool: the frame-module theorem (PROVEN, §3.3) | **OPEN** (cases (b), (c), `m ≥ 10`; no instance decided) | §5.2 |
+| 18 | **bit windows of 13–14 totals** (n ≥ 15 is excluded by hosting, a note) | word-priced P111 set-decoders ≤ 14 totals ≥ 63; P110 ≤ 12 totals ≥ 63 | **CLOSED, RECORDED** (card: n ≤ 13 PROVEN, n = 14 CHECKED) | §3.7, §5.3 |
+| 19a | punctures `p = 45`, `m ≥ 8` terms (Model C, dense `B`, column-space factors) | cost ≥ 40 > 39.71 (Theorem 45) | **RECORDED** (card: PROVEN from CHECKED data; floating-point MILP re-certified exactly) | §3.8, §5.4 |
+| 19 | **puncture windows `p ≥ 46`**, and `p = 45` with `m ≤ 7` | — | **OPEN** | §5.4 |
+| 20 | **batches `m ≥ 17` outside `col M`**, GL charts with `k ≥ 3`, mixed units, correlated demands, `h ≥ 10` joint tables | — | **OPEN** | §5.5 |
+| 22 | projected / asymmetric copy for P110 (cost 62) | SPEC-legal (a checker convention forbids it, not the SPEC), but on PR589's tuned chains the best term costs ≥ 3.57% c net | **RECORDED** pricing (not a theorem) | §3.7 |
+| 21 | **P104 units other than #968's** (Theorem R for all 1,260 frames `F1`; the Lemma 1.1 census for them) and **rank-9 square decoders** | — | **OPEN** | §5.6, §5.2 (c) |
+
+Rows 11–15 are *beyond* what the headline needs: at `h = 9` row 1 already forces `B = B_d`, so the headline uses `B_d` only. Their role is to show that the dense-pairing
+statements are not hiding a cheap non-dense escape *inside* the `h = 9` class; row 1 does that, and rows 11–13 give the independent every-`B` statements for the
+(square, root-code) sub-class.
+
+## 3. Results
+
+### 3.1 Theorem R: the minimal-rank label table is unique (CHECKED, DRAT)
+
+**Theorem R.** Let `U ∈ {E8, P112, P104, P111}` (P104 as defined in §1, plus the class representatives below) and let `B ∈ F2^{v×v}` fit `U` with `rank_F2 B ≤ 9`. Then `B = B_d`. The same holds for `E7, E6` with `rank B ≤ 7`. (**Credit:** for P111 this is #620's and #1097's result; see the paragraph after the table.)
+It holds in the general model `B = U Vᵀ` and in the symmetric model `B = P Pᵀ` (the physical one: `B_d = J + C` with `C` the alternating Gram of the even-weight label parts,
+which is `PPᵀ` for odd-weight labels `P_t = 1 + e_t`). For P104 the statement is checked for `H4`'s `F1` (the frame of #968; its unit has 759 live 8-frames, so it lies in the 759 class) and one representative of each of the three invariant
+classes (`759 / 767 / 801` live 8-frames) of frames disjoint from `F0`: **three classes, four instances** (`H4` is in the 759 class). **These classes are not proven to be single orbits**, and the backfill over all 1,260 frames was not finished,
+so P104 is claimed only for #968's unit (`F1 = H4`); Theorem P's census was run on `H4` only, and Theorem R / Theorem P for every other P104 unit is **not claimed** (§6, OPEN §5.6).
+
+*Encoding (`sat/rigid.py`).* `B = U Vᵀ` with `U, V ∈ F2^{v×h}`; constraints `⟨U_t, V_t⟩ = 1`, `⟨U_t, V_s⟩ = 0` for every non-orthogonal ordered pair `t ≠ s`; mode `alt` adds the clause
+"some orthogonal ordered pair (unordered in the symmetric model) has `B_ts = 0`"; mode `ctl` omits it. Products and parities are Tseitin variables with constant folding.
+*Gauge (PROVEN).* Let `S` be a pairwise non-orthogonal `k`-clique (`k = 8` for E8, P112, P104, P111; 7 for E7; 5 for E6; pinned in `results.jsonl`, `c1.gauge` checks the clique).
+Then `B[S,S] = I_k`, so `U[S]` has rank `k`; `GL(h)` acts by `U ↦ U g`, `V ↦ V g^{-T}`, preserves `B` and is transitive on rank-`k` `k`-tuples, so `U[S] = (e_1..e_k)` w.l.o.g. In the
+symmetric model with `k = 8`, `h = 9`: `P[S]` is orthonormal, `W = span P[S]` is nondegenerate, `W^⊥ = ⟨w⟩` with `w·w = 1` (`det I_9 = det I_8 · w·w`), so an isometry in `O(9)` maps
+`P[S]` to `(e_1..e_8)`; this needs `k ≥ h − 1`, which `registry()` asserts for every symmetric UNSAT instance. (For SAT instances the gauge is only a restriction, so a SAT verdict stands.)
+Rank `≤ h` is equivalent to a factorisation with `h` columns, so UNSAT of `alt` says every fitting `B` of rank `≤ h` is dense. (The general model contains the symmetric one as a sub-model, so general-model UNSAT already implies the symmetric statement and, for E7 and E6 where only the general model is run, covers the physical table; the symmetric runs are redundant but consistent.)
+
+| group (`results.jsonl`) | instances | verdict | check |
+|---|---|---|---|
+| `alt`, minimal rank | P112, E8, P104 (H4, 759, 767, 801), P111, each sym + gen (14 instances); E7, E6 gen at `h = 7` (2) | **UNSAT**, every proof verified by drat-trim (binary DRAT, kissat 4.0.4) | `c1.status`, `c1.resolve`; four proofs shipped (`proofs/`, sym P112 / E8 / P104-H4 / P111) |
+| `ctl`, no extra clause | P112, E8, P104-H4, P111 (sym + gen), E7, E6 | **SAT**; every decoded model is a fitting matrix with 0 non-dense orthogonal entries (model is `B_d`) | `c1.ctl` |
+| negative controls | `SUB20`, `SUB40` (the gauge clique plus the first 20 / 40 other lines of P112, `h = 9`, gen); P112 at `h = 10` (sym 59 of 3304, gen 89 of 6608 orthogonal pairs with `B_ts = 0`) | **SAT**: a non-dense fitting `B` exists | `c1.neg` |
+
+(The encoding is the one of the author's working card `STRAYS/rigid2.py`; the clique choice here is deterministic and pinned, so the CNFs differ from the card's files, with the
+same verdicts. The `h = 10` row shows the instance family does detect non-rigidity; the `SUB` rows show the same at `h = 9` on sub-units.)
+
+**Prior work on P111 and one-sided P112 rigidity (credit; this changes the novelty of Theorem R).** #620 (GamingPuzzled, open) found by SAT, without proof logs, that the rank-9 fitting matrix of its archived P111 pattern is unique; #1097 (bitplane, merged 2026-10-13) proof-checked this with LRAT: "fitting rank ≤ 9, unequal to `B0`" is UNSAT in the general (asymmetric) model with an 8-port gauge. That is the P111 row of Theorem R, and it is **theirs**. *Which set?* #1097's object is the archived sorted Hamming-root order of #620 with indices `39, 52, 57, 71, 76, 78, 103, 109, 114` deleted (`encoding.py:9`); #589's 111 lines (`data/p111_lines.json`) are a different 111-subset of the same 120 Hamming-coordinate lines: 104 lines in common (up to sign), 7 on each side only (a one-off comparison against #1097's retained `e8units.hamming_e8`, not part of `verify.sh`; whether the two sets are `W(E8)`-equivalent was not checked). So Theorem R here **re-derives** the P111 statement on #589's puncture, in both the general and the symmetric model, with DRAT, and does not rely on #1097. #1815 (jmbarrancoml, merged 2026-10-14) is the one-sided predecessor for P112: with the two column spaces fixed, unit diagonals and the required zeros force `N = RRᵀ` and `B = UUᵀ`; Theorem R removes the column-space hypothesis on `B` (every fitting `B` of rank `≤ 9` is dense). What is new here is Theorem R on E8, P112, P104 (#968's unit and representatives), E7 and E6.
+
+**Corollary R1 (PROVEN from Theorem R and the theorems of §3.2 / rows 2).** In the frontier format (one `F2^9` table, `F2^7` for E7), every term pairs through the dense `B_d`. Hence
+every statement made below for the dense pairing holds for every hosted decoder, and *the overcomplete "any `B`" slack* (orthogonal-normal blocks of fitting minrank 5–6;
+orthogonal E8 root–root terms of rank 6) *does not exist at `h = 9`*: it needs a non-dense `B`, hence `h ≥ 10`.
+**Corollary R2 (two-call tables, PROVEN).** If a two-call batch uses one `F2^9` and each call's block fits P112, the labels are `(P, PΦ)` with `Φ ∈ O(9, F2)` (general model:
+`(U, V), (UΦ, VΦ^{-T})`, `Φ ∈ GL(9)`). *Proof.* By Theorem R both blocks equal `B_d`, of rank 9. `P_1P_1ᵀ = P_2P_2ᵀ` has rank 9, so `P_1, P_2` have the same column space and `P_2 = P_1Φ`;
+then `P_1(ΦΦᵀ − I)P_1ᵀ = 0` with `P_1` of full column rank gives `ΦΦᵀ = I`. ∎
+
+### 3.2 Theorem P: P112 ≥ 64 in every rank-8 realisation (PROVEN from CHECKED)
+
+Setting (#2277 §5). `K` is any field (the swarm uses `Q` / `C`; Lemma 1.1 and Theorem P are field-independent). Let `M` be a realisation of rank exactly `T = 8` (the minimum), `M = P₀ N Q₀ᵀ`, `P₀, Q₀ ∈ K^{v×8}` bases of `col M`, `col Mᵀ`, `N ∈ GL_8`; `π(t)` is row `t` of `P₀`.
+Consider decoders with `p_j = P₀x_j`, `q_j = Q₀y_j` (every square decoder `m = 8` is of this form; for `m > 8` this is the hypothesis `col P ⊆ col M`). Then `N = Σ_j x_j y_jᵀ`, so at least 8 terms
+are nonzero.
+
+**Lemma 3.1 (support-only bound; #2277 Lemma 5.1, restated).** For `R, A ⊆ [v]`, `rank_F2 B_d[R, A]` depends only on the subspaces `Def(R), Def(A) ⊆ C`, and `≥ h − δ(R) − δ(A)`.
+*Proof.* Take `B_d = X Yᵀ`, `X = Y ∈ F2^{v×h}` of full column rank (`B_d` symmetric), `col X = C`. `ker X_R ≅ Def(R)` via `w = Xz`, so `rank X_R = h − δ(R)`, and the row space of `X_R` is
+the annihilator of `ker X_R`, i.e. determined by `Def(R)`; likewise for `A`. Sylvester gives the bound. ∎
+**Lemma 3.2 (Theorem 4′; #2277 §5, restated).** `cost ≥ Σ_{j : x_j, y_j ≠ 0} (h − δ(R(x_j)) − δ(A(y_j)))`, with `R(x) = {t : π(t)·x ≠ 0}`. If `w ∈ Def(R(x))` then `π(supp w) ⊆ x^⊥`: the class
+`supp w` is *deficient* (its `π`-image lies in a hyperplane). *Proof.* Lemma 3.1 and the count of nonzero terms. ∎
+
+**Lemma 1.1 (support propagation; working card `IDEAL3` §1.1, PROVEN here).** Let `E` be an 8-frame and write a functional `h*` that kills `π(O)` as `h* = Σ_{e ∈ E} c_e σ(e)`, where `σ(e) = N κ(e)ᵀ`, `κ(e)` = row `e` of `Q₀`
+(`π(e)·σ(e′) = M_{ee′}`: for a frame `E` the `σ(e)` are the dual basis of `{π(e)}` up to the nonzero scalars `M_ee`, and `σ(e)` depends on the line only). (i) `c_e = 0` for `e ∈ E ∩ O`: `h*(π(e)) = c_e M_ee`. (ii) For every 8-frame `F`: `supp_E(c) ⊆ (E ∖ O) ∩ ⋃_{g ∈ F∖O} N̄(g)`,
+`N̄(x) = {x} ∪ {lines non-orthogonal to x}`. *Proof.* (i) is the displayed identity. For (ii), applying (i) to `F` gives `h* ∈ span σ(F∖O)`; expanding `σ(g)` in the dual basis of `E`,
+`σ(g) = Σ_e (M_eg/M_ee) σ(e)`, whose `E`-support lies in `{e : M_eg ≠ 0} ⊆ N̄(g) ∩ E` (`M_eg = 0` for orthogonal `e ≠ g`). ∎
+*Corollary.* If iterating (ii) over all frames ends with some `S_E = ∅`, the class `O` is non-deficient in **every** rank-8 realisation.
+
+**Census (CHECKED, `c2`).** For every one of the `2^h − 1` classes: D4 (3 frames), D6 (15), E7 (135), E8 (2025): **all** certified. P112 (1260 frames): **exactly 8 classes uncertified** (the
+8 sets of 56 live lines orthogonal to one removed root; each has `rank_Q = 7`, i.e. is Gram-deficient, so the certificate is sharp); P104 (`H4`'s unit, 759 frames; the census was run on this unit only): 16 uncertified (sets of 52), also
+exactly the Gram-deficient ones. In both units the uncertified classes contain **no 2-dimensional subspace** (`a ⊕ b` is never one). For each uncertified `O`, the classes with support inside `O` are
+`{O}` alone (`c2.def`), so `Def(V∖O) = ⟨w_O⟩` and the single-deficiency rank is `rank B_d[V∖O, V] = 8`; over all ordered pairs of P112 survivors `rank B_d[V∖O, V∖O′] = 8` (64 of 64), and
+for P104 the values are `8` (192) and `7` (64).
+
+**Theorem P (PROVEN from the CHECKED census).** For P112, every rank-8 realisation `M`, every decoder with `col P ⊆ col M`, `col Q ⊆ row M` (all square decoders, any `m` otherwise), dense `B`:
+**cost ≥ 64**, attained by the removed-frame coordinate decoder (`c5`). For P104 = #968's unit (`F1 = H4`; the census of Lemma 1.1 is run on this unit only): **cost ≥ 56**, attained (`c5`).
+*Proof.* A nonzero `w ∈ Def(R(x_j))` is a deficient class (Lemma 3.2), hence one of the 8 (16) survivors (Corollary of Lemma 1.1; the census). Survivors contain no 2-dimensional subspace, so
+`δ(R(x_j)), δ(A(y_j)) ≤ 1`, and by Lemma 3.1 and the census the term's rank is `9` (no deficiency), `8` (one) or, for both deficient, the pair rank: `8` in P112, `≥ 7` in P104. So every nonzero
+term costs `≥ 8` (P112), `≥ 7` (P104); at least 8 terms are nonzero. ∎
+For E8 (72) and E7 (49) no class is deficient (census), so every term costs `h`; with at least `T` terms the floors are `8·9 = 72`, `7·7 = 49`. (#2277 Cor. 5.3 gives all of E8 72, E7 49, D6 30, D4 12, P104 56
+via the weaker clause-(c) certificate; its P112 value was 56, and "P112 ≥ 64 for every realisation" was listed there as open — Theorem P closes it.) **Sharpness (CHECKED, `c5`):**
+frame decoders with `M = Gram` cost 72 (E8), 49 (E7), 30 (D6), 12 (D4); the removed-frame decoder of P112 costs 64; the eight frame-pair terms of #968 cost 56 on P104.
+
+### 3.3 Few terms, outside `col M`, #1180 and the co-star (PROVEN / CHECKED)
+
+*(working card `STRAYS-MASK` §1–§3; dense `B`, which at `h = 9` is every `B` by Theorem R)*
+**1.1 Free-term absorption.** A term with `B[R_j, A_j] = 0` contributes `0` to the cost and nothing on the diagonal or on orthogonal pairs, so the paid part `N = Σ_{paid} p_j q_jᵀ` is again a realisation
+of the same pattern with the same cost; w.l.o.g. every term is paid.
+**1.2 Merge lemma (#1224 Lemma D, both sides).** If `q_i = c q_k` then `p_i q_iᵀ + p_k q_kᵀ = (c p_i + p_k) q_kᵀ`; the new row support lies in `R_i ∪ R_k`, and
+`rank B[R_i ∪ R_k, A_k] ≤ rank B[R_i, A_k] + rank B[R_k, A_k]` (`A_i = A_k`). The merge does not raise the cost for **any** `B`. W.l.o.g. no two row normals and no two column normals are proportional.
+**1.3 `m ≤ 8`.** `rank N ≥ α_⊥ = 8`, so `m ≥ 8`; `m = 8 = rank N` is the square case with factors in `col N / row N` (every factor lies in the column space of a rank-8 matrix with 8 terms), so Theorem P
+gives `≥ 64` (P112), `≥ 56` (P104, #968's unit), **whatever the factors, the realisation or the masking**. This covers every component of #1213, not only the connected one.
+**1.4 `m = 9` trichotomy.** `a = rank P = ρ + s`, `b = rank Q = ρ + t`; Sylvester: `ρ ≥ a + b − 9`, so `s + t ≤ 9 − ρ` with `ρ = rank N ∈ {8, 9}`. (a) `ρ = 8`, `s = t = 0`: Theorem P; (b) `ρ = 8`, `s + t = 1`: §5.2 (b) (#1180 / #1224's residual class); (c) `ρ = 9`: square in a rank-9 realisation (OPEN, §5.2 (c)).
+**#1180's example (CHECKED, `c4`).** Its nine-term identity `D Tᵀ = 8·Gram` holds on all `112 × 112` entries (`ex1180`-form: `t_1 = R_0 + z`, outside terms `(t_1, R_0)` and `(−z, R_0)`) and its term ranks under `B_d`
+are `[8]×8 + [1]`, **total 65**. Its two outside-`col M` terms share the column vector `R_0`: by the merge lemma (any `B`) the example costs at least the removed-frame decoder, whose terms are the blocks `B[N(f), N(f)]`,
+each of fitting minrank 8 for every `B` (`c6`, §3.5), so **after merging the two outside terms it is the removed-frame decoder, which costs ≥ 64 for every admissible `B` by E1a**: the "outside `col M`" in #1180's example is only a split of a proportional pair.
+**Co-star (CHECKED, `c4`; PROVEN consequence over any field of characteristic 0, the scope of the working card `STRAYS-MASK` Theorem 3.2).** *Definitions.* The **dead set** of a term `p qᵀ` on the row side is `{t : p_t = 0}` (the lines the term does not touch), on the column side `{t : q_t = 0}`; a set of lines is **spanning** if its images `π(t)` span `K^8` in every rank-8 realisation. For each of the 120 root lines `α`, the dead set `V ∖ S_α` (`S_α` = live lines orthogonal to `α`, plus `α` if live; `|S_α| = 60` for the 112 live `α`, 56 for the 8 removed) is certified spanning in every
+rank-8 realisation (Lemma 1.1). *Lemma (inside dead sets; STRAYS-MASK Lemma 3.1).* If a term of a rank-8 realisation has its column factor in `row M` (`q = Q₀ȳ`, `ȳ ≠ 0`, an "inside" side), its dead set `{t : κ(t)·ȳ = 0}` has images in the hyperplane `ȳ^⊥`, so it is not spanning and cannot contain `V ∖ S_α` (rows by transposition: the pattern is symmetric). *Consequence.* Let a nine-term masked co-star decoder (philippeVV, Discussion 1267; every term's supports inside co-stars, arbitrary coefficients, zeros, any `k`) have `ρ` = the rank of the full nine-term sum. If a term is free, or two row or two column normals are proportional, the paid or merged part has `≤ 8` terms, hence is square, and Theorem P gives `≥ 64` outright. Otherwise `ρ = 8` would give `s + t ≤ 1` (§1.4), so one side, say `t = 0`, is inside for all nine terms, contradicting the Lemma; `ρ ≥ 10 > m` is impossible. So `ρ = 9` and the decoder is a square
+biorthogonal decoder of a **rank-9** realisation: cases (a), (b) of §1.4 are empty for co-stars. This pins the open `k = 7/8/9` families to §5.2 (c); it does not close them. Every survivor class contains an
+orthogonal 7-clique and no 8-clique (`c4.survclique`), so its killing functional is unique up to scale in every rank-8 realisation.
+
+**Frame-module theorem (nine terms, any realisation, any rank, factors anywhere; PROVEN; working card `STRAYS-MASK2` §2, proof reproduced here).** Let `M = Σ_{j≤9} p_j q_jᵀ` be a nine-term decoder of a unit with an 8-frame `F` (so `M_ff ≠ 0`, `M_ff′ = 0`), `p(t), q(t) ∈ K^9` the rows of the factor matrices, `P_F, Q_F ∈ K^{8×9}` the rows `p(f), q(f)`, `f ∈ F`. Then `P_F Q_Fᵀ = D_F = diag(M_ff)` is invertible, so `rank P_F = rank Q_F = 8`, with one-dimensional kernels `ν` (`P_F ν = 0`) and `π` (`Q_F π = 0`). *(i)* `J := Q_Fᵀ D_F⁻¹ P_F` satisfies `J² = J`, `rank J = 8`, so `J = I − u wᵀ`, `wᵀu = 1`, and `P_F(I − J) = 0`, `(I − J)Q_Fᵀ = 0` force `u ∝ ν`, `w ∝ π`: **`π·ν ≠ 0`** and `J = I − νπᵀ/(π·ν)`. *(ii)* `π ∉ span p(F)` (if `π = Σ β_g p(g)`, then `0 = q(g)·π = β_g M_gg` for every `g ∈ F`, so `π = 0`), so every line has **`p(e) = Σ_{f∈F} (M_ef/M_ff) p(f) + λ_e π`**, and likewise **`q(s) = Σ_f (M_fs/M_ff) q(f) + μ_s ν`** (pair with `q(g)`, resp. `p(g)`). *(iii)* Substituting, `M_es = Σ_f M_ef M_fs / M_ff + (π·ν) λ_e μ_s`: the Schur defect of the frame is **rank one**, with `λ_e ∝ p(e)·ν`, `μ_s ∝ π·q(s)`. When `rank P = 8` (`λ ≡ 0`) this is Lemma 1.1; in rank 9 it is the value-level rank-9 Lemma 1.1 asked for in §5.2 (c), as a support calculus. *Status of its use:* the theorem is PROVEN; the SAT model built from it (case (b), co-star family, full `m = 9`) is RECORDED as sound on three positive controls but **no instance was decided** (timeouts at 25–28 min under load), and a class-level rank-9 pair test (restricted Lemma 1.1) leaves a 136-clique of mutually compatible dead classes, so pair data alone cannot close (c). For `m ≥ 10` the kernel becomes `(m − 8)`-dimensional and the three sharp rules (reverse expansion, Schur support, K-zero) are lost. Cases (b), (c), `m ≥ 10` remain OPEN (§5.2).
+
+### 3.4 Batching: independent calls on one `F2^9` table (PROVEN from CHECKED)
+
+*(working card `STRAYS-BATCH`; the model is #1714's: `k` independent P112 calls, `C = I_k`, cross-call blocks of the requested matrix are 0.)* The requested matrix is `M_1 ⊕ … ⊕ M_k`, `M_c = P_cQ_cᵀ` a rank-8
+realisation (Gram: `P_c = Q_c = X`). A decoder is `Σ_j d_j t_jᵀ = M` with `d_j = (P_ca_j^{(c)})_c`, `t_j = (Q_cc_j^{(c)})_c`; exactness is `A Cᵀ = I_{8k}`. One label table on all `112k` lines; each call's block fits P112,
+so by Theorem R it is dense and by Corollary R2 call `c` carries labels `PΦ_c`. The charge of term `j` is `rank_F2` of the pairing between the span of the output labels of its union support `S_j` and the span of the input
+labels of `T_j` (the cheapest charge, #1714; every costlier charge is covered). **Premises (CHECKED, `c3`; they are Lemma 1.1's sharpness in label language):**
+(P1) in any rank-8 realisation the support of `P_c x`, `x ≠ 0`, has label span `V` (dim 9) or one of 8 hyperplanes `H_i = w_i^⊥` (it avoids the deficient class `O_i`, the live lines orthogonal to `f_i`); the survivors contain no 2-dimensional
+subspace, so no support avoids two classes and every span has dim ≥ 8. (P2) `b(w_i, w_j) = 1` for all 64 ordered pairs, and `ρ(N(f_i), N(f_j)) = 8` for all 64 pairs, `i = j` included.
+**Theorem B (`k = 2`, PROVEN).** For every chart `Φ` (`O(9)` symmetric or `GL(9)` general) every decoder satisfies `Σ_j cost_j ≥ 128 + 3t`, `t = #{j : cost_j = 7}`; the minimum is 128 (two coordinate decoders), only at `t = 0`.
+*Step 1.* Union spans have dim ≥ 8 (P1), so cost `≥ 8 + 8 − 9 = 7`; at cost 7 both spans are hyperplanes. *Step 2 (rank-7 terms are pure cross-call).* If `a_j` has a nonzero part in call `c`, that part's span (dim ≥ 8) lies in the output span `H`
+of dim 8, hence equals it, so `H` is a call-`c` output hyperplane; likewise `H′` is the input hyperplane of every call where `c_j` is nonzero. If one call had both parts nonzero, `(H, H′)` would be an output / input hyperplane pair of
+that call, which pairs at rank 8 by (P2). So `calls(a_j) ∩ calls(c_j) = ∅`. *Step 3 (rank count).* With `N = Σ_{cost 7} a_jc_jᵀ = [[0, N₁₂],[N₂₁, 0]]`, `t₁₂ + t₂₁ = t`, `rank N₁₂ ≤ t₁₂`, `rank N₂₁ ≤ t₂₁`; the other active terms
+cost ≥ 8 and sum to `I₁₆ − N`, so there are at least `rank(I − N) = 8 + rank(I₈ − N₂₁N₁₂) = 16 − d` of them, `d = dim ker(I₈ − N₂₁N₁₂) ≤ min(t₁₂, t₂₁) ≤ t/2`. So `Σ cost ≥ 7t + 8(16 − d) ≥ 128 + 7t − 8min(t₁₂,t₂₁) ≥ 128 + 3t`. ∎
+**The counting floor 120 is not the truth** (`c3.chart.rank7`): there is a chart `Φ ∈ O(9, F2)` (shipped in `data/chart_rank7.json`) for which all 64 cross pairs (call-1 support `N(f_i)`, call-2 support `N(f_k)`) pair at rank 7, while within a call the same pairings have rank 8.
+Per-term counting alone gives 120; the extra 8 units come from the rank argument.
+**Theorem Bk (`k ≥ 3`, symmetric model, PROVEN).** Charts `Φ_c ∈ O(9, F2)`, any rank-8 realisations, any `m`: `Σ cost ≥ 64k + 3t`. *Proof.* Steps 1–2 verbatim. Every hyperplane is `n^⊥` for a unique normal; slot `(c,i)` has normal `Φ_cw_i`, and
+`b(n, n) = 1` by (P2). Partition the `8k` slots into classes by normal (at most one slot per call). A rank-7 term has `b(n, n′) = 0`, so `n ≠ n′`; `a_j` is supported in the class of `n`, `c_j` in the class of `n′`. For `x ∈ Z^P_{c,i}`, `y ∈ Z^Q_{c,i′}` (`Z^P_{c,i}` := the coefficient vectors `x` whose call-`c` output support `supp P_c x` avoids `O_i`, i.e. lies in the hyperplane slot `(c,i)` with normal `Φ_c w_i`; `Z^Q_{c,i′}` := the same on the input side, `supp Q_c y` avoiding `O_{i′}`),
+`i ≠ i′`: `yᵀx = Σ_{e ∈ E}(y·q_c(e))(p_c(e)·x)/M_ee` over any 8-frame `E` of live lines; a summand needs `e ∈ N(f_i) ∩ N(f_{i′})`, and `c3.framelemma` finds for every `i < i′` a frame with `E ∩ N(f_i) ∩ N(f_{i′}) = ∅`, so `yᵀx = 0`. Hence
+`K = CᵀA` over the rank-7 terms has `K_ij ≠ 0` only if `class(c_i) = class(a_j)`, `K_ii = 0`. *Lemma K:* `corank(I_{8k} − ACᵀ) = corank(I_t − K) ≤ t/2` (order the classes; the larger of `{j : α(j) < β(j)}`, `{j : α(j) > β(j)}` has size `≥ t/2`, along `K`-arcs inside it the class strictly
+moves, so `K[S,S]` is nilpotent up to a permutation and `I − K[S,S]` is invertible). So `Σ cost ≥ 7t + 8(8k − t/2) = 64k + 3t`. ∎ (Every batch with exactly `8k` terms needs no factor hypothesis, #1714 §5.)
+**Credit.** #2294 (thakrarsagar) proves the `k = 2`, `O(9)`, Gram-root-code core first (its Theorem A: `≥ 128 + 6μ + 7(r_01 + r_10 − 2μ)`, `μ = min(r_01, r_10)`) and independently finds that some isometric charts make all 64 exceptional pairs rank 7; the derivation above was done
+before #2294 was read and is the same inequality. Beyond #2294: `GL(9)` charts of the general factor model, any rank-8 realisation (the Theorem P setting), and `k ≥ 3` in the symmetric model.
+
+### 3.5 One coordinate block under any `B`; punctures (CHECKED)
+
+**EDGE E1a (`c6`, 8 DRAT).** For each removed root `f` (all 8), `N(f)` is the 56-line support of the coordinate term. *Every* admissible `B` has `rank_F2 B[N(f), N(f)] ≥ 8`: the instance "`rank ≤ 7`" (gauge: the largest non-orthogonal
+clique in `N(f)`, 7 lines) is UNSAT with a drat-trim-verified proof (8 proofs of about 70 kB each; one shipped), and "`rank ≤ 8`" is SAT (the dense block). So no choice of `B` lowers a coordinate term of the removed-frame decoder, and with
+`m ≥ 8` the removed-frame decoder costs `≥ 64` for every `B`. (Together with the merge lemma this is the "shape ≥ 64 for every `B`" of §3.3.) `ω_non(N(f)) = 7` and `α_⊥(N(f)) = 4` are recomputed in `c6`.
+**Punctures (NEWWORD C4.1).** A puncture `D ⊆ N(f)` (lines deleted from the support) that brings `rank B[R∖D, R∖D]` to `≤ 8 − s` for some admissible `B` must hit every `(9 − s)`-clique of pairwise non-orthogonal lines (a clique `C` has `B[C,C] = I`
+for every admissible `B`). `f(s)` := the least size of such a hitting set. Proven bounds: `f(2) ≥ 14` (the 576 7-cliques cannot be hit by 13 lines; DRAT), `f(6) ≥ 46` (the largest triangle-free kept set has 10 lines: 11 is UNSAT, DRAT; the working card
+had 15 and `≥ 42`), `f(7) ≥ 52` (`α_⊥(N(f)) = 4`, exact), `f(8) = 56`. Recorded (kissat UNSAT, working-card DRAT; `HIT_FULL=1` re-solves them here without a proof): `f(3) ≥ 23`, `f(4) ≥ 32`, `f(5) ≥ 38` (the card's `s = 1` value, `z ≥ 8`, is EDGE's separate
+`killgauge` SAT result and is not reproduced here). The ratios `s/f(s)` are `.1429, .130, .125, .132, .130, .135, .143` (`s = 2..8`; `c6.f` prints the proven ones): **no computed `s ∈ {2..8}` exceeds 1/7** (`s = 3–5` RECORDED, `s = 1` not computed here). The puncture-saving statement
+("punctured coordinate decoders tie P112 at best under any global label table") is therefore the clique-hitting bound plus the card's price model (break-even `s/f(s) > .1441`, margin under 1%, inside the price model's error): the **bound** is CHECKED, the
+**pricing consequence** is RECORDED and is not claimed as a theorem.
+
+### 3.6 Slow instances
+
+`HIT_FULL=1` re-solves `hit_k6_z22`, `hit_k5_z31`, `hit_k4_z37` (the `s = 3, 4, 5` bounds) with kissat only; recorded (kissat 4.0.4, UNSAT, no proof; wall time under machine load): `hit_k6_z22` 102 s, `hit_k5_z31` 227 s, `hit_k4_z37` 9 s, i.e. `f(3) ≥ 23`, `f(4) ≥ 32`, `f(5) ≥ 38`; their results are in `sat/results_misc.jsonl` (flagged `slow`) and re-derived by `HIT_FULL=1`. No DRAT is checked for these here (the proofs are 100–200 MB).
+
+### 3.7 The bit side: P111 (rigidity CHECKED, prior work of #620 / #1097; "≥ 63" for ≤ 14 totals RECORDED)
+
+**P111 is rigid at `h = 9` (CHECKED, `c1`, `c7`; prior work: #620 by SAT, #1097 LRAT-checked in the general model, see §3.1).** On #589's set, which is not #1097's (§3.1), the statement is re-derived here in two models. The 111 live lines of #589's word (`data/p111_lines.json`; the source file's sha256 is pinned in `SOURCES.json` and equals the entry of `research/e8-bit-p111-tuned/MANIFEST.sha256` on `main`) are a sub-configuration of an E8 line system
+(`c7`); `alt` is UNSAT in the symmetric and the general model (drat-trim verified; the symmetric proof is shipped), the controls are SAT with the dense `B`. So at `h = 9` the bit side is also a dense-`B` question.
+**RECORDED (not reproduced here): P111 set-decoders with at most 12 retained totals cost ≥ 63.** The working card `STRAYS-BIT` proves it premise-free from the full census of the E8 line matroid's flats (ranks 1–6: `120 / 4,900 / 85,680 / 661,542 / 2,091,600 / 2,221,780`, maximal line counts `1, 3, 6, 12, 20, 36`;
+the rank-6 flats with ≥ 24 lines are exactly the 4,900 sets `a^⊥ ∩ b^⊥`), `G ≥ 12` (no live code word is covered by rank-≤ 6 sets of total rank ≤ 11, exhaustive) and an induction `D(Λ) ≥ r_k + D(Λ ∩ a_k^⊥)`. That enumeration needs 378 s with numpy and was **not ported to the standard library**; this package
+does not verify it and no other statement here uses it. It extends #757 / #761 (63 optimal on the shipped P111 for 9, 10 and 11+ label terms) and agrees with #620 (63 for P111; exact SAT, cost ≤ 62 UNSAT, 8 totals UNSAT; also #1097's rank-9 uniqueness above).
+**RECORDED (the author's working card `STRAYS-BIT`, §0; not re-run and not reviewed here): word-priced P111 set-decoders with at most 14 totals cost ≥ 63.** The card's headline, quoted with its own labels: "in the word's own pricing (the set-decoder model: retained totals are arbitrary live-line sets, each priced by `rank_Q` of its span), no bit decoder on P111 with ≤ 14 retained totals costs below 63. That covers every total count the hosting wall allows (`R ≤ 4v` ⇒ `n ≤ 14`)." Its statuses:
+* `n ≤ 13`: **PROVEN** in the card (exhaustive enumerations plus exact rational Farkas certificates, re-checked there with `Fraction`s only; for `n = 13`, all 132 code classes of excess 4), on top of the exhaustive `G ≥ 12`, `G(3) ≥ 15`, `G(4) ≥ 14` (no ≤ 4-set low cover of total rank ≤ 13, no 3-set low cover of total rank ≤ 14).
+* `n = 14`: **CHECKED** in the card. Of 51,973 code classes (excess 5), 51,238 have exact Farkas certificates; the 735 integer-only classes are kissat UNSAT with drat-trim **VERIFIED**; the last 3 of those need the extra exhaustive lemma `B16low`.
+* The card's premise (P) is a theorem there and is **no longer used** (its facts are now exhaustive computations); `P110` (P111 minus line 38, the unique dual-root line of the shipped readers) satisfies Lemma A and `G ≥ 12`, and with `D(1) = 7` (the card's Lemma 1, `p = 10 ≤ 25`) every `P110` decoder with ≤ 12 totals costs ≥ 63, which is `P110`'s whole hosting window (`R = 439 ≤ 4·110`); rigidity at `h = 9` on **both P111 and P110** is drat-trim VERIFIED in the card (controls SAT). The package itself ships and re-checks the P111 rigidity only (credit for P111 rigidity: #620, #1097, as above; the `P110` rigidity is the card's).
+The set-decoder enumeration needs numpy (378 s for the census) and was **not ported to the standard library**, so this package neither verifies nor depends on it. It extends #757 / #761 (63 optimal on the shipped P111 for 9, 10 and 11+ label terms) and agrees with #620 (63 for P111; exact SAT). **So the bit windows of 13 and 14 totals are CLOSED (RECORDED from the card)**; `n ≥ 15` totals are excluded by hosting in the current word (`R ≤ 4v`), a note rather than a result. Not covered: decoders outside the set-decoder model (a retained total charged below its source span's rank, i.e. a projected or asymmetric copy), other units, and the helper mass that extra totals would add (unpriced; no word was built).
+**RECORDED pricing, not a theorem: the projected-copy route to `P110 = 62`** (working cards `SPECCHECK`, `BITCUT`). The SPEC does not forbid a projected copy (the bit SPEC has no COPY primitive: only per-vertex rational frames, edge cost `rank(M_head − M_tail)` and a common frame at each gate); what forbids it in the shipped word is the checker's COPY rule (COPY rank equals the dimension of the source frame, temp at frame 0), a format convention, so breaking it would need the four-part bar for convention-breaking changes. If built, the copy charge of the one orthogonal term drops 7 → 6 (cost 62, +2.80% c) minus the deleted port (−2.13%), before any reader-chain cost. Replaying PR589's tuned chains (`BITCUT`): all 111 targets sit at frame 0 at the scatter cut, and for the best candidate (term 5, one line) only a handful of the 55–63 readers already contain the line `⟨a⟩`, so the others pay extra climbs / descents: the exact repricing is **−3.57% c net including the +2.80% unit gain** (about −5.7% after the port), every other (term, line) pair is far worse, and the ideal bound (every reader already contains `⟨a⟩`) would be only +0.27% c. Caveats of the card: join frames are not in the 636-frame catalogue, the chains were not re-tuned, the identity of the orthogonal term was not pinned (so the best over all lines is quoted). So the SPEC-legal projected copy costs at least 3.57% c on PR589's tuned chains, and `P110 = 62` is not a supplier; nothing here is a κ claim.
+
+### 3.8 Recorded results of the working cards (not re-run)
+
+* **E8□ (IDEAL3 §4.6).** Every square E8 root-code decoder costs `≥ 72` for **every** `B` (4,022 non-orthogonal pair classes, each with fitting minrank `≥ 9`); the card's `census/e8drat.out` ends "DONE 4022 classes; not verified: 0". The proof logs (139 MB) are not shipped. Not needed at `h = 9`.
+* **FL(4) (IDEAL3 §2).** The Frame Lemma for `n ≤ 4` (PROVEN modulo a 144-class support-level enumeration) gives `D4 ≥ 12` for every decoder, every realisation, every `m`, every `B`. Lemmas 4.1 (maximal-pair reduction) and 4.2 (`k`-term averaging) of IDEAL3 §4 are the shared-`B` reductions used by E8□ and the E7 statement below.
+* **E7 (STRAYS S4).** Square maximal-normal root-code decoders cost `≥ 49` for every `B`: no decoder has ≥ 5 root–root partners (256 bad partners, 16 compatible 5-sets, 0 six-sets, 0 completions; Sonnet enumeration, independently re-audited). The 49 *on E7's own rank-7 table*, the case in the headline, needs only Theorem R at `h = 7` (CHECKED) and #2277 Cor. 5.3.
+* **P104 delivery (NEWWORD C4.2).** For #968's P104 frame-pair decoder (cost 56, rank-7 terms) no global admissible label table in `F2^9`, with any per-term gather orientation, allows helper-free nested delivery (24 DRAT-verified instances; pairs `(0,1), (0,4), (1,4)`, same orientation, both directions; the graph of class-1 pairs is triangle-free and 3-regular on the 8 terms, so among any three mutually adjacent terms two share an orientation). Extends EDGE-B's Delivery Lemma from the dense table to every table. Escape: `h > 9` (a P104 at `h = 10` already loses to P112 at `h = 9` on the format ceiling: `3.931e-3 < 3.995e-3`).
+* **PUNCT2, `p = 25..44` (NEWWORD c5).** Model C (dense pairing, column-space factors): at the 1,323 near-miss unions the bilinear forms vanishing on orthogonal live pairs have nullity 1 (`N ∝ Gram`), so every 8-term decoder is biorthogonal; for `m ≥ 9` merging and PUNCT2's deficiency census (`d ≤ 2`) give cost `≥ 5m ≥ 45 > 40.24` (`p = 44`) and `≥ 7m − 12 ≥ 51 > 44.47` (`p = 36`); rigidity at the two representatives is DRAT-verified and the 1,323 unions form two `W(E8)` orbits. So no decoder in the class beats P102's 54/102; the "+13–15%" near-miss points were relaxation artefacts. Depends on PUNCT2's census inputs, which are not shipped.
+* **E7 frame decoders (NEWWORD c3).** No E7 root-line decoder with `m = 8` and every cross `⟨y_i, x_j⟩ = ±1`; best type mixes cost `≥ 39` on `≤ 50` ports (`x ≥ .78`), none beats P56's `x = .75` even with per-term-optimal `B` and free delivery (scope: crosses in `{0, ±1}`, root-line normals).
+* **EDGE (coordinate block, minrank 8 every `B`):** CHECKED in §3.5. EDGE-B's Delivery Lemma (dense table) is the one C4.2 extends; not re-run.
+* **STRAYS-H10, `h = 10` root code (Oct 15; RECORDED, card status CHECKED; char 0).** Root code (Gram realisation, factors `p_j = D₁R x_j`, `q_j = D₂R y_j`), any `m`, any fitting `B = UVᵀ` of `F2`-rank ≤ 10: **every nonzero term has `rank B[R(x), A(y)] ≥ 8`, so P112 ≥ 64.** Ingredients (card): the exact rank formula `rank B[R,A] = rank V[A] − dim(rowspan V[A] ∩ ker U[R])` and Sylvester's `≥ r − d(R) − e(A)` (PROVEN), reduction to maximal sections (47 orbits of the P112 orthogonality graph under an order-172,032 group; PROVEN), the second gauge `V[S] = (I|0)` (PROVEN), `G(10,2,·)` UNSAT on 46 of 47 orbits (**46/46 DRAT verified**), and exact term queries on the remaining orbit `f^⊥` against all 172 pair orbits and splits: **688/688 UNSAT, their DRAT proofs are queued and not yet verified**. An audit of the logic and encodings by a Sonnet helper found no error. Scope: Gram realisation only; **non-Gram rank-8 realisations with factors in `col M` at `h ≥ 10` are OPEN** (the realisation-free certificate leaves 17 uncertified classes on a rank-10 table, so Theorem P's method does not transfer). `h = 11` (a floor of ≥ 56 would close it; break-even cost is ≤ 55): `G(11,3,·)` is UNSAT on all 46 orbits other than `f^⊥`, so every term is ≥ 7 unless one normal's maximal section is `f^⊥`; the remaining blocker is the orthogonal dead-root term `N(f) × N(g)`, `f ⊥ g` (one split timed out at 25 min; other pair orbits UNSAT so far; runs continue). `h ≥ 12` not attempted. P104 at `h = 10` was already dead by the format ceiling. Not in `verify.sh`.
+* **PUNCT4 / PUNCT5, `p = 45` (Oct 15; RECORDED).** Setting: Model C (`K = L ∖ S`, `|S| = p`, dense `B`, column-space factors, cost `Σ r_j`, exact law `r = 9 − s`, `s = d_x + dim(Z_y ∩ Z_x^⊥)`), bar = largest winning cost `c_p = ⌈(54/102)(120 − p)⌉ − 1` (`c_45 = 39`). **Theorem 45 (card: PROVEN from CHECKED data): `p = 45` is closed for decoders with `m ≥ 8` terms (after merging): cost ≥ 40 > 39.71.** Shape: a win needs a root normal with deficiency `d ≥ 3` (every other term saves ≤ 4, cost ≥ 5m ≥ 40); case `d = 4` (the 1,260 minimal kernels form one stabiliser class; `relaxF = 50`, nullity of the `N`-space 1, so `rank N = 8`); case `d = 3` (11 anchor classes, at most 3 other sides with `d ≥ 2` in every class, counting `cost ≥ 7m − 16 ≥ 40`). The exact-data inputs were re-certified by exact integer search in PUNCT5 (side counts 1,3,0,2,0,3,2,0,1,0,1 identical; `relaxF = 50` by an exact min-cost flow on five kernels), replacing a floating-point HiGHS MILP. **Lemma G (PROVEN):** if `s` is a live line whose orthogonal live lines span `s^⊥`, every `N` in the `N`-space has `N r_s = λ_s r_s`, `λ_s = M_ss/|r_s|² ≠ 0`; if the good lines span `Q^8`, then `rank N = 8` and every decoder has `m ≥ 8` terms. Honest limits (as stated in the cards): the nullity-1 / `rank N = 8` fact is CHECKED for `d = 4` but **not** for the `d = 3`-anchored `S = A + E`, so **`m ≤ 7` is OPEN wherever the `N`-space nullity exceeds 1**; for decoders with `m ≥ 8` terms (after merging) at `46 ≤ p ≤ 56`, a win needs a `d ≥ 3` root (PROVEN reduction) but the residue (R2) `m = 8` with a `Q`-root at `p ≥ 46` and (R3) `m ≥ 9` at `p = 46` and wherever the count-relaxed census exceeds its allowance (`p ≥ 50` not computed) is **OPEN**; where `m ≥ 9` is treated as closed at `p = 47–49` this rests on the floating-point HiGHS Q-census, which PUNCT5 §1 says was not re-certified, and is not covered by Theorem 45's exact data; PUNCT5's `p = 46` anchor runs (13 `d ≥ 3` anchor classes, bracket within the allowance on those logged) are partial (the `d ≥ 4` extensions and the `E7`-type rank-deficiency CNFs timed out or were unfinished). Any-`B` is untouched at `p ≥ 45`. Not in `verify.sh`.
+
+## 4. How to cite this
+
+"For every decoder hosted on one `F2^9` label table (Theorem R: the pairing is the dense one), with factors in the column space of a rank-8 realisation and any number of terms (Theorem P; #2228 Thm 4 for the root code), the copy costs of the E8-family units are exactly
+P112 64, E8 72, P104 56 (#968's unit, `F1 = H4`; E7 49 on rank-7 tables), and `k` independent P112 calls cost `≥ 64k` (`= 128` for `k = 2`; symmetric / physical table for `k ≥ 3`, `GL` charts with `k ≥ 3` are open, §5.5) (Theorem B, Bk; #2294). Remaining escapes: tables of rank `≥ 10`, rank-9 square decoders and overcomplete factors outside `col M` with `≥ 9` terms, non-Gram realisations at `h ≥ 10` and `h ≥ 11` (the `h = 10` Gram root code is RECORDED closed; 688 term-query DRATs pending, 1 verified, rows 16a/16), puncture windows `p ≥ 46` (and `p = 45` with `m ≤ 7`; `p = 45`, `m ≥ 8` is RECORDED closed), batches of `≥ 17` terms outside `col M`, other P104 units. The bit window of 13–14 totals is RECORDED closed (word-priced P111 set-decoders cost `≥ 63`)."
+
+## 5. OPEN (each leaves class X; priced where a price exists; none constructed)
+
+<a id="open-1"></a>
+### 5.1 Label tables of rank `h ≥ 10` (the `h = 10` Gram root code is RECORDED closed; the rest is OPEN)
+
+Non-dense fitting tables exist at rank 10 (`c1.neg`: `P112_sym_h10_alt`, `P112_gen_h10_alt` are SAT). *Price* (working card `STRAYS/PRICE-P112-H10.md`, a Sonnet helper's pricing, not a theorem; it reproduces the P104 rows of NEWWORD `c4/PRICE-H10.md`): a 112-port unit at
+`h = 10` must reach **cost ≤ 59 (−5 units)** to tie P112-at-`h = 9`, before any helper growth; at `h = 11`, `≤ 55`. **Status: undecided.** Per-term floors under a global rank-10 cap were probed on the first orthogonal-normal class (free-`B` minrank 6) and timed out at 20 minutes for cap 7 at both `h = 10` and `h = 12`. Per-term `≥ 8` at rank `≤ 10` would close `h = 10` (since `m ≥ 8`).
+For E8 overcomplete under any `B`: non-orthogonal terms `≥ 9`, other orthogonal terms `≥ 8`, orthogonal root–root terms are 6; counting alone allows `m ∈ {9, 10, 11}` below 72; the `m = 9` root-normal family is jointly `≥ 65` (EDGE). **Update (working card `STRAYS-H10`, §3.8; RECORDED, not re-run):** for the root code (Gram realisation) any `m` and any fitting `B` of rank ≤ 10, every term costs ≥ 8, so P112 ≥ 64 (CHECKED in the card: 46/46 `G`-query DRATs verified; 688 term-query instances UNSAT, **their DRATs pending**). **Still OPEN:** (i) non-Gram rank-8 realisations with factors in `col M` at `h ≥ 10`; (ii) `h = 11`: per-term ≥ 7 except possibly at pair orbit 0 (`N(f) × N(g)`, `f ⊥ g`; one split timed out) and at pair orbits not yet run (1, 2, 65–171); runs continue, not decided; (iii) `h ≥ 12`, not attempted (the price would have to be ≤ ~51); (iv) joint-table and non-root-code statements at `h ≥ 10`.
+
+<a id="open-2"></a>
+### 5.2 Factors outside `col M`, `m ≥ 9`
+
+Proven (§3.3): `m ≤ 8` ⇒ `≥ 64` / 56 for any factors and any realisation; `m = 9`: `ρ = rank(paid part) ∈ {8, 9}`, `s + t ≤ 9 − ρ`. **Open:** (b) `ρ = 8` with one factor outside `col M` (#1180's residual class; necessary conditions proven, 42k of 45k class pairs uncertified at support level);
+(c) `ρ = 9`, square in a rank-9 realisation (needs a rank-9 analogue of Lemma 1.1, `Σδ ≥ 18` to reach ≤ 63; contains every philippeVV co-star `k = 7/8/9` family, §3.3); (d) `m ≥ 10` (budget `s + t ≤ m − ρ`, #1633; the average term rank would have to drop below 6.4). All under dense `B`, which at `h = 9` is every `B`. (working card `STRAYS-MASK`.) **Update (working card `STRAYS-MASK2`; no case closed, nothing beats 64):** the **frame-module theorem** (PROVEN, §3.3) is the realisation-free rank-9 support calculus for every nine-term decoder; a SAT model built on it is sound on three positive controls (#1180; the coordinate decoder plus `c e_t e_tᵀ` for two lines `t`) but the decisive instances (case (b) with `π` global, the co-star family, full `m = 9`) **timed out at 25–28 min under machine load**; nothing is proved; longer runs are queued, not finished. So **(b), (c) and `m ≥ 10` remain OPEN.** Swarm results on one explicit rank-9 family (not the general case (c)): **#2321** (nine-term sharp COPY cost of the fixed P112 two-column completion, ports `(0,1)`), **#2385** (the same floor for every nonzero coefficient, nine terms) and **#2398** (the same optimum 64 for any finite number of terms with both factors in that completion's minimal nine-dimensional column and row spaces; the factor-space restriction is essential there). They settle that one rank-9 realisation; the question of an arbitrary rank-9 square decoder is §5.2 (c).
+
+<a id="open-3"></a>
+### 5.3 Bit windows of 13–14 totals (CLOSED, RECORDED from the working card); `n ≥ 15`: a note
+
+**CLOSED, RECORDED (§3.7):** word-priced P111 set-decoders with at most 14 retained totals cost ≥ 63 (card: `n ≤ 13` PROVEN by exact Farkas certificates, `n = 14` CHECKED with 735 integer-only classes DRAT-verified; P110 ≤ 12 totals ≥ 63, its whole hosting window). Not re-run here. **Note (not a result):** `n ≥ 15` totals (excess ≥ 6) are excluded by hosting in the current word (`R ≤ 4v`, hosting-forbidden); decoders outside the set-decoder model (projected copy) are priced, not excluded, in §3.7 (≥ 3.57% c net on PR589's tuned chains); extra totals add unpriced helper mass.
+
+<a id="open-4"></a>
+### 5.4 Puncture windows `p ≥ 46` (`p = 45`, `m ≥ 8` is RECORDED closed)
+
+PUNCT2's exclusion covers `p = 25..44` (RECORDED, §3.8). **Update (working cards `PUNCT4`, `PUNCT5`; RECORDED, §3.8):** Theorem 45 closes `p = 45` for decoders with `m ≥ 8` terms (cost ≥ 40 > 39.71; dense `B`, column-space factors; exact data), and Lemma G (PROVEN) gives `rank N = 8` (so `m ≥ 8`) whenever the good lines span `Q^8`. **Remaining residue, as stated in the cards, OPEN:** (R1) `m ≤ 7` where the `N`-space nullity exceeds 1 (including `p = 45` with a `d = 3`-anchored `S = A + E`); (R2) `m = 8` with a `d ≥ 3` root at `46 ≤ p ≤ 56`; (R3) `m ≥ 9` at `p = 46` and at the `p` where the count-relaxed census exceeds its allowance (`p ≥ 50` not computed; the `p = 47–49` rows rest on an uncertified floating-point HiGHS Q-census, PUNCT5 §1, not on Theorem 45's exact data); `57 ≤ p ≤ 112` and any-`B` are untouched. The `T²` law (#2125, argued) predicts no gain for `v ≲ 64`.
+
+<a id="open-5"></a>
+### 5.5 Batches outside class X
+
+`m ≥ 17` terms with factors outside `col M` (every 16-term batch needs no factor hypothesis, #1714 §5); `GL(9)` charts with `k ≥ 3` (mathematical only: the physical table is symmetric; the obstruction is a possible loop in the component quotient of the output / input hyperplane graph, so
+Lemma K's ordering argument may fail; the bound needs only `corank(I_t − K) ≤ 7t/8`); `h ≥ 10` joint tables (pure cross terms may cost `< 7`; #2294 Props B–D cover cross blocks that factor through the call labels as bilinear forms; **#2395** states a stronger two-call P112 COPY floor for arbitrary cross forms, addressing #2294's open arbitrary-cross-form question (its rank-only test certifies 93 of 100 ordered rank pairs; 7 low-rank pairs undecided), and **#2342** (theon199) states a three-call P112 COPY of 192 by a sharp block count, to be compared with our Theorem Bk (`k = 3`, symmetric model, `≥ 192`, any rank-8 realisations, any `m`): both are cited from their PR statements, **not re-derived, compared in scope or audited here**, and neither is used by anything in this package); correlated demands (`C ≠ I`, #1714 §4); mixed-unit batches; a second call on a different unit.
+
+<a id="open-6"></a>
+### 5.6 Other P104 units; rank-9 square decoders
+
+Theorem R and the Lemma 1.1 census (Theorem P) are run for P104 = #968's unit (`F1 = H4`) only, with Theorem R also at one representative of each of the classes `759 / 767 / 801`. **Not claimed:** Theorem R for all 1,260 frames `F1`, the census and Theorem P for any other P104 unit (the swarm has many, e.g. #1399's 896 admissible ones). The rank-9 square case is §5.2 (c).
+
+**Out of scope by construction:** non-E8 units (BIGTHEORY: no-go only for `h ≤ 13`; #2222-type large-`h` units are compensation-bound), and all word-side overheads (helpers, transport, packing). 1337isnot1337's rank-16 child-merging screen (Discussion 1166, `< 0.21%` even at zero overhead) is a word-side route, not a decoder saving.
+
+## 6. What was not reproduced
+
+See §3.5 (steps `s = 3, 4, 5` of the puncture table; `s = 1` not computed), §3.7 (the ≤ 14-total bit bounds and the projected-copy pricing) and §3.8 (including the `h = 10` root code, the frame-module SAT runs and Theorem 45): every RECORDED item is a result of the working cards that this package neither re-runs nor depends on for rows 1–10 of §2, with the single exception noted in §3.5 (the pricing
+consequence of the puncture table). Differences between the working cards and this package, none of them a failed reproduction: the SAT instances are regenerated with a deterministic gauge clique (the card's files differ, the verdicts agree); `f(6)` is `≥ 46` here (card: `≥ 42` from a looser 15-set instance); the `h = 10` witnesses differ from the card's
+(non-dense in 59 / 89 orthogonal entries rather than 171 / 381); the card's "rank(B − B_dense) = 8" for the `h = 10` witness is not claimed. Not claimed: Theorem R for all 1260 frames of P104 (class representatives only), and Theorem P or any P104 statement for units other than #968's (`F1 = H4`); the rank-9 square case (§5.2 (c)); novelty of the P111 row of Theorem R (#620 / #1097).
+
+## 7. Credits and related PRs
+
+Our PRs: #1590 (model, merged), #2111, #2125, #2162 (Lemma CR2 / Theorem B2; navinor's independent audit #2293 passes our CR2/B2 on 58 instances; the later edge-form counterexamples #2334 / #2340 and D2331 concern an edge-count reading of B2(iii), not the vertex form (MAS = maximum (vertex-count) acyclic subset of lines) that this package cites, and are credited, not used), #2228 (root-code floors Thm 4, dense polar law), #2244, #2277 (Theorem 4′, frame-intersection certificate, Cor. 5.3), #2265 (audited by thakrarsagar #2311: 0 FALSE / 0 MISSING-PROOF on its supplier premises). Swarm: #968 (frame-pair P104 decoder), #1180 (outside-code nine-term example), #1212 / #1213 / #1236 (rank-8 rigidity, components, root-star supports), #1744 (global fitting rank ≥ 9 on P112), #757 / #761 (P111 63), #620 (GamingPuzzled; P111 rank-9 uniqueness and 63, found by SAT) and #1097 (bitplane, merged; LRAT proof of that uniqueness in the general model, on the archived Hamming order, not on #589's set), #1815 (jmbarrancoml, merged; one-sided P112 fitting rigidity), #1331 (Arham-Tahir64, merged; the coordinate COPY 64 is not improved by one free rectangle; related to E1a and the punctures), #1249 (bbMisk, merged; independent verification of #1236's 64), #717 (ours; term cost = dimension of the label span, frontier-word censuses and decoder floors; the hosting model rests on it), #2176 / #2206 (forced minors, exact pairing costs),
+#2232 / #2240 / #2247 / #2137 (E6 screens, 1337isnot1337), #2272 (dense-polar small-`T` screen), #2267 (rectangular Lean form of the shadow lemma), #2294 (k = 2 batching, thakrarsagar), #2395 (two-call COPY floor for arbitrary cross forms), #2342 (theon199; three-call P112 COPY 192), #2321 / #2385 / #2398 (the fixed rank-9 P112 completion; §5.2), #1714 (batch model), #1224 (joaqcoo; the merge lemma and one-sided overcomplete structure), #1633 (bbMisk; excess-rank budgets), Discussion 1267 (philippeVV; co-star families).
+Tools: kissat 4.0.4, drat-trim (Marijn Heule, Nathan Wetzler). See `NOTICE.md`.
+
+Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0.
diff --git a/research/decoder-floors-frontier-format/SOURCES.json b/research/decoder-floors-frontier-format/SOURCES.json
new file mode 100644
index 0000000000..6d9441a011
--- /dev/null
+++ b/research/decoder-floors-frontier-format/SOURCES.json
@@ -0,0 +1,146 @@
+{
+ "description": "Pins for research/decoder-floors-frontier-format. files = library, generator and check code (own work); evidence = data exported from the author's working cards (data/h4_F1.json, data/p104reps.json: frames of P104 from cards/STRAYS; data/p104_frames.json from #2277's package; data/p111_lines.json: the 111 live lines of #589's P111 word; data/chart_rank7.json: an O(9) chart found by sat-free search with random.Random(52) and re-verified by checks/c3), the recorded SAT / DRAT results of sat/results.jsonl and sat/results_misc.jsonl (produced by sat/mkresults.py and sat/mkmisc.py with kissat 4.0.4 and drat-trim), and the shipped binary DRAT proofs (xz). Tools used (not vendored): kissat 4.0.4; drat-trim. scripts/provenance.py checks the pins and MANIFEST.sha256.",
+ "external": [
+  {
+   "what": "source of data/p111_lines.json",
+   "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz (CrocSwap/integer-mult-bounds, origin/main at 0fdd7d82)",
+   "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f"
+  }
+ ],
+ "files": [
+  {
+   "file": "checks/c1_rigidity.py",
+   "sha256": "4041cfeb1bc5131b5b57cce79de13e013061566128db38707cdc50efc3333e6a"
+  },
+  {
+   "file": "checks/c2_support_propagation.py",
+   "sha256": "a24a7f0907970257cdcfeaf3d1d234c34974b64a3d7aa584283124d79e0def7a"
+  },
+  {
+   "file": "checks/c3_batch_premises.py",
+   "sha256": "aa3c56bd79a36dd081b40e50c675064c4dc7e780aee02779813c618651cf0ad8"
+  },
+  {
+   "file": "checks/c4_masked_costar.py",
+   "sha256": "f06d5cc4685e81f5c1b52391a6a4f7548d9da146f0891aabdab09843c260ae11"
+  },
+  {
+   "file": "checks/c5_attaining_decoders.py",
+   "sha256": "359b20c67b8d4c0491a0a3b9cf5b595f5294570e6a7a98fbe900094396620790"
+  },
+  {
+   "file": "checks/c6_block_minrank_punctures.py",
+   "sha256": "42e91b63e455ddf020b678700ed45dc3ad3703374ba9d063002fffe13770b981"
+  },
+  {
+   "file": "checks/c7_p111_unit.py",
+   "sha256": "6d3e3bac50ef7054acaeaabecbc863e8f40c359655c61fc9483257184c25d6ae"
+  },
+  {
+   "file": "lib/frames.py",
+   "sha256": "b5e9f53dbdf15cb7667fd1e7d6db92f61fc773822746e895a56c2d21b6fa4612"
+  },
+  {
+   "file": "lib/report.py",
+   "sha256": "fc4bb6836cb34d310ca7b3275ef15ef2d5d03e511063ddb06d0eb60e7072a640"
+  },
+  {
+   "file": "lib/roots.py",
+   "sha256": "b2bdaa63376ab0c718b256e879d669f1465f4d3407b64ecc876ca0f3e6a32acd"
+  },
+  {
+   "file": "lib/satgen.py",
+   "sha256": "567df3a6f3277179f88cf17dffbe69dd40b1f6d8277baab3cb79e7332361077f"
+  },
+  {
+   "file": "lib/solve.py",
+   "sha256": "6872520ef5955082ab10e6f20960bb47cabfad03bdad246ebe79231007b36159"
+  },
+  {
+   "file": "lib/supprop.py",
+   "sha256": "a0883df40db120adc892aadec78ab15e6eefa7d8e7006883294ba1da62961081"
+  },
+  {
+   "file": "lib/units.py",
+   "sha256": "43eed628ea4c39f5aa47945697ccfe4dc63bbfc21d91affdd8a7d698c8ccd569"
+  },
+  {
+   "file": "sat/hitting.py",
+   "sha256": "8a4e7baaca75530be75d2483df1af4cbba48013c992129da5628bb2510ae0b82"
+  },
+  {
+   "file": "sat/misc.py",
+   "sha256": "5b72bcdf42c37cedb9cd4f60c61ac5fe884dbf2d78bf8e36939afe1c27f69358"
+  },
+  {
+   "file": "sat/mkmisc.py",
+   "sha256": "c748368f64c87d2842babb47f6ede23f8f16acf98bef8a48f5dd40259f3e2be1"
+  },
+  {
+   "file": "sat/mkresults.py",
+   "sha256": "3334ae7bd440971a6c751e8286a755cf632f0c3a325c1a27086bf6df5c0990df"
+  },
+  {
+   "file": "sat/rigid.py",
+   "sha256": "378f20d152d1c4c53c9bd528bd2e661fa75b68bbeaa1fecaa498af4acda9b0f9"
+  },
+  {
+   "file": "scripts/provenance.py",
+   "sha256": "a4cd33cef93721cd79ae3dfaf69556f8502b22152e363fcab33b1fa402d68d11"
+  }
+ ],
+ "evidence": [
+  {
+   "file": "data/chart_rank7.json",
+   "sha256": "66d019f311fd436c7e04517349d8d3e47d75d970951a7c99e1ef523cffd405b6"
+  },
+  {
+   "file": "data/h4_F1.json",
+   "sha256": "33e368cad0c95cd4af1c1d06d3a7abbd28abd14900bcada084d7b7583d89a270"
+  },
+  {
+   "file": "data/p104_frames.json",
+   "sha256": "52e1a2b0e963311eb74c1ec2bbb110497da57b606e132f784f9000603d10a306"
+  },
+  {
+   "file": "data/p104reps.json",
+   "sha256": "f85ac3b3c785964c04d53bcf879a74425d8d997ec3ccb92d971cce69c9c10a32"
+  },
+  {
+   "file": "data/p111_lines.json",
+   "sha256": "2b492989fd574f557533e237267bc6693d6917ce5b32e2ccdad7fa9de81a07f9"
+  },
+  {
+   "file": "sat/results.jsonl",
+   "sha256": "d7115712b22dca41e37813ac1236a91c198210b089651f0ec5cced78f6bdf296"
+  },
+  {
+   "file": "sat/results_misc.jsonl",
+   "sha256": "30889985d57b5bf1139ea29d9f52f9f5c24365c036b1acc8e263878fef8f94b7"
+  },
+  {
+   "file": "sat/proofs/E8_sym_h9_alt.drat.xz",
+   "sha256": "6d7b82565559777597a10dd65d34088ef03b65cd6789c55be59765b3ae30f89a"
+  },
+  {
+   "file": "sat/proofs/P104H4_sym_h9_alt.drat.xz",
+   "sha256": "fc385861ff98a07cf9f6267d8cc169deb4262394b23a5780cf08c27567b523e6"
+  },
+  {
+   "file": "sat/proofs/P111_sym_h9_alt.drat.xz",
+   "sha256": "6de05f478a04dfc97f5b66644262e2f0ac742f1b399bab775134641a9b30b04d"
+  },
+  {
+   "file": "sat/proofs/P112_sym_h9_alt.drat.xz",
+   "sha256": "db1e4a2526ed9593f7b8444bde8da3062c37ac00a3a49faa4ae92b035d95cc7d"
+  },
+  {
+   "file": "sat/proofs/edge_N0_r7.drat.xz",
+   "sha256": "9a22571653eb87be39b4650d03e7587072f5fd6332cc4162bde629e17d872e51"
+  },
+  {
+   "file": "sat/proofs/tri_keep11.drat.xz",
+   "sha256": "5f31be0fd422372d77319c45e51488bb8eb4474f4e31402715d40572b1ec2907"
+  }
+ ]
+}
\ No newline at end of file
diff --git a/research/decoder-floors-frontier-format/checks/c1_rigidity.py b/research/decoder-floors-frontier-format/checks/c1_rigidity.py
new file mode 100644
index 0000000000..7fa486b1bb
--- /dev/null
+++ b/research/decoder-floors-frontier-format/checks/c1_rigidity.py
@@ -0,0 +1,72 @@
+"""Theorem R (rigidity of the minimal-rank label table), replayed.  Standard library only; kissat 4.0.4 and drat-trim are optional (SKIP lines without them).
+For each registry instance (sat/rigid.py): the regenerated DIMACS must have the recorded sha256 (sat/results.jsonl); recorded statuses must equal the expected ones
+(alt instances at the minimal rank: UNSAT, DRAT-VERIFIED when recorded; controls and negative controls: SAT with a decoded model); shipped proofs
+(sat/proofs/*.drat.xz) are replayed with drat-trim; with kissat available every instance is re-solved, UNSAT proofs are checked, SAT models are decoded."""
+import sys, os, json, time, lzma, tempfile, itertools
+HERE = os.path.dirname(os.path.abspath(__file__)); PKG = os.path.join(HERE, '..')
+sys.path.insert(0, os.path.join(PKG, 'lib')); sys.path.insert(0, os.path.join(PKG, 'sat'))
+from report import check, finish
+from rigid import *
+import solve as S_
+
+rows = [json.loads(l) for l in open(os.path.join(PKG, 'sat', 'results.jsonl'))]
+R = registry(); t0 = time.time()
+check('c1.coverage', set(r['name'] for r in rows) == set(R) and len(rows) == len(R), 'every one of the %d registry instances has a recorded result' % len(R))
+bad = [r['name'] for r in rows if r['status'] != r['expect'] or (r['status'] == 'UNSAT' and r.get('drat') != 'VERIFIED')]
+check('c1.status', not bad, 'recorded statuses: %d UNSAT (all DRAT VERIFIED when recorded), %d SAT, none unexpected %s' % (
+    sum(r['status'] == 'UNSAT' for r in rows), sum(r['status'] == 'SAT' for r in rows), bad[:3]))
+badh = []; cnfs = {}
+for r in rows:
+    nv, cls, info, *_ = build_named(r['name']); d = dimacs(nv, cls)
+    if sha(d) != r['cnf_sha256'] or nv != r['nv'] or len(cls) != r['ncls']: badh.append(r['name'])
+    cnfs[r['name']] = d
+check('c1.hash', not badh, 'regenerated DIMACS of all %d instances has the recorded sha256, #vars, #clauses %s (%.0f s)' % (len(rows), badh[:3], time.time() - t0))
+# gauge cliques are pairwise non-orthogonal
+def of_for(r):
+    return p111()[1] if r['unit'] == 'P111' else orth
+badg = [n for n, r in R.items() if any(of_for(r)(a, b) for a, b in itertools.combinations(r['S'], 2))]
+check('c1.gauge', not badg, 'every gauge set S is a pairwise non-orthogonal clique (|S| = 8 for E8/P112/P104/P111, 7 for E7, 5 for E6)')
+# the alt instances at the minimal rank: UNSAT <=> every fitting B of rank <= h is dense.  Controls: SAT and the decoded model is dense for h = rank(dense B)
+ctl = [r for r in rows if r['mode'] == 'ctl']
+check('c1.ctl', all(r['status'] == 'SAT' and r['model_fitting'] and r['orth_zero'] == 0 for r in ctl),
+      'controls (no alt clause): all %d are SAT, every decoded model is a fitting matrix with 0 of its orthogonal entries equal to 0, i.e. equal to the dense B (h = rank of the dense B)' % len(ctl))
+neg = [r for r in rows if r['name'].startswith('SUB') or r['name'].startswith('P112_') and r['h'] == 10]
+check('c1.neg', all(r['status'] == 'SAT' and r['model_fitting'] and r['orth_zero'] > 0 for r in neg),
+      'negative controls: %s are SAT with decoded fitting matrices that are NOT dense (orthogonal entries equal to 0: %s)' % (
+          [r['name'] for r in neg], {r['name']: '%d/%d' % (r['orth_zero'], r['orth_total']) for r in neg}))
+# shipped proofs
+dt = S_.drat_trim(); ks = S_.kissat()
+pdir = os.path.join(PKG, 'sat', 'proofs'); proofs = sorted(f for f in os.listdir(pdir) if f[:-len('.drat.xz')] in R) if os.path.isdir(pdir) else []
+if dt and proofs:
+    okp = 0; badp = []
+    with tempfile.TemporaryDirectory() as td:
+        for f in proofs:
+            n = f[:-len('.drat.xz')]; cnf = os.path.join(td, 'x.cnf'); pr = os.path.join(td, 'x.drat')
+            open(cnf, 'w').write(cnfs[n]); open(pr, 'wb').write(lzma.open(os.path.join(pdir, f)).read())
+            if S_.run_drat(cnf, pr): okp += 1
+            else: badp.append(n)
+    check('c1.shipped', okp == len(proofs), 'drat-trim verifies all %d shipped DRAT proofs (sat/proofs, binary format) against the regenerated CNFs %s' % (okp, badp))
+else:
+    print('SKIP c1.shipped  drat-trim not found (set DRAT_TRIM=/path/to/drat-trim): %d shipped proofs not re-checked' % len(proofs), flush=True)
+# re-solve with kissat
+if ks:
+    only = os.environ.get('RIGID_ONLY'); okr = 0; fails = []; nd = 0; t1 = time.time()
+    with tempfile.TemporaryDirectory() as td:
+        for r in rows:
+            if only and only not in r['name']: continue
+            cnf = os.path.join(td, 'x.cnf'); pr = os.path.join(td, 'x.drat'); open(cnf, 'w').write(cnfs[r['name']])
+            st, model = S_.run_kissat(cnf, pr if r['expect'] == 'UNSAT' else None)
+            good = st == r['expect']
+            if good and st == 'UNSAT' and dt:
+                good = S_.run_drat(cnf, pr); nd += 1
+            if good and st == 'SAT':
+                fit, z, n = decode_model(r['name'], model)
+                good = fit and ((z == 0) if r['mode'] == 'ctl' else (z > 0))
+            okr += good
+            if not good: fails.append(r['name'])
+    check('c1.resolve', not fails, 're-solved %d instances with kissat 4.0.4 (%s): all as expected (UNSAT, %d proofs checked by drat-trim; SAT: models decode to fitting matrices, dense for controls, non-dense for negative controls) %s (%.0f s)' % (
+        okr, 'DRAT checked' if dt else 'drat-trim absent: UNSAT proofs NOT checked', nd, fails[:3], time.time() - t1))
+else:
+    print('SKIP c1.resolve  kissat not found (set KISSAT=/path/to/kissat): the %d recorded solver verdicts are not re-derived' % len(rows), flush=True)
+print('   (c1 %.0f s)' % (time.time() - t0))
+finish()
diff --git a/research/decoder-floors-frontier-format/checks/c2_support_propagation.py b/research/decoder-floors-frontier-format/checks/c2_support_propagation.py
new file mode 100644
index 0000000000..6a2f9d80c2
--- /dev/null
+++ b/research/decoder-floors-frontier-format/checks/c2_support_propagation.py
@@ -0,0 +1,56 @@
+"""Lemma 1.1 (support propagation) census and the survivor pair ranks behind Theorem P (IDEAL3 THEORY §1.1-1.3).  Exact bitmask arithmetic, standard library only.
+A label class O is the support of a nonzero vector of col B (B = dense pairing, rank h).  O is *deficient* in a rank-T realisation M iff some functional
+h* != 0 kills p0(O).  Lemma 1.1: for every T-frame E write h* = sum_e c_e q0(e); then c_e = 0 on E cap O, and for every T-frame F,
+supp(c) subset (E \\ O) cap union_{g in F \\ O} Nbar(g), Nbar(x) = {lines non-orthogonal to x} (x itself included).  Iterate to the fixed point; if some S_E becomes
+empty then O is non-deficient in EVERY rank-T realisation.  Survivors = classes that are not certified."""
+import sys, os, time, itertools
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, os.path.join(HERE, '..', 'lib'))
+from report import check, finish
+from units import *
+
+from supprop import setup, propagate, census
+
+t0 = time.time()
+L112 = sub(P112_IDX); L104 = sub(unit_idx('P104H4'))
+from roots import D4, D6, E7, E8
+exp = {  # name: (lines, T, #frames, #classes, #survivors, survivor sizes)
+    'D4': (D4, 4, 3, 7, 0, []), 'D6': (D6, 6, 15, 31, 0, []), 'E7': (E7, 7, 135, 127, 0, []),
+    'E8': (E8, 8, 2025, 511, 0, []), 'P112': (L112, 8, 1260, 511, 8, [56]), 'P104': (L104, 8, 759, 511, 16, [52])}
+R = {}
+for n, (L, T, nf, ncl, nsurv, sizes) in exp.items():
+    r = census(L, T); R[n] = r
+    got = (r['nframes'], r['nclasses'], len(r['unc']), sorted(set(popcount(w) for _, w in r['unc'])))
+    check('c2.cert.' + n, got == (nf, ncl, nsurv, sizes), '%s (T=%d, h=%d): %d T-frames, %d label classes, %d not certified by Lemma 1.1, sizes %s' % (n, T, r['h'], got[0], got[1], got[2], got[3]))
+print('   (census %.0f s)' % (time.time() - t0))
+# survivors: no 2-dim subspace; each survivor is the set of live lines orthogonal to one removed root f in F0 (P112) / in F0 u F1 (P104) and has Q-rank 7
+for n, L, removed in (('P112', L112, F0), ('P104', L104, F0 + H4F1)):
+    unc = R[n]['unc']; cos = set(c for c, _ in unc)
+    sub2 = any((a ^ b) in cos for a, b in itertools.combinations(sorted(cos), 2))
+    check('c2.nosub2.' + n, not sub2, '%s: the %d survivor classes contain no 2-dimensional subspace of the label space (a ^ b is never a survivor)' % (n, len(unc)))
+    ws = set(w for _, w in unc); want = set()
+    for f in removed:
+        want.add(sum(1 << i for i, r in enumerate(L) if dot(r, E8[f]) == 0))
+    check('c2.perp.' + n, ws == want, '%s: the survivors are exactly the sets of live lines orthogonal to one removed root (%d of them)' % (n, len(want)))
+    rk = set(rank_q([list(L[i]) for i in range(len(L)) if w >> i & 1]) for w in ws)
+    check('c2.qrank.' + n, rk == {7}, '%s: each survivor spans a 7-dimensional space over Q (Gram-deficient), rank_Q = %s' % (n, sorted(rk)))
+# pair ranks  rank_F2 B[V \ O, V \ O'] over all survivor pairs (O = O' included)
+for n, L in (('P112', L112), ('P104', L104)):
+    unc = R[n]['unc']; Br = R[n]['Br']; v = len(L); full = (1 << v) - 1; out = {}
+    for (_, O), (_, O2) in itertools.product(unc, unc):
+        k = blk(Br, bits(full & ~O), bits(full & ~O2)); out[k] = out.get(k, 0) + 1
+    want = {8: 64} if n == 'P112' else {8: 192, 7: 64}
+    check('c2.pairs.' + n, out == want, '%s: rank_F2 B[V\\O, V\\O\'] over all %d ordered survivor pairs (O = O\' included) takes the values %s (value: count); the minimum is %d, i.e. every term costs at least %d' % (n, len(unc) ** 2, out, min(out), min(out)))
+
+# exactness of the per-term rank: Def(V \\ O) = {0, w_O} for every survivor O (so the pair ranks above are the ranks of the pairs (Def(R), Def(A)) = (<w_O>, <w_O'>)),
+# and the single-deficiency ranks rank B[V \\ O, V] (the (1, 0) and (0, 1) cases)
+for n, L in (('P112', L112), ('P104', L104)):
+    unc = R[n]['unc']; Br = R[n]['Br']; v = len(L); full = (1 << v) - 1; classes = span_vectors(colspace_basis(Br))
+    ok = all(sorted(w for _, w in classes if w & ~O == 0) == [O] for _, O in unc)
+    check('c2.def.' + n, ok, '%s: for every survivor O the classes with support inside O are exactly {O} itself, so Def(V \\ O) is the one-dimensional space <w_O>' % n)
+    single = set(blk(Br, bits(full & ~O), list(range(v))) for _, O in unc)
+    check('c2.single.' + n, single == {8}, '%s: rank_F2 B[V \\ O, V] = %s for every survivor O (a single deficiency costs one unit of rank: 9 - 1)' % (n, sorted(single)))
+# gauge: dense B has rank h and the survivors are the only non-certified classes => Theorem P's per-term floor 9 - delta(R) - delta(A) >= 8 with delta <= 1
+for n in ('P112', 'P104', 'E8', 'E7'):
+    h = R[n]['h']; check('c2.rankB.' + n, h == (7 if n == 'E7' else 9), '%s: rank_F2 of the dense pairing is %d' % (n, h))
+finish()
diff --git a/research/decoder-floors-frontier-format/checks/c3_batch_premises.py b/research/decoder-floors-frontier-format/checks/c3_batch_premises.py
new file mode 100644
index 0000000000..dfd0395207
--- /dev/null
+++ b/research/decoder-floors-frontier-format/checks/c3_batch_premises.py
@@ -0,0 +1,91 @@
+"""Finite premises of Theorem B / Bk (STRAYS-BATCH THEORY §1-§3): labels of P112 in F2^9, the 8 exceptional hyperplanes, the normals w_i with b(w_i,w_j) = 1,
+rho(N(f_i), N(f_j)) = 8, the frame lemma E cap N(f_i) cap N(f_j) = empty, and an O(9) chart on which all 64 cross pairs of coordinate supports pair at rank 7
+(the per-term floor 7 of Theorem B is attained, so the counting bound 120 is not the truth).  Standard library only; the chart is searched
+with a fixed seed (random.Random(52)) and the found chart is shipped in data/chart_rank7.json, which is re-verified here."""
+import sys, os, json, random, itertools
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, os.path.join(HERE, '..', 'lib'))
+from report import check, finish
+from units import *
+
+L = sub(P112_IDX); v = len(L); Br = b0rows(L); G = gram(L)
+# dense B has rank 9; basis = first 9 independent rows
+basis = []
+for t in range(v):
+    if rank_f2([Br[x] for x in basis + [t]]) == len(basis) + 1: basis.append(t)
+    if len(basis) == 9: break
+check('c3.rank', rank_f2(Br) == 9 and len(basis) == 9, 'P112 dense pairing has rank 9; basis lines %s' % basis)
+combo = {}
+for co in range(512):
+    w = 0
+    for i in range(9):
+        if co >> i & 1: w ^= Br[basis[i]]
+    combo.setdefault(w, co)
+lab = [combo[Br[t]] for t in range(v)]                      # label of line t: coefficient vector (9-bit int) over the basis rows
+Gb = [[Br[basis[i]] >> basis[j] & 1 for j in range(9)] for i in range(9)]
+def bf(x, y):
+    s = 0
+    for i in range(9):
+        if x >> i & 1:
+            for j in range(9):
+                if y >> j & 1: s ^= Gb[i][j]
+    return s
+check('c3.labels', all(bf(lab[t], lab[s]) == (Br[t] >> s & 1) for t in range(v) for s in range(v)), 'labels realise the dense pairing: b(lab_t, lab_s) = B_ts for all 112 x 112 pairs')
+def hfun(h, x): return bin(h & x).count('1') & 1
+live_of = [E8[i] for i in P112_IDX]
+Of = []; N = []
+for f in F0:
+    Of.append(set(t for t in range(v) if dot(live_of[t], E8[f]) == 0)); N.append([t for t in range(v) if dot(live_of[t], E8[f]) != 0])
+hyps = []
+for Oset in Of:
+    sols = [h for h in range(1, 512) if set(t for t in range(v) if hfun(h, lab[t])) == Oset]
+    hyps.append(sols)
+check('c3.hyps', all(len(s) == 1 for s in hyps), 'for each removed root f_i the class O_i = {live lines orthogonal to f_i} is the support of exactly one functional h_i on the label space')
+W = []
+for s in hyps:
+    h = s[0]; ws = [w for w in range(512) if all(bf(w, 1 << j) == (h >> j & 1) for j in range(9))]
+    W.append(ws[0] if len(ws) == 1 else None)
+check('c3.normals', all(w is not None for w in W), 'the pairing is nondegenerate: each h_i = b(w_i, .) for a unique normal w_i')
+check('c3.premiseP2a', all(bf(W[i], W[j]) == 1 for i in range(8) for j in range(8)), 'b(w_i, w_j) = 1 for all 64 ordered pairs, i = j included (every normal is non-isotropic, any two are non-orthogonal)')
+rho = set(rank_f2([sum(1 << k for k, s in enumerate(N[j]) if Br[t] >> s & 1) for t in N[i]]) for i in range(8) for j in range(8))
+check('c3.premiseP2b', rho == {8}, 'rho(E_i, E_j) = rank_F2 B[N(f_i), N(f_j)] = %s for all 64 ordered pairs' % sorted(rho))
+# survivors (Gram-deficient classes) via Q-rank: label classes whose support has rank_Q < 8 ... equivalently the 8 hyperplanes O_i
+surv = [h for h in range(1, 512) if rank_q([list(L[t]) for t in range(v) if hfun(h, lab[t])]) < 8]
+check('c3.deficient', sorted(surv) == sorted(s[0] for s in hyps) and len(surv) == 8, 'the Gram-deficient label classes (support of rank_Q < 8) are exactly the 8 classes O_i')
+check('c3.nosub2', not any((a ^ b) in set(surv) for a, b in itertools.combinations(surv, 2)), 'no two of them add up to a third: no 2-dimensional subspace among the 8 deficient classes')
+# frame lemma for Theorem Bk: for every i < j some live 8-frame E has E cap N(f_i) cap N(f_j) = empty
+adj = orth_graph(L); frames = [c for c in maximal_cliques(adj) if popcount(c) == 8]
+Nm = [sum(1 << t for t in n) for n in N]
+ok = all(any(E & Nm[i] & Nm[j] == 0 for E in frames) for i, j in itertools.combinations(range(8), 2))
+check('c3.framelemma', ok and len(frames) == 1260, 'for every i < j (28 pairs) some one of the 1260 live 8-frames E has E cap N(f_i) cap N(f_j) = empty')
+# O(9) charts: transvections x -> x + b(x, u) u (u isotropic) generate; Phi given by images of the 9 basis vectors
+iso = [u for u in range(1, 512) if bf(u, u) == 0]
+def tv(u, x): return x ^ (u if bf(x, u) else 0)
+def compose(Phi, u): return [tv(u, x) for x in Phi]
+def apply(Phi, x):
+    y = 0
+    for i in range(9):
+        if x >> i & 1: y ^= Phi[i]
+    return y
+def orth_count(Phi): return sum(bf(W[i], apply(Phi, W[k])) == 0 for i in range(8) for k in range(8))
+def is_isometry(Phi): return all(bf(apply(Phi, 1 << i), apply(Phi, 1 << j)) == bf(1 << i, 1 << j) for i in range(9) for j in range(9))
+chart_file = os.path.join(HERE, '..', 'data', 'chart_rank7.json')
+if not os.path.exists(chart_file):
+    rng = random.Random(52); best = (0, None)
+    for s in range(30000):
+        Phi = [1 << i for i in range(9)]
+        for _ in range(rng.randint(1, 40)): Phi = compose(Phi, rng.choice(iso))
+        c = orth_count(Phi)
+        if c > best[0]: best = (c, Phi)
+        if c == 64: break
+    json.dump(dict(orth_cross_pairs=best[0], Phi=best[1], note='images of the 9 label basis vectors (9-bit ints); found by random.Random(52) products of isotropic transvections'), open(chart_file, 'w'))
+ch = json.load(open(chart_file)); Phi = ch['Phi']
+check('c3.chart.isometry', is_isometry(Phi), 'the shipped chart Phi preserves the pairing b (Phi in O(9, F2))')
+lab2 = [apply(Phi, x) for x in lab]
+def span_cost(S, T_):
+    return rank_f2([sum(bf(a, b) << k for k, b in enumerate(T_)) for a in S])
+costs = set(span_cost([lab[t] for t in N[i]], [lab2[t] for t in N[k]]) for i in range(8) for k in range(8))
+check('c3.chart.rank7', orth_count(Phi) == ch['orth_cross_pairs'] and costs == {7}, 'chart Phi: b(w_i, Phi w_k) = 0 for %d/64 (i,k) and all 64 cross pairs rho(call-1 support N(f_i), call-2 support N(f_k)) have F2-rank %s' % (orth_count(Phi), sorted(costs)))
+same = set(span_cost([lab[t] for t in N[i]], [lab[t] for t in N[k]]) for i in range(8) for k in range(8))
+check('c3.chart.same', same == {8}, 'within one call the same pairings have rank %s (so rank-7 terms are pure cross-call)' % sorted(same))
+finish()
diff --git a/research/decoder-floors-frontier-format/checks/c4_masked_costar.py b/research/decoder-floors-frontier-format/checks/c4_masked_costar.py
new file mode 100644
index 0000000000..85880e2fa1
--- /dev/null
+++ b/research/decoder-floors-frontier-format/checks/c4_masked_costar.py
@@ -0,0 +1,51 @@
+"""STRAYS-MASK finite inputs (standard library only): (1) #1180's nine-term outside-col-M identity on P112 costs exactly 65 under the dense B (and the
+removed-frame decoder it merges into costs 64); (2) all 120 co-star dead sets V \\ S_alpha are certified spanning in every rank-8 realisation (Lemma 1.1),
+so every nine-term masked co-star decoder is a square biorthogonal decoder of a rank-9 realisation; (3) every survivor class contains an orthogonal 7-clique."""
+import sys, os, itertools
+from collections import Counter
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, os.path.join(HERE, '..', 'lib'))
+from report import check, finish
+from units import *
+from supprop import setup, propagate, census
+
+L = sub(P112_IDX); v = len(L); Br = b0rows(L); G = gram(L)
+sup = lambda col: [t for t in range(v) if col[t] != 0]
+R = [[dot(r, E8[f]) for r in L] for f in F0]                      # coordinates in the removed-frame basis
+base = [blk(Br, sup(R[j]), sup(R[j])) for j in range(8)]
+check('c4.coordinate', base == [8] * 8, 'removed-frame coordinate decoder: term ranks %s, total %d' % (base, sum(base)))
+def identity_scale(D, T):
+    c = sum(D[0][k] * T[0][k] for k in range(len(D[0]))); c0 = G[0][0]
+    return c // c0 if c0 and c % c0 == 0 and all(sum(D[a][k] * T[b][k] for k in range(len(D[0]))) == (c // c0) * G[a][b] for a in range(v) for b in range(v)) else None
+for name, zval in (('z = e_line0 (value 1, #1180)', 1), ('z chosen to kill line 0 in term 1', -R[0][0])):
+    z = [zval if t == 0 else 0 for t in range(v)]
+    t1 = [R[0][t] + z[t] for t in range(v)]
+    terms = [(sup(t1), sup(R[0]))] + [(sup(R[j]), sup(R[j])) for j in range(1, 8)] + [(sup(z), sup(R[0]))]
+    rk = [blk(Br, a, b) for a, b in terms]
+    D = [[t1[t]] + [R[j][t] for j in range(1, 8)] + [-z[t]] for t in range(v)]
+    T = [[R[0][t]] + [R[j][t] for j in range(1, 8)] + [R[0][t]] for t in range(v)]
+    sc = identity_scale(D, T)
+    if zval == 1:
+        check('c4.ex1180', sc is not None and rk == [8] * 8 + [1] and sum(rk) == 65, '#1180 nine-term identity (%s): D T^T = %s x Gram exactly on all 112 x 112 entries; term ranks %s, total %d' % (name, sc, rk, sum(rk)))
+    else:
+        print('   info: %s -> identity scale %s, term ranks %s, total %d' % (name, sc, rk, sum(rk)))
+        check('c4.ex1180.alt', sc is not None and sum(rk) >= 64, 'variant %s: exact identity and total %d >= 64' % (name, sum(rk)))
+# the two outside-col-M terms of #1180 share one column vector R_0: they merge into the removed-frame term
+# (co-star theorem) all 120 dead sets are certified spanning
+v_, frames, nbar = setup(L, 8); full = (1 << v) - 1
+res = []
+for a in range(120):
+    S = sum(1 << t for t in range(v) if dot(L[t], E8[a]) == 0 or P112_IDX[t] == a)
+    dead = full & ~S
+    res.append((a in set(F0), popcount(S), min(popcount(s) for s in propagate(dead, frames, nbar)) == 0))
+cnt = Counter(res)
+check('c4.costar', cnt == Counter({(False, 60, True): 112, (True, 56, True): 8}), 'all 120 co-star dead sets V \\ S_alpha are certified spanning in every rank-8 realisation: %s (alpha in F0, |S_alpha|, certified): count' % dict(cnt))
+# survivor classes: max orthogonal clique 7
+unc = census(L, 8)['unc']
+og = orth_graph(L)
+w = set()
+for _, O in unc:
+    adj = [og[t] & O if O >> t & 1 else 0 for t in range(v)]
+    w.add(max(popcount(c) for c in maximal_cliques(adj) if c & O == c and c))
+check('c4.survclique', w == {7}, 'each of the 8 survivor classes contains an orthogonal 7-clique and no orthogonal 8-clique (so the killing functional is unique up to scale in every rank-8 realisation): %s' % sorted(w))
+finish()
diff --git a/research/decoder-floors-frontier-format/checks/c5_attaining_decoders.py b/research/decoder-floors-frontier-format/checks/c5_attaining_decoders.py
new file mode 100644
index 0000000000..d1025a383b
--- /dev/null
+++ b/research/decoder-floors-frontier-format/checks/c5_attaining_decoders.py
@@ -0,0 +1,48 @@
+"""(Adapted without change of content from the author's #2277 package, checks/c5_known_decoders.py.)  The floors are attained: explicit decoders and their exact dense-B costs (E8 72, E7 49, D6 30, D4 12, P112 64, P104 56),
+and the trivial decoder (cost v) for E6 and D5.  Exact Fractions; standard library only.
+Frame decoder of a unit with an orthogonal frame f_1..f_T spanning its space: p_j(t) = <r_t, f_j>, q_j(s) = <r_s, f_j>/<f_j, f_j>; then
+M = sum_j p_j q_j^T is the Gram matrix of the live lines.  (P112 uses the frame of the removed lines.)"""
+import sys, os, json
+sys.path.insert(0, os.path.join(os.path.dirname(os.path.abspath(__file__)), '..', 'lib'))
+from report import check, finish
+from fractions import Fraction as Fr
+from roots import *
+from frames import units
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+D = json.load(open(os.path.join(HERE, '..', 'data', 'p104_frames.json'))); F0, F1, pairs = D['F0'], D['F1'], D['pairs']
+
+def frame_decoder(live, frame_vecs):
+    v = len(live); Br = b0rows(live); G = gram(live); cost = 0
+    M = [[Fr(0)] * v for _ in range(v)]
+    for f in frame_vecs:
+        nf = dot(f, f); p = [dot(r, f) for r in live]
+        for t in range(v):
+            if p[t]:
+                for s in range(v):
+                    if p[s]: M[t][s] += Fr(p[t] * p[s], nf)
+        R = [t for t in range(v) if p[t] != 0]; cost += blk(Br, R, R)
+    return M == [[Fr(G[t][s]) for s in range(v)] for t in range(v)], cost
+
+U = units(); L8 = UNITS['E8'][0]
+for name, want in (('D4', 12), ('D6', 30), ('E7', 49), ('E8', 72)):
+    L, T = U[name]; fr = bits(next(c for c in maximal_cliques(orth_graph(L)) if popcount(c) == T))
+    ok, cost = frame_decoder(L, [L[i] for i in fr])
+    check('c5.' + name, ok and cost == want, '%s: frame decoder with %d terms has M = Gram (zero on orthogonal pairs, nonzero diagonal) and dense-B cost %d' % (name, T, cost))
+live112 = [L8[t] for t in range(120) if t not in set(F0)]
+ok, cost = frame_decoder(live112, [L8[i] for i in F0])
+check('c5.P112', ok and cost == 64, 'P112 (E8 minus a frame): removed-frame decoder has M = Gram and dense cost %d' % cost)
+# P104: E8 minus two frames; terms (a_j, b_j) with a_j in F0, b_j in F1 (pairs from the #968 construction as recorded in data/p104_frames.json):
+live104i = [t for t in range(120) if t not in set(F0) | set(F1)]; live104 = [L8[t] for t in live104i]; v = len(live104); Br = b0rows(live104); G = gram(live104)
+M = [[sum(dot(live104[t], L8[x]) * dot(live104[s], L8[y]) for x, y in pairs) for s in range(v)] for t in range(v)]
+okM = all(M[t][t] != 0 for t in range(v)) and all(M[t][s] == 0 for t in range(v) for s in range(v) if t != s and G[t][s] == 0)
+cost = 0
+for x, y in pairs:
+    R = [i for i, t in enumerate(live104i) if dot(L8[t], L8[x]) != 0]; A = [i for i, t in enumerate(live104i) if dot(L8[t], L8[y]) != 0]
+    cost += blk(Br, R, A)
+check('c5.P104', okM and cost == 56, 'P104: the 8 frame-pair terms give a realisation M (zero on orthogonal pairs, nonzero diagonal; not the Gram matrix) of dense cost %d' % cost)
+for name, v_ in (('E6', 36), ('D5', 20)):
+    L, T = U[name]; Br = b0rows(L)
+    cost = sum(blk(Br, [t], [t]) for t in range(len(L)))
+    check('c5.' + name, len(L) == v_ and cost == v_, '%s: the trivial decoder (M = I, one single-entry term per line) costs %d = v; this equals the floor proved for the scaled-Gram realisations (M = I is a different realisation)' % (name, cost))
+finish()
diff --git a/research/decoder-floors-frontier-format/checks/c6_block_minrank_punctures.py b/research/decoder-floors-frontier-format/checks/c6_block_minrank_punctures.py
new file mode 100644
index 0000000000..fb5ca2e4ae
--- /dev/null
+++ b/research/decoder-floors-frontier-format/checks/c6_block_minrank_punctures.py
@@ -0,0 +1,68 @@
+"""EDGE E1a (the coordinate block N(f) of P112 has fitting minrank 8 for EVERY admissible B) and NEWWORD C4.1 (clique-hitting bounds on punctures of N(f)).
+Standard library only; kissat 4.0.4 and drat-trim are optional.  Registry: sat/misc.py; recorded verdicts: sat/results_misc.jsonl."""
+import sys, os, json, time, lzma, tempfile, itertools
+HERE = os.path.dirname(os.path.abspath(__file__)); PKG = os.path.join(HERE, '..')
+sys.path.insert(0, os.path.join(PKG, 'lib')); sys.path.insert(0, os.path.join(PKG, 'sat'))
+from report import check, finish
+from units import *
+import misc, hitting
+import solve as S_
+
+t0 = time.time()
+L = sub(P112_IDX); v = len(L); G = gram(L)
+Ns = [[t for t in range(v) if dot(L[t], E8[f]) != 0] for f in F0]
+check('c6.N', all(len(n) == 56 for n in Ns) and all(sum(1 for n in Ns if t in n) == 4 for t in range(v)), 'N(f) has 56 live lines for each of the 8 removed roots, and every live line lies in exactly 4 of them')
+Br = b0rows(L)
+check('c6.dense', all(blk(Br, n, n) == 8 for n in Ns), 'dense pairing: rank_F2 B[N(f), N(f)] = 8 for all 8 f (the 64 of P112)')
+og = orth_graph(L); nog = nonorth_graph = [sum(1 << s for s in range(v) if s != t and G[t][s] != 0) for t in range(v)]
+Nm = [sum(1 << t for t in n) for n in Ns]
+alpha = max(popcount(c) for c in maximal_cliques([og[t] & Nm[0] if Nm[0] >> t & 1 else 0 for t in range(v)]))
+omega = max(popcount(c) for c in maximal_cliques([nog[t] & Nm[0] if Nm[0] >> t & 1 else 0 for t in range(v)]))
+check('c6.alpha', alpha == 4 and omega == 7, 'inside N(f): largest pairwise orthogonal set alpha = %d, largest pairwise non-orthogonal clique omega = %d' % (alpha, omega))
+check('c6.f7', 56 - alpha == 52, 'puncturing to rank <= 1 (s = 7) must leave a pairwise-orthogonal set: at most alpha = 4 lines kept, so f(7) >= 52 (exact, no SAT)')
+rows = [json.loads(l) for l in open(os.path.join(PKG, 'sat', 'results_misc.jsonl'))]
+R = misc.registry(); fast = {n for n in R if not R[n]['slow']}
+have = {r['name'] for r in rows}
+check('c6.coverage', fast <= have, 'every fast registry instance has a recorded result (%d recorded, %d fast)' % (len(have), len(fast)))
+bad = [r['name'] for r in rows if r['status'] != (R[r['name']]['expect'] if r['name'] in R else r['status']) or (r['status'] == 'UNSAT' and not r['slow'] and r.get('drat') != 'VERIFIED') or (r['status'] == 'SAT' and not r.get('model_ok'))]
+check('c6.status', not bad, 'recorded statuses as expected: %d UNSAT (DRAT VERIFIED when recorded unless flagged slow), %d SAT with checked models %s' % (
+    sum(r['status'] == 'UNSAT' for r in rows), sum(r['status'] == 'SAT' for r in rows), bad[:3]))
+cnfs = {}; badh = []
+for r in rows:
+    if r['slow'] and not os.environ.get('HIT_FULL'): continue
+    d = misc.dimacs_of(r['name']); cnfs[r['name']] = d
+    import hashlib
+    if hashlib.sha256(d.encode()).hexdigest() != r['cnf_sha256']: badh.append(r['name'])
+check('c6.hash', not badh, 'regenerated DIMACS of %d instances has the recorded sha256 %s' % (len(cnfs), badh[:3]))
+dt = S_.drat_trim(); ks = S_.kissat()
+pdir = os.path.join(PKG, 'sat', 'proofs'); proofs = sorted(f for f in (os.listdir(pdir) if os.path.isdir(pdir) else []) if f.split('_')[0] in ('edge', 'hit', 'tri'))
+if dt and proofs:
+    ok = 0
+    with tempfile.TemporaryDirectory() as td:
+        for f in proofs:
+            n = f[:-len('.drat.xz')]; cnf = os.path.join(td, 'x.cnf'); pr = os.path.join(td, 'x.drat')
+            open(cnf, 'w').write(cnfs[n]); open(pr, 'wb').write(lzma.open(os.path.join(pdir, f)).read()); ok += S_.run_drat(cnf, pr)
+    check('c6.shipped', ok == len(proofs), 'drat-trim verifies all %d shipped proofs of this check against the regenerated CNFs' % ok)
+else:
+    print('SKIP c6.shipped  drat-trim not found: %d shipped proofs not re-checked' % len(proofs), flush=True)
+if ks:
+    fails = []; nd = 0
+    with tempfile.TemporaryDirectory() as td:
+        for n, d in cnfs.items():
+            if R[n]['slow'] and not os.environ.get('HIT_FULL'): continue
+            cnf = os.path.join(td, 'x.cnf'); pr = os.path.join(td, 'x.drat'); open(cnf, 'w').write(d)
+            slow = R[n]['slow']
+            st, model = S_.run_kissat(cnf, None if (slow or R[n]['expect'] == 'SAT') else pr, tmo=3000)
+            good = st == R[n]['expect']
+            if good and st == 'UNSAT' and dt and not slow: good = S_.run_drat(cnf, pr); nd += 1
+            if good and st == 'SAT': good = misc.check_model(n, model)
+            if not good: fails.append(n)
+    check('c6.resolve', not fails, 're-solved the registry with kissat 4.0.4 (%s): all as expected, %d UNSAT proofs checked by drat-trim %s' % ('HIT_FULL: slow instances included' if os.environ.get('HIT_FULL') else 'fast instances', nd, fails[:3]))
+else:
+    print('SKIP c6.resolve  kissat not found: recorded verdicts not re-derived', flush=True)
+# consequences (arithmetic on the proven bounds)
+tri = [r for r in rows if r['name'] == 'tri_keep11'][0]
+f_ = {2: 14, 6: 56 - 10, 7: 52, 8: 56}
+check('c6.f', f_[2] == 13 + 1 and f_[6] == 46, 'f(2) >= 14 (k = 7: no hitting set of 13 lines for the 576 7-cliques); f(6) >= 56 - 10 = 46 (no triangle-free kept set of 11 lines); f(7) >= 52; f(8) = 56; ratios s/f(s): %s' % {s: round(s / f_[s], 4) for s in f_})
+print('   (c6 %.0f s)' % (time.time() - t0))
+finish()
diff --git a/research/decoder-floors-frontier-format/checks/c7_p111_unit.py b/research/decoder-floors-frontier-format/checks/c7_p111_unit.py
new file mode 100644
index 0000000000..c6e5e6a830
--- /dev/null
+++ b/research/decoder-floors-frontier-format/checks/c7_p111_unit.py
@@ -0,0 +1,31 @@
+"""The P111 bit unit of PR #589's word (data/p111_lines.json): 111 of the 120 lines of the E8 line system in the doubled Hamming coordinates of that word.
+Standard library only.  The rigidity SAT instances for it are replayed in c1 (P111_*); the 'at most 12 retained totals cost >= 63' statement is RECORDED, not checked here."""
+import sys, os, json, itertools
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, os.path.join(HERE, '..', 'lib'))
+from report import check, finish
+from roots import rank_f2, rank_q, maximal_cliques, popcount
+
+L = json.load(open(os.path.join(HERE, '..', 'data', 'p111_lines.json')))['lines']
+ip = lambda x, y: sum(a * b for a, b in zip(x, y))
+canon = lambda v: tuple(v) if next(x for x in v if x) > 0 else tuple(-x for x in v)
+check('c7.count', len(L) == 111 and len(set(canon(v) for v in L)) == 111, '111 distinct lines')
+check('c7.norm', all(ip(v, v) == 4 for v in L), 'every line has squared norm 4 (so ip // 2 is the Gram entry 2 on the diagonal)')
+check('c7.gram', all(ip(a, b) in (0, 2, -2) for a, b in itertools.combinations(L, 2)), 'distinct lines have inner product 0 or +-2, i.e. Gram entry 0 or +-1: the lines are roots of a root system (a sub-configuration of E8)')
+# the 120-line completion of core.py: 8 axes (2 e_i) and, for each 4-support occurring among the live weight-4 lines, all sign patterns with the first entry +1
+sup4 = sorted({tuple(i for i, x in enumerate(v) if x) for v in L if sum(1 for x in v if x) == 4})
+full = {tuple(2 if k == i else 0 for k in range(8)) for i in range(8)}
+for s in sup4:
+    for signs in itertools.product((1, -1), repeat=3):
+        v = [0] * 8; v[s[0]] = 1
+        for k, j in enumerate(s[1:]): v[j] = signs[k]
+        full.add(tuple(v))
+full = sorted(full); live = set(canon(v) for v in L)
+check('c7.e8', len(sup4) == 14 and len(full) == 120 and live <= set(canon(v) for v in full) and all(ip(a, b) in (0, 2, -2, 4) for a, b in itertools.combinations(full, 2)), 'the live lines lie in a 120-line root-line system (8 axes + 14 four-supports x 8 sign patterns): P111 = that system minus 9 lines')
+check('c7.rankQ', rank_q([list(v) for v in L]) == 8, 'the 111 lines span Q^8')
+orthmask = [sum(1 << s for s in range(111) if s != t and ip(L[t], L[s]) == 0) for t in range(111)]
+Br = [sum(1 << s for s in range(111) if s == t or ip(L[t], L[s]) == 0) for t in range(111)]
+check('c7.rankF2', rank_f2(Br) == 9, 'the dense pairing B_d = J + Abar of P111 has F2-rank 9 (so h = 9 is the minimal fitting rank when B_d is forced, Theorem R)')
+w = max(popcount(c) for c in maximal_cliques(orthmask))
+check('c7.frame', w == 8, 'P111 contains an orthogonal 8-frame (alpha_perp = 8, so every realisation has rank >= 8)')
+finish()
diff --git a/research/decoder-floors-frontier-format/data/chart_rank7.json b/research/decoder-floors-frontier-format/data/chart_rank7.json
new file mode 100644
index 0000000000..39d66833ad
--- /dev/null
+++ b/research/decoder-floors-frontier-format/data/chart_rank7.json
@@ -0,0 +1 @@
+{"orth_cross_pairs": 64, "Phi": [167, 164, 4, 182, 8, 32, 230, 152, 422], "note": "images of the 9 label basis vectors (9-bit ints); found by random.Random(52) products of isotropic transvections"}
\ No newline at end of file
diff --git a/research/decoder-floors-frontier-format/data/h4_F1.json b/research/decoder-floors-frontier-format/data/h4_F1.json
new file mode 100644
index 0000000000..5926a5adf3
--- /dev/null
+++ b/research/decoder-floors-frontier-format/data/h4_F1.json
@@ -0,0 +1 @@
+[[2, 0, 2, 0, 0, 0, 0, 0], [0, 2, 0, 0, 2, 0, 0, 0], [0, 0, 0, 2, 0, 0, 2, 0], [0, 0, 0, 0, 0, 2, 0, 2], [1, 1, -1, 1, -1, 1, -1, -1], [1, 1, -1, -1, -1, -1, 1, 1], [1, -1, -1, 1, 1, -1, -1, 1], [1, -1, -1, -1, 1, 1, 1, -1]]
\ No newline at end of file
diff --git a/research/decoder-floors-frontier-format/data/p104_frames.json b/research/decoder-floors-frontier-format/data/p104_frames.json
new file mode 100644
index 0000000000..3110c60982
--- /dev/null
+++ b/research/decoder-floors-frontier-format/data/p104_frames.json
@@ -0,0 +1,221 @@
+{
+ "note": "E8 lines (doubled coordinates, order of lib/roots.py:E8). F0,F1: two orthogonal 8-frames (indices into E8); pairs: the 8 (a in F0, b in F1) frame pairs of the #968 decoder as recorded in the author working card SHAPES/p104.pkl.",
+ "F0": [
+  0,
+  26,
+  44,
+  54,
+  1,
+  27,
+  45,
+  55
+ ],
+ "F1": [
+  2,
+  18,
+  40,
+  52,
+  77,
+  86,
+  107,
+  112
+ ],
+ "pairs": [
+  [
+   0,
+   77
+  ],
+  [
+   26,
+   40
+  ],
+  [
+   44,
+   52
+  ],
+  [
+   1,
+   107
+  ],
+  [
+   2,
+   27
+  ],
+  [
+   18,
+   45
+  ],
+  [
+   86,
+   54
+  ],
+  [
+   112,
+   55
+  ]
+ ],
+ "F0_vectors": [
+  [
+   2,
+   2,
+   0,
+   0,
+   0,
+   0,
+   0,
+   0
+  ],
+  [
+   0,
+   0,
+   2,
+   2,
+   0,
+   0,
+   0,
+   0
+  ],
+  [
+   0,
+   0,
+   0,
+   0,
+   2,
+   2,
+   0,
+   0
+  ],
+  [
+   0,
+   0,
+   0,
+   0,
+   0,
+   0,
+   2,
+   2
+  ],
+  [
+   2,
+   -2,
+   0,
+   0,
+   0,
+   0,
+   0,
+   0
+  ],
+  [
+   0,
+   0,
+   2,
+   -2,
+   0,
+   0,
+   0,
+   0
+  ],
+  [
+   0,
+   0,
+   0,
+   0,
+   2,
+   -2,
+   0,
+   0
+  ],
+  [
+   0,
+   0,
+   0,
+   0,
+   0,
+   0,
+   2,
+   -2
+  ]
+ ],
+ "F1_vectors": [
+  [
+   2,
+   0,
+   2,
+   0,
+   0,
+   0,
+   0,
+   0
+  ],
+  [
+   0,
+   2,
+   0,
+   0,
+   2,
+   0,
+   0,
+   0
+  ],
+  [
+   0,
+   0,
+   0,
+   2,
+   0,
+   0,
+   2,
+   0
+  ],
+  [
+   0,
+   0,
+   0,
+   0,
+   0,
+   2,
+   0,
+   2
+  ],
+  [
+   1,
+   1,
+   -1,
+   1,
+   -1,
+   1,
+   -1,
+   -1
+  ],
+  [
+   1,
+   1,
+   -1,
+   -1,
+   -1,
+   -1,
+   1,
+   1
+  ],
+  [
+   1,
+   -1,
+   -1,
+   1,
+   1,
+   -1,
+   -1,
+   1
+  ],
+  [
+   1,
+   -1,
+   -1,
+   -1,
+   1,
+   1,
+   1,
+   -1
+  ]
+ ]
+}
\ No newline at end of file
diff --git a/research/decoder-floors-frontier-format/data/p104reps.json b/research/decoder-floors-frontier-format/data/p104reps.json
new file mode 100644
index 0000000000..f89d0b9d23
--- /dev/null
+++ b/research/decoder-floors-frontier-format/data/p104reps.json
@@ -0,0 +1 @@
+{"(767, ((0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1)))": [2, 3, 24, 25, 36, 37, 50, 51], "(801, ((0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1)))": [2, 3, 16, 17, 46, 47, 52, 53], "(759, ((0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1), (0, 0, 0, 0, 1, 1, 1, 1)))": [2, 24, 37, 51, 72, 87, 107, 116]}
\ No newline at end of file
diff --git a/research/decoder-floors-frontier-format/data/p111_lines.json b/research/decoder-floors-frontier-format/data/p111_lines.json
new file mode 100644
index 0000000000..39a47aad70
--- /dev/null
+++ b/research/decoder-floors-frontier-format/data/p111_lines.json
@@ -0,0 +1 @@
+{"note": "The 111 live lines of the P111 bit unit of PR #589's word (research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz, key 'lines'), in the doubled Hamming coordinates used by that word: dot(x,y)//2 is 2 on the diagonal and 0/+-1 off it. Source sha256 of the gz file is recorded in SOURCES.json.", "lines": [[2, 0, 0, 0, 0, 0, 0, 0], [0, 2, 0, 0, 0, 0, 0, 0], [0, 0, 2, 0, 0, 0, 0, 0], [0, 0, 0, 2, 0, 0, 0, 0], [0, 0, 0, 0, 2, 0, 0, 0], [0, 0, 0, 0, 0, 2, 0, 0], [0, 0, 0, 0, 0, 0, 2, 0], [0, 0, 0, 0, 0, 0, 0, 2], [0, 1, 1, 0, 1, 0, 0, 1], [0, 1, 1, 0, 1, 0, 0, -1], [0, 1, 1, 0, -1, 0, 0, -1], [0, 1, -1, 0, 1, 0, 0, 1], [0, 1, -1, 0, 1, 0, 0, -1], [0, 1, -1, 0, -1, 0, 0, 1], [1, 0, 1, 0, 1, 0, 1, 0], [1, 0, 1, 0, 1, 0, -1, 0], [1, 0, 1, 0, -1, 0, 1, 0], [1, 0, 1, 0, -1, 0, -1, 0], [1, 0, -1, 0, 1, 0, 1, 0], [1, 0, -1, 0, 1, 0, -1, 0], [1, 0, -1, 0, -1, 0, 1, 0], [1, 0, -1, 0, -1, 0, -1, 0], [1, 1, 0, 0, 0, 0, 1, 1], [1, 1, 0, 0, 0, 0, 1, -1], [1, 1, 0, 0, 0, 0, -1, 1], [1, 1, 0, 0, 0, 0, -1, -1], [1, -1, 0, 0, 0, 0, 1, 1], [1, -1, 0, 0, 0, 0, 1, -1], [1, -1, 0, 0, 0, 0, -1, 1], [1, -1, 0, 0, 0, 0, -1, -1], [1, 1, 0, 0, 1, 1, 0, 0], [1, 1, 0, 0, 1, -1, 0, 0], [1, 1, 0, 0, -1, 1, 0, 0], [1, 1, 0, 0, -1, -1, 0, 0], [1, -1, 0, 0, 1, 1, 0, 0], [1, -1, 0, 0, 1, -1, 0, 0], [1, -1, 0, 0, -1, 1, 0, 0], [1, -1, 0, 0, -1, -1, 0, 0], [1, 0, 1, 0, 0, 1, 0, 1], [1, 0, 1, 0, 0, 1, 0, -1], [1, 0, 1, 0, 0, -1, 0, 1], [1, 0, 1, 0, 0, -1, 0, -1], [1, 0, -1, 0, 0, 1, 0, 1], [1, 0, -1, 0, 0, 1, 0, -1], [1, 0, -1, 0, 0, -1, 0, 1], [1, 0, -1, 0, 0, -1, 0, -1], [0, 1, 1, 0, 0, 1, 1, 0], [0, 1, 1, 0, 0, 1, -1, 0], [0, 1, 1, 0, 0, -1, 1, 0], [0, 1, -1, 0, 0, 1, 1, 0], [0, 1, -1, 0, 0, -1, 1, 0], [0, 1, -1, 0, 0, -1, -1, 0], [0, 0, 0, 0, 1, 1, 1, -1], [0, 0, 0, 0, 1, 1, -1, 1], [0, 0, 0, 0, 1, 1, -1, -1], [0, 0, 0, 0, 1, -1, 1, 1], [0, 0, 0, 0, 1, -1, 1, -1], [0, 0, 0, 0, 1, -1, -1, 1], [0, 0, 0, 0, 1, -1, -1, -1], [1, 1, 1, 1, 0, 0, 0, 0], [1, 1, 1, -1, 0, 0, 0, 0], [1, 1, -1, -1, 0, 0, 0, 0], [1, -1, 1, 1, 0, 0, 0, 0], [1, -1, 1, -1, 0, 0, 0, 0], [1, -1, -1, 1, 0, 0, 0, 0], [1, -1, -1, -1, 0, 0, 0, 0], [1, 0, 0, 1, 1, 0, 0, -1], [1, 0, 0, 1, -1, 0, 0, 1], [1, 0, 0, 1, -1, 0, 0, -1], [1, 0, 0, -1, 1, 0, 0, 1], [1, 0, 0, -1, 1, 0, 0, -1], [1, 0, 0, -1, -1, 0, 0, 1], [1, 0, 0, -1, -1, 0, 0, -1], [0, 1, 0, 1, 1, 0, 1, 0], [0, 1, 0, 1, 1, 0, -1, 0], [0, 1, 0, 1, -1, 0, 1, 0], [0, 1, 0, 1, -1, 0, -1, 0], [0, 1, 0, -1, 1, 0, 1, 0], [0, 1, 0, -1, 1, 0, -1, 0], [0, 1, 0, -1, -1, 0, 1, 0], [0, 1, 0, -1, -1, 0, -1, 0], [0, 0, 1, 1, 0, 0, 1, 1], [0, 0, 1, 1, 0, 0, -1, 1], [0, 0, 1, 1, 0, 0, -1, -1], [0, 0, 1, -1, 0, 0, 1, 1], [0, 0, 1, -1, 0, 0, 1, -1], [0, 0, 1, -1, 0, 0, -1, 1], [0, 0, 1, -1, 0, 0, -1, -1], [0, 0, 1, 1, 1, 1, 0, 0], [0, 0, 1, 1, 1, -1, 0, 0], [0, 0, 1, 1, -1, 1, 0, 0], [0, 0, 1, 1, -1, -1, 0, 0], [0, 0, 1, -1, 1, 1, 0, 0], [0, 0, 1, -1, 1, -1, 0, 0], [0, 0, 1, -1, -1, 1, 0, 0], [0, 0, 1, -1, -1, -1, 0, 0], [0, 1, 0, 1, 0, 1, 0, 1], [0, 1, 0, 1, 0, 1, 0, -1], [0, 1, 0, 1, 0, -1, 0, 1], [0, 1, 0, 1, 0, -1, 0, -1], [0, 1, 0, -1, 0, 1, 0, 1], [0, 1, 0, -1, 0, 1, 0, -1], [0, 1, 0, -1, 0, -1, 0, 1], [1, 0, 0, 1, 0, 1, 1, 0], [1, 0, 0, 1, 0, 1, -1, 0], [1, 0, 0, 1, 0, -1, 1, 0], [1, 0, 0, 1, 0, -1, -1, 0], [1, 0, 0, -1, 0, 1, 1, 0], [1, 0, 0, -1, 0, 1, -1, 0], [1, 0, 0, -1, 0, -1, 1, 0], [1, 0, 0, -1, 0, -1, -1, 0]]}
\ No newline at end of file
diff --git a/research/decoder-floors-frontier-format/lib/frames.py b/research/decoder-floors-frontier-format/lib/frames.py
new file mode 100644
index 0000000000..150bab4c3c
--- /dev/null
+++ b/research/decoder-floors-frontier-format/lib/frames.py
@@ -0,0 +1,39 @@
+"""Frame-intersection certificate (Lemma 3.3) for the label classes of the dense pairing; exact bitmask computations."""
+import json, os, itertools
+from roots import *
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+
+def units():
+    """name -> (list of lines, T).  P112 = E8 minus a frame, P104 = E8 minus two frames, 'E7-frame' = E7 minus a 7-frame (data/p104_frames.json)."""
+    D = json.load(open(os.path.join(HERE, '..', 'data', 'p104_frames.json')))
+    F0, F1 = D['F0'], D['F1']
+    out = {n: UNITS[n] for n in ('D4', 'D5', 'D6', 'E6', 'E7', 'E8')}
+    out['P112'] = ([E8[i] for i in range(120) if i not in set(F0)], 8)
+    out['P104'] = ([E8[i] for i in range(120) if i not in set(F0) | set(F1)], 8)
+    adj = orth_graph(E7)
+    fr7 = next(c for c in maximal_cliques(adj) if popcount(c) == 7)
+    out['E7-frame'] = ([E7[i] for i in range(63) if not fr7 >> i & 1], 7)
+    return out
+
+def analyse(L, T):
+    v = len(L); Br = b0rows(L); basis = colspace_basis(Br); h = len(basis)
+    adj = orth_graph(L)
+    cl = list(maximal_cliques(adj)); alpha = max(popcount(c) for c in cl)
+    frames = [c for c in cl if popcount(c) == T]
+    allcl = span_vectors(basis)
+    has_frame = []; unc = []; cert_c = []
+    for co, w in allcl:
+        if any(f & ~w == 0 for f in frames): has_frame.append((co, w)); continue
+        Os = [f & ~w for f in frames]; ok = False
+        for E in frames:
+            ins = [o for o in Os if o & ~E == 0]
+            if ins:
+                x = ins[0]
+                for o in ins[1:]: x &= o
+                if x == 0: ok = True; break
+        (cert_c if ok else unc).append((co, w))
+    cos = set(c for c, _ in unc)
+    sub2 = any((a ^ b) in cos for a, b in itertools.combinations(sorted(cos), 2))
+    return dict(v=v, T=T, h=h, alpha=alpha, nframes=len(frames), frames=frames, classes=len(allcl), has_frame=has_frame, cert_c=cert_c,
+                unc=unc, sub2=sub2, basis=basis, Br=Br)
diff --git a/research/decoder-floors-frontier-format/lib/report.py b/research/decoder-floors-frontier-format/lib/report.py
new file mode 100644
index 0000000000..e8973c2fa2
--- /dev/null
+++ b/research/decoder-floors-frontier-format/lib/report.py
@@ -0,0 +1,16 @@
+"""One PASS/FAIL line per assertion, so verify.sh can count them.  A check script exits 1 if any of its lines failed."""
+import sys
+_fails = 0
+_n = 0
+
+
+def check(ident, cond, msg):
+    global _fails, _n
+    _n += 1
+    if not cond:
+        _fails += 1
+    print('%s %s  %s' % ('PASS' if cond else 'FAIL', ident, msg), flush=True)
+
+
+def finish():
+    sys.exit(1 if _fails else 0)
diff --git a/research/decoder-floors-frontier-format/lib/roots.py b/research/decoder-floors-frontier-format/lib/roots.py
new file mode 100644
index 0000000000..bfddda2d20
--- /dev/null
+++ b/research/decoder-floors-frontier-format/lib/roots.py
@@ -0,0 +1,148 @@
+"""Root-system line sets and exact F2 / clique helpers (standard library only).
+Lines are given by integer vectors: E8 with doubled coordinates (so the inner product is 4x the usual one: roots have norm 8), D_n with norm 2.
+Only zero patterns of the Gram matrix are used by the F2 / frame checks; the decoder checks (frame120, Lemma OC) use exact Fractions with the
+proper scale (the E8 helpers below return the 'real' scaling through `real_dot`)."""
+import itertools
+from fractions import Fraction as Fr
+
+def dot(a, b): return sum(x * y for x, y in zip(a, b))
+
+def e8_roots2():
+    """E8 roots with coordinates doubled: +-2e_i +-2e_j and (+-1)^8 with an even number of minus signs (240 vectors)."""
+    R = []
+    for i, j in itertools.combinations(range(8), 2):
+        for si in (2, -2):
+            for sj in (2, -2):
+                r = [0] * 8; r[i] = si; r[j] = sj; R.append(tuple(r))
+    for s in itertools.product((1, -1), repeat=8):
+        if s.count(-1) % 2 == 0: R.append(tuple(s))
+    return R
+
+def dn_roots(n):
+    R = []
+    for i, j in itertools.combinations(range(n), 2):
+        for si in (1, -1):
+            for sj in (1, -1):
+                r = [0] * n; r[i] = si; r[j] = sj; R.append(tuple(r))
+    return R
+
+def lines(R):
+    """one representative per +-pair, in first-occurrence order"""
+    seen = set(); L = []
+    for r in R:
+        if tuple(-x for x in r) in seen: continue
+        seen.add(r); L.append(r)
+    return L
+
+def orth_sub(L, vs): return [r for r in L if all(dot(r, x) == 0 for x in vs)]
+
+E8 = lines(e8_roots2())                       # 120 lines, doubled coordinates
+_r0 = E8[0]; _r1 = next(r for r in E8 if dot(r, _r0) in (4, -4))
+E7 = orth_sub(E8, [_r0])                      # 63 lines
+E6 = orth_sub(E8, [_r0, _r1])                 # 36 lines
+D4 = lines(dn_roots(4)); D5 = lines(dn_roots(5)); D6 = lines(dn_roots(6))
+UNITS = {'D4': (D4, 4), 'D5': (D5, 5), 'D6': (D6, 6), 'E6': (E6, 6), 'E7': (E7, 7), 'E8': (E8, 8)}
+
+def gram(L): return [[dot(a, b) for b in L] for a in L]
+
+def b0rows(L):
+    """dense pairing B = J + Abar as row bitmasks: B_ts = 1 iff t = s or the lines t, s are orthogonal"""
+    G = gram(L); v = len(L)
+    return [sum(1 << s for s in range(v) if s == t or G[t][s] == 0) for t in range(v)]
+
+def rank_f2(rows):
+    basis = []
+    for r in rows:
+        x = r
+        for b in basis: x = min(x, x ^ b)
+        if x: basis.append(x)
+    return len(basis)
+
+def blk(Brows, R, A):
+    """rank over F2 of the submatrix B[R, A]"""
+    return rank_f2([sum(1 << i for i, s in enumerate(A) if Brows[t] >> s & 1) for t in R])
+
+def colspace_basis(rows):
+    """reduced echelon basis (bitmasks over the column index) of the span of the given rows"""
+    basis = []; piv = []
+    for r in rows:
+        x = r
+        for b, p in zip(basis, piv):
+            if x >> p & 1: x ^= b
+        if x:
+            p = x.bit_length() - 1
+            for i in range(len(basis)):
+                if basis[i] >> p & 1: basis[i] ^= x
+            basis.append(x); piv.append(p)
+    return basis
+
+def span_vectors(basis):
+    """all nonzero vectors of the F2 span as (coefficient mask, vector) pairs"""
+    h = len(basis); out = []
+    for co in range(1, 1 << h):
+        w = 0
+        for i in range(h):
+            if co >> i & 1: w ^= basis[i]
+        out.append((co, w))
+    return out
+
+def orth_graph(L):
+    G = gram(L); v = len(L)
+    return [sum(1 << s for s in range(v) if s != t and G[t][s] == 0) for t in range(v)]
+
+def maximal_cliques(adj):
+    """Bron-Kerbosch with pivoting on bitmask adjacency; yields clique bitmasks"""
+    def bk(R, P, X):
+        if not P and not X:
+            yield R; return
+        # pivot: vertex of P|X maximising |P & N(u)|
+        best = -1; piv = 0; PX = P | X; m = PX
+        while m:
+            low = m & -m; i = low.bit_length() - 1; m ^= low
+            c = bin(P & adj[i]).count('1')
+            if c > best: best = c; piv = i
+        cand = P & ~adj[piv]
+        while cand:
+            low = cand & -cand; i = low.bit_length() - 1; cand ^= low
+            yield from bk(R | low, P & adj[i], X & adj[i])
+            P &= ~low; X |= low
+    yield from bk(0, (1 << len(adj)) - 1, 0)
+
+def popcount(x): return bin(x).count('1')
+def bits(x):
+    out = []
+    while x:
+        low = x & -x; out.append(low.bit_length() - 1); x ^= low
+    return out
+
+# Fraction linear algebra
+def rank_q(rows):
+    M = [[Fr(x) for x in r] for r in rows]; r = 0
+    if not M: return 0
+    for c in range(len(M[0])):
+        piv = next((i for i in range(r, len(M)) if M[i][c] != 0), None)
+        if piv is None: continue
+        M[r], M[piv] = M[piv], M[r]; pv = M[r][c]; M[r] = [x / pv for x in M[r]]
+        for i in range(len(M)):
+            if i != r and M[i][c] != 0:
+                f = M[i][c]; M[i] = [x - f * y for x, y in zip(M[i], M[r])]
+        r += 1
+    return r
+
+def nullspace_q(rows, ncols):
+    """basis of {x : rows . x = 0} over Q"""
+    M = [[Fr(x) for x in r] for r in rows]; pivs = []; r = 0
+    for c in range(ncols):
+        piv = next((i for i in range(r, len(M)) if M[i][c] != 0), None)
+        if piv is None: continue
+        M[r], M[piv] = M[piv], M[r]; pv = M[r][c]; M[r] = [x / pv for x in M[r]]
+        for i in range(len(M)):
+            if i != r and M[i][c] != 0:
+                f = M[i][c]; M[i] = [x - f * y for x, y in zip(M[i], M[r])]
+        pivs.append(c); r += 1
+    free = [c for c in range(ncols) if c not in pivs]; out = []
+    for f in free:
+        x = [Fr(0)] * ncols; x[f] = Fr(1)
+        for i, c in enumerate(pivs): x[c] = -M[i][f]
+        out.append(x)
+    return out
diff --git a/research/decoder-floors-frontier-format/lib/satgen.py b/research/decoder-floors-frontier-format/lib/satgen.py
new file mode 100644
index 0000000000..21461b4137
--- /dev/null
+++ b/research/decoder-floors-frontier-format/lib/satgen.py
@@ -0,0 +1,86 @@
+"""DIMACS generators for the F2 low-rank (fitting-minrank) instances.  Standard library only.
+A matrix  X = U V^T  over F2 of rank <= r is encoded with U[t][i], V[s][i] variables,  X_ts = XOR_i (U[t][i] AND V[s][i])  (Tseitin chain).
+Symmetry breaking: if C is a set of rows/columns with X[C,C] = I (a clique of non-orthogonal lines for the fitting problem B, a clique of
+orthogonal lines for the Gamma problem), then U[C] has rank |C|, and applying a change of basis of F2^r we may fix U[C] = [I_|C| | 0]
+(and V[C] = [I | 0] too when r = |C|).  Any choice of C is valid."""
+import itertools
+from roots import *
+
+class CNF:
+    def __init__(self): self.nv = 0; self.cls = []
+    def new(self): self.nv += 1; return self.nv
+    def lowrank_entry(self, Urow, Vrow, val):
+        """add: XOR_i (Urow[i] AND Vrow[i]) == val  (val in {0,1}), or, if val is a variable index, == that variable"""
+        r = len(Urow); ands = []
+        for i in range(r):
+            a = self.new(); self.cls.extend([[-a, Urow[i]], [-a, Vrow[i]], [a, -Urow[i], -Vrow[i]]]); ands.append(a)
+        cur = ands[0]
+        for l in ands[1:]:
+            y = self.new(); self.cls.extend([[-y, cur, l], [-y, -cur, -l], [y, -cur, l], [y, cur, -l]]); cur = y
+        if val in (0, 1): self.cls.append([cur] if val else [-cur])
+        else: self.cls.extend([[-cur, val], [cur, -val]])
+    def dimacs(self):
+        return "p cnf %d %d\n" % (self.nv, len(self.cls)) + "".join(" ".join(map(str, c)) + " 0\n" for c in self.cls)
+
+def clique_in(adj, universe):
+    """a (deterministic) large clique of the graph adj inside the bitmask `universe`, as a sorted list (any clique is a valid symmetry-breaking choice)"""
+    adj2 = [a & universe for a in adj]; best = 0; bs = -1
+    for c in maximal_cliques(adj2):
+        if not (c & universe) == c: continue
+        k = popcount(c)
+        if k > bs or (k == bs and c < best): best, bs = c, k
+    return bits(best)
+
+def nonorth_graph(L):
+    G = gram(L); v = len(L)
+    return [sum(1 << s for s in range(v) if s != t and G[t][s] != 0) for t in range(v)]
+
+def fitting_cnf(L, R, A, r, clique, fixV=False):
+    """exists X = U V^T over F2 of rank <= r on rows R, columns A with X_tt = 1, X_ts = 0 for non-orthogonal t != s, entries on orthogonal
+    pairs free?  (the fitting minrank of the block B[R,A] over all admissible B).  clique: list of lines in R cap A, pairwise non-orthogonal."""
+    G = gram(L); c = CNF()
+    U = {t: [c.new() for _ in range(r)] for t in R}; V = {s: [c.new() for _ in range(r)] for s in A}
+    for t in R:
+        for s in A:
+            if t != s and G[t][s] == 0: continue
+            c.lowrank_entry(U[t], V[s], 1 if t == s else 0)
+    for k, t in enumerate(clique[:r]):
+        for i in range(r): c.cls.append([U[t][i]] if i == k else [-U[t][i]])
+        if fixV:                         # only valid when r == |clique|: X[C,C] = I = U[C] V[C]^T with U[C] = I forces V[C] = I
+            assert r == len(clique)
+            for i in range(r): c.cls.append([V[t][i]] if i == k else [-V[t][i]])
+    c.U, c.V = U, V
+    return c
+
+def gamma_cnf(L, r, clique):
+    """exists N = U V^T over F2 of rank <= r on all lines with N_tt = 1 and N_ts = 0 for ORTHOGONAL t != s (entries on non-orthogonal pairs free);
+    clique: pairwise orthogonal lines (N[C,C] = I)."""
+    G = gram(L); v = len(L); c = CNF()
+    U = [[c.new() for _ in range(r)] for _ in range(v)]; V = [[c.new() for _ in range(r)] for _ in range(v)]
+    for t in range(v):
+        for s in range(v):
+            if t != s and G[t][s] != 0: continue
+            c.lowrank_entry(U[t], V[s], 1 if t == s else 0)
+    for k, t in enumerate(clique[:r]):
+        for i in range(r): c.cls.append([U[t][i]] if i == k else [-U[t][i]])
+    c.U, c.V = U, V
+    return c
+
+def joint_cnf(L, terms, caps):
+    """exists an admissible B (B_tt = 1, B_ts = 0 on non-orthogonal pairs, free variables on orthogonal pairs, SHARED by all terms) with
+    rank B[R_j, A_j] <= caps[j] for every j.  Returns (cnf, bvars)."""
+    G = gram(L); v = len(L); c = CNF(); bvar = {}
+    nog = nonorth_graph(L)
+    for (R, A), r in zip(terms, caps):
+        D = sorted(set(R) & set(A)); C = clique_in(nog, sum(1 << t for t in D)) if D else []
+        U = {t: [c.new() for _ in range(r)] for t in R}; V = {s: [c.new() for _ in range(r)] for s in A}
+        for k, t in enumerate(C[:r]):
+            for i in range(r): c.cls.append([U[t][i]] if i == k else [-U[t][i]])
+        for t in R:
+            for s in A:
+                if t == s: c.lowrank_entry(U[t], V[s], 1)
+                elif G[t][s] != 0: c.lowrank_entry(U[t], V[s], 0)
+                else:
+                    if (t, s) not in bvar: bvar[t, s] = c.new()
+                    c.lowrank_entry(U[t], V[s], bvar[t, s])
+    return c, bvar
diff --git a/research/decoder-floors-frontier-format/lib/solve.py b/research/decoder-floors-frontier-format/lib/solve.py
new file mode 100644
index 0000000000..ea6aebae16
--- /dev/null
+++ b/research/decoder-floors-frontier-format/lib/solve.py
@@ -0,0 +1,19 @@
+"""Thin wrappers around kissat and drat-trim (both optional).  Never uses CaDiCaL."""
+import os, shutil, subprocess
+def find(env, name):
+    p = os.environ.get(env) or shutil.which(name)
+    return p if p and os.path.exists(p) else None
+def kissat(): return find('KISSAT', 'kissat')
+def drat_trim(): return find('DRAT_TRIM', 'drat-trim')
+def run_kissat(cnf, proof=None, tmo=900):
+    """returns (status 'SAT'|'UNSAT'|'UNKNOWN', set of true variables or None)"""
+    cmd = [kissat(), '-q'] + ([cnf, proof] if proof else [cnf])
+    try: o = subprocess.run(cmd, capture_output=True, text=True, timeout=tmo).stdout
+    except subprocess.TimeoutExpired: return 'UNKNOWN', None
+    if 'UNSATISFIABLE' in o: return 'UNSAT', None
+    if 'SATISFIABLE' in o:
+        return 'SAT', set(int(x) for l in o.splitlines() if l.startswith('v') for x in l.split()[1:] if int(x) > 0)
+    return 'UNKNOWN', None
+def run_drat(cnf, proof, tmo=3000):
+    d = subprocess.run([drat_trim(), cnf, proof, '-t', str(tmo)], capture_output=True, text=True)
+    return 's VERIFIED' in d.stdout
diff --git a/research/decoder-floors-frontier-format/lib/supprop.py b/research/decoder-floors-frontier-format/lib/supprop.py
new file mode 100644
index 0000000000..f8a24f3d61
--- /dev/null
+++ b/research/decoder-floors-frontier-format/lib/supprop.py
@@ -0,0 +1,32 @@
+"""Lemma 1.1 (support propagation) machinery shared by c2 and c4; standard library only."""
+import os, sys
+sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
+from units import *
+
+def setup(L, T):
+    v = len(L); G = gram(L); adj = orth_graph(L)
+    frames = [c for c in maximal_cliques(adj) if popcount(c) == T]
+    nbar = [sum(1 << s for s in range(v) if G[t][s] != 0) for t in range(v)]
+    return v, frames, nbar
+
+def propagate(O, frames, nbar):
+    S = [E & ~O for E in frames]
+    while True:
+        Wg = -1
+        for s in S:
+            w = 0; x = s
+            while x:
+                b = x & -x; w |= nbar[b.bit_length() - 1]; x ^= b
+            Wg &= w
+        S2 = [s & Wg for s in S]
+        if S2 == S: return S
+        S = S2
+
+def census(L, T):
+    v, frames, nbar = setup(L, T); Br = b0rows(L); basis = colspace_basis(Br); h = len(basis)
+    classes = span_vectors(basis); unc = []
+    for co, w in classes:
+        S = propagate(w, frames, nbar)
+        if min(popcount(s) for s in S) > 0: unc.append((co, w))
+    return dict(v=v, h=h, T=T, nframes=len(frames), nclasses=len(classes), unc=unc, Br=Br)
+
diff --git a/research/decoder-floors-frontier-format/lib/units.py b/research/decoder-floors-frontier-format/lib/units.py
new file mode 100644
index 0000000000..e52aa5ab13
--- /dev/null
+++ b/research/decoder-floors-frontier-format/lib/units.py
@@ -0,0 +1,38 @@
+"""The E8-family units used throughout this package (standard library only; built on lib/roots.py).
+E8 = 120 lines in doubled coordinates (lib/roots.py order).  F0 = the frame {2e_{2k} +- 2e_{2k+1}} (k = 0..3), the removed frame of P112.
+P112 = E8 minus F0 (112 lines).  P104 = P112 minus a second frame F1 disjoint from F0 (104 lines).  H4 = the F1 of #968 (data/h4_F1.json).
+E7 = lines orthogonal to line 0 (63); E6 = lines orthogonal to line 0 and to the first line non-orthogonal to line 0 (36)."""
+import json, os
+from roots import *
+
+_UH = os.path.dirname(os.path.abspath(__file__))
+DATA = os.path.join(_UH, '..', 'data')
+IDX = {r: i for i, r in enumerate(E8)}
+def idx(v):
+    v = tuple(v); w = tuple(-x for x in v)
+    return IDX[v] if v in IDX else IDX[w]
+F0 = []
+for _k in range(4):
+    for _s in (2, -2):
+        _v = [0] * 8; _v[2 * _k] = 2; _v[2 * _k + 1] = _s; F0.append(idx(_v))
+F0 = sorted(F0)
+H4F1 = sorted(idx(v) for v in json.load(open(os.path.join(DATA, 'h4_F1.json'))))
+GE8 = gram(E8)
+def orth(t, s): return GE8[t][s] == 0
+def sub(ix): return [E8[i] for i in ix]
+P112_IDX = [i for i in range(120) if i not in set(F0)]
+def p104_idx(F1): return [i for i in P112_IDX if i not in set(F1)]
+def p104_reps():
+    d = json.load(open(os.path.join(DATA, 'p104reps.json')))
+    return {int(k[1:k.index(',')]): v for k, v in d.items()}      # frame count (759, 767, 801) -> F1 as E8 indices
+_b = next(t for t in range(1, 120) if GE8[t][0] != 0)
+E7_IDX = [t for t in range(120) if GE8[t][0] == 0 and t != 0]
+E6_IDX = [t for t in range(120) if GE8[t][0] == 0 and GE8[t][_b] == 0 and t not in (0, _b)]
+def unit_idx(name):
+    if name == 'E8': return list(range(120))
+    if name == 'P112': return list(P112_IDX)
+    if name == 'P104H4': return p104_idx(H4F1)
+    if name.startswith('P104_'): return p104_idx(p104_reps()[int(name[5:])])
+    if name == 'E7': return list(E7_IDX)
+    if name == 'E6': return list(E6_IDX)
+    raise KeyError(name)
diff --git a/research/decoder-floors-frontier-format/requirements.txt b/research/decoder-floors-frontier-format/requirements.txt
new file mode 100644
index 0000000000..dee35c3194
--- /dev/null
+++ b/research/decoder-floors-frontier-format/requirements.txt
@@ -0,0 +1,2 @@
+# Tested set (Python 3.14.7).  Standard library only (fractions, itertools, hashlib, json, lzma, subprocess, random); no third-party packages.
+# Optional, for the DRAT re-check and for re-solving: drat-trim (set DRAT_TRIM=/path) and kissat 4.0.4 (set KISSAT=/path).  Never CaDiCaL.
diff --git a/research/decoder-floors-frontier-format/sat/hitting.py b/research/decoder-floors-frontier-format/sat/hitting.py
new file mode 100644
index 0000000000..1ca2e9a413
--- /dev/null
+++ b/research/decoder-floors-frontier-format/sat/hitting.py
@@ -0,0 +1,52 @@
+"""C4.1 (NEWWORD c4): multi-unit puncture savings on the P112 coordinate term under ANY admissible B.  Standard library only.
+R = N(f) (56 live lines non-orthogonal to a removed root f).  A kept clique C of pairwise non-orthogonal lines has B[C,C] = I for every admissible B,
+so a puncture D of R (lines deleted from the support) with rank B[R\\D, R\\D] <= 8 - s keeps no (9 - s)-clique: D must hit every (9 - s)-clique of R.
+f(s) = min |D| over hitting sets; 'z-1 infeasible' <=> UNSAT of 'hit all k-cliques with at most z-1 lines' (k = 9 - s), encoded with a sequential counter.
+For k = 3 (s = 6) the dual form is used: no triangle-free kept set of size `keep`.   CNF text is a deterministic function of (k, z)."""
+import os, sys
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, os.path.join(HERE, '..', 'lib'))
+from units import *
+
+def region():
+    L = sub(P112_IDX); f = F0[0]
+    R = [t for t in range(len(L)) if dot(L[t], E8[f]) != 0]
+    return L, R
+def cliques(L, R, k):
+    NO = lambda a, b: dot(L[a], L[b]) != 0
+    out = []
+    def ext(cur, cand):
+        if len(cur) == k: out.append(cur); return
+        for i, c in enumerate(cand): ext(cur + [c], [d for d in cand[i + 1:] if NO(c, d)])
+    ext([], R); return out
+
+def seqcounter_atmost(lits, bound, top):
+    """Sinz sequential counter: at most `bound` of lits true; returns (clauses, new top)"""
+    n = len(lits); s = [[0] * (bound + 1) for _ in range(n)]; cl = []
+    for i in range(n):
+        for j in range(1, bound + 1): top += 1; s[i][j] = top
+    cl.append([-lits[0], s[0][1]])
+    for j in range(2, bound + 1): cl.append([-s[0][j]])
+    for i in range(1, n):
+        cl.append([-lits[i], s[i][1]]); cl.append([-s[i - 1][1], s[i][1]])
+        for j in range(2, bound + 1):
+            cl.append([-lits[i], -s[i - 1][j - 1], s[i][j]]); cl.append([-s[i - 1][j], s[i][j]])
+        cl.append([-lits[i], -s[i - 1][bound]])
+    return cl, top
+
+def hit_cnf(k, z):
+    """UNSAT  <=>  no set of at most z lines of R meets every k-clique"""
+    L, R = region(); idx = {t: i + 1 for i, t in enumerate(R)}
+    C = cliques(L, R, k); cl = [[idx[t] for t in c] for c in C]
+    card, top = seqcounter_atmost([idx[t] for t in R], z, len(R)); cl += card
+    return top, cl, len(C)
+
+def tri_cnf(keep):
+    """UNSAT <=> no triangle-free subset of R (no three pairwise non-orthogonal lines) has `keep` lines"""
+    L, R = region(); idx = {t: i + 1 for i, t in enumerate(R)}
+    tris = cliques(L, R, 3); cl = [[-idx[a], -idx[b], -idx[c]] for a, b, c in tris]
+    # at least `keep` kept = at most len(R)-keep dropped; encode on negated literals
+    card, top = seqcounter_atmost([-idx[t] for t in R], len(R) - keep, len(R)); cl += card
+    return top, cl, len(tris)
+
+def dimacs(nv, cl): return "p cnf %d %d\n" % (nv, len(cl)) + "".join(" ".join(map(str, c)) + " 0\n" for c in cl)
diff --git a/research/decoder-floors-frontier-format/sat/misc.py b/research/decoder-floors-frontier-format/sat/misc.py
new file mode 100644
index 0000000000..5bd9f8e85d
--- /dev/null
+++ b/research/decoder-floors-frontier-format/sat/misc.py
@@ -0,0 +1,51 @@
+"""Registry of the smaller SAT instances: EDGE E1a (coordinate block N(f) of P112 has fitting minrank 8 for every admissible B) and the C4.1 clique-hitting
+bounds on punctures.  Standard library only; DIMACS text is a deterministic function of the name."""
+import os, sys, functools
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, os.path.join(HERE, '..', 'lib'))
+from units import *
+from satgen import fitting_cnf, clique_in, nonorth_graph
+import hitting as H
+
+@functools.lru_cache(maxsize=None)
+def edge_instance(i, r):
+    """rank <= r admissible B on the block B[N(f_i), N(f_i)] of P112 (f_i = i-th removed root); gauge clique = largest non-orthogonal clique in N(f_i)"""
+    L = sub(P112_IDX); f = F0[i]
+    N = [t for t in range(len(L)) if dot(L[t], E8[f]) != 0]
+    adj = nonorth_graph(L); C = clique_in(adj, sum(1 << t for t in N))
+    return fitting_cnf(L, N, N, r, C[:r], fixV=False), N, C
+
+def registry():
+    R = {}
+    for i in range(8): R['edge_N%d_r7' % i] = dict(expect='UNSAT', slow=False)
+    R['edge_N0_r8'] = dict(expect='SAT', slow=False)
+    R['hit_k7_z13'] = dict(expect='UNSAT', slow=False); R['hit_k7_z14'] = dict(expect='SAT', slow=False)
+    R['tri_keep11'] = dict(expect='UNSAT', slow=False); R['tri_keep10'] = dict(expect='SAT', slow=False)
+    for k, z in ((6, 22), (5, 31), (4, 37)):
+        R['hit_k%d_z%d' % (k, z)] = dict(expect='UNSAT', slow=True)
+    return R
+
+def dimacs_of(name):
+    if name.startswith('edge_N'):
+        i = int(name[6]); r = int(name.split('_r')[1]); return edge_instance(i, r)[0].dimacs()
+    if name.startswith('hit_k'):
+        k, z = name[5:].split('_z'); nv, cl, _ = H.hit_cnf(int(k), int(z)); return H.dimacs(nv, cl)
+    if name.startswith('tri_keep'):
+        nv, cl, _ = H.tri_cnf(int(name[8:])); return H.dimacs(nv, cl)
+    raise KeyError(name)
+
+def check_model(name, pos):
+    """SAT models: edge_N0_r8 -> decode U,V and check B = U V^T is admissible on the block; hit_*: the hitting set of the model hits every clique and has <= z lines;
+    tri_keep10: the kept set is triangle-free of size >= 10."""
+    if name.startswith('edge_N'):
+        i = int(name[6]); r = int(name.split('_r')[1]); c, N, C = edge_instance(i, r); L = sub(P112_IDX)
+        ent = lambda t, s: sum(((u in pos) & (w in pos)) for u, w in zip(c.U[t], c.V[s])) & 1
+        return all(ent(t, t) == 1 for t in N) and all(ent(t, s) == 0 for t in N for s in N if t != s and dot(L[t], L[s]) != 0)
+    L, R = H.region(); idx = {t: j + 1 for j, t in enumerate(R)}
+    if name.startswith('hit_k'):
+        k, z = name[5:].split('_z'); k, z = int(k), int(z); D = [t for t in R if idx[t] in pos]
+        return len(D) <= z and all(any(t in D for t in cl) for cl in H.cliques(L, R, k))
+    if name.startswith('tri_keep'):
+        keep = int(name[8:]); K = [t for t in R if idx[t] in pos]
+        return len(K) >= keep and not any(all(t in K for t in tr) for tr in H.cliques(L, R, 3))
+    raise KeyError(name)
diff --git a/research/decoder-floors-frontier-format/sat/mkmisc.py b/research/decoder-floors-frontier-format/sat/mkmisc.py
new file mode 100644
index 0000000000..09899adc2d
--- /dev/null
+++ b/research/decoder-floors-frontier-format/sat/mkmisc.py
@@ -0,0 +1,23 @@
+"""Author tool for sat/misc.py (see mkresults.py).  usage: python3 mkmisc.py OUTDIR [--slow] [name ...]  -> JSON lines on stdout.
+Instances flagged slow are solved WITHOUT a proof (UNSAT recorded as 'UNSAT (no proof)')."""
+import sys, os, json, time, lzma, shutil, hashlib
+SATDIR = os.path.dirname(os.path.abspath(__file__)); HERE = SATDIR
+sys.path.insert(0, os.path.join(HERE, '..', 'lib'))
+from misc import *
+from solve import *
+args = [a for a in sys.argv[1:] if not a.startswith('--')]; out = args[0]; os.makedirs(out, exist_ok=True)
+R = registry(); names = args[1:] or [n for n in R if not R[n]['slow'] or '--slow' in sys.argv]
+SHIP = set(os.environ.get('SHIP', '').split(','))
+for nm in names:
+    t0 = time.time(); d = dimacs_of(nm); cnf = os.path.join(out, nm + '.cnf'); open(cnf, 'w').write(d); pr = os.path.join(out, nm + '.drat')
+    slow = R[nm]['slow']; st, model = run_kissat(cnf, None if slow else pr, tmo=3000)
+    row = dict(name=nm, expect=R[nm]['expect'], slow=slow, cnf_sha256=hashlib.sha256(d.encode()).hexdigest(), status=st)
+    if st == 'UNSAT' and not slow:
+        row['drat'] = 'VERIFIED' if run_drat(cnf, pr) else 'FAILED'; row['proof_bytes'] = os.path.getsize(pr)
+        if nm in SHIP:
+            os.makedirs(os.path.join(SATDIR, 'proofs'), exist_ok=True)
+            with open(pr, 'rb') as f, lzma.open(os.path.join(SATDIR, 'proofs', nm + '.drat.xz'), 'wb', preset=9) as g: shutil.copyfileobj(f, g)
+    elif st == 'SAT': row['model_ok'] = check_model(nm, model)
+    for p in (cnf, pr):
+        if os.path.exists(p): os.remove(p)
+    row['secs'] = round(time.time() - t0, 1); print(json.dumps(row), flush=True)
diff --git a/research/decoder-floors-frontier-format/sat/mkresults.py b/research/decoder-floors-frontier-format/sat/mkresults.py
new file mode 100644
index 0000000000..76a61a660f
--- /dev/null
+++ b/research/decoder-floors-frontier-format/sat/mkresults.py
@@ -0,0 +1,27 @@
+"""Author tool: solve every instance of the registry (kissat 4.0.4, binary DRAT proof), verify UNSAT proofs with drat-trim, decode SAT models,
+and write results.jsonl (one JSON line per instance).  Optionally xz-ships selected proofs into proofs/.
+usage: python3 mkresults.py OUTDIR [name ...]"""
+import sys, os, json, time, lzma, shutil
+SATDIR = os.path.dirname(os.path.abspath(__file__)); HERE = SATDIR
+sys.path.insert(0, os.path.join(HERE, '..', 'lib'))
+from rigid import *
+from solve import *
+SHIP = set(os.environ.get('SHIP', '').split(','))
+out = sys.argv[1]; os.makedirs(out, exist_ok=True)
+R = registry(); names = sys.argv[2:] or list(R)
+rows = []
+for nm in names:
+    t0 = time.time(); nv, cls, info, *_ = build_named(nm); d = dimacs(nv, cls); h = sha(d)
+    cnf = os.path.join(out, nm + '.cnf'); open(cnf, 'w').write(d); pr = os.path.join(out, nm + '.drat')
+    st, model = run_kissat(cnf, pr)
+    row = dict(name=nm, unit=R[nm]['unit'], h=R[nm]['h'], sym=R[nm]['sym'], mode=R[nm]['mode'], expect=R[nm]['expect'], nv=nv, ncls=len(cls),
+               orth=info['orth'], gauge=R[nm]['S'], cnf_sha256=h, status=st)
+    if st == 'UNSAT':
+        row['drat'] = 'VERIFIED' if run_drat(cnf, pr) else 'FAILED'; row['proof_bytes'] = os.path.getsize(pr)
+        if nm in SHIP:
+            os.makedirs(os.path.join(SATDIR, 'proofs'), exist_ok=True)
+            with open(pr, 'rb') as f, lzma.open(os.path.join(SATDIR, 'proofs', nm + '.drat.xz'), 'wb', preset=9) as g: shutil.copyfileobj(f, g)
+    elif st == 'SAT':
+        fit, z, n = decode_model(nm, model); row.update(model_fitting=fit, orth_zero=z, orth_total=n)
+    os.remove(pr) if os.path.exists(pr) else None; os.remove(cnf)
+    row['secs'] = round(time.time() - t0, 1); rows.append(row); print(json.dumps(row), flush=True)
diff --git a/research/decoder-floors-frontier-format/sat/proofs/E8_sym_h9_alt.drat.xz b/research/decoder-floors-frontier-format/sat/proofs/E8_sym_h9_alt.drat.xz
new file mode 100644
index 0000000000..6daca3d1b3
Binary files /dev/null and b/research/decoder-floors-frontier-format/sat/proofs/E8_sym_h9_alt.drat.xz differ
diff --git a/research/decoder-floors-frontier-format/sat/proofs/P104H4_sym_h9_alt.drat.xz b/research/decoder-floors-frontier-format/sat/proofs/P104H4_sym_h9_alt.drat.xz
new file mode 100644
index 0000000000..686c3ac87b
Binary files /dev/null and b/research/decoder-floors-frontier-format/sat/proofs/P104H4_sym_h9_alt.drat.xz differ
diff --git a/research/decoder-floors-frontier-format/sat/proofs/P111_sym_h9_alt.drat.xz b/research/decoder-floors-frontier-format/sat/proofs/P111_sym_h9_alt.drat.xz
new file mode 100644
index 0000000000..9ed2748547
Binary files /dev/null and b/research/decoder-floors-frontier-format/sat/proofs/P111_sym_h9_alt.drat.xz differ
diff --git a/research/decoder-floors-frontier-format/sat/proofs/P112_sym_h9_alt.drat.xz b/research/decoder-floors-frontier-format/sat/proofs/P112_sym_h9_alt.drat.xz
new file mode 100644
index 0000000000..5172614316
Binary files /dev/null and b/research/decoder-floors-frontier-format/sat/proofs/P112_sym_h9_alt.drat.xz differ
diff --git a/research/decoder-floors-frontier-format/sat/proofs/edge_N0_r7.drat.xz b/research/decoder-floors-frontier-format/sat/proofs/edge_N0_r7.drat.xz
new file mode 100644
index 0000000000..71cf2223e3
Binary files /dev/null and b/research/decoder-floors-frontier-format/sat/proofs/edge_N0_r7.drat.xz differ
diff --git a/research/decoder-floors-frontier-format/sat/proofs/tri_keep11.drat.xz b/research/decoder-floors-frontier-format/sat/proofs/tri_keep11.drat.xz
new file mode 100644
index 0000000000..1643881a53
Binary files /dev/null and b/research/decoder-floors-frontier-format/sat/proofs/tri_keep11.drat.xz differ
diff --git a/research/decoder-floors-frontier-format/sat/results.jsonl b/research/decoder-floors-frontier-format/sat/results.jsonl
new file mode 100644
index 0000000000..ca60b61573
--- /dev/null
+++ b/research/decoder-floors-frontier-format/sat/results.jsonl
@@ -0,0 +1,30 @@
+{"name": "P112_sym_h9_alt", "unit": "P112", "h": 9, "sym": true, "mode": "alt", "expect": "UNSAT", "nv": 135728, "ncls": 474121, "orth": 3304, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "b7506887d226c52154dc8fff7fa8078c611536b203cd283d5801689131ab4f8a", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 10255882}
+{"name": "P112_gen_h9_alt", "unit": "P112", "h": 9, "sym": false, "mode": "alt", "expect": "UNSAT", "nv": 199960, "ncls": 693169, "orth": 6608, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "84964b1317bacaa45a15f47d2d31a08922d9888bd4e6093a0418ca2b2a3de5c2", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 31214571}
+{"name": "E8_sym_h9_alt", "unit": "E8", "h": 9, "sym": true, "mode": "alt", "expect": "UNSAT", "nv": 157556, "ncls": 550565, "orth": 3780, "gauge": [0, 2, 4, 6, 8, 10, 12, 56], "cnf_sha256": "923938f157e5747dda4e8d22fc86660d6cf6b996e4686a9ea0a7faa08f9cbfb3", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 11807441}
+{"name": "E8_gen_h9_alt", "unit": "E8", "h": 9, "sym": false, "mode": "alt", "expect": "UNSAT", "nv": 230568, "ncls": 799801, "orth": 7560, "gauge": [0, 2, 4, 6, 8, 10, 12, 56], "cnf_sha256": "f456c4fbb24800ec0fb3c9481de0fe7716757585689dae73fa2430d9c1fc1e61", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 36473900}
+{"name": "P104H4_sym_h9_alt", "unit": "P104H4", "h": 9, "sym": true, "mode": "alt", "expect": "UNSAT", "nv": 115532, "ncls": 403405, "orth": 2860, "gauge": [8, 20, 30, 38, 56, 57, 60, 61], "cnf_sha256": "17ff8b7950788c8e1cfdfe03097585819acdae98d9a7336a4ce8916f31b916b3", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 8687969}
+{"name": "P104H4_gen_h9_alt", "unit": "P104H4", "h": 9, "sym": false, "mode": "alt", "expect": "UNSAT", "nv": 171528, "ncls": 594153, "orth": 5720, "gauge": [8, 20, 30, 38, 56, 57, 60, 61], "cnf_sha256": "c9f2c86f751c140b322e07395388604f326e05547c7ff0082e6a91ddfc7b2650", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 49799502}
+{"name": "P104_759_sym_h9_alt", "unit": "P104_759", "h": 9, "sym": true, "mode": "alt", "expect": "UNSAT", "nv": 115532, "ncls": 403405, "orth": 2860, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "df8bd02e0d41bbf93a00bd8aac1abeb8027eb9a829e9a5b606c9f5647b1c99c1", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 8684256}
+{"name": "P104_759_gen_h9_alt", "unit": "P104_759", "h": 9, "sym": false, "mode": "alt", "expect": "UNSAT", "nv": 171528, "ncls": 594153, "orth": 5720, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "80b078434974e70f84a6c5718cd1bc40f2d6c33e0349e515f5719b79957dfe15", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 34587369}
+{"name": "P104_767_sym_h9_alt", "unit": "P104_767", "h": 9, "sym": true, "mode": "alt", "expect": "UNSAT", "nv": 115532, "ncls": 403405, "orth": 2860, "gauge": [8, 20, 30, 38, 56, 57, 60, 61], "cnf_sha256": "557d3d29aa927bbe71f6b2ae06e5499d6fd82563abe8c789d33e6401d2fb63b4", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 8742339}
+{"name": "P104_767_gen_h9_alt", "unit": "P104_767", "h": 9, "sym": false, "mode": "alt", "expect": "UNSAT", "nv": 171528, "ncls": 594153, "orth": 5720, "gauge": [8, 20, 30, 38, 56, 57, 60, 61], "cnf_sha256": "b337c28ff878b786427a0c50f0ee25db555144a7b36b59d33ed419b6b92e71d3", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 64727910}
+{"name": "P104_801_sym_h9_alt", "unit": "P104_801", "h": 9, "sym": true, "mode": "alt", "expect": "UNSAT", "nv": 115532, "ncls": 403405, "orth": 2860, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "edc102555c165f1b5be5dc82d2f6f187a6bc7cb79fba63a2120fe34b2311258f", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 8762203}
+{"name": "P104_801_gen_h9_alt", "unit": "P104_801", "h": 9, "sym": false, "mode": "alt", "expect": "UNSAT", "nv": 171528, "ncls": 594153, "orth": 5720, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "55d44ae6a54506ad7672185caf3c236fdb94353171dd32c3558e91e0368231ef", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 43980864}
+{"name": "E7_gen_h7_alt", "unit": "E7", "h": 7, "sym": false, "mode": "alt", "expect": "UNSAT", "nv": 46697, "ncls": 160840, "orth": 1890, "gauge": [26, 28, 36, 88, 89, 90, 91], "cnf_sha256": "15125d0e5db176a0b5ac959ae78bd66a3e121ae23425e1fd319cc0c42752f03f", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 2719685}
+{"name": "E6_gen_h7_alt", "unit": "E6", "h": 7, "sym": false, "mode": "alt", "expect": "UNSAT", "nv": 14977, "ncls": 50977, "orth": 540, "gauge": [36, 38, 40, 42, 104], "cnf_sha256": "215dbe2055a5287aa0932ec887fc759305ee2f2648d703ea1ba8cdb903952d07", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 40159628}
+{"name": "P112_sym_h9_ctl", "unit": "P112", "h": 9, "sym": true, "mode": "ctl", "expect": "SAT", "nv": 87584, "ncls": 307032, "orth": 3304, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "6cb151c69a5d29d98deaaff229e401077500ac984ce34388162f238f6e167457", "status": "SAT", "model_fitting": true, "orth_zero": 0, "orth_total": 3304}
+{"name": "P112_gen_h9_ctl", "unit": "P112", "h": 9, "sym": false, "mode": "ctl", "expect": "SAT", "nv": 95648, "ncls": 331144, "orth": 6608, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "d0ad279baf7926c210545d6264f0d4db8b48d1591f3a35c72f79cd9c5c5548a8", "status": "SAT", "model_fitting": true, "orth_zero": 0, "orth_total": 6608}
+{"name": "E8_sym_h9_ctl", "unit": "E8", "h": 9, "sym": true, "mode": "ctl", "expect": "SAT", "nv": 101864, "ncls": 357280, "orth": 3780, "gauge": [0, 2, 4, 6, 8, 10, 12, 56], "cnf_sha256": "5d9ffbd7cf1eb366333999bc93758570e47ebfdc84e673d13fc8eec1f56179c9", "status": "SAT", "model_fitting": true, "orth_zero": 0, "orth_total": 3780}
+{"name": "E8_gen_h9_ctl", "unit": "E8", "h": 9, "sym": false, "mode": "ctl", "expect": "SAT", "nv": 110616, "ncls": 383496, "orth": 7560, "gauge": [0, 2, 4, 6, 8, 10, 12, 56], "cnf_sha256": "e6b37bcabe5f0fa88d282a5766d226aef2199dd3f79549308fdf4de452f905dd", "status": "SAT", "model_fitting": true, "orth_zero": 0, "orth_total": 7560}
+{"name": "P104H4_sym_h9_ctl", "unit": "P104H4", "h": 9, "sym": true, "mode": "ctl", "expect": "SAT", "nv": 74392, "ncls": 260624, "orth": 2860, "gauge": [8, 20, 30, 38, 56, 57, 60, 61], "cnf_sha256": "90b718304b15b6a4be9b63dfd0f3a19b089f0af78d225f0b4148214269ab659b", "status": "SAT", "model_fitting": true, "orth_zero": 0, "orth_total": 2860}
+{"name": "P104H4_gen_h9_ctl", "unit": "P104H4", "h": 9, "sym": false, "mode": "ctl", "expect": "SAT", "nv": 81768, "ncls": 282632, "orth": 5720, "gauge": [8, 20, 30, 38, 56, 57, 60, 61], "cnf_sha256": "cdbc3242c23f84731b509cd9af16072f3ac2d2f06bc8b4f0f75234bcb783ee21", "status": "SAT", "model_fitting": true, "orth_zero": 0, "orth_total": 5720}
+{"name": "E7_gen_h7_ctl", "unit": "E7", "h": 7, "sym": false, "mode": "ctl", "expect": "SAT", "nv": 24857, "ncls": 85239, "orth": 1890, "gauge": [26, 28, 36, 88, 89, 90, 91], "cnf_sha256": "0785d0cce64f288e13abce1997f28d7d939e2a0173a494f6a03f3c39256807de", "status": "SAT", "model_fitting": true, "orth_zero": 0, "orth_total": 1890}
+{"name": "E6_gen_h7_ctl", "unit": "E6", "h": 7, "sym": false, "mode": "ctl", "expect": "SAT", "nv": 8932, "ncls": 30051, "orth": 540, "gauge": [36, 38, 40, 42, 104], "cnf_sha256": "7e50a6fde6b451810bddefd7ac6bfba17ec9f9581e2f830caab2121309f92750", "status": "SAT", "model_fitting": true, "orth_zero": 0, "orth_total": 540}
+{"name": "SUB20_gen_h9_alt", "unit": "P112", "h": 9, "sym": false, "mode": "alt", "expect": "SAT", "nv": 9952, "ncls": 33459, "orth": 366, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "f04ff774a1eb232ded0d1b6ee70ef144bb8dc23b46cbd56a5acdbd1f613d81d5", "status": "SAT", "model_fitting": true, "orth_zero": 226, "orth_total": 366}
+{"name": "SUB40_gen_h9_alt", "unit": "P112", "h": 9, "sym": false, "mode": "alt", "expect": "SAT", "nv": 33432, "ncls": 114325, "orth": 1260, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "f211b55153baf0ca07c3ae44e31bafe3dd5aaa537531a7b027ffe1b8cc137b89", "status": "SAT", "model_fitting": true, "orth_zero": 792, "orth_total": 1260}
+{"name": "P112_sym_h10_alt", "unit": "P112", "h": 10, "sym": true, "mode": "alt", "expect": "SAT", "nv": 151696, "ncls": 529697, "orth": 3304, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "2f9a6d619ee09e9477ffd9c529ef0bb726e5a51aebc6e97288e2c9c79ca606e8", "status": "SAT", "model_fitting": true, "orth_zero": 59, "orth_total": 3304}
+{"name": "P112_gen_h10_alt", "unit": "P112", "h": 10, "sym": false, "mode": "alt", "expect": "SAT", "nv": 223472, "ncls": 774705, "orth": 6608, "gauge": [6, 18, 28, 36, 56, 57, 58, 59], "cnf_sha256": "1f4f0bcf8ff11ab3e11ee7ebcef400703bda262fbdfe933dae76261dfba6f81e", "status": "SAT", "model_fitting": true, "orth_zero": 89, "orth_total": 6608}
+{"name": "P111_sym_h9_alt", "unit": "P111", "h": 9, "sym": true, "mode": "alt", "expect": "UNSAT", "nv": 133246, "ncls": 465449, "orth": 3235, "gauge": [8, 9, 14, 15, 30, 31, 59, 60], "cnf_sha256": "8189ccce184ca974844a67b715ce8932f41b5a49f2557c5fb3ecfa3007ba3f0f", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 9978227}
+{"name": "P111_sym_h9_ctl", "unit": "P111", "h": 9, "sym": true, "mode": "ctl", "expect": "SAT", "nv": 86139, "ncls": 301959, "orth": 3235, "gauge": [8, 9, 14, 15, 30, 31, 59, 60], "cnf_sha256": "d118231f77991c000814010cd031df56d15bcb92fd62dfad4f5c8f0894cf524c", "status": "SAT", "model_fitting": true, "orth_zero": 0, "orth_total": 3235}
+{"name": "P111_gen_h9_alt", "unit": "P111", "h": 9, "sym": false, "mode": "alt", "expect": "UNSAT", "nv": 196287, "ncls": 680399, "orth": 6470, "gauge": [8, 9, 14, 15, 30, 31, 59, 60], "cnf_sha256": "761b2e656ed81e63fd44768dc085685dd272022b8a83443f1c9f79291733a088", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 38488427}
+{"name": "P111_gen_h9_ctl", "unit": "P111", "h": 9, "sym": false, "mode": "ctl", "expect": "SAT", "nv": 94185, "ncls": 326044, "orth": 6470, "gauge": [8, 9, 14, 15, 30, 31, 59, 60], "cnf_sha256": "4d7fbb647464431021e350d70310fe3b977df7b5aff85d00f80ba995b178b9d5", "status": "SAT", "model_fitting": true, "orth_zero": 0, "orth_total": 6470}
diff --git a/research/decoder-floors-frontier-format/sat/results_misc.jsonl b/research/decoder-floors-frontier-format/sat/results_misc.jsonl
new file mode 100644
index 0000000000..e22aa63c82
--- /dev/null
+++ b/research/decoder-floors-frontier-format/sat/results_misc.jsonl
@@ -0,0 +1,16 @@
+{"name": "edge_N0_r7", "expect": "UNSAT", "slow": false, "cnf_sha256": "3c9be5f36365fecf8183a6544e90420268e2c649081feb1eff866eef82503e92", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 72962}
+{"name": "edge_N1_r7", "expect": "UNSAT", "slow": false, "cnf_sha256": "507ff80293131732e3afac972ba738cb316bb456f4d087dce4474dd849982584", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 73008}
+{"name": "edge_N2_r7", "expect": "UNSAT", "slow": false, "cnf_sha256": "33c7b0ef22b013fb13bc03c97d6e1fc7a85dd607a74f83c9068010d2a48fc76a", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 70824}
+{"name": "edge_N3_r7", "expect": "UNSAT", "slow": false, "cnf_sha256": "706b0055dbea3ca9a3b712a5704d20d98b5e6ff1e3f4ac97b23a37b7d8fd29df", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 70869}
+{"name": "edge_N4_r7", "expect": "UNSAT", "slow": false, "cnf_sha256": "36afc2e70b6cac4afd3bd7bb4466e14d43cda735b5da32c9229a6a2216ded31b", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 70869}
+{"name": "edge_N5_r7", "expect": "UNSAT", "slow": false, "cnf_sha256": "bb3eb34305ee881b1b3c703e9f1460251c02da6d6733206341883536a72edd1c", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 70894}
+{"name": "edge_N6_r7", "expect": "UNSAT", "slow": false, "cnf_sha256": "90e66a1c40bb0b21b1ef5426dcc1f989ea7e4f1a554e71352bfa6fe44e45bc4e", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 71080}
+{"name": "edge_N7_r7", "expect": "UNSAT", "slow": false, "cnf_sha256": "4e73af6008e548f7ff0b246e41554dd83f5492f865e5f83e3f06ef2f37fa5fff", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 71129}
+{"name": "edge_N0_r8", "expect": "SAT", "slow": false, "cnf_sha256": "85bcdb300ff85401735044d24f6d41e1b16ef84bfee91359c9556f352e5db365", "status": "SAT", "model_ok": true}
+{"name": "hit_k7_z13", "expect": "UNSAT", "slow": false, "cnf_sha256": "7e339bb0fe0d869801a42a5a89ec541e7c4c88c6f58a6f4cab8c020d04b13c69", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 10092729}
+{"name": "hit_k7_z14", "expect": "SAT", "slow": false, "cnf_sha256": "066bb756d288d5ffa19ed9b8c8833baf8dd9436d5bde662585efd8ff8c3fc581", "status": "SAT", "model_ok": true}
+{"name": "tri_keep11", "expect": "UNSAT", "slow": false, "cnf_sha256": "cef7e9c5b4daf925715430a6c5d74daaf58c14c26556798f2276c85c5527a063", "status": "UNSAT", "drat": "VERIFIED", "proof_bytes": 2970357}
+{"name": "tri_keep10", "expect": "SAT", "slow": false, "cnf_sha256": "76c83f12fdaf33e328edb5685a12c48397beada896759a9b63da4bde0dd43e80", "status": "SAT", "model_ok": true}
+{"name": "hit_k6_z22", "expect": "UNSAT", "slow": true, "cnf_sha256": "32987c89a3bda7663f14ee7c2e493ba3dde7d8de3ae91abca80b8ac85eb034b1", "status": "UNSAT"}
+{"name": "hit_k5_z31", "expect": "UNSAT", "slow": true, "cnf_sha256": "bf22088f13614093a067d50cf835478f4902819454e240292dab90952749b4f9", "status": "UNSAT"}
+{"name": "hit_k4_z37", "expect": "UNSAT", "slow": true, "cnf_sha256": "f2b036d292465026cd617f8e6e6a487a5afc0e4e20c915cc5eff0e4deb56ea85", "status": "UNSAT"}
diff --git a/research/decoder-floors-frontier-format/sat/rigid.py b/research/decoder-floors-frontier-format/sat/rigid.py
new file mode 100644
index 0000000000..447cf459f5
--- /dev/null
+++ b/research/decoder-floors-frontier-format/sat/rigid.py
@@ -0,0 +1,138 @@
+"""CNF generator for Theorem R (rigidity of the minimal-rank label table).  Standard library only.
+Unit U (v lines), h = label dimension.  General model: B = U V^T, U, V in F2^{v x h}; symmetric model (the physical one, B = P P^T): V = U.
+Fitting: B_tt = 1, B_ts = 0 for every non-orthogonal pair t != s; entries on orthogonal pairs are free.  Dense B: 1 on every orthogonal pair.
+mode 'alt': add the clause "some orthogonal ordered pair (unordered if symmetric) has B_ts = 0".  UNSAT  <=>  every fitting B of F2-rank <= h is dense.
+mode 'ctl': no extra clause (must be SAT, and every model must decode to a fitting matrix; for h = rank of the dense B the model is the dense B).
+Gauge: S = a pairwise non-orthogonal clique (|S| = 8 for E8/P112/P104, 7 for E7, 5 for E6, pinned in data/gauge.json): B[S,S] = I, so U[S] has rank |S|,
+GL(h) is transitive on such tuples, hence U[S] = (e_1..e_|S|) WLOG (symmetric model: P[S] orthonormal, the isometry argument of STRAYS Thm R requires
+|S| >= h - 1).  This is the encoding of the author's working card STRAYS/rigid2.py; the clique choice here is deterministic and pinned."""
+import sys, os, json, hashlib
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, os.path.join(HERE, '..', 'lib'))
+from units import *
+
+def gauge_clique(name, L_idx, kc):
+    """lexicographically least (by bitmask) maximum clique of the non-orthogonality graph on the unit, truncated to kc lines (deterministic)"""
+    from satgen import clique_in, nonorth_graph
+    L = sub(L_idx); adj = nonorth_graph(L)
+    S = clique_in(adj, (1 << len(L)) - 1)
+    assert len(S) >= kc
+    return [L_idx[i] for i in S[:kc]]
+
+def build(name, h, sym, mode, S, V=None, orthf=None):
+    """returns (nv, clauses, info); line labels are positions in the unit's index list"""
+    orthf = orthf or orth
+    V = V if V is not None else unit_idx(name); pos = {t: i for i, t in enumerate(V)}; v = len(V)
+    kc = len(S); assert all(t in pos for t in S)
+    nv = 0; cls = []
+    def new():
+        nonlocal nv; nv += 1; return nv
+    Sset = {t: k for k, t in enumerate(S)}
+    Uv = {t: [new() for _ in range(h)] for t in V if t not in Sset}
+    Vv = Uv if sym else {t: [new() for _ in range(h)] for t in V}
+    def ub(t, k): return ('c', int(Sset[t] == k)) if t in Sset else ('v', Uv[t][k])
+    def vb(t, k): return ub(t, k) if sym else ('v', Vv[t][k])
+    def AND(a, b):
+        if a[0] == 'c' and b[0] == 'c': return ('c', a[1] & b[1])
+        if a[0] == 'c': return b if a[1] else ('c', 0)
+        if b[0] == 'c': return a if b[1] else ('c', 0)
+        if a[1] == b[1]: return a
+        z = new(); x, y = a[1], b[1]; cls.extend([[-z, x], [-z, y], [z, -x, -y]]); return ('v', z)
+    def XOR(a, b):
+        if a[0] == 'c' and b[0] == 'c': return ('c', a[1] ^ b[1])
+        if a[0] == 'c': return ('v', -b[1]) if a[1] else b
+        if b[0] == 'c': return ('v', -a[1]) if b[1] else a
+        z = new(); x, y = a[1], b[1]; cls.extend([[-z, x, y], [-z, -x, -y], [z, -x, y], [z, x, -y]]); return ('v', z)
+    def Bent(t, s):
+        acc = ('c', 0)
+        for k in range(h): acc = XOR(acc, AND(ub(t, k), vb(s, k)))
+        return acc
+    def force(l, val):
+        if l[0] == 'c':
+            if l[1] != val: cls.append([])
+            return
+        cls.append([l[1] if val else -l[1]])
+    orthp = []
+    for t in V:
+        force(Bent(t, t), 1)
+        for s in V:
+            if s == t: continue
+            if not orthf(t, s): force(Bent(t, s), 0)
+            elif not sym or t < s: orthp.append((t, s))
+    if mode == 'alt':
+        lits = []
+        for (t, s) in orthp:
+            d = Bent(t, s)
+            if d[0] == 'c':
+                assert d[1] == 1, 'trivially SAT'
+                continue
+            lits.append(-d[1])
+        cls.append(lits)
+    info = dict(v=v, h=h, sym=sym, mode=mode, nv=nv, ncls=len(cls), orth=len(orthp), gauge=S)
+    return nv, cls, info, Uv, Vv, orthp
+
+def dimacs(nv, cls):
+    return "p cnf %d %d\n" % (nv, len(cls)) + "".join(" ".join(map(str, c)) + " 0\n" for c in cls)
+
+def sha(s): return hashlib.sha256(s.encode()).hexdigest()
+
+# ---------------------------------------------------------------- registry
+def sub_unit(kc_S, k):
+    """negative control: the gauge clique S plus the first k other lines of P112 (index order)"""
+    return list(kc_S) + [t for t in P112_IDX if t not in set(kc_S)][:k]
+
+import functools
+KC = {'E8': 8, 'P112': 8, 'P104H4': 8, 'P104_759': 8, 'P104_767': 8, 'P104_801': 8, 'E7': 7, 'E6': 5}
+@functools.lru_cache(maxsize=None)
+def registry():
+    """name -> dict(unit, h, sym, mode, expect, S, V)"""
+    R = {}
+    def add(unit, h, sym, mode, expect, V=None, tag=None):
+        S = gauge_clique(unit if V is None else 'P112', unit_idx(unit if V is None else 'P112'), KC[unit if V is None else 'P112'])
+        if expect == 'UNSAT' and sym: assert len(S) >= h - 1
+        name = '%s_%s_h%d_%s' % (tag or unit, 'sym' if sym else 'gen', h, mode)
+        R[name] = dict(unit=unit, h=h, sym=sym, mode=mode, expect=expect, S=S, V=V)
+    for u in ('P112', 'E8', 'P104H4', 'P104_759', 'P104_767', 'P104_801'):
+        for sym in (True, False): add(u, 9, sym, 'alt', 'UNSAT')
+    for u in ('E7', 'E6'): add(u, 7, False, 'alt', 'UNSAT')
+    for u in ('P112', 'E8', 'P104H4'):
+        for sym in (True, False): add(u, 9, sym, 'ctl', 'SAT')
+    for u in ('E7', 'E6'): add(u, 7, False, 'ctl', 'SAT')
+    S = gauge_clique('P112', unit_idx('P112'), 8)
+    for k in (20, 40): add('P112', 9, False, 'alt', 'SAT', V=sub_unit(S, k), tag='SUB%d' % k)
+    for sym in (True, False): add('P112', 10, sym, 'alt', 'SAT')
+    # P111 (bit unit of PR #589): own coordinates, gauge clique from its own Gram
+    L, of = p111(); adjn = [sum(1 << s for s in range(111) if s != t and not of(t, s)) for t in range(111)]
+    from satgen import clique_in
+    S1 = clique_in(adjn, (1 << 111) - 1)[:8]
+    for sym in (True, False):
+        for mode, ex in (('alt', 'UNSAT'), ('ctl', 'SAT')):
+            name = 'P111_%s_h9_%s' % ('sym' if sym else 'gen', mode)
+            R[name] = dict(unit='P111', h=9, sym=sym, mode=mode, expect=ex, S=S1, V=None)
+    return R
+
+def p111():
+    """(vectors, orthf) of the P111 bit unit (data/p111_lines.json)"""
+    L = json.load(open(os.path.join(DATA, 'p111_lines.json')))['lines']
+    return L, (lambda t, s: sum(a * b for a, b in zip(L[t], L[s])) == 0)
+
+def build_named(name):
+    r = registry()[name]
+    if r['unit'] == 'P111':
+        L, of = p111(); return build('P111', r['h'], r['sym'], r['mode'], r['S'], V=list(range(111)), orthf=of)
+    return build(r['unit'], r['h'], r['sym'], r['mode'], r['S'], V=r['V'])
+
+def decode_model(name, pos_vars):
+    """returns (fitting?, #orthogonal pairs with B_ts = 0, #orthogonal pairs) for a model of an instance"""
+    r = registry()[name]; nv, cls, info, Uv, Vv, orthp = build_named(name)
+    V = r['V'] if r['V'] is not None else (list(range(111)) if r['unit'] == 'P111' else unit_idx(r['unit'])); h = r['h']; Sset = {t: k for k, t in enumerate(r['S'])}
+    def row(t, M):
+        if M is Uv and t in Sset: return [int(Sset[t] == k) for k in range(h)]
+        return [int(x in pos_vars) for x in M[t]]
+    # in the symmetric model V = U so the S rows are constants for both
+    Ur = {t: row(t, Uv) for t in V}; Vr = Ur if r['sym'] else {t: [int(x in pos_vars) for x in Vv[t]] for t in V}
+    ent = lambda t, s: sum(a & b for a, b in zip(Ur[t], Vr[s])) & 1
+    of = p111()[1] if r['unit'] == 'P111' else orth
+    fit = all(ent(t, t) == 1 for t in V) and all(ent(t, s) == 0 for t in V for s in V if t != s and not of(t, s))
+    zeros = sum(1 for (t, s) in orthp if ent(t, s) == 0)
+    return fit, zeros, len(orthp)
diff --git a/research/decoder-floors-frontier-format/scripts/provenance.py b/research/decoder-floors-frontier-format/scripts/provenance.py
new file mode 100644
index 0000000000..d12d3d802a
--- /dev/null
+++ b/research/decoder-floors-frontier-format/scripts/provenance.py
@@ -0,0 +1,45 @@
+"""Step 0 of verify.sh (standard library only).  Prints one PASS/FAIL line per group and exits 1 on any mismatch.
+  0.manifest  every file of the package matches MANIFEST.sha256 (sha256), none is missing and none is extra
+  0.sources   every pin of SOURCES.json holds: the sha256 of each pinned package file (checks and libraries)
+usage: python3 provenance.py [--write-manifest]   (--write-manifest is for the authors: it rewrites MANIFEST.sha256; SOURCES.json is written by --write-sources)"""
+import hashlib, json, os, sys
+PKG = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
+bad = 0
+def sha(b): return hashlib.sha256(b).hexdigest()
+def listing():
+    out = []
+    for d, ds, fs in os.walk(PKG):
+        ds[:] = sorted(x for x in ds if x != '__pycache__' and x != 'bin')
+        for f in fs:
+            if f.endswith('.pyc') or f == '.DS_Store': continue
+            p = os.path.relpath(os.path.join(d, f), PKG)
+            if p != 'MANIFEST.sha256': out.append(p)
+    return sorted(out)
+if '--write-manifest' in sys.argv:
+    with open(os.path.join(PKG, 'MANIFEST.sha256'), 'w') as h:
+        for p in listing(): h.write('%s  %s\n' % (sha(open(os.path.join(PKG, p), 'rb').read()), p))
+    print('wrote MANIFEST.sha256 (%d files)' % len(listing())); sys.exit(0)
+if '--write-sources' in sys.argv:
+    S = json.load(open(os.path.join(PKG, 'SOURCES.json')))
+    for sect in ('files', 'evidence'):
+        for e in S[sect]: e['sha256'] = sha(open(os.path.join(PKG, e['file']), 'rb').read())
+    json.dump(S, open(os.path.join(PKG, 'SOURCES.json'), 'w'), indent=1); print('wrote SOURCES.json pins'); sys.exit(0)
+want = {}
+for l in open(os.path.join(PKG, 'MANIFEST.sha256'), encoding='utf-8'):
+    h, p = l.rstrip('\n').split('  ', 1); want[p] = h
+have = listing(); n = 0
+for p in sorted(set(want) | set(have)):
+    f = os.path.join(PKG, p)
+    if p not in want: print('FAIL 0.manifest extra file not in MANIFEST: ' + p); bad += 1
+    elif not os.path.isfile(f): print('FAIL 0.manifest missing file: ' + p); bad += 1
+    elif sha(open(f, 'rb').read()) != want[p]: print('FAIL 0.manifest hash differs: ' + p); bad += 1
+    else: n += 1
+print('%s 0.manifest  %d files match MANIFEST.sha256' % ('PASS' if not bad else 'FAIL', n), flush=True)
+S = json.load(open(os.path.join(PKG, 'SOURCES.json'))); b0 = bad; k = 0
+for sect in ('files', 'evidence'):
+    for e in S[sect]:
+        k += 1; f = os.path.join(PKG, e['file'])
+        if not os.path.isfile(f): print('FAIL 0.sources missing ' + e['file']); bad += 1
+        elif sha(open(f, 'rb').read()) != e['sha256']: print('FAIL 0.sources pin differs: ' + e['file']); bad += 1
+print('%s 0.sources  %d pins hold (checks and libraries)' % ('PASS' if bad == b0 else 'FAIL', k - (bad - b0)), flush=True)
+sys.exit(1 if bad else 0)
diff --git a/research/decoder-floors-frontier-format/verify.sh b/research/decoder-floors-frontier-format/verify.sh
new file mode 100755
index 0000000000..c67127a50c
--- /dev/null
+++ b/research/decoder-floors-frontier-format/verify.sh
@@ -0,0 +1,43 @@
+#!/usr/bin/env bash
+# One-command verification of research/decoder-floors-frontier-format (no kappa claim).  Recomputes every CHECKED item of the README:
+#   c1 Theorem R (rigidity of the minimal-rank label table): CNF regeneration + hashes, shipped DRAT proofs, kissat re-solve + drat-trim;
+#   c2 Lemma 1.1 census, survivors and pair ranks (Theorem P);  c3 batching premises and an O(9) chart with 64 rank-7 cross pairs;
+#   c4 #1180's nine-term identity (65), co-star dead sets;  c5 decoders attaining the floors;  c6 EDGE E1a block minrank and puncture clique-hitting bounds;
+#   c7 the P111 bit unit.
+# Step 0 checks the package against MANIFEST.sha256 and every pin of SOURCES.json and stops hard on any mismatch.
+# Single process at a time; standard-library Python only.  kissat 4.0.4 (KISSAT=/path or on PATH) and drat-trim (DRAT_TRIM=/path or on PATH) are OPTIONAL:
+# without them the lines that need them are SKIP lines (never PASS).  HIT_FULL=1 re-solves three slow clique-hitting instances (kissat only, no proof).
+#   usage: bash verify.sh [/fresh/output/dir]     (inside a checkout or `git archive` of the repository)
+#   set PYTHON to choose the interpreter (>= 3.11).  Prints PASS / FAIL; exit status is nonzero on any FAIL.
+set -uo pipefail
+HERE=$(cd "$(dirname "$0")" && pwd)
+OUT=${1:-$(mktemp -d "${TMPDIR:-/tmp}/decoder-floors-frontier-format.XXXXXX")}
+mkdir -p "$OUT"; OUT=$(cd "$OUT" && pwd)
+case "$OUT/" in "$HERE"/*) echo "output dir must be outside the package"; exit 2;; esac
+PY="${PYTHON:-python3}"; export PYTHONDONTWRITEBYTECODE=1
+T0=$SECONDS
+echo "== 0. manifest and provenance"
+if ! "$PY" -B "$HERE/scripts/provenance.py" | tee "$OUT/provenance.log" | sed 's/^/   /' || grep -q '^FAIL' "$OUT/provenance.log" \
+   || [ "$(grep -c '^PASS' "$OUT/provenance.log")" != 2 ]; then
+  echo "step 0 FAILED"; exit 1
+fi
+echo "   tools: kissat=$(command -v "${KISSAT:-kissat}" 2>/dev/null || echo none)  drat-trim=$(command -v "${DRAT_TRIM:-drat-trim}" 2>/dev/null || echo none)"
+mkdir -p "$OUT/logs"; : > "$OUT/all.out"
+run() {  # name script
+  echo "== $1"
+  ( cd "$HERE/checks" && "$PY" -B "$2" > "$OUT/logs/$2.log" 2>&1; echo $? > "$OUT/logs/$2.rc" )
+  cat "$OUT/logs/$2.log" | tee -a "$OUT/all.out" | sed 's/^/   /'
+  [ "$(cat "$OUT/logs/$2.rc")" = 0 ] || echo "FAIL $2 exit status $(cat "$OUT/logs/$2.rc")" | tee -a "$OUT/all.out"
+}
+run "c1 Theorem R: rigidity of the minimal-rank label table (30 SAT instances)" c1_rigidity.py
+run "c2 Lemma 1.1 census, survivors and pair ranks" c2_support_propagation.py
+run "c3 batching premises (P112 labels, normals, frame lemma, O(9) chart)" c3_batch_premises.py
+run "c4 #1180 identity, co-star dead sets, survivor cliques" c4_masked_costar.py
+run "c5 decoders attaining the floors" c5_attaining_decoders.py
+run "c6 coordinate-block minrank under every B; puncture clique hitting" c6_block_minrank_punctures.py
+run "c7 the P111 bit unit" c7_p111_unit.py
+npass=$(grep -c '^PASS' "$OUT/all.out"); nfail=$(grep -c '^FAIL' "$OUT/all.out"); nskip=$(grep -c '^SKIP' "$OUT/all.out")
+EXPECT=$((72 - nskip))
+echo "== done in $((SECONDS - T0))s: $((npass + 2)) PASS (2 in step 0), $nskip SKIP, $nfail FAIL; logs in $OUT"
+if [ "$nfail" = 0 ] && [ "$npass" = "$EXPECT" ]; then echo "PASS: all expected assertions hold"; exit 0; fi
+echo "FAIL: expected $EXPECT assertion PASS lines after step 0, got $npass PASS / $nfail FAIL / $nskip SKIP"; exit 1