diff --git a/research/nine-costly-rank8-copy-floor/PROOF.md b/research/nine-costly-rank8-copy-floor/PROOF.md
new file mode 100644
index 0000000000..e2ef7e01c2
--- /dev/null
+++ b/research/nine-costly-rank8-copy-floor/PROOF.md
@@ -0,0 +1,207 @@
+# Rank-8 factors of the E8 root Gram cost 9 per term
+
+Real coefficients. No new κ. The finite facts cited as **(Bk)** or **(Ck)** are
+checked by `verify.py`. One standard theorem is cited rather than recomputed.
+
+## 1. Model
+
+Let the 120 lines of the E8 root system have representatives \(r_i\) of norm 2,
+and let \(G_{ij}=\langle r_i,r_j\rangle\). The label pairing is
+\[
+S(i,j)=(\langle r_i,r_j\rangle+1)\bmod 2.
+\]
+Its \(120\times 120\) matrix has F2-rank 9 and distinct rows **(A.pairing-rank)**,
+so the labels span a 9-dimensional space on which \(S\) is nondegenerate. For
+line sets \(X,Y\), the copy cost \(\rho(X,Y)\) is the F2-rank of \(S\) between
+them. If \(V_X\) and \(V_Y\) are their label spans, nondegeneracy gives
+\[
+\rho(X,Y)=\dim V_X-\dim(V_X\cap V_Y^\perp),
+\]
+and in particular \(\rho=9\) whenever both spans are the whole label space.
+The complement of any proper violator spans exactly 8 dimensions
+**(B.kernel-sizes)**. Nonzero violators have sizes 56, 64 or 120
+**(B.violator-sizes)**.
+
+A real factorization \(\sum_{k=1}^{t} a_k b_k^{\mathsf T}=2I_8\) is called
+**root-linear**, or of factor rank \((8,8)\), when every factor is one of these
+normals in \(\mathbb R^8\). Equivalently, the \(120\times t\) matrices with
+columns \((\langle r_i,a_k\rangle)_i\) and \((\langle r_i,b_k\rangle)_i\) both
+have rank 8. The support of \(a_k\) is
+\(C(a_k)=\{i:\langle r_i,a_k\rangle\neq 0\}\). Zero factors are deleted; a
+nonzero term has both normals nonzero. The live roots span \(\mathbb R^8\)
+**(A.root-span)**.
+
+This is the root-span branch of the term-count gap in
+`docs/research/complex-decoder-scope-map.md`. It is not a binary factorization
+of the pairing matrix, and it does not allow a factor column to leave the
+8-dimensional root span.
+
+## 2. Hyperplane census
+
+The eight doubled vectors in `verify.py` are a base of simple roots: their
+Gram matrix is a Cartan matrix of determinant 1 with nonpositive off-diagonal
+entries **(A.cartan-det)**, and every root is an integer combination of them
+**(A.roots-in-lattice)**. Their \(\mathbb Z\)-span \(L\) is therefore the E8
+root lattice and is unimodular.
+
+**Lemma 1 (normal length).** Let \(H\) be a hyperplane spanned by roots, and
+let \(n\in L\) be a primitive normal. Then \(|n|^2\le 128\).
+
+*Proof.* Seven linearly independent roots in \(H\) have Gram determinant at
+most \(2^7=128\) by Hadamard's inequality. Their \(\mathbb Z\)-span sits in
+\(H\cap L\) at index \(m\ge 1\), so that determinant equals \(m^2|n|^2\). For
+the covolume claim: unimodularity and primitivity give a vector \(v\) with
+\(\langle v,n\rangle=1\), hence \(L=(H\cap L)\oplus\mathbb Z v\), and the unit
+covolume of \(L\) forces the covolume of \(H\cap L\) to equal \(|n|\). ∎
+
+**Cited theorem (W).** Every vector of an irreducible crystallographic root
+lattice is conjugate under the Weyl group to exactly one dominant weight: the
+closed fundamental chamber is a fundamental domain. Bourbaki, *Lie Groups and
+Lie Algebras*, Chapter VI, §1. The pairing and the orthogonal-line count are
+Weyl-invariant, so every lattice normal has the same flat profile as its
+dominant representative.
+
+`verify.py` enumerates all 383 dominant vectors of norm at most 128
+**(B.dominant-count)**. Their orthogonal-line counts are at most 42, or exactly
+63, or 120 for the origin. The 63-line vectors are the eight positive multiples
+of one root **(B.root-direction, B.root-flat-profile)**. Every orthogonal set
+that spans seven dimensions has one of the eight sizes
+\[
+14,16,22,23,28,37,42,63
+\]
+**(B.hyperplane-sizes)**. The 63-line flat has violator profile \((1,24,25)\)
+and its complement has label span 9. Every other seven-dimensional flat has
+smallest violator at least 14, paired violator at least 25, and complement span
+9 **(B.nonroot-flat-profile)**. The same root profile holds for all 120 roots,
+and the unique one-line violator is the root line itself **(B.every-root)**.
+
+**Lemma 2 (every real normal).** For every nonzero \(a\in\mathbb R^8\), the
+complement \(C(a)\) has label span 9. If \(a\) is not parallel to a root, every
+violator meets \(C(a)\) in at least 14 lines. A pair of violators meets \(C(a)\)
+in at least 25 lines. If \(a\) is parallel to a root \(\alpha\), the only
+violator of size less than 24 is \(\{\alpha\}\).
+
+*Proof.* Let \(U\) be the span of the roots orthogonal to \(a\). Those roots
+lie in a root-spanned hyperplane: while their span has dimension less than 7,
+some root lies outside it because the roots span \(\mathbb R^8\), and adjoining
+roots reaches dimension 7. A root-spanned hyperplane has a primitive lattice
+normal of norm at most 128 by Lemma 1, so Lemma W and the census give its
+profile.
+
+If \(\dim U=7\), then \(a\) is parallel to that normal. The census gives the
+stated violator bounds, and span 9 follows because every violator meets
+\(C(a)\). If \(\dim U\le 6\), at least two extra roots can be omitted from an
+extension to a root basis of \(\mathbb R^8\), giving two distinct hyperplanes
+\(H_1,H_2\) that contain \(U\). Their complements sit inside \(C(a)\). Suppose
+some functional met \(C(a)\) in at most 13 lines. Each hyperplane would then
+have a violator of size at most 13, so each would be a root flat and the
+functional would be that root's self-line functional. Distinct root lines have
+distinct functionals **(A.pairing-rank)**, so the two hyperplanes cannot share
+that functional. This contradiction gives the bound 14. One hyperplane already
+has paired-violator size at least 25, and the same inclusion raises the bound
+to \(C(a)\). ∎
+
+Over \(\mathbb F_2\), any two distinct nonzero functionals are linearly
+independent, so the paired minimum in the census is the codimension-2 count.
+
+## 3. Rank-(8, 8) bill
+
+**Theorem 3.** Let \(\sum_k a_k b_k^{\mathsf T}=2I_8\) with real vectors
+\(a_k,b_k\). After deleting terms with a zero factor, \(t\) nonzero terms
+remain, \(t\ge 8\), and the copy cost on all 120 lines is exactly \(9t\).
+In particular the cost is at least 72, and at least 81 when \(t\ge 9\).
+
+*Proof.* The identity has rank 8, and each nonzero outer product has rank 1,
+so \(t\ge 8\). For nonzero \(a_k\) and \(b_k\), Lemma 2 says both supports
+span the label space. Nondegeneracy makes the pairing rank exactly 9. The
+coordinate frame attains \(t=8\) and cost 72 **(C.frame-cost)**. Replacing
+one frame term \(f_0 f_0^{\mathsf T}\) by
+\((e_0+e_1)e_0^{\mathsf T}+(e_0-e_1)e_0^{\mathsf T}\) and keeping
+\(2e_i e_i^{\mathsf T}\) for \(i\ge 1\) gives nine terms, still of factor rank
+8, and cost 81 **(C.split-identity, C.split-cost)**. Seven frame terms do not
+factor \(2I\) **(C.seven-terms)**. ∎
+
+**Theorem 4.** Under the same identity, charge only the lines outside a deleted
+set \(P\) of size \(p\le 13\). The live copy cost is at least \(9t-p\). Thus
+on any 8-line puncture, nine nonzero terms cost at least 73.
+
+*Proof.* A live support \(C(a)\setminus P\) fails to span the label space only
+if some violator is covered by \(P\). By Lemma 2, \(p\le 13\) cannot do that
+unless \(a\) is parallel to a root \(\alpha\in P\), in which case exactly one
+functional dies. A second functional would be a violator pair of size at most
+13, but every pair has size at least 25. The surviving lines therefore span
+the whole hyperplane kernel of the self-line functional, not a smaller
+subspace.
+
+A term therefore has two live spans of dimension 8 or 9. If either span is the
+whole label space, nondegeneracy pins the cost at the other dimension, so the
+saving \(9-\rho\) is 0 or 1. If both spans have dimension 8, they are the
+kernels of the self-line functionals \(\lambda_\alpha\) and \(\lambda_\beta\).
+The annihilator of \(\ker\lambda_\beta\) is the span of the label \(u_\beta\),
+and \(u_\beta\) lies in \(\ker\lambda_\alpha\) exactly when
+\(S(u_\alpha,u_\beta)=0\), that is when \(\langle\alpha,\beta\rangle\) is odd.
+Hence
+\[
+\rho=8-[\langle\alpha,\beta\rangle\text{ is odd}],
+\]
+and the saving is 1 or 2. When \(\alpha\) and \(\beta\) are the same line,
+\(\langle\alpha,\alpha\rangle=2\) is even, so \(u_\alpha\) is not in its own
+kernel and the cost is 8. The saving is then 1. Deleting either sample root from its own
+complement drops the span from 9 to 8 **(C.self-line-drop)**. The two odd
+roots \(e_0+e_1\) and \(e_0+e_2\), with both lines deleted, have live pairing
+rank 7 **(C.odd-pair)**.
+
+The normals of nonzero terms are pairwise non-parallel on each side, because a
+parallel pair would make an off-diagonal entry of \(\sum a_k b_k^{\mathsf T}\)
+nonzero. A row normal parallel to a column normal of a different term is
+likewise impossible. Each deleted root line is therefore used by at most one
+term. The saving of a term is at most the number of such lines it uses, so
+the total saving is at most \(p\) and the live cost is at least \(9t-p\). ∎
+
+The nine-term witness, after deletion of the coordinate frame
+\(\{e_{2a}\pm e_{2a+1}\}\), costs \(8+8+7\cdot 9=79\) **(C.punctured-cost)**.
+That is above \(81-8=73\). The bound is a floor, not an attainment claim for
+\(t>8\).
+
+## 4. Why factor rank 9 is a different question
+
+Columns confined to the root span cannot cancel a coordinate without changing
+the normal. Leaving the span can. Replacing one frame column \(x\) by
+\(x+e\) and \(x-e\), with \(e\) supported at one nonzero coordinate, preserves
+the Gram identity and raises the left factor rank from 8 to 9. One of the two
+new terms then has pairing rank 8, and the nine-term cost is 80 rather than
+81 **(C.excursion)**. The rank hypothesis in Theorem 3 is therefore necessary
+for the exact count \(9t\).
+
+`research/ten-term-copy-cost` records a different ten-term factorization of
+rank \((9,9)\) with copy cost 72. That example sits outside Theorem 3. It
+meets the eight-term floor and does not undercut it. This package does not
+extend the floor to factor rank 9 or higher.
+
+## 5. E-graph corollary, cited
+
+PR1212, Theorem 1, proves that a real rank-8 solution of the E-graph equations
+on P120, or on the complement of any frame, equals \(D(2G)D^{-1}\) for an
+invertible diagonal \(D\). This package does not re-prove that theorem. Any
+factorization of such a matrix into real rank-1 terms whose two factor
+matrices both have rank 8 has columns in that eight-dimensional column space.
+The diagonal does not change zero patterns, so the supports and costs are those
+of Theorem 3 or, on a frame complement, of Theorem 4 with \(p=8\). Nine or
+more nonzero rank-(8, 8) terms therefore cost at least 81 on P120 and at least
+73 on a frame complement. Both are strictly above the eight-term floors 72
+and 64.
+
+Factor matrices of rank greater than 8, and E-graph solutions of rank greater
+than 8, remain outside this corollary. Complex coefficients remain outside it
+as well: PR1212's gauge algebra extends to characteristic zero, but the copy
+count uses the real normal geometry above, not the PR1077 extension.
+
+## 6. What is not claimed
+
+The selected record is unchanged. There is no frame, restoration, centre, or
+full per-call invoice, and no claim that a physical word improves κ. A
+factorization whose cost is at least 72 does not by itself produce a supplier.
+The dominant-weight transport uses cited theorem (W); the verifier does not
+enumerate the Weyl group. Lower-dimensional dominant flats are bounded by the
+census **(B.no-large-lower-flat)** only as a check of that list, not as a
+classification of every real subspace.
diff --git a/research/nine-costly-rank8-copy-floor/README.md b/research/nine-costly-rank8-copy-floor/README.md
new file mode 100644
index 0000000000..c429f0a867
--- /dev/null
+++ b/research/nine-costly-rank8-copy-floor/README.md
@@ -0,0 +1,107 @@
+# Rank-(8, 8) copy bill for every term count
+
+**Negative result for one algebraic branch. No new κ.**
+
+On the 120 real E8 root lines, every factorization
+\(\sum_k a_k b_k^{\mathsf T}=2I_8\) whose factors lie in \(\mathbb R^8\) has
+copy cost exactly \(9t\) after zero factors are deleted. Thus \(t\ge 8\), the
+eight-term frame costs 72, and nine or more terms cost at least 81. After
+deleting any set of at most 13 lines, the same identity costs at least
+\(9t-p\). On a coordinate-frame puncture, the explicit nine-term split costs
+79, which is above the floor \(73\) and above the eight-term floor \(64\).
+
+The hypothesis is the factor rank. A one-coordinate excursion raises the left
+factor rank to 9, preserves the Gram identity, and drops a term from 9 to 8
+(total 80). The published ten-term rank-(9, 9) example in
+`research/ten-term-copy-cost` costs 72 and is outside this theorem.
+
+PR1212's Theorem 1 identifies every real rank-8 E-graph solution on P120 and
+on a frame complement with a diagonal gauge of \(2G\). Rank-(8, 8)
+factorizations of that matrix inherit the same supports and the same floors.
+That is the root-span branch of the nine-or-more-term gap in
+[the decoder scope map](../../docs/research/complex-decoder-scope-map.md).
+Factor rank above 8, E-graph rank above 8, and complex coefficients stay open.
+The argument is in [PROOF.md](PROOF.md). The selected frontier is unchanged.
+
+## Scope and evidence
+
+Original card: `complex-rank-shape-decoder`. Scope **changed**, as recorded in
+[TASK.json](TASK.json). The card asks for a block-climb profile that beats the
+selected word. The scope map instead leaves the copy bill of nine or more
+costly rank-8 terms undetermined. This package prices the branch in which both
+factor matrices have rank 8, and it exhibits a rank-9 term whose cost drops
+below 9 so the branch boundary is visible.
+
+Base: `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority revision 7.
+Pins are in [SOURCES.json](SOURCES.json). The catalogue card and the selected
+record are historical provenance. The verifier recomputes its geometry from
+the standard library and does not import a predecessor package.
+
+| Check | Role |
+| --- | --- |
+| 511 violator sizes, kernel spans, Cartan determinant 1 | Label and lattice setup |
+| 383 dominant vectors of norm at most 128 | Replaces an uncomputed orbit list inside this norm bound |
+| All 120 root complements, profile (1, 24, 25) | Self-line reductions |
+| Frame, nine-term split, seven-term failure, mutated split | Exact identities and the 72 / 81 costs |
+| Frame puncture of the split, odd deleted pair, self-line drop | Puncture savings |
+| Rank-9 excursion of cost 80 | Shows the rank hypothesis is necessary |
+
+These finite checks are the census and the witnesses. Theorems 3 and 4 in the
+proof are written arguments from that census. They are not an enumeration of
+all real factorizations. The Weyl-chamber transport is cited from Bourbaki VI §1 and is not recomputed. PR1212's gauge theorem is cited and is not
+recomputed. No Lean, Docker, or frontier replay was run.
+
+## Reproduce
+
+From the repository root, CPython 3.12 and the standard library:
+
+```sh
+python3 -B research/nine-costly-rank8-copy-floor/verify.py
+python3 scripts/research_package.py --package research/nine-costly-rank8-copy-floor
+```
+
+The verifier prints one `PASS` line per check and exits 0 on
+
+```text
+PASS_NINE_COSTLY_RANK8_COPY_FLOOR rank88_cost=9t p120_nine=81 p112_nine=79 excursion_rank9_cost=80 no_new_kappa
+```
+
+Direct `python3 -O` keeps the same checks, because failures are explicit
+exceptions rather than assertions. Runtime is about one second. The command
+writes nothing.
+
+## Open next questions
+
+1. Can a factorization of \(2G\) with a factor rank at least 9 cost less than
+   72? Theorem 3 stops at rank 8, and the rank-9 excursion only drops one term
+   to 8 (total 80). The ten-term rank-(9, 9) example meets 72 without going
+   under it. Start from that example, or from the explicit excursion in
+   `verify.py`, and either cancel enough further label mass to go under 72 or
+   isolate a defect that restores the floor. Nothing in this package forbids
+   the attempt; the missing tool is a normal form once a column leaves the
+   root span.
+2. Can a real E-graph solution of rank at least 9, on P120 or on a frame
+   complement, have costly-term copy cost below 72 or 64? PR1212's Theorem 1
+   does not describe those solutions, so the support identification used here
+   does not apply. Start by writing one exact rank-9 solution of the E-graph
+   equations and pricing its terms. The blocker is the absence of a gauge
+   form, not a computation inside this package.
+
+## Credit
+
+The E-graph model and the eight-term copy problem come from DreamingOfClouds
+(PR717). The eight-term all-pairs floor, the label pairing, and the violator
+calculus come from themilkman216 (PR968). The rank-8 gauge form comes from
+Brett Halligan / burntout76 (PR1212). The scope map that isolates the
+nine-or-more-term gap was prepared by Arham Tahir, with the masked-rigidity
+navigation update by starship-s. The contrasting ten-term rank-(9, 9) cost-72
+example is the factorization recorded in `research/ten-term-copy-cost`
+(conorholds' construction; package notes by jwr). Nick Petalas's
+`research/e8-one-extra-direction` prices binary factorizations of the pairing
+matrix and is a different field; it is not a premise here. Unpaidmoon's earlier
+E8 label-rank and k8/u2 child-count notes bound child rank; they do not price
+this Gram factorization.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent
+human review or proof-assistant verification is claimed. New work is
+Apache-2.0.
diff --git a/research/nine-costly-rank8-copy-floor/SOURCES.json b/research/nine-costly-rank8-copy-floor/SOURCES.json
new file mode 100644
index 0000000000..58e81aab1f
--- /dev/null
+++ b/research/nine-costly-rank8-copy-floor/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "docs/research/complex-decoder-scope-map.md",
+      "usage": "provenance",
+      "git_blob": "727a8e0bd89da47e4842b02648c93466f42ff27f",
+      "sha256": "f22492089b77631cab712183beea11a8ed1ff0493d895a07f0022600d7af656c"
+    },
+    {
+      "path": "research/complex-frame-pair-decoders/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "889f3a653ed1bdbb7df61ebe3af4f2103602a1f4",
+      "sha256": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74"
+    },
+    {
+      "path": "research/complex-rank8-decoder-rigidity/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "5940f280c1ffe46148f4a75ab0107933f8f9ce29",
+      "sha256": "bccab452803cb0094685c298fe4fba5ceeddf9d6158a6af0b584712391db14c9"
+    }
+  ]
+}
diff --git a/research/nine-costly-rank8-copy-floor/TASK.json b/research/nine-costly-rank8-copy-floor/TASK.json
new file mode 100644
index 0000000000..648175ff73
--- /dev/null
+++ b/research/nine-costly-rank8-copy-floor/TASK.json
@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "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": "For real factorizations of 2I_8 by E8 root normals, prove the label-pairing copy cost is exactly 9 per nonzero term, hence at least 81 for nine or more terms; after deleting at most 13 lines the cost is at least 9t-p. Rank-9 excursions and E-graph rank above 8 stay outside the floor.",
+  "scope_change_reason": "The card asks for a block-climb profile beating the selected word by at least 5 percent. The decoder scope map leaves the copy bill of nine or more costly rank-8 terms undetermined, which is the overcomplete branch of that question. This package prices only the factor-rank-(8, 8) branch and shows it cannot undercut the eight-term floor. It does not produce a per-call profile or a kappa improvement.",
+  "bottleneck_link": "Rank-1 children are a large part of recursive cost, so a factorization that delivered the same rank-8 mass at lower copy cost would matter. Inside factor rank 8 the copy bill is exactly 9 per term, above the eight-term floor once nine or more terms are used. Any saving on this identity has to leave the root span. This is a side obstruction, not a new supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop when the rank-(8, 8) bill is proved for every term count and a rank-9 control shows the hypothesis is necessary. Do not search this class for a word that beats the selected kappa.",
+  "outcome": "negative-result",
+  "evidence": "research/nine-costly-rank8-copy-floor/PROOF.md and verify.py. P120 rank-(8, 8) cost is 9t (witnesses 72 and 81). Any deletion of at most 13 lines costs at least 9t-p (frame-puncture witness 79). A rank-9 excursion costs 80 and drops one term to 8. No selected-frontier edit.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance (session r28).",
+  "open_questions": [
+    {
+      "question": "Can a real factorization of 2G with at least one factor rank greater than 8 have label-pairing copy cost below 72?",
+      "why_it_matters": "Theorem 3 gives 9t only while both factors stay in the root span. The ten-term rank-(9, 9) example meets 72, and the rank-9 excursion in verify.py only reaches 80, so this is the smallest remaining way for extra terms to undercut the eight-term floor.",
+      "first_step": "Start from the explicit excursion in verify.py, section excursion_control, or from the ten-term factorization in research/ten-term-copy-cost, and either drive the measured copy cost under 72 or isolate a defect budget that forbids it.",
+      "blocked_by": "No normal form is known once a factor column leaves the eight-dimensional root span. This package does not supply one."
+    },
+    {
+      "question": "Can a real E-graph solution of rank at least 9 on P120 or on a frame complement have costly-term copy cost below the eight-term floor?",
+      "why_it_matters": "PR1212 Theorem 1, which this corollary cites, stops at rank 8. A rank-9 E-graph solution is the other half of the scope-map gap and is not priced by Theorems 3 or 4.",
+      "first_step": "Write one exact real rank-9 solution of the E-graph equations on P120 and compute the label-pairing costs of its costly terms.",
+      "blocked_by": "There is no gauge form for rank >= 9. Finding a solution is a new search, not a computation inside this census."
+    }
+  ]
+}
diff --git a/research/nine-costly-rank8-copy-floor/VERIFY.json b/research/nine-costly-rank8-copy-floor/VERIFY.json
new file mode 100644
index 0000000000..8402b07eda
--- /dev/null
+++ b/research/nine-costly-rank8-copy-floor/VERIFY.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "E8 line and pairing setup, dominant-weight hyperplane census through norm 128, all 120 root profiles, frame and nine-term rank-8 identities, frame-puncture and odd-pair controls, and one rank-9 excursion that drops a term to cost 8."
+    }
+  ]
+}
diff --git a/research/nine-costly-rank8-copy-floor/verify.py b/research/nine-costly-rank8-copy-floor/verify.py
new file mode 100644
index 0000000000..8f041abe75
--- /dev/null
+++ b/research/nine-costly-rank8-copy-floor/verify.py
@@ -0,0 +1,522 @@
+#!/usr/bin/env python3
+"""Rank-(8, 8) copy bill for every term count of the E8 root Gram.
+
+Finite census and witness controls for the written argument in PROOF.md.
+Standard library only. Explicit checks stay active under python -O.
+"""
+
+from fractions import Fraction
+import itertools
+import math
+
+
+def fail(message):
+    raise SystemExit("FAIL_NINE_COSTLY_RANK8_COPY_FLOOR " + message)
+
+
+def check(name, condition, detail):
+    if not condition:
+        fail(name + ": " + detail)
+    print("PASS", name)
+
+
+def dot(left, right):
+    return sum(a * b for a, b in zip(left, right))
+
+
+def doubled_inner(left, right):
+    value = dot(left, right)
+    if value % 4 != 0:
+        fail("doubled inner product is not a multiple of 4")
+    return value // 4
+
+
+def e8_roots():
+    roots = []
+    for i, j in itertools.combinations(range(8), 2):
+        for si in (1, -1):
+            for sj in (1, -1):
+                vector = [0] * 8
+                vector[i] = 2 * si
+                vector[j] = 2 * sj
+                roots.append(tuple(vector))
+    for signs in itertools.product((1, -1), repeat=8):
+        if signs.count(-1) % 2 == 0:
+            roots.append(tuple(signs))
+    return roots
+
+
+def root_lines(roots):
+    lines = []
+    seen = set()
+    for root in roots:
+        opposite = tuple(-entry for entry in root)
+        key = root if root > opposite else opposite
+        if key not in seen:
+            seen.add(key)
+            lines.append(root)
+    return lines
+
+
+def f2_rank(rows):
+    basis = {}
+    for value in rows:
+        while value:
+            pivot = value.bit_length() - 1
+            if pivot in basis:
+                value ^= basis[pivot]
+            else:
+                basis[pivot] = value
+                break
+    return len(basis)
+
+
+def rational_rank(columns):
+    if not columns:
+        return 0
+    width = len(columns)
+    height = len(columns[0])
+    matrix = [[Fraction(column[row]) for column in columns] for row in range(height)]
+    rank = 0
+    for column in range(width):
+        pivot = next((row for row in range(rank, height) if matrix[row][column]), None)
+        if pivot is None:
+            continue
+        matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank]
+        scale = matrix[rank][column]
+        for row in range(height):
+            if row != rank and matrix[row][column]:
+                factor = matrix[row][column] / scale
+                for entry in range(column, width):
+                    matrix[row][entry] -= factor * matrix[rank][entry]
+        rank += 1
+    return rank
+
+
+def real_span_rank(vectors):
+    return rational_rank([[Fraction(entry) for entry in vector] for vector in vectors])
+
+
+def solve_linear(matrix, rhs):
+    size = len(matrix)
+    augmented = [[Fraction(entry) for entry in row] + [Fraction(value)]
+                 for row, value in zip(matrix, rhs)]
+    for column in range(size):
+        pivot = next(row for row in range(column, size) if augmented[row][column])
+        augmented[column], augmented[pivot] = augmented[pivot], augmented[column]
+        scale = augmented[column][column]
+        for row in range(size):
+            if row != column and augmented[row][column]:
+                factor = augmented[row][column] / scale
+                augmented[row] = [entry - factor * other
+                                  for entry, other in zip(augmented[row], augmented[column])]
+    return [augmented[row][size] / augmented[row][row] for row in range(size)]
+
+
+def determinant(matrix):
+    size = len(matrix)
+    rows = [[Fraction(entry) for entry in row] for row in matrix]
+    sign = 1
+    for column in range(size):
+        pivot = next((row for row in range(column, size) if rows[row][column]), None)
+        if pivot is None:
+            return Fraction(0)
+        if pivot != column:
+            rows[column], rows[pivot] = rows[pivot], rows[column]
+            sign = -sign
+        for row in range(column + 1, size):
+            factor = rows[row][column] / rows[column][column]
+            for entry in range(column, size):
+                rows[row][entry] -= factor * rows[column][entry]
+    value = Fraction(sign)
+    for index in range(size):
+        value *= rows[index][index]
+    return value
+
+
+def pairing_rows(lines):
+    count = len(lines)
+    inner = [[doubled_inner(lines[i], lines[j]) for j in range(count)] for i in range(count)]
+    rows = [sum(((inner[i][j] + 1) & 1) << j for j in range(count)) for i in range(count)]
+    return inner, rows
+
+
+def label_masks(pairing):
+    basis = []
+    for index, row in enumerate(pairing):
+        if f2_rank([pairing[item] for item in basis] + [row]) == len(basis) + 1:
+            basis.append(index)
+        if len(basis) == 9:
+            break
+    coordinates = [sum(((pairing[index] >> bit) & 1) << place
+                       for place, bit in enumerate(basis))
+                   for index in range(len(pairing))]
+    masks = []
+    for functional in range(1, 512):
+        mask = 0
+        for index, coordinate in enumerate(coordinates):
+            if (functional & coordinate).bit_count() & 1:
+                mask |= 1 << index
+        masks.append(mask)
+    return masks
+
+
+def support_of(lines, normal):
+    mask = 0
+    for index, line in enumerate(lines):
+        if dot(line, normal):
+            mask |= 1 << index
+    return mask
+
+
+def pair_rank(pairing, left_mask, right_mask):
+    rows = []
+    left = left_mask
+    while left:
+        bit = left.bit_length() - 1
+        rows.append(pairing[bit] & right_mask)
+        left ^= 1 << bit
+    return f2_rank(rows)
+
+
+def span_of(pairing, mask):
+    rows = []
+    value = mask
+    while value:
+        bit = value.bit_length() - 1
+        rows.append(pairing[bit])
+        value ^= 1 << bit
+    return f2_rank(rows)
+
+
+def profile(masks, support):
+    hits = [mask & support for mask in masks]
+    ordered = sorted(hit.bit_count() for hit in hits)
+    smallest_pair = min((hits[left] | hits[right]).bit_count()
+                        for left in range(len(hits)) for right in range(left + 1, len(hits)))
+    return ordered[0], ordered[1], smallest_pair
+
+
+def simple_roots():
+    system = [(1, -1, -1, -1, -1, -1, -1, 1), (2, 2, 0, 0, 0, 0, 0, 0),
+              (-2, 2, 0, 0, 0, 0, 0, 0)]
+    for index in range(1, 6):
+        vector = [0] * 8
+        vector[index] = -2
+        vector[index + 1] = 2
+        system.append(tuple(vector))
+    return system
+
+
+def fundamental_weights(system):
+    weights = []
+    for index in range(8):
+        matrix = [[Fraction(entry, 2) for entry in root] for root in system]
+        weights.append(solve_linear(matrix, [1 if place == index else 0 for place in range(8)]))
+    return weights
+
+
+def dominant_weights(gram, norm_limit):
+    bounds = []
+    for index in range(8):
+        limit = 0
+        while gram[index][index] * (limit + 1) * (limit + 1) <= norm_limit:
+            limit += 1
+        bounds.append(limit)
+    found = []
+
+    def walk(index, coefficients, norm):
+        if index == 8:
+            found.append((tuple(coefficients), norm))
+            return
+        for value in range(bounds[index] + 1):
+            extra = gram[index][index] * value * value
+            extra += 2 * value * sum(gram[index][earlier] * coefficients[earlier]
+                                     for earlier in range(index))
+            if norm + extra > norm_limit:
+                break
+            coefficients.append(value)
+            walk(index + 1, coefficients, norm + extra)
+            coefficients.pop()
+
+    walk(0, [], 0)
+    return found
+
+
+def integer_weights(weights):
+    denominator = 1
+    for weight in weights:
+        for coordinate in weight:
+            denominator = denominator * coordinate.denominator // math.gcd(
+                denominator, coordinate.denominator)
+    return denominator, [tuple(int(coordinate * denominator) for coordinate in weight)
+                         for weight in weights]
+
+
+def flat_mask(lines, coefficients, integer_weight):
+    vector = [0] * 8
+    for coefficient, weight in zip(coefficients, integer_weight):
+        if coefficient:
+            for index in range(8):
+                vector[index] += coefficient * weight[index]
+    mask = 0
+    orthogonal = []
+    for index, line in enumerate(lines):
+        if dot(vector, line) == 0:
+            mask |= 1 << index
+            orthogonal.append(line)
+    return mask, orthogonal, vector
+
+
+def frame_normals():
+    normals = []
+    for plane in range(4):
+        for sign in (1, -1):
+            vector = [0] * 8
+            vector[2 * plane] = 1
+            vector[2 * plane + 1] = sign
+            normals.append(tuple(vector))
+    return normals
+
+
+def split_normals():
+    left = [(1, 1, 0, 0, 0, 0, 0, 0), (1, -1, 0, 0, 0, 0, 0, 0)]
+    right = [(1, 0, 0, 0, 0, 0, 0, 0), (1, 0, 0, 0, 0, 0, 0, 0)]
+    for index in range(1, 8):
+        row = [0] * 8
+        column = [0] * 8
+        row[index] = 2
+        column[index] = 1
+        left.append(tuple(row))
+        right.append(tuple(column))
+    return left, right
+
+
+def sum_outer(left_normals, right_normals):
+    matrix = [[0] * 8 for _ in range(8)]
+    for left, right in zip(left_normals, right_normals):
+        for row in range(8):
+            for column in range(8):
+                matrix[row][column] += left[row] * right[column]
+    return matrix
+
+
+def is_twice_identity(matrix):
+    for row in range(8):
+        for column in range(8):
+            expected = 2 if row == column else 0
+            if matrix[row][column] != expected:
+                return False
+    return True
+
+
+def term_costs(lines, pairing, left_normals, right_normals, deleted=0):
+    costs = []
+    for left, right in zip(left_normals, right_normals):
+        left_mask = support_of(lines, left) & ~deleted
+        right_mask = support_of(lines, right) & ~deleted
+        costs.append(pair_rank(pairing, left_mask, right_mask))
+    return costs
+
+
+def frame_deletion(lines):
+    deleted = 0
+    for normal in frame_normals():
+        doubled = tuple(2 * entry for entry in normal)
+        deleted |= 1 << lines.index(doubled)
+    return deleted
+
+
+def section_geometry(lines, pairing, inner):
+    count = len(lines)
+    check("A.lines", count == 120, "expected 120 root lines")
+    off_values = {inner[i][j] for i in range(count) for j in range(count) if i != j}
+    check("A.inner-products",
+          all(inner[i][i] == 2 for i in range(count)) and off_values == {-1, 0, 1},
+          "line inner products must be 2, 0 or ±1")
+    check("A.pairing-rank", f2_rank(pairing) == 9 and len(set(pairing)) == count,
+          "the label pairing must have rank 9 and distinct rows")
+    system = simple_roots()
+    cartan = [[doubled_inner(system[i], system[j]) for j in range(8)] for i in range(8)]
+    check("A.cartan-det", determinant(cartan) == 1 and
+          all(cartan[i][j] <= 0 for i in range(8) for j in range(8) if i != j),
+          "the simple-root Gram determinant must be 1")
+    coefficients = []
+    for root in e8_roots():
+        right = [doubled_inner(root, simple) for simple in system]
+        coefficients.append(solve_linear(cartan, right))
+    check("A.roots-in-lattice",
+          all(value.denominator == 1 for row in coefficients for value in row),
+          "every root must be an integer combination of the simple system")
+    check("A.root-span", real_span_rank(system) == 8, "the simple roots must span R^8")
+    return system, cartan
+
+
+def section_census(lines, pairing, masks):
+    violator_sizes = sorted({mask.bit_count() for mask in masks})
+    check("B.violator-sizes", violator_sizes == [56, 64, 120],
+          "nonzero label violators must have sizes 56, 64 and 120")
+    universe = (1 << 120) - 1
+    kernel_spans = sorted({span_of(pairing, universe ^ mask) for mask in masks if mask.bit_count() != 120})
+    check("B.kernel-sizes", kernel_spans == [8],
+          "the complement of every proper violator must span exactly 8 label dimensions")
+    system = simple_roots()
+    weights = fundamental_weights(system)
+    gram = [[sum(weights[i][place] * weights[j][place] for place in range(8))
+             for j in range(8)] for i in range(8)]
+    denominator, integer_weight = integer_weights(weights)
+    check("B.weight-denominator", denominator == 2, "fundamental weights must clear over denominator 2")
+    dominant = dominant_weights(gram, 128)
+    check("B.dominant-count", len(dominant) == 383, "expected 383 dominant vectors of norm at most 128")
+    unique = {}
+    root_direction = (0, 0, 0, 0, 0, 0, 1, 1)
+    root_like = []
+    for coefficients, norm in dominant:
+        if norm == 0:
+            continue
+        mask, orthogonal, vector = flat_mask(lines, coefficients, integer_weight)
+        unique.setdefault(mask, (coefficients, norm, orthogonal, vector))
+        if mask.bit_count() == 63:
+            root_like.append(vector)
+    rank7 = []
+    lower = []
+    for mask, (coefficients, norm, orthogonal, vector) in unique.items():
+        rank = real_span_rank(orthogonal)
+        record = (mask.bit_count(), rank, coefficients, norm, vector, orthogonal)
+        if rank == 7:
+            rank7.append((mask,) + record)
+        else:
+            lower.append(record)
+    sizes = sorted({item[1] for item in rank7})
+    check("B.hyperplane-sizes", sizes == [14, 16, 22, 23, 28, 37, 42, 63],
+          "root-spanned hyperplanes must have one of the eight flat sizes")
+    check("B.no-large-lower-flat", all(item[0] <= 42 for item in lower),
+          "a dominant vector whose orthogonal roots span at most 6 dimensions has at most 42 lines")
+    nonroot_ok = True
+    root_ok = True
+    for mask, size, rank, coefficients, norm, vector, orthogonal in (
+            (item[0], item[1], item[2], item[3], item[4], item[5], item[6]) for item in rank7):
+        smallest, second, pair = profile(masks, ((1 << 120) - 1) ^ mask)
+        span = span_of(pairing, ((1 << 120) - 1) ^ mask)
+        if size == 63:
+            root_ok = root_ok and smallest == 1 and second == 24 and pair == 25 and span == 9
+        else:
+            nonroot_ok = nonroot_ok and smallest >= 14 and pair >= 25 and span == 9
+    check("B.root-flat-profile", root_ok and len(root_like) == 8,
+          "the only 63-line dominant flat must be the root profile")
+    check("B.root-direction",
+          all(vector[index] * root_direction[place] == vector[place] * root_direction[index]
+              for vector in root_like for index in range(8) for place in range(8)),
+          "every 63-line dominant normal must be a multiple of the root weight")
+    check("B.nonroot-flat-profile", nonroot_ok,
+          "every other root hyperplane needs at least 14 violators and 25 for a pair")
+    root_profiles = True
+    self_line = True
+    for index, line in enumerate(lines):
+        orthogonal = 0
+        for other, candidate in enumerate(lines):
+            if doubled_inner(line, candidate) == 0:
+                orthogonal |= 1 << other
+        support = ((1 << 120) - 1) ^ orthogonal
+        smallest, second, pair = profile(masks, support)
+        root_profiles = root_profiles and orthogonal.bit_count() == 63 and smallest == 1
+        root_profiles = root_profiles and second == 24 and pair == 25 and span_of(pairing, support) == 9
+        hits = [mask & support for mask in masks if (mask & support).bit_count() == 1]
+        self_line = self_line and hits == [1 << index]
+    check("B.every-root", root_profiles and self_line,
+          "every root complement has profile (1, 24, 25), span 9, and self-line violator")
+    samples = [[1 if place == index else 0 for place in range(8)] for index in range(8)]
+    samples.append((1, 1, 1, 0, 0, 0, 0, 0))
+    sample_spans = [span_of(pairing, support_of(lines, sample)) for sample in samples]
+    check("B.sample-spans", sample_spans == [9] * len(samples),
+          "axis and triple samples are controls, not a substitute for the census")
+
+
+def section_witnesses(lines, pairing):
+    frame = frame_normals()
+    check("C.frame-identity", is_twice_identity(sum_outer(frame, frame)),
+          "the coordinate frame must factor 2I")
+    frame_costs = term_costs(lines, pairing, frame, frame)
+    check("C.frame-cost", frame_costs == [9] * 8 and rational_rank(frame) == 8,
+          "eight root-linear frame terms cost 9 each")
+    left, right = split_normals()
+    split_costs = term_costs(lines, pairing, left, right)
+    check("C.split-identity", is_twice_identity(sum_outer(left, right)) and rational_rank(left) == 8,
+          "the nine-term split must remain inside factor rank 8 and factor 2I")
+    check("C.split-cost", split_costs == [9] * 9 and sum(split_costs) == 81,
+          "nine rank-8 terms cost 81 on all 120 lines")
+    deleted = frame_deletion(lines)
+    punctured = term_costs(lines, pairing, left, right, deleted)
+    check("C.punctured-cost", deleted.bit_count() == 8 and punctured == [8, 8, 9, 9, 9, 9, 9, 9, 9],
+          "the same nine terms cost 79 after deleting the coordinate frame")
+    partial = frame[:7]
+    check("C.seven-terms", not is_twice_identity(sum_outer(partial, partial)),
+          "seven frame terms do not factor 2I")
+    mutated = [list(normal) for normal in left]
+    mutated[0][0] += 1
+    mutated = [tuple(normal) for normal in mutated]
+    check("C.mutated-split", not is_twice_identity(sum_outer(mutated, right)),
+          "changing one split coordinate must leave 2I")
+    excursion = excursion_control(lines, pairing, frame)
+    check("C.excursion", excursion == (9, 80, 8),
+          "a rank-9 excursion must be able to drop one term to cost 8")
+    odd = odd_pair_cost(lines, pairing)
+    check("C.odd-pair", odd == 7, "two odd punctured roots must have live pairing rank 7")
+    root_support = support_of(lines, (1, 1, 0, 0, 0, 0, 0, 0))
+    removed = root_support ^ (1 << lines.index((2, 2, 0, 0, 0, 0, 0, 0)))
+    check("C.self-line-drop", span_of(pairing, root_support) == 9 and span_of(pairing, removed) == 8,
+          "deleting a root from its own complement drops the label span from 9 to 8")
+
+
+def excursion_control(lines, pairing, frame):
+    columns = []
+    for normal in frame:
+        columns.append([dot(line, normal) for line in lines])
+    pivot = next(index for index, value in enumerate(columns[0]) if value)
+    spike = [0] * len(lines)
+    spike[pivot] = columns[0][pivot]
+    plus = [value + extra for value, extra in zip(columns[0], spike)]
+    minus = [value - extra for value, extra in zip(columns[0], spike)]
+    new_columns = [plus, minus] + columns[1:]
+    rank = rational_rank(new_columns)
+    costs = []
+    for column, normal in zip(new_columns, [frame[0], frame[0]] + frame[1:]):
+        right = support_of(lines, normal)
+        left = 0
+        for index, value in enumerate(column):
+            if value:
+                left |= 1 << index
+        costs.append(pair_rank(pairing, left, right))
+    # (x+e) y^T + (x-e) y^T = 2 x y^T, so halving both new right factors
+    # preserves the frame identity. The supports are unchanged by that scale.
+    if not is_twice_identity(sum_outer(frame, frame)):
+        return None
+    return rank, sum(costs), min(costs)
+
+
+def odd_pair_cost(lines, pairing):
+    alpha = (1, 1, 0, 0, 0, 0, 0, 0)
+    beta = (1, 0, 1, 0, 0, 0, 0, 0)
+    if doubled_inner((2, 2, 0, 0, 0, 0, 0, 0), (2, 0, 2, 0, 0, 0, 0, 0)) != 1:
+        fail("the odd-pair sample is not an odd root pair")
+    deleted = (1 << lines.index((2, 2, 0, 0, 0, 0, 0, 0))) | (
+        1 << lines.index((2, 0, 2, 0, 0, 0, 0, 0)))
+    left = support_of(lines, alpha) & ~deleted
+    right = support_of(lines, beta) & ~deleted
+    return pair_rank(pairing, left, right)
+
+
+def main():
+    roots = e8_roots()
+    lines = root_lines(roots)
+    inner, pairing = pairing_rows(lines)
+    masks = label_masks(pairing)
+    section_geometry(lines, pairing, inner)
+    section_census(lines, pairing, masks)
+    section_witnesses(lines, pairing)
+    print("PASS_NINE_COSTLY_RANK8_COPY_FLOOR rank88_cost=9t "
+          "p120_nine=81 p112_nine=79 excursion_rank9_cost=80 no_new_kappa")
+
+
+if __name__ == "__main__":
+    main()