diff --git a/research/two-axis-native-cutoff/PROOF.md b/research/two-axis-native-cutoff/PROOF.md
new file mode 100644
index 0000000000..68c7f71040
--- /dev/null
+++ b/research/two-axis-native-cutoff/PROOF.md
@@ -0,0 +1,328 @@
+# The exact two-axis native tensor cutoff is six
+
+Prepared for Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex
+assistance, including a separately assisted derivation and review.
+New work is Apache-2.0. This is an algebraic result for the precise monomial
+class below, not a physical supplier, a cost improvement, or a new
+multiplication bound.
+
+## 1. Class, definitions, and quantified result
+
+We specialize Ali Romman's
+[native tensor cutoff theorem](../native-tensor-cutoff/PROOF.md), Sections
+1–5, to two binary address axes. Retain its input-phase convention and
+fixed external scalar coefficients. Let $X=\mathbb F_2^2$, with addresses
+ordered as $(00,10,01,11)$, or equivalently $(0,1,2,3)$. The native group
+consists of
+
+$$
+ U(g,q)e_x=i^{q(x)}e_{g(x)},\qquad
+ q(x)=c+a_1x_1+a_2x_2+2b x_1x_2\pmod4,
+$$
+
+where $g\in\operatorname{AGL}(2,2)$, $c,a_1,a_2\in\mathbb Z/4$, and
+$b\in\mathbb Z/2$. Write $D_q=U(1,q)$ and use the factorization
+$U(g,q)=gD_q$: the phase acts first. This is the predecessor's exact
+Gaussian affine/quadratic monomial grammar. Hadamard gates and other
+nonmonomial operators are excluded.
+
+There are 128 diagonal phases and 24 affine permutations. Each group
+element has a unique factorization $gD_q$, so $|G|=3072$. Indeed, the
+affine permutation and four phase values determine it, and evaluation at
+$0,e_1,e_2,e_1+e_2$ recovers the displayed coefficients. The predecessor
+proves closure and inversion for this grammar. The faithful action of
+$\operatorname{AGL}(2,2)$, of order $4\cdot6=24$, on its four addresses
+identifies it with $S_4$. Its sign character is denoted $\operatorname{sgn}$.
+
+Work over $k=\mathbb Q(i)$ or $\mathbb C$. For every positive integer
+$f$, extend $\rho_f([U])=U^{\otimes f}$ linearly to $k[G]$. In
+particular, $\rho_f(\sum\alpha_U[U])=\sum\alpha_U U^{\otimes f}$; the
+external coefficients are not tensorized. Put $z=[iI]$, and let
+$I_r=(z-i^r[1])$ be the two-sided ideal of $k[G]$, for
+$r\in\{0,1,2,3\}$.
+
+**Theorem.** Set
+
+$$
+ (L_0,L_1,L_2,L_3)=(8,9,6,7).
+$$
+
+For every positive integer $f$, with $r=f\bmod4$,
+
+$$
+ \ker\rho_f=I_r\quad\Longleftrightarrow\quad f\ge L_r. \tag{1}
+$$
+
+Consequently the least integer $F\ge1$ such that
+$\ker\rho_f=I_{f\bmod4}$ for **every** $f\ge F$ is $F=6$.
+This is periodic stabilization after the central scalar relation; it does
+not assert that the four different residue kernels are equal.
+
+More exactly, a set $T$ of positive integer widths detects every
+nonzero $P\in k[G]$, in the sense that
+
+$$
+ (\forall f\in T,\ \rho_f(P)=0)\ \Longrightarrow\ P=0, \tag{2}
+$$
+
+if and only if, for each residue $r$, it contains some
+$f\equiv r\pmod4$ with $f\ge L_r$. Thus $6,7,8,9$ suffice,
+four widths are necessary, and no test set contained in $1,\ldots,8$
+suffices. This improves the predecessor's sufficient two-axis window
+$8,9,10,11$ to its least possible common cutoff. It does not improve
+its general-axis theorem.
+
+## 2. Fourier fibers and the exact faithfulness criterion
+
+Write a residual as
+
+$$
+ P=\sum_{g,c,a_1,a_2,b}\alpha_{g,c,a_1,a_2,b}[gD_q].
+$$
+
+At widths congruent to $r$, combine its constant phases by
+
+$$
+ \beta_{g,a_1,a_2,b}
+   =\sum_{c=0}^3\alpha_{g,c,a_1,a_2,b}i^{rc}.
+$$
+
+The unique normal forms $[gD_{0,a_1,a_2,b}]$ form a basis of
+$k[G]/I_r$, of dimension $24\cdot32=768$. Equivalently,
+$P\in I_r$ exactly when every $\beta$ vanishes. This also follows
+by taking the one-coordinate Fourier transform on the central $C_4$.
+
+For $\chi=(u_1,u_2,v)\in(\mathbb Z/4)^2\times\mathbb Z/2$, define
+
+$$
+ b_g(\chi)=\sum_{a_1,a_2,b}\beta_{g,a_1,a_2,b}
+                  i^{u_1a_1+u_2a_2+2vb}. \tag{3}
+$$
+
+The finite Fourier transform is invertible over both fields in question.
+Thus all $b_g(\chi)$ vanish exactly when $P\in I_r$. Conversely,
+for a fixed $r$, arbitrary values of the 768 quantities $b_g(\chi)$
+are realized by an element of this quotient.
+
+Let $\mathbf x\in X^f$ be an ordered input tuple, with multiplicities
+$m=(m_{00},m_{10},m_{01},m_{11})$. Its nonconstant phase character is
+
+$$
+ \chi_{\mathbf x}=
+ (m_{10}+m_{11}\bmod4,\ m_{01}+m_{11}\bmod4,\ m_{11}\bmod2).
+ \tag{4}
+$$
+
+For any ordered output tuple $\mathbf y$, direct substitution gives
+
+$$
+ \langle e_{\mathbf y},\rho_f(P)e_{\mathbf x}\rangle
+   =\sum_{g:\,g\mathbf x=\mathbf y}b_g(\chi_{\mathbf x}). \tag{5}
+$$
+
+Let $H_{\mathbf x}$ be the pointwise stabilizer of the addresses
+appearing in $\mathbf x$. If $\mathbf y=g_0\mathbf x$, the sum in
+(5) runs over $g_0H_{\mathbf x}$. If at least three distinct addresses
+appear, $H_{\mathbf x}$ is trivial: a permutation of four points
+fixing three fixes the fourth. Such a tuple exposes each
+$b_{g_0}(\chi_{\mathbf x})$ separately.
+
+If at most two distinct addresses appear, their pointwise stabilizer
+contains a transposition of two unused addresses. Consequently
+
+$$
+ \sum_{h\in H_{\mathbf x}}\operatorname{sgn}(h)=0. \tag{6}
+$$
+
+For example, multiplying the summation set by that transposition pairs
+its even and odd members. Suppose a character $\chi_*$ has no
+length-$f$ realization using at least three addresses. The nonzero
+Fourier assignment
+
+$$
+ b_g(\chi)=
+ \begin{cases}\operatorname{sgn}(g),&\chi=\chi_*,\\0,&\text{otherwise}
+ \end{cases}
+$$
+
+then makes every entry (5) zero by (6). It represents a nonzero element
+of $k[G]/I_r$. We have proved the **equivalence**
+
+$$
+ \ker\rho_f=I_r
+ \quad\Longleftrightarrow\quad
+ \text{every one of the 32 characters has a length-$f$
+ realization using at least three distinct addresses}. \tag{7}
+$$
+
+The necessity is essential. Merely improving a construction of an
+affinely spanning tuple would establish a sufficient cutoff, not its
+optimality. Here necessity follows from the special $S_4$ sign
+character; no analogous necessity is asserted for larger axis counts.
+
+## 3. Exact minimum width for each character
+
+Fix $r$ and $\chi=(u_1,u_2,v)$. Let
+$h=m_{11}\bmod4$. Equation (4) and the total length residue imply
+that $h\in\{v,v+2\}$ and the residue vector of $m$ is
+
+$$
+ a(h)=\bigl((r-u_1-u_2+h)\bmod4,
+              (u_1-h)\bmod4,
+              (u_2-h)\bmod4,h\bigr), \tag{8}
+$$
+
+with all four representatives chosen in $\{0,1,2,3\}$. Every
+admissible multiplicity vector is uniquely $a(h)+4t$, with
+$t\in\mathbb Z_{\ge0}^4$. An initially zero coordinate requires at
+least four added copies to become positive. Therefore the exact minimum
+length having at least three positive coordinates is
+
+$$
+ \ell(r,\chi)=\min_{h\in\{v,v+2\}}
+ \left(\sum_j a_j(h)
+       +4\max\bigl(0,3-|\{j:a_j(h)>0\}|\bigr)\right). \tag{9}
+$$
+
+This bound is attained: raise exactly the needed zero coordinates by
+four and leave the others unchanged. All candidate lengths are
+congruent to $r$. Adding four copies of address $00$ preserves
+the character, residue, and support condition. It follows that for a
+positive $f\equiv r$, a spanning realization exists **exactly** when
+$f\ge\ell(r,\chi)$. This formula and padding prove an all-width
+statement, without extrapolation from a finite census.
+
+## 4. Analytic upper bounds and their sharpness
+
+First take $r=2$. The two vectors in (8) are entrywise partners
+$a'=(a+2)\bmod4$. Write $S=\sum_j a_j$; then
+$S\in\{2,6,10\}$. If $S=10$, at least three entries are at
+least two, since otherwise $S\le3+3+1+1=8$. For
+$k=|\{j:a_j\ge2\}|$, the partner sum is
+$S'=S+8-4k\le6$. It is congruent to two, so we may replace $a$
+by its partner and assume $S=2$ or $6$.
+
+If $S=6$ and the support has at least three entries, it already
+gives the desired six-point tuple. Otherwise its only possible pattern
+is a permutation of $(3,3,0,0)$; its partner is a permutation of
+$(1,1,2,2)$, with sum six and full support. If $S=2$, its
+pattern is either $(2,0,0,0)$, whose partner is $(0,2,2,2)$,
+or $(1,1,0,0)$, for which adding four to one zero gives sum six
+and three positive entries. Thus **every** character has a six-point
+spanning realization at residue two.
+
+Adding one, two, or three copies of $00$ changes only the constant
+phase character. It gives a realization of every same nonconstant
+character at widths seven, eight, or nine, respectively. Four-copy
+padding then proves the upper bounds
+
+$$
+ \max_\chi\ell(0,\chi)\le8,\quad
+ \max_\chi\ell(1,\chi)\le9,\quad
+ \max_\chi\ell(2,\chi)\le6,\quad
+ \max_\chi\ell(3,\chi)\le7. \tag{10}
+$$
+
+For sharpness choose $\chi_0=(0,0,0)$. Its two vectors (8) are
+$(r,0,0,0)$ and $((r+2)\bmod4,2,2,2)$. Substituting in (9)
+gives the following two candidate lengths and their minima:
+
+| Residue $r$ | Candidate from $h=0$ | Candidate from $h=2$ | $\ell(r,\chi_0)$ |
+|---|---:|---:|---:|
+| 0 | 12 | 8 | 8 |
+| 1 | 9 | 9 | 9 |
+| 2 | 10 | 6 | 6 |
+| 3 | 11 | 7 | 7 |
+
+These attain all four upper bounds in (10). Equation (7) now proves
+(1). In particular residue one still has extra kernel at width five,
+so no $F\le5$ can be a common stabilization cutoff, whereas every
+width at least six meets its own residue threshold.
+
+## 5. Four explicit residuals and the exact test-set criterion
+
+The necessity witnesses can be given as fixed elements of $k[G]$,
+independent of the evaluated width. For a diagonal character
+$(r,\chi)=(r,u_1,u_2,v)$, put
+
+$$
+ E_{r,\chi}=\frac1{128}\sum_{c,a_1,a_2,b}
+       i^{-(rc+u_1a_1+u_2a_2+2vb)}[D_q],\qquad
+ A_{\mathrm{sgn}}=\sum_{g\in\operatorname{AGL}(2,2)}
+       \operatorname{sgn}(g)[g],
+$$
+
+and define $P_r=A_{\mathrm{sgn}}E_{r,\chi_0}$. The diagonal factor
+evaluates to the projector onto tuples with total length congruent to
+$r$ and nonconstant character $\chi$, by finite Fourier
+orthogonality. The order of multiplication is part of this definition:
+the phase projector acts on the input before the affine permutation.
+
+Each $P_r$ is nonzero in $k[G]$. In its expansion, each of the
+3072 unique normal forms $[gD_q]$ has a nonzero coefficient, a
+Gaussian unit times $1/128$. There are no collisions between terms.
+At a wrong-residue width its phase projector vanishes. At a
+matching-residue width below $L_r$, every surviving tuple uses at
+most two addresses, so (6) annihilates it. At every matching-residue
+width at least $L_r$, choose a three-address realization of
+$\chi_0$; its pointwise stabilizer is trivial, and
+
+$$
+ \langle e_{\mathbf x},\rho_f(P_r)e_{\mathbf x}\rangle=1. \tag{11}
+$$
+
+Concrete threshold multiplicities, in the address order fixed above,
+are $(2,2,2,2)$, $(1,0,4,4)$, $(0,2,2,2)$, and
+$(1,2,2,2)$ for $r=0,1,2,3$, respectively. For example,
+$P_1$ vanishes at **every** positive width one through eight, but
+has the entry (11) equal to one at width nine on the input/output
+tuple $(0,2,2,2,2,3,3,3,3)$.
+
+If a test set $T$ contains a threshold-reaching width in every
+residue and $\rho_f(P)=0$ on $T$, (1) gives $P\in I_r$
+for all four $r$. The four-coordinate Fourier transform in $c$
+then forces every $\alpha_{g,c,a_1,a_2,b}=0$. Conversely, if $T$
+has no threshold-reaching width in some residue $r$, the fixed
+nonzero residual $P_r$ vanishes on every width in $T$. This proves
+the necessity and sufficiency in (2), including for arbitrary finite
+or infinite sets of positive widths.
+
+## 6. Application boundary, evidence, and attribution
+
+All statements apply entrywise to complete matrices over $k[G]$.
+Consequently the predecessor's register-program endpoint interface can
+use widths $6,7,8,9$ for this two-axis grammar, provided the same
+recipes, scalar coefficients, and program are used at all widths.
+Every independent dirty input and every specified returned role must
+still be represented in the endpoint matrix; this result does not
+license omitting borrowed-role restoration or other outputs. Expansion
+of a program into group-algebra entries may be expensive. No new
+physical execution or efficient circuit-expansion claim follows.
+
+The executable evidence in this package checks the finite residue and
+character arithmetic and the explicit residual witnesses using exact
+arithmetic. The all-width conclusion is proved by (5)–(9) and the
+padding argument, not by sampling tensor widths. The normal forms,
+finite Fourier inversion, and $\operatorname{AGL}(2,2)\cong S_4$
+argument are the mathematical interface linking that finite evidence
+to the theorem. They are not a proof-kernel certificate or an
+independent human acceptance of the result.
+
+Ali Romman's predecessor supplies the native grammar, Fourier-separation
+method, four-residue obstruction, general sufficient cutoff, and
+register interface, and explicitly asks for the least stabilized width.
+Its retained PR #2250 source and notices credit Jose Manuel
+(@jmbarrancoml) and Douglas Colkitt; Chris R (@Clear1nsight) retains
+credit for the earlier finite-alphabet separation lineage. These inputs
+remain unchanged. Classical finite Fourier theory and the alternating
+representation of $S_4$ supply the tools used here. The addition is
+the exact two-axis criterion (7), sharp multiplicity formula (9), and
+its four optimal thresholds and test-set characterization. Mihir's
+[adjacent one-axis/general review](https://github.com/CrocSwap/integer-mult-bounds/discussions/5354#discussioncomment-19174027)
+explicitly leaves axis counts at least two outside its scope; this
+result addresses that distinct two-axis case.
+
+The least cutoff for $n\ge3$, sharper general-axis bounds, and
+extensions beyond the monomial grammar remain open here. In particular,
+neither the selected nine-axis frontier nor its admitted physical
+suppliers, costs, or multiplication exponent are changed by this proof.
diff --git a/research/two-axis-native-cutoff/README.md b/research/two-axis-native-cutoff/README.md
new file mode 100644
index 0000000000..b9278370bf
--- /dev/null
+++ b/research/two-axis-native-cutoff/README.md
@@ -0,0 +1,135 @@
+# The sharp two-axis native cutoff is six
+
+For the **two-axis affine/quadratic Gaussian monomial group**, a fixed
+scalar register identity holds at every positive tensor width exactly when
+it holds at widths **6, 7, 8 and 9**. This is the earliest sufficient
+consecutive window. A fixed nonzero residual vanishes at every width from
+1 through 8 and has a matrix entry equal to one at width 9.
+
+This answers the two-axis case of the least-cutoff question in
+[PR #5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369).
+Its general sufficient window specializes to 8–11; the new result gives
+the exact two-axis minimum and an obstruction to every earlier test set.
+The original general-axis theorem and checker remain unchanged.
+
+## Exact statement and why the lower bound holds
+
+Use the predecessor's input-phase convention
+`U(g,q)|x> = i^q(x)|g(x)>`, where `g` is binary affine on two axes and
+`q=c+a1*x1+a2*x2+2*b*x1*x2 (mod 4)`. External coefficients remain outside
+the tensor power. There are 128 phase recipes and 24 affine maps.
+
+At width `f`, the central scalar relation is `[iI]=i^r`, with `r=f mod 4`.
+After this relation, the group-algebra evaluation has zero kernel exactly
+at the following widths and every subsequent width of the same residue:
+
+| Residue r | First faithful width | A sharp witness's address multiplicities |
+| --- | ---: | --- |
+| 0 | 8 | (2,2,2,2) |
+| 1 | 9 | (1,0,4,4) |
+| 2 | 6 | (0,2,2,2) |
+| 3 | 7 | (1,2,2,2) |
+
+Address order is `(00,10,01,11)`. Thus the least common stabilized cutoff
+is **F=6**. The kernels are periodic in the central residue; they are not
+all the same kernel. More generally, a set of test widths is complete
+**if and only if** it contains a threshold-reaching width in every residue.
+The same recipes, external coefficients and program must be used at all
+widths, with all independent dirty inputs and specified output roles retained.
+
+The [proof](PROOF.md) establishes necessity as well as sufficiency.
+`AGL(2,2)=S4`: three distinct input addresses determine an affine map,
+while a tuple using at most two addresses has an odd permutation in its
+pointwise stabilizer. The alternating sum of affine maps therefore kills
+such tuples. Combining it with a normalized phase projector supplies four
+explicit fixed residuals, one per residue. Exact multiplicity congruences
+and an analytic case split prove the four sharp thresholds. This necessity
+argument is special to two axes; a phase-character census alone would not
+establish a representation-kernel minimum.
+
+For the residue-one residual, the width-nine input and output are both
+`(0,2,2,2,2,3,3,3,3)`. Its diagonal entry is exactly `1`, and its column
+has 24 distinct signed outputs. The [receipt](RESULT.json) gives all four
+witnesses. No enormous tensor matrix is built.
+
+## Reproduce and evidence
+
+Python 3.12 and the standard library suffice:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/two-axis-native-cutoff --check-only
+python3.12 -B scripts/research_package.py --package research/two-axis-native-cutoff
+python3.12 -I -O -B research/two-axis-native-cutoff/verify.py
+```
+
+Expected marker: `PASS_SHARP_TWO_AXIS_NATIVE_CUTOFF`.
+
+[verify.py](verify.py) checks the minimum formula for all 128 phase characters
+against a separate complete 625-count normal-form census and exact fixed-width
+realizations through 13. Reducing each positive multiplicity to 1–4 preserves
+its phase and support, which proves the minimum census complete.
+[literal.py](literal.py) independently evaluates all 128 Fourier terms and
+signed affine images. It checks all 24 affine maps, 576 sign compositions,
+3,072 phase pullbacks, all 15 nonempty pointwise stabilizers, all 1,364 ordered
+tuples at the relevant below-threshold widths, and 2,856 phase sums on count
+classes through width 9. Controls omit affine signs, omit the quadratic phase,
+tensorize external Fourier coefficients, or confuse phase realization with
+full affine separation. They give different exact outcomes as required.
+Neither implementation imports a predecessor evaluator. The shared mathematical
+contract and Python runtime remain limits to computational independence.
+
+[VERIFICATION.md](VERIFICATION.md) records the normal, optimized,
+committed-byte/source-history and Git-free export checks. Finite results
+corroborate the proof; they do not establish an unbounded-width theorem by
+sampling. No independent human review or proof-kernel acceptance is claimed.
+
+## Scope, coordination and remaining work
+
+This is a scoped mathematical result. It does not supply a physical supplier,
+complete native caller adapter, tape/precision invoice, or new multiplication
+exponent. The selected conditional κ remains 0.003027288235, with its inherited
+assumptions. In particular, the current nine-axis supplier does not acquire
+a new cutoff from this two-axis result. Hadamards, arbitrary width-dependent
+programs and nonlinear or rectangular interfaces are outside this grammar.
+
+The round starts from canonical main
+`32890bc5de034ab8fc93ac88ead7279a6a416d04`, priority revision 7; the predecessor
+head is `18354f41de4dc7bfda4692e814cf1d91a6d619ef`.
+[SOURCES.json](SOURCES.json) pins its exact proof, scope and attribution bytes.
+The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5354#discussioncomment-19174077)
+records this bounded specialization. It complements
+[Mihir Srivastava's active one-axis/general-proof audit](https://github.com/CrocSwap/integer-mult-bounds/discussions/5354#discussioncomment-19174027),
+which explicitly excludes least cutoffs for n>=2. Its small-character
+enumerations are overlapping corroboration, not the new result claimed here.
+
+The initial fresh snapshot covered 378 open PR bodies and 4,790 Discussion
+records, with complete local-note coverage. Targeted successor and canonical
+thread checks found no two-axis sharp-cutoff contribution in that coverage;
+arbitrary diffs and unpublished work remain unknown. [TASK.json](TASK.json)
+records the scope change from the formal-interface card: a written kernel
+lemma and exact certificates, with no proof-assistant build. The current picker
+was run once (seed `77f1c0eee02e0484b09774f596f29b84`, bit-mechanism suggestions);
+the explicit least-cutoff question supplied this scoped mathematical assignment.
+
+## Open next questions
+
+For n>=3, which phase-fiber permutation representations are needed for the
+exact central-quotient kernel? The two-axis sign obstruction does not establish
+necessity of affine-span tuples there. A useful next step is to calculate the
+pointwise-stabilizer coset-sum row spaces in one specified three-axis phase
+fiber, and compare their common kernel with affine-bucket isolation. That
+representation-theoretic bridge, rather than another character table alone,
+is the missing step toward a sharper general cutoff. No general-n search
+is claimed or reserved by this package.
+
+## Credit
+
+Prepared by Hiroki KUMAZAKI with substantial OpenAI Codex assistance, including
+separate automated proof, literal-checker and adversarial-review subagents.
+Ali Romman supplied the native grammar, Fourier-separation method, uniform
+cutoff and open least-width question in #5369. Jose Manuel's native recipe
+and phase-sector conventions, ywz65's affine-basis argument, Chris R's
+finite-alphabet tensor-separation lineage, Douglas Colkitt, and the retained
+source contributors keep their credit. The source NOTICE remains pinned.
+Fourier inversion and symmetric-group sign representations are classical;
+no global literature-priority claim is made. New work is Apache-2.0.
diff --git a/research/two-axis-native-cutoff/RESULT.json b/research/two-axis-native-cutoff/RESULT.json
new file mode 100644
index 0000000000..14bdb54fa4
--- /dev/null
+++ b/research/two-axis-native-cutoff/RESULT.json
@@ -0,0 +1,540 @@
+{
+  "authenticated_inputs": [
+    "LICENSE",
+    "research/native-tensor-cutoff/PROOF.md",
+    "research/native-tensor-cutoff/README.md",
+    "research/native-tensor-cutoff/TASK.json",
+    "research/native-tensor-cutoff/source/NOTICE.md"
+  ],
+  "general_n_cutoff_claimed": false,
+  "literal_obstructions": {
+    "accepted_compositions_by_width_and_residue": {
+      "1": [
+        0,
+        1,
+        0,
+        0
+      ],
+      "2": [
+        0,
+        0,
+        1,
+        0
+      ],
+      "3": [
+        0,
+        0,
+        0,
+        1
+      ],
+      "4": [
+        4,
+        0,
+        0,
+        0
+      ],
+      "5": [
+        0,
+        4,
+        0,
+        0
+      ],
+      "6": [
+        0,
+        0,
+        5,
+        0
+      ],
+      "7": [
+        0,
+        0,
+        0,
+        5
+      ],
+      "8": [
+        11,
+        0,
+        0,
+        0
+      ],
+      "9": [
+        0,
+        11,
+        0,
+        0
+      ]
+    },
+    "affine_composition_sign_checks": 576,
+    "affine_maps": 24,
+    "arithmetic": "integer Gaussian pairs and exact rational normalization; no floating point",
+    "below_threshold_census": [
+      {
+        "enumerated_widths": [
+          4
+        ],
+        "first_nonzero_width": 8,
+        "ordered_tuple_cases": 256,
+        "residue": 0
+      },
+      {
+        "enumerated_widths": [
+          1,
+          5
+        ],
+        "first_nonzero_width": 9,
+        "ordered_tuple_cases": 1028,
+        "residue": 1
+      },
+      {
+        "enumerated_widths": [
+          2
+        ],
+        "first_nonzero_width": 6,
+        "ordered_tuple_cases": 16,
+        "residue": 2
+      },
+      {
+        "enumerated_widths": [
+          3
+        ],
+        "first_nonzero_width": 7,
+        "ordered_tuple_cases": 64,
+        "residue": 3
+      }
+    ],
+    "coefficient_order": "(sum_h sign(h)[h]) E_chi; input phases act first",
+    "controls": {
+      "omitted_quadratic": {
+        "correct_projector": "0",
+        "counts": [
+          0,
+          3,
+          3,
+          1
+        ],
+        "residue": 3,
+        "wrong_output_count": 24,
+        "wrong_projector": "1"
+      },
+      "omitted_sign": [
+        {
+          "residue": 0,
+          "width": 4,
+          "wrong_coefficients": "6",
+          "wrong_output_count": 4
+        },
+        {
+          "residue": 1,
+          "width": 1,
+          "wrong_coefficients": "6",
+          "wrong_output_count": 4
+        },
+        {
+          "residue": 2,
+          "width": 2,
+          "wrong_coefficients": "6",
+          "wrong_output_count": 4
+        },
+        {
+          "residue": 3,
+          "width": 3,
+          "wrong_coefficients": "6",
+          "wrong_output_count": 4
+        }
+      ],
+      "tensor_powered_external_coefficients": {
+        "correct_projector": "0",
+        "counts": [
+          0,
+          2,
+          2,
+          2
+        ],
+        "residue": 1,
+        "wrong_output_count": 24,
+        "wrong_projector": "1/34359738368"
+      }
+    },
+    "first_witnesses": [
+      {
+        "counts": [
+          2,
+          2,
+          2,
+          2
+        ],
+        "diagonal_entry": "1",
+        "distinct_output_tuples": 24,
+        "input_tuple": [
+          0,
+          0,
+          1,
+          1,
+          2,
+          2,
+          3,
+          3
+        ],
+        "negative_output_coefficients": 12,
+        "positive_output_coefficients": 12,
+        "residue": 0,
+        "width": 8
+      },
+      {
+        "counts": [
+          1,
+          0,
+          4,
+          4
+        ],
+        "diagonal_entry": "1",
+        "distinct_output_tuples": 24,
+        "input_tuple": [
+          0,
+          2,
+          2,
+          2,
+          2,
+          3,
+          3,
+          3,
+          3
+        ],
+        "negative_output_coefficients": 12,
+        "positive_output_coefficients": 12,
+        "residue": 1,
+        "width": 9
+      },
+      {
+        "counts": [
+          0,
+          2,
+          2,
+          2
+        ],
+        "diagonal_entry": "1",
+        "distinct_output_tuples": 24,
+        "input_tuple": [
+          1,
+          1,
+          2,
+          2,
+          3,
+          3
+        ],
+        "negative_output_coefficients": 12,
+        "positive_output_coefficients": 12,
+        "residue": 2,
+        "width": 6
+      },
+      {
+        "counts": [
+          1,
+          2,
+          2,
+          2
+        ],
+        "diagonal_entry": "1",
+        "distinct_output_tuples": 24,
+        "input_tuple": [
+          0,
+          1,
+          1,
+          2,
+          2,
+          3,
+          3
+        ],
+        "negative_output_coefficients": 12,
+        "positive_output_coefficients": 12,
+        "residue": 3,
+        "width": 7
+      }
+    ],
+    "method": "literal affine permutations, all128 input-phase Fourier terms, signed tuple images",
+    "native_group_elements": 3072,
+    "phase_polynomials": 128,
+    "phase_pullback_checks": 3072,
+    "projector_normalization": "1/128",
+    "scope": "Independent finite evidence for the written two-axis theorem; no physical supplier or all-n cutoff",
+    "stabilizers": [
+      {
+        "odd_stabilizer_elements": 3,
+        "points": [
+          0
+        ],
+        "stabilizer_size": 6
+      },
+      {
+        "odd_stabilizer_elements": 3,
+        "points": [
+          1
+        ],
+        "stabilizer_size": 6
+      },
+      {
+        "odd_stabilizer_elements": 1,
+        "points": [
+          0,
+          1
+        ],
+        "stabilizer_size": 2
+      },
+      {
+        "odd_stabilizer_elements": 3,
+        "points": [
+          2
+        ],
+        "stabilizer_size": 6
+      },
+      {
+        "odd_stabilizer_elements": 1,
+        "points": [
+          0,
+          2
+        ],
+        "stabilizer_size": 2
+      },
+      {
+        "odd_stabilizer_elements": 1,
+        "points": [
+          1,
+          2
+        ],
+        "stabilizer_size": 2
+      },
+      {
+        "odd_stabilizer_elements": 0,
+        "points": [
+          0,
+          1,
+          2
+        ],
+        "stabilizer_size": 1
+      },
+      {
+        "odd_stabilizer_elements": 3,
+        "points": [
+          3
+        ],
+        "stabilizer_size": 6
+      },
+      {
+        "odd_stabilizer_elements": 1,
+        "points": [
+          0,
+          3
+        ],
+        "stabilizer_size": 2
+      },
+      {
+        "odd_stabilizer_elements": 1,
+        "points": [
+          1,
+          3
+        ],
+        "stabilizer_size": 2
+      },
+      {
+        "odd_stabilizer_elements": 0,
+        "points": [
+          0,
+          1,
+          3
+        ],
+        "stabilizer_size": 1
+      },
+      {
+        "odd_stabilizer_elements": 1,
+        "points": [
+          2,
+          3
+        ],
+        "stabilizer_size": 2
+      },
+      {
+        "odd_stabilizer_elements": 0,
+        "points": [
+          0,
+          2,
+          3
+        ],
+        "stabilizer_size": 1
+      },
+      {
+        "odd_stabilizer_elements": 0,
+        "points": [
+          1,
+          2,
+          3
+        ],
+        "stabilizer_size": 1
+      },
+      {
+        "odd_stabilizer_elements": 0,
+        "points": [
+          0,
+          1,
+          2,
+          3
+        ],
+        "stabilizer_size": 1
+      }
+    ],
+    "weak_composition_phase_checks": 2856,
+    "wrong_central_residue_checks": 2142
+  },
+  "minimum_widths": {
+    "complete_four_width_window": [
+      6,
+      7,
+      8,
+      9
+    ],
+    "count_normal_forms": 625,
+    "fixed_width_corroboration": [
+      {
+        "central_quotient_injective": false,
+        "full_span_characters": 0,
+        "width": 1
+      },
+      {
+        "central_quotient_injective": false,
+        "full_span_characters": 0,
+        "width": 2
+      },
+      {
+        "central_quotient_injective": false,
+        "full_span_characters": 4,
+        "width": 3
+      },
+      {
+        "central_quotient_injective": false,
+        "full_span_characters": 13,
+        "width": 4
+      },
+      {
+        "central_quotient_injective": false,
+        "full_span_characters": 28,
+        "width": 5
+      },
+      {
+        "central_quotient_injective": true,
+        "full_span_characters": 32,
+        "width": 6
+      },
+      {
+        "central_quotient_injective": true,
+        "full_span_characters": 32,
+        "width": 7
+      },
+      {
+        "central_quotient_injective": true,
+        "full_span_characters": 32,
+        "width": 8
+      },
+      {
+        "central_quotient_injective": true,
+        "full_span_characters": 32,
+        "width": 9
+      },
+      {
+        "central_quotient_injective": true,
+        "full_span_characters": 32,
+        "width": 10
+      },
+      {
+        "central_quotient_injective": true,
+        "full_span_characters": 32,
+        "width": 11
+      },
+      {
+        "central_quotient_injective": true,
+        "full_span_characters": 32,
+        "width": 12
+      },
+      {
+        "central_quotient_injective": true,
+        "full_span_characters": 32,
+        "width": 13
+      }
+    ],
+    "formula_matches_complete_minimum_census": true,
+    "per_residue": [
+      {
+        "attaining_character": [
+          0,
+          0,
+          0,
+          0
+        ],
+        "attaining_minimum": 8,
+        "first_faithful_width": 8,
+        "minimum_width_histogram": {
+          "4": 13,
+          "8": 19
+        },
+        "residue": 0
+      },
+      {
+        "attaining_character": [
+          1,
+          0,
+          0,
+          0
+        ],
+        "attaining_minimum": 9,
+        "first_faithful_width": 9,
+        "minimum_width_histogram": {
+          "5": 28,
+          "9": 4
+        },
+        "residue": 1
+      },
+      {
+        "attaining_character": [
+          2,
+          0,
+          0,
+          0
+        ],
+        "attaining_minimum": 6,
+        "first_faithful_width": 6,
+        "minimum_width_histogram": {
+          "6": 32
+        },
+        "residue": 2
+      },
+      {
+        "attaining_character": [
+          3,
+          0,
+          0,
+          0
+        ],
+        "attaining_minimum": 7,
+        "first_faithful_width": 7,
+        "minimum_width_histogram": {
+          "3": 4,
+          "7": 28
+        },
+        "residue": 3
+      }
+    ],
+    "phase_character_count": 128,
+    "phase_only_false_positive_width": 1,
+    "uniform_cutoff": 6
+  },
+  "physical_supplier_claimed": false,
+  "proof": "PROOF.md supplies the all-width necessity/sufficiency and analytic upper-bound argument",
+  "scope": "Two-axis affine/quadratic Gaussian monomials over Q(i) or C; group-algebra kernel modulo central phase",
+  "selected_frontier_changed": false,
+  "status": "PASS_SHARP_TWO_AXIS_NATIVE_CUTOFF",
+  "test_set_criterion": {
+    "all_widths_one_through_eight_fail": true,
+    "criterion": "For each r, include an f congruent to r modulo 4 with f >= (8,9,6,7)[r]",
+    "first_sufficient_consecutive_window_start": 6,
+    "fixed_external_coefficients_required": true,
+    "test_sets_with_at_most_three_widths_checked": 378
+  }
+}
diff --git a/research/two-axis-native-cutoff/SOURCES.json b/research/two-axis-native-cutoff/SOURCES.json
new file mode 100644
index 0000000000..61bb484b08
--- /dev/null
+++ b/research/two-axis-native-cutoff/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "LICENSE",
+      "usage": "input",
+      "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64",
+      "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4"
+    },
+    {
+      "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/native-tensor-cutoff/PROOF.md",
+      "usage": "input",
+      "git_blob": "2d92f17cd8e1064028656cd4ff06c1d38f14ebc0",
+      "sha256": "b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041"
+    },
+    {
+      "path": "research/native-tensor-cutoff/README.md",
+      "usage": "input",
+      "git_blob": "91ae9eadd8a8679de7cf488fc2e3f350214feeff",
+      "sha256": "98a3166b7d0db513e8918f17f73359bebde1f802af251f6c55305fb99b869f87"
+    },
+    {
+      "path": "research/native-tensor-cutoff/TASK.json",
+      "usage": "input",
+      "git_blob": "d76d6738ff583c6b2b7d5b7667106bb1bb98f302",
+      "sha256": "0c6f72983c036d4b2f737c1e35363bab0e31b08de2317b31180ecf038d498e7d"
+    },
+    {
+      "path": "research/native-tensor-cutoff/source/NOTICE.md",
+      "usage": "input",
+      "git_blob": "e82bfef53054bd753ba0aa8a966f84427faa2293",
+      "sha256": "74a9f03e9ce467c75f5f7cf1b8465d349ea38ef114afad261824c3bcf13da00f"
+    }
+  ]
+}
diff --git a/research/two-axis-native-cutoff/TASK.json b/research/two-axis-native-cutoff/TASK.json
new file mode 100644
index 0000000000..5fcf35c262
--- /dev/null
+++ b/research/two-axis-native-cutoff/TASK.json
@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "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": "Sharp two-axis affine/quadratic Gaussian monomial central-quotient kernel cutoff F=6, exact per-residue thresholds and complete test-set criterion, with fixed phase-sign obstruction residuals.",
+  "scope_change_reason": "The predecessor explicitly asks for least stabilized widths. This bounded two-axis mathematical result is complementary to the live one-axis/general audit and replaces a proof-assistant formalization with a written theorem and exact executable evidence.",
+  "bottleneck_link": "Finite native identity tests need an exact width contract. This closes the two-axis minimum question and demonstrates phase-affine cancellation invisible through width eight, without asserting a cutoff for the selected nine-axis supplier or changing its paid bill.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the n=2 necessity/sufficiency proof, sharp residuals, bounded independent checks and portable publication; no n>=3 search, complete native supplier, formal build or selected change.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, RESULT.json, verify.py, literal.py, VERIFICATION.md",
+  "author": "Hiroki KUMAZAKI",
+  "ai_assistance": "Substantial OpenAI Codex assistance, including separate automated mathematical derivation, literal checker and adversarial review subagents in the same session. No independent human or proof-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "For n>=3, what is the exact common kernel of phase-fiber pointwise-stabilizer coset-sum representations?",
+      "why_it_matters": "Full-span tuple realization is sufficient in general, but the S4 sign argument making it necessary here does not extend automatically. The exact representation kernel is needed for a minimum cutoff.",
+      "first_step": "Choose one three-axis phase fiber and compute the coset-sum row spaces from all its attainable support stabilizers; distinguish their common kernel from simple affine-span availability.",
+      "blocked_by": "No general-n necessity bridge or minimal-threshold theorem is supplied; a character census alone cannot fill it."
+    }
+  ],
+  "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5354#discussioncomment-19174077",
+  "predecessor": {
+    "pr": 5369,
+    "head": "18354f41de4dc7bfda4692e814cf1d91a6d619ef"
+  },
+  "adjacent_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5354#discussioncomment-19174027"
+}
diff --git a/research/two-axis-native-cutoff/VERIFICATION.md b/research/two-axis-native-cutoff/VERIFICATION.md
new file mode 100644
index 0000000000..537876639f
--- /dev/null
+++ b/research/two-axis-native-cutoff/VERIFICATION.md
@@ -0,0 +1,58 @@
+# Verification record
+
+Environment: CPython 3.12.13, Linux x86_64, standard library only, 2026-10-25.
+The scientific base and publication refresh both resolve canonical main to
+`32890bc5de034ab8fc93ac88ead7279a6a416d04`. PR5369 remains merged at
+`18354f41de4dc7bfda4692e814cf1d91a6d619ef`; its source bytes, relevant
+instructions, priorities and selected record were unchanged.
+
+These checks passed:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/two-axis-native-cutoff --check-only
+python3.12 -B scripts/research_package.py --package research/two-axis-native-cutoff
+python3.12 -I -O -B research/two-axis-native-cutoff/verify.py
+python3.12 -B scripts/check_research_commit.py --package research/two-axis-native-cutoff --check-source-history
+python3.12 -B scripts/export_research_package.py export --package research/two-axis-native-cutoff --output /tmp/imb-two-axis-cutoff.tar
+python3.12 -B scripts/export_research_package.py check /tmp/imb-two-axis-cutoff.tar
+```
+
+The official committed export was extracted with Python's `data` tar filter
+to a fresh directory outside the checkout. Its verifier passed using the
+absolute interpreter path, `-I -O -B`, `PATH=/nonexistent` and empty
+`PYTHONPATH`. The exported package needs neither Git nor predecessor code
+imports. Normal and optimized runs compare the entire deterministic receipt.
+Proof-relevant checks use explicit exceptions, so optimization cannot remove
+them. Committed-byte/source-history and export checks authenticate transport
+and provenance; they do not establish mathematical acceptance.
+
+The receipt covers 128 character minima against all 625 count normal forms,
+fixed-width realizations through 13, 24 affine maps, 128 phase polynomials,
+576 affine sign-composition checks, 3,072 phase pullbacks, all 15 nonempty
+pointwise stabilizers, all 1,364 relevant below-threshold ordered tuples,
+and 2,856 direct phase-projector sums on count classes through width 9.
+All four first witnesses have diagonal entry one and 24 distinct signed
+outputs. Controls detect missing signs, an omitted quadratic phase,
+tensor-powered external coefficients and phase-only false acceptance.
+
+The analytic Fourier/stabilizer argument and multiplicity formula in
+PROOF.md establish the all-width theorem and necessity. Finite results
+corroborate these arguments; this is not an extrapolation of a small-width
+census. Automated subagents separately derived the proof, implemented the
+literal checker and reviewed the kernel/test-set implications. This is
+substantial AI-assisted evidence, not independent human or proof-kernel
+acceptance. No general-axis theorem, physical invoice, complete native
+supplier/outer/selected cold replay, Lean or Docker run is claimed.
+
+Hosted CI is separate from this local verification record and is reported
+on the pull request. The frozen predecessor and selected frontier remain
+unchanged.
+
+Submission overlap refresh: 379 open PR bodies at 06:25:52 UTC and 4,797
+Discussion records through 06:27:01 UTC, both with complete pagination.
+All 7,402 tracked base local notes were searched, along with this package's
+then-untracked README/TASK notes; no coverage warnings were reported. The
+original #5369 result/handoff, the complementary one-axis audit, related
+full-Clifford/caller work and this round's own claim were distinguished.
+No matching sharp two-axis theorem appeared in that coverage. Arbitrary
+code diffs and unpublished work remain outside the search.
diff --git a/research/two-axis-native-cutoff/VERIFY.json b/research/two-axis-native-cutoff/VERIFY.json
new file mode 100644
index 0000000000..33e084dcc9
--- /dev/null
+++ b/research/two-axis-native-cutoff/VERIFY.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "LICENSE",
+    "research/native-tensor-cutoff/PROOF.md",
+    "research/native-tensor-cutoff/README.md",
+    "research/native-tensor-cutoff/TASK.json",
+    "research/native-tensor-cutoff/source/NOTICE.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact two-axis minimum formula against complete count normal forms; independent literal phase/sign residuals, all four threshold witnesses and semantic controls; deterministic receipt."
+    }
+  ]
+}
diff --git a/research/two-axis-native-cutoff/literal.py b/research/two-axis-native-cutoff/literal.py
new file mode 100644
index 0000000000..f0bde3fd53
--- /dev/null
+++ b/research/two-axis-native-cutoff/literal.py
@@ -0,0 +1,254 @@
+"""Independent literal checks for the two-axis native cutoff.
+
+Hiroki KUMAZAKI, with substantial OpenAI Codex assistance. Apache-2.0.
+No predecessor implementation or package verifier is imported. Arithmetic is
+integer Gaussian arithmetic, with explicit rational normalization. Points are
+00,10,01,11, encoded by 0,1,2,3; phases are evaluated at the input.
+"""
+from collections import Counter
+from fractions import Fraction
+from itertools import permutations, product
+
+
+ROOTS = ((1, 0), (0, 1), (-1, 0), (0, -1))
+LIMITS = (8, 9, 6, 7)
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def parity(permutation):
+    inversions = sum(permutation[i] > permutation[j]
+                     for i in range(4) for j in range(i+1, 4))
+    return -1 if inversions % 2 else 1
+
+
+def affine_and_phase_tables():
+    affine = []
+    for first, second, offset in product(range(1, 4), range(1, 4), range(4)):
+        if first == second:
+            continue
+        table = tuple((((first & x).bit_count() % 2)
+                       | (((second & x).bit_count() % 2) << 1)) ^ offset
+                      for x in range(4))
+        need(len(set(table)) == 4, 'Invertible literal affine map')
+        affine.append(table)
+    need(len(affine) == len(set(affine)) == 24, 'Twenty-four distinct affine maps')
+    need(set(affine) == set(permutations(range(4))), 'AGL(2,2) is the full S4')
+    affine.sort()
+    for left, right in product(affine, repeat=2):
+        composed = tuple(left[right[x]] for x in range(4))
+        need(composed in affine and parity(composed) == parity(left)*parity(right),
+             'Literal permutation sign is multiplicative')
+
+    phases = []
+    for c, a1, a2, b in product(range(4), range(4), range(4), range(2)):
+        table = tuple((c+a1*(x & 1)+a2*((x >> 1) & 1)
+                       +2*b*(x & 1)*((x >> 1) & 1)) % 4 for x in range(4))
+        phases.append(((c, a1, a2, b), table))
+    phase_functions = {table for _, table in phases}
+    need(len(phases) == len(phase_functions) == 128, 'All phase recipes are distinct')
+    for permutation, (_, table) in product(affine, phases):
+        need(tuple(table[permutation[x]] for x in range(4)) in phase_functions,
+             'Affine pullback preserves the literal phase family')
+    return affine, phases
+
+
+def fourier_numerator(points, residue, phases, *, omit_quadratic=False,
+                      tensor_power_coefficients=False):
+    """Sum all 128 terms of E_(residue,0,0,0), before normalization.
+
+    U(h,q)=[h][d_q], so the phase acts on the original tuple, before h.
+    The correct external Fourier coefficient i^(-residue*c)/128 occurs once.
+    The tensor-power control intentionally raises that coefficient to |points|.
+    """
+    real, imaginary = 0, 0
+    coefficient_power = len(points) if tensor_power_coefficients else 1
+    for (c, a1, a2, _), table in phases:
+        if omit_quadratic:
+            phase = sum(c+a1*(x & 1)+a2*((x >> 1) & 1) for x in points)
+        else:
+            phase = sum(table[x] for x in points)
+        value = ROOTS[(phase-coefficient_power*residue*c) % 4]
+        real += value[0]
+        imaginary += value[1]
+    return real, imaginary
+
+
+def projector(points, residue, phases, *, omit_quadratic=False):
+    numerator = fourier_numerator(points, residue, phases,
+                                  omit_quadratic=omit_quadratic)
+    need(numerator in ((0, 0), (128, 0)), 'Normalized Fourier projector is zero or one')
+    return numerator[0] // 128
+
+
+def antisymmetrize(points, affine, *, omit_sign=False):
+    output = Counter()
+    for permutation in affine:
+        destination = tuple(permutation[x] for x in points)
+        output[destination] += 1 if omit_sign else parity(permutation)
+    return {key: value for key, value in output.items() if value}
+
+
+def evaluate(points, residue, affine, phases, *, omit_quadratic=False):
+    # This order is the literal product (sum sign(h)[h]) E_chi.
+    weight = projector(points, residue, phases, omit_quadratic=omit_quadratic)
+    if not weight:
+        return {}
+    return {key: weight*value for key, value in antisymmetrize(points, affine).items()}
+
+
+def compositions(total):
+    for c0 in range(total+1):
+        for c1 in range(total-c0+1):
+            for c2 in range(total-c0-c1+1):
+                yield c0, c1, c2, total-c0-c1-c2
+
+
+def tuple_of_counts(counts):
+    return tuple(point for point, count in enumerate(counts) for _ in range(count))
+
+
+def stabilizer_checks(affine):
+    reports = []
+    identity = (0, 1, 2, 3)
+    for mask in range(1, 16):
+        subset = tuple(x for x in range(4) if (mask >> x) & 1)
+        stabilizer = [p for p in affine if all(p[x] == x for x in subset)]
+        odd = [p for p in stabilizer if parity(p) == -1]
+        if len(subset) <= 2:
+            need(odd and sum(parity(p) for p in stabilizer) == 0,
+                 'Every small-support pointwise stabilizer contains odd cancellation')
+            need(not antisymmetrize(subset, affine), 'All small-support coset sums vanish')
+        else:
+            need(stabilizer == [identity], 'Three distinct points have trivial stabilizer')
+            need(len(antisymmetrize(subset, affine)) == 24,
+                 'Full-span tuples have twenty-four distinct images')
+        reports.append({'points': list(subset), 'stabilizer_size': len(stabilizer),
+                        'odd_stabilizer_elements': len(odd)})
+    return reports
+
+
+def run():
+    affine, phases = affine_and_phase_tables()
+    stabilizers = stabilizer_checks(affine)
+
+    # Enumerate actual ordered tuples, not only count classes, at every
+    # positive same-residue width below the alleged first nonzero width.
+    below = []
+    for residue, limit in enumerate(LIMITS):
+        cases, widths = 0, []
+        for width in range(1, limit):
+            if width % 4 != residue:
+                continue
+            widths.append(width)
+            for points in product(range(4), repeat=width):
+                need(not evaluate(points, residue, affine, phases),
+                     'Literal residual vanishes on every below-threshold tuple')
+                cases += 1
+        below.append({'residue': residue, 'first_nonzero_width': limit,
+                      'enumerated_widths': widths, 'ordered_tuple_cases': cases})
+    need(sum(row['ordered_tuple_cases'] for row in below) == 1364,
+         'Complete declared ordered-tuple census')
+
+    # Direct 128-term sums on all weak compositions corroborate the central
+    # selection rule and all positive widths through nine. Tuple ordering
+    # cannot change a sum of input phases. The all-width central-residue
+    # statement is the elementary sum over c, not an inference from this bound.
+    composition_cases, wrong_residue_cases = 0, 0
+    accepted_by_width = {}
+    for width in range(1, 10):
+        accepted = [0]*4
+        for counts in compositions(width):
+            points = tuple_of_counts(counts)
+            for residue in range(4):
+                value = projector(points, residue, phases)
+                composition_cases += 1
+                if width % 4 != residue:
+                    need(value == 0, 'All other central residues vanish')
+                    wrong_residue_cases += 1
+                accepted[residue] += value
+        accepted_by_width[str(width)] = accepted
+    need(composition_cases == 2856 and wrong_residue_cases == 2142,
+         'All positive weak compositions through nine, in all four residues')
+
+    witnesses = []
+    for residue, width in enumerate(LIMITS):
+        candidates = []
+        for counts in compositions(width):
+            if sum(count > 0 for count in counts) < 3:
+                continue
+            points = tuple_of_counts(counts)
+            if projector(points, residue, phases):
+                candidates.append((counts, points))
+        need(candidates, 'A literal full-span first witness exists')
+        counts, points = candidates[0]
+        result = evaluate(points, residue, affine, phases)
+        need(len(result) == 24 and result.get(points) == 1
+             and set(result.values()) == {-1, 1},
+             'First witness has diagonal entry one and twenty-four distinct signed outputs')
+        witnesses.append({'residue': residue, 'width': width, 'counts': list(counts),
+                          'input_tuple': list(points), 'diagonal_entry': '1',
+                          'distinct_output_tuples': len(result),
+                          'positive_output_coefficients': sum(v == 1 for v in result.values()),
+                          'negative_output_coefficients': sum(v == -1 for v in result.values())})
+    need(witnesses[1]['counts'] == [1, 0, 4, 4], 'Declared width-nine witness binding')
+
+    no_sign = []
+    for residue, limit in enumerate(LIMITS):
+        width = residue or 4
+        points = (0,)*width
+        need(width < limit and projector(points, residue, phases) == 1,
+             'Sign-removal control has an admitted phase below the cutoff')
+        correct = evaluate(points, residue, affine, phases)
+        wrong = antisymmetrize(points, affine, omit_sign=True)
+        need(not correct and len(wrong) == 4 and set(wrong.values()) == {6},
+             'Omitting permutation signs destroys the below-cutoff identity')
+        no_sign.append({'residue': residue, 'width': width,
+                        'wrong_output_count': 4, 'wrong_coefficients': '6'})
+
+    quadratic_points = tuple_of_counts((0, 3, 3, 1))
+    need(projector(quadratic_points, 3, phases) == 0
+         and projector(quadratic_points, 3, phases, omit_quadratic=True) == 1
+         and len(evaluate(quadratic_points, 3, affine, phases, omit_quadratic=True)) == 24,
+         'Omitting the quadratic phase wrongly accepts an odd pair count')
+
+    scalar_points = tuple_of_counts((0, 2, 2, 2))
+    correct = fourier_numerator(scalar_points, 1, phases)
+    wrong = fourier_numerator(scalar_points, 1, phases, tensor_power_coefficients=True)
+    need(correct == (0, 0) and wrong == (128, 0)
+         and len(antisymmetrize(scalar_points, affine)) == 24,
+         'Tensoring an external Fourier coefficient creates a false residue witness')
+    wrong_normalized = Fraction(wrong[0], 128**len(scalar_points))
+
+    return {
+        'method': 'literal affine permutations, all128 input-phase Fourier terms, signed tuple images',
+        'arithmetic': 'integer Gaussian pairs and exact rational normalization; no floating point',
+        'affine_maps': len(affine), 'phase_polynomials': len(phases),
+        'native_group_elements': len(affine)*len(phases),
+        'affine_composition_sign_checks': len(affine)**2,
+        'phase_pullback_checks': len(affine)*len(phases),
+        'projector_normalization': '1/128',
+        'coefficient_order': '(sum_h sign(h)[h]) E_chi; input phases act first',
+        'stabilizers': stabilizers, 'below_threshold_census': below,
+        'weak_composition_phase_checks': composition_cases,
+        'wrong_central_residue_checks': wrong_residue_cases,
+        'accepted_compositions_by_width_and_residue': accepted_by_width,
+        'first_witnesses': witnesses,
+        'controls': {
+            'omitted_sign': no_sign,
+            'omitted_quadratic': {'residue': 3, 'counts': [0, 3, 3, 1],
+                                  'correct_projector': '0', 'wrong_projector': '1',
+                                  'wrong_output_count': 24},
+            'tensor_powered_external_coefficients': {
+                'residue': 1, 'counts': [0, 2, 2, 2], 'correct_projector': '0',
+                'wrong_projector': str(wrong_normalized), 'wrong_output_count': 24}},
+        'scope': 'Independent finite evidence for the written two-axis theorem; no physical supplier or all-n cutoff',
+    }
+
+
+if __name__ == '__main__':
+    import json
+    print(json.dumps(run(), sort_keys=True, indent=2))
diff --git a/research/two-axis-native-cutoff/verify.py b/research/two-axis-native-cutoff/verify.py
new file mode 100644
index 0000000000..6d183d5f6a
--- /dev/null
+++ b/research/two-axis-native-cutoff/verify.py
@@ -0,0 +1,172 @@
+#!/usr/bin/env python3
+"""Exact two-axis minimum-width certificate and separate literal witness replay.
+
+Hiroki KUMAZAKI, with substantial OpenAI Codex assistance. Apache-2.0.
+No predecessor verifier is imported. The all-width argument is in PROOF.md.
+"""
+from collections import Counter
+import hashlib
+import importlib.util
+import itertools
+import json
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+THRESHOLDS = (8, 9, 6, 7)
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def character(counts):
+    """Point order 00,10,01,11; phases are evaluated on input addresses."""
+    a, b, c, d = counts
+    return (sum(counts) % 4, (b+d) % 4, (c+d) % 4, d % 2)
+
+
+def spanning(counts):
+    # Any three distinct points form an affine basis of the two-axis space.
+    return sum(x != 0 for x in counts) >= 3
+
+
+def minimum_formula(chi):
+    r, u1, u2, v = chi
+    candidates = []
+    for z in (v, v+2):
+        a = [(r-u1-u2+z) % 4, (u1-z) % 4, (u2-z) % 4, z]
+        missing = max(0, 3-sum(x != 0 for x in a))
+        cost = sum(a)+4*missing
+        # Realize the displayed cost without changing the residue or character.
+        counts = a[:]
+        for index in [i for i, value in enumerate(a) if value == 0][:missing]:
+            counts[index] = 4
+        need(character(counts) == chi and spanning(counts) and sum(counts) == cost,
+             'Residue-formula witness is a genuine full-span tuple')
+        candidates.append((cost, tuple(counts)))
+    return min(candidates)
+
+
+def compositions(width):
+    for a in range(width+1):
+        for b in range(width-a+1):
+            for c in range(width-a-b+1):
+                yield a, b, c, width-a-b-c
+
+
+def minimum_checks():
+    characters = list(itertools.product(range(4), range(4), range(4), range(2)))
+    # A positive count can be reduced by four until it lies in 1..4;
+    # this preserves both character and support. Thus this is a complete
+    # minimum census, not a guessed maximum-width search cutoff.
+    census = {}
+    for counts in itertools.product(range(5), repeat=4):
+        if spanning(counts):
+            chi = character(counts)
+            candidate = (sum(counts), counts)
+            if chi not in census or candidate < census[chi]:
+                census[chi] = candidate
+    need(set(census) == set(characters), 'All 128 phase characters occur')
+    minima = {}
+    histograms = []
+    for chi in characters:
+        cost, witness = minimum_formula(chi)
+        need(cost == census[chi][0], 'Formula matches independent bounded count census')
+        minima[chi] = cost
+    for r in range(4):
+        histogram = Counter(value for chi, value in minima.items() if chi[0] == r)
+        need(max(histogram) == THRESHOLDS[r] and sum(histogram.values()) == 32,
+             'Exact worst character in each central residue')
+        histograms.append({'residue': r, 'first_faithful_width': THRESHOLDS[r],
+                           'minimum_width_histogram': {str(k): histogram[k] for k in sorted(histogram)},
+                           'attaining_character': [r, 0, 0, 0],
+                           'attaining_minimum': minima[r, 0, 0, 0]})
+        need(minima[r, 0, 0, 0] == THRESHOLDS[r], 'Zero nonconstant character attains worst case')
+    fixed_widths = []
+    for width in range(1, 14):
+        actual = {character(counts) for counts in compositions(width) if spanning(counts)}
+        predicted = {chi for chi, lower in minima.items() if chi[0] == width % 4 and lower <= width}
+        need(actual == predicted, 'Exact fixed-width realization agrees with minimum and four-zero padding')
+        fixed_widths.append({'width': width, 'full_span_characters': len(actual),
+                            'central_quotient_injective': len(actual) == 32})
+    need([row['full_span_characters'] for row in fixed_widths[:9]] == [0, 0, 4, 13, 28, 32, 32, 32, 32],
+         'Small-width boundary counts')
+    need(all(row['central_quotient_injective'] for row in fixed_widths[5:])
+         and not fixed_widths[4]['central_quotient_injective'], 'First uniform threshold is six')
+    # Affine span is essential: one zero point realizes the late residue-one
+    # phase character, but cannot distinguish affine coefficient vectors.
+    need(character((1, 0, 0, 0)) == (1, 0, 0, 0)
+         and not spanning((1, 0, 0, 0)) and minima[1, 0, 0, 0] == 9,
+         'Phase realization alone is not a kernel certificate')
+    return {'phase_character_count': len(characters), 'count_normal_forms': 5**4,
+            'formula_matches_complete_minimum_census': True,
+            'per_residue': histograms, 'fixed_width_corroboration': fixed_widths,
+            'uniform_cutoff': 6, 'complete_four_width_window': [6, 7, 8, 9],
+            'phase_only_false_positive_width': 1}
+
+
+def test_set_checks():
+    def detects(widths):
+        return all(any(f % 4 == r and f >= THRESHOLDS[r] for f in widths) for r in range(4))
+    need(detects([6, 7, 8, 9]) and detects([8, 9, 10, 11]), 'Both sharp and inherited windows suffice')
+    need(not detects(range(1, 9)), 'No set below width nine can suffice')
+    # The four explicit sign-projectors provide the necessity witnesses.
+    checked = 0
+    for size in range(4):
+        for widths in itertools.combinations(range(1, 14), size):
+            need(not detects(widths), 'At least four distinct residues are required')
+            checked += 1
+    return {'test_sets_with_at_most_three_widths_checked': checked,
+            'first_sufficient_consecutive_window_start': 6,
+            'all_widths_one_through_eight_fail': True,
+            'criterion': 'For each r, include an f congruent to r modulo 4 with f >= (8,9,6,7)[r]',
+            'fixed_external_coefficients_required': True}
+
+
+def authenticate():
+    manifest = json.loads((HERE/'SOURCES.json').read_text())
+    paths = []
+    for row in manifest['files']:
+        if row['usage'] == 'input':
+            need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'],
+                 'Pinned input bytes: '+row['path'])
+            paths.append(row['path'])
+    return paths
+
+
+def run():
+    sources = authenticate()
+    spec = importlib.util.spec_from_file_location('two_axis_literal', HERE/'literal.py')
+    module = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(module)
+    return {'status': 'PASS_SHARP_TWO_AXIS_NATIVE_CUTOFF',
+            'scope': 'Two-axis affine/quadratic Gaussian monomials over Q(i) or C; group-algebra kernel modulo central phase',
+            'authenticated_inputs': sources,
+            'minimum_widths': minimum_checks(),
+            'test_set_criterion': test_set_checks(),
+            'literal_obstructions': module.run(),
+            'proof': 'PROOF.md supplies the all-width necessity/sufficiency and analytic upper-bound argument',
+            'general_n_cutoff_claimed': False, 'physical_supplier_claimed': False,
+            'selected_frontier_changed': False}
+
+
+def main():
+    need(sys.argv[1:] in ([], ['--write']), 'Use no arguments or --write')
+    result = run()
+    encoded = json.dumps(result, sort_keys=True, indent=2)+'\n'
+    receipt = HERE/'RESULT.json'
+    if sys.argv[1:]:
+        need(not receipt.exists(), 'Refuse to overwrite receipt')
+        receipt.write_text(encoded)
+    else:
+        need(receipt.read_text() == encoded, 'Exact deterministic receipt differs')
+    print(result['status'])
+    print(json.dumps({'cutoff': 6, 'residue_thresholds': list(THRESHOLDS),
+                      'minimal_window': [6, 7, 8, 9], 'late_witness_first_width': 9}))
+
+
+if __name__ == '__main__':
+    main()