diff --git a/research/nine-axis-cutoff-sharpness/PROOF.md b/research/nine-axis-cutoff-sharpness/PROOF.md
new file mode 100644
index 0000000000..1ba92a64c5
--- /dev/null
+++ b/research/nine-axis-cutoff-sharpness/PROOF.md
@@ -0,0 +1,205 @@
+# The nine-axis window is sharp
+
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+
+## 1. The theorem
+
+Retain the input-phase grammar of PR5369 and PR5529 on X=F2^n:
+
+    U(g,q)e_x = i^q(x) e_(g x),
+    q(x) = c + sum_j a_j x_j + 2 sum_(j<k) b_jk x_j x_k modulo 4,
+
+where g is affine invertible, c and a_j are modulo four, and b_jk are
+modulo two. Let G be this finite monomial group. Work over Q(i) or C.
+Let rho_f evaluate each group element at its f-th tensor power; external
+coefficients stay fixed. Let z=[iI] and I_r=(z-i^r[1]).
+
+For every n>=5 with n=1 modulo four, put F=2n+3 and
+
+    L_r = F + ((r-F) modulo 4).
+
+Then, for every positive f congruent to r modulo four,
+
+    ker rho_f = I_r  if and only if  f >= L_r.
+
+For n=9, F=21 and (L_0,L_1,L_2,L_3)=(24,21,22,23).
+Thus 21,22,23,24 is a sharp four-width test window. Four residue tests
+are necessary, and no complete test set can have maximum width below 24.
+The corresponding statement for general n has maximum width at least 2n+6.
+
+The upper bound is the retained PR5529 theorem. The new part is a general
+lower residual from a code obstruction and a cuspidal character. No
+physical cost, supplier, efficient expansion or kappa improvement follows.
+This result concerns the complete fixed endpoint grammar, including all
+independent inputs and every specified return.
+
+## 2. The zero-phase tuple must be longer than 2n+2
+
+A tuple x_1,...,x_f has zero nonconstant phase character exactly when
+
+    sum_t x_tj = 0 modulo 4,
+    sum_t x_tj x_tk = 0 modulo 2 for j<k.
+
+Its n binary row words generate a doubly even code C: every codeword has
+weight divisible by four. The row words have zero pairwise dot products,
+and wt(u+v)=wt(u)+wt(v)-2|supp(u) intersect supp(v)| proves this assertion
+for their whole span. Full affine span of the tuple is equivalent to both
+rank(C)=n and the all-one word being outside C. A nonzero linear functional
+constant on every tuple point is exactly a row relation or the all-one word.
+
+Suppose f<=N=2n+2. Append zero columns to reach length N. This preserves the
+phase conditions and full affine span. Since n=1 modulo four, N=4 modulo
+eight. The all-one word 1_N has weight divisible by four and is orthogonal
+to C. It is not in C. Therefore C+<1_N> is doubly even, self-orthogonal,
+and has dimension n+1=N/2. It is self-dual.
+
+Here is the required elementary obstruction. If a doubly even code D is
+self-dual at length N, sum i^wt(x) over F2^N. On the one hand it equals
+(1+i)^N. On a coset x+D, it equals
+
+    i^wt(x) sum_(d in D) (-1)^(x.d).
+
+This sum is zero unless x belongs to D-perp=D. The only contributing coset
+is D, and its sum is |D|=2^(N/2). Thus (1+i)^N=2^(N/2), which requires
+N divisible by eight. This contradicts N=4 modulo eight. Consequently no
+zero-phase tuple of length at most 2n+2 has full affine span.
+
+This is a classical doubly-even code argument. Missing full affine span
+alone is not a representation-kernel lower bound. Section 3 supplies that
+additional step.
+
+## 3. A nonzero integer affine cancellation element
+
+We use the following established part of Green's character theory. A
+regular multiplicative character theta of F_(2^n)^* gives a genuine
+irreducible complex character chi_theta of GL(n,2). Frobenius orbits give
+the same representation. Its degree is
+
+    d_n = product_(j=1)^(n-1) (2^j-1),
+
+and its value at a transvection is -d_n/(2^(n-1)-1). These facts follow
+from the identity and unipotent cases of Green's formula. See J. A. Green,
+[The characters of the finite general linear groups](https://doi.org/10.1090/S0002-9947-1955-0072878-2),
+Trans. AMS 80 (1955), 402-447, and the explicit statement in Dipendra
+Prasad, [The Space of Degenerate Whittaker Models for General Linear Groups over a Finite Field](https://www.math.iitb.ac.in/~dprasad/imrn.pdf),
+IMRN 2000 no. 11, Section 2, pages 581-582, Theorem 2.
+
+Take all primitive characters theta of order 2^n-1, one representative
+per Frobenius orbit, and sum their chi_theta. Call the resulting genuine
+character Psi. Each orbit has length n: a smaller positive power 2^j
+cannot equal one modulo 2^n-1. There are phi(2^n-1)/n such orbits. Green's
+formula places their values in the corresponding cyclotomic field, and
+Galois automorphisms permute this set. Hence Psi is rational valued.
+Character values are algebraic integers, so Psi is integer valued.
+Its degree Psi(1) is positive.
+
+Let H be the pointwise stabilizer of a linear hyperplane. Over F2 its
+size is 2^(n-1); every nonidentity element is a transvection. Thus
+
+    sum_(h in H) Psi(h) = Psi(1) + (2^(n-1)-1) Psi(transvection) = 0.
+
+For a representation with character Psi, the average of its H matrices
+is the projection onto its H-fixed space. Its trace is zero, so this
+projection is zero. Therefore, for every g,
+
+    sum_(h in gH) Psi(h^-1) = 0.                         (1)
+
+This argument converts two character values into all coset identities;
+it does not assume that a zero character sum on H alone gives (1) for an
+arbitrary class function. The genuine-representation condition is needed.
+
+Define an element of the affine group algebra by
+
+    A_n = sum_(t in F2^n) sum_(g in GL(n,2)) Psi(g^-1) [x -> gx+t].
+
+The pointwise stabilizer of any affine hyperplane is a translation
+conjugate of H. Its linear parts give the same hyperplane stabilizer in
+GL(n,2), up to linear conjugation. Thus (1) gives zero coefficient sum
+on every coset of every affine-hyperplane pointwise stabilizer.
+
+If a tuple lies in a proper affine subspace, choose an affine hyperplane
+that contains it. For any possible output tuple, the affine maps that
+produce it form a coset of the tuple stabilizer. That coset is a union
+of cosets of the hyperplane pointwise stabilizer. Therefore
+
+    rho_f(A_n)e_tuple = 0                               (2)
+
+for every such tuple. The coefficient of the identity affine map in A_n
+is Psi(1)>0, so A_n is nonzero.
+
+At n=9, d_n=19923090075 and phi(511)/9=48. Thus Psi(1)=956308323600 and
+Psi(transvection)=-3750228720. Their stabilizer sum is zero because H has
+255 nonidentity elements. No GL(9,2) enumeration is needed for this proof.
+The verifier checks every hyperplane coset in GL(3,2) and GL(4,2) using
+explicit instances of this integer character. These finite checks
+corroborate the formula; they do not replace Green's theorem.
+
+## 4. Fixed residuals and their first visible widths
+
+Let D be the diagonal phase subgroup. For each residue r, put
+
+    E_r = (1/|D|) sum_(c,a,b) i^(-r*c) [D_q],
+    P_r = A_n E_r.
+
+Finite Fourier orthogonality says that rho_f(E_r) is the projector onto
+zero nonconstant phase tuples when f=r modulo four, and is zero at every
+other residue. Sections 2 and 3 show that rho_f(P_r)=0 at each positive
+matching width f<L_r. It also vanishes at every wrong residue. Thus one
+fixed residual P_r vanishes at every positive width below L_r.
+
+Write n=4k+1. Use k disjoint copies of the length-eight code with row basis
+
+    11111111, 10101010, 11001100, 11110000,
+
+then one row 1111 on four new coordinates and one final zero coordinate.
+The n independent rows have length 8k+5=2n+3. All weights are divisible
+by four and all pairwise dot products are even. Their columns form a
+zero-phase tuple. The zero column and row rank n give full affine span.
+Append zero points to reach L_r; this preserves the nonconstant character.
+
+Only the identity affine map fixes this full-span tuple. Its diagonal
+entry under rho_(L_r)(P_r) is exactly Psi(1)>0. Therefore P_r is nonzero
+and is outside I_r. Its coefficients lie in Q(i), since Psi is integer
+valued. This proves the lower kernel statement over Q(i) as well as C.
+
+## 5. Upper bound and completeness of test sets
+
+The pinned PR5529 argument realizes every nonconstant phase character at
+every f>=2n+3 by a tuple with full affine span. It starts with zero and an
+adapted binary basis, factors the nonalternating residual Gram form in at
+most n columns, corrects the linear phase with two equal points, then pads
+with zeros. Finite Fourier separation then gives ker rho_f=I_(f modulo 4).
+Its original proof and constructor remain unchanged inputs to this package.
+
+For a fixed residue r, the first width at least 2n+3 is L_r. The upper
+bound and Section 4 give the claimed equivalence. The four central ideals
+have zero intersection. Hence any test set containing one matching width
+at or above each L_r decides all positive widths. Conversely, if a test
+set lacks such a width in residue r, the nonzero P_r vanishes on every
+one of its tests and fails at L_r. This also proves necessity for infinite
+test sets, and gives the sharp maximum-width claim.
+
+## Evidence and limits
+
+The written argument proves the unbounded dimension family. Finite replay
+checks the explicit code tuples through 129 axes, all four residue pads,
+the exact Gauss-sum contradiction, 38094 small-group cosets, 512 outputs
+of the retained upper constructor and four controls. Source files are
+hashed before the retained constructor is loaded.
+
+Green's character theorem and the complete PR5529 upper proof are cited
+mathematical inputs. They are not proof-kernel checked in this package.
+The GL(9,2) residual is defined by a finite formula and is not expanded.
+No enumeration of all nine-axis phase characters is claimed. The proof
+excludes Hadamards, width-dependent external coefficients, changing
+program families and undeclared aliases. It supplies no physical caller,
+precision, compiler, stock, movement or outer-transfer result.
+
+Joseph Anglada's PR5542 gives the three-axis code/coset argument. Ali
+Romman's PR5622 gives the four-axis affine version. Hiroki KUMAZAKI's
+PR5522 and Mihir Srivastava's PR5521 supply the earlier sharpness/audit
+line. PR5369 and PR5529 supply the grammar, upper bound and Fourier
+interface. The new contribution is the cuspidal affine residual and its
+use with the code obstruction to settle the nine-axis case and the whole
+n=1 modulo four family. The classical code and character theorems are not
+new claims. Retain Jose Manuel, ywz65, Chris R and the native source lineage.
diff --git a/research/nine-axis-cutoff-sharpness/README.md b/research/nine-axis-cutoff-sharpness/README.md
new file mode 100644
index 0000000000..5da1243757
--- /dev/null
+++ b/research/nine-axis-cutoff-sharpness/README.md
@@ -0,0 +1,35 @@
+# Sharp nine-axis native test window 21–24
+
+The fixed affine-quadratic monomial grammar has sharp nine-axis tensor
+cutoff 21 and residue thresholds (24,21,22,23). The same proof gives sharp
+cutoff 2n+3 for every n>=5 with n=1 modulo four. Four matching residue tests
+are necessary. PROOF.md contains the complete argument and citations.
+No physical paid profile or kappa changes.
+
+A doubly-even code obstruction rules out short zero-phase full-span tuples.
+A genuine cuspidal character gives an affine cancellation element, which
+turns that absence into a nonzero representation-kernel witness. Explicit
+E8 code blocks give the first visible tuple. This closes the distinction
+between a character-realization bound and representation sharpness.
+
+Run `python3 -B scripts/research_package.py --package research/nine-axis-cutoff-sharpness`.
+Python 3.12 and the standard library suffice. RESULT.json records exact
+code, Gauss-sum, coset, constructor and corruption controls.
+
+## Sources and credit
+
+SOURCES.json pins PR5529's upper proof and constructor and Joseph Anglada's
+PR5542 three-axis proof. PROOF.md cites Green's character theorem and its
+explicit formulation in Prasad's published paper. Credit PR5369, PR5522,
+PR5521, PR5622 and the retained native/phase contributors. The code and
+character theory are classical; this application and proof are the new work.
+
+## Open next questions
+
+Other axis-count residues need separate sharpness arguments. An efficient
+way to apply the cutoff to large straight-line programs is still needed;
+this proof does not expand GL(9,2) or the diagonal phase group. Actual
+native callers need exact source bindings, all returned fields and a full
+paid bill. No human or formal-kernel acceptance is claimed.
+
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
diff --git a/research/nine-axis-cutoff-sharpness/RESULT.json b/research/nine-axis-cutoff-sharpness/RESULT.json
new file mode 100644
index 0000000000..5168d1b9d8
--- /dev/null
+++ b/research/nine-axis-cutoff-sharpness/RESULT.json
@@ -0,0 +1,462 @@
+{
+  "limits": [
+    "Green character theory is a cited theorem, not kernel-checked or enumerated at n=9.",
+    "The general upper proof is retained from PR5529; finite controls do not prove it.",
+    "No physical supplier, efficient group-algebra expansion or kappa improvement."
+  ],
+  "nine_axis": {
+    "cutoff": 21,
+    "integer_character_identity": 956308323600,
+    "integer_character_transvection": -3750228720,
+    "irreducible_degree": 19923090075,
+    "primitive_cuspidal_count": 48,
+    "thresholds": [
+      24,
+      21,
+      22,
+      23
+    ]
+  },
+  "rejection_controls": 4,
+  "scope": "n=1 mod 4, n>=5; fixed affine-quadratic input-phase grammar",
+  "small_group_controls": [
+    {
+      "character_norm": 2,
+      "coefficient_counts": {
+        "-1": 48,
+        "-2": 21,
+        "0": 56,
+        "2": 42,
+        "6": 1
+      },
+      "cosets": 294,
+      "dimension": 3,
+      "group_order": 168
+    },
+    {
+      "character_norm": 2,
+      "coefficient_counts": {
+        "-1": 2688,
+        "-2": 2520,
+        "-6": 217,
+        "0": 10240,
+        "2": 4494,
+        "42": 1
+      },
+      "cosets": 37800,
+      "dimension": 4,
+      "group_order": 20160
+    }
+  ],
+  "status": "PASS_NINE_AXIS_CUTOFF_SHARPNESS",
+  "upper_witness_controls": 512,
+  "witnesses": [
+    {
+      "axes": 5,
+      "cutoff": 13,
+      "forbidden_self_dual_length": 12,
+      "gauss_sum": -64,
+      "thresholds": [
+        16,
+        13,
+        14,
+        15
+      ]
+    },
+    {
+      "axes": 9,
+      "cutoff": 21,
+      "forbidden_self_dual_length": 20,
+      "gauss_sum": -1024,
+      "shortest_points": [
+        1,
+        3,
+        5,
+        7,
+        9,
+        11,
+        13,
+        15,
+        16,
+        48,
+        80,
+        112,
+        144,
+        176,
+        208,
+        240,
+        256,
+        256,
+        256,
+        256,
+        0
+      ],
+      "thresholds": [
+        24,
+        21,
+        22,
+        23
+      ]
+    },
+    {
+      "axes": 13,
+      "cutoff": 29,
+      "forbidden_self_dual_length": 28,
+      "gauss_sum": -16384,
+      "thresholds": [
+        32,
+        29,
+        30,
+        31
+      ]
+    },
+    {
+      "axes": 17,
+      "cutoff": 37,
+      "forbidden_self_dual_length": 36,
+      "gauss_sum": -262144,
+      "thresholds": [
+        40,
+        37,
+        38,
+        39
+      ]
+    },
+    {
+      "axes": 21,
+      "cutoff": 45,
+      "forbidden_self_dual_length": 44,
+      "gauss_sum": -4194304,
+      "thresholds": [
+        48,
+        45,
+        46,
+        47
+      ]
+    },
+    {
+      "axes": 25,
+      "cutoff": 53,
+      "forbidden_self_dual_length": 52,
+      "gauss_sum": -67108864,
+      "thresholds": [
+        56,
+        53,
+        54,
+        55
+      ]
+    },
+    {
+      "axes": 29,
+      "cutoff": 61,
+      "forbidden_self_dual_length": 60,
+      "gauss_sum": -1073741824,
+      "thresholds": [
+        64,
+        61,
+        62,
+        63
+      ]
+    },
+    {
+      "axes": 33,
+      "cutoff": 69,
+      "forbidden_self_dual_length": 68,
+      "gauss_sum": -17179869184,
+      "thresholds": [
+        72,
+        69,
+        70,
+        71
+      ]
+    },
+    {
+      "axes": 37,
+      "cutoff": 77,
+      "forbidden_self_dual_length": 76,
+      "gauss_sum": -274877906944,
+      "thresholds": [
+        80,
+        77,
+        78,
+        79
+      ]
+    },
+    {
+      "axes": 41,
+      "cutoff": 85,
+      "forbidden_self_dual_length": 84,
+      "gauss_sum": -4398046511104,
+      "thresholds": [
+        88,
+        85,
+        86,
+        87
+      ]
+    },
+    {
+      "axes": 45,
+      "cutoff": 93,
+      "forbidden_self_dual_length": 92,
+      "gauss_sum": -70368744177664,
+      "thresholds": [
+        96,
+        93,
+        94,
+        95
+      ]
+    },
+    {
+      "axes": 49,
+      "cutoff": 101,
+      "forbidden_self_dual_length": 100,
+      "gauss_sum": -1125899906842624,
+      "thresholds": [
+        104,
+        101,
+        102,
+        103
+      ]
+    },
+    {
+      "axes": 53,
+      "cutoff": 109,
+      "forbidden_self_dual_length": 108,
+      "gauss_sum": -18014398509481984,
+      "thresholds": [
+        112,
+        109,
+        110,
+        111
+      ]
+    },
+    {
+      "axes": 57,
+      "cutoff": 117,
+      "forbidden_self_dual_length": 116,
+      "gauss_sum": -288230376151711744,
+      "thresholds": [
+        120,
+        117,
+        118,
+        119
+      ]
+    },
+    {
+      "axes": 61,
+      "cutoff": 125,
+      "forbidden_self_dual_length": 124,
+      "gauss_sum": -4611686018427387904,
+      "thresholds": [
+        128,
+        125,
+        126,
+        127
+      ]
+    },
+    {
+      "axes": 65,
+      "cutoff": 133,
+      "forbidden_self_dual_length": 132,
+      "gauss_sum": -73786976294838206464,
+      "thresholds": [
+        136,
+        133,
+        134,
+        135
+      ]
+    },
+    {
+      "axes": 69,
+      "cutoff": 141,
+      "forbidden_self_dual_length": 140,
+      "gauss_sum": -1180591620717411303424,
+      "thresholds": [
+        144,
+        141,
+        142,
+        143
+      ]
+    },
+    {
+      "axes": 73,
+      "cutoff": 149,
+      "forbidden_self_dual_length": 148,
+      "gauss_sum": -18889465931478580854784,
+      "thresholds": [
+        152,
+        149,
+        150,
+        151
+      ]
+    },
+    {
+      "axes": 77,
+      "cutoff": 157,
+      "forbidden_self_dual_length": 156,
+      "gauss_sum": -302231454903657293676544,
+      "thresholds": [
+        160,
+        157,
+        158,
+        159
+      ]
+    },
+    {
+      "axes": 81,
+      "cutoff": 165,
+      "forbidden_self_dual_length": 164,
+      "gauss_sum": -4835703278458516698824704,
+      "thresholds": [
+        168,
+        165,
+        166,
+        167
+      ]
+    },
+    {
+      "axes": 85,
+      "cutoff": 173,
+      "forbidden_self_dual_length": 172,
+      "gauss_sum": -77371252455336267181195264,
+      "thresholds": [
+        176,
+        173,
+        174,
+        175
+      ]
+    },
+    {
+      "axes": 89,
+      "cutoff": 181,
+      "forbidden_self_dual_length": 180,
+      "gauss_sum": -1237940039285380274899124224,
+      "thresholds": [
+        184,
+        181,
+        182,
+        183
+      ]
+    },
+    {
+      "axes": 93,
+      "cutoff": 189,
+      "forbidden_self_dual_length": 188,
+      "gauss_sum": -19807040628566084398385987584,
+      "thresholds": [
+        192,
+        189,
+        190,
+        191
+      ]
+    },
+    {
+      "axes": 97,
+      "cutoff": 197,
+      "forbidden_self_dual_length": 196,
+      "gauss_sum": -316912650057057350374175801344,
+      "thresholds": [
+        200,
+        197,
+        198,
+        199
+      ]
+    },
+    {
+      "axes": 101,
+      "cutoff": 205,
+      "forbidden_self_dual_length": 204,
+      "gauss_sum": -5070602400912917605986812821504,
+      "thresholds": [
+        208,
+        205,
+        206,
+        207
+      ]
+    },
+    {
+      "axes": 105,
+      "cutoff": 213,
+      "forbidden_self_dual_length": 212,
+      "gauss_sum": -81129638414606681695789005144064,
+      "thresholds": [
+        216,
+        213,
+        214,
+        215
+      ]
+    },
+    {
+      "axes": 109,
+      "cutoff": 221,
+      "forbidden_self_dual_length": 220,
+      "gauss_sum": -1298074214633706907132624082305024,
+      "thresholds": [
+        224,
+        221,
+        222,
+        223
+      ]
+    },
+    {
+      "axes": 113,
+      "cutoff": 229,
+      "forbidden_self_dual_length": 228,
+      "gauss_sum": -20769187434139310514121985316880384,
+      "thresholds": [
+        232,
+        229,
+        230,
+        231
+      ]
+    },
+    {
+      "axes": 117,
+      "cutoff": 237,
+      "forbidden_self_dual_length": 236,
+      "gauss_sum": -332306998946228968225951765070086144,
+      "thresholds": [
+        240,
+        237,
+        238,
+        239
+      ]
+    },
+    {
+      "axes": 121,
+      "cutoff": 245,
+      "forbidden_self_dual_length": 244,
+      "gauss_sum": -5316911983139663491615228241121378304,
+      "thresholds": [
+        248,
+        245,
+        246,
+        247
+      ]
+    },
+    {
+      "axes": 125,
+      "cutoff": 253,
+      "forbidden_self_dual_length": 252,
+      "gauss_sum": -85070591730234615865843651857942052864,
+      "thresholds": [
+        256,
+        253,
+        254,
+        255
+      ]
+    },
+    {
+      "axes": 129,
+      "cutoff": 261,
+      "forbidden_self_dual_length": 260,
+      "gauss_sum": -1361129467683753853853498429727072845824,
+      "thresholds": [
+        264,
+        261,
+        262,
+        263
+      ]
+    }
+  ]
+}
diff --git a/research/nine-axis-cutoff-sharpness/SOURCES.json b/research/nine-axis-cutoff-sharpness/SOURCES.json
new file mode 100644
index 0000000000..ef63308a11
--- /dev/null
+++ b/research/nine-axis-cutoff-sharpness/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/shorter-native-phase-witness/README.md",
+      "usage": "input",
+      "git_blob": "5b68f6be4a297f6ccc1ac1631f40d310ff2236b4",
+      "sha256": "abc1224cb79a7056d476636522100a375dbe7d51f2e9a985e667d0d7729f3212"
+    },
+    {
+      "path": "research/shorter-native-phase-witness/verify.py",
+      "usage": "input",
+      "git_blob": "e192625ff95c7181fa1a4da405c2aa55360528af",
+      "sha256": "1a3053f3b9268679adc413a3383f238c7b3dd8667dc792aa308e3047c2a8ba73"
+    },
+    {
+      "path": "research/three-axis-sharp-cutoff/PROOF.md",
+      "usage": "input",
+      "git_blob": "ef0be5ce6b06cecbd3e414a492eda35fca673dee",
+      "sha256": "6aeeb430e589e34481ea1e867bd99334e6094a5c59b252ce9b87fcce3cffe217"
+    }
+  ]
+}
diff --git a/research/nine-axis-cutoff-sharpness/TASK.json b/research/nine-axis-cutoff-sharpness/TASK.json
new file mode 100644
index 0000000000..bc5c6fd7c3
--- /dev/null
+++ b/research/nine-axis-cutoff-sharpness/TASK.json
@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63",
+  "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": "Prove the sharp nine-axis native cutoff and the unbounded n=1 modulo four family.",
+  "scope_change_reason": "Resolve the released sharpness question for the actual nine-axis monomial grammar, using a representation-kernel residual rather than only a tuple bound.",
+  "bottleneck_link": "Determine the exact finite tensor widths required to certify fixed native endpoints that can support changed kappa suppliers.",
+  "budget_minutes": 75,
+  "stop_rule": "Construct a nonzero lower residual and match the retained upper theorem, with explicit source assumptions and exact controls.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and RESULT.json",
+  "author": "Ali Romman with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance for derivation, classical-source verification, code and publication.",
+  "open_questions": [
+    {
+      "question": "What are the sharp cutoffs in the remaining axis-count residues?",
+      "why_it_matters": "The general upper theorem can still be loose in those families.",
+      "first_step": "Analyze the zero-phase code obstruction and other phase sectors before a larger enumeration.",
+      "blocked_by": "The present code contradiction uses n=1 modulo four."
+    }
+  ]
+}
diff --git a/research/nine-axis-cutoff-sharpness/VERIFY.json b/research/nine-axis-cutoff-sharpness/VERIFY.json
new file mode 100644
index 0000000000..866b809738
--- /dev/null
+++ b/research/nine-axis-cutoff-sharpness/VERIFY.json
@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/shorter-native-phase-witness/README.md",
+    "research/shorter-native-phase-witness/verify.py",
+    "research/three-axis-sharp-cutoff/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Code tuples through 129 axes, exact Gauss sums, all GL3/GL4 hyperplane cosets, retained upper witnesses and four controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Code tuples through 129 axes, exact Gauss sums, all GL3/GL4 hyperplane cosets, retained upper witnesses and four controls."
+    }
+  ]
+}
diff --git a/research/nine-axis-cutoff-sharpness/verify.py b/research/nine-axis-cutoff-sharpness/verify.py
new file mode 100644
index 0000000000..9e85aef4e6
--- /dev/null
+++ b/research/nine-axis-cutoff-sharpness/verify.py
@@ -0,0 +1,163 @@
+#!/usr/bin/env python3
+"""Check code witnesses, affine coset sums and the retained upper construction.
+
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+from collections import Counter, defaultdict
+import hashlib
+from itertools import combinations
+import json
+from math import comb, prod, gcd
+from pathlib import Path
+import random
+import runpy
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def need(c, message):
+    if not c: raise ValueError(message)
+
+
+def rank(vectors):
+    pivots = {}
+    for value in vectors:
+        while value:
+            k = value.bit_length()-1
+            if k not in pivots:
+                pivots[k] = value; break
+            value ^= pivots[k]
+    return len(pivots)
+
+
+def code_rows(n):
+    need(n >= 5 and n % 4 == 1, 'axis family')
+    rows = []
+    for block in range((n-1)//4):
+        rows.extend(x << (8*block) for x in [255,170,204,240])
+    rows.append(15 << (2*n-2))
+    return rows, 2*n+3
+
+
+def points_from_rows(rows, length):
+    return [sum(((r >> j) & 1) << i for i,r in enumerate(rows)) for j in range(length)]
+
+
+def check_tuple(points, n, residue):
+    need(len(points) % 4 == residue, 'constant character')
+    need(rank(x ^ points[0] for x in points) == n, 'full affine span')
+    rows = [sum(((x >> i) & 1) << j for j,x in enumerate(points)) for i in range(n)]
+    need(all(r.bit_count() % 4 == 0 for r in rows), 'linear phase character')
+    need(all((x & y).bit_count() % 2 == 0 for x,y in combinations(rows,2)), 'quadratic phase character')
+
+
+def gl(n):
+    def extend(columns, span):
+        if len(columns) == n:
+            table = [0]*(1 << n)
+            for x in range(1,1 << n):
+                bit = x & -x; table[x] = table[x ^ bit] ^ columns[bit.bit_length()-1]
+            yield tuple(table); return
+        for x in range(1,1 << n):
+            if x not in span:
+                yield from extend(columns+[x],span | {x ^ y for y in span})
+    return list(extend([], {0}))
+
+
+def character(g, n):
+    identity = tuple(range(1 << n)); power = g; order = 1
+    while power != identity:
+        power = tuple(g[x] for x in power); order += 1
+        need(order <= (1 << n), 'group order control')
+    r = rank(g[1 << j] ^ (1 << j) for j in range(n))
+    if n == 3: return {1:6,2:-2,3:0,4:2,7:-1}[order]
+    if order == 1: return 42
+    if order == 2: return -6 if r == 1 else 2
+    if order == 4: return 2 if r == 2 else -2
+    if order == 3: return -6 if r == 4 else 0
+    if order == 6: return 2 if r == 4 else 0
+    if order == 5: return 2
+    if order == 7: return 0
+    if order == 15: return -1
+    raise ValueError('unclassified element')
+
+
+def coset_checks(n):
+    group = gl(n); weights = [character(g,n) for g in group]
+    need(sum(x*x for x in weights) % len(group) == 0, 'character norm')
+    count = 0
+    for normal in range(1,1 << n):
+        basis = []
+        for x in range(1,1 << n):
+            if not (x & normal).bit_count() % 2 and rank(basis+[x]) > len(basis): basis.append(x)
+        need(len(basis) == n-1, 'hyperplane')
+        sums = defaultdict(int)
+        for g,w in zip(group,weights): sums[tuple(g[x] for x in basis)] += w
+        need(set(sums.values()) == {0}, 'every hyperplane coset sum')
+        count += len(sums)
+    need(any(weights) and sum(weights) == 0, 'nonzero cancellation character')
+    # An identity coefficient corruption leaves a nonzero coset sum.
+    normal = 1; basis = [1 << j for j in range(1,n)]
+    bad = defaultdict(int)
+    for g,w in zip(group,weights): bad[tuple(g[x] for x in basis)] += w+int(g == tuple(range(1 << n)))
+    need(any(bad.values()), 'character corruption detected')
+    return {'dimension':n,'group_order':len(group),'cosets':count,'coefficient_counts':dict(Counter(weights)),'character_norm':sum(x*x for x in weights)//len(group)}
+
+
+def run():
+    pins = json.loads((HERE/'SOURCES.json').read_text())['files']
+    for s in pins:
+        if s['usage'] == 'input': need(hashlib.sha256((ROOT/s['path']).read_bytes()).hexdigest() == s['sha256'],'source bytes')
+    witnesses = []
+    for n in range(5,130,4):
+        rows,length = code_rows(n)
+        need(rank(rows) == n and rank(rows+[(1 << length)-1]) == n+1, 'code and affine ranks')
+        base = points_from_rows(rows,length)
+        record = {'axes':n,'cutoff':length,'thresholds':[length+(r-length)%4 for r in range(4)]}
+        for r in range(4): check_tuple(base+[0]*((r-length)%4),n,r)
+        if n == 9: record['shortest_points'] = base
+        # Direct binomial Gauss sum at the forbidden self-dual length.
+        N = 2*n+2
+        real = sum((-1)**(j//2)*comb(N,j) for j in range(0,N+1,2))
+        imag = sum((-1)**((j-1)//2)*comb(N,j) for j in range(1,N+1,2))
+        need((real,imag) == (-(1 << (N//2)),0), 'length-four-mod-eight Gauss contradiction')
+        record['forbidden_self_dual_length'] = N
+        record['gauss_sum'] = real
+        witnesses.append(record)
+    row8 = [255,170,204,240]
+    words = [0]
+    for r in row8: words += [r ^ x for x in words]
+    need(len(set(words)) == 16 and all(x.bit_count()%4 == 0 for x in words), 'E8 code control')
+    need(sum((-1)**(j//2)*comb(8,j) for j in range(0,9,2)) == 16, 'length-eight positive Gauss control')
+    smallest,_ = code_rows(5)
+    short = points_from_rows(smallest,12)
+    need(rank(x ^ short[0] for x in short) == 4, 'deleted zero loses affine span')
+    bad = points_from_rows(*code_rows(9));bad[0] ^= 1
+    try: check_tuple(bad,9,len(bad)%4)
+    except ValueError: pass
+    else: raise ValueError('phase mutation accepted')
+    groups = [coset_checks(3),coset_checks(4)]
+    upper = runpy.run_path(str(ROOT/'research/shorter-native-phase-witness/verify.py'))
+    rng = random.Random(562233); cases = 0
+    for n in [5,9,13,17,21,25,29,33]:
+        for _ in range(64):
+            u = tuple(rng.randrange(4) for j in range(n));v = tuple(rng.randrange(2) for j in range(n*(n-1)//2));f = 2*n+3+rng.randrange(4)
+            pts = upper['witness'](n,u,v,f)
+            rows = [sum(((x >> i)&1) << j for j,x in enumerate(pts)) for i in range(n)]
+            need(len(pts) == f and rank(x ^ pts[0] for x in pts) == n, 'upper affine witness')
+            need(tuple(x.bit_count()%4 for x in rows) == u, 'upper linear statistics')
+            need(tuple((rows[i]&rows[j]).bit_count()%2 for i,j in combinations(range(n),2)) == v, 'upper quadratic statistics')
+            cases += 1
+    n = 9; N = (1 << n)-1; phi = sum(gcd(k,N) == 1 for k in range(N)); copies = phi//n
+    degree = prod((1 << j)-1 for j in range(1,n));transvection = -degree//((1 << (n-1))-1)
+    need(phi % n == 0 and copies*degree+((1 << (n-1))-1)*copies*transvection == 0, 'cuspidal fixed-space dimension')
+    return {'status':'PASS_NINE_AXIS_CUTOFF_SHARPNESS','scope':'n=1 mod 4, n>=5; fixed affine-quadratic input-phase grammar','witnesses':witnesses,'small_group_controls':groups,'upper_witness_controls':cases,'nine_axis':{'cutoff':21,'thresholds':[24,21,22,23],'primitive_cuspidal_count':copies,'irreducible_degree':degree,'integer_character_identity':copies*degree,'integer_character_transvection':copies*transvection},'rejection_controls':4,'limits':['Green character theory is a cited theorem, not kernel-checked or enumerated at n=9.','The general upper proof is retained from PR5529; finite controls do not prove it.','No physical supplier, efficient group-algebra expansion or kappa improvement.']}
+
+
+if __name__ == '__main__':
+    result = json.loads(json.dumps(run(),sort_keys=True))
+    if '--write' in sys.argv: (HERE/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n')
+    else: need(result == json.loads((HERE/'RESULT.json').read_text()),'receipt differs')
+    print(result['status'])