diff --git a/research/scalar-pivot-header-counts/PROOF.md b/research/scalar-pivot-header-counts/PROOF.md
new file mode 100644
index 0000000000..6290dc02e8
--- /dev/null
+++ b/research/scalar-pivot-header-counts/PROOF.md
@@ -0,0 +1,146 @@
+# Complete headers for a common nonidentity scalar pivot
+
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Retained results and the new consumer
+
+Nick Petalas's [PR #4785](https://github.com/CrocSwap/integer-mult-bounds/pull/4785)
+proves the six-map sharpness criterion for every common scalar pivot.
+Its [proof](https://github.com/CrocSwap/integer-mult-bounds/blob/7c472563474e60185e6ca101a17622133d047e56/research/scalar-block-schur-dimension/PROOF.md)
+and [open question 2](https://github.com/CrocSwap/integer-mult-bounds/blob/7c472563474e60185e6ca101a17622133d047e56/research/scalar-block-schur-dimension/README.md)
+supply the exact consumer used here. Nick Petalas's
+[PR #4803](https://github.com/CrocSwap/integer-mult-bounds/pull/4803)
+already gives the two-shift distribution. Ali Romman's
+[Discussion #5261](https://github.com/CrocSwap/integer-mult-bounds/discussions/5261)
+already gives the distribution for any number of distinct scalar shifts.
+The distribution and the criterion are not new here.
+
+The new result combines these results with the factor weights from ssafwann's
+[PR #4678](https://github.com/CrocSwap/integer-mult-bounds/pull/4678)
+to count complete headers for every common nonzero scalar pivot. It resolves
+the named F5 caller and treats the collisions among the three scalar shifts.
+The code checks actual nonbinary Schur complements as well as matrix counts.
+
+## Ensemble and formula
+
+Let q be a prime power, d >= 1, and lambda in Fq be nonzero. Fix four
+joint-sector dimensions r00,r10,r01,r11 with total n >= d. The two fixed
+commuting projectors P0,Q0 have these sectors. A header is a complete
+ordered basis M in GL_n(Fq). Count headers for which the leading d blocks
+of M^-1 P0 M and M^-1 Q0 M are both lambda I. Call this count C. Let B be
+the number of these headers whose Schur commutator has rank 2d.
+There is no quotient by basis changes, sector orbits or residual orbits.
+
+Write I(r,k)=product_(j=0)^(k-1)(q^r-q^j), with value zero when k>r or
+k<0. Let G(r,k) be the Gaussian binomial coefficient. For a fixed d by d
+matrix T of rank rho, the number of factors X:Fq^r -> Fq^d and
+Y:Fq^d -> Fq^r with XY=T is
+
+```text
+U(r,d,rho) = sum_(k=rho)^min(r,d) G(d-rho,k-rho) I(r,k) q^[d(r-k)].
+```
+
+If X must be onto and Y must be injective, the count is
+
+```text
+A(r,d,rho) = I(r,d) q^[rho(r-d)] I(r-d,d-rho), for r>=d;
+A(r,d,rho) = 0, for r<d.
+```
+
+These are the retained factor-count arguments. For U, choose im X containing
+im T, choose the onto map to it, then choose all lifts of T. For A, choose
+X onto. Modulo ker X, Y is fixed by T. On ker T it must inject into ker X;
+on a complement it has q^[rho(r-d)] lifts. This proves the formulas over
+all finite fields, with no assumption on the Jordan form of T.
+
+For H=pi P0 Q0 i, the sector products are
+
+```text
+T00 = H-(2lambda-1)I,  T10=T01=lambda I-H,  T11=H.
+```
+
+Let rho_j=rank T_j. For each fixed H the common-pivot split count is
+product_j U(r_j,d,rho_j). The sharp split count is
+U(r00,d,rho00) times product_(j=10,01,11) A(r_j,d,rho_j).
+This follows directly from the retained six-map criterion. The four products
+sum to I, so the stacked maps always satisfy pi i=I. In particular i is
+injective and pi is onto. Every such pair (i,pi) has exactly GL_(n-d)(Fq)
+complete headers: choose any ordered basis of ker pi after the columns of i.
+Thus the complete counts are
+
+```text
+C = |GL_(n-d)| sum_H product_j U(r_j,d,rho_j(H)),
+B = |GL_(n-d)| sum_H U(r00,d,rho00(H)) product_(j=10,01,11) A(r_j,d,rho_j(H)).
+```
+
+The unconditional sharp probability is B/|GL_n|. The conditional probability
+is B/C only when C>0. The implementation returns None when C=0.
+
+## Three shifts and their collisions
+
+Only the nullities at 0,lambda,2lambda-1 enter these weights. Since lambda
+is nonzero, the first two shifts are distinct. If lambda=1, the third shift
+is lambda. If 2lambda=1, it is zero; this case requires odd characteristic.
+In every other case all three shifts are distinct. The implementation takes
+this equality class as a supplied premise. It does not interpret integer
+labels as extension-field elements. Its verifier computes the class from
+actual field arithmetic.
+
+Use the retained multi-shift incidence law. For t distinct shifts and a tuple
+k with K=sum k_i<=d, let s_i=sum_(j<i) k_j. Then
+
+```text
+M(k)=q^[d(d-K)] product_i G(d-s_i,k_i) q^[s_i k_i]
+    =sum_(e>=k) N(e) product_i G(e_i,k_i).
+```
+
+The first formula chooses disjoint subspaces on which H has each specified
+eigenvalue, then its arbitrary extension. The second counts those subspaces
+inside the actual eigenspaces. Descending componentwise subtraction gives
+N(k) exactly, because the diagonal coefficient is one. Replace the sums over
+H above by sums over N(k) and the corresponding ranks. This preserves the
+joint distribution. It does not assume independence of the ranks.
+
+For fixed t<=3 there are binomial(d+t,t) tuples and O(d^(2t)) arithmetic
+summands in this direct implementation. All integer bit lengths are polynomial
+in d and log q. This is an application of the predecessor incidence law,
+not a new counting shortcut. The supplied q must be a prime power.
+
+## Named F5 caller
+
+Take lambda=2, d=2, profile (1,2,2,2). The source asks about H=J2(3).
+Then the four ranks are (1,2,2,2). U(1,2,1)=4 and A(2,2,2)=480, so
+there are exactly 4*480^3=442368000 sharp splits for this fixed H.
+Multiply by |GL5(F5)| for complete headers.
+
+For the full profile, sharpness requires H and 2I-H invertible and
+rank(H-3I)<=1. H=3I has U(1,2,0)=49. For H-3I of rank one, there are
+24 nonzero nilpotent matrices and 30 matrices of each allowed nonzero trace
+1 and 3. Traces 2 and 4 would make H or 2I-H singular. Thus there are 84
+rank-one matrices and the full sharp split count is
+
+```text
+(49+84*4)*480^3 = 42577920000.
+```
+
+The independent census checks all 625 matrices H, including the common-pivot
+count without the full-rank conditions. RESULT.json gives the exact integers
+and reduced fractions. These counts distinguish the Jordan and scalar cases
+which have the same nullities at 0 and lambda. Omitting the third shift loses
+that distinction.
+
+## Actual nonbinary Schur check and limits
+
+Over F4=F2[x]/(x^2+x+1), take lambda=x, d=1 and profile (0,1,1,1).
+The verifier checks all 4032 pairs of a nonzero inclusion column and a
+projection row. Exactly 27 have the required common pivot. For each it forms
+an actual header with a kernel basis, conjugates both projectors, takes the
+Schur complements with lambda^-1, and obtains commutator rank two.
+There are 27*|GL2(F4)|=4860 complete headers, or probability 3/112.
+The verifier checks all split pairs, not all 181440 complete headers.
+
+The algebraic result is one-block only. It does not give a later-guard
+transition, residual-orbit law, physical cover, header generator, paid
+consumer, native theorem or complete multiplication theorem. The selected
+kappa and all its open assumptions remain unchanged. No independent human
+or proof-kernel acceptance is claimed.
diff --git a/research/scalar-pivot-header-counts/README.md b/research/scalar-pivot-header-counts/README.md
new file mode 100644
index 0000000000..c58f53c3b5
--- /dev/null
+++ b/research/scalar-pivot-header-counts/README.md
@@ -0,0 +1,57 @@
+# Exact nonidentity scalar-pivot header counts
+
+This package answers the header-frequency question in Nick Petalas's
+[PR #4785](https://github.com/CrocSwap/integer-mult-bounds/pull/4785).
+It gives exact complete-header counts for every nonzero common scalar pivot,
+including the three-shift generic case and both shift-collision cases.
+The named F5 caller has 442368000 sharp splits at H=J2(3), and 42577920000
+sharp splits over its full profile. Each split has |GL5(F5)| completions.
+
+[PROOF.md](PROOF.md) states the ensemble, weights, proof and predecessor
+credit. [counts.py](counts.py) evaluates the exact law. [RESULT.json](RESULT.json)
+records the checks and full integers. The actual F4 split/Schur oracle checks
+4032 pairs and gives 4860 complete headers, with probability 3/112.
+Five nonidentity matrix contexts include F4 and F8. The generic q=4,d=12
+case uses 455 strata for a space of 2^288 compressed matrices.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/scalar-pivot-header-counts
+```
+
+Both registered Python3.12 modes print `PASS_SCALAR_PIVOT_HEADER_COUNTS`.
+The checks also retain 25291 two-shift matrix cases, 11527 factor pairs,
+382 product targets, five binary source comparisons and 20160 literal
+binary headers. The standard library suffices. The checker verifies source
+bytes and the complete typed receipt. Prime-power q and the scalar equality
+class are supplied premises of the integer-only count API.
+
+The scalar criterion, two-shift and multi-shift incidence laws, factor counts
+and completion factor are credited predecessor results. This contribution
+binds them to the missing nonidentity weights and the actual named caller.
+It does not change kappa, price a physical cover or prove later-guard survival.
+Lean, Docker, selected cold replay and full-history validation were not run.
+
+## Open next questions
+
+Can these exact nonbinary masses support one state-aware second Schur step?
+Start with the complete F4 split domain here. Preserve the ordered residual
+pair; its two matrices need not commute. A nullity-only repeated transition
+is not justified. Physical selection and emission need a separate paid proof.
+
+## Coordination and credit
+
+Base 7c472563474e60185e6ca101a17622133d047e56, priority 7.
+[SOURCES.json](SOURCES.json) pins the retained source files. The public
+[multi-shift proof](https://github.com/CrocSwap/integer-mult-bounds/discussions/5261)
+is also retained as an explicit predecessor. See PROOF.md for source links.
+
+A separate general-H gluing artifact was shared as corroboration for Mihir
+Srivastava's concurrent claim. It is not part of this PR. A deeper overlap
+check also found that the two-shift shortcut was already complete. This
+package makes no new claim for either result. Current PR and Discussion
+bodies and relevant main notes were checked; arbitrary historical diffs and
+unpublished work remain outside that coverage.
+
+Ali Romman with substantial OpenAI Codex assistance in derivation,
+implementation, review and verification. Apache-2.0. Source notices remain
+unchanged. Independent human and proof-kernel review remain open.
diff --git a/research/scalar-pivot-header-counts/RESULT.json b/research/scalar-pivot-header-counts/RESULT.json
new file mode 100644
index 0000000000..112f4ee891
--- /dev/null
+++ b/research/scalar-pivot-header-counts/RESULT.json
@@ -0,0 +1,269 @@
+{
+  "binary_comparisons": [
+    {
+      "conditional_probability": "3/172",
+      "d": 1,
+      "profile": [
+        1,
+        1,
+        1,
+        2
+      ],
+      "sharp_probability": "3/496"
+    },
+    {
+      "conditional_probability": "9/100",
+      "d": 1,
+      "profile": [
+        0,
+        2,
+        2,
+        1
+      ],
+      "sharp_probability": "9/496"
+    },
+    {
+      "conditional_probability": "27/20128",
+      "d": 2,
+      "profile": [
+        2,
+        2,
+        2,
+        2
+      ],
+      "sharp_probability": "27/2763520"
+    },
+    {
+      "conditional_probability": "189/34864",
+      "d": 2,
+      "profile": [
+        1,
+        3,
+        3,
+        2
+      ],
+      "sharp_probability": "189/6353920"
+    },
+    {
+      "conditional_probability": "13474755/17178857984",
+      "d": 3,
+      "profile": [
+        3,
+        3,
+        3,
+        4
+      ],
+      "sharp_probability": "898317/57139711442944"
+    }
+  ],
+  "controls": 4,
+  "counts_sha256": "b16d6b834ad64ee07af4db12bf354dd3f7b930458050549a55cfb28cce89e79b",
+  "domains": [
+    {
+      "d": 1,
+      "matrices": 2,
+      "nonempty_strata": 2,
+      "q": 2
+    },
+    {
+      "d": 2,
+      "matrices": 16,
+      "nonempty_strata": 6,
+      "q": 2
+    },
+    {
+      "d": 3,
+      "matrices": 512,
+      "nonempty_strata": 10,
+      "q": 2
+    },
+    {
+      "d": 1,
+      "matrices": 3,
+      "nonempty_strata": 3,
+      "q": 3
+    },
+    {
+      "d": 2,
+      "matrices": 81,
+      "nonempty_strata": 6,
+      "q": 3
+    },
+    {
+      "d": 3,
+      "matrices": 19683,
+      "nonempty_strata": 10,
+      "q": 3
+    },
+    {
+      "d": 1,
+      "matrices": 5,
+      "nonempty_strata": 3,
+      "q": 5
+    },
+    {
+      "d": 2,
+      "matrices": 625,
+      "nonempty_strata": 6,
+      "q": 5
+    },
+    {
+      "d": 1,
+      "matrices": 4,
+      "nonempty_strata": 3,
+      "q": 4
+    },
+    {
+      "d": 2,
+      "matrices": 256,
+      "nonempty_strata": 6,
+      "q": 4
+    },
+    {
+      "d": 1,
+      "matrices": 8,
+      "nonempty_strata": 3,
+      "q": 8
+    },
+    {
+      "d": 2,
+      "matrices": 4096,
+      "nonempty_strata": 6,
+      "q": 8
+    }
+  ],
+  "factor_pairs": 11527,
+  "factor_targets": 382,
+  "generic_large": {
+    "common": {
+      "bits": 4032,
+      "sha256": "1e314354aaab82379f63cb26bf131df95c21b602b474834566aab5a52819d95f"
+    },
+    "d": 12,
+    "q": 4,
+    "sharp": {
+      "bits": 4029,
+      "sha256": "02bb2d9db919591f41a6a22075f1548c8d9de380d12e8bb8f8d453921e481098"
+    },
+    "strata": 455,
+    "total": {
+      "bits": 4608,
+      "sha256": "d46870f27125ae0fb93759dbe7c56f6d89f189bce943f80a6ff84d39c5d02c34"
+    }
+  },
+  "large": [
+    {
+      "common": {
+        "bits": 14339,
+        "sha256": "7aa1aaa1838ebae6539331eaf6c1e9e9c9bc60b26dbcaabd871890bf66f83356"
+      },
+      "d": 32,
+      "matrix_space_bits": 1025,
+      "q": 2,
+      "sharp": {
+        "bits": 14324,
+        "sha256": "74e8ef41493a19d0898382a6e7abe62796a330634cbccbf6e1dcaee4bb116164"
+      },
+      "strata": 561,
+      "total": {
+        "bits": 16383,
+        "sha256": "ee549992dcb6e16e61191a84eb17da2ff0dd6430a8063996bbfd3512f4fc741e"
+      }
+    },
+    {
+      "common": {
+        "bits": 7170,
+        "sha256": "cbd0b64f26ecf641918954c985577959a42bba727986ab2a0c6a9cc3f8fe5a0a"
+      },
+      "d": 16,
+      "matrix_space_bits": 513,
+      "q": 4,
+      "sharp": {
+        "bits": 7165,
+        "sha256": "0fe5fb1ed77370aa46301134becd442c30634de72654682e6cc6240f85148537"
+      },
+      "strata": 153,
+      "total": {
+        "bits": 8192,
+        "sha256": "22b553649a4aceab21558d36038575ed77197c9b159d9e48ad9f0515926ed39b"
+      }
+    }
+  ],
+  "literal_F4": {
+    "admissible_splits": 27,
+    "probability": "3/112",
+    "sharp_headers": 4860,
+    "split_pairs": 4032,
+    "total_headers": 181440
+  },
+  "literal_headers": 20160,
+  "matrices": 25291,
+  "named_F5": {
+    "conditional_probability": "154/505",
+    "fixed_H_sharp_headers": 100247206625280000000000000,
+    "fixed_H_sharp_splits": 442368000,
+    "full_profile_common_headers": 31640524591104000000000000000,
+    "full_profile_sharp_headers": 9648793637683200000000000000,
+    "full_profile_sharp_splits": 42577920000,
+    "probability": "33792/47301640625",
+    "total_headers": 13506266841692625000000000000000000
+  },
+  "scalar_censuses": [
+    {
+      "common_splits": 30083948176896,
+      "conditional_probability": "6987136/80600427",
+      "d": 2,
+      "matrices": 81,
+      "pivot_class": "half",
+      "q": 3,
+      "scalar": 2,
+      "sharp_probability": "17199104/989794159299",
+      "sharp_splits": 2607934537728
+    },
+    {
+      "common_splits": 139622400000,
+      "conditional_probability": "154/505",
+      "d": 2,
+      "matrices": 625,
+      "pivot_class": "generic",
+      "q": 5,
+      "scalar": 2,
+      "sharp_probability": "33792/47301640625",
+      "sharp_splits": 42577920000
+    },
+    {
+      "common_splits": 317750400000,
+      "conditional_probability": "0",
+      "d": 2,
+      "matrices": 625,
+      "pivot_class": "half",
+      "q": 5,
+      "scalar": 3,
+      "sharp_probability": "0",
+      "sharp_splits": 0
+    },
+    {
+      "common_splits": 3514752000,
+      "conditional_probability": "51/226",
+      "d": 2,
+      "matrices": 256,
+      "pivot_class": "generic",
+      "q": 4,
+      "scalar": 2,
+      "sharp_probability": "11475/4071022592",
+      "sharp_splits": 793152000
+    },
+    {
+      "common_splits": 284651776475136,
+      "conditional_probability": "1351/2836",
+      "d": 2,
+      "matrices": 4096,
+      "pivot_class": "generic",
+      "q": 8,
+      "scalar": 2,
+      "sharp_probability": "1787373/62245791858688",
+      "sharp_splits": 135601040203776
+    }
+  ],
+  "status": "PASS_SCALAR_PIVOT_HEADER_COUNTS"
+}
diff --git a/research/scalar-pivot-header-counts/SOURCES.json b/research/scalar-pivot-header-counts/SOURCES.json
new file mode 100644
index 0000000000..ad43d8d446
--- /dev/null
+++ b/research/scalar-pivot-header-counts/SOURCES.json
@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c472563474e60185e6ca101a17622133d047e56",
+  "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": "research/schur-header-count/README.md",
+      "usage": "input",
+      "git_blob": "5e644cf316312c0fdd489c8d33911583f1b88af2",
+      "sha256": "472295f32ebf3fcdc8daa4137af63db70d9943de7cbb97e47ed272823b2a227e"
+    },
+    {
+      "path": "research/schur-header-count/verify.py",
+      "usage": "input",
+      "git_blob": "0da95c051b1cafa3da6838495e8b7829c79f0971",
+      "sha256": "22fc801fda7212a64410a8fb55530764166c971bc4da9a96b1a2a5500fa539e3"
+    },
+    {
+      "path": "research/schur-nilpotent-extension/README.md",
+      "usage": "input",
+      "git_blob": "1e738614a419c8f91941886179bdf235e4e5ed52",
+      "sha256": "7e5e74f4e5ddc1793ac6e427a80492d8d978aa78f01f189e33d2831147c9639a"
+    },
+    {
+      "path": "research/schur-rank-pair-law/README.md",
+      "usage": "input",
+      "git_blob": "f81da1f15cc3e388c57e89d8a3a36a4e6ecf3969",
+      "sha256": "b81dd6c355f4d13e03be85dfe76ab99b0840eeaeddaf1da65deca7d3e83046ba"
+    },
+    {
+      "path": "research/schur-rank-pair-law/PROOF.md",
+      "usage": "input",
+      "git_blob": "9673ed63693032fe4841400cd617d1a8122c3366",
+      "sha256": "d29465a73aa399c3e632b7b77ca5b31615c0de1a60cbc4984ad7c7668d3937dc"
+    },
+    {
+      "path": "research/scalar-block-schur-dimension/PROOF.md",
+      "usage": "input",
+      "git_blob": "0c4eb58ed9e08522e8d2a054148d069c7879a1ca",
+      "sha256": "a9353583643e35fdcaac8864bb4c2321ca7d8bee3755583a20bee9383626583b"
+    },
+    {
+      "path": "research/scalar-block-schur-dimension/README.md",
+      "usage": "input",
+      "git_blob": "cbed8b8dd78912e6ef101dd1c5f2cb01a05bfb6a",
+      "sha256": "681c059c2a7bcbe3c522bb8ee56675204072804a28972fb47517520aa6f9ffb3"
+    }
+  ]
+}
diff --git a/research/scalar-pivot-header-counts/TASK.json b/research/scalar-pivot-header-counts/TASK.json
new file mode 100644
index 0000000000..170cf4eb46
--- /dev/null
+++ b/research/scalar-pivot-header-counts/TASK.json
@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "7c472563474e60185e6ca101a17622133d047e56",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact complete-header counts for nonidentity common scalar pivots, with the named F5 Jordan caller, shift collisions and an actual F4 split/Schur oracle.",
+  "scope_change_reason": "Source review found that the two-shift shortcut and multi-shift incidence law were already complete. This package takes the explicit nonidentity weight handoff from PR4785 and Discussion5261.",
+  "bottleneck_link": "The scalar-block dimension theorem left its actual nonbinary header frequencies open. This count supplies those frequencies without assuming independent shifted ranks.",
+  "budget_minutes": 90,
+  "stop_rule": "One exact scalar-pivot count and actual finite-field consumer. No later-guard, physical generator, supplier or kappa claim.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, counts.py, verify.py, RESULT.json",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, review and verification; no independent human or proof-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Can this exact nonbinary mass support one state-aware second Schur step?",
+      "why_it_matters": "One-block mass does not give full-guard survival.",
+      "first_step": "Use the complete F4 split domain and preserve the ordered residual pair.",
+      "blocked_by": "Residuals need not commute; physical header generation remains unpriced."
+    }
+  ]
+}
diff --git a/research/scalar-pivot-header-counts/VERIFY.json b/research/scalar-pivot-header-counts/VERIFY.json
new file mode 100644
index 0000000000..15cf7a32c9
--- /dev/null
+++ b/research/scalar-pivot-header-counts/VERIFY.json
@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/schur-header-count/README.md",
+    "research/schur-header-count/verify.py",
+    "research/schur-nilpotent-extension/README.md",
+    "research/schur-rank-pair-law/README.md",
+    "research/schur-rank-pair-law/PROOF.md",
+    "research/scalar-block-schur-dimension/PROOF.md",
+    "research/scalar-block-schur-dimension/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 90,
+      "checks": "Exact scalar header weights with shift collisions, complete F4 split and Schur oracle, named F5 Jordan caller, prime and extension-field matrix/factor domains, retained binary cases, source hashes and typed receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 90,
+      "checks": "Exact scalar header weights with shift collisions, complete F4 split and Schur oracle, named F5 Jordan caller, prime and extension-field matrix/factor domains, retained binary cases, source hashes and typed receipt."
+    }
+  ]
+}
diff --git a/research/scalar-pivot-header-counts/counts.py b/research/scalar-pivot-header-counts/counts.py
new file mode 100644
index 0000000000..4243f28d2f
--- /dev/null
+++ b/research/scalar-pivot-header-counts/counts.py
@@ -0,0 +1,96 @@
+"""Exact sharp-header counts without enumerating compressed matrices.
+
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+The field order q is a supplied prime power.
+"""
+from fractions import Fraction
+from math import prod
+from itertools import product
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def injection(q, n, k):
+    if k < 0 or n < k:
+        return 0
+    return prod(q**n - q**i for i in range(k))
+
+
+def gl(q, n):
+    return injection(q, n, n)
+
+
+def gaussian(q, n, k):
+    if k < 0 or k > n:
+        return 0
+    value, rem = divmod(injection(q, n, k), gl(q, k))
+    need(rem == 0, 'integer Gaussian coefficient')
+    return value
+
+
+def joint_nullities(q, d, shifts=2):
+    need(type(q) is int and q >= shifts and type(d) is int and d >= 0 and
+         shifts in (2, 3), 'field order, dimension and distinct shifts')
+    g = [[gaussian(q, n, k) for k in range(n + 1)] for n in range(d + 1)]
+    count = {}
+    # This is the retained incidence inversion from Discussion 5261.
+    for a in product(range(d, -1, -1), repeat=shifts):
+        if sum(a) > d:
+            continue
+        used = 0
+        incidence = q**(d*(d-sum(a)))
+        for size in a:
+            incidence *= g[d-used][size] * q**(used*size)
+            used += size
+        larger = sum(prod(g[e[i]][a[i]] for i in range(shifts)) * value
+                     for e, value in count.items()
+                     if all(e[i] >= a[i] for i in range(shifts)))
+        count[a] = incidence - larger
+        need(count[a] >= 0, 'nonnegative exact stratum')
+    need(sum(count.values()) == q**(d*d), 'all matrices counted')
+    return count
+
+
+def unrestricted(q, r, d, rho):
+    return sum(gaussian(q, d-rho, k-rho) * injection(q, r, k) * q**(d*(r-k))
+               for k in range(rho, min(d, r) + 1))
+
+
+def full_rank(q, r, d, rho):
+    if r < d:
+        return 0
+    return injection(q, r, d) * q**(rho*(r-d)) * injection(q, r-d, d-rho)
+
+
+def fixed_product(q, d, profile, ranks):
+    arbitrary = [unrestricted(q, r, d, rho) for r, rho in zip(profile, ranks)]
+    full = [full_rank(q, r, d, rho) for r, rho in zip(profile[1:], ranks[1:])]
+    return prod(arbitrary), arbitrary[0] * prod(full)
+
+
+def headers(q, d, profile, pivot_class='identity'):
+    need(type(d) is int and d >= 1 and len(profile) == 4 and
+         all(type(r) is int and r >= 0 for r in profile), 'header dimensions')
+    n = sum(profile)
+    need(n >= d, 'pivot fits ambient space')
+    # The caller supplies the equality class of (0, lambda, 2lambda-1).
+    need(pivot_class in ('identity', 'half', 'generic'), 'pivot class')
+    need(pivot_class != 'half' or q % 2 == 1, 'half needs odd characteristic')
+    need(pivot_class != 'generic' or q >= 4, 'generic class must exist')
+    shifts = 3 if pivot_class == 'generic' else 2
+    zero_sector = {'identity': 1, 'half': 0, 'generic': 2}[pivot_class]
+    sharp = common = 0
+    for nullities, multiplicity in joint_nullities(q, d, shifts).items():
+        ranks = (d-nullities[zero_sector], d-nullities[1],
+                 d-nullities[1], d-nullities[0])
+        all_splits, good_splits = fixed_product(q, d, profile, ranks)
+        common += multiplicity * all_splits
+        sharp += multiplicity * good_splits
+    completion = gl(q, n-d)
+    total = gl(q, n)
+    return dict(sharp=sharp*completion, common=common*completion, total=total,
+                sharp_probability=Fraction(sharp*completion, total),
+                conditional_probability=Fraction(sharp, common) if common else None)
diff --git a/research/scalar-pivot-header-counts/verify.py b/research/scalar-pivot-header-counts/verify.py
new file mode 100644
index 0000000000..fcc521a267
--- /dev/null
+++ b/research/scalar-pivot-header-counts/verify.py
@@ -0,0 +1,208 @@
+"""Compare incidence inversion with complete matrix and factor domains.
+
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+from collections import Counter
+import argparse
+import hashlib
+from itertools import product
+import json
+from pathlib import Path
+import sys
+import types
+
+P=Path(__file__).resolve().parent
+ROOT=P.parents[1]
+
+
+def need(ok,message):
+    if not ok:raise ValueError(message)
+
+
+def load(name,path):
+    m=types.ModuleType(name);m.__file__=str(path);sys.modules[name]=m
+    exec(compile(path.read_bytes(),str(path),'exec'),m.__dict__)
+    return m
+
+
+class Field:
+    def __init__(self,q):
+        self.q=q
+        self.poly={4:0b111,8:0b1011}.get(q)
+        self.add=lambda a,b:(a^b) if self.poly else (a+b)%q
+        self.neg=lambda a:a if self.poly else (-a)%q
+        self.inv={a:next(b for b in range(1,q) if self.mul(a,b)==1) for a in range(1,q)}
+    def mul(self,a,b):
+        if not self.poly:return a*b%self.q
+        out=0
+        while b:
+            if b&1:out^=a
+            b>>=1;a<<=1
+            if a&self.q:a^=self.poly
+        return out
+    def rank(self,a):
+        a=[row[:] for row in a]
+        if not a:return 0
+        rank=0
+        for j in range(len(a[0])):
+            k=next((i for i in range(rank,len(a)) if a[i][j]),None)
+            if k is None:continue
+            a[k],a[rank]=a[rank],a[k]
+            inv=self.inv[a[rank][j]];a[rank]=[self.mul(inv,v) for v in a[rank]]
+            for i in range(rank+1,len(a)):
+                c=a[i][j]
+                a[i]=[self.add(x,self.neg(self.mul(c,y))) for x,y in zip(a[i],a[rank])]
+            rank+=1
+            if rank==len(a):break
+        return rank
+    def mm(self,x,y,d):
+        out=[]
+        for row in x:
+            result=[]
+            for j in range(d):
+                value=0
+                for k,a in enumerate(row):value=self.add(value,self.mul(a,y[k][j]))
+                result.append(value)
+            out.append(result)
+        return out
+
+
+def matrices(r,c,q):
+    for v in product(range(q),repeat=r*c):yield [list(v[i*c:(i+1)*c]) for i in range(r)]
+
+
+def fingerprint(value):
+    raw=value.to_bytes(max(1,(value.bit_length()+7)//8),'big')
+    return dict(bits=value.bit_length(),sha256=hashlib.sha256(raw).hexdigest())
+
+
+def inverse(field, a):
+    n=len(a);a=[row[:] + [int(i==j) for j in range(n)] for i,row in enumerate(a)]
+    for j in range(n):
+        k=next(i for i in range(j,n) if a[i][j])
+        a[k],a[j]=a[j],a[k];scale=field.inv[a[j][j]]
+        a[j]=[field.mul(scale,v) for v in a[j]]
+        for i in range(n):
+            if i!=j:
+                c=a[i][j]
+                a[i]=[field.add(x,field.neg(field.mul(c,y))) for x,y in zip(a[i],a[j])]
+    return [row[n:] for row in a]
+
+
+def literal_f4_splits(c):
+    f=Field(4);counts=Counter();checked=0
+    for inclusion in product(range(4),repeat=3):
+        if not any(inclusion):continue
+        for projection in product(range(4),repeat=3):
+            checked+=1
+            def compress(mask):
+                value=0
+                for x,y,m in zip(projection,inclusion,mask):
+                    if m:value=f.add(value,f.mul(x,y))
+                return value
+            if (compress((1,1,1)),compress((1,0,1)),compress((0,1,1)))!=(1,2,2):continue
+            pivot=next(j for j in range(3) if projection[j])
+            kernel=[]
+            for j in range(3):
+                if j!=pivot:
+                    v=[0]*3;v[j]=1;v[pivot]=f.neg(f.mul(projection[j],f.inv[projection[pivot]]));kernel.append(v)
+            header=[list(row) for row in zip(inclusion,*kernel)];inv=inverse(f,header)
+            def schur(mask):
+                p=f.mm(inv,[[f.mul(mask[i],v) for v in header[i]] for i in range(3)],3)
+                need(p[0][0]==2,'literal scalar pivot')
+                return [[f.add(p[i][j],f.neg(f.mul(f.mul(p[i][0],f.inv[2]),p[0][j]))) for j in (1,2)] for i in (1,2)]
+            s=schur((1,0,1));t=schur((0,1,1));st=f.mm(s,t,2);ts=f.mm(t,s,2)
+            counts[f.rank([[f.add(st[i][j],f.neg(ts[i][j])) for j in range(2)] for i in range(2)])]+=1
+    got=c.headers(4,1,(0,1,1,1),'generic')
+    need(checked==4032 and dict(counts)=={2:27},'all F4 literal scalar splits')
+    need(got['sharp']==got['common']==4860 and str(got['sharp_probability'])=='3/112','F4 complete header count')
+    return dict(split_pairs=checked,admissible_splits=27,sharp_headers=4860,total_headers=got['total'],probability='3/112')
+
+
+def scalar_censuses(c):
+    rows=[]
+    for q,d,lam,kind,profile in ((3,2,2,'half',(2,3,3,2)),(5,2,2,'generic',(1,2,2,2)),
+        (5,2,3,'half',(1,2,2,2)),(4,2,2,'generic',(1,2,2,2)),(8,2,2,'generic',(1,2,2,2))):
+        f=Field(q);shift=f.add(f.add(lam,lam),f.neg(1));distinct=[0,lam]
+        if shift not in distinct:distinct.append(shift)
+        observed=Counter();common=sharp=0
+        for h in matrices(d,d,q):
+            ranks=[]
+            for scalar in distinct:
+                ranks.append(f.rank([[f.add(h[i][j],f.neg(scalar if i==j else 0)) for j in range(d)] for i in range(d)]))
+            observed[tuple(d-r for r in ranks)]+=1
+            all_splits,good_splits=c.fixed_product(q,d,profile,(ranks[distinct.index(shift)],ranks[1],ranks[1],ranks[0]))
+            common+=all_splits;sharp+=good_splits
+        need(dict(observed)=={k:v for k,v in c.joint_nullities(q,d,len(distinct)).items() if v},'scalar three-shift census')
+        got=c.headers(q,d,profile,kind);completion=c.gl(q,sum(profile)-d)
+        need((got['common'],got['sharp'])==(common*completion,sharp*completion),'scalar header weights')
+        rows.append(dict(q=q,d=d,scalar=lam,pivot_class=kind,matrices=q**(d*d),common_splits=common,sharp_splits=sharp,sharp_probability=str(got['sharp_probability']),conditional_probability=str(got['conditional_probability'])))
+    fixed=c.fixed_product(5,2,(1,2,2,2),(1,2,2,2))
+    need(fixed==(442368000,442368000),'named F5 Jordan split count')
+    named=c.headers(5,2,(1,2,2,2),'generic')
+    need(named['sharp']==385*480**3*c.gl(5,5),'named F5 full profile count')
+    return rows,dict(fixed_H_sharp_splits=fixed[1],fixed_H_sharp_headers=fixed[1]*c.gl(5,5),full_profile_sharp_splits=385*480**3,full_profile_sharp_headers=named['sharp'],full_profile_common_headers=named['common'],total_headers=named['total'],probability=str(named['sharp_probability']),conditional_probability=str(named['conditional_probability']))
+
+def main():
+    ap=argparse.ArgumentParser();ap.add_argument('--write-result',action='store_true');args=ap.parse_args()
+    for row in json.loads((P/'SOURCES.json').read_text())['files']:
+        if row['usage']=='input':need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'source hash')
+    c=load('counts',P/'counts.py')
+    old=load('binary_source',ROOT/'research/schur-header-count/verify.py')
+    domains=[];total=0
+    for q,d in ((2,1),(2,2),(2,3),(3,1),(3,2),(3,3),(5,1),(5,2),(4,1),(4,2),(8,1),(8,2)):
+        field=Field(q);observed=Counter()
+        for h in matrices(d,d,q):
+            w=[[field.add(int(i==j),field.neg(h[i][j])) for j in range(d)] for i in range(d)]
+            observed[d-field.rank(h),d-field.rank(w)]+=1
+        predicted=c.joint_nullities(q,d)
+        need(dict(observed)=={k:v for k,v in predicted.items() if v},'complete joint-nullity census')
+        domains.append(dict(q=q,d=d,matrices=sum(observed.values()),nonempty_strata=len(observed)))
+        total+=sum(observed.values())
+    factor_pairs=0;factor_targets=0
+    for q,d,r in ((2,1,0),(2,1,1),(2,1,2),(2,2,2),(2,2,3),(3,1,2),(3,2,2),(4,1,2),(4,2,1)):
+        field=Field(q);all_counts=Counter();full_counts=Counter()
+        for x in matrices(d,r,q):
+            for y in matrices(r,d,q):
+                a=field.mm(x,y,d);key=tuple(map(tuple,a));all_counts[key]+=1;factor_pairs+=1
+                if field.rank(x)==d and field.rank(y)==d:full_counts[key]+=1
+        for a in matrices(d,d,q):
+            key=tuple(map(tuple,a));rho=field.rank(a)
+            need(all_counts[key]==c.unrestricted(q,r,d,rho),'unrestricted factor count')
+            need(full_counts[key]==c.full_rank(q,r,d,rho),'full factor count')
+            factor_targets+=1
+    comparisons=[]
+    for d,profile in ((1,(1,1,1,2)),(1,(0,2,2,1)),(2,(2,2,2,2)),(2,(1,3,3,2)),(3,(3,3,3,4))):
+        got=c.headers(2,d,profile);want=old.predict(profile,d)
+        need((got['sharp'],got['common'],got['total'])==(want['sharp_headers'],want['identity_headers'],want['total_headers']),'retained binary header law')
+        comparisons.append(dict(d=d,profile=list(profile),sharp_probability=str(got['sharp_probability']),conditional_probability=str(got['conditional_probability'])))
+    # Literal full headers use the predecessor's independent bit-matrix oracle.
+    profile=(1,1,1,1);common=sharp=0
+    for h in old.gl_headers(4):
+        rank=old.inspect_header(h,profile,1)
+        common+=rank is not None;sharp+=rank==2
+    got=c.headers(2,1,profile)
+    need((common,sharp)==(got['common'],got['sharp']),'all GL4 literal headers')
+    large=[]
+    for q,d in ((2,32),(4,16)):
+        law=c.joint_nullities(q,d)
+        need(law[d,0]==law[0,d]==1 and all(law[a,b]==law[b,a] for a,b in law),'large symmetry and unique endpoints')
+        result=c.headers(q,d,(d,d,d,d))
+        need(0<=result['sharp']<=result['common']<=result['total'],'large containment')
+        large.append(dict(q=q,d=d,strata=len(law),matrix_space_bits=(q**(d*d)).bit_length(),sharp=fingerprint(result['sharp']),common=fingerprint(result['common']),total=fingerprint(result['total'])))
+    need(c.joint_nullities(2,1).get((1,1),0)==0,'zero and one eigenspaces disjoint')
+    need(c.headers(2,1,(1,0,0,0))['conditional_probability'] is None,'empty event has no conditional probability')
+    need(c.headers(3,1,(1,1,1,1))['sharp']==16*c.gl(3,3),'odd-field scalar H2 count')
+    need(c.headers(2,1,(0,2,2,1))['sharp']==181440,'unrestricted00 boundary')
+    scalar_rows,named=scalar_censuses(c)
+    literal_scalar=literal_f4_splits(c)
+    generic=c.headers(4,12,(12,12,12,12),'generic')
+    need(0<generic['sharp']<=generic['common']<=generic['total'],'large generic containment')
+    generic_large=dict(q=4,d=12,strata=len(c.joint_nullities(4,12,3)),sharp=fingerprint(generic['sharp']),common=fingerprint(generic['common']),total=fingerprint(generic['total']))
+    result=dict(status='PASS_SCALAR_PIVOT_HEADER_COUNTS',scalar_censuses=scalar_rows,named_F5=named,literal_F4=literal_scalar,generic_large=generic_large,domains=domains,matrices=total,factor_pairs=factor_pairs,factor_targets=factor_targets,binary_comparisons=comparisons,literal_headers=c.gl(2,4),large=large,controls=4,counts_sha256=hashlib.sha256((P/'counts.py').read_bytes()).hexdigest())
+    if args.write_result:(P/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n')
+    else:need(json.dumps(result,sort_keys=True)==json.dumps(json.loads((P/'RESULT.json').read_text()),sort_keys=True),'typed complete receipt')
+    print(json.dumps({k:result[k] for k in ('status','matrices','factor_pairs','factor_targets','literal_headers','controls')}))
+
+
+if __name__=='__main__':main()