diff --git a/research/e7-bitsliced-exhaustion/BENCHMARK.json b/research/e7-bitsliced-exhaustion/BENCHMARK.json
new file mode 100644
index 0000000000..ce06d46c40
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/BENCHMARK.json
@@ -0,0 +1,52 @@
+{
+  "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]",
+  "platform": "macOS-26.6.1-arm64-arm-64bit",
+  "command_flags": [
+    "-I",
+    "-B"
+  ],
+  "serial": true,
+  "records": [
+    {
+      "implementation": "old",
+      "seconds": 15.090498709003441,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "implementation": "new",
+      "seconds": 0.7883416670374572,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "implementation": "new",
+      "seconds": 0.8870171670569107,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "implementation": "old",
+      "seconds": 13.816090291016735,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "implementation": "old",
+      "seconds": 13.72491204191465,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    },
+    {
+      "implementation": "new",
+      "seconds": 0.723674124921672,
+      "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4",
+      "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
+    }
+  ],
+  "median_seconds": {
+    "old": 13.816090291016735,
+    "new": 0.7883416670374572
+  },
+  "speed_ratio": 17.525510662067134
+}
diff --git a/research/e7-bitsliced-exhaustion/PROOF.md b/research/e7-bitsliced-exhaustion/PROOF.md
new file mode 100644
index 0000000000..29ea6c69f7
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/PROOF.md
@@ -0,0 +1,118 @@
+# Exact binary-code exhaustion in bit lanes
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Claim and consumer
+
+Let g_0,...,g_(d-1) be independent vectors in F2^n. Encode each vector as a
+nonnegative integer with at most n bits. For 0 <= w <= n, `low_weight_words`
+returns every word of their span with Hamming weight at most w, exactly once.
+It includes zero. There is no assumption about the code, its minimum distance,
+the generator order, or the relation between n and a machine word width.
+The input check rejects dependent generators and malformed bounds.
+
+The complete E7 classifier from PR5669 uses this function with n=63, d=27,
+and w=12. It checks that zero and exactly 1,638 weight-twelve words remain.
+Thus every nonzero word has weight at least twelve and all equality supports
+are retained. The bound, equality theorem and all geometric conclusions are
+the predecessor's results. This package changes their exact replay method.
+
+## Coefficient partition
+
+Set k=min(batch_bits,d) and L=2^k. Number lanes by integers a in [0,L).
+The integer mask has a one at each of those L positions. For each j<k, the
+coefficient pattern has bit a equal to bit j of a. The geometric-series
+formula in the implementation repeats a block of 2^j zero bits followed by
+2^j one bits. Its period divides L. Integer multiplication concatenates
+these disjoint blocks; it cannot create a carry between them.
+
+For each coordinate i, XOR the coefficient patterns whose generator g_j
+has coordinate i equal to one. Lane a now holds coordinate i of the low
+coefficient sum. Gray traversal enumerates every coefficient vector on
+g_k,...,g_(d-1) exactly once. At step t>0 it changes the generator indexed
+by the least significant one bit of t. Induction gives the usual Gray word
+t XOR floor(t/2), a bijection on all high coefficients.
+
+For a fixed high sum h, XOR the full lane mask at coordinate i precisely
+when h_i=1. Each lane is now one complete codeword. Every coefficient vector
+appears in exactly one batch and lane. Independence makes their images
+distinct. No pruning or sampling occurs.
+
+## Weight addition and comparison
+
+For three one-bit operands a,b,c in one lane, set
+
+```text
+s = a XOR b
+sum_bit = s XOR c
+carry_bit = (a AND b) OR (s AND c).
+```
+
+The integer identity a+b+c=sum_bit+2*carry_bit holds in each of the eight
+cases. Every operation is bitwise, so the same identity holds separately
+in every lane. The program keeps carry bits in a separate plane of twice
+the weight; it never shifts them into another lane. Two operands use the
+same half-adder identity. At each level, these steps reduce the operand
+list and send carries to the next level. They terminate with the exact
+binary expansion of each lane's Hamming weight.
+
+The comparator scans those planes from high to low. `equal` contains the
+lanes whose prefix equals the bound prefix; `less` contains those already
+strictly smaller. If the next bound bit is one, zero lanes leave `equal`
+and enter `less`. If it is zero, one lanes leave `equal` without entering
+`less`. This invariant proves that `less OR equal` contains exactly weights
+at most w. The final mask removes all positions outside the finite lane set.
+If the bound exceeds the largest representable value, every lane qualifies.
+
+For each retained lane, the program reconstructs the literal XOR of the
+chosen low generators and h. This is its exact input word. Zero dimension,
+zero width, zero weight, and a bound equal to n follow from the same rules.
+
+## Resource bound and scope
+
+The public batch parameter is an integer in 1..20, with default 16. Input
+dimension and width have no fixed cap. The plane storage is O(n*2^k) bits,
+in addition to O(nd) bits for generators and elimination. Outputs are yielded
+one at a time. The E7 default uses 2,048 batches of 65,536 lanes; it does not
+store a 134-million-entry word table.
+
+Each batch uses O(n) Boolean adder operations and O(log(n+1)) comparison
+operations on L-bit integers. Input planes require O(nk) such operations.
+Literal output reconstruction costs at most d vector XORs per output.
+The coefficient space is still exponential in d. This is an exact arithmetic
+implementation improvement, not a polynomial algorithm for minimum distance.
+Python object overhead and integer operations remain positive costs.
+
+## Full replay boundary
+
+The source archive is retained byte for byte. The derived `classify.py`
+differs from the source verifier at only `HERE` and `minimum_supports`.
+The first locates the retained archive; the second calls the new engine.
+The registered check compares every other Python syntax node exactly.
+It then runs the complete derived check and compares every field of the
+source receipt. All 63 reflection maps, all 135 frames, rational lift and
+quadratic ranks, all 120 ambient slices, omission controls and rejection
+controls remain active. There is no runtime replacement of a function and
+no cache of source results.
+
+The independent small oracle constructs spans by literal list doubling and
+uses integer Hamming weights. It covers all 1,381 independent unordered
+generator sets in F2^4, all five weight bounds, and five batch sizes: 34,525
+comparisons. Separate tests cover widths through 127, malformed domains,
+changed bases, changed bounds and a full changed basis for the E7 code.
+These finite checks corroborate the general lane argument above.
+
+## Relevance and attribution
+
+E7 support exhaustion is used in the E8 deletion and quadratic-extension
+work. Faster exact replays reduce the cost of checking those certificates
+and permit larger bounded code searches. The implementation does not alter
+the physical multiplication word, its paid profile or any selected bound.
+Complete kappa is unchanged.
+
+Credit Nick Petalas's PR5238 for the geometry, support theorem and binary
+code; Ali Romman's PR5669 for the equality classification and complete
+consumer; and the source's JoyboyBrian, Josie Elliston, Andrey Mas, Aaron
+Wang, Brett Halligan, themilkman216 and DreamingOfClouds lineage. All source
+notices remain in the retained archive. Boolean adders and bit-parallel
+enumeration are established methods; no literature-priority claim is made.
diff --git a/research/e7-bitsliced-exhaustion/README.md b/research/e7-bitsliced-exhaustion/README.md
new file mode 100644
index 0000000000..e695812860
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/README.md
@@ -0,0 +1,73 @@
+# Exact E7 exhaustion in bit lanes
+
+The complete E7 minimum-support classifier runs 17.53 times faster in the
+recorded local comparison: median 13.816 seconds becomes 0.788 seconds.
+All six fresh-process outputs are byte-identical. All 134,217,727 nonzero
+codewords remain covered. Complete kappa is unchanged.
+
+The [proof](PROOF.md) establishes the exact iterator for arbitrary independent
+binary generators. [binary.py](binary.py) computes Hamming weights in parallel
+integer bit lanes. [classify.py](classify.py) is the complete derived consumer.
+Only its source-root path and minimum-support function differ from the frozen
+verifier; the registered check compares every other syntax node.
+
+[RESULT.json](RESULT.json) records all scientific checks.
+[BENCHMARK.json](BENCHMARK.json) records alternating fresh-process timings on
+Python 3.12.14, macOS arm64. [VALIDATION.md](VALIDATION.md) states the limits.
+[SOURCES.json](SOURCES.json) binds all eleven retained input files.
+
+## Reproduce
+
+From the repository root, with Python 3.12 and its standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/e7-bitsliced-exhaustion
+```
+
+Expected markers:
+
+```text
+PASS_E7_BITSLICED_EXHAUSTION
+PASS_REGISTERED_RESEARCH_PACKAGE
+```
+
+The registered verifier covers all 1,381 independent unordered generator sets
+in F2^4, all five weight bounds and five batch sizes: 34,525 comparisons.
+It also checks 108 wide-code cases, sixteen domain and invalidation controls,
+the full original classification result, and a second full E7 basis.
+The full classification retains all reflection, frame, rational-rank,
+ambient-pivot and corruption controls from the predecessor.
+
+For a separate timing run, use an output path outside the package:
+
+```sh
+python3.12 -I -B research/e7-bitsliced-exhaustion/benchmark.py --output /tmp/e7-timings.json
+```
+
+The timing command alternates three complete old and three complete new
+fresh-process replays on the same interpreter. It checks exact output equality.
+Runtime ratios are local measurements, not a universal hardware guarantee or
+a physical multiplication speedup. The iterator still exhausts an exponential
+coefficient space. Its bounded bit-lane storage avoids a full word table.
+
+## Credit and scope
+
+[PR #5669](https://github.com/CrocSwap/integer-mult-bounds/pull/5669), exact head
+700efb538a3d919409c9506d117846b7895b02ea, supplies the complete classification,
+consumer and receipt. Its retained [PR #5238](https://github.com/CrocSwap/integer-mult-bounds/pull/5238)
+source supplies Nick Petalas's frame-code geometry and minimum-support proof.
+The complete predecessor notices and attribution remain unchanged in `source/`.
+The new bit-lane implementation, proof and independent small-code oracle are
+by Ali Romman with substantial OpenAI Codex assistance. No subagents.
+Apache-2.0. The consumer uses the same assistant family as its predecessor;
+no independent human or proof-kernel acceptance is claimed.
+
+No new geometry bound, physical supplier, selected-frontier change or complete
+kappa gain is inferred. The value is faster exact verification for the E7/E8
+deletion and decoder work. No other consumer is silently changed.
+
+## Open next questions
+
+- Bind another actual deletion or decoder code to the iterator. Compare all
+  old checks and outputs, then measure its full replay. No other installation
+  or speed claim is included here.
diff --git a/research/e7-bitsliced-exhaustion/RESULT.json b/research/e7-bitsliced-exhaustion/RESULT.json
new file mode 100644
index 0000000000..2aa871777b
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/RESULT.json
@@ -0,0 +1,207 @@
+{
+  "all_nonzero_E7_words": 134217727,
+  "derivative_changes": [
+    "HERE",
+    "minimum_supports"
+  ],
+  "malformed_and_invalidation_controls": 16,
+  "minimum_supports": 1638,
+  "small_codes": {
+    "comparisons": 34525,
+    "independent_generator_sets": 1381,
+    "sha256": "f1ec458a850f90dc54148aaba4f3dc8b78f2a2614af4e07307735eb10ce930b5"
+  },
+  "source_result": {
+    "ambient_root_slices": 120,
+    "binary_dimension": 27,
+    "binary_rank": 36,
+    "characteristic": "zero",
+    "frames": 135,
+    "minimum_support": 12,
+    "minimum_supports": 1638,
+    "nonzero_codewords": 134217727,
+    "orbits": [
+      {
+        "orbit_sha256": "d08f659fab919baab7b2c87c0b7e55edb5a3e23e05a313522f0b17e684d8ee39",
+        "quadratic_rank": 6,
+        "rational_lift_dimension": 1,
+        "representative_support": [
+          0,
+          1,
+          2,
+          3,
+          4,
+          5,
+          12,
+          19,
+          20,
+          21,
+          28,
+          29
+        ],
+        "representative_values": [
+          -8,
+          -8,
+          -8,
+          -8,
+          -8,
+          -8,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          8,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          8,
+          8,
+          8,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          8,
+          8,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0
+        ],
+        "restricted_frame_rank": 11,
+        "supports": 630,
+        "type": "diagonal"
+      },
+      {
+        "orbit_sha256": "a9bb36def7396f184d343e38f410d705a50be3188b40725235f866ad0753309b",
+        "quadratic_rank": 2,
+        "rational_lift_dimension": 1,
+        "representative_support": [
+          20,
+          21,
+          28,
+          29,
+          34,
+          35,
+          36,
+          37,
+          38,
+          39,
+          40,
+          41
+        ],
+        "representative_values": [
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          4,
+          -4,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          4,
+          -4,
+          0,
+          0,
+          0,
+          0,
+          -4,
+          -4,
+          -4,
+          -4,
+          4,
+          4,
+          4,
+          4,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0,
+          0
+        ],
+        "restricted_frame_rank": 11,
+        "supports": 1008,
+        "type": "product"
+      }
+    ],
+    "reflection_generators": 63,
+    "rejecting_or_omission_controls": 28,
+    "root_lines": 63,
+    "status": "PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION"
+  },
+  "status": "PASS_E7_BITSLICED_EXHAUSTION",
+  "supports_sha256": "658e6ccf9f643cb1b25fe3a0032b51c4c282d5333730eccd83cf8cdd869988b6",
+  "wide_comparisons": 108
+}
diff --git a/research/e7-bitsliced-exhaustion/SOURCE-ORIGIN.json b/research/e7-bitsliced-exhaustion/SOURCE-ORIGIN.json
new file mode 100644
index 0000000000..62be5fa84d
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/SOURCE-ORIGIN.json
@@ -0,0 +1,72 @@
+[
+  {
+    "path": "source/PROOF.md",
+    "source_path": "research/e7-minimum-support-classification/PROOF.md",
+    "source_commit": "700efb538a3d919409c9506d117846b7895b02ea",
+    "git_blob": "af4663e4a8465f2b653e83d1531da9e50dfbdd8b",
+    "sha256": "6749a3aba19ed159f0958c84918828f6da941aa2bebc4b0560ab2db9be11edb3"
+  },
+  {
+    "path": "source/README.md",
+    "source_path": "research/e7-minimum-support-classification/README.md",
+    "source_commit": "700efb538a3d919409c9506d117846b7895b02ea",
+    "git_blob": "ffb6879ecce8662247585479c300406fd6b971ba",
+    "sha256": "8f1519c6816eb6fb22f1779331299b3a18c087b30b967d05f5fb790d5cd1aa6b"
+  },
+  {
+    "path": "source/RESULT.json",
+    "source_path": "research/e7-minimum-support-classification/RESULT.json",
+    "source_commit": "700efb538a3d919409c9506d117846b7895b02ea",
+    "git_blob": "d32035693b23f114723c953c94370b349aa13cad",
+    "sha256": "2742bd01c85c988cb4b8c13359839ce9e10672bde1a40c8bf668aae70b12c98d"
+  },
+  {
+    "path": "source/SOURCES.json",
+    "source_path": "research/e7-minimum-support-classification/SOURCES.json",
+    "source_commit": "700efb538a3d919409c9506d117846b7895b02ea",
+    "git_blob": "195cf52a31ad494b2a4444beaa2bf66f0c8942e8",
+    "sha256": "6281c850b2827c2d10624822c9fa2aed4f7ecf50e1c615777e72214aa568ecc6"
+  },
+  {
+    "path": "source/TASK.json",
+    "source_path": "research/e7-minimum-support-classification/TASK.json",
+    "source_commit": "700efb538a3d919409c9506d117846b7895b02ea",
+    "git_blob": "13006c1f4ba7804813bc5f3bfc8bfd4ce0d0159b",
+    "sha256": "42a96382145d816ca458c7dca7fd810f9823672606b9104c3f0bf404412546da"
+  },
+  {
+    "path": "source/VALIDATION.md",
+    "source_path": "research/e7-minimum-support-classification/VALIDATION.md",
+    "source_commit": "700efb538a3d919409c9506d117846b7895b02ea",
+    "git_blob": "a42933b4d67e268fdae8b1e8e68ace07d722f66f",
+    "sha256": "dcb04f1c258fcf7806c287388e33a02891d05db542021c069d4aea294f18808b"
+  },
+  {
+    "path": "source/VERIFY.json",
+    "source_path": "research/e7-minimum-support-classification/VERIFY.json",
+    "source_commit": "700efb538a3d919409c9506d117846b7895b02ea",
+    "git_blob": "6ecba772c6e44789d72258ece1ae816a76aff8bf",
+    "sha256": "370904ed6b746b34f7359cfb9e32fe642e7aa5923a16d62087cdf5e4dc389024"
+  },
+  {
+    "path": "source/vendor/PR5238.md",
+    "source_path": "research/e7-minimum-support-classification/vendor/PR5238.md",
+    "source_commit": "700efb538a3d919409c9506d117846b7895b02ea",
+    "git_blob": "5dc802961147c41af039e899d8baa3c8bb9e3909",
+    "sha256": "36e2263d28280043d6861caa4c81270be4800246e17647ec09da7cb4c2826085"
+  },
+  {
+    "path": "source/vendor/PR5238.py",
+    "source_path": "research/e7-minimum-support-classification/vendor/PR5238.py",
+    "source_commit": "700efb538a3d919409c9506d117846b7895b02ea",
+    "git_blob": "781a074d45126b1a84b92ee2393dc95790c0cb1b",
+    "sha256": "95502bb9e551302cbb0483097250441e96e5f858a5624745678875e3cedba9d2"
+  },
+  {
+    "path": "source/verify.py",
+    "source_path": "research/e7-minimum-support-classification/verify.py",
+    "source_commit": "700efb538a3d919409c9506d117846b7895b02ea",
+    "git_blob": "dc91e3362d7074d9655afc3b07109bff219f3572",
+    "sha256": "bac0023fe4a1d42af4c57412b7974158ca1a56b89da25c45e28b8e106e5b2649"
+  }
+]
diff --git a/research/e7-bitsliced-exhaustion/SOURCES.json b/research/e7-bitsliced-exhaustion/SOURCES.json
new file mode 100644
index 0000000000..bf3bc7dfc1
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/SOURCES.json
@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/PROOF.md",
+      "usage": "input",
+      "git_blob": "af4663e4a8465f2b653e83d1531da9e50dfbdd8b",
+      "sha256": "6749a3aba19ed159f0958c84918828f6da941aa2bebc4b0560ab2db9be11edb3",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/source/PROOF.md"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/README.md",
+      "usage": "input",
+      "git_blob": "ffb6879ecce8662247585479c300406fd6b971ba",
+      "sha256": "8f1519c6816eb6fb22f1779331299b3a18c087b30b967d05f5fb790d5cd1aa6b",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/source/README.md"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/RESULT.json",
+      "usage": "input",
+      "git_blob": "d32035693b23f114723c953c94370b349aa13cad",
+      "sha256": "2742bd01c85c988cb4b8c13359839ce9e10672bde1a40c8bf668aae70b12c98d",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/source/RESULT.json"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/SOURCES.json",
+      "usage": "input",
+      "git_blob": "195cf52a31ad494b2a4444beaa2bf66f0c8942e8",
+      "sha256": "6281c850b2827c2d10624822c9fa2aed4f7ecf50e1c615777e72214aa568ecc6",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/source/SOURCES.json"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/TASK.json",
+      "usage": "input",
+      "git_blob": "13006c1f4ba7804813bc5f3bfc8bfd4ce0d0159b",
+      "sha256": "42a96382145d816ca458c7dca7fd810f9823672606b9104c3f0bf404412546da",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/source/TASK.json"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/VALIDATION.md",
+      "usage": "input",
+      "git_blob": "a42933b4d67e268fdae8b1e8e68ace07d722f66f",
+      "sha256": "dcb04f1c258fcf7806c287388e33a02891d05db542021c069d4aea294f18808b",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/source/VALIDATION.md"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/VERIFY.json",
+      "usage": "input",
+      "git_blob": "6ecba772c6e44789d72258ece1ae816a76aff8bf",
+      "sha256": "370904ed6b746b34f7359cfb9e32fe642e7aa5923a16d62087cdf5e4dc389024",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/source/VERIFY.json"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/vendor/PR5238.md",
+      "usage": "input",
+      "git_blob": "5dc802961147c41af039e899d8baa3c8bb9e3909",
+      "sha256": "36e2263d28280043d6861caa4c81270be4800246e17647ec09da7cb4c2826085",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/source/vendor/PR5238.md"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/vendor/PR5238.py",
+      "usage": "input",
+      "git_blob": "781a074d45126b1a84b92ee2393dc95790c0cb1b",
+      "sha256": "95502bb9e551302cbb0483097250441e96e5f858a5624745678875e3cedba9d2",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/source/vendor/PR5238.py"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/source/verify.py",
+      "usage": "input",
+      "git_blob": "dc91e3362d7074d9655afc3b07109bff219f3572",
+      "sha256": "bac0023fe4a1d42af4c57412b7974158ca1a56b89da25c45e28b8e106e5b2649",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/source/verify.py"
+    },
+    {
+      "path": "research/e7-bitsliced-exhaustion/SOURCE-ORIGIN.json",
+      "usage": "input",
+      "git_blob": "62be5fa84d756296fc8d12a7434bb3711f90771d",
+      "sha256": "5927595aedd4299c8deaee531011e71b92230aea6e5b20f081674eddc4e82aef",
+      "pin": "head:1b853397390a537a3d63ed22976f8cc699743619:research/e7-bitsliced-exhaustion/SOURCE-ORIGIN.json"
+    }
+  ]
+}
diff --git a/research/e7-bitsliced-exhaustion/TASK.json b/research/e7-bitsliced-exhaustion/TASK.json
new file mode 100644
index 0000000000..8a2d452abc
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/TASK.json
@@ -0,0 +1,75 @@
+{
+  "schema_version": 1,
+  "task_id": "replay-runtime",
+  "priority_revision": 7,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "original_card": {
+    "id": "replay-runtime",
+    "question": "Can one measured replay bottleneck be sped up without dropping coverage?",
+    "starting_points": [
+      "scripts/run_isolated_tests.py",
+      "scripts/verify_replay_coverage.py",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Profile one isolated replay and optimize the measured bottleneck.",
+      "Design source-bound reuse with explicit dependency invalidation and negative controls."
+    ],
+    "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.",
+    "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.",
+    "allowed_variations": [
+      "Profile one stage or design one source-bound cache boundary."
+    ],
+    "scope_change_triggers": [
+      "Skipping coverage or comparing different fixtures to claim speedup."
+    ],
+    "overlap_terms": [
+      "replay runtime",
+      "cache invalidation",
+      "isolated tests"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Exact bit-lane enumeration of low-weight binary words, integrated into the complete pinned E7 classification replay.",
+  "scope_change_reason": "Refine the replay-runtime card to the binary frame-code census in PR5669.",
+  "bottleneck_link": "The full E7 support census is a dependency of E8 deletion and decoder certificates. Exact faster replay increases verification capacity without changing a physical bill.",
+  "budget_minutes": 120,
+  "stop_rule": "Require complete old/new result equality, unchanged downstream checks, exhaustive small-code oracles and a measured complete-replay speed gain. Reject on any mismatch.",
+  "outcome": "completed",
+  "evidence": "RESULT.json, BENCHMARK.json, PROOF.md and VALIDATION.md give exact scope, timings, checks and limits.",
+  "author": "Ali Romman with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance in implementation, proof, verification and prose. No subagents. Same assistant family as the consumed classifier; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Which larger deletion or decoder code census benefits from this exact iterator?",
+      "why_it_matters": "The present consumer is the complete E7 classification; another consumer needs its own correctness and runtime check.",
+      "first_step": "Bind one actual code basis and compare all checks and outputs before replacing its enumeration.",
+      "blocked_by": "No other consumer is installed by this package."
+    }
+  ],
+  "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19197143",
+  "expansion_decision": {
+    "decision": "Optimize the complete existing consumer and provide a general exact code iterator. Stop before a new geometry search.",
+    "proved_costs": "All coefficient assignments remain covered; finite storage and Boolean arithmetic costs are explicit.",
+    "unknowns": "No physical supplier, native-cost change, whole-caller benefit or new kappa is inferred."
+  },
+  "freshness": {
+    "main": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+    "checked_utc": "2026-10-26T14:30:44Z",
+    "open_prs": 404,
+    "discussion_records": 5072,
+    "main_notes": 7676,
+    "scope": "No competing E7 bit-lane optimization within searched public coverage."
+  }
+}
diff --git a/research/e7-bitsliced-exhaustion/VALIDATION.md b/research/e7-bitsliced-exhaustion/VALIDATION.md
new file mode 100644
index 0000000000..5d4575c9c8
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/VALIDATION.md
@@ -0,0 +1,74 @@
+# Validation and limits
+
+Base: canonical main df0137efd35e11b4445734bf612bdd4c7ebc330c, priority 7,
+selected conditional kappa 0.00310045. The current source-binding baseline
+passes. It does not constitute a selected cold replay.
+
+The consumed classifier is PR5669 at
+700efb538a3d919409c9506d117846b7895b02ea. All ten original files are retained
+byte for byte. SOURCE-ORIGIN.json maps their original paths and hashes.
+SOURCES.json binds these files and that map to retention commit
+1b853397390a537a3d63ed22976f8cc699743619.
+
+## Scientific checks
+
+Python 3.12.14 passes the complete new verifier. It covers 34,525 comparisons
+across every independent unordered generator set in F2^4, all weight bounds
+and five batch sizes; 108 wide-code comparisons; 13 malformed inputs and
+three changed-input/bound controls; the full original scientific receipt; and
+a second full E7 basis. The original source also passes unchanged on
+Python 3.14.7. No skipped source check or runtime function replacement occurs.
+
+The syntax comparison confirms that the derived classifier changes only its
+source-root expression and minimum-support function. Every downstream check
+and every source-receipt field remains active. RESULT.json records the exact
+normal result and support digest.
+
+## Complete replay timing
+
+BENCHMARK.json records six serial fresh Python 3.12.14 processes, in the
+order old,new,new,old,old,new. All use -I -B. Each process runs the complete
+classification and verifies its fixed receipt. All six stdout hashes match,
+and all stderr streams are empty.
+
+The old times are 15.090499, 13.816090, 13.724912 seconds. The new times are
+0.788342, 0.887017, 0.723674 seconds. The median ratio is 17.525510662.
+These are local macOS arm64 measurements. They compare the same complete
+scientific replay, not the extra generic-code conformance suite. They do
+not establish a universal hardware ratio or a multiplication speedup.
+
+## Remaining limits
+
+This checkout is shallow. Full-history publication preflight is unavailable;
+exact source bytes and immediate retained-source ancestry are checked.
+No selected cold replay, all-history suite, native/outer supplier admission,
+Lean build, independent human review or proof-kernel acceptance is claimed.
+No physical word or invoice changes, so no new kappa follows.
+
+The shared current-main CI navigation defect has existing repair PRs 5659
+and 5703. Hosted checks must be reported separately from local checks.
+
+## Registered replay
+
+The registered Python 3.12.14 command passes all declared checks and ends
+with PASS_REGISTERED_RESEARCH_PACKAGE. The normal result equals RESULT.json.
+The complete source classification is unchanged. No locally declared command
+is omitted.
+
+## Isolated export and final overlap
+
+The official committed-byte and export checks pass for all 23 package files
+at scientific commit 5c5aa5674885a81b11d301bd393481843ff3c266.
+The exported package passes Python 3.12.14 with -I -O -B, no Git directory,
+an empty executable PATH and read-only files. All 24 exported files retain
+their bytes and permissions. An actual changed source input is rejected
+before the full replay; its bytes are restored before that replay.
+
+The final remote refresh covers 404 open PRs and 5,072 Discussion records
+at 2026-10-26T14:30:44Z. All 7,676 main package notes are searched. A separate
+recent-body scan finds no competing E7 bit-lane optimization. The live source
+head is still the consumed commit. Canonical main remains unchanged. Closed
+unretained and unpublished work are outside this coverage.
+
+The final evidence commit changes documentation and coordination metadata
+only. Scientific code and source inputs are unchanged from the isolated run.
diff --git a/research/e7-bitsliced-exhaustion/VERIFY.json b/research/e7-bitsliced-exhaustion/VERIFY.json
new file mode 100644
index 0000000000..0bd950300d
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/VERIFY.json
@@ -0,0 +1,31 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/e7-bitsliced-exhaustion/source/PROOF.md",
+    "research/e7-bitsliced-exhaustion/source/README.md",
+    "research/e7-bitsliced-exhaustion/source/RESULT.json",
+    "research/e7-bitsliced-exhaustion/source/SOURCES.json",
+    "research/e7-bitsliced-exhaustion/source/TASK.json",
+    "research/e7-bitsliced-exhaustion/source/VALIDATION.md",
+    "research/e7-bitsliced-exhaustion/source/VERIFY.json",
+    "research/e7-bitsliced-exhaustion/source/vendor/PR5238.md",
+    "research/e7-bitsliced-exhaustion/source/vendor/PR5238.py",
+    "research/e7-bitsliced-exhaustion/source/verify.py",
+    "research/e7-bitsliced-exhaustion/SOURCE-ORIGIN.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "All 34525 four-coordinate code comparisons, wide and malformed controls, exact source authentication, complete E7 classification and basis change."
+    }
+  ]
+}
diff --git a/research/e7-bitsliced-exhaustion/benchmark.py b/research/e7-bitsliced-exhaustion/benchmark.py
new file mode 100644
index 0000000000..adfa559b40
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/benchmark.py
@@ -0,0 +1,47 @@
+"""Compare complete fresh E7 replays. Ali Romman with OpenAI Codex. Apache-2.0."""
+import argparse
+from hashlib import sha256
+import json
+from pathlib import Path
+import platform
+from runpy import run_path
+import statistics
+import subprocess
+import sys
+import time
+
+HERE = Path(__file__).resolve().parent
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--output', required=True, type=Path)
+    args = parser.parse_args()
+    run_path(str(HERE / 'verify.py'))['authenticate']()
+    records = []
+    for label in ('old', 'new', 'new', 'old', 'old', 'new'):
+        entry = HERE / ('source/verify.py' if label == 'old' else 'classify.py')
+        start = time.perf_counter()
+        result = subprocess.run([sys.executable, '-I', '-B', str(entry)],
+                                capture_output=True, check=True, timeout=180)
+        seconds = time.perf_counter() - start
+        if not result.stdout.startswith(b'PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION\n'):
+            raise ValueError('Missing complete classification result')
+        record = dict(implementation=label, seconds=seconds,
+                      stdout_sha256=sha256(result.stdout).hexdigest(),
+                      stderr_sha256=sha256(result.stderr).hexdigest())
+        records.append(record)
+        print(json.dumps(record), flush=True)
+    if len({row['stdout_sha256'] for row in records}) != 1:
+        raise ValueError('Scientific output differs')
+    medians = {name: statistics.median(row['seconds'] for row in records
+                                      if row['implementation'] == name)
+               for name in ('old', 'new')}
+    receipt = dict(python=sys.version, platform=platform.platform(),
+                   command_flags=['-I', '-B'], serial=True, records=records,
+                   median_seconds=medians, speed_ratio=medians['old'] / medians['new'])
+    args.output.write_text(json.dumps(receipt, indent=2) + '\n', encoding='utf-8')
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/e7-bitsliced-exhaustion/binary.py b/research/e7-bitsliced-exhaustion/binary.py
new file mode 100644
index 0000000000..cad9fc43ec
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/binary.py
@@ -0,0 +1,104 @@
+"""Exact low-weight binary words. Ali Romman with OpenAI Codex. Apache-2.0."""
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def population_planes(values):
+    """Add one-bit lanes without a carry between lanes."""
+    buckets = [list(values)]
+    output = []
+    while buckets:
+        current = buckets.pop()
+        carry = []
+        while len(current) >= 3:
+            a, b, c = current.pop(), current.pop(), current.pop()
+            parity = a ^ b
+            current.append(parity ^ c)
+            carry.append((a & b) | (parity & c))
+        if len(current) == 2:
+            a, b = current
+            output.append(a ^ b)
+            carry.append(a & b)
+        else:
+            output.append(current[0] if current else 0)
+        if carry:
+            buckets.append(carry)
+    return output
+
+
+def at_most(planes, bound, mask):
+    """Return exactly the lanes whose nonnegative integer is at most bound."""
+    if bound >= (1 << len(planes)) - 1:
+        return mask
+    equal, less = mask, 0
+    for power in range(len(planes) - 1, -1, -1):
+        bits = planes[power]
+        if bound >> power & 1:
+            less |= equal & ~bits
+            equal &= bits
+        else:
+            equal &= ~bits
+    return (less | equal) & mask
+
+
+def low_weight_words(generators, width, maximum, batch_bits=16):
+    """Yield every word once, including zero, from independent binary rows.
+
+    Each row is a nonnegative integer with at most width bits. The memory for
+    bit planes is O(width * 2^min(batch_bits, dimension)) bits. There are no
+    cached results. Batch size changes storage and runtime, not the code.
+    """
+    require(type(width) is int and width >= 0, 'width must be a nonnegative integer')
+    require(type(maximum) is int and 0 <= maximum <= width, 'invalid weight bound')
+    require(type(batch_bits) is int and 1 <= batch_bits <= 20, 'batch bits must be in 1..20')
+    rows = tuple(generators)
+    pivots = {}
+    for row in rows:
+        require(type(row) is int and row >= 0 and row.bit_length() <= width,
+                'invalid binary generator')
+        reduced = row
+        while reduced:
+            pivot = reduced.bit_length() - 1
+            if pivot not in pivots:
+                pivots[pivot] = reduced
+                break
+            reduced ^= pivots[pivot]
+        require(reduced != 0, 'binary generators must be independent')
+    count = min(batch_bits, len(rows))
+    lanes = 1 << count
+    mask = (1 << lanes) - 1
+    patterns = []
+    for bit in range(count):
+        block = 1 << bit
+        repetitions = mask // ((1 << (2 * block)) - 1)
+        patterns.append(repetitions * (((1 << block) - 1) << block))
+    columns = [0] * width
+    for row, pattern in zip(rows[:count], patterns):
+        while row:
+            bit = row & -row
+            columns[bit.bit_length() - 1] ^= pattern
+            row ^= bit
+    offset = 0
+    for index in range(1 << (len(rows) - count)):
+        if index:
+            offset ^= rows[count + (index & -index).bit_length() - 1]
+        values = list(columns)
+        bits = offset
+        while bits:
+            bit = bits & -bits
+            values[bit.bit_length() - 1] ^= mask
+            bits ^= bit
+        hits = at_most(population_planes(values), maximum, mask)
+        while hits:
+            bit = hits & -hits
+            coefficient = bit.bit_length() - 1
+            word = offset
+            while coefficient:
+                chosen = coefficient & -coefficient
+                word ^= rows[chosen.bit_length() - 1]
+                coefficient ^= chosen
+            yield word
+            hits ^= bit
diff --git a/research/e7-bitsliced-exhaustion/classify.py b/research/e7-bitsliced-exhaustion/classify.py
new file mode 100644
index 0000000000..3c14a223ae
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/classify.py
@@ -0,0 +1,194 @@
+#!/usr/bin/env python3
+"""Classify minimum E7 supports. Ali Romman with OpenAI Codex. Apache-2.0."""
+from fractions import Fraction as F
+from hashlib import sha256
+from pathlib import Path
+from runpy import run_path
+import json
+
+HERE = Path(__file__).resolve().parent / 'source'
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def geometry():
+    manifest = json.loads((HERE / 'SOURCES.json').read_text())
+    for row in manifest['external_inputs']:
+        need(sha256((HERE / row['local_path']).read_bytes()).hexdigest()
+             == row['sha256'], 'retained source changed')
+    return run_path(str(HERE / 'vendor/PR5238.py'), run_name='retained_geometry')
+
+
+def rank(rows):
+    basis = {}
+    for row in rows:
+        row = list(map(F, row))
+        for p, b in basis.items():
+            c = row[p]
+            if c:
+                row = [x-c*y for x, y in zip(row, b)]
+        p = next((i for i, x in enumerate(row) if x), None)
+        if p is not None:
+            c = row[p]
+            basis[p] = [x/c for x in row]
+    return len(basis)
+
+
+def minimum_supports(basis):
+    engine = run_path(str(HERE.parent / 'binary.py'))
+    words = set(engine['low_weight_words'](basis, 63, 12))
+    need(0 in words, 'zero word retained')
+    supports = words - {0}
+    need(len(supports) == 1638 and all(word.bit_count() == 12 for word in supports),
+         'complete minimum census')
+    return supports
+
+
+def reflections(roots, frames, dot):
+    lookup = {r: i for i, r in enumerate(roots)}
+    frame_set = set(frames)
+    out = []
+    for normal in roots:
+        p = []
+        for r in roots:
+            inner = dot(r, normal)
+            need(inner % 4 == 0, 'integral reflection')
+            image = tuple(r[i]-inner//4*normal[i] for i in range(8))
+            if next(x for x in image if x) < 0:
+                image = tuple(-x for x in image)
+            need(image in lookup, 'root reflection closure')
+            p.append(lookup[image])
+        need(sorted(p) == list(range(63)), 'root permutation')
+        need(all(tuple(sorted(p[j] for j in frame)) in frame_set
+                 for frame in frames), 'frame reflection closure')
+        out.append(tuple(p))
+    return out
+
+
+def transport(mask, permutation):
+    image = 0
+    while mask:
+        bit = mask & -mask
+        image |= 1 << permutation[bit.bit_length()-1]
+        mask ^= bit
+    return image
+
+
+def orbit(mask, permutations):
+    seen, queue = {mask}, [mask]
+    for current in queue:
+        for p in permutations:
+            image = transport(current, p)
+            if image not in seen:
+                seen.add(image)
+                queue.append(image)
+    return seen
+
+
+def form_a(x):
+    return sum(x[i]*x[i] for i in range(4))-sum(x[i]*x[i] for i in range(4, 8))
+
+
+def form_b(x):
+    return (x[0]-x[1])*(x[2]-x[3])
+
+
+def quadratic_matrix(form):
+    vectors = []
+    for i in (1, 2, 3, 5, 6, 7):
+        x = [0]*8
+        x[i] = 1
+        vectors.append(x)
+    vectors.append([1, 0, 0, 0, -1, 0, 0, 0])
+    matrix = [[F(form([x+y for x, y in zip(a, b)])-form(a)-form(b), 2)
+               for b in vectors] for a in vectors]
+    need(sum(matrix[i][i] for i in range(6))+matrix[6][6]/2 == 0,
+         'restricted trace zero')
+    return matrix
+
+
+def supported_rank(frames, support):
+    return rank([[int(j in frame) for j in support] for frame in frames])
+
+
+def check_relation(frames, values):
+    need(sum(x != 0 for x in values) == 12, 'twelve nonzero values')
+    need(all(sum(values[j] for j in frame) == 0 for frame in frames),
+         'literal rational frame sums')
+
+
+def partition(supports, orbits):
+    need(not orbits[0] & orbits[1], 'disjoint equality orbits')
+    need(orbits[0] | orbits[1] == supports, 'every minimum support classified')
+
+
+def reject(fn):
+    try:
+        fn()
+    except ValueError:
+        return
+    raise ValueError('invalid control accepted')
+
+
+def check():
+    g = geometry()
+    roots = g['intrinsic_e7']()
+    g['validate_domain'](roots)
+    need(roots == tuple(r for r in g['e8_lines']() if g['dot'](r, g['PIVOT']) == 0),
+         'ambient and intrinsic domains agree')
+    need(g['check_root_transitivity']() == 120, 'every ambient root slice')
+    frames = g['orthogonal_frames'](roots)
+    rows = tuple(sum(1 << j for j in frame) for frame in frames)
+    basis, free = g['binary_kernel'](rows)
+    supports = minimum_supports(basis)
+    permutations = reflections(roots, frames, g['dot'])
+    orbits, records, controls = [], [], 0
+    for name, form, size, qrank, scale in (
+            ('diagonal', form_a, 630, 6, 8), ('product', form_b, 1008, 2, 4)):
+        values = tuple(form(r) for r in roots)
+        check_relation(frames, values)
+        need(set(values) == {-scale, 0, scale}, 'constant nonzero magnitudes')
+        need(values.count(scale) == values.count(-scale) == 6, 'six values of each sign')
+        support = [j for j, x in enumerate(values) if x]
+        mask = sum(1 << j for j in support)
+        current = orbit(mask, permutations)
+        need(len(current) == size and current <= supports, 'complete attained orbit')
+        need(supported_rank(frames, support) == 11, 'one-dimensional rational lift')
+        need(rank(quadratic_matrix(form)) == qrank, 'quadratic rank')
+        for omitted in support:
+            need(supported_rank(frames, [j for j in support if j != omitted]) == 11,
+                 'every single omission has zero kernel')
+            controls += 1
+        changed = list(values)
+        changed[support[0]] += 1
+        reject(lambda: check_relation(frames, changed))
+        controls += 1
+        orbits.append(current)
+        records.append(dict(type=name, supports=size, representative_support=support,
+                            representative_values=list(values), quadratic_rank=qrank,
+                            restricted_frame_rank=11, rational_lift_dimension=1,
+                            orbit_sha256=sha256(json.dumps(sorted(current)).encode()).hexdigest()))
+    partition(supports, orbits)
+    reject(lambda: partition(supports-{next(iter(supports))}, orbits))
+    reject(lambda: partition(supports, [orbits[0], orbits[1] | orbits[0]]))
+    controls += 2
+    return dict(status='PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION', root_lines=63,
+                frames=135, binary_rank=36, binary_dimension=27,
+                nonzero_codewords=(1 << 27)-1, minimum_support=12,
+                minimum_supports=len(supports), reflection_generators=len(permutations),
+                ambient_root_slices=120, characteristic='zero', orbits=records,
+                rejecting_or_omission_controls=controls)
+
+
+def main():
+    result = check()
+    need(result == json.loads((HERE / 'RESULT.json').read_text()), 'fixed result receipt')
+    print(result['status'])
+    print('1638 minimum supports = 630 rank-six + 1008 rank-two; one scalar family per support')
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/e7-bitsliced-exhaustion/source/PROOF.md b/research/e7-bitsliced-exhaustion/source/PROOF.md
new file mode 100644
index 0000000000..af4663e4a8
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/source/PROOF.md
@@ -0,0 +1,130 @@
+# Equality in the E7 support bound
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+The source geometry and support bound are due to Nick Petalas, PR5238.
+
+## Statement
+
+Use doubled E8 roots, with squared norm eight. Fix
+`a=(2,0,0,0,2,0,0,0)`. Let R be the 63 root lines perpendicular to a,
+with one root on each line. Let H be the incidence matrix of all 135
+orthogonal seven-line frames in R. Let K be any field of characteristic zero.
+
+A nonzero function f:R -> K with Hf=0 has support at least twelve.
+If its support has size twelve, there are exactly two possibilities up to
+a nonzero scalar and E7 root reflections. Representatives are the
+restrictions to a-perp of
+
+```
+A(x) = x0^2+x1^2+x2^2+x3^2-x4^2-x5^2-x6^2-x7^2,
+B(x) = (x0-x1)(x2-x3).
+```
+
+The support orbit of A has 630 members. The support orbit of B has 1008
+members. They are disjoint and include all 1638 minimum supports. Each
+support admits exactly one scalar family of frame relations. Every such
+relation is the evaluation of a trace-zero quadratic. The two quadratic
+ranks on a-perp are six and two. Thus the two types cannot be identified
+by any orthogonal map and nonzero scalar.
+
+The same statement holds on the perpendicular slice of any E8 root,
+by rational orthogonal transport. It also classifies every trace-zero
+quadratic that attains support twelve. The zero quadratic is excluded.
+
+## Finite certificate and its completeness
+
+The retained PR5238 code constructs the 63 roots in two ways, constructs all
+135 frames by increasing orthogonal cliques, and computes a binary kernel
+basis of dimension 27. Its free-coordinate submatrix is the identity.
+Each basis vector has zero parity on every frame. These checks prove that
+all binary frame relations are in the generated code.
+
+The new checker traverses all 2^27-1 nonzero coefficient vectors in Gray
+order. It uses every basis direction at its prescribed toggle. Independence
+makes the resulting codewords distinct and nonzero. The minimum weight is
+twelve. Exactly 1638 distinct supports have this weight. No saved support
+list or numerical rank test supplies this result.
+
+For each root r in R, the map
+
+```
+s_r(x) = x - (x dot r) r / 4
+```
+
+is an orthogonal reflection because r dot r=8. It fixes a. The checker
+constructs its exact permutation of R and checks its action on every frame.
+These 63 maps generate the E7 reflection action used here. Breadth-first
+closure of the two representative supports gives sets of sizes 630 and
+1008. Their union is exactly the exhaustive minimum-support set, and their
+intersection is empty. This proves coverage; it does not require an assumed
+Weyl-group order or an external group catalogue.
+
+The evaluations of A are six +8 values, six -8 values, and 51 zeros.
+The evaluations of B are six +4 values, six -4 values, and 51 zeros.
+The checker verifies all 135 frame sums for both vectors. Exact rational
+elimination gives rank eleven for H restricted to either representative
+support. Therefore each restricted kernel has dimension one. Reflection
+transport gives the same rank and a nonzero quadratic lift on every support.
+As a separate check, removal of any one coordinate from either support gives
+column rank eleven and no nonzero relation.
+
+## From the binary certificate to characteristic zero
+
+First let f be rational and nonzero with Hf=0. Clear denominators and divide
+all entries by their greatest common divisor. The result is a primitive
+integer relation. Its reduction modulo two is nonzero, lies in the binary
+kernel, and has support contained in that of f. Thus f has support at least
+twelve. If f has support twelve, its binary reduction must have the same
+support, which is in the two checked orbits. This is the PR5238 reduction,
+now used with the full equality list.
+
+Now let f have values in any characteristic-zero field K, and let S be its
+support. The integer matrix H restricted to S has the same rank over Q and
+K: its nonzero rational minors stay nonzero in K. A nonzero K-kernel therefore
+implies a nonzero rational kernel. A rational vector in that kernel has
+support at most |S|, so the rational lower bound gives |S| >= 12.
+
+If |S|=12, any nonzero rational kernel vector has support exactly S. The
+previous paragraph puts S in the two orbits. The checked restricted rank
+is eleven over Q and hence over K. The K-kernel is the scalar span of the
+transported representative. This proves the stated classification for
+arbitrary characteristic zero, without reduction of K itself modulo two.
+
+## Quadratic interpretation
+
+On a-perp, set y=x0=-x4 and use the other coordinates
+`x1,x2,x3,x5,x6,x7`. The Euclidean metric in this basis is
+`diag(1,1,1,1,1,1,2)`. The trace of a quadratic matrix M in these coordinates
+is the sum of its first six diagonal entries plus M_yy/2.
+Both representatives have trace zero. Exact polarization gives ranks six
+and two. A frame is an orthogonal basis of a-perp of equal squared length,
+so every trace-zero quadratic gives a frame relation.
+
+The quadratic evaluation map is injective in characteristic zero. On the
+six ordinary coordinates, the roots `2e_i +/- 2e_j` force all mixed
+coefficients to zero and every pair of diagonal coefficients to sum to zero.
+Three indices force all six diagonal coefficients to zero. The root
+`2e0-2e4` then kills the y-square term. Only y times a linear form in the
+six coordinates remains. The 32 odd-parity sign rows have Gram matrix
+32I, so their evaluations kill all six remaining coefficients. These are
+exact identities over Q and remain valid in every characteristic-zero field.
+This is the injectivity argument retained from PR5238.
+
+Thus the relation classification gives the quadratic classification as well.
+The retained nine ambient generators preserve the E8 roots and move a to
+all 120 root lines. They are rational orthogonal maps. This transports the
+whole result to every root slice.
+
+## Relevance and limits
+
+This resolves PR5238's equality-classification question. Sparse incidence
+failures at the twelve-line threshold have two explicit quadratic types;
+a diagonal balanced-pair ansatz alone misses the rank-two type. A future
+sharp deletion-boundary proof can now use a complete equality list.
+
+The arbitrary-deletion extension statement in Discussion1502 remains open.
+This result does not prove it, the seven-deletion incidence implication,
+a decoder cost floor, a physical supplier, or an improvement in complete
+kappa. The selected metadata still has conditional kappa 0.00310045, with
+the main transform as its limiting outer row. No formal proof kernel or
+independent human review is claimed.
diff --git a/research/e7-bitsliced-exhaustion/source/README.md b/research/e7-bitsliced-exhaustion/source/README.md
new file mode 100644
index 0000000000..ffb6879ecc
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/source/README.md
@@ -0,0 +1,77 @@
+# All minimum E7 frame relations: two quadratic types
+
+There are exactly **1638** twelve-line supports for a nonzero characteristic-zero
+E7 frame relation. They form **two** root-reflection orbits, of sizes **630**
+and **1008**. Each support has one scalar family of relations. Both families
+are trace-zero quadratics, of ranks six and two. This completes the equality
+question left by Nick Petalas's PR5238. No new kappa is claimed.
+
+[PROOF.md](PROOF.md) gives the exact statement and the characteristic-zero
+argument. [RESULT.json](RESULT.json) gives the representatives, orbit hashes,
+ranks and coverage. [SOURCES.json](SOURCES.json) pins the retained geometry
+and predecessor proof. [verify.py](verify.py) recomputes the full census.
+
+For the slice perpendicular to `(2,0,0,0,2,0,0,0)`, representatives are
+`x0^2+x1^2+x2^2+x3^2-x4^2-x5^2-x6^2-x7^2` and
+`(x0-x1)(x2-x3)`. Their nonzero evaluations have equal magnitude, with six
+of each sign. Rational orthogonal transport covers every E8 root slice.
+
+## Why this helps the decoder work
+
+PR5238 proves minimum support twelve but leaves equality open. The new
+classification supplies all sparse equality obstructions at that boundary.
+It also shows that the diagonal type alone does not cover all obstructions.
+It does not supply the separate arbitrary-deletion extension lemma in the
+[released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19145642).
+No decoder floor or physical caller follows without that missing implication.
+
+## Verification
+
+Python 3.12 and its standard library suffice.
+
+```
+python3.12 -B scripts/research_package.py --package research/e7-minimum-support-classification
+python3.12 -B scripts/check_research_commit.py --package research/e7-minimum-support-classification
+```
+
+Expected: `PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION`,
+`PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`.
+The normal and optimized checks each enumerate all 134217727 nonzero binary
+codewords. They check all 63 reflection generators on all 135 frames, the
+complete two-orbit partition, exact rational lift ranks, quadratic ranks,
+ambient transport, 24 coordinate omissions and four corruption controls.
+The verifier authenticates retained sources before it executes them.
+It writes no source file. The registered time cap is 600 seconds per mode.
+
+The same assistant supplied the proof and checker. These are exact finite
+checks plus a written proof, not independent human or formal acceptance.
+No native or selected cold replay, outer admission, full historical suite,
+Lean or Docker run was used. Full source-history preflight is unavailable
+in this shallow checkout; exact bytes and immediate source ancestry are
+separate checks. Selected files are unchanged.
+
+## Open next questions
+
+1. Does every live-frame relation after at most seven P112 deletions extend
+   to an ambient trace-zero quadratic? Retain all deletion quantifiers.
+   The equality classification does not prove this separate extension.
+2. At the next incidence boundary, which of the two equality types is
+   compatible with the literal deleted frame and pivot conditions? Start
+   from the two explicit representatives and charge every omitted line.
+   No new deletion census or reservation is made here.
+
+## Credit and scope
+
+Nick Petalas's [PR5238](https://github.com/CrocSwap/integer-mult-bounds/pull/5238)
+supplies the minimum bound, root and frame code, and quadratic injectivity.
+Its source files are retained byte for byte, with all source notices.
+The originating handoff is JoyboyBrian's. The retained lineage includes
+Josie Elliston, Andrey Mas, Aaron Wang, Brett Halligan, themilkman216 and
+DreamingOfClouds; their individual contributions remain in the source note.
+New equality census, orbit classification, characteristic-zero extension,
+proof and checks: Ali Romman with substantial OpenAI Codex assistance.
+Apache-2.0.
+
+Canonical base: `df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority revision 7.
+The selected source check passes at conditional kappa 0.00310045. This package
+changes no selected result and reserves no physical construction.
diff --git a/research/e7-bitsliced-exhaustion/source/RESULT.json b/research/e7-bitsliced-exhaustion/source/RESULT.json
new file mode 100644
index 0000000000..d32035693b
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/source/RESULT.json
@@ -0,0 +1,190 @@
+{
+  "ambient_root_slices": 120,
+  "binary_dimension": 27,
+  "binary_rank": 36,
+  "characteristic": "zero",
+  "frames": 135,
+  "minimum_support": 12,
+  "minimum_supports": 1638,
+  "nonzero_codewords": 134217727,
+  "orbits": [
+    {
+      "orbit_sha256": "d08f659fab919baab7b2c87c0b7e55edb5a3e23e05a313522f0b17e684d8ee39",
+      "quadratic_rank": 6,
+      "rational_lift_dimension": 1,
+      "representative_support": [
+        0,
+        1,
+        2,
+        3,
+        4,
+        5,
+        12,
+        19,
+        20,
+        21,
+        28,
+        29
+      ],
+      "representative_values": [
+        -8,
+        -8,
+        -8,
+        -8,
+        -8,
+        -8,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        8,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        8,
+        8,
+        8,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        8,
+        8,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "restricted_frame_rank": 11,
+      "supports": 630,
+      "type": "diagonal"
+    },
+    {
+      "orbit_sha256": "a9bb36def7396f184d343e38f410d705a50be3188b40725235f866ad0753309b",
+      "quadratic_rank": 2,
+      "rational_lift_dimension": 1,
+      "representative_support": [
+        20,
+        21,
+        28,
+        29,
+        34,
+        35,
+        36,
+        37,
+        38,
+        39,
+        40,
+        41
+      ],
+      "representative_values": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        4,
+        -4,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        4,
+        -4,
+        0,
+        0,
+        0,
+        0,
+        -4,
+        -4,
+        -4,
+        -4,
+        4,
+        4,
+        4,
+        4,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "restricted_frame_rank": 11,
+      "supports": 1008,
+      "type": "product"
+    }
+  ],
+  "reflection_generators": 63,
+  "rejecting_or_omission_controls": 28,
+  "root_lines": 63,
+  "status": "PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION"
+}
diff --git a/research/e7-bitsliced-exhaustion/source/SOURCES.json b/research/e7-bitsliced-exhaustion/source/SOURCES.json
new file mode 100644
index 0000000000..195cf52a31
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/source/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "research/e7-minimum-support-classification/vendor/PR5238.py",
+      "usage": "input",
+      "git_blob": "781a074d45126b1a84b92ee2393dc95790c0cb1b",
+      "sha256": "95502bb9e551302cbb0483097250441e96e5f858a5624745678875e3cedba9d2",
+      "pin": "head:8be0f6dc6c8d704f1b9bbe3b497a3fdd6729408b:research/e7-minimum-support-classification/vendor/PR5238.py"
+    },
+    {
+      "path": "research/e7-minimum-support-classification/vendor/PR5238.md",
+      "usage": "input",
+      "git_blob": "5dc802961147c41af039e899d8baa3c8bb9e3909",
+      "sha256": "36e2263d28280043d6861caa4c81270be4800246e17647ec09da7cb4c2826085",
+      "pin": "head:8be0f6dc6c8d704f1b9bbe3b497a3fdd6729408b:research/e7-minimum-support-classification/vendor/PR5238.md"
+    }
+  ],
+  "external_inputs": [
+    {
+      "local_path": "vendor/PR5238.py",
+      "source_repository": "CrocSwap/integer-mult-bounds",
+      "source_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+      "source_path": "research/e7-quadratic-support/verify.py",
+      "sha256": "95502bb9e551302cbb0483097250441e96e5f858a5624745678875e3cedba9d2"
+    },
+    {
+      "local_path": "vendor/PR5238.md",
+      "source_repository": "CrocSwap/integer-mult-bounds",
+      "source_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+      "source_path": "research/e7-quadratic-support/README.md",
+      "sha256": "36e2263d28280043d6861caa4c81270be4800246e17647ec09da7cb4c2826085"
+    }
+  ]
+}
diff --git a/research/e7-bitsliced-exhaustion/source/TASK.json b/research/e7-bitsliced-exhaustion/source/TASK.json
new file mode 100644
index 0000000000..13006c1f4b
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/source/TASK.json
@@ -0,0 +1,89 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 7,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md",
+      "research/selected-k8-unrestricted-ends/README.md",
+      "research/eisenstein-reduction-copy-floor/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Classify all minimum-support E7 frame relations and trace-zero quadratics in characteristic zero.",
+  "scope_change_reason": "Take the explicit released equality question in PR5238. It is a structural prerequisite at the decoder-incidence boundary, not a physical supplier.",
+  "bottleneck_link": "Identify every sparse equality obstruction for the proposed sharp incidence boundary. The separate arbitrary-deletion extension is still needed.",
+  "budget_minutes": 120,
+  "stop_rule": "Complete the two-type equality classification. Do not expand into an unpriced decoder or duplicate the minimum-support theorem.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, RESULT.json and verify.py.",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance. The same assistant supplied the proof and checker; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Does the arbitrary-deletion quadratic extension hold?",
+      "why_it_matters": "It is the missing bridge to the seven-deletion incidence claim.",
+      "first_step": "Prove the extension with all deletion quantifiers retained.",
+      "blocked_by": "No uniform extension proof is supplied."
+    },
+    {
+      "question": "Which equality types meet the literal next-boundary deletion conditions?",
+      "why_it_matters": "The two complete orbit types restrict possible sparse obstructions.",
+      "first_step": "Compare the two representatives with the actual deleted-frame and pivot conditions.",
+      "blocked_by": "No new deletion classification is supplied."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19188245",
+    "nonce": "00770df06ad58b13ce127059b5948653",
+    "upstream": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+    "priority_revision": 7,
+    "overlap_utc": "2026-10-26T04:19:48.351555+00:00",
+    "local_notes": 7676,
+    "open_prs": 357,
+    "discussion_records": 4977,
+    "coverage": "All tracked main notes and complete cached PR/Discussion pagination; no unpublished-work coverage."
+  }
+}
diff --git a/research/e7-bitsliced-exhaustion/source/VALIDATION.md b/research/e7-bitsliced-exhaustion/source/VALIDATION.md
new file mode 100644
index 0000000000..a42933b4d6
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/source/VALIDATION.md
@@ -0,0 +1,28 @@
+# Validation record
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+
+The scientific package at `fb38d6b41cb2847f7ec92152d0a8bbe9cd6e803a` passed
+the registered normal and optimized checks with CPython 3.12.14. Both checks
+recomputed all 134217727 nonzero binary codewords and the exact two-orbit
+partition. The same fixed result passed in a read-only Git-free export under
+optimized Python, with an empty PATH. All ten exported files, including the
+export manifest, kept their hashes. A separate copy with one appended line
+in the retained source failed before execution with `retained source changed`.
+
+The nine package files passed committed-byte checks and official export
+validation at that science commit. The base and retention commit are verified
+ancestors. The final update adds this record and the refreshed coordination
+counts; it changes no scientific code, source or receipt. Final committed bytes
+and export integrity are checked separately before publication.
+
+Current main was refreshed to `df0137efd35e11b4445734bf612bdd4c7ebc330c`.
+Guidance, priorities, catalogue and selected record have no drift. The selected
+source check passes at conditional kappa 0.00310045. The final full cache has
+357 open PRs and 4977 Discussion records. The complete tracked-note inventory
+and targeted equality searches found only the predecessor and this claim.
+Unpublished work and arbitrary PR diffs are outside this coverage.
+
+No full-history source preflight was run in the shallow checkout. No selected
+cold replay, native supplier, outer admission, complete theorem, Lean, Docker
+or independent human review was run. CI status is not asserted here.
diff --git a/research/e7-bitsliced-exhaustion/source/VERIFY.json b/research/e7-bitsliced-exhaustion/source/VERIFY.json
new file mode 100644
index 0000000000..6ecba772c6
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/source/VERIFY.json
@@ -0,0 +1,31 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/e7-minimum-support-classification/vendor/PR5238.py",
+    "research/e7-minimum-support-classification/vendor/PR5238.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Exhaust all binary words; classify all minimum supports; check exact rational and quadratic ranks, reflections, transport and negative controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Exhaust all binary words; classify all minimum supports; check exact rational and quadratic ranks, reflections, transport and negative controls."
+    }
+  ]
+}
diff --git a/research/e7-bitsliced-exhaustion/source/vendor/PR5238.md b/research/e7-bitsliced-exhaustion/source/vendor/PR5238.md
new file mode 100644
index 0000000000..5dc8029611
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/source/vendor/PR5238.md
@@ -0,0 +1,178 @@
+# Sharp support twelve for trace-zero E7 quadratics
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Result and claim type
+
+**Scoped mathematical proof with an exact finite certificate.** Every nonzero
+rational trace-zero quadratic form on the seven-dimensional orthogonal
+complement of an E8 root is nonzero on at least **twelve** of its 63 root
+lines. Twelve is attained.
+
+This proves the trace-zero replacement for auxiliary statement (2) in
+[JoyboyBrian's released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19145642).
+The unrestricted statement there needs correction: products of two linear
+forms can have support eleven, as already follows from the 52-line two-flat
+union in DreamingOfClouds's #595 and DaysSky's
+[#897](https://github.com/CrocSwap/integer-mult-bounds/pull/897).
+DreamingOfClouds's open
+[#3045](https://github.com/CrocSwap/integer-mult-bounds/pull/3045)
+also records an E7 intersection of supports of size eleven. The eleven-line
+example first reported in this contribution's progress post is therefore
+credited to that existing coverage, not claimed as an original result.
+The new result is the sharp trace-zero bound and its frame-code certificate.
+
+The arbitrary-deletion quadratic extension in handoff statement (1) remains
+open. This package does not prove the seven-deletion rigidity shortcut.
+
+## Finite certificate
+
+Use doubled E8 roots, with canonical line representatives
+`2e_i +/- 2e_j`, `i < j`, and `(1,s_1,...,s_7)` with an even number of
+negative coordinates. All have squared norm eight. Coordinates run from zero
+through seven. Fix `a=2e_0+2e_4`, and let `R` be the 63 root lines in `a`-perp.
+An orthogonal frame consists of seven mutually orthogonal lines in `R`.
+
+The verifier constructs every frame by an increasing-clique traversal,
+retaining a branch only when enough candidates remain to complete it.
+It finds 135 frames. Their binary incidence matrix `H`, of shape `135 x 63`,
+has rank 36 and kernel dimension 27. The verifier constructs a kernel basis
+with an identity submatrix on its free coordinates, checks every basis vector
+against every row, and enumerates every one of its **134,217,727 nonzero
+vectors**. Their minimum Hamming weight is **12**.
+
+The enumeration uses a Gray traversal. At step `i`, toggling basis vector
+`v_((i & -i).bit_length()-1)` changes the coefficient vector to `i xor (i>>1)`.
+These coefficient vectors visit every nonzero element of `F2^27` once.
+The identity on the free coordinates proves that their images are distinct.
+The finite minimum is recomputed on every registered replay; no saved census
+or external solver is trusted.
+
+## Proof of the rational lower bound
+
+More generally, every nonzero rational function on `R` whose sum on every
+orthogonal frame is zero has support at least twelve. Clear its denominators
+and divide its integer values by their greatest common divisor. The resulting
+primitive integer vector still has zero frame sums, and its reduction modulo
+two is nonzero. That reduction lies in `ker(H)`, and its support is contained
+in the original support. The finite certificate therefore proves the bound.
+
+For a trace-zero quadratic `q`, every frame has zero sum: its seven roots
+are an orthogonal basis of `a`-perp with squared norm eight, so
+`sum(q(r): r in frame) = 8 trace(q) = 0`.
+It remains to check that a nonzero quadratic cannot vanish on all of `R`.
+Here is an elementary injectivity argument.
+
+Write `J={1,2,3,5,6,7}` and `y=x_0=-x_4` on `a`-perp. If a quadratic
+vanishes on every `2e_i +/- 2e_j`, with `i,j` in `J`, subtracting the two
+evaluations kills each mixed coefficient within `J`, and adding them shows
+that every pair of diagonal coefficients sums to zero. Three distinct indices
+then force all six diagonal coefficients to vanish over the rationals.
+The root `2e_0-2e_4` kills the coefficient of `y^2`. Only
+`y sum(b_i x_i: i in J)` remains. The 32 half-root lines have `y=1`, with
+all odd-parity six-sign rows `s`. These rows satisfy `sum(s s^T)=32 I_6`,
+so vanishing on them forces every `b_i=0`. Thus the original quadratic was zero.
+
+This proves the lower bound for the stated rational domain. To transport it
+to any E8 root, the verifier checks nine orthogonal root-set automorphisms:
+seven adjacent coordinate swaps, negation of coordinates zero and one, and
+reflection in `(1,-1,-1,-1,1,-1,-1,-1)`. Their orbit on `a` contains all
+120 root lines. Orthogonal rational transport preserves trace and support.
+
+## A twelve-line attainer
+
+Restrict
+
+\[
+ q_0(x)=x_0^2+x_1^2+x_2^2+x_3^2-x_4^2-x_5^2-x_6^2-x_7^2
+\]
+
+to `a`-perp. The ambient trace is zero and `q_0(a)=0`, so the restricted
+trace is zero. On `R`, the six coordinate-root lines within `{1,2,3}` have
+value `+8`, the six within `{5,6,7}` have value `-8`, and the other 51 lines
+have value zero. Indeed, cross-part coordinate roots cancel, `2e_0-2e_4`
+cancels, and every half-root has four positive and four negative square terms.
+The verifier checks the twelve nonzero values and all 135 literal frame sums.
+
+## Relation to the handoff and limits
+
+The delivered scope repairs the proposed auxiliary support statement by adding
+trace zero. If an ambient trace-zero quadratic vanishes on the pivot, its
+restriction to the pivot's orthogonal complement is trace-zero: in an
+orthonormal basis beginning with the pivot direction, that first diagonal
+entry and the total trace are both zero. The new lemma can therefore supply
+the support step in the handoff's proposed reduction, conditional on its
+separate arbitrary-deletion extension statement and the remaining hypotheses.
+
+The advance claim asked about the unrestricted statement. Semantic overlap
+checking identified the earlier eleven-line coverage before any commit.
+The original contribution delivered here is the trace-zero replacement.
+Neither the earlier flat census nor any predecessor's rigidity result is
+replayed or re-verified as this contribution.
+
+The binary minimum is a complete finite enumeration, not a formal proof-kernel
+certificate. The rational implication and injectivity argument are written
+proofs. Native realization, physical supplier admission, selected cold replay,
+Lean and the complete multiplication theorem are outside scope. No new kappa
+or selected-frontier change is claimed.
+
+## Reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/e7-quadratic-support/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/e7-quadratic-support/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e7-quadratic-support
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e7-quadratic-support --check-source-history
+```
+
+Another CPython 3.12 path can replace the local interpreter path.
+Expected status is `PASS_E7_TRACE_ZERO_SUPPORT`, with 63 lines, 135 frames,
+binary rank 36, dimension 27, 134217727 nonzero codewords, minimum weight 12,
+a quadratic attainer with six positive and six negative values, and 92
+rejecting controls. Normal and optimized modes use explicit checks, not assertions.
+
+The verifier constructs E8 and the intrinsic E7 slice separately and checks the
+root orbit. Omission controls reject every incomplete 63-line domain; basis
+controls reject every one-bit-corrupted basis vector and wrong dimensions.
+It uses bounded traversals, no recursion, and a constant-memory Gray census.
+Python runtime allocation is unavoidable; the stored geometry has only 120
+root lines, 135 frames and 27 kernel vectors. Optional
+`--receipt /absolute/path/outside/the/package.json` writes a generated receipt
+bound to all five package source hashes. Direct replay needs no Git or
+predecessor imports and writes nothing into its source package.
+
+## Open next questions
+
+1. Does every live-frame zero-sum rational function on P112 minus at most
+   seven lines extend to an ambient trace-zero quadratic? This is handoff
+   statement (1) and is the remaining uniform bridge in that reduction.
+   First prove an extension lemma retaining every deletion quantifier.
+   Its existing finite fixtures do not establish that implication.
+2. Which trace-zero quadratics attain support twelve? A classification could
+   identify all possible sparse equality obstructions. First determine the
+   rational kernels on the weight-twelve supports; no equality classification
+   is claimed or required for the present minimum.
+
+## Sources and credit
+
+The immediate question comes from
+[JoyboyBrian's released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19145642).
+The full-family shortcut and its eight-deletion counterexamples are Josie
+Elliston's [#1668](https://github.com/CrocSwap/integer-mult-bounds/pull/1668),
+following [#1650](https://github.com/CrocSwap/integer-mult-bounds/pull/1650)
+and [#1616](https://github.com/CrocSwap/integer-mult-bounds/pull/1616).
+Andrey Mas's [#1560](https://github.com/CrocSwap/integer-mult-bounds/pull/1560)
+supplies the incidence criterion. Aaron Wang's
+[#1649](https://github.com/CrocSwap/integer-mult-bounds/pull/1649) separates
+the subfamily question. DreamingOfClouds / #595 and #3045 and DaysSky / #897
+retain credit for the earlier unrestricted eleven-line support coverage.
+The retained E8 model and rigidity lineage credit Brett Halligan / #1212,
+themilkman216 / #968, and DreamingOfClouds / #717.
+
+These are motivation and provenance, not mathematical inputs to the new
+self-contained certificate. `SOURCES.json` pins the originating catalogue and
+predecessor notes at canonical main
+`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`.
diff --git a/research/e7-bitsliced-exhaustion/source/vendor/PR5238.py b/research/e7-bitsliced-exhaustion/source/vendor/PR5238.py
new file mode 100644
index 0000000000..781a074d45
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/source/vendor/PR5238.py
@@ -0,0 +1,262 @@
+#!/usr/bin/env python3
+"""Sharp support twelve for rational trace-zero E7 quadratics. Exact integers."""
+
+import argparse
+from collections import Counter
+import hashlib
+import itertools
+import json
+from pathlib import Path
+import platform
+
+
+PIVOT = (2, 0, 0, 0, 2, 0, 0, 0)
+DIAGONAL = (1, 1, 1, 1, -1, -1, -1, -1)
+N = 63
+DIMENSION = 27
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def dot(left, right):
+    require(len(left) == len(right) == 8, "eight coordinates required")
+    return sum(left[i] * right[i] for i in range(8))
+
+
+def e8_lines():
+    roots = []
+    for i, j in itertools.combinations(range(8), 2):
+        for sign in (-1, 1):
+            root = [0] * 8
+            root[i], root[j] = 2, 2 * sign
+            roots.append(tuple(root))
+    for tail in itertools.product((-1, 1), repeat=7):
+        root = (1,) + tail
+        if root.count(-1) % 2 == 0:
+            roots.append(root)
+    require(len(roots) == len(set(roots)) == 120, "E8 line count")
+    require(all(dot(root, root) == 8 for root in roots), "E8 norms")
+    return tuple(sorted(roots))
+
+
+def intrinsic_e7():
+    roots = []
+    for i, j in itertools.combinations((1, 2, 3, 5, 6, 7), 2):
+        for sign in (-1, 1):
+            root = [0] * 8
+            root[i], root[j] = 2, 2 * sign
+            roots.append(tuple(root))
+    roots.append((2, 0, 0, 0, -2, 0, 0, 0))
+    for signs in itertools.product((-1, 1), repeat=6):
+        if signs.count(-1) % 2 == 1:
+            roots.append((1,) + signs[:3] + (-1,) + signs[3:])
+    return tuple(sorted(roots))
+
+
+def validate_domain(roots):
+    require(len(roots) == len(set(roots)) == N, "63 distinct root lines")
+    require(tuple(sorted(roots)) == intrinsic_e7(), "intrinsic E7 agreement")
+    require(all(dot(PIVOT, root) == 0 for root in roots), "orthogonal slice")
+
+
+def root_transport(root, generator):
+    out = list(root)
+    if generator < 7:
+        out[generator], out[generator + 1] = out[generator + 1], out[generator]
+    elif generator == 7:
+        out[0], out[1] = -out[0], -out[1]
+    else:
+        require(generator == 8, "nine fixed orthogonal generators")
+        normal = (1, -1, -1, -1, 1, -1, -1, -1)
+        inner = dot(root, normal)
+        require(inner % 4 == 0, "integral E8 reflection")
+        out = [root[i] - inner // 4 * normal[i] for i in range(8)]
+    first = next(value for value in out if value)
+    return tuple(value if first > 0 else -value for value in out)
+
+
+def check_root_transitivity():
+    domain = set(e8_lines())
+    for generator, root in itertools.product(range(9), domain):
+        require(root_transport(root, generator) in domain, "root-set automorphism")
+    orbit = {PIVOT}
+    stack = [PIVOT]
+    for _ in range(120):
+        if not stack:
+            break
+        root = stack.pop()
+        for generator in range(9):
+            image = root_transport(root, generator)
+            if image not in orbit:
+                orbit.add(image)
+                stack.append(image)
+    require(not stack and orbit == domain, "all 120 root lines reached")
+    return len(orbit)
+
+
+def orthogonal_frames(roots):
+    adjacency = [{j for j in range(N) if j != i and dot(roots[i], roots[j]) == 0}
+                 for i in range(N)]
+    frames = []
+    stack = [((), tuple(range(N)))]
+    # Each state is an increasing orthogonal subset; 100000 is a fail-closed cap.
+    for _ in range(100000):
+        if not stack:
+            break
+        frame, candidates = stack.pop()
+        if len(frame) == 7:
+            frames.append(frame)
+            continue
+        for offset, j in enumerate(candidates):
+            tail = tuple(k for k in candidates[offset + 1:] if k in adjacency[j])
+            if len(tail) >= 6 - len(frame):
+                stack.append((frame + (j,), tail))
+    else:
+        raise ValueError("frame enumeration exceeded its state cap")
+    require(len(frames) == len(set(frames)) == 135, "135 complete frames")
+    for frame in frames:
+        require(len(frame) == 7 and all(j in adjacency[i] for i, j in
+                itertools.combinations(frame, 2)), "orthogonal frame")
+    return tuple(sorted(frames))
+
+
+def binary_kernel(rows):
+    echelon = {}
+    for row in rows:
+        for pivot in range(N - 1, -1, -1):
+            if row >> pivot & 1:
+                if pivot in echelon:
+                    row ^= echelon[pivot]
+                else:
+                    echelon[pivot] = row
+                    break
+    free = tuple(j for j in range(N) if j not in echelon)
+    basis = []
+    for j in free:
+        vector = 1 << j
+        for pivot in sorted(echelon):
+            if (echelon[pivot] & vector).bit_count() % 2:
+                vector |= 1 << pivot
+        basis.append(vector)
+    require(len(echelon) == 36 and len(free) == DIMENSION, "binary rank 36")
+    validate_basis(rows, basis, free)
+    return tuple(basis), free
+
+
+def validate_basis(rows, basis, free):
+    require(len(basis) == len(free) == DIMENSION, "complete kernel dimension")
+    require(len(set(free)) == DIMENSION, "distinct free coordinates")
+    for index, vector in enumerate(basis):
+        require(0 < vector < 1 << N, "bounded nonzero kernel vector")
+        require(all((vector & row).bit_count() % 2 == 0 for row in rows),
+                "every frame parity vanishes")
+        require(tuple(vector >> j & 1 for j in free) ==
+                tuple(int(k == index) for k in range(DIMENSION)),
+                "identity on free coordinates proves independence")
+
+
+def full_weight_census(basis):
+    word = 0
+    minimum = N
+    visited = 0
+    for index in range(1, 1 << DIMENSION):
+        word ^= basis[(index & -index).bit_length() - 1]
+        weight = word.bit_count()
+        require(weight != 0, "independent basis cannot revisit zero")
+        if weight < minimum:
+            minimum = weight
+        visited += 1
+    require(visited == 134217727, "every nonzero binary kernel vector visited")
+    require(minimum == 12, "binary frame code has minimum weight twelve")
+    return visited, minimum
+
+
+def check_witness(roots, frames):
+    values = tuple(sum(DIAGONAL[i] * root[i] ** 2 for i in range(8))
+                   for root in roots)
+    require(sum(DIAGONAL) == 0, "ambient quadratic has trace zero")
+    require(sum(DIAGONAL[i] * PIVOT[i] ** 2 for i in range(8)) == 0,
+            "pivot diagonal entry vanishes, so restricted trace is zero")
+    require(Counter(values) == {0: 51, 8: 6, -8: 6}, "twelve-line attainer")
+    require(all(sum(values[j] for j in frame) == 0 for frame in frames),
+            "literal rational frame sums vanish")
+    # Odd-parity six-sign rows span all six remaining coordinates. Together
+    # with coordinate +/- pairs and e0-e4, this proves quadratic injectivity.
+    signs = [tuple(root[j] for j in (1, 2, 3, 5, 6, 7))
+             for root in roots if root[0] == 1]
+    require(len(signs) == 32, "all odd-parity sign rows")
+    for i, j in itertools.product(range(6), repeat=2):
+        require(sum(row[i] * row[j] for row in signs) == 32 * int(i == j),
+                "sign-row Gram identity")
+    return values
+
+
+def rejection_controls(roots, rows, basis, free):
+    rejected = 0
+    for j in range(N):
+        try:
+            validate_domain(roots[:j] + roots[j + 1:])
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError("incomplete root domain accepted")
+    for j in range(DIMENSION):
+        changed = list(basis)
+        changed[j] ^= 1
+        try:
+            validate_basis(rows, changed, free)
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError("non-kernel basis accepted")
+    for changed in (basis[:-1], basis + (basis[0],)):
+        try:
+            validate_basis(rows, changed, free)
+        except ValueError:
+            rejected += 1
+        else:
+            raise ValueError("wrong kernel dimension accepted")
+    require(rejected == 92, "all 92 omission and basis controls executed")
+    return rejected
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--receipt", type=Path, help="write generated receipt outside package")
+    args = parser.parse_args()
+    orbit_size = check_root_transitivity()
+    roots = tuple(root for root in e8_lines() if dot(root, PIVOT) == 0)
+    validate_domain(roots)
+    frames = orthogonal_frames(roots)
+    rows = tuple(sum(1 << j for j in frame) for frame in frames)
+    basis, free = binary_kernel(rows)
+    values = check_witness(roots, frames)
+    controls = rejection_controls(roots, rows, basis, free)
+    visited, minimum = full_weight_census(basis)
+    package = Path(__file__).resolve().parent
+    files = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")
+    receipt = {
+        "status": "PASS_E7_TRACE_ZERO_SUPPORT", "e7_lines": len(roots),
+        "pivot_orbit": orbit_size,
+        "frames": len(frames), "binary_rank": N - len(basis),
+        "binary_kernel_dimension": len(basis), "nonzero_codewords": visited,
+        "minimum_binary_weight": minimum, "quadratic_support": sum(v != 0 for v in values),
+        "positive_values": sum(v > 0 for v in values),
+        "negative_values": sum(v < 0 for v in values), "rejecting_controls": controls,
+        "python": platform.python_version(),
+        "source_sha256": {name: hashlib.sha256((package / name).read_bytes()).hexdigest()
+                          for name in files},
+    }
+    serialized = json.dumps(receipt, indent=2, sort_keys=True) + "\n"
+    if args.receipt is not None:
+        require(not args.receipt.resolve().is_relative_to(package),
+                "receipt must be outside the source package")
+        args.receipt.write_text(serialized, encoding="utf-8")
+    print(serialized, end="")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/research/e7-bitsliced-exhaustion/source/verify.py b/research/e7-bitsliced-exhaustion/source/verify.py
new file mode 100644
index 0000000000..dc91e3362d
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/source/verify.py
@@ -0,0 +1,197 @@
+#!/usr/bin/env python3
+"""Classify minimum E7 supports. Ali Romman with OpenAI Codex. Apache-2.0."""
+from fractions import Fraction as F
+from hashlib import sha256
+from pathlib import Path
+from runpy import run_path
+import json
+
+HERE = Path(__file__).resolve().parent
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def geometry():
+    manifest = json.loads((HERE / 'SOURCES.json').read_text())
+    for row in manifest['external_inputs']:
+        need(sha256((HERE / row['local_path']).read_bytes()).hexdigest()
+             == row['sha256'], 'retained source changed')
+    return run_path(str(HERE / 'vendor/PR5238.py'), run_name='retained_geometry')
+
+
+def rank(rows):
+    basis = {}
+    for row in rows:
+        row = list(map(F, row))
+        for p, b in basis.items():
+            c = row[p]
+            if c:
+                row = [x-c*y for x, y in zip(row, b)]
+        p = next((i for i, x in enumerate(row) if x), None)
+        if p is not None:
+            c = row[p]
+            basis[p] = [x/c for x in row]
+    return len(basis)
+
+
+def minimum_supports(basis):
+    word, minimum, supports = 0, 63, set()
+    for index in range(1, 1 << 27):
+        word ^= basis[(index & -index).bit_length()-1]
+        weight = word.bit_count()
+        if weight < minimum:
+            minimum, supports = weight, {word}
+        elif weight == minimum:
+            supports.add(word)
+    need(minimum == 12 and len(supports) == 1638, 'complete minimum census')
+    return supports
+
+
+def reflections(roots, frames, dot):
+    lookup = {r: i for i, r in enumerate(roots)}
+    frame_set = set(frames)
+    out = []
+    for normal in roots:
+        p = []
+        for r in roots:
+            inner = dot(r, normal)
+            need(inner % 4 == 0, 'integral reflection')
+            image = tuple(r[i]-inner//4*normal[i] for i in range(8))
+            if next(x for x in image if x) < 0:
+                image = tuple(-x for x in image)
+            need(image in lookup, 'root reflection closure')
+            p.append(lookup[image])
+        need(sorted(p) == list(range(63)), 'root permutation')
+        need(all(tuple(sorted(p[j] for j in frame)) in frame_set
+                 for frame in frames), 'frame reflection closure')
+        out.append(tuple(p))
+    return out
+
+
+def transport(mask, permutation):
+    image = 0
+    while mask:
+        bit = mask & -mask
+        image |= 1 << permutation[bit.bit_length()-1]
+        mask ^= bit
+    return image
+
+
+def orbit(mask, permutations):
+    seen, queue = {mask}, [mask]
+    for current in queue:
+        for p in permutations:
+            image = transport(current, p)
+            if image not in seen:
+                seen.add(image)
+                queue.append(image)
+    return seen
+
+
+def form_a(x):
+    return sum(x[i]*x[i] for i in range(4))-sum(x[i]*x[i] for i in range(4, 8))
+
+
+def form_b(x):
+    return (x[0]-x[1])*(x[2]-x[3])
+
+
+def quadratic_matrix(form):
+    vectors = []
+    for i in (1, 2, 3, 5, 6, 7):
+        x = [0]*8
+        x[i] = 1
+        vectors.append(x)
+    vectors.append([1, 0, 0, 0, -1, 0, 0, 0])
+    matrix = [[F(form([x+y for x, y in zip(a, b)])-form(a)-form(b), 2)
+               for b in vectors] for a in vectors]
+    need(sum(matrix[i][i] for i in range(6))+matrix[6][6]/2 == 0,
+         'restricted trace zero')
+    return matrix
+
+
+def supported_rank(frames, support):
+    return rank([[int(j in frame) for j in support] for frame in frames])
+
+
+def check_relation(frames, values):
+    need(sum(x != 0 for x in values) == 12, 'twelve nonzero values')
+    need(all(sum(values[j] for j in frame) == 0 for frame in frames),
+         'literal rational frame sums')
+
+
+def partition(supports, orbits):
+    need(not orbits[0] & orbits[1], 'disjoint equality orbits')
+    need(orbits[0] | orbits[1] == supports, 'every minimum support classified')
+
+
+def reject(fn):
+    try:
+        fn()
+    except ValueError:
+        return
+    raise ValueError('invalid control accepted')
+
+
+def check():
+    g = geometry()
+    roots = g['intrinsic_e7']()
+    g['validate_domain'](roots)
+    need(roots == tuple(r for r in g['e8_lines']() if g['dot'](r, g['PIVOT']) == 0),
+         'ambient and intrinsic domains agree')
+    need(g['check_root_transitivity']() == 120, 'every ambient root slice')
+    frames = g['orthogonal_frames'](roots)
+    rows = tuple(sum(1 << j for j in frame) for frame in frames)
+    basis, free = g['binary_kernel'](rows)
+    supports = minimum_supports(basis)
+    permutations = reflections(roots, frames, g['dot'])
+    orbits, records, controls = [], [], 0
+    for name, form, size, qrank, scale in (
+            ('diagonal', form_a, 630, 6, 8), ('product', form_b, 1008, 2, 4)):
+        values = tuple(form(r) for r in roots)
+        check_relation(frames, values)
+        need(set(values) == {-scale, 0, scale}, 'constant nonzero magnitudes')
+        need(values.count(scale) == values.count(-scale) == 6, 'six values of each sign')
+        support = [j for j, x in enumerate(values) if x]
+        mask = sum(1 << j for j in support)
+        current = orbit(mask, permutations)
+        need(len(current) == size and current <= supports, 'complete attained orbit')
+        need(supported_rank(frames, support) == 11, 'one-dimensional rational lift')
+        need(rank(quadratic_matrix(form)) == qrank, 'quadratic rank')
+        for omitted in support:
+            need(supported_rank(frames, [j for j in support if j != omitted]) == 11,
+                 'every single omission has zero kernel')
+            controls += 1
+        changed = list(values)
+        changed[support[0]] += 1
+        reject(lambda: check_relation(frames, changed))
+        controls += 1
+        orbits.append(current)
+        records.append(dict(type=name, supports=size, representative_support=support,
+                            representative_values=list(values), quadratic_rank=qrank,
+                            restricted_frame_rank=11, rational_lift_dimension=1,
+                            orbit_sha256=sha256(json.dumps(sorted(current)).encode()).hexdigest()))
+    partition(supports, orbits)
+    reject(lambda: partition(supports-{next(iter(supports))}, orbits))
+    reject(lambda: partition(supports, [orbits[0], orbits[1] | orbits[0]]))
+    controls += 2
+    return dict(status='PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION', root_lines=63,
+                frames=135, binary_rank=36, binary_dimension=27,
+                nonzero_codewords=(1 << 27)-1, minimum_support=12,
+                minimum_supports=len(supports), reflection_generators=len(permutations),
+                ambient_root_slices=120, characteristic='zero', orbits=records,
+                rejecting_or_omission_controls=controls)
+
+
+def main():
+    result = check()
+    need(result == json.loads((HERE / 'RESULT.json').read_text()), 'fixed result receipt')
+    print(result['status'])
+    print('1638 minimum supports = 630 rank-six + 1008 rank-two; one scalar family per support')
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/e7-bitsliced-exhaustion/verify.py b/research/e7-bitsliced-exhaustion/verify.py
new file mode 100644
index 0000000000..3977128dc7
--- /dev/null
+++ b/research/e7-bitsliced-exhaustion/verify.py
@@ -0,0 +1,147 @@
+"""Check exact bit-lane exhaustion. Ali Romman with OpenAI Codex. Apache-2.0."""
+import ast
+from hashlib import sha256
+from itertools import combinations
+import json
+from pathlib import Path
+from random import Random
+from runpy import run_path
+
+HERE = Path(__file__).resolve().parent
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def authenticate():
+    sources = json.loads((HERE / 'SOURCES.json').read_text())
+    prefix = 'research/e7-bitsliced-exhaustion/'
+    for row in sources['files']:
+        if row['usage'] == 'input':
+            need(row['path'].startswith(prefix), 'source path outside package')
+            file = HERE / row['path'][len(prefix):]
+            need(sha256(file.read_bytes()).hexdigest() == row['sha256'],
+                 'source hash mismatch: ' + row['path'])
+
+
+def unchanged_consumer():
+    old = ast.parse((HERE / 'source/verify.py').read_text())
+    new = ast.parse((HERE / 'classify.py').read_text())
+    need(len(old.body) == len(new.body), 'consumer statement inventory')
+    changed = []
+    for left, right in zip(old.body, new.body):
+        if ast.dump(left) == ast.dump(right):
+            continue
+        if isinstance(left, ast.Assign):
+            need(isinstance(right, ast.Assign)
+                 and [ast.dump(x) for x in left.targets] == [ast.dump(x) for x in right.targets]
+                 == [ast.dump(ast.Name(id='HERE', ctx=ast.Store()))], 'only source root may change')
+            changed.append('HERE')
+        else:
+            need(isinstance(left, ast.FunctionDef) and isinstance(right, ast.FunctionDef)
+                 and left.name == right.name == 'minimum_supports', 'downstream check changed')
+            changed.append(left.name)
+    need(changed == ['HERE', 'minimum_supports'], 'exact derivative boundary')
+
+
+def literal_words(rows):
+    words = [0]
+    for row in rows:
+        words += [word ^ row for word in words]
+    return words
+
+
+def small_codes(engine):
+    digest = sha256()
+    codes = comparisons = 0
+    for dimension in range(5):
+        for rows in combinations(range(1, 16), dimension):
+            full = literal_words(rows)
+            if len(set(full)) != len(full):
+                continue
+            codes += 1
+            for maximum in range(5):
+                expected = sorted(word for word in full if word.bit_count() <= maximum)
+                for batch in range(1, 6):
+                    actual = sorted(engine(rows, 4, maximum, batch))
+                    need(actual == expected, 'complete four-coordinate code domain')
+                    digest.update(json.dumps([rows, maximum, batch, actual]).encode())
+                    comparisons += 1
+    need(codes == 1381 and comparisons == 34525, 'small-code coverage')
+    return dict(independent_generator_sets=codes, comparisons=comparisons,
+                sha256=digest.hexdigest())
+
+
+def wide_codes(engine):
+    rng = Random(20261026)
+    comparisons = 0
+    for width in (0, 1, 7, 31, 63, 64, 65, 127):
+        dimension = min(10, width)
+        rows = tuple((rng.getrandbits(width - dimension) << dimension) | (1 << i)
+                     for i in range(dimension))
+        full = literal_words(rows)
+        for maximum in sorted({0, width // 3, width // 2, width}):
+            expected = sorted(word for word in full if word.bit_count() <= maximum)
+            for batch in (1, 3, 7, 16):
+                need(sorted(engine(rows, width, maximum, batch)) == expected,
+                     'word-width or batch boundary')
+                comparisons += 1
+    return comparisons
+
+
+def reject(function):
+    try:
+        function()
+    except ValueError:
+        return
+    raise ValueError('invalid input accepted')
+
+
+def controls(engine):
+    cases = [([1], -1, 0, 1), ([1], True, 0, 1), ([1], 1, -1, 1),
+             ([1], 1, True, 1), ([1], 1, 2, 1), ([True], 1, 1, 1),
+             ([-1], 1, 1, 1), ([2], 1, 1, 1), ([0], 1, 1, 1),
+             ([1, 2, 3], 2, 1, 1), ([1], 1, 1, 0),
+             ([1], 1, 1, 21), ([1], 1, 1, True)]
+    for args in cases:
+        reject(lambda args=args: list(engine(*args)))
+    need(set(engine([1, 2], 3, 1)) == {0, 1, 2}, 'known initial code')
+    need(set(engine([1, 4], 3, 1)) == {0, 1, 4}, 'changed generator is not cached')
+    need(set(engine([1, 2], 3, 0)) == {0}, 'changed bound is not cached')
+    need(set(engine([1, 2], 3, 2)) == {0, 1, 2, 3}, 'full weight bound')
+    return len(cases) + 3
+
+
+def check():
+    authenticate()
+    unchanged_consumer()
+    functions = run_path(str(HERE / 'binary.py'))
+    engine = functions['low_weight_words']
+    small = small_codes(engine)
+    wide = wide_codes(engine)
+    rejected = controls(engine)
+    current = run_path(str(HERE / 'classify.py'))
+    result = current['check']()
+    need(result == json.loads((HERE / 'source/RESULT.json').read_text()),
+         'complete predecessor scientific result')
+    geometry = current['geometry']()
+    roots = geometry['intrinsic_e7']()
+    frames = geometry['orthogonal_frames'](roots)
+    basis, _ = geometry['binary_kernel'](tuple(sum(1 << j for j in row) for row in frames))
+    reference = current['minimum_supports'](basis)
+    changed = list(reversed(basis))
+    changed[0] ^= changed[1]
+    need(current['minimum_supports'](changed) == reference, 'full E7 basis change')
+    return dict(status='PASS_E7_BITSLICED_EXHAUSTION', small_codes=small,
+                wide_comparisons=wide, malformed_and_invalidation_controls=rejected,
+                all_nonzero_E7_words=(1 << 27) - 1, minimum_supports=len(reference),
+                supports_sha256=sha256(json.dumps(sorted(reference)).encode()).hexdigest(),
+                source_result=result, derivative_changes=['HERE', 'minimum_supports'])
+
+
+if __name__ == '__main__':
+    result = check()
+    need(result == json.loads((HERE / 'RESULT.json').read_text()), 'fixed result receipt')
+    print(json.dumps(result, indent=2, sort_keys=True))