diff --git a/research/e8-fprime-uniform-ceiling/README.md b/research/e8-fprime-uniform-ceiling/README.md
new file mode 100644
index 0000000000..fcf761ca20
--- /dev/null
+++ b/research/e8-fprime-uniform-ceiling/README.md
@@ -0,0 +1,124 @@
+# The F′ certificate ceiling on P120 is 360/17
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped proof with an exact finite certificate. No new κ,
+supplier or frontier change.**
+
+[PR #2962](https://github.com/CrocSwap/integer-mult-bounds/pull/2962)
+(DreamingOfClouds, `research/decoder-certificate-ceilings`, §2.1) proves that
+every linear rank-counting certificate in its larger family **F′** gives at most
+**24** on the E8 unit P120, and records as OPEN whether the sharper Theorem C
+value **360/17** also bounds F′. This package settles that item for P120:
+
+> Among all sets of `k` lines of E8, the least number of frames meeting the set
+> is **765** for `k = 8` and **701** for `k = 7`. Both are attained only by
+> pairwise-orthogonal sets. Hence the least feasible uniform weight is
+> `y = 8/765`, and the uniform F′ ceiling on P120 is
+> `2025 · 8/765 = 360/17`.
+
+With the predecessor's fake-decoder argument, every F′ certificate on P120
+gives at most 360/17 ≈ 21.18, not 24. F′ is therefore no stronger than F on
+P120 under this witness, and both stop far below the targeted floor 72.
+
+## Model (unchanged from PR #2962)
+
+`L` is the 120 root lines of E8. A frame is a maximal set of pairwise-orthogonal
+lines. There are 2025 frames, each of size 8. For a set `D` of lines, `meet(D)`
+is the number of frames meeting `D`. A uniform fake decoder puts weight `y` on
+every frame and costs `2025 y`. For F′ it is feasible when
+
+```text
+y · meet(D) >= min(|D|, 8)    for every set D of lines.
+```
+
+PR #2962 takes `y = 8/675` from a Bonferroni bound and gets the ceiling 24.
+Its script requires only `min(|D|-1, 8)` for non-orthogonal `D`. The result
+below is the same under both forms, because every binding set is a frame.
+
+## Proof
+
+Write `μ_k` for the least `meet(D)` over `k`-sets and `p(D)` for the number of
+non-orthogonal pairs in `D`.
+
+1. **Incidences.** Every line lies in 135 frames, every orthogonal pair in 15,
+   and no non-orthogonal pair in any frame (checked).
+2. **Bonferroni.** `meet(D) >= 135k - 15·(C(k,2) - p(D))`. For `k <= 6` this
+   gives `μ_k >= 135, 255, 360, 450, 525, 585`.
+3. **Pair caps.** A frame meets 765 frames and any 7 of its lines meet 701. By
+   step 2, an 8-set with `meet <= 765` has `p <= 7`. A 7-set with `meet <= 701`
+   has `p <= 4`.
+4. **Orthogonal cores.** By Caro–Wei, a graph on `k` vertices with `P` edges
+   has an independent set of size at least `k²/(k+2P)`. Apply it to the
+   non-orthogonality graph of `D`. Every candidate 8-set then contains an
+   orthogonal triple, and every candidate 7-set contains an orthogonal 4-set.
+5. **Symmetry.** The reflections in the 120 roots permute the lines and the
+   frames (checked), so they preserve `meet` and `p`. Under the group they
+   generate, orthogonal triples form one orbit and orthogonal 4-sets form two.
+6. **Search.** Every extension of each orbit representative within the pair cap
+   is enumerated exhaustively. The least meet is 765 for `k = 8` and 701 for
+   `k = 7`. Every minimiser has `p = 0`.
+7. **Ceiling.** `8/765` exceeds `k/μ_k` for every `k <= 7`, where the bound
+   uses step 2 for `k <= 6` and `7/701` for `k = 7`. For `|D| >= 9`, `meet(D) >= μ_8`. The least
+   feasible uniform weight is therefore `8/765`, and a frame makes it tight.
+   `2025 · 8/765 = 360/17`.
+
+**Positive control.** The same search on E7 (63 lines, 135 frames of size 7)
+reproduces the predecessor's MILP minima 55, 62 and 68 for `k = 5, 6, 7`. There
+the least meet 68 is below the frame value 71, attained by sets with six
+non-orthogonal pairs. So the search does find non-frame minimisers where they
+exist. It also shows that uniform weights cannot reach Theorem C's 945/71 on E7.
+That gap does not occur on P120.
+
+## Reproduce
+
+From the repository root, with the repository interpreter (CPython 3.12.15,
+standard library only):
+
+```sh
+python3.12 -W error -I -B research/e8-fprime-uniform-ceiling/verify.py
+python3.12 -W error -I -O -B research/e8-fprime-uniform-ceiling/verify.py
+python3.12 -B scripts/research_package.py --package research/e8-fprime-uniform-ceiling
+```
+
+Expected: `PASS_E8_FPRIME_UNIFORM_CEILING mu8 765 ceiling 360/17 no_new_kappa`.
+Each run takes about 35 seconds. `--emit` prints the recomputed
+[RESULT.json](RESULT.json). A normal run requires byte equality with it.
+The checks use `require()`, so they stay active under `-O`. A rejecting
+control confirms that weight `8/766` violates a frame's constraint.
+
+## Scope and limits
+
+- Uniform frame weights only. A non-uniform F′ certificate is bounded by this
+  witness. Whether 360/17 is the exact F′ optimum is not decided.
+- P120 only. P112, where the proven F′ ceiling is still 15968/667, is not
+  computed.
+- Theorem C, the F′ constraint form and the fake-decoder argument are cited
+  from PR #2962. They are not replayed here.
+- This is a statement about certificate families. It gives no decoder floor,
+  supplier, invoice or κ.
+
+## Open next questions
+
+1. **P112.** Does 15968/757 also bound F′ on P112? First step: the stabilizer
+   of the removed frame acts on the 112 lines. Use it with these pair caps and
+   orthogonal cores for `k = 7, 8`. Blocker: P112 is not line-transitive, its
+   1996 maximal orthogonal sets have mixed sizes, and no generators are
+   supplied here.
+2. **Non-uniform optimum.** Is 360/17 the exact F′ optimum on P120? First
+   step: an orbit-reduced linear program over W(E8) orbits of line sets, with
+   an exact dual.
+3. **E7 and E6.** On E7, uniform weights stop at 945/68 because a non-frame
+   7-set meets only 68 frames. Can non-uniform weights reach 945/71 there?
+
+## Credit
+
+DreamingOfClouds's PR #2962 supplies the certificate families F and F′,
+Theorem C, the fake-decoder argument, the F′ constraint, the Bonferroni
+ceiling 24 and the E7/E6 MILP values used as a control. The charging
+certificate shape is from #1977 and #798, as credited there. Those results are
+cited, not rechecked. The new contribution is the exact least meets for
+`k = 7, 8`, the orbit-reduced proof that frames minimise them, and the
+resulting 360/17 ceiling for F′ on P120. No predecessor credit line or frozen
+package is changed. Independent human and formal proof-kernel review are
+unclaimed.
diff --git a/research/e8-fprime-uniform-ceiling/RESULT.json b/research/e8-fprime-uniform-ceiling/RESULT.json
new file mode 100644
index 0000000000..0765e022dd
--- /dev/null
+++ b/research/e8-fprime-uniform-ceiling/RESULT.json
@@ -0,0 +1,70 @@
+{
+  "binding_size": 8,
+  "bonferroni_floor_k_le_6": {
+    "1": 135,
+    "2": 255,
+    "3": 360,
+    "4": 450,
+    "5": 525,
+    "6": 585
+  },
+  "e7_positive_control": {
+    "5": {
+      "frame_subset": 55,
+      "minimiser_nonorthogonal_pairs": [
+        0,
+        1,
+        2
+      ],
+      "minimum": 55
+    },
+    "6": {
+      "frame_subset": 63,
+      "minimiser_nonorthogonal_pairs": [
+        3,
+        4
+      ],
+      "minimum": 62
+    },
+    "7": {
+      "frame_subset": 71,
+      "minimiser_nonorthogonal_pairs": [
+        6
+      ],
+      "minimum": 68
+    }
+  },
+  "exact_minimum_meet": {
+    "7": {
+      "core_orbits": 2,
+      "k": 7,
+      "minimiser_nonorthogonal_pairs": [
+        0
+      ],
+      "minimum": 701,
+      "orthogonal_core": 4,
+      "pair_cap": 4,
+      "seed_frame_subset": 701
+    },
+    "8": {
+      "core_orbits": 1,
+      "k": 8,
+      "minimiser_nonorthogonal_pairs": [
+        0
+      ],
+      "minimum": 765,
+      "orthogonal_core": 3,
+      "pair_cap": 7,
+      "seed_frame_subset": 765
+    }
+  },
+  "maximal_orthogonal_sets": 2025,
+  "previous_proven_fprime_ceiling": "24",
+  "sets_through_line": 135,
+  "sets_through_nonorthogonal_pair": 0,
+  "sets_through_orthogonal_pair": 15,
+  "theorem_c_f_ceiling": "360/17",
+  "uniform_fprime_ceiling": "360/17",
+  "uniform_weight": "8/765",
+  "unit": "P120 (all 120 E8 root lines)"
+}
diff --git a/research/e8-fprime-uniform-ceiling/SOURCES.json b/research/e8-fprime-uniform-ceiling/SOURCES.json
new file mode 100644
index 0000000000..157e8a62f2
--- /dev/null
+++ b/research/e8-fprime-uniform-ceiling/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/decoder-certificate-ceilings/README.md",
+      "usage": "provenance",
+      "git_blob": "bf5a8fd5d353c304aa42e3333a9799ba082122bb",
+      "sha256": "22c0f68e0b553ce70054ece41a13b18b6e3fb45d84165ec6f0bfe78e2f39cc75"
+    }
+  ]
+}
diff --git a/research/e8-fprime-uniform-ceiling/TASK.json b/research/e8-fprime-uniform-ceiling/TASK.json
new file mode 100644
index 0000000000..44b1a3f5d2
--- /dev/null
+++ b/research/e8-fprime-uniform-ceiling/TASK.json
@@ -0,0 +1,97 @@
+{
+  "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": "Settle the OPEN item of PR2962 (research/decoder-certificate-ceilings, section 2.1) for the unit P120: compute the exact least number of maximal orthogonal sets meeting any k lines of E8 for k = 7, 8 and decide whether the uniform-weight fake decoder certifies the Theorem C value 360/17 for the larger family F'.",
+  "scope_change_reason": "This is an open question posed by the predecessor package about ceilings for linear rank-counting certificates of the E8 decoder cost. It sharpens a proven certificate ceiling (24 to 360/17) rather than constructing or pricing a changed decoder.",
+  "bottleneck_link": "Side result. It shows that the larger certificate family F' is no stronger than F on P120 under uniform weights, so linear rank-counting certificates of this shape still stop at 360/17, far below the targeted floor 72. No supplier, invoice or kappa is affected.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the exact P120 uniform ceiling and an E7 positive control. Do not extend to P112, non-uniform weights or the true decoder floor.",
+  "outcome": "completed",
+  "evidence": "Standard-library verifier: E8 lines and 2025 frames, incidence counts 135/15/0, reflection automorphisms, Bonferroni pair caps, Caro-Wei orthogonal cores, orbit representatives and exhaustive extension search for k = 7, 8; exact Fraction ceiling; E7 control reproduces the predecessor MILP minima 55, 62, 68; RESULT.json byte equality.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does 15968/757 also bound F' on P112?",
+      "why_it_matters": "It would settle the same OPEN item for the second unit, where the proven F' ceiling is still 15968/667.",
+      "first_step": "Compute exact least meets for k = 7, 8 over the 112 lines with automorphisms of P112 (the stabilizer of the removed frame), then reuse this pair-cap and orthogonal-core search.",
+      "blocked_by": "P112 is not line-transitive and its 1996 maximal orthogonal sets have mixed sizes; generators of the frame stabilizer are not supplied here."
+    },
+    {
+      "question": "Is 360/17 the exact optimum of F' on P120 over non-uniform weights?",
+      "why_it_matters": "The uniform witness gives an upper ceiling; a dual certificate would show no F' certificate exceeds a smaller value.",
+      "first_step": "Write the F' ceiling as an orbit-reduced linear program over W(E8) orbits of line sets and solve it exactly.",
+      "blocked_by": "The F' constraint family ranges over all line sets; an exact orbit LP is not built here."
+    },
+    {
+      "question": "Does the uniform F' ceiling on E6 or E7 improve beyond the predecessor's MILP-computed values with non-uniform weights?",
+      "why_it_matters": "On E7 the least meet 68 lies below the frame value 71, so uniform weights there cannot reach the Theorem C value 945/71.",
+      "first_step": "Use the same orbit LP on W(E7).",
+      "blocked_by": "No non-uniform witness or dual is computed."
+    }
+  ],
+  "claim_type": "scoped proof with an exact finite certificate",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220126",
+  "unrun_obligations": [
+    "No replay of PR2962's Theorem C witness, Bonferroni or MILP checks; Theorem C and the F' constraint form are cited premises.",
+    "No P112 computation, non-uniform F' optimum, true decoder floor, supplier, Lean, Docker or complete multiplication theorem."
+  ],
+  "environment": {
+    "python": "Python 3.12.15",
+    "platform": "Darwin arm64"
+  }
+}
diff --git a/research/e8-fprime-uniform-ceiling/VERIFY.json b/research/e8-fprime-uniform-ceiling/VERIFY.json
new file mode 100644
index 0000000000..268e855083
--- /dev/null
+++ b/research/e8-fprime-uniform-ceiling/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "E8 frames and incidence counts, reflection automorphisms, exact least meets for k = 7, 8 by pair caps, Caro-Wei cores and orbit search, exact 360/17 ceiling, rejecting weight control, E7 positive control and RESULT.json equality."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "The same exact checks under python -O; contracts use explicit require() and stay active."
+    }
+  ]
+}
diff --git a/research/e8-fprime-uniform-ceiling/verify.py b/research/e8-fprime-uniform-ceiling/verify.py
new file mode 100644
index 0000000000..8c2f938389
--- /dev/null
+++ b/research/e8-fprime-uniform-ceiling/verify.py
@@ -0,0 +1,290 @@
+"""Exact frame-meet minima on the 120 E8 root lines and the uniform F' ceiling.
+
+Standard library only. See README.md for the statement and proof.
+"""
+import itertools
+import json
+import pathlib
+import sys
+from fractions import Fraction
+
+FRAME_SIZE = 8
+
+
+def require(cond, msg):
+    """Contract check that stays active under python -O."""
+    if not cond:
+        raise SystemExit("FAIL: " + msg)
+
+
+def e8_lines():
+    """The 120 lines of E8 as doubled integer coordinates (norm 8)."""
+    roots = []
+    for i, j in itertools.combinations(range(8), 2):
+        for si in (2, -2):
+            for sj in (2, -2):
+                v = [0] * 8
+                v[i], v[j] = si, sj
+                roots.append(tuple(v))
+    for signs in itertools.product((1, -1), repeat=8):
+        if signs.count(-1) % 2 == 0:
+            roots.append(signs)
+    require(len(roots) == 240, 'len(roots) == 240')
+    lines = sorted(r for r in roots if next(x for x in r if x) > 0)
+    require(len(lines) == 120, 'len(lines) == 120')
+    return lines
+
+
+def dot(u, v):
+    return sum(a * b for a, b in zip(u, v))
+
+
+def canonical_line(v):
+    return v if next(x for x in v if x) > 0 else tuple(-x for x in v)
+
+
+def build():
+    lines = e8_lines()
+    n = len(lines)
+    pos = {v: i for i, v in enumerate(lines)}
+    gram = [[dot(a, b) // 4 for b in lines] for a in lines]
+    require(all(gram[i][i] == 2 for i in range(n)), 'all(gram[i][i] == 2 for i in range(n))')
+    require(all(abs(gram[i][j]) in (0, 1) for i in range(n) for j in range(n) if i != j), 'all(abs(gram[i][j]) in (0, 1) for i in range(n) for j in ran')
+    orth = [sum(1 << j for j in range(n) if j != i and gram[i][j] == 0) for i in range(n)]
+    return lines, pos, gram, orth
+
+
+def maximal_orthogonal_sets(n, orth):
+    """All maximal cliques of the orthogonality graph (bounded DFS, depth <= 8)."""
+    out = []
+    stack = [(1 << i, orth[i] & ~((1 << (i + 1)) - 1), orth[i]) for i in range(n)]
+    while stack:
+        members, cand, common = stack.pop()
+        require(bin(members).count("1") <= FRAME_SIZE, 'bin(members).count("1") <= FRAME_SIZE')
+        if common == 0:
+            out.append(members)
+        c = cand
+        while c:
+            t = (c & -c).bit_length() - 1
+            c &= c - 1
+            stack.append((members | 1 << t, cand & orth[t] & ~((1 << (t + 1)) - 1), common & orth[t]))
+    return sorted(out)
+
+
+def reflections(lines, pos):
+    """Permutation of the 120 lines induced by the reflection in each root."""
+    perms = []
+    for r in lines:
+        perm = []
+        for v in lines:
+            c = dot(v, r) // 4  # <v,r> in root normalisation (roots of norm 2)
+            w = tuple(a - c * b for a, b in zip(v, r))
+            perm.append(pos[canonical_line(w)])
+        require(sorted(perm) == list(range(len(lines))), 'sorted(perm) == list(range(len(lines)))')
+        perms.append(perm)
+    return perms
+
+
+def popcount(x):
+    return bin(x).count("1")
+
+
+def meet_bitsets(n, frames):
+    fb = [0] * n
+    for j, members in enumerate(frames):
+        for t in range(n):
+            if members >> t & 1:
+                fb[t] |= 1 << j
+    return fb
+
+
+def orthogonal_sets(n, orth, s):
+    """Sorted tuples of s pairwise-orthogonal lines (bounded DFS, depth s)."""
+    out = []
+    stack = [((i,), orth[i] & ~((1 << (i + 1)) - 1)) for i in range(n)]
+    while stack:
+        members, cand = stack.pop()
+        if len(members) == s:
+            out.append(members)
+            continue
+        c = cand
+        while c:
+            t = (c & -c).bit_length() - 1
+            c &= c - 1
+            stack.append((members + (t,), cand & orth[t] & ~((1 << (t + 1)) - 1)))
+    return out
+
+
+def orbit_representatives(sets, perms):
+    """Least element of each orbit of `sets` under the group generated by `perms`."""
+    index = {x: i for i, x in enumerate(sets)}
+    seen = [False] * len(sets)
+    reps = []
+    for i, start in enumerate(sets):
+        if seen[i]:
+            continue
+        seen[i] = True
+        reps.append(start)
+        queue = [start]
+        while queue:  # each set enters the queue at most once
+            cur = queue.pop()
+            for p in perms:
+                img = tuple(sorted(p[t] for t in cur))
+                j = index[img]  # KeyError would mean a non-automorphism
+                if not seen[j]:
+                    seen[j] = True
+                    queue.append(img)
+    return reps
+
+
+def caro_wei_floor(k, edges):
+    """Least integer >= k^2/(k+2*edges): every graph on k vertices with
+    `edges` edges has an independent set this large (Caro-Wei/Turan)."""
+    return -((-k * k) // (k + 2 * edges))
+
+
+def extension_minimum(n, orth, fb, rep, k, pmax):
+    """Minimum meet over k-sets D containing `rep` with at most pmax non-orthogonal pairs."""
+    base = 0
+    for t in rep:
+        base |= fb[t]
+    rep_mask = sum(1 << t for t in rep)
+    nonorth = [((1 << n) - 1) & ~orth[t] & ~(1 << t) for t in range(n)]
+    best, minimisers = None, []
+    stack = [(rep_mask, base, 0, ((1 << n) - 1) & ~rep_mask, len(rep))]
+    while stack:  # depth <= k - len(rep)
+        members, union, pairs, cand, size = stack.pop()
+        if size == k:
+            v = popcount(union)
+            if best is None or v < best:
+                best, minimisers = v, []
+            if v == best:
+                minimisers.append(members)
+            continue
+        c = cand
+        while c:
+            t = (c & -c).bit_length() - 1
+            c &= c - 1
+            q = pairs + popcount(nonorth[t] & members)
+            if q <= pmax:
+                stack.append((members | 1 << t, union | fb[t], q, c, size + 1))
+    return best, minimisers
+
+
+def exact_minimum(n, orth, fb, frames, perms, k, per, pair_max):
+    """Exact least meet over all k-sets of lines, via Bonferroni + Caro-Wei + orbits."""
+    frame0 = [t for t in range(n) if frames[0] >> t & 1]
+    seed = 0
+    for t in frame0[:k]:
+        seed |= fb[t]
+    incumbent = popcount(seed)
+    # Bonferroni: meet(D) >= per*k - pair_max*(orthogonal pairs of D).
+    pmax = (incumbent - per * k + pair_max * (k * (k - 1) // 2)) // pair_max
+    s = caro_wei_floor(k, pmax)
+    require(1 <= s <= k, '1 <= s <= k')
+    reps = orbit_representatives(orthogonal_sets(n, orth, s), perms)
+    best, minimisers = incumbent, []
+    for rep in reps:
+        value, found = extension_minimum(n, orth, fb, rep, k, pmax)
+        require(value is not None, "representative has no extension")
+        if value < best:
+            best, minimisers = value, []
+        if value == best:
+            minimisers.extend(found)
+    require(best <= incumbent, 'best <= incumbent')
+    nonorth_pairs = sorted({sum(1 for a, b in itertools.combinations(
+        [t for t in range(n) if d >> t & 1], 2) if not orth[a] >> b & 1) for d in minimisers})
+    return {"k": k, "seed_frame_subset": incumbent, "pair_cap": pmax,
+            "orthogonal_core": s, "core_orbits": len(reps), "minimum": best,
+            "minimiser_nonorthogonal_pairs": nonorth_pairs}
+
+
+def check_automorphisms(perms, frames):
+    """Each reflection permutes the maximal orthogonal sets, so it preserves meet."""
+    frame_set = set(frames)
+    for p in perms:
+        for f in frames:
+            img = sum(1 << p[t] for t in range(len(p)) if f >> t & 1)
+            require(img in frame_set, "reflection does not permute the frames")
+
+
+def unit_analysis(n, orth, perms, frame_count, frame_size, per, pair_max, sizes):
+    frames = maximal_orthogonal_sets(n, orth)
+    require(len(frames) == frame_count, "maximal orthogonal set count")
+    require({popcount(f) for f in frames} == {frame_size}, "maximal orthogonal set size")
+    fb = meet_bitsets(n, frames)
+    pairs = [(a, b) for a in range(n) for b in range(a + 1, n)]
+    require({popcount(x) for x in fb} == {per}, "sets through each line")
+    require({popcount(fb[a] & fb[b]) for a, b in pairs if orth[a] >> b & 1} == {pair_max},
+            "sets through each orthogonal pair")
+    require({popcount(fb[a] & fb[b]) for a, b in pairs if not orth[a] >> b & 1} == {0},
+            "sets through a non-orthogonal pair")
+    check_automorphisms(perms, frames)
+    return frames, fb, {k: exact_minimum(n, orth, fb, frames, perms, k, per, pair_max) for k in sizes}
+
+
+def e7_control(lines, gram, all_perms):
+    """Positive control: E7 = lines orthogonal to line 0 (predecessor MILP 55, 62, 68)."""
+    unit = [t for t in range(len(lines)) if gram[t][0] == 0]
+    loc = {t: i for i, t in enumerate(unit)}
+    orth = [sum(1 << loc[s] for s in unit if s != t and gram[t][s] == 0) for t in unit]
+    perms = [[loc[all_perms[r][t]] for t in unit] for r in unit]
+    _, _, exact = unit_analysis(len(unit), orth, perms, 135, 7, 15, 3, (5, 6, 7))
+    return {str(k): {"minimum": v["minimum"], "frame_subset": v["seed_frame_subset"],
+                     "minimiser_nonorthogonal_pairs": v["minimiser_nonorthogonal_pairs"]}
+            for k, v in exact.items()}
+
+
+def main():
+    lines, pos, gram, orth = build()
+    n = len(lines)
+    perms = reflections(lines, pos)
+    per, pair_max = 135, 15
+    frames, fb, exact = unit_analysis(n, orth, perms, 2025, FRAME_SIZE, per, pair_max, (7, 8))
+    bonferroni = {k: per * k - pair_max * (k * (k - 1) // 2) for k in range(1, 7)}
+    ratio = {k: Fraction(k, bonferroni[k]) for k in bonferroni}
+    ratio.update({k: Fraction(k, exact[k]["minimum"]) for k in exact})
+    y = max(ratio.values())
+    require(y == ratio[8] and all(ratio[k] < y for k in ratio if k != 8), "size 8 binds")
+    ceiling = len(frames) * y
+    require(ceiling == Fraction(360, 17), "uniform F' ceiling equals Theorem C value")
+    # Rejecting control: any smaller uniform weight violates a frame's constraint.
+    frame_meet = popcount(sum_bits(fb, frames[0], n))
+    require(Fraction(8, 766) * frame_meet < 8 and y * frame_meet == 8, "frame constraint is tight")
+    control = e7_control(lines, gram, perms)
+    require(control["7"]["minimum"] == 68 and control["7"]["frame_subset"] == 71,
+            "E7 control reproduces the predecessor MILP value 68 below the frame value 71")
+    return {
+        "unit": "P120 (all 120 E8 root lines)",
+        "maximal_orthogonal_sets": len(frames),
+        "sets_through_line": per, "sets_through_orthogonal_pair": pair_max,
+        "sets_through_nonorthogonal_pair": 0,
+        "exact_minimum_meet": {str(k): exact[k] for k in exact},
+        "bonferroni_floor_k_le_6": {str(k): v for k, v in bonferroni.items()},
+        "binding_size": 8,
+        "uniform_weight": str(y),
+        "uniform_fprime_ceiling": str(ceiling),
+        "previous_proven_fprime_ceiling": "24",
+        "theorem_c_f_ceiling": "360/17",
+        "e7_positive_control": control,
+    }
+
+
+def sum_bits(fb, members, n):
+    out = 0
+    for t in range(n):
+        if members >> t & 1:
+            out |= fb[t]
+    return out
+
+
+if __name__ == "__main__":
+    out = main()
+    text = json.dumps(out, indent=2, sort_keys=True) + "\n"
+    if "--emit" in sys.argv:
+        sys.stdout.write(text)
+    else:
+        expected = pathlib.Path(__file__).with_name("RESULT.json").read_text(encoding="utf-8")
+        require(expected == text, "RESULT.json mismatch")
+        m8 = out["exact_minimum_meet"]["8"]["minimum"]
+        print(f"PASS_E8_FPRIME_UNIFORM_CEILING mu8 {m8} ceiling {out['uniform_fprime_ceiling']} no_new_kappa")