diff --git a/docs/research/native-tensor-cutoff.md b/docs/research/native-tensor-cutoff.md
new file mode 100644
index 0000000000..c04caeb0f9
--- /dev/null
+++ b/docs/research/native-tensor-cutoff.md
@@ -0,0 +1,53 @@
+# Certify identities with actual affine and phase relations
+
+Use [native-tensor-cutoff](../../research/native-tensor-cutoff/README.md) when
+every payload operator is a binary affine permutation with a quadratic
+Gaussian phase. This is the fixed monomial recipe grammar in [PR #2250](https://github.com/CrocSwap/integer-mult-bounds/pull/2250).
+The checker respects actual inverse, finite-order, commutation and phase
+relations. It checks all dirty inputs and all returned roles.
+
+The proof gives a finite criterion for a fixed n-axis program: equality at
+widths **2n+4 through 2n+7** is equivalent to equality at every positive
+width. The tool checks canonical native coefficients and constructs a short
+basis witness on failure. It does not materialize those four tensor spaces.
+The number of stored terms can still grow exponentially.
+
+```sh
+python3 -I -B research/native-tensor-cutoff/native_identity.py \
+  /path/to/problem.json --output /tmp/native-certificate.json
+python3 -I -B research/native-tensor-cutoff/check_certificate.py \
+  /path/to/problem.json /tmp/native-certificate.json
+```
+
+Copy the input format from the package's source-conjugation example. Bind
+each generator to exact source recipe bytes. Use a second complete program
+as the reference. Keep a borrowed role's identity output when it must return
+its dirt. Save both input and certificate files with the source pins.
+
+The actual nine-axis example is a relation-dependent identity. Its deliberate
+constant-phase error passes even widths but fails the separate checker's
+width-25 witness. Another nine-axis example vanishes at every width below 9.
+Small-matrix tests alone therefore do not establish the all-width claim.
+
+Keep three boundaries explicit:
+
+- Scalars stay outside tensor powers. A recipe phase c contributes f*c at
+  width f. A scalar multiplying the complete register operation contributes
+  that same scalar, not its f-th power.
+- The four-width criterion requires a single fixed program and fixed scalar
+  coefficients. Arbitrary width-dependent choices need the proof's separate
+  phase-residue statement.
+- This grammar excludes Hadamard gates, rectangular operators, nonlinear
+  leaves and external aliases. Physical costs, precision, tape movement and
+  supplier admission need their own proofs.
+
+For independent operator symbols, use the
+[universal dirty-circuit guide](universal-dirty-circuit-guide.md). Its smaller
+grammar supports compact polynomial-size certificates. Named inverses alone
+have their own [inverse certificate package](../../research/inverse-dirty-certificates/README.md).
+Choose the grammar that the actual source satisfies. A failed independent
+operator check does not refute an identity which uses native relations.
+
+Prepared by Ali Romman with substantial OpenAI Codex assistance. The package
+retains the source and classical mathematical attribution. This is an
+author-checked research interface, not a selected-frontier update.
diff --git a/docs/research/universal-dirty-circuit-guide.md b/docs/research/universal-dirty-circuit-guide.md
index 0989fd6e51..ccfd2ca5b8 100644
--- a/docs/research/universal-dirty-circuit-guide.md
+++ b/docs/research/universal-dirty-circuit-guide.md
@@ -74,6 +74,12 @@ not tensorize sums or admit physical implementations. See the
 
 For free-group native programs, use the existing
 [free-word tensor audit](../../research/free-word-tensor-lift-audit/README.md).
+For fixed binary affine maps with quadratic Gaussian phases, the
+[native tensor-cutoff guide](native-tensor-cutoff.md) supplies a relation-aware
+endpoint checker and a four-width completeness theorem. It preserves actual
+global phases and dirty roles; nonmonomial Cliffords and physical admission
+remain outside that interface.
+
 For rectangular scratch and one-sided invariants, the existing
 [dirty-phase audit](../../research/universal-dirty-phase-identities/README.md)
 has a different contract. Nonlinear leaves, aliasing, rounding, native frames,
diff --git a/research/native-tensor-cutoff/MUTATIONS.json b/research/native-tensor-cutoff/MUTATIONS.json
new file mode 100644
index 0000000000..1692454bb7
--- /dev/null
+++ b/research/native-tensor-cutoff/MUTATIONS.json
@@ -0,0 +1,53 @@
+{
+  "status": "PASS_NATIVE_CUTOFF_MUTATIONS",
+  "cases": [
+    {
+      "mutation": "one-copy-phase-repair",
+      "optimized": false,
+      "exit_code": 1,
+      "rejection": "complete phase-character statistics"
+    },
+    {
+      "mutation": "one-copy-phase-repair",
+      "optimized": true,
+      "exit_code": 1,
+      "rejection": "complete phase-character statistics"
+    },
+    {
+      "mutation": "ignore-central-residue",
+      "optimized": false,
+      "exit_code": 1,
+      "rejection": "complete phase-character statistics"
+    },
+    {
+      "mutation": "ignore-central-residue",
+      "optimized": true,
+      "exit_code": 1,
+      "rejection": "complete phase-character statistics"
+    },
+    {
+      "mutation": "drop-native-constant",
+      "optimized": false,
+      "exit_code": 1,
+      "rejection": "separate composition formulas"
+    },
+    {
+      "mutation": "drop-native-constant",
+      "optimized": true,
+      "exit_code": 1,
+      "rejection": "separate composition formulas"
+    },
+    {
+      "mutation": "omit-last-dirty-return",
+      "optimized": false,
+      "exit_code": 1,
+      "rejection": "negative control was accepted"
+    },
+    {
+      "mutation": "omit-last-dirty-return",
+      "optimized": true,
+      "exit_code": 1,
+      "rejection": "negative control was accepted"
+    }
+  ]
+}
diff --git a/research/native-tensor-cutoff/PROOF.md b/research/native-tensor-cutoff/PROOF.md
new file mode 100644
index 0000000000..2d92f17cd8
--- /dev/null
+++ b/research/native-tensor-cutoff/PROOF.md
@@ -0,0 +1,380 @@
+# Four widths decide every affine-quadratic native identity
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+
+This is a complete algebraic result for the class below. It does not prove a
+physical native implementation, a cost saving, or a multiplication exponent.
+The group-theoretic and Fourier tools used in the proof are classical.
+
+## 1. Exact class and result
+
+Fix n>=1. Let V have basis e_x, x in F_2^n. The group G_n consists of the maps
+
+    U(A,t,c,a,b) e_x = i^q(x) e_(Ax+t),
+    q(x) = c + sum_j a_j x_j + 2 sum_(j<k) b_jk x_j x_k  (mod 4),
+
+where A is invertible over F_2, t is binary, c and each a_j are in Z/4,
+and each b_jk is in Z/2. The phase is evaluated at the input. This is exactly
+the affine/quadratic Gaussian monomial grammar used by the pinned [PR #2250](https://github.com/CrocSwap/integer-mult-bounds/pull/2250)
+recipe functions. It excludes Hadamard gates and other nonmonomial operators.
+
+The recipe is unique. Its affine part is determined by its action on 0 and
+the n unit vectors. Its phase coefficients are determined by q(0), q(e_j),
+and q(e_j+e_k). Composition and inversion preserve this form: a Boolean
+affine form is a quadratic polynomial modulo four, and twice a product of
+two Boolean affine forms is quadratic modulo four. The two implementations
+use these two different ways to compute the coefficients.
+
+Write rho_f(U)=U^(tensor f). The tensor power acts on payloads; it does not
+tensorize a scalar combination of operators. All external coefficients in
+this proof remain fixed scalars. Let
+
+    P = sum_(U in G_n) alpha_U [U] in C[G_n].
+
+Only finitely many coefficients need be stored. Put F=2n+4.
+
+**Theorem.** The following statements are equivalent:
+
+1. Every coefficient alpha_U is zero.
+2. rho_f(P)=0 for every positive integer f.
+3. rho_f(P)=0 at the four widths F,F+1,F+2,F+3.
+
+If P is nonzero, the proof constructs f in this four-width window and two
+basis tuples x,y in (F_2^n)^f such that the (y,x) entry of rho_f(P) is nonzero.
+The two tuples need O(n^2) bits. This is a compressed basis address, not a
+polynomial bound on the dimension 2^(nf) of the tensor space.
+
+For Gaussian rational coefficients and s stored nonzero group terms, the
+witness construction uses O(s n^2) exact Gaussian scalar operations for its
+Fourier choices, plus polynomial binary linear algebra and bit operations.
+This count starts from the expanded residual. Expansion of a register circuit
+can require exponentially many terms. There is no polynomial-time claim for
+the complete circuit checker.
+
+The theorem applies entry by entry to a complete matrix over C[G_n]. Thus it
+applies to scalar register programs using ADD, SCALE, SWAP, unary APPLY and
+`v_dst += alpha U v_src`, including a self query. The compiler starts every
+role as a separate arbitrary input and checks every returned role. A reference
+program must state any discarded or zero output. A borrowed role is restored
+only when the reference contains its identity endpoint.
+
+The four-width equivalence requires the same recipes, scalar coefficients
+and program at all four widths. It does not apply to an arbitrary program
+which changes with f. The per-residue statement in Section 5 is more general.
+
+## 2. A short tuple realizes every phase character
+
+The diagonal phase subgroup D has coefficient group
+
+    (Z/4)^(n+1) x (Z/2)^(n(n-1)/2).
+
+Write a character of D as (r,u,v), with r,u_j in Z/4 and v_jk in Z/2. Its
+value on a phase polynomial q is
+
+    chi(q) = i^(r c + sum_j u_j a_j + 2 sum_(j<k) v_jk b_jk).
+
+We construct an ordered tuple X of points which has affine span F_2^n and
+has exactly these phase statistics:
+
+    |X| = r (mod 4),
+    sum_(x in X) x_j = u_j (mod 4),
+    sum_(x in X) x_j x_k = v_jk (mod 2), j<k.
+
+Start X with 0,e_1,...,e_n. This fixes the affine span. Form the symmetric
+binary matrix M with diagonal u_j mod 2 and off-diagonal entries v_jk.
+The starting tuple has Gram matrix I, so factor M+I as YY^T with at most
+n+1 columns. Append those binary columns as points of X.
+
+For completeness, such a factor always exists. Symmetric elimination splits
+a binary form into nonsingular one-dimensional blocks, hyperbolic pairs,
+and its radical. If there are a one-dimensional blocks and b hyperbolic
+pairs, embed the first blocks on a separate orthonormal coordinate set.
+Embed the alternating 2b-dimensional part in the even-weight subspace of
+F_2^(2b+1). That subspace is nonsingular: its orthogonal complement is the
+all-ones vector, which has odd weight and is outside the subspace. A
+symplectic basis gives the required hyperbolic pairs. Undo the original
+congruence. The number of columns is a+2b+1 if b>0, or a otherwise, hence
+at most rank(M+I)+1<=n+1. This is a sufficient form of the classical binary
+symmetric factorization result; no optimal factor width is claimed here.
+
+The current Gram matrix is now M. Let w_j be the current coordinate count
+modulo four. Then u_j-w_j is even. Define the single binary vector
+
+    z_j = (u_j-w_j)/2 (mod 2).
+
+Append two copies of z if z is nonzero. They correct every coordinate count
+modulo four at once. They change no pair count modulo two. This two-copy
+correction is necessary; Gram parity alone does not determine a Gaussian
+phase character.
+
+The tuple now has length at most
+
+    (n+1) + (n+1) + 2 = 2n+4 = F.
+
+For any prescribed f>=F with f=r mod 4, append zero points until its length
+is f. Zero points change neither coordinate nor pair counts. Their count
+sets the constant-phase character. In particular there is such an f among
+F,F+1,F+2,F+3. The tuple still contains 0 and every unit vector.
+
+This construction is uniform in n and in the character. No group enumeration
+or tensor matrix is needed.
+
+## 3. Separate an arbitrary nonzero residual
+
+Choose a nonzero affine bucket (A,t) of P. Its coefficients are a nonzero
+function alpha(q) on D. Finite Fourier inversion gives a character chi with
+
+    S = sum_q alpha(q) chi(q) != 0.
+
+Construct X for chi by Section 2, and put Y=(Ax+t : x in X), in the same
+order. A term with a different affine map cannot send X to Y, because X
+contains an affine basis. A term in the chosen bucket contributes exactly
+alpha(q) i^(sum_(x in X) q(x))=alpha(q) chi(q). Therefore
+
+    <e_Y, rho_f(P) e_X> = S != 0.
+
+This proves the theorem. It also proves the bound on the witness encoding.
+The proof does not assume that independent free operators represent the
+native symbols; it uses their actual affine and phase relations.
+
+The executable finds chi without enumerating D or its dual. Regard alpha as
+a sparse table on the coefficient coordinates of D. For the first coordinate,
+try each of its two or four characters, collect terms on the remaining
+coordinates, and retain a nonzero table. At least one choice is nonzero:
+otherwise the invertible Fourier matrix for that coordinate would imply that
+the original table was zero. Repeat. The final table is the single nonzero
+number S. Each stage has at most s terms and at most four trials. There are
+1+n+n(n-1)/2 stages. This proves the stated exact scalar-operation bound.
+
+## 4. Four widths are necessary; the widths must grow with n
+
+For each residue r modulo four consider the central phase projector
+
+    C_r = sum_(c=0..3) i^(-r c) [i^c I].
+
+At width f it is 4I if f=r mod 4, and zero otherwise. Any proposed test set
+that misses one residue admits a false all-width identity. Thus no set of
+three widths can replace the four tests for this full group. The theorem is
+optimal in the number of widths, not in the value of the cutoff F.
+
+A second family shows that a fixed small-width test is insufficient even
+when scalar phases are treated correctly. Let S_j have phase x_j and let
+Z_j=S_j^2. Let CZ_jk have phase 2x_jx_k. Form the matrix polynomial
+
+    P_n = product_j ((I-i S_j)(I-Z_j)/4)
+          product_(j<k) ((I+CZ_jk)/2),
+
+with all products interpreted termwise at width f. These diagonal operators
+commute. On a basis tuple X, the first factors select coordinate counts
+equal to one modulo four, and the second factors select even pair counts.
+If the entry is nonzero, the n-by-f binary matrix with columns X satisfies
+XX^T=I_n. Hence f>=n. Thus rho_f(P_n)=0 at every positive f<n.
+At f=n, the tuple (e_1,...,e_n) has eigenvalue one. Zero padding gives a
+witness at any larger width too.
+
+The program has O(n^2) instructions, but its expanded phase support can be
+exponential. The nine-axis example is invisible at all widths 1 through 8.
+The independent checker executes its basis witness without expanding that
+support. This example is an algebraic diagnostic; it is not a paid native
+supplier or a proof that its self queries have an admitted physical cost.
+
+## 5. Exact stabilization within a phase residue
+
+Fix r in Z/4. Combine global phases in each affine/nonconstant-phase class:
+
+    beta_(A,t,a,b) = sum_(c=0..3) alpha_(A,t,c,a,b) i^(r c).
+
+For every f>=F with f=r mod 4, rho_f(P)=0 if and only if every beta is zero.
+The forward implication follows by applying the Fourier argument to (a,b)
+only and using Section 2 with the prescribed constant character r. The
+reverse implication follows directly by collecting the same tensor maps.
+
+Thus the kernel of tensor evaluation, after the scalar relation [iI]=i^r,
+has stabilized by F. This is a quantitative replacement, for this monomial
+subgroup, of the older general finite-alphabet separation bound
+[f>=|G/Z|-1](https://github.com/CrocSwap/integer-mult-bounds/blob/7c472563474e60185e6ca101a17622133d047e56/research/two-full-retained-helper-ceiling/science/PROOF.md). It does not assert this linear cutoff for the full Clifford group.
+For n=9 the stabilized threshold is 22; the four all-width tests are 22..25.
+For n=17 they are 38..41. These are sufficient bounds, not minimum thresholds.
+
+This statement permits any scalar coefficients at one specified f. To infer
+an identity for all f from four tests, the single fixed P premise in Section 1
+must still hold.
+
+## 6. A computational boundary even for reversible dirty programs
+
+Consider five-role programs which use only the commuting sign generators
+Z_j e_x=(-1)^x_j e_x, rational ADD and QUERY between distinct roles, unary
+APPLY(Z_j), and SWAP. Every instruction is invertible. All five roles start
+with arbitrary independent inputs. With n unbounded and rational coefficients
+in ordinary binary notation, equality of complete endpoints for this class
+is coNP-complete. No clean scratch or zero-return role is needed.
+
+For membership, every tensor basis tuple supplies only the n signs
+z_j=(-1)^(sum x_j). All sign tuples already occur at width one. For a chosen
+sign tuple, the complete five-by-five scalar endpoint can be evaluated in
+polynomial time and exact bit complexity. The product of all instruction
+denominators is a common denominator for the final entries. For L instructions,
+the numerator bit lengths are bounded by the total coefficient bit length
+plus O(L log 5). A sign tuple and a differing matrix entry therefore
+certify inequality. This argument concerns the unbounded mathematical class;
+the implementation has the separate finite input limits in README.md.
+
+For hardness, we use Barrington's classical width-five permutation program
+construction. The following explicit version is in `reversible_cnf.py`.
+Represent a permutation by its five images, and let composition p q mean
+apply q first. Set
+
+    A = (1,2,3,4,0),
+    B = (1,3,0,4,2),
+    C = B^-1 A^-1 B A = (4,3,1,0,2).
+
+Each of A, B and C is a five-cycle. A Boolean literal gives a single branch
+instruction which is the identity when the literal is false and a chosen
+five-cycle when it is true. Negation inverts the word and then appends the
+target cycle. For an AND, choose a permutation F with F C F^-1 equal to
+the target cycle. Compile the two children to F A F^-1 and F B F^-1.
+The chronological word P,Q,P^-1,Q^-1 is identity if either child is false,
+and the target cycle if both are true. OR follows by De Morgan's law.
+These rules prove the Boolean program property by induction. The conjugator
+exists because both C and the target are five-cycles: map C^k(0) to the
+target's k-th iterate of 0.
+
+A clause with at most three literals needs at most 25 branch instructions.
+Combine m clauses with a balanced AND tree. Each leaf is copied at most
+2^ceil(log2(m)) times, so the word has at most 50*max(1,m)^2 instructions.
+An empty conjunction is true and an empty clause is false. The resulting
+word is A if the three-literal CNF formula is true, and identity otherwise.
+
+It remains to implement each branch with the permitted dirty operations.
+A permutation of five roles needs at most four swaps. For a branch which
+selects permutation a at bit zero and b at bit one, first perform a. Then
+perform the swaps for b a^-1, each controlled by the native sign Z_j. A
+controlled swap on arbitrary dirty inputs x,y is the five-step word
+
+    x -= y
+    y += x/2
+    y -= Z_j x/2
+    x  = Z_j x
+    x += y
+
+On sign +1 this is identity. On sign -1 it swaps x and y. Direct substitution
+proves both claims for all x,y. Each step is a distinct-role shear or an
+invertible unary map. Thus each branch needs at most 4+4*5=24 instructions,
+and the complete reduction needs at most 1200*max(1,m)^2 instructions. Its
+only nonintegral coefficients are 1/2 and -1/2.
+
+Every truth assignment occurs as one tensor basis address at width one.
+On that address the full five-role endpoint is the identity if the formula
+is false and the nonidentity permutation A if it is true. The program equals
+the empty reference on all dirty inputs at all positive widths exactly when
+the CNF formula is unsatisfiable. This is a polynomial reduction from
+three-literal CNF unsatisfiability and proves coNP-hardness.
+
+The construction is an algebraic statement. It does not assign physical
+cost to a native query or admit a paid supplier. Barrington retains credit
+for the permutation program theorem; the package makes its use in this exact
+native dirty grammar explicit. The checker reports a resource limit as no
+decision, not as identity. No general polynomial runtime bound is claimed.
+
+## 7. Source binding and verification boundary
+
+The retained source files and hashes are in [SOURCES.json](SOURCES.json)
+and [SOURCE-PINS.json](SOURCE-PINS.json). [PR #2250](https://github.com/CrocSwap/integer-mult-bounds/pull/2250) evaluates
+the same input phase, affine matrix rows and offset. Its quadratic rows use
+only the strict upper entries; the adapter preserves that convention. Its
+tensor phase includes f times the constant phase. The source check covers
+all 512 one-column addresses of the retained nine-axis event8814 recipe,
+its inverse and a native Pauli-conjugation identity, plus tensor phase probes.
+
+For the actual recipe G=(A,t,q), take Z_v e_x=(-1)^(v.x)e_x. Then
+
+    G Z_v G^-1 = (-1)^(v.A^-1.t) Z_(A^-T.v).
+
+The package chooses v so that the constant sign is negative. Its complete
+two-role circuit adds the conjugated source to a dirty target, restores the
+source, and subtracts the stated native right side. The checker proves this
+endpoint is identity at all positive widths. Removing the constant phase
+from the right side passes all even widths but fails at the generated odd
+width witness. This is an application of actual native relations, not a
+new discovery of Pauli conjugation.
+
+The recipe fixture was supplied by the predecessor packet investigation.
+This package authenticates those bytes and the scalar recipe convention;
+it does not reproduce the full dispatcher-to-chart chain, production packet
+order, recursive child, fixed-tape implementation, precision, hosting or
+complete paid invoice. The full multiplication theorem and selected kappa
+are unchanged.
+
+The certificate checker imports neither the producer nor its group algebra.
+For a positive claim it rebuilds the complete endpoint with direct Boolean
+polynomial substitution, whereas the producer interpolates coefficients at
+0, unit vectors and pairs. For a negative claim it runs the original program
+on the declared tensor basis input, with literal affine maps, phases and
+inverse actions. Both share exact Gaussian rational arithmetic, Python and
+the declared instruction semantics. This is separate implementation evidence,
+not an independent human review or a proof-assistant kernel.
+
+## 8. Prior work and open next questions
+
+Binary symmetric factorization is classical; see Abraham Lempel,
+[Matrix Factorization over GF(2) and Trace-Orthogonal Bases of GF(2^n), 1975](https://doi.org/10.1137/0204014).
+The proof above includes the sufficient factorization argument it uses.
+Finite Fourier inversion is classical. General tensor generation by a
+faithful finite-group representation is the Burnside-Brauer theorem; see
+Benjamin Steinberg's [account and extension, 2014](https://arxiv.org/abs/1409.7632).
+The coNP statement uses the classical NP-completeness of Boolean SAT; see
+Stephen Cook's [The Complexity of Theorem-Proving Procedures, 1971](https://www.cs.toronto.edu/~sacook/homepage/1971.pdf).
+Its reversible reduction uses David A. Mix Barrington's
+[Bounded-Width Polynomial-Size Branching Programs Recognize Exactly Those Languages in NC1, 1989](https://people.cs.umass.edu/~barring/publications/bwbp.pdf),
+[journal record](https://doi.org/10.1016/0022-0000(89)90037-8).
+Section 6 gives the permutation construction and its exact dirty-register
+implementation explicitly.
+
+The [binary-stream faithfulness proof](https://github.com/CrocSwap/integer-mult-bounds/blob/7c472563474e60185e6ca101a17622133d047e56/research/binary-stream-faithfulness/PROOF.md)
+prepared for @ywz65 in
+[PR #2599](https://github.com/CrocSwap/integer-mult-bounds/pull/2599)
+already uses the affine basis 0,e_1,...,e_n to recover
+complete dirty-register coefficients for the binary permutation action over
+F_2, with a sharp width boundary for that action. That result keeps its
+credit. The Gaussian phase subgroup here has additional Fourier characters
+and four central residues. An affine basis alone does not separate them.
+
+Jose Manuel (@jmbarrancoml) also constructs selected phase-character sectors
+at a common tensor length in
+[Discussion #2106](https://github.com/CrocSwap/integer-mult-bounds/discussions/2106).
+That construction uses pair vectors and repeated unit vectors for a specified
+three-axis invariant sector. This package does not claim phase-character
+realization as a new idea. Sections 2 and 3 give a linear width bound for every
+character, preserve an affine basis, and separate every native residual.
+
+The repository's [PR #4928](https://github.com/CrocSwap/integer-mult-bounds/pull/4928) and [PR #4978](https://github.com/CrocSwap/integer-mult-bounds/pull/4978) already use finite-alphabet tensor
+separation, including the projective |G/Z|-1 bound. Chris R (@Clear1nsight) and
+the retained source authors keep that credit. [PR #5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235) by zxv and [PR #5262](https://github.com/CrocSwap/integer-mult-bounds/pull/5262) by
+Krzysztof Wójt (@krzysztofwojt) supply the related complete dirty-register certificate
+interfaces for independent operators and true named inverses. Those methods
+do not impose the native finite-order and phase relations used here.
+Jose Manuel (@jmbarrancoml) supplied [PR #2250](https://github.com/CrocSwap/integer-mult-bounds/pull/2250)'s recipe implementation, with
+Douglas Colkitt's compact construction and the retained notices. JoyboyBrian
+and Cinna Davis supply the event fixture/caller lineage recorded in the source
+manifest. No general Fourier, Gram, tensor generation, Pauli conjugation or
+PIT theorem is claimed as new.
+
+The contribution is the explicit four-width native criterion, constructive
+short basis witness, residue stabilization bound, executable complete-endpoint
+interface, matching test-count and growing-width obstructions, and an explicit
+reversible complexity reduction for this exact source grammar. No global
+literature priority is claimed.
+
+Open next questions:
+
+1. Determine the least stabilized width for G_n. The projector lower bound
+   and F=2n+4 leave a gap. Start with exact small-n phase-character realizations
+   with an affine-span constraint; a minimum for one character is not the
+   complete representation threshold.
+2. Extend a quantitative witness theorem to nonmonomial native Cliffords.
+   The affine-bucket isolation argument does not apply to Hadamard operators.
+   Start with a specified finite Clifford group and its projective character
+   sectors. Keep that hypothesis separate from this proof.
+3. Add a source-bound adapter for another complete monomial register word.
+   Preserve every dirty input, global phase, source order and scalar placement.
+   Physical realization and its full invoice must still be supplied separately.
diff --git a/research/native-tensor-cutoff/README.md b/research/native-tensor-cutoff/README.md
new file mode 100644
index 0000000000..91ae9eadd8
--- /dev/null
+++ b/research/native-tensor-cutoff/README.md
@@ -0,0 +1,169 @@
+# Complete native identities from four tensor widths
+
+For an n-axis binary affine map with a quadratic Gaussian phase, a fixed
+scalar register identity holds at **every positive tensor width if and only
+if it holds at widths 2n+4, 2n+5, 2n+6 and 2n+7**. The full map includes every
+dirty input and every returned role. Four widths are necessary for this full
+family: three widths always miss a global-phase residue class.
+
+The [proof](PROOF.md) gives a constructive basis witness for every false
+identity, encoded in O(n^2) bits. It also proves that phase-residue kernels
+stabilize by width 2n+4. For this monomial group, this replaces the general
+projective-alphabet bound `|G/Z|-1` used in the retained tensor-separation
+argument. It does not give this cutoff for nonmonomial Cliffords.
+
+This is an enabling proof and reusable exact checker. It does **not** change
+the complete kappa calculation. Physical placement, cost, precision, stock,
+compiler admission and the remaining selected theorem assumptions stay open.
+The selected conditional value at the base is `60403/20000000`.
+
+## Use the checker
+
+Python 3.12 or later is sufficient. There are no third-party dependencies.
+From the repository root:
+
+```sh
+python3 -I -B research/native-tensor-cutoff/native_identity.py \
+  research/native-tensor-cutoff/examples/source-conjugation.json \
+  --output /tmp/native-certificate.json
+python3 -I -B research/native-tensor-cutoff/check_certificate.py \
+  research/native-tensor-cutoff/examples/source-conjugation.json \
+  /tmp/native-certificate.json
+```
+
+Expected output:
+
+```text
+IDENTITY_ALL_POSITIVE_WIDTHS
+PASS_NATIVE_IDENTITY_ALL_POSITIVE_WIDTHS
+```
+
+The first tool compares canonical native group coefficients. It does not
+construct the four enormous tensor matrices. If a coefficient remains, it
+uses exact Fourier choices and a binary Gram factorization to construct a
+counterexample in the proved window. The separate checker uses a different
+composition formula for positive certificates and literal tensor basis
+execution for negative certificates. It imports no producer or group-algebra
+code. Both share `exact.py` and the declared program semantics.
+
+The examples include the complete two-role identity for the actual nine-axis
+event8814 recipe, a missing-global-phase mutation, a nine-axis projector that
+vanishes at **all widths 1 through 8**, and two CNF reductions. The compact
+nine-axis projector witness can be checked directly:
+
+```sh
+python3 -I -B research/native-tensor-cutoff/check_certificate.py \
+  research/native-tensor-cutoff/examples/late-projector-9.json \
+  research/native-tensor-cutoff/examples/late-projector-9.certificate.json
+```
+
+It prints `PASS_NATIVE_TENSOR_COUNTEREXAMPLE`. The witness has width 22 and
+discrepancy one. Its first possible nonzero width is 9, by the written rank
+argument. The generic producer need not expand this large projector to check
+the supplied witness.
+
+## Input contract
+
+A problem has `axes`, `roles`, `generators`, `program` and `reference` fields.
+Each generator uses the source recipe fields `matrix_rows`, `offset`,
+`phase`, `linear_Z4` and `quadratic_rows`. The affine matrix must be invertible.
+Quadratic rows use the strict upper entries, as in the pinned source. The
+phase is evaluated at the input coordinate. A generator's constant phase
+is multiplied by the tensor width; an external scalar coefficient is not.
+
+Instructions are:
+
+| op | Required operands | Meaning |
+| --- | --- | --- |
+| `add` | `src`, `dst` | `v_dst += coefficient * v_src` |
+| `query` | `src`, `dst`, `generator` | Add the generator image of the source |
+| `apply` | `dst`, `generator` | Replace the destination by its generator image |
+| `scale` | `dst` | Multiply the destination by `coefficient` |
+| `swap` | `src`, `dst` | Exchange the roles |
+
+Coefficients default to one. They are integers, explicit rational strings,
+or `[real,imaginary]` pairs of such values. Floats and exponent syntax are
+rejected. `apply` and `query` accept a Boolean `inverse` flag. It denotes the
+actual inverse of that generator. Source and destination can coincide.
+The reference is a second program over the same inputs and generators.
+
+All roles start as arbitrary independent inputs. To restore a borrowed role,
+retain its identity endpoint in the reference. Explicit zero outputs are
+allowed, but do not count as restored dirty inputs. External aliases, changing
+recipes or coefficients across widths, nonlinear leaves, Hadamard operations,
+and rectangular types require a different contract.
+
+The implementation accepts 1..256 axes and 1..4096 roles. The theorem has no
+such finite limits. Both CLIs have `--max-terms`, with a default of 100000
+stored terms per program state. A resource failure is **no decision**. Sparse
+expansion can be exponential. The proof shows that endpoint equality is
+coNP-complete even with five arbitrary dirty roles, reversible instructions,
+and commuting native sign generators. It uses Barrington's classical
+permutation program construction and an explicit five-step controlled swap.
+No clean scratch or erase is needed. It does not claim a fast general solver.
+
+## Evidence
+
+The [receipt](RESULT.json) is from the complete exact replay on macOS
+with CPython 3.12.14. Normal and optimized isolated runs have the same output:
+
+```sh
+python3 -I -W error -B research/native-tensor-cutoff/verify.py
+python3 -I -O -W error -B research/native-tensor-cutoff/verify.py
+python3 -I -B research/native-tensor-cutoff/audit_mutations.py
+python3 -B scripts/research_package.py --package research/native-tensor-cutoff
+```
+
+The replay checks all 33,866 symmetric binary matrices through dimension
+five; all 2,192 phase characters through three axes; 100 larger cases through
+73 axes; 1,152 native composition pairs and 19,328 literal native points;
+120 complete circuits with 11,760 dirty-input basis checks; 4,444 complete
+below-rank projector cases; 80 CNF formulas on 992 assignments; 480 reversible
+branch pairs on 4,800 dirty basis columns; 120 full CNF circuit columns; five
+committed examples; and 37 rejection controls. The actual source check covers all 512
+one-column addresses and six tensor phase probes. The phase mutation is
+invisible in 512 even-width cases and fails at the generated width-25 witness.
+
+The [mutation receipt](MUTATIONS.json) records four changes to mathematical
+code in private package copies. Every change must fail at its stated semantic
+check in both normal and optimized Python. These eight failures check the
+two-copy phase repair, constant-phase residue, native composition constant,
+and final dirty return. The original package is not changed by the audit.
+
+Finite checks corroborate the written uniform proof; they do not replace it.
+The tools and proof are author-checked with substantial OpenAI Codex assistance.
+No independent human or proof-kernel acceptance is claimed. No selected cold
+replay, full native supplier, production packet, Lean or Docker run is included.
+
+## Sources and credit
+
+Base: canonical main `7c472563474e60185e6ca101a17622133d047e56`, priority
+revision 7. [SOURCES.json](SOURCES.json) pins historical provenance.
+[SOURCE-PINS.json](SOURCE-PINS.json) authenticates the six byte-identical
+local source exports used by direct replay. No network or Git is needed by
+the standalone verifier. The source fixture is the predecessor's supplied
+event8814 recipe; the complete dispatcher/cover chain is not reproduced.
+
+Jose Manuel (@jmbarrancoml) supplied [PR #2250](https://github.com/CrocSwap/integer-mult-bounds/pull/2250)'s recipe implementation, with
+Douglas Colkitt's compact construction. JoyboyBrian and Cinna Davis supplied
+the retained event/caller lineage. Chris R (@Clear1nsight)'s [PR #4928](https://github.com/CrocSwap/integer-mult-bounds/pull/4928) and [PR #4978](https://github.com/CrocSwap/integer-mult-bounds/pull/4978)
+retain credit for their finite-alphabet tensor-separation arguments. The
+phase-character sector construction in
+[Discussion #2106](https://github.com/CrocSwap/integer-mult-bounds/discussions/2106)
+also retains Jose Manuel's credit. The
+binary-stream affine-basis argument retains @ywz65's credit and its distinct
+F_2 scalar contract. The
+related independent-operator and inverse certificate interfaces are zxv's
+[PR #5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235) and Krzysztof Wójt (@krzysztofwojt)'s [PR #5262](https://github.com/CrocSwap/integer-mult-bounds/pull/5262). Lempel's binary Gram factorization, finite
+Fourier inversion, Burnside-Brauer tensor generation, Pauli conjugation,
+SAT completeness and Barrington's width-five construction are classical.
+Exact links and distinctions are
+in [PROOF.md](PROOF.md) and [SOURCES.json](SOURCES.json). No global literature
+priority is claimed. The retained license notice is in [source/NOTICE.md](source/NOTICE.md).
+
+## Open next questions
+
+The proof lists three concrete next tasks: determine the least stabilized
+width, extend the quantitative construction to a specified nonmonomial
+Clifford group, or bind another complete native register word. Each requires
+its own evidence. None is a completed physical supplier or a kappa claim.
diff --git a/research/native-tensor-cutoff/RESULT.json b/research/native-tensor-cutoff/RESULT.json
new file mode 100644
index 0000000000..2d22f7e503
--- /dev/null
+++ b/research/native-tensor-cutoff/RESULT.json
@@ -0,0 +1,39 @@
+{
+  "CNF_assignments": 992,
+  "CNF_formulas": 80,
+  "below_rank_projector_basis_cases": 4444,
+  "central_residue_cases": 48,
+  "circuits": 120,
+  "committed_examples": 5,
+  "larger_character_cases": 100,
+  "limits": [
+    "No full Clifford/Hadamard theorem",
+    "Expanded circuit support can be exponential",
+    "No physical supplier, precision, outer admission or new kappa",
+    "No independent human or proof-kernel acceptance"
+  ],
+  "literal_CNF_columns": 120,
+  "literal_dirty_basis_cases": 11760,
+  "literal_native_points": 19328,
+  "literal_reversible_columns": 4800,
+  "native_composition_pairs": 1152,
+  "negative_circuits": 55,
+  "phase_characters": 2192,
+  "positive_circuits": 65,
+  "rejection_controls": 37,
+  "reversible_branch_pairs": 480,
+  "source_binding": {
+    "discrepancy": [
+      "-2",
+      "0"
+    ],
+    "even_width_blind_cases": 512,
+    "failure_width": 25,
+    "source_addresses": 512,
+    "tensor_phase_probes": 6
+  },
+  "sources": 6,
+  "status": "PASS_NATIVE_TENSOR_CUTOFF",
+  "symmetric_Gram_matrices": 33866,
+  "unsatisfiable_formulas": 52
+}
diff --git a/research/native-tensor-cutoff/SOURCE-PINS.json b/research/native-tensor-cutoff/SOURCE-PINS.json
new file mode 100644
index 0000000000..042983ed22
--- /dev/null
+++ b/research/native-tensor-cutoff/SOURCE-PINS.json
@@ -0,0 +1,53 @@
+{
+  "base": "7c472563474e60185e6ca101a17622133d047e56",
+  "files": [
+    {
+      "retained": "source/BOUNDARY.json",
+      "original_path": "research/complex-segment-boundary/BOUNDARY.json",
+      "commit": "7c472563474e60185e6ca101a17622133d047e56",
+      "sha256": "41374b4ecf3169b9a205d340eca97e36969e16d1eaf403afe4b13832b243c8e5",
+      "bytes": 1435,
+      "git_blob": "5b017fcb9bb21105a929466ce83816531dcbcddc"
+    },
+    {
+      "retained": "source/NOTICE.md",
+      "original_path": "research/selected-complex-compact-adapters/NOTICE.md",
+      "commit": "7c472563474e60185e6ca101a17622133d047e56",
+      "sha256": "74a9f03e9ce467c75f5f7cf1b8465d349ea38ef114afad261824c3bcf13da00f",
+      "bytes": 2140,
+      "git_blob": "e82bfef53054bd753ba0aa8a966f84427faa2293"
+    },
+    {
+      "retained": "source/RIGHT-RECIPE.json",
+      "original_path": "research/complex-segment-boundary/RIGHT-RECIPE.json",
+      "commit": "7c472563474e60185e6ca101a17622133d047e56",
+      "sha256": "fe4736e77996c627f024d464626fb58d2181fd595281332e8296b36544393080",
+      "bytes": 309,
+      "git_blob": "1b5473743f8f9981cc20dce2207bf93c3fbaf3ee"
+    },
+    {
+      "retained": "source/compact.py",
+      "original_path": "research/selected-complex-compact-adapters/compact.py",
+      "commit": "7c472563474e60185e6ca101a17622133d047e56",
+      "sha256": "0e1027a60f38c21cfd808c8ce44dcc2423810efdab0e15f02b07f261ad48fc3c",
+      "bytes": 9400,
+      "git_blob": "60bc206c78150f23563a4775800b0dd32025843d"
+    },
+    {
+      "retained": "source/monomial.py",
+      "original_path": "research/selected-complex-compact-adapters/monomial.py",
+      "commit": "7c472563474e60185e6ca101a17622133d047e56",
+      "sha256": "394f9a465ac9148af0c20844d375e4befbef17d92b2fcc840d83419480dd4740",
+      "bytes": 4656,
+      "git_blob": "5fa4494167c4ba668993a2b1c902969518728a4c"
+    },
+    {
+      "retained": "source/streams.py",
+      "original_path": "research/selected-complex-compact-adapters/streams.py",
+      "commit": "7c472563474e60185e6ca101a17622133d047e56",
+      "sha256": "718a582a50aee8f1f04945ed942be1d4162962fe47dbf05c6ff37b7fb8c61257",
+      "bytes": 4369,
+      "git_blob": "61542ce4c9eb51bfc113475b4f98649cb90a853e"
+    }
+  ]
+}
diff --git a/research/native-tensor-cutoff/SOURCES.json b/research/native-tensor-cutoff/SOURCES.json
new file mode 100644
index 0000000000..b3b1d29264
--- /dev/null
+++ b/research/native-tensor-cutoff/SOURCES.json
@@ -0,0 +1,117 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c472563474e60185e6ca101a17622133d047e56",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/complex-segment-boundary/BOUNDARY.json",
+      "usage": "provenance",
+      "git_blob": "5b017fcb9bb21105a929466ce83816531dcbcddc",
+      "sha256": "41374b4ecf3169b9a205d340eca97e36969e16d1eaf403afe4b13832b243c8e5"
+    },
+    {
+      "path": "research/complex-segment-boundary/RIGHT-RECIPE.json",
+      "usage": "provenance",
+      "git_blob": "1b5473743f8f9981cc20dce2207bf93c3fbaf3ee",
+      "sha256": "fe4736e77996c627f024d464626fb58d2181fd595281332e8296b36544393080"
+    },
+    {
+      "path": "research/selected-complex-compact-adapters/NOTICE.md",
+      "usage": "provenance",
+      "git_blob": "e82bfef53054bd753ba0aa8a966f84427faa2293",
+      "sha256": "74a9f03e9ce467c75f5f7cf1b8465d349ea38ef114afad261824c3bcf13da00f"
+    },
+    {
+      "path": "research/selected-complex-compact-adapters/compact.py",
+      "usage": "provenance",
+      "git_blob": "60bc206c78150f23563a4775800b0dd32025843d",
+      "sha256": "0e1027a60f38c21cfd808c8ce44dcc2423810efdab0e15f02b07f261ad48fc3c"
+    },
+    {
+      "path": "research/selected-complex-compact-adapters/monomial.py",
+      "usage": "provenance",
+      "git_blob": "5fa4494167c4ba668993a2b1c902969518728a4c",
+      "sha256": "394f9a465ac9148af0c20844d375e4befbef17d92b2fcc840d83419480dd4740"
+    },
+    {
+      "path": "research/selected-complex-compact-adapters/streams.py",
+      "usage": "provenance",
+      "git_blob": "61542ce4c9eb51bfc113475b4f98649cb90a853e",
+      "sha256": "718a582a50aee8f1f04945ed942be1d4162962fe47dbf05c6ff37b7fb8c61257"
+    }
+  ],
+  "retained_sources": "SOURCE-PINS.json binds the package-local byte-identical copies used by direct replay. No live external input is imported.",
+  "references": [
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2250",
+      "head": "d404b48a1e7b147556b309497d55089c837dddb2",
+      "title": "Execute selected complex compact adapters with sequential repair",
+      "role": "retained source lineage"
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4928",
+      "head": "6df6ed294614423836cbde182fb4368c9c346fe7",
+      "title": "Prove a separated-control ceiling for two FULLs with retained helpers (no new κ)",
+      "role": "related mathematical interface; not imported"
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4978",
+      "head": "db3f8456a3efb425e337337d85dcc43b797888cd",
+      "title": "Bound passive saved-query recovery for the actual coded p2 caller (no new κ)",
+      "role": "related mathematical interface; not imported"
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5235",
+      "head": "48976daa4dce59b4867ef046da72a370e389925d",
+      "title": "Add compact universal certificates for dirty linear circuits (no new κ)",
+      "role": "related mathematical interface; not imported"
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5262",
+      "head": "6f92ccf1e61c4668c8ee687bd1df8b42932b8759",
+      "title": "Add inverse-aware universal certificates for dirty linear circuits (no new κ)",
+      "role": "related mathematical interface; not imported"
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5329",
+      "head": "08456995d5e520a4f9e0501c9b2ea9b03dbae87a",
+      "title": "research: add segment-local PR2250 refinement and nested source replays",
+      "role": "retained source lineage"
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5327",
+      "head": "e95b239ebcbfe6e0a45b4ee89de13115fb5b85a1",
+      "title": "Bind actual FOUR/base data-climb packet to native chart and source owner",
+      "role": "retained source lineage"
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2106",
+      "author": "jmbarrancoml, named in the discussion",
+      "role": "Related phase-character sector realization; not imported. The new bound covers all characters and isolates all affine buckets."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/7c472563474e60185e6ca101a17622133d047e56/research/binary-stream-faithfulness/PROOF.md",
+      "author": "Prepared for ywz65, as stated in the proof",
+      "sha256": "0d82d13bdcca7953a8f1e6647a78fe6008c407795b363af5be7cd1b7ea8ee2a9",
+      "git_blob": "daee560b155a09484e644069272d002f8ae65c82",
+      "role": "Related affine-basis coefficient recovery over F_2; citation only, not imported."
+    }
+  ],
+  "comparison_proof": {
+    "path": "research/two-full-retained-helper-ceiling/science/PROOF.md",
+    "commit": "7c472563474e60185e6ca101a17622133d047e56",
+    "sha256": "63ec5034fb526dc9243de487f97477e51221773f4b7cae21b38df719ba1362c7",
+    "usage": "citation only; Section All-width faithfulness and exact free-control boundary"
+  }
+}
diff --git a/research/native-tensor-cutoff/TASK.json b/research/native-tensor-cutoff/TASK.json
new file mode 100644
index 0000000000..d76d6738ff
--- /dev/null
+++ b/research/native-tensor-cutoff/TASK.json
@@ -0,0 +1,123 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "7c472563474e60185e6ca101a17622133d047e56",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Constructive four-width completeness and phase-residue stabilization for all binary affine/quadratic Gaussian native monomials; complete dirty-register verifier, literal counterexamples, sharp test-count obstruction, and a reversible five-role coNP-completeness reduction.",
+  "scope_change_reason": "The user requested a substantial reusable result. This supplies a written quantified native-interface theorem and executable checker instead of a proof-assistant formalization or another numerical frontier check.",
+  "bottleneck_link": "Native finite-order, phase and commutation relations are absent from the existing independent-operator certificates. A constructive linear tensor cutoff gives a complete algebraic test and bounded actual-native witnesses for this entire source grammar.",
+  "budget_minutes": 180,
+  "stop_rule": "Complete the uniform theorem, independent implementation, actual source binding, adversarial controls, portable replay and focused publication. Do not claim a new supplier or a result for nonmonomial Clifford gates.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; RESULT.json; MUTATIONS.json; five examples; separate Boolean-polynomial and literal tensor checker. Source conventions are checked on all 512 event8814 addresses.",
+  "author": "Ali Romman, with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, source inspection, implementation, verification, documentation and publication. No subagents, independent human review or proof assistant were used.",
+  "open_questions": [
+    {
+      "question": "What is the least stabilized tensor width for this group?",
+      "why_it_matters": "The proved 2n+4 threshold and the rank lower bound leave a quantitative gap.",
+      "first_step": "Solve the phase-character realization problem with an affine-span constraint for small n.",
+      "blocked_by": "A uniform minimum theorem, not just one finite character table."
+    },
+    {
+      "question": "Can a quantitative witness be constructed for nonmonomial Cliffords?",
+      "why_it_matters": "Hadamard gates are outside the current exact native grammar.",
+      "first_step": "Specify one full finite Clifford group and analyze each projective phase sector.",
+      "blocked_by": "Affine-bucket isolation no longer applies."
+    },
+    {
+      "question": "Which further complete native caller can use this interface?",
+      "why_it_matters": "Exact source adapters make the generic algebraic theorem usable in research.",
+      "first_step": "Translate one literal monomial program and every dirty input/output with exact source pins.",
+      "blocked_by": "The source grammar and scalar placement must match; physical costs remain separate."
+    }
+  ],
+  "coordination": {
+    "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5354",
+    "initial_snapshot": {
+      "open_prs": 304,
+      "discussion_records": 4621,
+      "main": "7c472563474e60185e6ca101a17622133d047e56"
+    },
+    "limits": "Complete remote text pagination plus targeted source/related-work reads; not every historical diff or unpublished work.",
+    "submission_snapshot": {
+      "main": "7c472563474e60185e6ca101a17622133d047e56",
+      "open_prs": 316,
+      "discussion_records": 4648,
+      "open_prs_fetched_at": "2026-10-23T19:36:54Z",
+      "discussions_fetched_at": "2026-10-23T19:38:11Z"
+    }
+  }
+}
diff --git a/research/native-tensor-cutoff/VERIFY.json b/research/native-tensor-cutoff/VERIFY.json
new file mode 100644
index 0000000000..dfcc384e53
--- /dev/null
+++ b/research/native-tensor-cutoff/VERIFY.json
@@ -0,0 +1,44 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticate retained sources; exact Gram/character theorem cases, native composition, complete dirty endpoints, actual recipe phase, lower-width projector, CNF reduction, committed certificates and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticate retained sources; exact Gram/character theorem cases, native composition, complete dirty endpoints, actual recipe phase, lower-width projector, CNF reduction, committed certificates and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/audit_mutations.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Four private-copy mathematical mutations must fail at their stated semantic checks in normal and optimized modes."
+    }
+  ]
+}
diff --git a/research/native-tensor-cutoff/audit_mutations.py b/research/native-tensor-cutoff/audit_mutations.py
new file mode 100644
index 0000000000..c78a5c5840
--- /dev/null
+++ b/research/native-tensor-cutoff/audit_mutations.py
@@ -0,0 +1,47 @@
+"""Check that the replay rejects four mathematical changes in private copies."""
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+
+HERE = Path(__file__).resolve().parent
+MUTATIONS = (
+    ('one-copy-phase-repair', 'native.py', 'points.extend((z, z))', 'points.extend((z,))',
+     'complete phase-character statistics'),
+    ('ignore-central-residue', 'native.py', 'f = floor + (c - floor) % 4', 'f = floor',
+     'complete phase-character statistics'),
+    ('drop-native-constant', 'native.py', 'c = phase_function(0) % 4', 'c = 0',
+     'separate composition formulas'),
+    ('omit-last-dirty-return', 'check_certificate.py', 'need(a == b and certificate.get(',
+     'need(a[:-1] == b[:-1] and certificate.get(', 'negative control was accepted'),
+)
+
+
+def main():
+    results = []
+    for name, filename, old, new, message in MUTATIONS:
+        with tempfile.TemporaryDirectory(prefix='native-cutoff-mutation-') as tmp:
+            target = Path(tmp) / 'package'
+            shutil.copytree(HERE, target, ignore=shutil.ignore_patterns('__pycache__'))
+            path = target / filename
+            text = path.read_text()
+            if text.count(old) != 1:
+                raise ValueError('mutation anchor is not unique')
+            path.write_text(text.replace(old, new))
+            for optimized in (False, True):
+                command = [sys.executable, '-I', '-B', '-W', 'error']
+                if optimized:
+                    command.append('-O')
+                command.append(str(target / 'verify.py'))
+                run = subprocess.run(command, capture_output=True, text=True, timeout=120)
+                if run.returncode == 0 or 'ValueError: ' + message not in run.stderr:
+                    raise ValueError('mutation did not fail at its mathematical check: ' + name + '\n' + run.stderr)
+                results.append({'mutation': name, 'optimized': optimized, 'exit_code': run.returncode,
+                                'rejection': message})
+    print(json.dumps({'status': 'PASS_NATIVE_CUTOFF_MUTATIONS', 'cases': results}, indent=2))
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/native-tensor-cutoff/check_certificate.py b/research/native-tensor-cutoff/check_certificate.py
new file mode 100644
index 0000000000..929ccceeff
--- /dev/null
+++ b/research/native-tensor-cutoff/check_certificate.py
@@ -0,0 +1,244 @@
+"""Check certificates without importing the producer or its native algebra."""
+import argparse
+import hashlib
+import json
+from pathlib import Path
+import sys
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+from exact import QI, need, scalar, unit
+
+
+def dot(row, x):
+    return (row & x).bit_count() % 2
+
+
+def image(g, x):
+    return sum(dot(row, x) << i for i, row in enumerate(g[0])) ^ g[1]
+
+
+def exponent(g, x):
+    return (g[2] + sum(g[3][i] for i in range(len(g[0])) if x & (1 << i))
+            + 2 * sum(1 for i in range(len(g[0])) for j in range(i + 1, len(g[0]))
+                      if x & (1 << i) and x & (1 << j) and g[4][i] & (1 << j))) % 4
+
+
+def invert_matrix(rows):
+    size = len(rows)
+    a, b = list(rows), [1 << i for i in range(size)]
+    for col in range(size):
+        choices = [i for i in range(col, size) if a[i] & (1 << col)]
+        need(bool(choices), 'checker: singular matrix')
+        i = choices[0]
+        a[col], a[i], b[col], b[i] = a[i], a[col], b[i], b[col]
+        for row in range(size):
+            if row != col and a[row] & (1 << col):
+                a[row] ^= a[col]
+                b[row] ^= b[col]
+    return tuple(b)
+
+
+def normalize(data, n):
+    need(isinstance(data, dict) and set(data) == {'matrix_rows', 'offset', 'phase', 'linear_Z4', 'quadratic_rows'},
+         'checker: native fields')
+    a, p, q = data['matrix_rows'], data['linear_Z4'], data['quadratic_rows']
+    need(all(isinstance(x, list) and len(x) == n for x in (a, p, q)), 'checker: native dimensions')
+    need(all(type(x) is int and 0 <= x < (1 << n) for x in a + q), 'checker: binary rows')
+    need(all(type(x) is int and 0 <= x < 4 for x in p), 'checker: linear phases')
+    need(type(data['offset']) is int and 0 <= data['offset'] < (1 << n), 'checker: offset')
+    need(type(data['phase']) is int and 0 <= data['phase'] < 4, 'checker: phase')
+    invert_matrix(a)
+    return (tuple(a), data['offset'], data['phase'], tuple(p),
+            tuple(q[i] & ~((1 << (i + 1)) - 1) for i in range(n)))
+
+
+def problem_data(problem):
+    need(isinstance(problem, dict) and set(problem) == {'axes', 'roles', 'generators', 'program', 'reference'},
+         'checker: problem fields')
+    n, r = problem['axes'], problem['roles']
+    need(type(n) is int and 1 <= n <= 256 and type(r) is int and 1 <= r <= 4096,
+         'checker: dimensions')
+    need(isinstance(problem['generators'], dict), 'checker: generator table')
+    gs = {}
+    for name, value in problem['generators'].items():
+        need(isinstance(name, str) and bool(name), 'checker: generator name')
+        gs[name] = normalize(value, n)
+    fields = {'add': {'op', 'src', 'dst', 'coefficient'},
+              'query': {'op', 'src', 'dst', 'coefficient', 'generator', 'inverse'},
+              'apply': {'op', 'dst', 'generator', 'inverse'},
+              'scale': {'op', 'dst', 'coefficient'}, 'swap': {'op', 'src', 'dst'}}
+    for code in (problem['program'], problem['reference']):
+        need(isinstance(code, list), 'checker: instruction list')
+        for ins in code:
+            need(isinstance(ins, dict), 'checker: instruction object')
+            op = ins.get('op')
+            need(isinstance(op, str) and op in fields and set(ins) <= fields[op], 'checker: instruction fields')
+            for key in (('src', 'dst') if op in ('add', 'query', 'swap') else ('dst',)):
+                need(type(ins.get(key)) is int and 0 <= ins[key] < r, 'checker: role')
+            if op in ('apply', 'query'):
+                need(isinstance(ins.get('generator'), str) and ins['generator'] in gs, 'checker: generator')
+                need(type(ins.get('inverse', False)) is bool, 'checker: inverse flag')
+            if 'coefficient' in ins:
+                scalar(ins['coefficient'])
+    return gs
+
+
+def compose(g, h):
+    """Expand affine Boolean forms modulo four, without interpolation."""
+    n = len(g[0])
+    a = []
+    for row in g[0]:
+        out = 0
+        for j in range(n):
+            if row & (1 << j):
+                out ^= h[0][j]
+        a.append(out)
+    constant = h[2] + g[2]
+    linear = list(h[3])
+    quad = [[2 * ((h[4][j] >> k) & 1) for k in range(n)] for j in range(n)]
+    bits = [[(row >> j) & 1 for j in range(n)] for row in h[0]]
+    shifts = [(h[1] >> i) & 1 for i in range(n)]
+    for i in range(n):
+        coefficient, t = g[3][i], shifts[i]
+        constant += coefficient * t
+        for j in range(n):
+            linear[j] += coefficient * (1 - 2 * t) * bits[i][j]
+            for k in range(j + 1, n):
+                quad[j][k] -= 2 * coefficient * bits[i][j] * bits[i][k]
+        for l in range(i + 1, n):
+            if not (g[4][i] >> l & 1):
+                continue
+            u = shifts[l]
+            constant += 2 * t * u
+            for j in range(n):
+                linear[j] += 2 * (t * bits[l][j] + u * bits[i][j] + bits[i][j] * bits[l][j])
+                for k in range(j + 1, n):
+                    quad[j][k] += 2 * (bits[i][j] * bits[l][k] + bits[i][k] * bits[l][j])
+    return (tuple(a), image(g, h[1]), constant % 4, tuple(x % 4 for x in linear),
+            tuple(sum(((quad[j][k] % 4) // 2) << k for k in range(j + 1, n)) for j in range(n)))
+
+
+def inverse(g):
+    n = len(g[0])
+    rows = invert_matrix(g[0])
+    offset = sum(dot(row, g[1]) << i for i, row in enumerate(rows))
+    h = (rows, offset, 0, (0,) * n, (0,) * n)
+    phase = compose(g, h)
+    return (rows, offset, -phase[2] % 4, tuple(-x % 4 for x in phase[3]), phase[4])
+
+
+def accumulate(row, key, value):
+    if key in row:
+        value = value + row[key]
+    if value:
+        row[key] = value
+    elif key in row:
+        del row[key]
+
+
+def algebra_endpoint(problem, code, generators, max_terms):
+    n, r = problem['axes'], problem['roles']
+    need(type(max_terms) is int and max_terms >= r, 'checker: expanded-term limit; no decision')
+    identity = (tuple(1 << i for i in range(n)), 0, 0, (0,) * n, (0,) * n)
+    state = [{(i, identity): QI(1)} for i in range(r)]
+    for ins in code:
+        op, d = ins['op'], ins['dst']
+        if op == 'swap':
+            s = ins['src']
+            state[s], state[d] = state[d], state[s]
+        elif op == 'scale':
+            c = scalar(ins.get('coefficient', 1))
+            state[d] = {k: c * v for k, v in state[d].items()} if c else {}
+        else:
+            s = d if op == 'apply' else ins['src']
+            old = list(state[s].items())
+            if op != 'add':
+                g = generators[ins['generator']]
+                if ins.get('inverse', False):
+                    g = inverse(g)
+                old = [((i, compose(g, h)), c) for (i, h), c in old]
+            if op == 'apply':
+                state[d] = {}
+            c = scalar(ins.get('coefficient', 1))
+            for key, value in old:
+                accumulate(state[d], key, c * value)
+        need(sum(len(row) for row in state) <= max_terms, 'checker: expanded-term limit; no decision')
+    return state
+
+
+def literal_endpoint(problem, code, generators, input_role, points, max_terms):
+    """Run literal tensor basis actions. No group products or Gram factors are used."""
+    state = [{} for _ in range(problem['roles'])]
+    state[input_role][tuple(points)] = QI(1)
+    for ins in code:
+        op, d = ins['op'], ins['dst']
+        if op == 'swap':
+            s = ins['src']
+            state[s], state[d] = state[d], state[s]
+        elif op == 'scale':
+            c = scalar(ins.get('coefficient', 1))
+            state[d] = {k: c * v for k, v in state[d].items()} if c else {}
+        else:
+            s = d if op == 'apply' else ins['src']
+            old = list(state[s].items())
+            if op != 'add':
+                g = generators[ins['generator']]
+                if ins.get('inverse', False):
+                    rows = invert_matrix(g[0])
+                    moved = []
+                    for xs, value in old:
+                        ys = tuple(sum(dot(row, x ^ g[1]) << j for j, row in enumerate(rows)) for x in xs)
+                        moved.append((ys, value * unit(-sum(exponent(g, y) for y in ys))))
+                else:
+                    moved = [(tuple(image(g, x) for x in xs), value * unit(sum(exponent(g, x) for x in xs)))
+                             for xs, value in old]
+                old = moved
+            if op == 'apply':
+                state[d] = {}
+            c = scalar(ins.get('coefficient', 1))
+            for xs, value in old:
+                accumulate(state[d], xs, c * value)
+        need(sum(map(len, state)) <= max_terms, 'checker: literal-term limit; no decision')
+    return state
+
+
+def check(problem, certificate, max_terms=100000):
+    need(isinstance(certificate, dict), 'checker: certificate object')
+    need(type(max_terms) is int and max_terms >= 1, 'checker: positive term limit')
+    generators = problem_data(problem)
+    digest = hashlib.sha256(json.dumps(problem, sort_keys=True, separators=(',', ':')).encode()).hexdigest()
+    need(certificate.get('schema') == 'native-tensor-cutoff/v1' and certificate.get('problem_sha256') == digest,
+         'checker: certificate binding')
+    n, r = problem['axes'], problem['roles']
+    need(certificate.get('axes') == n and certificate.get('roles') == r and
+         certificate.get('window') == [2 * n + 4, 2 * n + 7], 'checker: certificate dimensions')
+    if certificate.get('status') == 'IDENTITY_ALL_POSITIVE_WIDTHS':
+        a = algebra_endpoint(problem, problem['program'], generators, max_terms)
+        b = algebra_endpoint(problem, problem['reference'], generators, max_terms)
+        need(a == b and certificate.get('residual_terms') == 0, 'checker: complete native endpoints differ')
+        return 'PASS_NATIVE_IDENTITY_ALL_POSITIVE_WIDTHS'
+    need(certificate.get('status') == 'COUNTEREXAMPLE', 'checker: status')
+    xs, ys = certificate.get('input_points'), certificate.get('output_points')
+    need(isinstance(xs, list) and isinstance(ys, list) and len(xs) == len(ys) and
+         2 * n + 4 <= len(xs) <= 2 * n + 7, 'checker: witness width')
+    need(all(type(x) is int and 0 <= x < 1 << n for x in xs + ys), 'checker: witness coordinates')
+    i, o = certificate.get('input_role'), certificate.get('output_role')
+    need(type(i) is int and 0 <= i < r and type(o) is int and 0 <= o < r, 'checker: witness roles')
+    a = literal_endpoint(problem, problem['program'], generators, i, xs, max_terms)
+    b = literal_endpoint(problem, problem['reference'], generators, i, xs, max_terms)
+    observed = a[o].get(tuple(ys), QI()) - b[o].get(tuple(ys), QI())
+    need(bool(observed) and observed == scalar(certificate.get('discrepancy')), 'checker: witness discrepancy')
+    return 'PASS_NATIVE_TENSOR_COUNTEREXAMPLE'
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('problem', type=Path)
+    parser.add_argument('certificate', type=Path)
+    parser.add_argument('--max-terms', type=int, default=100000)
+    args = parser.parse_args()
+    need(args.max_terms >= 1, 'positive checker term limit')
+    print(check(json.loads(args.problem.read_text()), json.loads(args.certificate.read_text()), args.max_terms))
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/native-tensor-cutoff/exact.py b/research/native-tensor-cutoff/exact.py
new file mode 100644
index 0000000000..4f8514d1a2
--- /dev/null
+++ b/research/native-tensor-cutoff/exact.py
@@ -0,0 +1,68 @@
+"""Exact Gaussian rational arithmetic shared by the two checkers."""
+from fractions import Fraction
+import re
+
+
+class QI:
+    __slots__ = ('real', 'imag')
+
+    def __init__(self, real=0, imag=0):
+        if isinstance(real, QI):
+            self.real, self.imag = real.real, real.imag
+        else:
+            self.real, self.imag = Fraction(real), Fraction(imag)
+
+    def __add__(self, other):
+        other = QI(other)
+        return QI(self.real + other.real, self.imag + other.imag)
+
+    __radd__ = __add__
+
+    def __neg__(self):
+        return QI(-self.real, -self.imag)
+
+    def __sub__(self, other):
+        return self + -QI(other)
+
+    def __mul__(self, other):
+        other = QI(other)
+        return QI(self.real * other.real - self.imag * other.imag,
+                  self.real * other.imag + self.imag * other.real)
+
+    __rmul__ = __mul__
+
+    def __eq__(self, other):
+        if not isinstance(other, (QI, int, Fraction)):
+            return False
+        other = QI(other)
+        return self.real == other.real and self.imag == other.imag
+
+    def __bool__(self):
+        return bool(self.real or self.imag)
+
+    def json(self):
+        return [str(self.real), str(self.imag)]
+
+
+def scalar(value):
+    """Accept integers, rational strings, or two such components. Reject floats."""
+    def component(x):
+        if type(x) is int:
+            return Fraction(x)
+        if isinstance(x, str) and re.fullmatch(r'[+-]?[0-9]+(?:/[+-]?[0-9]+)?', x):
+            return Fraction(x)
+        raise ValueError('explicit integer or rational component required')
+    if type(value) is int or isinstance(value, str):
+        return QI(component(value))
+    if isinstance(value, list) and len(value) == 2:
+        return QI(component(value[0]), component(value[1]))
+    raise ValueError('exact Gaussian coefficient required')
+
+
+def unit(power):
+    return (QI(1), QI(0, 1), QI(-1), QI(0, -1))[power % 4]
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
diff --git a/research/native-tensor-cutoff/examples.py b/research/native-tensor-cutoff/examples.py
new file mode 100644
index 0000000000..616b6dd242
--- /dev/null
+++ b/research/native-tensor-cutoff/examples.py
@@ -0,0 +1,83 @@
+"""Build source-bound examples and the two obstruction families."""
+import json
+from pathlib import Path
+import sys
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+from native import Native, act, inverse
+from reversible_cnf import cnf_problem
+
+HERE = Path(__file__).resolve().parent
+
+
+def diagonal(n, phase=0, linear=None, quadratic=None):
+    return Native(tuple(1 << i for i in range(n)), 0, phase,
+                  tuple(linear or [0] * n), tuple(quadratic or [0] * n)).json()
+
+
+def source_conjugation(mutate=False):
+    raw = json.loads((HERE / 'source/RIGHT-RECIPE.json').read_text())
+    n = len(raw['matrix_rows'])
+    rows = inverse(raw['matrix_rows'])
+    shift = act(rows, raw['offset'])
+    i = next(i for i in range(n) if shift >> i & 1)
+    z = [0] * n
+    z[i] = 2
+    r = [2 * ((rows[i] >> j) & 1) for j in range(n)]
+    generators = {'G': raw, 'Z': diagonal(n, linear=z),
+                  'R': diagonal(n, phase=0 if mutate else 2, linear=r)}
+    # G Z G^-1 is R. The source role is restored before the final subtraction.
+    sequence = [{'op': 'apply', 'dst': 0, 'generator': 'G', 'inverse': True},
+                {'op': 'apply', 'dst': 0, 'generator': 'Z'},
+                {'op': 'apply', 'dst': 0, 'generator': 'G'},
+                {'op': 'add', 'src': 0, 'dst': 1},
+                {'op': 'apply', 'dst': 0, 'generator': 'G', 'inverse': True},
+                {'op': 'apply', 'dst': 0, 'generator': 'Z', 'inverse': True},
+                {'op': 'apply', 'dst': 0, 'generator': 'G'},
+                {'op': 'query', 'src': 0, 'dst': 1, 'generator': 'R', 'coefficient': -1}]
+    return {'axes': n, 'roles': 2, 'generators': generators, 'program': sequence, 'reference': []}
+
+
+def late_projector(n):
+    generators, code = {}, []
+    for i in range(n):
+        a = [0] * n
+        a[i] = 1
+        generators['S' + str(i)] = diagonal(n, linear=a)
+        a[i] = 2
+        generators['Z' + str(i)] = diagonal(n, linear=a)
+        code.extend([{'op': 'query', 'src': 0, 'dst': 0, 'generator': 'S' + str(i), 'coefficient': [0, -1]},
+                     {'op': 'query', 'src': 0, 'dst': 0, 'generator': 'Z' + str(i), 'coefficient': -1},
+                     {'op': 'scale', 'dst': 0, 'coefficient': '1/4'}])
+    for i in range(n):
+        for j in range(i + 1, n):
+            q = [0] * n
+            q[i] = 1 << j
+            name = f'CZ{i}_{j}'
+            generators[name] = diagonal(n, quadratic=q)
+            code.extend([{'op': 'query', 'src': 0, 'dst': 0, 'generator': name},
+                         {'op': 'scale', 'dst': 0, 'coefficient': '1/2'}])
+    return {'axes': n, 'roles': 1, 'generators': generators, 'program': code,
+            'reference': [{'op': 'scale', 'dst': 0, 'coefficient': 0}]}
+
+
+def write_examples():
+    from native_identity import decide, digest
+    cases = {'source-conjugation': source_conjugation(),
+             'source-phase-error': source_conjugation(True),
+             'cnf-unsatisfiable': cnf_problem(3, [[1], [-1]]),
+             'cnf-satisfiable': cnf_problem(3, [[1, 2], [-1]])}
+    for name, problem in cases.items():
+        (HERE / 'examples' / (name + '.json')).write_text(json.dumps(problem, indent=2) + '\n')
+        (HERE / 'examples' / (name + '.certificate.json')).write_text(json.dumps(decide(problem), indent=2) + '\n')
+    problem = late_projector(9)
+    points = [1 << i for i in range(9)] + [0] * 13
+    certificate = {'schema': 'native-tensor-cutoff/v1', 'problem_sha256': digest(problem),
+                   'status': 'COUNTEREXAMPLE', 'axes': 9, 'roles': 1, 'window': [22, 25],
+                   'input_role': 0, 'output_role': 0, 'input_points': points,
+                   'output_points': points, 'discrepancy': ['1', '0']}
+    (HERE / 'examples/late-projector-9.json').write_text(json.dumps(problem, indent=2) + '\n')
+    (HERE / 'examples/late-projector-9.certificate.json').write_text(json.dumps(certificate, indent=2) + '\n')
+
+
+if __name__ == '__main__':
+    write_examples()
diff --git a/research/native-tensor-cutoff/examples/cnf-satisfiable.certificate.json b/research/native-tensor-cutoff/examples/cnf-satisfiable.certificate.json
new file mode 100644
index 0000000000..5259dd5256
--- /dev/null
+++ b/research/native-tensor-cutoff/examples/cnf-satisfiable.certificate.json
@@ -0,0 +1,56 @@
+{
+  "schema": "native-tensor-cutoff/v1",
+  "problem_sha256": "a7a99f3e9a4a15e6394a47d58634f40cf81f85e03b16887748ba92a1af8f33fe",
+  "axes": 3,
+  "roles": 5,
+  "window": [
+    10,
+    13
+  ],
+  "peak_expanded_terms": 78,
+  "residual_terms": 40,
+  "status": "COUNTEREXAMPLE",
+  "input_role": 0,
+  "output_role": 0,
+  "input_points": [
+    0,
+    1,
+    2,
+    4,
+    1,
+    4,
+    5,
+    5,
+    0,
+    0,
+    0,
+    0
+  ],
+  "output_points": [
+    0,
+    1,
+    2,
+    4,
+    1,
+    4,
+    5,
+    5,
+    0,
+    0,
+    0,
+    0
+  ],
+  "character": [
+    0,
+    0,
+    1,
+    0,
+    0,
+    0,
+    0
+  ],
+  "discrepancy": [
+    "-1",
+    "0"
+  ]
+}
diff --git a/research/native-tensor-cutoff/examples/cnf-satisfiable.json b/research/native-tensor-cutoff/examples/cnf-satisfiable.json
new file mode 100644
index 0000000000..204fe57df4
--- /dev/null
+++ b/research/native-tensor-cutoff/examples/cnf-satisfiable.json
@@ -0,0 +1,1466 @@
+{
+  "axes": 3,
+  "roles": 5,
+  "generators": {
+    "Z1": {
+      "matrix_rows": [
+        1,
+        2,
+        4
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        2,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0
+      ]
+    },
+    "Z2": {
+      "matrix_rows": [
+        1,
+        2,
+        4
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        2,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0
+      ]
+    },
+    "Z3": {
+      "matrix_rows": [
+        1,
+        2,
+        4
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        2
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0
+      ]
+    }
+  },
+  "program": [
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z2",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z2"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    }
+  ],
+  "reference": []
+}
diff --git a/research/native-tensor-cutoff/examples/cnf-unsatisfiable.certificate.json b/research/native-tensor-cutoff/examples/cnf-unsatisfiable.certificate.json
new file mode 100644
index 0000000000..7a11f7a5e7
--- /dev/null
+++ b/research/native-tensor-cutoff/examples/cnf-unsatisfiable.certificate.json
@@ -0,0 +1,13 @@
+{
+  "schema": "native-tensor-cutoff/v1",
+  "problem_sha256": "2cc99a0c1756ebea3d2243e1b022e662c910f23e55e6f55d6642857cb48809bb",
+  "axes": 3,
+  "roles": 5,
+  "window": [
+    10,
+    13
+  ],
+  "peak_expanded_terms": 28,
+  "residual_terms": 0,
+  "status": "IDENTITY_ALL_POSITIVE_WIDTHS"
+}
diff --git a/research/native-tensor-cutoff/examples/cnf-unsatisfiable.json b/research/native-tensor-cutoff/examples/cnf-unsatisfiable.json
new file mode 100644
index 0000000000..d350933d9c
--- /dev/null
+++ b/research/native-tensor-cutoff/examples/cnf-unsatisfiable.json
@@ -0,0 +1,570 @@
+{
+  "axes": 3,
+  "roles": 5,
+  "generators": {
+    "Z1": {
+      "matrix_rows": [
+        1,
+        2,
+        4
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        2,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0
+      ]
+    },
+    "Z2": {
+      "matrix_rows": [
+        1,
+        2,
+        4
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        2,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0
+      ]
+    },
+    "Z3": {
+      "matrix_rows": [
+        1,
+        2,
+        4
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        2
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0
+      ]
+    }
+  },
+  "program": [
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 2
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 4
+    },
+    {
+      "op": "swap",
+      "src": 0,
+      "dst": 3
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 3,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 3,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 3,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 4,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 4,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 4,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 1,
+      "dst": 0
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0,
+      "coefficient": -1
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 2,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 2,
+      "generator": "Z1",
+      "coefficient": "-1/2"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z1"
+    },
+    {
+      "op": "add",
+      "src": 2,
+      "dst": 0
+    }
+  ],
+  "reference": []
+}
diff --git a/research/native-tensor-cutoff/examples/late-projector-9.certificate.json b/research/native-tensor-cutoff/examples/late-projector-9.certificate.json
new file mode 100644
index 0000000000..100839ae79
--- /dev/null
+++ b/research/native-tensor-cutoff/examples/late-projector-9.certificate.json
@@ -0,0 +1,65 @@
+{
+  "schema": "native-tensor-cutoff/v1",
+  "problem_sha256": "7f0f881fb08fb94719b17fe5b0ed81305e82934f2077e0700d2a48890df46e0a",
+  "status": "COUNTEREXAMPLE",
+  "axes": 9,
+  "roles": 1,
+  "window": [
+    22,
+    25
+  ],
+  "input_role": 0,
+  "output_role": 0,
+  "input_points": [
+    1,
+    2,
+    4,
+    8,
+    16,
+    32,
+    64,
+    128,
+    256,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0
+  ],
+  "output_points": [
+    1,
+    2,
+    4,
+    8,
+    16,
+    32,
+    64,
+    128,
+    256,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0
+  ],
+  "discrepancy": [
+    "1",
+    "0"
+  ]
+}
diff --git a/research/native-tensor-cutoff/examples/late-projector-9.json b/research/native-tensor-cutoff/examples/late-projector-9.json
new file mode 100644
index 0000000000..0f16529e34
--- /dev/null
+++ b/research/native-tensor-cutoff/examples/late-projector-9.json
@@ -0,0 +1,2607 @@
+{
+  "axes": 9,
+  "roles": 1,
+  "generators": {
+    "S0": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        1,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "Z0": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        2,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "S1": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        1,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "Z1": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        2,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "S2": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        1,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "Z2": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        2,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "S3": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        1,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "Z3": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        2,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "S4": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        1,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "Z4": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        2,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "S5": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        1,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "Z5": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        2,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "S6": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        1,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "Z6": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        2,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "S7": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        1,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "Z7": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        2,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "S8": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        1
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "Z8": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        2
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ0_1": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        2,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ0_2": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        4,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ0_3": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        8,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ0_4": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        16,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ0_5": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        32,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ0_6": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        64,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ0_7": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        128,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ0_8": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        256,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ1_2": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        4,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ1_3": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        8,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ1_4": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        16,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ1_5": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        32,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ1_6": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        64,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ1_7": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        128,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ1_8": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        256,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ2_3": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        8,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ2_4": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        16,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ2_5": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        32,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ2_6": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        64,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ2_7": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        128,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ2_8": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        256,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ3_4": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        16,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ3_5": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        32,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ3_6": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        64,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ3_7": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        128,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ3_8": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        256,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ4_5": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        32,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ4_6": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        64,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ4_7": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        128,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ4_8": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        256,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ5_6": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        64,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ5_7": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        128,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ5_8": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        256,
+        0,
+        0,
+        0
+      ]
+    },
+    "CZ6_7": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        128,
+        0,
+        0
+      ]
+    },
+    "CZ6_8": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        256,
+        0,
+        0
+      ]
+    },
+    "CZ7_8": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        256,
+        0
+      ]
+    }
+  },
+  "program": [
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "S0",
+      "coefficient": [
+        0,
+        -1
+      ]
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "Z0",
+      "coefficient": -1
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/4"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "S1",
+      "coefficient": [
+        0,
+        -1
+      ]
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "Z1",
+      "coefficient": -1
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/4"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "S2",
+      "coefficient": [
+        0,
+        -1
+      ]
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "Z2",
+      "coefficient": -1
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/4"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "S3",
+      "coefficient": [
+        0,
+        -1
+      ]
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "Z3",
+      "coefficient": -1
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/4"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "S4",
+      "coefficient": [
+        0,
+        -1
+      ]
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "Z4",
+      "coefficient": -1
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/4"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "S5",
+      "coefficient": [
+        0,
+        -1
+      ]
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "Z5",
+      "coefficient": -1
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/4"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "S6",
+      "coefficient": [
+        0,
+        -1
+      ]
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "Z6",
+      "coefficient": -1
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/4"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "S7",
+      "coefficient": [
+        0,
+        -1
+      ]
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "Z7",
+      "coefficient": -1
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/4"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "S8",
+      "coefficient": [
+        0,
+        -1
+      ]
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "Z8",
+      "coefficient": -1
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/4"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ0_1"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ0_2"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ0_3"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ0_4"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ0_5"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ0_6"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ0_7"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ0_8"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ1_2"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ1_3"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ1_4"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ1_5"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ1_6"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ1_7"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ1_8"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ2_3"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ2_4"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ2_5"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ2_6"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ2_7"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ2_8"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ3_4"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ3_5"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ3_6"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ3_7"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ3_8"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ4_5"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ4_6"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ4_7"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ4_8"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ5_6"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ5_7"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ5_8"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ6_7"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ6_8"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 0,
+      "generator": "CZ7_8"
+    },
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": "1/2"
+    }
+  ],
+  "reference": [
+    {
+      "op": "scale",
+      "dst": 0,
+      "coefficient": 0
+    }
+  ]
+}
diff --git a/research/native-tensor-cutoff/examples/source-conjugation.certificate.json b/research/native-tensor-cutoff/examples/source-conjugation.certificate.json
new file mode 100644
index 0000000000..ee46505bf0
--- /dev/null
+++ b/research/native-tensor-cutoff/examples/source-conjugation.certificate.json
@@ -0,0 +1,13 @@
+{
+  "schema": "native-tensor-cutoff/v1",
+  "problem_sha256": "2c6c396b75ab7f59a41db62f6a5b8706fdc87abf839a3f2377d0fc1ed38cea64",
+  "axes": 9,
+  "roles": 2,
+  "window": [
+    22,
+    25
+  ],
+  "peak_expanded_terms": 3,
+  "residual_terms": 0,
+  "status": "IDENTITY_ALL_POSITIVE_WIDTHS"
+}
diff --git a/research/native-tensor-cutoff/examples/source-conjugation.json b/research/native-tensor-cutoff/examples/source-conjugation.json
new file mode 100644
index 0000000000..760f54ac2d
--- /dev/null
+++ b/research/native-tensor-cutoff/examples/source-conjugation.json
@@ -0,0 +1,165 @@
+{
+  "axes": 9,
+  "roles": 2,
+  "generators": {
+    "G": {
+      "matrix_rows": [
+        6,
+        64,
+        384,
+        5,
+        34,
+        32,
+        8,
+        48,
+        256
+      ],
+      "offset": 426,
+      "quadratic_rows": [
+        4,
+        38,
+        39,
+        0,
+        0,
+        6,
+        256,
+        256,
+        448
+      ],
+      "linear_Z4": [
+        2,
+        1,
+        3,
+        0,
+        0,
+        2,
+        0,
+        0,
+        1
+      ],
+      "phase": 1
+    },
+    "Z": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        2,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "R": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 2,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        2,
+        2,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    }
+  },
+  "program": [
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "G",
+      "inverse": true
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "G"
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "G",
+      "inverse": true
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z",
+      "inverse": true
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "G"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "R",
+      "coefficient": -1
+    }
+  ],
+  "reference": []
+}
diff --git a/research/native-tensor-cutoff/examples/source-phase-error.certificate.json b/research/native-tensor-cutoff/examples/source-phase-error.certificate.json
new file mode 100644
index 0000000000..6325413cbe
--- /dev/null
+++ b/research/native-tensor-cutoff/examples/source-phase-error.certificate.json
@@ -0,0 +1,121 @@
+{
+  "schema": "native-tensor-cutoff/v1",
+  "problem_sha256": "e7bd947c70fd0938d04a922dc7ab3b4b55819caab46dc8a54d6320f01e380637",
+  "axes": 9,
+  "roles": 2,
+  "window": [
+    22,
+    25
+  ],
+  "peak_expanded_terms": 4,
+  "residual_terms": 2,
+  "status": "COUNTEREXAMPLE",
+  "input_role": 0,
+  "output_role": 1,
+  "input_points": [
+    0,
+    1,
+    2,
+    4,
+    8,
+    16,
+    32,
+    64,
+    128,
+    256,
+    1,
+    2,
+    4,
+    8,
+    16,
+    32,
+    64,
+    128,
+    256,
+    511,
+    511,
+    0,
+    0,
+    0,
+    0
+  ],
+  "output_points": [
+    0,
+    1,
+    2,
+    4,
+    8,
+    16,
+    32,
+    64,
+    128,
+    256,
+    1,
+    2,
+    4,
+    8,
+    16,
+    32,
+    64,
+    128,
+    256,
+    511,
+    511,
+    0,
+    0,
+    0,
+    0
+  ],
+  "character": [
+    1,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0,
+    0
+  ],
+  "discrepancy": [
+    "-2",
+    "0"
+  ]
+}
diff --git a/research/native-tensor-cutoff/examples/source-phase-error.json b/research/native-tensor-cutoff/examples/source-phase-error.json
new file mode 100644
index 0000000000..72283b7edf
--- /dev/null
+++ b/research/native-tensor-cutoff/examples/source-phase-error.json
@@ -0,0 +1,165 @@
+{
+  "axes": 9,
+  "roles": 2,
+  "generators": {
+    "G": {
+      "matrix_rows": [
+        6,
+        64,
+        384,
+        5,
+        34,
+        32,
+        8,
+        48,
+        256
+      ],
+      "offset": 426,
+      "quadratic_rows": [
+        4,
+        38,
+        39,
+        0,
+        0,
+        6,
+        256,
+        256,
+        448
+      ],
+      "linear_Z4": [
+        2,
+        1,
+        3,
+        0,
+        0,
+        2,
+        0,
+        0,
+        1
+      ],
+      "phase": 1
+    },
+    "Z": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        2,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    },
+    "R": {
+      "matrix_rows": [
+        1,
+        2,
+        4,
+        8,
+        16,
+        32,
+        64,
+        128,
+        256
+      ],
+      "offset": 0,
+      "phase": 0,
+      "linear_Z4": [
+        0,
+        0,
+        0,
+        0,
+        2,
+        2,
+        0,
+        0,
+        0
+      ],
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ]
+    }
+  },
+  "program": [
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "G",
+      "inverse": true
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z"
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "G"
+    },
+    {
+      "op": "add",
+      "src": 0,
+      "dst": 1
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "G",
+      "inverse": true
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "Z",
+      "inverse": true
+    },
+    {
+      "op": "apply",
+      "dst": 0,
+      "generator": "G"
+    },
+    {
+      "op": "query",
+      "src": 0,
+      "dst": 1,
+      "generator": "R",
+      "coefficient": -1
+    }
+  ],
+  "reference": []
+}
diff --git a/research/native-tensor-cutoff/native.py b/research/native-tensor-cutoff/native.py
new file mode 100644
index 0000000000..8872f540e1
--- /dev/null
+++ b/research/native-tensor-cutoff/native.py
@@ -0,0 +1,193 @@
+"""Canonical affine maps with quadratic Gaussian phases."""
+from dataclasses import dataclass
+from exact import need
+
+
+def parity(x):
+    return x.bit_count() & 1
+
+
+def act(rows, x):
+    return sum(parity(row & x) << j for j, row in enumerate(rows))
+
+
+def inverse(rows):
+    n = len(rows)
+    work = [row | (1 << (n + i)) for i, row in enumerate(rows)]
+    for j in range(n):
+        p = next((k for k in range(j, n) if work[k] >> j & 1), None)
+        need(p is not None, 'invertible binary matrix required')
+        work[j], work[p] = work[p], work[j]
+        for k in range(n):
+            if k != j and work[k] >> j & 1:
+                work[k] ^= work[j]
+    return tuple(x >> n for x in work)
+
+
+def matrix_product(left, right):
+    result = []
+    for row in left:
+        value = 0
+        for j, other in enumerate(right):
+            if row >> j & 1:
+                value ^= other
+        result.append(value)
+    return tuple(result)
+
+
+@dataclass(frozen=True)
+class Native:
+    rows: tuple
+    offset: int
+    phase: int
+    linear: tuple
+    quadratic: tuple
+
+    @property
+    def n(self):
+        return len(self.rows)
+
+    @classmethod
+    def identity(cls, n):
+        return cls(tuple(1 << j for j in range(n)), 0, 0, (0,) * n, (0,) * n)
+
+    @classmethod
+    def parse(cls, data, n):
+        need(isinstance(data, dict), 'native recipe object required')
+        need(set(data) == {'matrix_rows', 'offset', 'phase', 'linear_Z4', 'quadratic_rows'},
+             'exact native recipe fields required')
+        rows, linear, quadratic = (data[k] for k in ('matrix_rows', 'linear_Z4', 'quadratic_rows'))
+        need(all(isinstance(x, list) and len(x) == n for x in (rows, linear, quadratic)),
+             'native recipe dimension')
+        need(all(type(x) is int and 0 <= x < 1 << n for x in rows + quadratic),
+             'binary row extent')
+        need(all(type(x) is int and 0 <= x < 4 for x in linear), 'linear phase extent')
+        need(type(data['offset']) is int and 0 <= data['offset'] < 1 << n, 'offset extent')
+        need(type(data['phase']) is int and 0 <= data['phase'] < 4, 'constant phase extent')
+        inverse(rows)
+        # The source convention ignores diagonal and lower quadratic entries.
+        quadratic = tuple(row & ~((1 << (j + 1)) - 1) for j, row in enumerate(quadratic))
+        return cls(tuple(rows), data['offset'], data['phase'], tuple(linear), quadratic)
+
+    def json(self):
+        return {'matrix_rows': list(self.rows), 'offset': self.offset, 'phase': self.phase,
+                'linear_Z4': list(self.linear), 'quadratic_rows': list(self.quadratic)}
+
+    def image(self, x):
+        return act(self.rows, x) ^ self.offset
+
+    def exponent(self, x):
+        return (self.phase + sum(self.linear[i] for i in range(self.n) if x >> i & 1)
+                + 2 * sum(parity(self.quadratic[i] & x) for i in range(self.n) if x >> i & 1)) % 4
+
+    @classmethod
+    def from_function(cls, rows, offset, phase_function):
+        n = len(rows)
+        c = phase_function(0) % 4
+        a = tuple((phase_function(1 << i) - c) % 4 for i in range(n))
+        quadratic = []
+        for i in range(n):
+            row = 0
+            for j in range(i + 1, n):
+                delta = (phase_function((1 << i) | (1 << j)) - c - a[i] - a[j]) % 4
+                need(delta in (0, 2), 'quadratic phase parity')
+                row |= (delta // 2) << j
+            quadratic.append(row)
+        return cls(tuple(rows), offset, c, a, tuple(quadratic))
+
+    def compose(self, right):
+        """Apply right first, then this map. Scalars stay outside this operation."""
+        need(self.n == right.n, 'composition dimension')
+        return Native.from_function(matrix_product(self.rows, right.rows),
+                                    act(self.rows, right.offset) ^ self.offset,
+                                    lambda x: right.exponent(x) + self.exponent(right.image(x)))
+
+    def inv(self):
+        rows = inverse(self.rows)
+        offset = act(rows, self.offset)
+        return Native.from_function(rows, offset, lambda x: -self.exponent(act(rows, x) ^ offset))
+
+    def phase_key(self):
+        return ((self.phase,) + self.linear +
+                tuple((self.quadratic[i] >> j) & 1 for i in range(self.n) for j in range(i + 1, self.n)))
+
+
+def gram_factor(rows):
+    """Return at most n+1 columns whose binary outer products sum to rows."""
+    n = len(rows)
+    need(all(0 <= r < 1 << n for r in rows), 'Gram row extent')
+    need(all(((rows[i] >> j) & 1) == ((rows[j] >> i) & 1)
+             for i in range(n) for j in range(n)), 'symmetric Gram matrix')
+
+    def pair(x, y):
+        return parity(x & act(rows, y))
+
+    pending = [1 << i for i in range(n)]
+    singles, pairs = [], []
+    while pending:
+        p = next((i for i, v in enumerate(pending) if pair(v, v)), None)
+        if p is not None:
+            v = pending.pop(p)
+            singles.append(v)
+            pending = [w ^ (v if pair(v, w) else 0) for w in pending]
+            continue
+        hit = next(((i, j) for i in range(len(pending)) for j in range(i + 1, len(pending))
+                    if pair(pending[i], pending[j])), None)
+        if hit is None:
+            break
+        i, j = hit
+        v, w = pending[i], pending[j]
+        pairs.append((v, w))
+        pending = [u ^ (v if pair(u, w) else 0) ^ (w if pair(u, v) else 0)
+                   for k, u in enumerate(pending) if k not in (i, j)]
+
+    basis = singles + [v for pair_ in pairs for v in pair_] + pending
+    a, b = len(singles), len(pairs)
+    rank = a + 2 * b
+    width = rank + bool(b)
+    # Even-weight vectors in odd dimension have a nonsingular alternating form.
+    even = [(1 << i) | (1 << (2 * b)) for i in range(2 * b)]
+    hyperbolic = []
+    while even:
+        v = even.pop(0)
+        j = next(j for j, w in enumerate(even) if parity(v & w))
+        w = even.pop(j)
+        hyperbolic.extend((v, w))
+        even = [u ^ (v if parity(u & w) else 0) ^ (w if parity(u & v) else 0) for u in even]
+    canonical = ([1 << i for i in range(a)] + [v << a for v in hyperbolic]
+                 + [0] * len(pending))
+    undo = inverse(basis)
+    vectors = []
+    for row in undo:
+        value = 0
+        for j in range(n):
+            if row >> j & 1:
+                value ^= canonical[j]
+        vectors.append(value)
+    return [sum(((vectors[i] >> j) & 1) << i for i in range(n)) for j in range(width)]
+
+
+def character_tuple(n, character, floor=None):
+    """Realize one phase character on an affinely spanning tuple."""
+    need(len(character) == 1 + n + n * (n - 1) // 2, 'phase character dimension')
+    need(all(type(x) is int and 0 <= x < 4 for x in character[:n + 1]) and
+         all(type(x) is int and x in (0, 1) for x in character[n + 1:]), 'phase character extent')
+    floor = 2 * n + 4 if floor is None else floor
+    need(type(floor) is int and floor >= 2 * n + 4, 'tensor window floor')
+    c, a = character[0], character[1:n + 1]
+    rows = [((a[i] & 1) ^ 1) << i for i in range(n)]
+    k = n + 1
+    for i in range(n):
+        for j in range(i + 1, n):
+            rows[i] |= character[k] << j
+            rows[j] |= character[k] << i
+            k += 1
+    points = [0] + [1 << i for i in range(n)] + gram_factor(rows)
+    counts = [sum((x >> i) & 1 for x in points) % 4 for i in range(n)]
+    need(all((a[i] - counts[i]) % 2 == 0 for i in range(n)), 'Gram parity invariant')
+    z = sum((((a[i] - counts[i]) % 4) // 2) << i for i in range(n))
+    if z:
+        points.extend((z, z))
+    f = floor + (c - floor) % 4
+    need(len(points) <= f, 'proved tensor cutoff')
+    return points + [0] * (f - len(points))
diff --git a/research/native-tensor-cutoff/native_identity.py b/research/native-tensor-cutoff/native_identity.py
new file mode 100644
index 0000000000..85376a935d
--- /dev/null
+++ b/research/native-tensor-cutoff/native_identity.py
@@ -0,0 +1,159 @@
+"""Decide complete dirty endpoints and produce a short native tensor witness."""
+import argparse
+import hashlib
+import json
+from pathlib import Path
+import sys
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+from exact import QI, need, scalar, unit
+from native import Native, character_tuple
+
+
+def digest(problem):
+    return hashlib.sha256(json.dumps(problem, sort_keys=True, separators=(',', ':')).encode()).hexdigest()
+
+
+def validate(problem):
+    need(isinstance(problem, dict) and set(problem) == {'axes', 'roles', 'generators', 'program', 'reference'},
+         'exact problem fields required')
+    n, r = problem['axes'], problem['roles']
+    need(type(n) is int and 1 <= n <= 256, 'axes must be in 1..256')
+    need(type(r) is int and 1 <= r <= 4096, 'roles must be in 1..4096')
+    need(isinstance(problem['generators'], dict), 'generator table required')
+    generators = {}
+    for name, data in problem['generators'].items():
+        need(isinstance(name, str) and bool(name), 'generator name required')
+        generators[name] = Native.parse(data, n)
+    for program in (problem['program'], problem['reference']):
+        need(isinstance(program, list), 'instruction list required')
+        for instruction in program:
+            need(isinstance(instruction, dict), 'instruction object required')
+            op = instruction.get('op')
+            fields = {'add': {'op', 'src', 'dst', 'coefficient'},
+                      'query': {'op', 'src', 'dst', 'coefficient', 'generator', 'inverse'},
+                      'apply': {'op', 'dst', 'generator', 'inverse'},
+                      'scale': {'op', 'dst', 'coefficient'},
+                      'swap': {'op', 'src', 'dst'}}
+            need(isinstance(op, str) and op in fields and set(instruction) <= fields[op], 'instruction fields')
+            need('dst' in instruction, 'destination required')
+            if op in ('add', 'query', 'swap'):
+                need('src' in instruction, 'source required')
+            for key in ('src', 'dst'):
+                if key in instruction:
+                    need(type(instruction[key]) is int and 0 <= instruction[key] < r, 'role index')
+            if op in ('query', 'apply'):
+                need(isinstance(instruction.get('generator'), str) and instruction['generator'] in generators,
+                     'known native generator required')
+                need(type(instruction.get('inverse', False)) is bool, 'inverse flag')
+            if 'coefficient' in instruction:
+                scalar(instruction['coefficient'])
+    return generators
+
+
+def add_term(row, key, value):
+    new = row.get(key, QI()) + value
+    if new:
+        row[key] = new
+    else:
+        row.pop(key, None)
+
+
+def endpoint(problem, instructions, generators, max_terms=100000):
+    need(type(max_terms) is int and max_terms >= problem['roles'], 'expanded-term limit exceeded; no decision')
+    identity = Native.identity(problem['axes'])
+    state = [{(i, identity): QI(1)} for i in range(problem['roles'])]
+    inverses = {}
+    peak = len(state)
+    for instruction in instructions:
+        op, d = instruction['op'], instruction['dst']
+        if op == 'swap':
+            s = instruction['src']
+            state[s], state[d] = state[d], state[s]
+        elif op == 'scale':
+            c = scalar(instruction.get('coefficient', 1))
+            state[d] = {key: c * value for key, value in state[d].items()} if c else {}
+        else:
+            s = d if op == 'apply' else instruction['src']
+            old = list(state[s].items())
+            c = scalar(instruction.get('coefficient', 1))
+            if op in ('apply', 'query'):
+                name = instruction['generator']
+                g = generators[name]
+                if instruction.get('inverse', False):
+                    if name not in inverses:
+                        inverses[name] = g.inv()
+                    g = inverses[name]
+                old = [((i, g.compose(h)), value) for (i, h), value in old]
+            if op == 'apply':
+                state[d] = {}
+            for key, value in old:
+                add_term(state[d], key, c * value)
+        size = sum(map(len, state))
+        need(size <= max_terms, 'expanded-term limit exceeded; no decision')
+        peak = max(peak, size)
+    return state, peak
+
+
+def choose_character(table, n):
+    """Choose a nonzero finite Fourier value without enumerating all characters."""
+    moduli = [4] * (n + 1) + [2] * (n * (n - 1) // 2)
+    chosen = []
+    for modulus in moduli:
+        for k in range(modulus):
+            reduced = {}
+            for key, coefficient in table.items():
+                add_term(reduced, key[1:], coefficient * unit((4 // modulus) * k * key[0]))
+            if reduced:
+                table = reduced
+                chosen.append(k)
+                break
+        else:
+            raise ValueError('nonzero Fourier invariant failed')
+    need(set(table) == {()}, 'complete Fourier projection')
+    return chosen, table[()]
+
+
+def decide(problem, max_terms=100000):
+    need(type(max_terms) is int and max_terms >= 1, 'positive expanded-term limit')
+    generators = validate(problem)
+    left, p = endpoint(problem, problem['program'], generators, max_terms)
+    right, q = endpoint(problem, problem['reference'], generators, max_terms)
+    residual = []
+    for a, b in zip(left, right):
+        row = dict(a)
+        for key, value in b.items():
+            add_term(row, key, -value)
+        residual.append(row)
+    n = problem['axes']
+    result = {'schema': 'native-tensor-cutoff/v1', 'problem_sha256': digest(problem),
+              'axes': n, 'roles': problem['roles'], 'window': [2 * n + 4, 2 * n + 7],
+              'peak_expanded_terms': max(p, q), 'residual_terms': sum(map(len, residual))}
+    if not any(residual):
+        result['status'] = 'IDENTITY_ALL_POSITIVE_WIDTHS'
+        return result
+    o = next(i for i, row in enumerate(residual) if row)
+    source, g = next(iter(residual[o]))
+    table = {h.phase_key(): value for (i, h), value in residual[o].items()
+             if i == source and h.rows == g.rows and h.offset == g.offset}
+    character, amplitude = choose_character(table, n)
+    points = character_tuple(n, character)
+    result.update(status='COUNTEREXAMPLE', input_role=source, output_role=o,
+                  input_points=points, output_points=[g.image(x) for x in points],
+                  character=character, discrepancy=amplitude.json())
+    return result
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('problem', type=Path)
+    parser.add_argument('--output', type=Path, required=True)
+    parser.add_argument('--max-terms', type=int, default=100000)
+    args = parser.parse_args()
+    need(args.max_terms >= 1, 'positive expanded-term limit')
+    result = decide(json.loads(args.problem.read_text()), args.max_terms)
+    args.output.write_text(json.dumps(result, indent=2) + '\n')
+    print(result['status'])
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/native-tensor-cutoff/reversible_cnf.py b/research/native-tensor-cutoff/reversible_cnf.py
new file mode 100644
index 0000000000..6878b4c33e
--- /dev/null
+++ b/research/native-tensor-cutoff/reversible_cnf.py
@@ -0,0 +1,125 @@
+"""Compile three-literal CNF to a reversible five-role native identity test.
+
+The width-five group-program construction is Barrington's classical method.
+"""
+from exact import need
+
+IDENTITY = (0, 1, 2, 3, 4)
+A = (1, 2, 3, 4, 0)
+B = (1, 3, 0, 4, 2)
+C = (4, 3, 1, 0, 2)
+
+
+def compose(p, q):
+    return tuple(p[q[i]] for i in range(5))
+
+
+def inverse(p):
+    return tuple(p.index(i) for i in range(5))
+
+
+def conjugator(source, target):
+    out = [None] * 5
+    i = j = 0
+    for _ in range(5):
+        out[i] = j
+        i, j = source[i], target[j]
+    need(sorted(out) == list(range(5)), 'five-cycle conjugator')
+    return tuple(out)
+
+
+def invert_word(word):
+    return [(variable, inverse(zero), inverse(one)) for variable, zero, one in reversed(word)]
+
+
+def formula_word(formula, target=A):
+    if type(formula) is bool:
+        return [(None, target, target)] if formula else []
+    if type(formula) is int:
+        return [(abs(formula) - 1, IDENTITY, target)] if formula > 0 else [(abs(formula) - 1, target, IDENTITY)]
+    op, *children = formula
+    if op == 'not':
+        return invert_word(formula_word(children[0], target)) + [(None, target, target)]
+    if op == 'or':
+        return formula_word(('not', ('and', ('not', children[0]), ('not', children[1]))), target)
+    need(op == 'and', 'Boolean formula operation')
+    f = conjugator(C, target)
+    left_target = compose(f, compose(A, inverse(f)))
+    right_target = compose(f, compose(B, inverse(f)))
+    left, right = formula_word(children[0], left_target), formula_word(children[1], right_target)
+    return left + right + invert_word(left) + invert_word(right)
+
+
+def balanced(op, items, empty):
+    if not items:
+        return empty
+    items = list(items)
+    while len(items) > 1:
+        items = [(op, items[i], items[i + 1]) if i + 1 < len(items) else items[i]
+                 for i in range(0, len(items), 2)]
+    return items[0]
+
+
+def cnf_word(n, clauses):
+    need(type(n) is int and n >= 1, 'CNF axis count')
+    need(all(len(clause) <= 3 and all(type(lit) is int and 1 <= abs(lit) <= n for lit in clause)
+             for clause in clauses), 'CNF literal or clause extent')
+    formula = balanced('and', [balanced('or', clause, False) for clause in clauses], True)
+    word = formula_word(formula)
+    need(len(word) <= 50 * max(1, len(clauses)) ** 2, 'proved group-program bound')
+    return word
+
+
+def evaluate(word, assignment):
+    p = IDENTITY
+    for variable, zero, one in word:
+        step = one if variable is not None and assignment >> variable & 1 else zero
+        p = compose(step, p)
+    return p
+
+
+def swaps(permutation):
+    seen = set()
+    result = []
+    for i in range(5):
+        if i in seen:
+            continue
+        seen.add(i)
+        j = permutation[i]
+        while j != i:
+            result.append((i, j))
+            seen.add(j)
+            j = permutation[j]
+    return result
+
+
+def controlled_swap(i, j, generator):
+    """Swap at native sign -1 and act as identity at sign +1."""
+    return [{'op': 'add', 'src': j, 'dst': i, 'coefficient': -1},
+            {'op': 'add', 'src': i, 'dst': j, 'coefficient': '1/2'},
+            {'op': 'query', 'src': i, 'dst': j, 'generator': generator, 'coefficient': '-1/2'},
+            {'op': 'apply', 'dst': i, 'generator': generator},
+            {'op': 'add', 'src': j, 'dst': i}]
+
+
+def lower_word(n, word):
+    generators = {}
+    for i in range(n):
+        linear = [0] * n
+        linear[i] = 2
+        generators['Z' + str(i + 1)] = {'matrix_rows': [1 << j for j in range(n)], 'offset': 0,
+                                       'phase': 0, 'linear_Z4': linear, 'quadratic_rows': [0] * n}
+    code = []
+    for variable, zero, one in word:
+        code.extend({'op': 'swap', 'src': i, 'dst': j} for i, j in swaps(zero))
+        if variable is not None:
+            for i, j in swaps(compose(one, inverse(zero))):
+                code.extend(controlled_swap(i, j, 'Z' + str(variable + 1)))
+        else:
+            need(zero == one, 'constant group instruction')
+    need(len(code) <= 24 * len(word), 'proved register instruction bound')
+    return {'axes': n, 'roles': 5, 'generators': generators, 'program': code, 'reference': []}
+
+
+def cnf_problem(n, clauses):
+    return lower_word(n, cnf_word(n, clauses))
diff --git a/research/native-tensor-cutoff/source/BOUNDARY.json b/research/native-tensor-cutoff/source/BOUNDARY.json
new file mode 100644
index 0000000000..5b017fcb9b
--- /dev/null
+++ b/research/native-tensor-cutoff/source/BOUNDARY.json
@@ -0,0 +1,13 @@
+{
+  "schema": "four-base-packet-v1",
+  "status": "immutable-boundary-ABI; first actual descriptor being generated",
+  "source_base": "4c0a359d88f22f05189d51f48387750b801a45d4",
+  "actual_event": {"provider": "FOUR/base", "dispatch_tick": 1665, "stage": 3, "replica": 73, "orientation": "backward", "event_index": 8814, "event": ["climb", "A", 57, 310, 255, 3], "family": 65689},
+  "node": {"e": 147, "f": 2, "t": 1, "child_width": 6, "remaining_row_stock": 2},
+  "packet_fields": ["remaining_row", "child_active_bits", "inactive_core_bits", "remainder_bits", "compact", "prefix", "suffix", "dirty"],
+  "return_labels": ["provider", "dispatch_tick", "event_index", "orientation", "family", "cover_matrix_rows", "return_site"],
+  "charts": "source-derived right/left 9-bit affine-Z4 recipes, lifted columnwise after the actual source rho and cover view; no host-supplied chart accepted",
+  "schedule": ["validate_and_enter_source_view", "apply_right_and_pack", "one_child_C_power_rf", "unpack_and_apply_left", "restore_source_view_and_labels"],
+  "child_contract": "Exactly one abstract C tensor child on child_active_bits, independently on every complete remaining field. No allocation/rewind/time claim. Rank zero emits no child.",
+  "task07_boundary": "Treat descriptor JSON and tagged packet fields as immutable saved continuation data. Physical compact role inventory and fixed-tape serialization remain task07's responsibility."
+}
diff --git a/research/native-tensor-cutoff/source/NOTICE.md b/research/native-tensor-cutoff/source/NOTICE.md
new file mode 100644
index 0000000000..e82bfef530
--- /dev/null
+++ b/research/native-tensor-cutoff/source/NOTICE.md
@@ -0,0 +1,38 @@
+# Attribution
+
+Jose Manuel (`jmbarrancoml`) prepared the new sequential interpreter,
+selected monomial compiler, checks and written composition with substantial
+OpenAI Codex assistance. We use the repository's Apache-2.0 license.
+
+Douglas Colkitt's compact-control movement/layout construction and the
+retained OpenAI framework supply the dirty-control identity, original
+guard, exceptional repair method, record-paid arithmetic and asymptotic
+domain. We implement that method; we claim no new generic guard or sorting
+algorithm. The source-authenticated address audit remains a separate oracle.
+
+The existing carry and guard audits retain their credit: John-Michael
+Smith's PR763, bbMisk's PR1219 and later-source audit, Hanson Sun's PR1247,
+Sagar Thakrar's PR1475, and the PR1603 lineage. Our new path uses the original
+predicate and does not replace their refinements.
+
+The selected scalar word, native Clifford compilation, frame recipes,
+owner maps and T16 packing retain the contributors and disclosures in
+`research/complex-sw4-frame8/NOTICE.md` and the gauge44/T16 notices linked
+from `research/joint-query/NOTICE.md`. We reuse Ali Romman's retained source
+loader to read the frozen local archive. It authenticates the five source
+members and does not run the exploratory producer.
+
+The unchanged selected `clifford_exact.py` interpreter supplies the exact
+single-column comparison. The new compiler independently lowers its
+serialized affine matrices and follows its strict-upper quadratic convention.
+We compare both selected literal programs and their source hashes, rather
+than substituting the nearby R492 predecessor.
+
+PR2234 by Jose Manuel, head `d047ef86fbc5b1614d3d8e2b8d3441413beab73f`, supplies
+a pending written completed ordinary-interchange construction. We import
+none of its code. The physical tests use the elementary completed supplier;
+the faster complexity statement names the ordinary contract as a premise.
+
+`SOURCES.json` pins retained code, proof notes and archives. We have not
+merged or closed predecessor work, changed the selected frontier, or obtained
+independent human or proof-assistant verification.
diff --git a/research/native-tensor-cutoff/source/RIGHT-RECIPE.json b/research/native-tensor-cutoff/source/RIGHT-RECIPE.json
new file mode 100644
index 0000000000..1b5473743f
--- /dev/null
+++ b/research/native-tensor-cutoff/source/RIGHT-RECIPE.json
@@ -0,0 +1,37 @@
+{
+  "matrix_rows": [
+    6,
+    64,
+    384,
+    5,
+    34,
+    32,
+    8,
+    48,
+    256
+  ],
+  "offset": 426,
+  "quadratic_rows": [
+    4,
+    38,
+    39,
+    0,
+    0,
+    6,
+    256,
+    256,
+    448
+  ],
+  "linear_Z4": [
+    2,
+    1,
+    3,
+    0,
+    0,
+    2,
+    0,
+    0,
+    1
+  ],
+  "phase": 1
+}
diff --git a/research/native-tensor-cutoff/source/compact.py b/research/native-tensor-cutoff/source/compact.py
new file mode 100644
index 0000000000..60bc206c78
--- /dev/null
+++ b/research/native-tensor-cutoff/source/compact.py
@@ -0,0 +1,203 @@
+"""Retained dirty compact-control word with a sequential repair interpreter.
+
+The algebra and original guard are Douglas Colkitt's retained construction.
+This interpreter supplies payload movement, keyed repair and scratch closure.
+"""
+from dataclasses import dataclass
+from math import prod
+
+from streams import (Tape,need,copy,bit_key,key_value,stable_radix,
+                     digit_permutation,flip_digit)
+
+
+@dataclass(frozen=True)
+class Layout:
+    fields: tuple
+    record_bits: int
+
+    @property
+    def bits(self):return sum(width for _,width in self.fields)
+    @property
+    def records(self):return 1<<self.bits
+    @property
+    def names(self):return tuple(name for name,_ in self.fields)
+
+    def width(self,name):return dict(self.fields)[name]
+
+    def position(self,name,low_bit=0):
+        before=0
+        for field,width in self.fields:
+            if field==name:
+                need(0<=low_bit<width,"field bit extent")
+                return before+width-1-low_bit
+            before+=width
+        raise ValueError("unknown field")
+
+    def decode(self,index):
+        need(0<=index<self.records,"full record address")
+        out={}
+        for name,width in reversed(self.fields):
+            out[name]=index% (1<<width);index>>=width
+        return out
+
+    def encode(self,state):
+        out=0
+        for name,width in self.fields:
+            need(0<=state[name]<1<<width,"encoded field extent")
+            out=(out<<width)+state[name]
+        return out
+
+
+@dataclass(frozen=True)
+class Compact:
+    n: int
+    K: int
+    G: int
+    rho: int
+    source: str | None
+    target: str
+    late: bool=False
+
+    def validate(self,layout):
+        need(self.n>=1 and self.K>=1 and self.G>=1 and 0<=self.rho<self.K,"compact domain")
+        need(layout.width(self.target)==(self.n+1)*self.K,"wide target extent")
+        need(all(layout.width(name)==self.n*self.G for name in ("u","t","b")),
+             "complete equal compact fields")
+        need(layout.names.index("u")<layout.names.index(self.target) and
+             layout.names.index("t")<layout.names.index(self.target)<layout.names.index("b"),
+             "front and back compact placement")
+        if self.source is not None:
+            need(layout.width(self.source)==(self.n+1)*self.K,"wide source extent")
+            need((layout.names.index(self.source)>layout.names.index(self.target))==self.late,
+                 "declared source order")
+        else:need(not self.late,"constant toggle uses early routine")
+
+    def select(self,value):
+        return sum(((value>>(self.rho+i*self.K))&1)<<(i*self.G) for i in range(self.n))
+
+    def mask(self,value,compact=False):
+        return sum(((value>>(i*self.G if compact else self.rho+i*self.K))&1)
+                   <<(self.rho+i*self.K) for i in range(self.n))
+
+    def operations(self):
+        ops=[]
+        def rot(target,controls,kind,sign=1):ops.append(("rotate",target,controls,kind,sign))
+        def load(front,controls,kind,sign=1):
+            ops.append(("swap",front,"b"));rot("b",controls,kind,sign);ops.append(("swap",front,"b"))
+        def flip(control,is_compact=False):
+            tag="compact" if is_compact else "wide"
+            controls=(() if control is None else (control,))+("t",)
+            rot(self.target,controls,"first_"+tag)
+            load("t",(self.target,),"selected_y")
+            rot(self.target,controls,"second_"+tag)
+            controls=(() if control is None else (control,))+(self.target,)
+            load("t",controls,"original_"+tag,-1)
+        if self.late:
+            flip("u",True);load("u",(self.source,),"selected_x")
+            flip("u",True);load("u",(self.source,),"selected_x",-1)
+        else:flip(self.source)
+        return tuple(ops)
+
+    def offset(self,state,operation):
+        _,target,controls,kind,sign=operation
+        if kind=="selected_y":return sign*self.select(state[self.target])
+        if kind=="selected_x":return sign*self.select(state[self.source])
+        compact=kind.endswith("compact")
+        control="u" if compact else self.source
+        bits=[1 if control is None else (state[control]>>(i*self.G if compact else self.rho+i*self.K))&1
+              for i in range(self.n)]
+        if kind.startswith("original"):
+            value=state[self.target]^sum(b<<(self.rho+i*self.K) for i,b in enumerate(bits))
+            return sign*self.select(value)
+        B=1<<self.G
+        return sign*sum(bits[i]*(2*((state["t"]>>(i*self.G))&(B-1)) if kind.startswith("first")
+                               else 1-2*((state["t"]>>(i*self.G))&(B-1)))
+                       <<(self.rho+i*self.K) for i in range(self.n))
+
+    def execute(self,state,layout,inverse=False):
+        out=dict(state)
+        for op in reversed(self.operations()) if inverse else self.operations():
+            if op[0]=="swap":out[op[1]],out[op[2]]=out[op[2]],out[op[1]]
+            else:out[op[1]]=(out[op[1]]+(-1 if inverse else 1)*self.offset(out,op))%(1<<layout.width(op[1]))
+        return out
+
+    def ideal(self,state,highest=False):
+        out=dict(state);n=self.n+int(highest)
+        value=(sum(1<<(self.rho+i*self.K) for i in range(n)) if self.source is None else
+               sum(((state[self.source]>>(self.rho+i*self.K))&1)<<(self.rho+i*self.K) for i in range(n)))
+        out[self.target]^=value
+        return out
+
+    def bad(self,state):
+        B=1<<self.G;upper=(1<<(self.K-1))-2*B;mask=(1<<(self.K-1))-1
+        return any(((state["t"]>>(i*self.G))&(B-1))==B-1 or
+                   not 2*B<=((state[self.target]>>(self.rho+i*self.K+1))&mask)<upper or
+                   (self.late and ((state["u"]>>(i*self.G))&(B-1))==B-1)
+                   for i in range(self.n))
+
+
+def ordinary(source,layout,first,second):
+    """Completed elementary supplier used in tests; retain the abstract call bill."""
+    width=layout.width(first);need(width==layout.width(second),"equal ordinary chunks")
+    source.meter.ordinary_calls.append({"width":width,"volume":len(source.data)})
+    for bit in range(width):
+        a,b=sorted((layout.position(first,bit),layout.position(second,bit)))
+        source=digit_permutation(source,layout.bits,a,b,layout.record_bits,(0,2,1,3))
+    return source
+
+
+def rotate(source,layout,word,op):
+    _,target,controls,_,_=op;at=layout.names.index(target)
+    need(all(layout.names.index(name)<at for name in controls),"all rotation controls precede target")
+    before=sum(width for _,width in layout.fields[:at]);after=sum(width for _,width in layout.fields[at+1:])
+    width=layout.width(target);radix=1<<width;suffix=(1<<after)*layout.record_bits
+    source.rewind();left=Tape(source.meter);right=Tape(source.meter);out=Tape(source.meter)
+    for prefix in range(1<<before):
+        state=layout.decode(prefix<<(width+after));cut=word.offset(state,op)%radix
+        source.meter.control_evaluations+=1
+        copy(source,left,(radix-cut)*suffix);copy(source,right,cut*suffix)
+    source.finish();left.rewind();right.rewind()
+    for prefix in range(1<<before):
+        state=layout.decode(prefix<<(width+after));cut=word.offset(state,op)%radix
+        source.meter.control_evaluations+=1
+        copy(right,out,cut*suffix);copy(left,out,(radix-cut)*suffix)
+    left.finish();right.finish();left.erase();right.erase();source.erase();out.rewind()
+    source.meter.rotation_passes+=1
+    return out
+
+
+def repair(source,layout,word,wrong_inverse=False):
+    source.rewind();good=Tape(source.meter);bad=Tape(source.meter);holes=Tape(source.meter)
+    for index in range(layout.records):
+        state=layout.decode(index);exception=word.bad(state);holes.write(bytes((int(exception),)))
+        if exception:
+            old=state if wrong_inverse else word.execute(state,layout,True)
+            destination=layout.encode(word.ideal(old))
+            bad.write(bit_key(destination,layout.bits));copy(source,bad,layout.record_bits)
+            source.meter.repair_records+=1;source.meter.control_evaluations+=1
+        else:copy(source,good,layout.record_bits)
+    source.finish();source.erase();bad.rewind();good.rewind();holes.rewind()
+    bad=stable_radix(bad,layout.bits,layout.record_bits);out=Tape(source.meter)
+    for index in range(layout.records):
+        if holes.read(1)[0]:
+            destination=key_value(bad.read(layout.bits))
+            need(destination==index,"sorted exceptional keys fill precisely the marked holes")
+            copy(bad,out,layout.record_bits)
+        else:copy(good,out,layout.record_bits)
+    for tape in (bad,good,holes):tape.finish();tape.erase()
+    out.rewind();return out
+
+
+def execute(source,layout,word,omit_repair=False,wrong_inverse=False):
+    word.validate(layout);need(len(source.data)==layout.records*layout.record_bits,"complete record rectangle")
+    for op in word.operations():
+        source=ordinary(source,layout,op[1],op[2]) if op[0]=="swap" else rotate(source,layout,word,op)
+    if not omit_repair:source=repair(source,layout,word,wrong_inverse)
+    y=layout.position(word.target,word.rho+word.n*word.K)
+    if word.source is None:source=flip_digit(source,layout.bits,y,layout.record_bits)
+    else:
+        x=layout.position(word.source,word.rho+word.n*word.K);a,b=sorted((x,y))
+        mapping=(0,1,3,2) if x<y else (0,3,2,1)
+        source=digit_permutation(source,layout.bits,a,b,layout.record_bits,mapping)
+    need(source.head==0,"completed compact output origin")
+    return source
diff --git a/research/native-tensor-cutoff/source/monomial.py b/research/native-tensor-cutoff/source/monomial.py
new file mode 100644
index 0000000000..5fa4494167
--- /dev/null
+++ b/research/native-tensor-cutoff/source/monomial.py
@@ -0,0 +1,102 @@
+"""Columnwise lift of fixed binary affine maps and Gaussian unit phases."""
+from streams import Tape,need,copy,digit_permutation,flip_digit
+from compact import Compact,execute
+
+
+def binary_word(recipe):
+    rows=list(recipe["matrix_rows"]);m=len(rows);reduction=[]
+    need(0<m<=73 and all(0<=row<1<<m for row in rows),"fixed binary matrix extent")
+    for j in range(m):
+        p=next((i for i in range(j,m) if rows[i]>>j&1),None)
+        need(p is not None,"invertible monomial linear map")
+        if p!=j:
+            for target,source in ((j,p),(p,j),(j,p)):
+                rows[target]^=rows[source];reduction.append(("add",target,source))
+        for i in range(m):
+            if i!=j and rows[i]>>j&1:
+                rows[i]^=rows[j];reduction.append(("add",i,j))
+    need(rows==[1<<i for i in range(m)],"complete binary elimination")
+    return tuple(reversed(reduction))+tuple(("flip",i,-1) for i in range(m) if recipe["offset"]>>i&1)
+
+
+def column_phase(recipe,x):
+    m=len(recipe["matrix_rows"])
+    # Raw retained recipes can store symmetric/diagonal entries. The source
+    # qvalue convention uses only the strict upper part; alpha holds diagonals.
+    value=sum(recipe["linear_Z4"][i] for i in range(m) if x>>i&1)
+    value+=2*sum(((recipe["quadratic_rows"][i]>>(i+1))&(x>>(i+1))).bit_count()
+                 for i in range(m) if x>>i&1)
+    return value%4
+
+
+def column_map(recipe,x):
+    return recipe["offset"]^sum(((row&x).bit_count()%2)<<i
+                                for i,row in enumerate(recipe["matrix_rows"]))
+
+
+def columns(state,m,f,K,rho):
+    return tuple(sum(((state["v"+str(i)]>>(rho+j*K))&1)<<i for i in range(m)) for j in range(f))
+
+
+def tensor_phase(recipe,state,f,K,rho,omit_tensor_constant=False):
+    constant=recipe["phase"]*(1 if omit_tensor_constant else f)
+    return (constant+sum(column_phase(recipe,x)
+                        for x in columns(state,len(recipe["matrix_rows"]),f,K,rho)))%4
+
+
+def negate(bits):
+    """Two's-complement negation in least-significant-bit stream order."""
+    carry=1;out=bytearray()
+    for bit in bits:
+        value=(1-bit)+carry;out.append(value&1);carry=value>>1
+    return out
+
+
+def phase_pass(source,layout,recipe,f,K,rho,coefficient_bits,inverse=False,
+               omit_tensor_constant=False):
+    need(coefficient_bits>=2 and layout.record_bits%(2*coefficient_bits)==0,"Gaussian record extent")
+    source.rewind();out=Tape(source.meter);real=Tape(source.meter);imag=Tape(source.meter)
+    def emit(tape,negative):
+        if negative:
+            carry=1
+            for _ in range(coefficient_bits):
+                value=(1-tape.read(1)[0])+carry
+                out.write(bytes((value&1,)));carry=value>>1
+        else:copy(tape,out,coefficient_bits)
+        tape.finish()
+    for index in range(layout.records):
+        phase=tensor_phase(recipe,layout.decode(index),f,K,rho,omit_tensor_constant)
+        if inverse:phase=-phase%4
+        source.meter.control_evaluations+=1
+        for _ in range(layout.record_bits//(2*coefficient_bits)):
+            copy(source,real,coefficient_bits);copy(source,imag,coefficient_bits)
+            real.rewind();imag.rewind()
+            if phase==0:emit(real,False);emit(imag,False)
+            elif phase==1:emit(imag,True);emit(real,False)
+            elif phase==2:emit(real,True);emit(imag,True)
+            else:emit(imag,False);emit(real,True)
+            real.erase();imag.erase()
+    source.finish();source.erase();out.rewind();return out
+
+
+def execute_monomial(source,layout,recipe,f,K,G,rho,coefficient_bits,inverse=False,
+                     omit_tensor_constant=False):
+    need(f>=1,"positive tensor width");word=binary_word(recipe)
+    if not inverse:
+        source=phase_pass(source,layout,recipe,f,K,rho,coefficient_bits,
+                          omit_tensor_constant=omit_tensor_constant)
+    for kind,i,k in reversed(word) if inverse else word:
+        target="v"+str(i);control=None if kind=="flip" else "v"+str(k)
+        if f>1:
+            source=execute(source,layout,Compact(f-1,K,G,rho,control,target,
+                           False if control is None else k>i))
+        elif control is None:
+            source=flip_digit(source,layout.bits,layout.position(target,rho),layout.record_bits)
+        else:
+            a,b=layout.position(control,rho),layout.position(target,rho)
+            mapping=(0,1,3,2) if a<b else (0,3,2,1)
+            source=digit_permutation(source,layout.bits,min(a,b),max(a,b),layout.record_bits,mapping)
+    if inverse:
+        source=phase_pass(source,layout,recipe,f,K,rho,coefficient_bits,True,
+                          omit_tensor_constant)
+    return source
diff --git a/research/native-tensor-cutoff/source/streams.py b/research/native-tensor-cutoff/source/streams.py
new file mode 100644
index 0000000000..61542ce4c9
--- /dev/null
+++ b/research/native-tensor-cutoff/source/streams.py
@@ -0,0 +1,115 @@
+"""Sequential bit-stream simulator with charged contiguous transfers.
+
+Bulk methods abbreviate consecutive tape transitions; they charge each bit.
+Payload destinations are append-only. Random lookup is confined to controls.
+"""
+from dataclasses import dataclass,field
+
+
+def need(condition,message):
+    if not condition:
+        raise ValueError(message)
+
+
+@dataclass
+class Meter:
+    reads: int=0
+    writes: int=0
+    moves: int=0
+    erases: int=0
+    control_evaluations: int=0
+    digit_passes: int=0
+    rotation_passes: int=0
+    radix_passes: int=0
+    repair_records: int=0
+    ordinary_calls: list=field(default_factory=list)
+
+
+class Tape:
+    def __init__(self,meter,data=b""):
+        self.meter=meter;self.data=bytearray(data);self.head=0
+
+    def read(self,size):
+        need(0<=size<=len(self.data)-self.head,"sequential read boundary")
+        value=self.data[self.head:self.head+size];self.head+=size
+        self.meter.reads+=size;self.meter.moves+=size
+        return value
+
+    def write(self,value):
+        need(self.head==len(self.data),"append-only output")
+        self.data.extend(value);self.head+=len(value)
+        self.meter.writes+=len(value);self.meter.moves+=len(value)
+
+    def rewind(self):
+        self.meter.moves+=self.head;self.head=0
+
+    def finish(self):
+        need(self.head==len(self.data),"complete sequential consumption")
+
+    def erase(self):
+        self.rewind();size=len(self.data)
+        self.meter.erases+=size;self.meter.moves+=2*size
+        self.data.clear();self.head=0
+
+
+def copy(source,target,size):
+    target.write(source.read(size))
+
+
+def bit_key(value,width):
+    need(0<=value<1<<width,"binary control key extent")
+    return bytes((value>>i)&1 for i in range(width))
+
+
+def key_value(bits):
+    need(all(b in (0,1) for b in bits),"binary control encoding")
+    return sum(b<<i for i,b in enumerate(bits))
+
+
+def digit_permutation(source,total_bits,first,second,record_bits,mapping):
+    """Two physical address-bit positions, numbered from the left."""
+    need(0<=first<second<total_bits,"two ordered bit fields")
+    need(sorted(mapping)==list(range(4)),"four-state permutation")
+    middle=1<<(second-first-1);suffix=(1<<(total_bits-second-1))*record_bits
+    slab=4*middle*suffix;need(len(source.data)%slab==0,"complete digit slabs")
+    source.rewind();out=Tape(source.meter);buckets=[Tape(source.meter) for _ in range(4)]
+    inverse=[mapping.index(i) for i in range(4)]
+    for _prefix in range(len(source.data)//slab):
+        for a in range(2):
+            for _mid in range(middle):
+                for b in range(2):copy(source,buckets[2*a+b],suffix)
+        for bucket in buckets:bucket.rewind()
+        for a in range(2):
+            for _mid in range(middle):
+                for b in range(2):copy(buckets[inverse[2*a+b]],out,suffix)
+        for bucket in buckets:bucket.finish();bucket.erase()
+    source.finish();source.erase();out.rewind();source.meter.digit_passes+=1
+    return out
+
+
+def flip_digit(source,total_bits,position,record_bits):
+    suffix=(1<<(total_bits-position-1))*record_bits;slab=2*suffix
+    need(len(source.data)%slab==0,"complete bit-flip slabs")
+    source.rewind();out=Tape(source.meter);left=Tape(source.meter);right=Tape(source.meter)
+    for _ in range(len(source.data)//slab):
+        copy(source,left,suffix);copy(source,right,suffix)
+        left.rewind();right.rewind();copy(right,out,suffix);copy(left,out,suffix)
+        left.finish();right.finish();left.erase();right.erase()
+    source.finish();source.erase();out.rewind();source.meter.digit_passes+=1
+    return out
+
+
+def stable_radix(source,key_bits,payload_bits):
+    """LSD binary partition and concatenation; no sorting or seek oracle."""
+    width=key_bits+payload_bits;need(len(source.data)%width==0,"complete keyed records")
+    for position in range(key_bits):
+        source.rewind();buckets=[Tape(source.meter),Tape(source.meter)]
+        for _ in range(len(source.data)//width):
+            key=source.read(key_bits)
+            bucket=buckets[key[position]]
+            bucket.write(key);copy(source,bucket,payload_bits)
+        source.finish();source.erase();out=Tape(source.meter)
+        for bucket in buckets:
+            bucket.rewind();copy(bucket,out,len(bucket.data));bucket.finish();bucket.erase()
+        out.rewind();source=out;source.meter.radix_passes+=1
+    return source
diff --git a/research/native-tensor-cutoff/verify.py b/research/native-tensor-cutoff/verify.py
new file mode 100644
index 0000000000..56ac95ef81
--- /dev/null
+++ b/research/native-tensor-cutoff/verify.py
@@ -0,0 +1,347 @@
+"""Check the proof's algebra, complete circuits, source adapter and controls."""
+import copy
+import hashlib
+import itertools
+import json
+from pathlib import Path
+import random
+import sys
+
+HERE = Path(__file__).resolve().parent
+sys.path.insert(0, str(HERE))
+from exact import QI, need, unit
+from native import Native, act, character_tuple, gram_factor
+from native_identity import decide, endpoint, validate
+import check_certificate as checker
+from examples import cnf_problem, diagonal, late_projector, source_conjugation
+import reversible_cnf as reversible
+
+def authenticated_sources():
+    pins = json.loads((HERE / 'SOURCE-PINS.json').read_text())
+    for row in pins['files']:
+        data = (HERE / row['retained']).read_bytes()
+        need(hashlib.sha256(data).hexdigest() == row['sha256'], 'source SHA256 mismatch')
+        need(len(data) == row['bytes'], 'source length mismatch')
+    sys.path.insert(0, str(HERE / 'source'))
+    import monomial
+    return monomial, len(pins['files'])
+
+
+def statistics(points, n):
+    return ((len(points) % 4,) + tuple(sum((x >> i) & 1 for x in points) % 4 for i in range(n))
+            + tuple(sum(((x >> i) & 1) * ((x >> j) & 1) for x in points) % 2
+                    for i in range(n) for j in range(i + 1, n)))
+
+
+def gram_checks():
+    count = 0
+    for n in range(1, 6):
+        entries = [(i, j) for i in range(n) for j in range(i, n)]
+        for mask in range(1 << len(entries)):
+            rows = [0] * n
+            for k, (i, j) in enumerate(entries):
+                if mask >> k & 1:
+                    rows[i] |= 1 << j
+                    rows[j] |= 1 << i
+            vectors = gram_factor(rows)
+            need(len(vectors) <= n + 1, 'Gram factor width')
+            actual = [sum((sum(((v >> i) & 1) * ((v >> j) & 1) for v in vectors) % 2) << j
+                          for j in range(n)) for i in range(n)]
+            need(actual == rows, 'literal Gram product')
+            count += 1
+    return count
+
+
+def character_checks(rng):
+    count = 0
+    for n in range(1, 4):
+        for first in itertools.product(range(4), repeat=n + 1):
+            for tail in itertools.product(range(2), repeat=n * (n - 1) // 2):
+                character = first + tail
+                points = character_tuple(n, character)
+                need(statistics(points, n) == character, 'complete phase-character statistics')
+                need(points[:n + 1] == [0] + [1 << i for i in range(n)], 'affine basis retained')
+                need(2 * n + 4 <= len(points) <= 2 * n + 7, 'four-width cutoff')
+                count += 1
+    large = 0
+    for n, trials in ((4, 32), (9, 32), (17, 32), (73, 4)):
+        for _ in range(trials):
+            ch = tuple(rng.randrange(4) for _ in range(n + 1)) + tuple(rng.randrange(2) for _ in range(n * (n - 1) // 2))
+            points = character_tuple(n, ch, 2 * n + 8)
+            need(statistics(points, n) == ch and len(points) >= 2 * n + 8, 'later-window phase realization')
+            large += 1
+    return count, large
+
+
+def random_native(n, rng):
+    rows = [1 << i for i in range(n)]
+    for _ in range(4 * n):
+        i, j = rng.randrange(n), rng.randrange(n)
+        if i != j:
+            rows[i] ^= rows[j]
+    return Native(tuple(rows), rng.randrange(1 << n), rng.randrange(4),
+                  tuple(rng.randrange(4) for _ in range(n)),
+                  tuple(rng.randrange(1 << n) & ~((1 << (i + 1)) - 1) for i in range(n)))
+
+
+def group_checks(rng):
+    one = [Native((1,), t, c, (a,), (0,)) for t in range(2) for c in range(4) for a in range(4)]
+    pairs = [(g, h) for g in one for h in one]
+    pairs += [(random_native(n, rng), random_native(n, rng)) for n in (2, 3, 4, 9) for _ in range(32)]
+    point_checks = 0
+    for g, h in pairs:
+        p, inv = g.compose(h), g.inv()
+        a, b = checker.normalize(g.json(), g.n), checker.normalize(h.json(), h.n)
+        need(checker.compose(a, b) == checker.normalize(p.json(), g.n), 'separate composition formulas')
+        need(checker.inverse(a) == checker.normalize(inv.json(), g.n), 'separate inverse formulas')
+        need(g.compose(inv) == Native.identity(g.n) == inv.compose(g), 'two-sided inverse')
+        for x in range(1 << g.n):
+            need(p.image(x) == g.image(h.image(x)), 'literal composed address')
+            need(p.exponent(x) == (h.exponent(x) + g.exponent(h.image(x))) % 4, 'literal composed phase')
+            need(inv.image(g.image(x)) == x and (g.exponent(x) + inv.exponent(g.image(x))) % 4 == 0,
+                 'literal inverse phase')
+            point_checks += 1
+    return len(pairs), point_checks
+
+
+def literal_from_algebra(rows, input_role, points):
+    out = []
+    for row in rows:
+        result = {}
+        for (i, g), value in row.items():
+            if i == input_role:
+                key = tuple(g.image(x) for x in points)
+                checker.accumulate(result, key, value * unit(sum(g.exponent(x) for x in points)))
+        out.append(result)
+    return out
+
+
+def circuit_checks(rng):
+    checked, positives, negatives, basis_checks = 0, 0, 0, 0
+    for trial in range(120):
+        n = 1 + trial % 3
+        g, h = random_native(n, rng), random_native(n, rng)
+        gs = {'G': g.json(), 'H': h.json(), 'K': g.compose(h).json()}
+        prefix = []
+        for _ in range(5):
+            op = rng.choice(['add', 'query', 'apply', 'scale', 'swap'])
+            ins = {'op': op, 'dst': rng.randrange(3)}
+            if op in ('add', 'query', 'swap'):
+                ins['src'] = rng.randrange(3)
+            if op in ('apply', 'query'):
+                ins.update(generator=rng.choice(['G', 'H']), inverse=bool(rng.randrange(2)))
+            if op in ('add', 'query', 'scale'):
+                ins['coefficient'] = rng.choice([0, 1, -1, '1/2', [0, 1], ['1/3', '-1/2']])
+            prefix.append(ins)
+        left = prefix + [{'op': 'apply', 'dst': 1, 'generator': 'H'}, {'op': 'apply', 'dst': 1, 'generator': 'G'}]
+        right = prefix + [{'op': 'apply', 'dst': 1, 'generator': 'K'}]
+        if trial % 2:
+            right.append({'op': 'add', 'src': 0, 'dst': 2})
+        problem = {'axes': n, 'roles': 3, 'generators': gs, 'program': left, 'reference': right}
+        cert = decide(problem)
+        checker.check(problem, cert)
+        if cert['status'] == 'COUNTEREXAMPLE':
+            negatives += 1
+        else:
+            positives += 1
+        checked += 1
+        generators = validate(problem)
+        formal, _ = endpoint(problem, left, generators)
+        raw = checker.problem_data(problem)
+        for width in (1, 2):
+            for points in itertools.product(range(1 << n), repeat=width):
+                for source in range(3):
+                    direct = checker.literal_endpoint(problem, left, raw, source, points, 100000)
+                    need(direct == literal_from_algebra(formal, source, points), 'complete literal endpoint differential')
+                    basis_checks += 1
+    need(positives >= 60 and negatives >= 30, 'nontrivial positive and negative coverage')
+    return checked, positives, negatives, basis_checks
+
+
+def source_checks(monomial):
+    raw = json.loads((HERE / 'source/RIGHT-RECIPE.json').read_text())
+    g = Native.parse(raw, 9)
+    for x in range(512):
+        need(g.image(x) == monomial.column_map(raw, x), 'actual native address convention')
+        need(g.exponent(x) == (raw['phase'] + monomial.column_phase(raw, x)) % 4,
+             'actual native phase convention')
+    probes = 0
+    for f in (1, 2, 22, 23, 24, 25):
+        points = [(17 * j + 7 * f) % 512 for j in range(f)]
+        state = {'v' + str(i): sum(((points[j] >> i) & 1) << (1 + 2 * j) for j in range(f)) for i in range(9)}
+        need(monomial.tensor_phase(raw, state, f, 2, 1) == sum(g.exponent(x) for x in points) % 4,
+             'source constant phase scales with width')
+        probes += 1
+    good, bad = source_conjugation(), source_conjugation(True)
+    need(decide(good)['status'] == 'IDENTITY_ALL_POSITIVE_WIDTHS', 'actual conjugation identity')
+    cert = decide(bad)
+    need(cert['status'] == 'COUNTEREXAMPLE' and len(cert['input_points']) % 2 == 1, 'constant omission needs odd witness')
+    checker.check(good, decide(good)); checker.check(bad, cert)
+    gs = checker.problem_data(bad)
+    for x in range(512):
+        points = [x, x ^ 511]
+        a = checker.literal_endpoint(bad, bad['program'], gs, 0, points, 100000)
+        b = checker.literal_endpoint(bad, bad['reference'], gs, 0, points, 100000)
+        need(a == b, 'phase mutation is invisible at even width')
+    return {'source_addresses': 512, 'tensor_phase_probes': probes, 'even_width_blind_cases': 512,
+            'failure_width': len(cert['input_points']), 'discrepancy': cert['discrepancy']}
+
+
+def projector_checks():
+    vanished = 0
+    for n in range(1, 5):
+        problem = late_projector(n)
+        gs = checker.problem_data(problem)
+        for f in range(1, n):
+            for points in itertools.product(range(1 << n), repeat=f):
+                got = checker.literal_endpoint(problem, problem['program'], gs, 0, points, 100000)
+                need(got == [{}], 'complete below-rank projector vanishing')
+                vanished += 1
+        points = tuple(1 << i for i in range(n))
+        got = checker.literal_endpoint(problem, problem['program'], gs, 0, points, 100000)
+        need(got == [{points: QI(1)}], 'first possible projector width is attained')
+    # Each omitted residue has a central projector that only it detects.
+    for residue in range(4):
+        for f in range(1, 13):
+            value = sum((unit(-residue * c) * unit(f * c) for c in range(4)), QI())
+            need(value == (4 if f % 4 == residue else 0), 'four-width necessity')
+    return vanished, 48
+
+
+def cnf_checks(rng):
+    formulas, assignments, unsat = 0, 0, 0
+    for n in range(1, 6):
+        for trial in range(16):
+            clauses = [[rng.choice((-1, 1)) * rng.randint(1, n) for _ in range(rng.randrange(4))]
+                       for _ in range(rng.randrange(1, 8))]
+            if trial == 0:
+                clauses = [[1], [-1]]
+            word = reversible.cnf_word(n, clauses)
+            sat = False
+            for x in range(1 << n):
+                value = all(any(bool(x >> (abs(lit) - 1) & 1) == (lit > 0) for lit in clause) for clause in clauses)
+                sat |= value
+                need(reversible.evaluate(word, x) == (reversible.A if value else reversible.IDENTITY),
+                     'complete CNF permutation truth table')
+                assignments += 1
+            unsat += not sat
+            formulas += 1
+    return formulas, assignments, unsat
+
+
+def reversible_checks():
+    need(reversible.compose(reversible.inverse(reversible.B),
+         reversible.compose(reversible.inverse(reversible.A), reversible.compose(reversible.B, reversible.A)))
+         == reversible.C, 'five-cycle commutator')
+    pairs, columns = 0, 0
+    for zero in itertools.permutations(range(5)):
+        for one in (reversible.IDENTITY, reversible.A, reversible.B, reversible.C):
+            problem = reversible.lower_word(1, [(0, zero, one)])
+            gs = checker.problem_data(problem)
+            need(all(ins['op'] != 'scale' and
+                     (ins['op'] not in ('add', 'query', 'swap') or ins['src'] != ins['dst'])
+                     for ins in problem['program']), 'only invertible dirty-role operations')
+            for x in (0, 1):
+                for i in range(5):
+                    out = checker.literal_endpoint(problem, problem['program'], gs, i, [x], 100000)
+                    expected = [{} for _ in range(5)]
+                    expected[(one if x else zero)[i]][(x,)] = QI(1)
+                    need(out == expected, 'literal conditional permutation on every dirty column')
+                    columns += 1
+            pairs += 1
+    literal_cnf = 0
+    for clauses in ([[1], [-1]], [[1, 2], [-1]], [[1, 2, 3], [-1, -2, -3]]):
+        problem = cnf_problem(3, clauses)
+        gs = checker.problem_data(problem)
+        for x in range(8):
+            truth = all(any(bool(x >> (abs(lit) - 1) & 1) == (lit > 0) for lit in clause) for clause in clauses)
+            permutation = reversible.A if truth else reversible.IDENTITY
+            for source in range(5):
+                expected = [{} for _ in range(5)]
+                expected[permutation[source]][(x,)] = QI(1)
+                out = checker.literal_endpoint(problem, problem['program'], gs, source, [x], 100000)
+                need(out == expected, 'complete literal reversible CNF endpoint')
+                literal_cnf += 1
+    return pairs, columns, literal_cnf
+
+
+def rejection_checks():
+    count = 0
+    def rejects(action):
+        nonlocal count
+        try:
+            action()
+        except (ValueError, TypeError, KeyError):
+            count += 1
+        else:
+            raise ValueError('negative control was accepted')
+    good, bad = source_conjugation(), source_conjugation(True)
+    certificate = decide(bad)
+    for field, value in [('problem_sha256', '0' * 64), ('axes', 8), ('roles', 1), ('window', [1, 4]),
+                         ('input_role', 2), ('output_role', -1), ('discrepancy', ['0', '0']), ('status', 'UNKNOWN'),
+                         ('input_points', [-1] * 23), ('output_points', []), ('input_points', [0])]:
+        changed = dict(certificate); changed[field] = value
+        rejects(lambda c=changed: checker.check(bad, c))
+    fake = dict(certificate, status='IDENTITY_ALL_POSITIVE_WIDTHS', residual_terms=0)
+    rejects(lambda: checker.check(bad, fake))
+    for field, value in [('axes', 0), ('roles', True)]:
+        p = copy.deepcopy(good); p[field] = value
+        rejects(lambda p=p: decide(p)); rejects(lambda p=p: checker.problem_data(p))
+    for mutate in (lambda p: p['generators']['G'].__setitem__('phase', 4),
+                   lambda p: p['generators']['G'].__setitem__('matrix_rows', [0] * 9),
+                   lambda p: p['program'][3].__setitem__('coefficient', 0.5),
+                   lambda p: p['program'][3].__setitem__('coefficient', '1e10000000'),
+                   lambda p: p['program'][0].__setitem__('inverse', 1),
+                   lambda p: p['program'][0].__setitem__('coefficient', 2),
+                   lambda p: p['program'][0].__setitem__('dst', 2)):
+        p = copy.deepcopy(good); mutate(p)
+        rejects(lambda p=p: decide(p)); rejects(lambda p=p: checker.problem_data(p))
+    p = late_projector(2)
+    rejects(lambda: decide(p, max_terms=1))
+    rejects(lambda: checker.algebra_endpoint(p, p['program'], checker.problem_data(p), 1))
+    rejects(lambda: gram_factor([2, 0]))
+    rejects(lambda: character_tuple(1, (4, 0)))
+    rejects(lambda: character_tuple(1, (0, 0), floor=5))
+    empty = {'axes': 1, 'roles': 2, 'generators': {}, 'program': [], 'reference': []}
+    rejects(lambda: decide(empty, max_terms=1))
+    rejects(lambda: checker.algebra_endpoint(empty, [], {}, 1))
+    return count
+
+
+def committed_examples():
+    count = 0
+    for path in sorted((HERE / 'examples').glob('*.certificate.json')):
+        problem_path = path.with_name(path.name.replace('.certificate.json', '.json'))
+        problem, certificate = json.loads(problem_path.read_text()), json.loads(path.read_text())
+        checker.check(problem, certificate)
+        if not path.name.startswith('late-projector'):
+            need(decide(problem) == certificate, 'committed certificate replay')
+        count += 1
+    need(count == 5, 'complete committed example set')
+    return count
+
+
+def main():
+    rng = random.Random(5354)
+    monomial, sources = authenticated_sources()
+    result = {'status': 'PASS_NATIVE_TENSOR_CUTOFF', 'sources': sources,
+              'symmetric_Gram_matrices': gram_checks()}
+    result['phase_characters'], result['larger_character_cases'] = character_checks(rng)
+    result['native_composition_pairs'], result['literal_native_points'] = group_checks(rng)
+    (result['circuits'], result['positive_circuits'], result['negative_circuits'],
+     result['literal_dirty_basis_cases']) = circuit_checks(rng)
+    result['source_binding'] = source_checks(monomial)
+    result['below_rank_projector_basis_cases'], result['central_residue_cases'] = projector_checks()
+    result['CNF_formulas'], result['CNF_assignments'], result['unsatisfiable_formulas'] = cnf_checks(rng)
+    (result['reversible_branch_pairs'], result['literal_reversible_columns'],
+     result['literal_CNF_columns']) = reversible_checks()
+    result['rejection_controls'] = rejection_checks()
+    result['committed_examples'] = committed_examples()
+    result['limits'] = ['No full Clifford/Hadamard theorem', 'Expanded circuit support can be exponential',
+                        'No physical supplier, precision, outer admission or new kappa',
+                        'No independent human or proof-kernel acceptance']
+    print(json.dumps(result, sort_keys=True, indent=2))
+
+
+if __name__ == '__main__':
+    main()