diff --git a/research/e6-e7-shadow-minrank-upper/README.md b/research/e6-e7-shadow-minrank-upper/README.md
new file mode 100644
index 0000000000..b427e19164
--- /dev/null
+++ b/research/e6-e7-shadow-minrank-upper/README.md
@@ -0,0 +1,131 @@
+# F2 shadow minranks of the E6 and E7 root lines: upper bounds 8 and 11
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: finite exact certificate. No new κ.** On the root lines of E6
+and E7, explicit F2 matrices with unit diagonal and zeros on every orthogonal
+pair have exact F2 rank 8 and 11. Combined with the lower bounds cited from
+DreamingOfClouds's [PR #2277](https://github.com/CrocSwap/integer-mult-bounds/pull/2277):
+
+```text
+mr₂(Γ_E6) ∈ {7, 8},        8 ≤ mr₂(Γ_E7) ≤ 11.
+```
+
+Before this package, no upper bound was recorded for either value. PR #2277
+(`research/overcomplete-and-realisation-floors`, §8 Open next question 5)
+asks for both exact values. This package answers the upper side and leaves
+both exact values open.
+
+## Object
+
+Let `L` be the 36 E6 or 63 E7 root lines, one representative per `±` pair.
+A **shadow** is an F2 matrix `N` indexed by `L` with
+
+- `N_tt = 1` for every line `t`;
+- `N_ts = 0` whenever `t ≠ s` are orthogonal;
+- entries on non-orthogonal pairs free.
+
+`mr₂(Γ)` is the minimum F2 rank of a shadow. This is the definition used in
+PR #2277 §9.2 (SAT-2). In graph terms it is Haemers's F2 minrank of the
+non-orthogonality graph. By PR #2277's shadow lemma, a shadow of rank at most
+`m` is what a B-independent F2 certificate needs to certify all lines of a
+decoder with `m` terms.
+
+## Evidence
+
+[WITNESSES.json](WITNESSES.json) stores `N = U Vᵀ` with F2 factors `U`, `V` of
+widths 8 (E6) and 11 (E7). The lines are stored explicitly as E8 roots in
+doubled coordinates. The anchors are one root (E7, the orthogonal complement
+of an A1) or two roots with inner product ±4 (E6, the complement of an A2).
+
+[verify.py](verify.py) uses the standard library only. It:
+
+1. rebuilds all 240 E8 roots and checks that the stored lines are exactly the
+   lines orthogonal to the stored anchors (36 and 63 lines);
+2. checks every one of the 36² and 63² entries against the pattern: 36 and 63
+   unit diagonal entries, 270 and 945 orthogonal pairs (each in both orders)
+   forced to zero;
+3. computes the exact F2 rank of `N` by elimination: 8 and 11;
+4. rejects two mutations per unit, a cleared diagonal entry and a set
+   orthogonal entry, and calibrates the rank routine;
+5. enumerates every pairwise non-orthogonal 7-set and 8-set of E7 lines and
+   counts exact covers of the 63 lines by nine 7-sets (see Limitations).
+
+Output:
+
+```text
+PASS E6: 36 lines, 270 orthogonal pairs forced zero, 36 unit diagonal entries, 142/720 free entries set; exact F2 rank 8 <= 8
+PASS E6 controls: diagonal and orthogonal-entry mutations rejected; rank helper calibrated
+PASS E7: 63 lines, 945 orthogonal pairs forced zero, 63 unit diagonal entries, 321/2016 free entries set; exact F2 rank 11 <= 11
+PASS E7 controls: diagonal and orthogonal-entry mutations rejected; rank helper calibrated
+PASS E7 clique cover: no 8-set of pairwise non-orthogonal lines; 288 7-sets; 0 partitions of the 63 lines into nine 7-sets
+PASS e6-e7-shadow-minrank-upper: mr2(Gamma_E6) <= 8 and mr2(Gamma_E7) <= 11
+```
+
+The witnesses were found with a CaDiCaL search of the `U Vᵀ` encoding.
+[search_witness.py](search_witness.py) reproduces that search. It is optional,
+needs `python-sat`, and is not part of the registered replay. Fresh runs may
+return different witnesses; two such regenerated witnesses also passed
+`verify.py` before submission.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/e6-e7-shadow-minrank-upper/verify.py
+python3.12 -B scripts/research_package.py --package research/e6-e7-shadow-minrank-upper
+```
+
+Optional witness search (needs `python-sat`):
+
+```sh
+cd research/e6-e7-shadow-minrank-upper
+python3.12 -B search_witness.py E6 8 /tmp/e6.json 60
+python3.12 -B search_witness.py E7 11 /tmp/e7.json 60
+```
+
+## Limitations
+
+- The lower bounds 7 (E6) and 8 (E7) are PR #2277's DRAT-verified SAT-2
+  results. They are cited, not re-run.
+- Search failures are not proofs. Plain CaDiCaL runs, each fixing `U` on
+  one maximum set of pairwise orthogonal lines (4 for E6, 7 for E7), did not
+  finish: E6 rank 7 (stopped after 12 minutes), E7 rank 8
+  (stopped after 12 minutes), E7 rank 9 (600 s limit) and E7 rank 10 (150 s
+  limit). No UNSAT claim is made for any of them.
+- Only F2 is covered. Larger fields of characteristic 2 remain open, as in
+  PR #2277 §8.5; an F2 witness also works over every extension field, so the
+  upper bounds hold there.
+- No decoder, decoder floor, supplier, invoice or κ consequence is claimed.
+  The global fitting minrank of PR #2277 SAT-1 is a different problem (zeros
+  on non-orthogonal pairs) and is not touched.
+
+One structural finding narrows the E7 search. The largest pairwise
+non-orthogonal sets of E7 lines have size 7 (288 of them). An exhaustive
+exact-cover count in `verify.py` finds no partition of the 63 lines into nine such sets.
+So rank 9 cannot come from an all-ones block-diagonal clique cover. This is a
+statement about that one construction, not about rank 9.
+
+## Open next questions
+
+The structured versions are in [TASK.json](TASK.json).
+
+1. **Is `mr₂(Γ_E6)` 7 or 8?** Rank 7 would equal the global fitting minrank
+   of SAT-1. First step: rerun rank 7 with symmetry breaking under W(E6). A
+   possible model, not checked here, is the 36 non-singular points of an
+   elliptic quadric in F2⁶. Keep a DRAT proof if the result is UNSAT.
+2. **Which of 8, 9, 10, 11 is `mr₂(Γ_E7)`?** Decide rank 10 first. The 63
+   lines carry an Sp(6,2) structure that gives strong symmetry breaking.
+3. **Do extension fields of characteristic 2 lower either value?** Encode
+   GF(4) entries and repeat the E6 rank-7 test.
+
+## Credit
+
+DreamingOfClouds's PR #2277 supplies the shadow lemma, the definition of
+`mr₂(Γ)`, the lower bounds `mr₂(Γ_E6) ≥ 7` and `mr₂(Γ_E7) ≥ 8`, the E8/E7/E6
+line construction this package follows, and the open question. Those results
+are used as cited premises, not re-verified here. The `U Vᵀ` Tseitin encoding
+follows that package's `lib/satgen.py`. New here: the two explicit witnesses,
+their standalone checker and the exact-cover negative for E7. Independent
+human and formal proof-kernel review are unclaimed.
diff --git a/research/e6-e7-shadow-minrank-upper/SOURCES.json b/research/e6-e7-shadow-minrank-upper/SOURCES.json
new file mode 100644
index 0000000000..7a62f8c639
--- /dev/null
+++ b/research/e6-e7-shadow-minrank-upper/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/overcomplete-and-realisation-floors/README.md",
+      "usage": "input",
+      "git_blob": "04894070db67d13a67f8587760b227e44d182671",
+      "sha256": "4128824937445ed3de10307da5cf1347a499da33f7ca8cdcf5297426a22b191a"
+    }
+  ]
+}
diff --git a/research/e6-e7-shadow-minrank-upper/TASK.json b/research/e6-e7-shadow-minrank-upper/TASK.json
new file mode 100644
index 0000000000..b7e71b7b11
--- /dev/null
+++ b/research/e6-e7-shadow-minrank-upper/TASK.json
@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Upper bounds for the F2 shadow minranks mr2(Gamma_E6) and mr2(Gamma_E7) left open in PR #2277 (research/overcomplete-and-realisation-floors, Open next question 5): minimum F2 rank of a matrix on the 36 E6 or 63 E7 root lines with unit diagonal and zeros on every orthogonal pair.",
+  "scope_change_reason": "Side result on the decoder-cost shadow lemma, not a decoder or coframe change. It answers part of a precisely stated open question in the decoder-floor lineage and needs no supplier or invoice.",
+  "bottleneck_link": "Side result. PR #2277's shadow lemma bounds the cost of any exact root-code decoder by rank_L(B o N). A rank bound on N limits how far F2-valued B-independent shadows can certify decoder floors; no kappa, decoder or supplier consequence is claimed.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified improvement: explicit witnesses giving new upper bounds. Do not continue into the E6 rank-7 or E7 rank-8..10 decision within the 60-minute budget.",
+  "outcome": "partial",
+  "evidence": "WITNESSES.json gives N = U V^T over F2 with U, V of widths 8 (E6) and 11 (E7). verify.py rebuilds both line sets from E8, checks all 1296 and 3969 pattern entries, computes exact F2 ranks 8 and 11, and rejects a diagonal and an orthogonal-entry mutation. With the cited PR #2277 lower bounds: mr2(Gamma_E6) in {7,8}, 8 <= mr2(Gamma_E7) <= 11.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is mr2(Gamma_E6) equal to 7 or 8?",
+      "why_it_matters": "It is the last undecided value for E6; rank 7 would match the global fitting minrank of SAT-1.",
+      "first_step": "Run the rank-7 instance with symmetry breaking under W(E6), possibly via an elliptic-quadric model of the 36 lines (not checked here), and keep a DRAT proof if UNSAT.",
+      "blocked_by": "A plain CaDiCaL run fixing U on one maximum orthogonal 4-set was stopped unfinished after 12 minutes."
+    },
+    {
+      "question": "What is mr2(Gamma_E7) in {8,9,10,11}?",
+      "why_it_matters": "It fixes the exact F2 shadow capacity on E7; the lower bound is one above T = 7.",
+      "first_step": "Decide rank 10 first. The 63 lines carry the Sp(6,2) structure, which gives strong symmetry breaking.",
+      "blocked_by": "Plain CaDiCaL runs did not finish: rank 8 stopped after 12 minutes, rank 9 at a 600 s limit, rank 10 at a 150 s limit. No partition of the 63 lines into nine pairwise non-orthogonal 7-sets exists (verify.py), so the clique-cover route to rank 9 is closed."
+    },
+    {
+      "question": "Do larger fields of characteristic 2 lower either value?",
+      "why_it_matters": "PR #2277 section 8.5 leaves characteristic-2 extension fields open; the witnesses here are F2 matrices and transfer upward unchanged.",
+      "first_step": "Encode GF(4) entries and repeat the rank-7 E6 test.",
+      "blocked_by": "Not attempted."
+    }
+  ]
+}
diff --git a/research/e6-e7-shadow-minrank-upper/VERIFY.json b/research/e6-e7-shadow-minrank-upper/VERIFY.json
new file mode 100644
index 0000000000..540e938131
--- /dev/null
+++ b/research/e6-e7-shadow-minrank-upper/VERIFY.json
@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/e6-e7-shadow-minrank-upper/WITNESSES.json",
+    "research/overcomplete-and-realisation-floors/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Rebuild the E6/E7 line sets from E8; check unit diagonal and every orthogonal-pair zero of N = U V^T; exact F2 ranks 8 and 11; diagonal and orthogonal-entry mutation controls rejected."
+    }
+  ]
+}
diff --git a/research/e6-e7-shadow-minrank-upper/WITNESSES.json b/research/e6-e7-shadow-minrank-upper/WITNESSES.json
new file mode 100644
index 0000000000..79c05b6950
--- /dev/null
+++ b/research/e6-e7-shadow-minrank-upper/WITNESSES.json
@@ -0,0 +1 @@
+{"description":"N = U V^T over F2; rows indexed like `lines` (E8 roots, doubled coordinates, one per +-pair).","units":{"E6":{"anchors":[[2,2,0,0,0,0,0,0],[2,0,2,0,0,0,0,0]],"rank_cap":8,"lines":[[0,0,0,2,2,0,0,0],[0,0,0,2,-2,0,0,0],[0,0,0,2,0,2,0,0],[0,0,0,2,0,-2,0,0],[0,0,0,2,0,0,2,0],[0,0,0,2,0,0,-2,0],[0,0,0,2,0,0,0,2],[0,0,0,2,0,0,0,-2],[0,0,0,0,2,2,0,0],[0,0,0,0,2,-2,0,0],[0,0,0,0,2,0,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,0,-2],[0,0,0,0,0,2,2,0],[0,0,0,0,0,2,-2,0],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,0,2,-2],[1,-1,-1,1,1,1,1,1],[1,-1,-1,1,1,1,-1,-1],[1,-1,-1,1,1,-1,1,-1],[1,-1,-1,1,1,-1,-1,1],[1,-1,-1,1,-1,1,1,-1],[1,-1,-1,1,-1,1,-1,1],[1,-1,-1,1,-1,-1,1,1],[1,-1,-1,1,-1,-1,-1,-1],[1,-1,-1,-1,1,1,1,-1],[1,-1,-1,-1,1,1,-1,1],[1,-1,-1,-1,1,-1,1,1],[1,-1,-1,-1,1,-1,-1,-1],[1,-1,-1,-1,-1,1,1,1],[1,-1,-1,-1,-1,1,-1,-1],[1,-1,-1,-1,-1,-1,1,-1],[1,-1,-1,-1,-1,-1,-1,1]],"U":[[0,0,0,1,0,1,0,1],[0,0,0,1,0,0,0,0],[0,0,0,1,0,1,0,1],[0,0,1,0,0,0,0,0],[1,0,0,0,0,0,0,0],[0,1,0,0,0,0,0,0],[0,0,0,0,1,0,0,0],[0,0,0,1,0,1,0,1],[0,0,1,0,0,0,0,0],[0,0,0,1,0,0,0,0],[1,0,0,0,0,0,0,0],[0,0,0,1,0,0,0,0],[0,0,0,0,1,0,0,0],[0,0,0,1,0,0,0,0],[1,0,0,0,0,0,0,0],[0,0,1,0,0,0,0,0],[0,0,1,0,0,0,0,0],[0,0,0,0,1,0,0,0],[0,0,0,0,1,0,0,0],[1,0,0,0,0,0,0,0],[0,0,1,0,0,0,1,1],[0,0,1,0,0,0,1,1],[0,0,0,0,0,1,0,0],[0,0,1,0,0,0,1,1],[0,0,0,0,0,1,0,0],[0,0,1,0,0,0,1,1],[0,0,0,0,0,1,0,0],[0,0,1,0,0,1,1,1],[0,1,0,0,0,0,0,0],[0,0,0,0,0,0,1,1],[0,1,0,0,0,0,0,0],[0,0,0,1,0,0,0,0],[0,1,0,0,0,0,0,0],[0,0,0,0,1,0,0,0],[0,1,0,0,0,0,0,0],[0,0,0,1,0,1,0,1]],"V":[[0,0,0,0,0,0,1,1],[0,0,0,1,0,0,1,1],[0,0,0,0,0,0,1,1],[0,0,1,0,0,0,1,0],[1,0,0,0,0,0,1,1],[0,1,0,0,0,0,0,0],[0,0,0,0,1,0,0,0],[0,0,0,0,0,0,1,1],[0,0,1,0,0,0,1,0],[0,0,0,1,0,0,1,1],[1,0,0,0,0,0,0,0],[0,0,0,1,0,0,1,1],[0,0,0,0,1,0,0,0],[0,0,0,1,0,0,1,1],[1,0,0,0,0,0,0,0],[0,0,1,0,0,0,1,0],[0,0,1,0,0,0,1,0],[0,0,0,0,1,0,0,0],[0,0,0,0,1,0,0,0],[1,0,0,0,0,0,0,0],[0,0,0,0,0,1,0,1],[0,0,0,0,0,0,1,0],[0,0,0,0,0,1,1,1],[0,0,0,0,0,0,1,0],[0,0,0,0,0,1,1,1],[0,0,0,0,0,0,1,0],[0,0,0,0,0,1,1,1],[0,0,0,0,0,1,1,1],[0,1,0,0,0,0,0,0],[0,0,1,0,0,0,1,0],[0,1,0,0,0,0,0,0],[0,0,0,1,0,0,1,1],[0,1,0,0,0,0,0,0],[0,0,0,0,1,0,0,0],[0,1,0,0,0,0,0,0],[0,0,0,0,0,0,1,1]]},"E7":{"anchors":[[2,2,0,0,0,0,0,0]],"rank_cap":11,"lines":[[2,-2,0,0,0,0,0,0],[0,0,2,2,0,0,0,0],[0,0,2,-2,0,0,0,0],[0,0,2,0,2,0,0,0],[0,0,2,0,-2,0,0,0],[0,0,2,0,0,2,0,0],[0,0,2,0,0,-2,0,0],[0,0,2,0,0,0,2,0],[0,0,2,0,0,0,-2,0],[0,0,2,0,0,0,0,2],[0,0,2,0,0,0,0,-2],[0,0,0,2,2,0,0,0],[0,0,0,2,-2,0,0,0],[0,0,0,2,0,2,0,0],[0,0,0,2,0,-2,0,0],[0,0,0,2,0,0,2,0],[0,0,0,2,0,0,-2,0],[0,0,0,2,0,0,0,2],[0,0,0,2,0,0,0,-2],[0,0,0,0,2,2,0,0],[0,0,0,0,2,-2,0,0],[0,0,0,0,2,0,2,0],[0,0,0,0,2,0,-2,0],[0,0,0,0,2,0,0,2],[0,0,0,0,2,0,0,-2],[0,0,0,0,0,2,2,0],[0,0,0,0,0,2,-2,0],[0,0,0,0,0,2,0,2],[0,0,0,0,0,2,0,-2],[0,0,0,0,0,0,2,2],[0,0,0,0,0,0,2,-2],[1,-1,1,1,1,1,1,-1],[1,-1,1,1,1,1,-1,1],[1,-1,1,1,1,-1,1,1],[1,-1,1,1,1,-1,-1,-1],[1,-1,1,1,-1,1,1,1],[1,-1,1,1,-1,1,-1,-1],[1,-1,1,1,-1,-1,1,-1],[1,-1,1,1,-1,-1,-1,1],[1,-1,1,-1,1,1,1,1],[1,-1,1,-1,1,1,-1,-1],[1,-1,1,-1,1,-1,1,-1],[1,-1,1,-1,1,-1,-1,1],[1,-1,1,-1,-1,1,1,-1],[1,-1,1,-1,-1,1,-1,1],[1,-1,1,-1,-1,-1,1,1],[1,-1,1,-1,-1,-1,-1,-1],[1,-1,-1,1,1,1,1,1],[1,-1,-1,1,1,1,-1,-1],[1,-1,-1,1,1,-1,1,-1],[1,-1,-1,1,1,-1,-1,1],[1,-1,-1,1,-1,1,1,-1],[1,-1,-1,1,-1,1,-1,1],[1,-1,-1,1,-1,-1,1,1],[1,-1,-1,1,-1,-1,-1,-1],[1,-1,-1,-1,1,1,1,-1],[1,-1,-1,-1,1,1,-1,1],[1,-1,-1,-1,1,-1,1,1],[1,-1,-1,-1,1,-1,-1,-1],[1,-1,-1,-1,-1,1,1,1],[1,-1,-1,-1,-1,1,-1,-1],[1,-1,-1,-1,-1,-1,1,-1],[1,-1,-1,-1,-1,-1,-1,1]],"U":[[1,0,0,0,0,0,0,0,0,0,0],[0,0,1,0,0,0,0,0,0,0,0],[0,0,0,0,1,0,0,0,0,1,0],[0,0,0,0,0,0,0,0,0,1,0],[0,1,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,1,0,0,0],[0,0,0,0,0,0,1,0,0,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,1,0,0,0],[0,1,0,0,0,0,0,0,0,0,0],[0,0,1,0,0,0,0,0,0,0,0],[0,0,0,0,1,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,1,0],[0,0,0,0,0,0,1,0,0,0,0],[0,0,0,0,1,0,0,0,0,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,0,0,1,0,0,0,0,0,0],[0,0,0,0,1,0,0,0,0,0,0],[0,0,1,0,0,0,0,0,0,0,0],[0,0,0,0,0,1,0,0,0,0,0],[0,0,0,0,0,0,1,0,0,0,0],[0,0,0,0,0,0,0,1,1,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,1,1,0,0],[0,0,0,0,0,1,0,0,0,0,0],[0,0,0,0,0,0,1,0,0,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,0,0,0,0,1,0,0,0,0],[0,0,0,0,0,1,0,0,0,0,0],[0,0,0,0,0,0,0,1,1,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,0,0,0,1,0,0,0,0,0],[1,0,0,0,0,0,0,0,0,0,0],[1,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,0,1],[0,1,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,1,1,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,1,0,0,0,0,0,0,0,0,0],[1,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,0,1],[0,0,0,0,0,0,0,0,0,0,1],[0,0,0,0,0,0,0,0,0,0,1],[0,0,0,0,1,0,0,0,0,0,0],[0,1,0,0,0,0,0,0,0,0,0],[0,1,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,1,1,0,0],[1,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,1,0,0,0,0,0],[0,0,0,0,0,0,0,1,0,0,0],[0,0,0,0,1,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,1,0],[0,0,0,0,0,0,0,0,0,1,0],[0,0,0,0,0,0,0,1,0,1,0],[0,0,0,0,0,0,0,1,1,0,0],[0,0,0,0,0,1,0,0,0,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,1,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,0,1],[0,0,1,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,1,1,0,0],[0,0,0,0,0,0,0,1,0,0,0],[0,0,1,0,0,0,0,0,0,0,0]],"V":[[1,0,0,0,0,0,0,0,0,0,0],[0,0,1,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,1,0],[0,0,0,0,0,0,0,0,0,1,0],[0,1,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,1,1,0,0],[0,0,0,0,0,0,1,0,0,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,1,1,0,0],[0,1,0,0,0,0,0,0,0,0,0],[0,0,1,0,0,0,0,0,0,0,0],[0,0,0,0,1,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,1,0],[0,0,0,0,0,0,1,0,0,0,0],[0,0,0,0,1,0,0,0,0,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,0,0,1,0,0,0,0,0,0],[0,0,0,0,1,0,0,0,0,0,0],[0,0,1,0,0,0,0,0,0,0,0],[0,0,0,0,0,1,0,0,0,0,0],[0,0,0,0,0,0,1,0,0,0,0],[0,0,0,0,0,0,0,0,1,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,1,0,0],[0,0,0,0,0,1,0,0,0,0,0],[0,0,0,0,0,0,1,0,0,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,0,0,0,0,1,0,0,0,0],[0,0,0,0,0,1,0,0,0,0,0],[0,0,0,0,0,0,0,0,1,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,0,0,0,0,1,0,0,0,0,0],[1,0,0,0,0,0,0,0,0,0,0],[1,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,0,1],[0,1,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,1,0,0],[0,0,0,1,0,0,0,0,0,0,0],[0,1,0,0,0,0,0,0,0,0,0],[1,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,0,1],[0,0,0,0,0,0,0,0,0,0,1],[0,0,0,0,0,0,0,0,0,0,1],[0,0,0,0,1,0,0,0,0,0,0],[0,1,0,0,0,0,0,0,0,0,0],[0,1,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,1,0,0],[1,0,0,0,0,0,0,0,0,0,0],[0,0,0,0,0,1,0,0,0,0,0],[0,0,0,0,0,0,0,1,1,0,0],[0,0,0,0,1,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,1,0],[0,0,0,0,0,0,0,0,0,1,0],[0,0,0,0,0,0,0,1,1,0,0],[0,0,0,0,0,0,0,0,1,0,0],[0,0,0,0,0,1,0,0,0,0,0],[0,0,1,1,0,0,0,0,0,0,0],[0,0,1,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,0,0,1],[0,0,1,0,0,0,0,0,0,0,0],[0,0,0,0,0,0,0,0,1,0,0],[0,0,0,0,0,0,0,1,1,0,0],[0,0,1,0,0,0,0,0,0,0,0]]}}}
\ No newline at end of file
diff --git a/research/e6-e7-shadow-minrank-upper/search_witness.py b/research/e6-e7-shadow-minrank-upper/search_witness.py
new file mode 100644
index 0000000000..2dea8ed42e
--- /dev/null
+++ b/research/e6-e7-shadow-minrank-upper/search_witness.py
@@ -0,0 +1,81 @@
+"""Optional: search for a rank-r F2 shadow N = U V^T on the E6 or E7 lines.
+
+Not part of the registered replay; needs python-sat (CaDiCaL 1.5.3).  The
+registered check is verify.py on the committed WITNESSES.json.  A fresh run
+may return a different witness; verify.py accepts any valid one.
+
+usage: search_witness.py {E6|E7} RANK OUT.json [SECONDS]
+Prepared by Nick Petalas.  Apache-2.0.
+"""
+import json
+import sys
+import threading
+
+from pysat.solvers import Cadical153
+
+from verify import dot, e8_roots_doubled, line_set
+
+ANCHORS = {"E6": [(2, 2, 0, 0, 0, 0, 0, 0), (0, -2, -2, 0, 0, 0, 0, 0)],
+           "E7": [(2, 2, 0, 0, 0, 0, 0, 0)]}
+
+
+def orthogonal_clique(lines):
+    """A greedy set of pairwise orthogonal lines (fixes U on it: valid symmetry breaking)."""
+    clique = []
+    for i, v in enumerate(lines):
+        if all(dot(v, lines[j]) == 0 for j in clique):
+            clique.append(i)
+    return clique
+
+
+def main():
+    unit, r, out = sys.argv[1], int(sys.argv[2]), sys.argv[3]
+    seconds = float(sys.argv[4]) if len(sys.argv) > 4 else 600.0
+    anchors = ANCHORS[unit]
+    lines = sorted(line_set(anchors))
+    n = len(lines)
+    count = [0]
+    clauses = []
+
+    def new():
+        count[0] += 1
+        return count[0]
+
+    U = [[new() for _ in range(r)] for _ in range(n)]
+    V = [[new() for _ in range(r)] for _ in range(n)]
+
+    def entry(t, s, val):
+        ands = []
+        for i in range(r):
+            a = new()
+            clauses.extend([[-a, U[t][i]], [-a, V[s][i]], [a, -U[t][i], -V[s][i]]])
+            ands.append(a)
+        cur = ands[0]
+        for lit in ands[1:]:
+            y = new()
+            clauses.extend([[-y, cur, lit], [-y, -cur, -lit], [y, -cur, lit], [y, cur, -lit]])
+            cur = y
+        clauses.append([cur] if val else [-cur])
+
+    for t in range(n):
+        for s in range(n):
+            if t == s or dot(lines[t], lines[s]) == 0:
+                entry(t, s, int(t == s))
+    for k, t in enumerate(orthogonal_clique(lines)[:r]):
+        clauses.extend([[U[t][i]] if i == k else [-U[t][i]] for i in range(r)])
+    with Cadical153(bootstrap_with=clauses) as solver:
+        timer = threading.Timer(seconds, solver.interrupt)
+        timer.start()
+        status = solver.solve_limited(expect_interrupt=True)
+        timer.cancel()
+        print(unit, r, {True: "SAT", False: "UNSAT", None: "UNKNOWN (time limit)"}[status])
+        if status:
+            model = {x for x in solver.get_model() if x > 0}
+            item = {"anchors": [list(a) for a in anchors], "rank_cap": r, "lines": [list(v) for v in lines],
+                    "U": [[int(x in model) for x in row] for row in U],
+                    "V": [[int(x in model) for x in row] for row in V]}
+            json.dump({"units": {unit: item}}, open(out, "w"), separators=(",", ":"))
+
+
+if __name__ == "__main__":
+    main()
diff --git a/research/e6-e7-shadow-minrank-upper/verify.py b/research/e6-e7-shadow-minrank-upper/verify.py
new file mode 100644
index 0000000000..8a52e2deee
--- /dev/null
+++ b/research/e6-e7-shadow-minrank-upper/verify.py
@@ -0,0 +1,173 @@
+"""Check explicit F2 shadow matrices for the E6 and E7 root-line patterns.
+
+A shadow on a root-line set L is an F2 matrix N indexed by L with N_tt = 1 and
+N_ts = 0 whenever t != s are orthogonal; entries on non-orthogonal pairs are free
+(PR #2277, SAT-2).  WITNESSES.json stores N = U V^T for E6 (rank 8) and E7
+(rank 11).  This script rebuilds the line sets from E8, checks every pattern
+entry, computes the exact F2 rank of N and runs mutation controls.
+Standard library only.  Prepared by Nick Petalas.  Apache-2.0.
+"""
+import itertools
+import json
+import pathlib
+import sys
+
+HERE = pathlib.Path(__file__).resolve().parent
+EXPECTED = {"E6": (36, 8), "E7": (63, 11)}
+
+
+def dot(a, b):
+    return sum(x * y for x, y in zip(a, b))
+
+
+def e8_roots_doubled():
+    """All 240 E8 roots with doubled coordinates (norm 8)."""
+    roots = []
+    for i, j in itertools.combinations(range(8), 2):
+        for si in (2, -2):
+            for sj in (2, -2):
+                r = [0] * 8
+                r[i], r[j] = si, sj
+                roots.append(tuple(r))
+    for signs in itertools.product((1, -1), repeat=8):
+        if signs.count(-1) % 2 == 0:
+            roots.append(signs)
+    assert len(roots) == 240
+    return roots
+
+
+def canonical(v):
+    """Representative of the line {v, -v}: first nonzero coordinate positive."""
+    first = next(x for x in v if x != 0)
+    return tuple(v) if first > 0 else tuple(-x for x in v)
+
+
+def line_set(anchors):
+    """Lines of E8 roots orthogonal to every anchor root."""
+    return {canonical(r) for r in e8_roots_doubled() if all(dot(r, a) == 0 for a in anchors)}
+
+
+def rank_f2(rows):
+    """Exact rank over F2 of integer bitmask rows."""
+    pivots = {}
+    for row in rows:
+        while row:
+            top = row.bit_length() - 1
+            if top not in pivots:
+                pivots[top] = row
+                break
+            row ^= pivots[top]
+    return len(pivots)
+
+
+def shadow_rows(U, V):
+    """Rows of N = U V^T over F2 as bitmasks."""
+    n = len(U)
+    return [sum(1 << s for s in range(n) if sum(a & b for a, b in zip(U[t], V[s])) & 1) for t in range(n)]
+
+
+def pattern_violations(lines, rows):
+    """Entries breaking N_tt = 1 or N_ts = 0 on orthogonal pairs."""
+    bad = []
+    n = len(lines)
+    for t in range(n):
+        for s in range(n):
+            bit = rows[t] >> s & 1
+            if t == s and bit != 1:
+                bad.append((t, s))
+            elif t != s and dot(lines[t], lines[s]) == 0 and bit != 0:
+                bad.append((t, s))
+    return bad
+
+
+def check_unit(name, item):
+    size, rank_cap = EXPECTED[name]
+    anchors = [tuple(a) for a in item["anchors"]]
+    roots = set(e8_roots_doubled())
+    assert all(a in roots for a in anchors), f"{name}: anchor is not an E8 root"
+    if name == "E6":
+        assert abs(dot(anchors[0], anchors[1])) == 4, "E6 anchors must span an A2"
+    lines = [tuple(v) for v in item["lines"]]
+    assert len(set(lines)) == len(lines) == size, f"{name}: expected {size} distinct lines"
+    assert {canonical(v) for v in lines} == line_set(anchors), f"{name}: stored lines are not the {name} line set"
+    U, V = item["U"], item["V"]
+    assert item["rank_cap"] == rank_cap and len(U) == len(V) == size
+    assert all(len(row) == rank_cap and set(row) <= {0, 1} for row in U + V), f"{name}: factor shape"
+    rows = shadow_rows(U, V)
+    bad = pattern_violations(lines, rows)
+    assert not bad, f"{name}: {len(bad)} pattern violations, first {bad[0]}"
+    exact = rank_f2(rows)
+    assert exact <= rank_cap, f"{name}: rank {exact} > {rank_cap}"
+    orth_pairs = sum(1 for t in range(size) for s in range(t + 1, size) if dot(lines[t], lines[s]) == 0)
+    free = size * (size - 1) - 2 * orth_pairs
+    ones_free = sum(bin(r).count("1") for r in rows) - size
+    print(f"PASS {name}: {size} lines, {orth_pairs} orthogonal pairs forced zero, "
+          f"{size} unit diagonal entries, {ones_free}/{free} free entries set; exact F2 rank {exact} <= {rank_cap}")
+    return lines, rows
+
+
+def controls(lines, rows, name):
+    """The checker must reject a diagonal zero and a nonzero orthogonal entry."""
+    t = 0
+    s = next(s for s in range(len(lines)) if s != t and dot(lines[t], lines[s]) == 0)
+    flipped_diag = list(rows)
+    flipped_diag[t] ^= 1 << t
+    flipped_orth = list(rows)
+    flipped_orth[t] ^= 1 << s
+    assert pattern_violations(lines, flipped_diag) == [(t, t)]
+    assert pattern_violations(lines, flipped_orth) == [(t, s)]
+    assert rank_f2([1, 2, 3]) == 2 and rank_f2([1 << k for k in range(9)]) == 9
+    print(f"PASS {name} controls: diagonal and orthogonal-entry mutations rejected; rank helper calibrated")
+
+
+def nonorthogonal_cliques(lines, size):
+    """Every set of `size` pairwise non-orthogonal lines, as bitmasks."""
+    n = len(lines)
+    adj = [sum(1 << s for s in range(n) if s != t and dot(lines[t], lines[s]) != 0) for t in range(n)]
+    found = []
+
+    def grow(members, mask, cand):
+        if len(members) == size:
+            found.append(mask)
+            return
+        while cand:
+            t = cand.bit_length() - 1
+            cand &= ~(1 << t)
+            grow(members + [t], mask | 1 << t, cand & adj[t] & ((1 << t) - 1))
+
+    grow([], 0, (1 << n) - 1)
+    return adj, found
+
+
+def e7_seven_clique_partitions(lines):
+    """Exhaustive exact cover of the 63 E7 lines by pairwise non-orthogonal 7-sets."""
+    adj, sevens = nonorthogonal_cliques(lines, 7)
+    assert not nonorthogonal_cliques(lines, 8)[1], "an 8-set of pairwise non-orthogonal E7 lines exists"
+    by_low = {}
+    for c in sevens:
+        by_low.setdefault((c & -c).bit_length() - 1, []).append(c)
+
+    def cover(rem):
+        if rem == 0:
+            return 1
+        low = (rem & -rem).bit_length() - 1
+        return sum(cover(rem & ~c) for c in by_low.get(low, []) if c & rem == c)
+
+    return len(sevens), cover((1 << len(lines)) - 1)
+
+
+def main():
+    data = json.loads((HERE / "WITNESSES.json").read_text())
+    assert sorted(data["units"]) == ["E6", "E7"]
+    for name in ("E6", "E7"):
+        lines, rows = check_unit(name, data["units"][name])
+        controls(lines, rows, name)
+    sevens, partitions = e7_seven_clique_partitions([tuple(v) for v in data["units"]["E7"]["lines"]])
+    assert (sevens, partitions) == (288, 0), (sevens, partitions)
+    print(f"PASS E7 clique cover: no 8-set of pairwise non-orthogonal lines; {sevens} 7-sets; "
+          f"{partitions} partitions of the 63 lines into nine 7-sets")
+    print("PASS e6-e7-shadow-minrank-upper: mr2(Gamma_E6) <= 8 and mr2(Gamma_E7) <= 11")
+
+
+if __name__ == "__main__":
+    sys.exit(main())