From dc2b1ff607c55e70786bd567b342f096fc0024f1 Mon Sep 17 00:00:00 2001
From: Joseph Anglada <fluorine@users.noreply.github.com>
Date: Sun, 25 Oct 2026 03:55:57 -0400
Subject: [PATCH] Prove the sharp three-axis native monomial tensor cutoff

---
 research/three-axis-sharp-cutoff/PROOF.md     | 197 ++++++++++++++++++
 research/three-axis-sharp-cutoff/README.md    |  86 ++++++++
 research/three-axis-sharp-cutoff/RESULT.json  |  32 +++
 .../SOURCE-CONTEXT.json                       |  11 +
 research/three-axis-sharp-cutoff/SOURCES.json |  24 +++
 research/three-axis-sharp-cutoff/TASK.json    | 101 +++++++++
 research/three-axis-sharp-cutoff/VERIFY.json  |  61 ++++++
 research/three-axis-sharp-cutoff/audit.py     | 114 ++++++++++
 .../inputs/PR5529-README.md                   | 186 +++++++++++++++++
 research/three-axis-sharp-cutoff/verify.py    | 197 ++++++++++++++++++
 10 files changed, 1009 insertions(+)
 create mode 100644 research/three-axis-sharp-cutoff/PROOF.md
 create mode 100644 research/three-axis-sharp-cutoff/README.md
 create mode 100644 research/three-axis-sharp-cutoff/RESULT.json
 create mode 100644 research/three-axis-sharp-cutoff/SOURCE-CONTEXT.json
 create mode 100644 research/three-axis-sharp-cutoff/SOURCES.json
 create mode 100644 research/three-axis-sharp-cutoff/TASK.json
 create mode 100644 research/three-axis-sharp-cutoff/VERIFY.json
 create mode 100644 research/three-axis-sharp-cutoff/audit.py
 create mode 100644 research/three-axis-sharp-cutoff/inputs/PR5529-README.md
 create mode 100644 research/three-axis-sharp-cutoff/verify.py

diff --git a/research/three-axis-sharp-cutoff/PROOF.md b/research/three-axis-sharp-cutoff/PROOF.md
new file mode 100644
index 0000000000..ef0be5ce6b
--- /dev/null
+++ b/research/three-axis-sharp-cutoff/PROOF.md
@@ -0,0 +1,197 @@
+# The three-axis native monomial tensor cutoff is exactly seven
+
+Joseph Anglada (@fluorine), with substantial OpenAI Codex assistance.
+Apache-2.0. This is a scoped computer-assisted algebraic proof, not an
+improved multiplication exponent, physical supplier or full theorem audit.
+
+## 1. Statement and exact grammar
+
+Use the input-phase grammar of Ali Romman's PR5369 and PR5529. Let
+X = F_2^3, with addresses 0..7 and bit j the coefficient of e_j. Put
+
+    U(g,q)e_x = i^{q(x)} e_{g(x)},
+    q(x) = c + sum_j a_j x_j + 2 sum_{j<k} b_jk x_j x_k (mod 4),
+
+where g is in AGL(3,2), c,a_j are in Z/4, and b_jk are in Z/2.
+Let G be this finite monomial group and k = Q(i) or C. Its diagonal
+subgroup D has 2048 elements; each gD_q is a unique normal form. Work in
+k[G] with rho_f([U]) = U^{tensor f}, extended linearly. External scalar
+coefficients are fixed outside the tensor power. Set z=[iI] and
+I_r=(z-i^r[1]), for r=0,1,2,3. These are two-sided central ideals.
+
+**Theorem.** For every positive f with residue r modulo four,
+
+    ker rho_f = I_r  if and only if  f >= L_r,
+    (L_0,L_1,L_2,L_3) = (8,9,10,7).
+
+The least F for which the equality holds for every f>=F is therefore
+seven. A set T of positive tensor widths decides every fixed k[G] identity
+at all positive widths exactly when, for each r, T contains a width
+f>=L_r congruent to r. In particular 7,8,9,10 suffice, four residue tests
+are necessary, and no complete test set can have maximum width below ten.
+
+The upper bound and its exact full-span census are PR5529's result. The
+addition here is necessity for the **complete representation**, using the
+explicit cancellation witness below. Full-span minima alone do not prove it.
+
+## 2. A 168-term cancellation certificate
+
+Embed H=GL(3,2) in the affine subgroup by fixing the zero address. For h in H
+define a(h) by its order:
+
+    order       1    2    3    4    7
+    a(h)        6   -2    0    2   -1.
+
+Put A=sum_h a(h)[h]. This is nonzero: its identity coefficient is six.
+For any two-dimensional linear plane V in X, let K_V be its pointwise
+stabilizer in H. It has four elements. The exact finite certificate is
+
+    sum_{h in g K_V} a(h) = 0       for every g in H and every V.       (1)
+
+Here is a small checkable description of the whole certificate. Take the
+standard plane V={0,1,2,3}. Its stabilizer consists of the matrices with
+first two columns e_1,e_2 and third column e_3+v, v in V. Right cosets are
+indexed by the 42 ordered independent image pairs (h(e_1),h(e_2)). The
+multisets of element orders and their multiplicities are exactly:
+
+    (1,2,2,2): 1; (2,2,4,4): 3; (2,3,3,4): 12;
+    (3,3,3,3): 2; (3,4,7,7): 24.
+
+Every displayed multiset has coefficient sum zero. Conjugation sends the
+standard plane to any linear plane and preserves orders, proving (1)
+from this finite table. The executables independently reconstruct all
+168 maps and the table: one enumerates independent binary matrix columns,
+the other enumerates all 5040 permutations of the seven nonzero addresses
+and retains exactly the XOR-preserving maps. The separate audit also
+recovers the coefficient vector by rationally solving the coset equations
+with a(1)=6. No character table or floating-point rank is an input.
+
+As redundant corroboration, direct group-algebra multiplication gives
+A^2=56 A. This idempotent relation is not needed for the proof.
+
+If a tuple x uses addresses lying in a proper linear subspace, choose a
+linear plane V containing it. For each output tuple y, the set
+{h:h x=y} is empty or a coset of the tuple's pointwise stabilizer, hence a
+disjoint union of right cosets of K_V. Equation (1) gives
+
+    A^{(f)} e_x := sum_h a(h) h^{tensor f} e_x = 0.                  (2)
+
+This defines a linear combination of tensor powers, not the tensor power
+of the sum A. That distinction is essential.
+
+## 3. A coding-theory obstruction below width seven
+
+Say a tuple x_1,...,x_f has zero nonconstant phase character if
+
+    sum_t x_tj = 0 (mod 4),
+    sum_t x_tj x_tk = 0 (mod 2)  for j<k.                          (3)
+
+Let the three binary row words of this tuple be R_1,R_2,R_3 in F_2^f.
+Their weights are divisible by four and their pairwise dot products are
+zero. Every word in their binary linear span has weight divisible by
+four: wt(u+v)=wt(u)+wt(v)-2|supp(u) intersect supp(v)|, and the whole
+span is self-orthogonal. This is a doubly even binary code.
+
+If the rows were independent, the seven nonzero codewords would each
+have weight at least four, so their total weight would be at least 28.
+But every nonzero address column contributes to exactly four of those
+seven words. Thus that total is 4 times the number of nonzero columns,
+at most 4f. For f<=6 this is at most 24, a contradiction. Therefore the
+row rank, and equivalently the linear span of the address columns, is
+at most two. Equation (2) now annihilates every tuple satisfying (3)
+at every positive width below seven.
+
+This seven-column threshold is the elementary binary simplex-code
+weight-counting bound. It is classical coding theory, not a new coding
+bound. Its use here supplies the missing stabilizer-kernel witness.
+
+## 4. Four explicit fixed residuals
+
+Define the finite phase projector and residual
+
+    E_r = (1/2048) sum_{c,a,b} i^{-r c} [D_q],
+    P_r = A E_r.                                                 (4)
+
+The phase acts first, in the predecessor's input-phase convention.
+Finite Fourier orthogonality says rho_f(E_r) projects onto tuples
+satisfying (3) when f=r modulo four, and is zero at all other residues.
+For a matching residue at f<L_r, the positive f is at most six.
+Sections 2 and 3 prove rho_f(P_r)=0. At a wrong residue this is already
+forced by E_r. Thus P_r vanishes at **every** positive f<L_r.
+
+At width L_r, take each of the seven nonzero addresses once and add
+L_r-7 zero addresses. Each coordinate then occurs four times and each
+coordinate pair twice, so E_r acts as identity. Only the identity
+linear map fixes this tuple. Its diagonal matrix entry under rho_f(P_r)
+is exactly six. The same construction with additional groups of four
+zeros works for every larger width of that residue.
+
+Each P_r is nonzero as a formal group-algebra element: in the expansion
+hD_q the normal forms are distinct and the identity-h coefficient is a
+nonzero Gaussian multiple of 6/2048. Moreover z P_r=i^r P_r, so P_r is
+not in I_r (evaluation at width L_r also proves this). It follows that
+ker rho_f properly contains I_r at every matching f<L_r. In particular
+P_2 is zero at widths 1..9 but has diagonal entry six at width ten.
+This is the missing necessity statement, not an inference from an absent
+full-span tuple or a rank modulo one prime.
+
+## 5. Upper bound and all-width completeness
+
+For completeness the PR5529 upper bound is checked in two separate finite
+ways. For a multiplicity vector m on the eight addresses define its phase
+statistics (r,u,v) by (3), retaining the actual coordinate residues u in
+(Z/4)^3, pair parities v in (Z/2)^3 and r=sum m mod four. There are
+4*4^3*2^3=2048 characters.
+
+The first checker exhausts all 43758 nonnegative multiplicity vectors
+with total at most ten and records the least total with full affine span
+for each character. Every character occurs; the largest minima in the
+four residues are (8,9,10,7). The second checks all 65536 vectors
+a in {0,1,2,3}^8 using PR5529's exact formula
+
+    shortest full-span length for this a = sum a + 4(3-d(a)),
+
+where d(a) is the affine dimension of its positive support, with -1 for
+empty support. Indeed every new support address costs at least four
+copies and adds at most one affine dimension; conversely exactly 3-d
+new addresses extend that support to full affine span. Taking minima
+over a gives the same result. Thus this finite certificate is exhaustive,
+not a sample of widths. Four-copy zero padding preserves a character
+and full affine span at all later widths of the same residue.
+
+Write an arbitrary group-algebra residual as a sum over unique affine
+buckets and phases. After imposing the residue relation, a nonzero
+residual has a nonzero Fourier coefficient in some bucket g. At
+f>=L_r, choose a full-affine-span tuple realizing that character and
+output g times the tuple. No other affine map gives that same output,
+so the corresponding matrix entry is the nonzero Fourier coefficient.
+Hence ker rho_f=I_r. This is the predecessor Fourier-separation argument.
+
+The four central ideals have zero intersection by Fourier inversion in
+the constant phase. Upper bounds therefore prove sufficiency of any
+test set reaching all four thresholds. If a test set misses the threshold
+in residue r, the fixed nonzero residual P_r vanishes at every test in
+that set and fails at L_r. This proves necessity even for infinite T.
+
+## 6. Scope and evidence
+
+The theorem applies entrywise to complete fixed register-program endpoint
+matrices over k[G], with every independent dirty input and specified
+return retained. It excludes Hadamard/nonmonomial gates, width-dependent
+external coefficients or program families, and undeclared aliases.
+It does not provide efficient expansion of a circuit into group algebra.
+No physical cost, ownership budget, compiler, precision, stock, tape,
+analytic reduction or multiplication exponent changes.
+
+The integer coset table is computer-assisted finite evidence. The
+all-width statement follows from the written Fourier, code-weight and
+padding arguments. Same-agent separate implementations are corroboration,
+not independent human review or formal proof-kernel acceptance.
+
+Credit Ali Romman for PR5369's grammar/Fourier theorem and PR5529's
+improved sufficient bound and explicit open question; Hiroki KUMAZAKI for
+PR5522's two-axis sharpness and warning about the representation-kernel
+gap; Mihir Srivastava for PR5521's one-axis/general audit; Jose Manuel,
+ywz65, Chris R and the retained native/phase/compiler lineage. The
+GL(3,2), finite Fourier and doubly-even/simplex-code tools are classical.
+No general literature-priority claim is made.
diff --git a/research/three-axis-sharp-cutoff/README.md b/research/three-axis-sharp-cutoff/README.md
new file mode 100644
index 0000000000..95fbde2fa2
--- /dev/null
+++ b/research/three-axis-sharp-cutoff/README.md
@@ -0,0 +1,86 @@
+# Sharp three-axis native monomial cutoff: seven
+
+This resolves the least-three-axis-cutoff question explicitly left open in
+[PR #5529](https://github.com/CrocSwap/integer-mult-bounds/pull/5529): the
+sufficient tensor window **7,8,9,10 is sharp**. The addition is a nonzero
+fixed group-algebra residual invisible at widths 1..9 and visible at ten,
+plus the four exact central-residue kernel thresholds `(8,9,10,7)`.
+The complete multiplication exponent **does not change**.
+
+## Scope and evidence
+
+The [proof](PROOF.md) uses classical binary coding theory and an explicit
+168-term GL(3,2) cancellation. Zero phase forces a doubly even code. Three
+independent rows would have seven nonzero codewords of total weight at
+least 28, impossible below seven columns. A finite integer coset certificate
+then kills every remaining low-width tuple; a full-span tuple exposes the
+residual at each threshold. No modular-rank experiment is used as a lower proof.
+
+The monomial grammar, Fourier separation and sufficient upper bound remain
+Ali Romman's contributions. Fixed external coefficients and complete dirty
+inputs/returns are essential. This excludes Hadamards, width-dependent
+programs and physical supplier costs. It is a written computer-assisted
+proof with separately implemented finite checks, not human or proof-kernel
+acceptance or a complete multiplication proof.
+
+[RESULT.json](RESULT.json) binds the primary result. Checks cover 168 linear
+maps, all 294 plane cosets, an integer idempotent identity, all 43758
+multiplicity vectors through width ten, all 2048 phase characters, literal
+Gaussian phase sums, four threshold diagonal entries and six semantic
+coefficient/quadratic-phase rejection controls. A separately written audit
+reconstructs the group from permutations, solves the coefficient equations
+over rationals, checks all 65536 residue vectors and all 299593 ordered
+words through width six (784 zero-phase words and 27496 output fibers).
+Both implementations were written in the same agent context, not by an
+independent reviewer.
+
+The user explicitly requested a mathematical attempt after a tooling round.
+[TASK.json](TASK.json) changes the `formal-interface-lemma` card to this
+written interface theorem; no Lean formalization is claimed. Canonical
+base is `32890bc5de034ab8fc93ac88ead7279a6a416d04`, priority revision 7.
+[SOURCES.json](SOURCES.json) pins the original native grammar proof at that
+base. [SOURCE-CONTEXT.json](SOURCE-CONTEXT.json) identifies the byte-exact
+pending PR5529 README snapshot and its immutable Git blob. Neither predecessor
+executable is imported or changed.
+
+## Reproduce
+
+Python 3.12, standard library only, from repository root:
+
+```sh
+python -B scripts/research_package.py --package research/three-axis-sharp-cutoff --check-only
+python -B scripts/research_package.py --package research/three-axis-sharp-cutoff
+```
+
+The registered commands run each implementation normally and with `-O`,
+isolated and warning-strict, with a 60-second cap per command. Expected
+lines: `PASS_THREE_AXIS_SHARP_CUTOFF`, `PASS_THREE_AXIS_SEPARATE_AUDIT`,
+then `PASS_REGISTERED_RESEARCH_PACKAGE`. Direct verifiers also work in an
+official Git-free export containing the declared grammar source.
+
+Selected baseline bindings remain unchanged. No selected cold replay,
+physical native supplier, compiler/stock/precision/outer admission, Lean
+or Docker execution is part of this package.
+
+## Open next questions
+
+For a higher axis count, look for a similarly explicit stabilizer-kernel
+witness at the last pre-threshold residue. This would distinguish sufficient
+character realizations from a sharp representation threshold; the blocker
+is the absent higher-dimensional annihilator, not numerical root precision.
+
+A physical application should first bind one complete source program and
+all its dirty inputs/returns to this exact three-axis grammar. The theorem
+alone supplies no physical invoice or compiler admission. Structured first
+steps and blockers are in TASK.json.
+
+## Credit
+
+Prepared for Joseph Anglada (@fluorine), with substantial OpenAI Codex
+assistance in derivation, programming, checking and writing. New work is
+Apache-2.0. Credit Ali Romman for PR5369/PR5529 and the open question;
+Hiroki KUMAZAKI for PR5522's two-axis sharpness and representation-kernel
+distinction; Mihir Srivastava for PR5521; Jose Manuel, ywz65, Chris R and
+the retained native/phase/compiler source lineage. The finite Fourier,
+GL(3,2), doubly-even-code and simplex-code ingredients are classical.
+No global literature-priority claim is made.
diff --git a/research/three-axis-sharp-cutoff/RESULT.json b/research/three-axis-sharp-cutoff/RESULT.json
new file mode 100644
index 0000000000..d8e4df65e3
--- /dev/null
+++ b/research/three-axis-sharp-cutoff/RESULT.json
@@ -0,0 +1,32 @@
+{
+  "status": "PASS_THREE_AXIS_SHARP_CUTOFF",
+  "cutoff": 7,
+  "residue_thresholds": [
+    8,
+    9,
+    10,
+    7
+  ],
+  "sufficient_and_sharp_window": [
+    7,
+    8,
+    9,
+    10
+  ],
+  "gl3_elements": 168,
+  "plane_cosets": 294,
+  "coset_order_types": {
+    "1,2,2,2": 1,
+    "2,2,4,4": 3,
+    "2,3,3,4": 12,
+    "3,3,3,3": 2,
+    "3,4,7,7": 24
+  },
+  "multiplicities": 43758,
+  "phase_characters": 2048,
+  "lower_zero_phase_multisets": 35,
+  "exact_lower_image_fibers": 448,
+  "threshold_entries": 4,
+  "rejection_controls": 6,
+  "no_new_kappa": true
+}
diff --git a/research/three-axis-sharp-cutoff/SOURCE-CONTEXT.json b/research/three-axis-sharp-cutoff/SOURCE-CONTEXT.json
new file mode 100644
index 0000000000..e47504f580
--- /dev/null
+++ b/research/three-axis-sharp-cutoff/SOURCE-CONTEXT.json
@@ -0,0 +1,11 @@
+{
+  "purpose": "Immutable context snapshot, not an imported executable or accepted physical supplier",
+  "repository": "aliromman/integer-mult-bounds",
+  "commit": "0fac48cff6252349cee0d5350914170d4acf9dfb",
+  "source_path": "research/shorter-native-phase-witness/README.md",
+  "local_path": "inputs/PR5529-README.md",
+  "git_blob": "5b68f6be4a297f6ccc1ac1631f40d310ff2236b4",
+  "sha256": "abc1224cb79a7056d476636522100a375dbe7d51f2e9a985e667d0d7729f3212",
+  "license": "Apache-2.0; original contributor attribution retained verbatim",
+  "source_url": "https://github.com/aliromman/integer-mult-bounds/blob/0fac48cff6252349cee0d5350914170d4acf9dfb/research/shorter-native-phase-witness/README.md"
+}
diff --git a/research/three-axis-sharp-cutoff/SOURCES.json b/research/three-axis-sharp-cutoff/SOURCES.json
new file mode 100644
index 0000000000..224c716abb
--- /dev/null
+++ b/research/three-axis-sharp-cutoff/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/native-tensor-cutoff/PROOF.md",
+      "usage": "input",
+      "git_blob": "2d92f17cd8e1064028656cd4ff06c1d38f14ebc0",
+      "sha256": "b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041"
+    }
+  ]
+}
diff --git a/research/three-axis-sharp-cutoff/TASK.json b/research/three-axis-sharp-cutoff/TASK.json
new file mode 100644
index 0000000000..f0c0d44986
--- /dev/null
+++ b/research/three-axis-sharp-cutoff/TASK.json
@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Determine the sharp three-axis native monomial representation cutoff left open by PR5529: construct nonzero fixed residuals invisible below each residue threshold.",
+  "scope_change_reason": "The user explicitly requests a mathematical attempt after tooling work. This is a written computer-assisted interface theorem, not a Lean formalization or a new kappa; it addresses the live PR5529 sharpness handoff.",
+  "bottleneck_link": "Settles whether smaller tensor test widths can certify fixed native identities; prevents unsound shorter finite verification. Physical supplier costs and kappa are unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after an explicit lower witness plus exhaustive matching upper certificate, or a counterexample to the candidate. No physical supplier or complete exponent claim.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; primary exact group/coset and complete composition checks; separately written permutation/rational/base-four/ordered-word audit; RESULT.json.",
+  "author": "Joseph Anglada, with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation and writing. Two separately written implementations in the same agent context; no independent human or formal-kernel review.",
+  "open_questions": [
+    {
+      "question": "Can another axis count admit similarly small explicit stabilizer-kernel witnesses?",
+      "why_it_matters": "Full-span character minima are only sufficient in general; a genuine representation witness is required for necessity.",
+      "first_step": "Inspect the next dimension at its last pre-threshold residue, before launching any large group census.",
+      "blocked_by": "No higher-axis stabilizer annihilator or priced caller supplied here."
+    },
+    {
+      "question": "Can the criterion be used on one complete source-bound native program?",
+      "why_it_matters": "An abstract cutoff alone does not execute the physical supplier.",
+      "first_step": "Bind a fixed monomial program and every dirty input/return to its actual three-axis grammar.",
+      "blocked_by": "Actual endpoint binding, physical costs and compiler admission are outside this theorem."
+    }
+  ]
+}
diff --git a/research/three-axis-sharp-cutoff/VERIFY.json b/research/three-axis-sharp-cutoff/VERIFY.json
new file mode 100644
index 0000000000..a2f2c55eeb
--- /dev/null
+++ b/research/three-axis-sharp-cutoff/VERIFY.json
@@ -0,0 +1,61 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/native-tensor-cutoff/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact group/coset/phase and full-span certificates with semantic controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact group/coset/phase and full-span certificates with semantic controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/audit.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Separate permutation/rational solve/base-four/ordered-word enumeration"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "-O",
+        "{package}/audit.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Separate permutation/rational solve/base-four/ordered-word enumeration"
+    }
+  ]
+}
diff --git a/research/three-axis-sharp-cutoff/audit.py b/research/three-axis-sharp-cutoff/audit.py
new file mode 100644
index 0000000000..5177025ef8
--- /dev/null
+++ b/research/three-axis-sharp-cutoff/audit.py
@@ -0,0 +1,114 @@
+#!/usr/bin/env python3
+"""Separate enumeration: permutations, rational solves, base-four forms, tuples.
+
+Joseph Anglada with substantial OpenAI Codex assistance. Apache-2.0.
+Written separately in the same agent context; not an independent human audit.
+Imports neither verify.py nor any predecessor arithmetic/executable.
+"""
+from collections import Counter
+from fractions import Fraction
+from itertools import permutations, product
+from math import lcm
+import json
+
+def check(value, label):
+    if not value:
+        raise ValueError(label)
+
+def span(items):
+    space = {0}
+    for x in items:
+        space |= {y ^ x for y in space}
+    return space
+
+def cycle_order(g):
+    unseen, order = set(range(8)), 1
+    while unseen:
+        start = min(unseen)
+        x, length = start, 0
+        while x in unseen:
+            unseen.remove(x)
+            x, length = g[x], length + 1
+        check(x == start, 'permutation cycle')
+        order = lcm(order, length)
+    return order
+
+def solve(rows, size):
+    rows = [[Fraction(x) for x in row] for row in rows]
+    pivot = 0
+    for col in range(size):
+        hit = next((k for k in range(pivot, len(rows)) if rows[k][col]), None)
+        check(hit is not None, 'unique rational coefficient solution')
+        rows[pivot], rows[hit] = rows[hit], rows[pivot]
+        divisor = rows[pivot][col]
+        rows[pivot] = [x / divisor for x in rows[pivot]]
+        for k in range(len(rows)):
+            if k != pivot:
+                factor = rows[k][col]
+                rows[k] = [x - factor * y for x, y in zip(rows[k], rows[pivot])]
+        pivot += 1
+    check(all(not any(row[:-1]) and not row[-1] for row in rows[size:]), 'rational consistency')
+    return [rows[k][-1] for k in range(size)]
+
+def main():
+    group = []
+    for tail in permutations(range(1, 8)):
+        g = (0,) + tail
+        if all(g[x ^ y] == (g[x] ^ g[y]) for x in range(8) for y in range(8)):
+            group.append(g)
+    check(len(group) == 168, 'independent GL3 inventory')
+    orders = {g: cycle_order(g) for g in group}
+    subgroup = [g for g in group if g[:4] == (0, 1, 2, 3)]
+    seen, patterns = set(), Counter()
+    for g in group:
+        if g in seen:
+            continue
+        coset = {tuple(g[h[x]] for x in range(8)) for h in subgroup}
+        seen |= coset
+        patterns[tuple(sorted(orders[h] for h in coset))] += 1
+    classes = (1, 2, 3, 4, 7)
+    equations = [[1, 0, 0, 0, 0, 6]]
+    equations += [[pattern.count(order) for order in classes] + [0] for pattern in sorted(patterns)]
+    solution = solve(equations, 5)
+    check(solution == list(map(Fraction, (6, -2, 0, 2, -1))), 'rederived coefficients')
+    coefficient = {g: solution[classes.index(orders[g])] for g in group}
+    minima = {}
+    for a in product(range(4), repeat=8):
+        points = [x for x, count in enumerate(a) if count]
+        affine = (len(span([x ^ points[0] for x in points])).bit_length() - 1) if points else -1
+        key = (sum(a) & 3, sum(a[x] for x in (1, 3, 5, 7)) & 3,
+               sum(a[x] for x in (2, 3, 6, 7)) & 3, sum(a[x] for x in (4, 5, 6, 7)) & 3,
+               (a[3] + a[7]) & 1, (a[5] + a[7]) & 1, (a[6] + a[7]) & 1)
+        length = sum(a) + 4 * (3 - affine)
+        minima[key] = min(minima.get(key, 100), length)
+    check(len(minima) == 2048, 'independent phase census')
+    check([max(v for k, v in minima.items() if k[0] == r) for r in range(4)] == [8, 9, 10, 7],
+          'independent full-span thresholds')
+    words = accepted = output_fibers = 0
+    for width in range(7):
+        for word in product(range(8), repeat=width):
+            words += 1
+            rows = [sum(((x >> j) & 1) << bit for bit, x in enumerate(word)) for j in range(3)]
+            if any(row.bit_count() % 4 for row in rows):
+                continue
+            if any((rows[j] & rows[k]).bit_count() % 2 for j, k in ((0, 1), (0, 2), (1, 2))):
+                continue
+            accepted += 1
+            check(len(span(rows)) <= 4, 'doubly-even length-six bound')
+            images = Counter()
+            for g in group:
+                images[tuple(g[x] for x in word)] += coefficient[g]
+            check(not any(images.values()), 'literal short tensor column')
+            output_fibers += len(images)
+    check(words == sum(8 ** f for f in range(7)), 'complete ordered word census')
+    for residue, width in enumerate((8, 9, 10, 7)):
+        word = (0,) * (width - 7) + tuple(range(1, 8))
+        check(sum(coefficient[g] for g in group if tuple(g[x] for x in word) == word) == 6,
+              'literal threshold diagonal')
+    print('PASS_THREE_AXIS_SEPARATE_AUDIT ' + json.dumps(dict(
+        group_elements=len(group), normal_forms=65536, characters=len(minima),
+        ordered_words=words, zero_phase_words=accepted, exact_output_fibers=output_fibers,
+        rederived_coefficients=[str(x) for x in solution], cutoff=7), sort_keys=True))
+
+if __name__ == '__main__':
+    main()
diff --git a/research/three-axis-sharp-cutoff/inputs/PR5529-README.md b/research/three-axis-sharp-cutoff/inputs/PR5529-README.md
new file mode 100644
index 0000000000..5b68f6be4a
--- /dev/null
+++ b/research/three-axis-sharp-cutoff/inputs/PR5529-README.md
@@ -0,0 +1,186 @@
+# Shorter constructive witnesses for native monomial identities
+
+This package improves the sufficient tensor-width bound for the affine/quadratic
+Gaussian monomial grammar in [PR #5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369).
+For n>=2 axes, the general cutoff is 2n+3. For three axes, an exact finite
+character calculation improves it further to seven. Thus widths 7,8,9,10
+decide every fixed three-axis identity in this grammar. The complete kappa
+calculation is unchanged.
+
+## Contract and result
+
+Retain the input-phase action and fixed external coefficients:
+
+```text
+U(g,q)e_x = i^q(x) e_g(x),
+q(x) = c + sum_j a_j x_j + 2 sum_(j<k) b_jk x_j x_k modulo 4,
+g in AGL(n,2), c,a_j in Z/4, b_jk in Z/2.
+```
+
+For P in the complex group algebra, let rho_f(P) evaluate each group term at
+its f-th tensor power. The external coefficients stay fixed. Write I_r for
+the ideal generated by [iI]-i^r[1]. Then
+
+```text
+n>=2 and f>=2n+3  imply  ker(rho_f)=I_(f mod 4).
+n=3 and f>=7     imply  ker(rho_f)=I_(f mod 4).
+```
+
+Consequently four consecutive widths starting at either sufficient cutoff
+decide equality for a single fixed P at all positive widths. The same result
+applies entrywise to complete register endpoints. All independent dirty inputs
+and all specified returned roles remain part of the endpoint. A width-dependent
+program cannot be promoted to an all-width identity by four tests.
+
+For nine axes the sufficient window changes from 22..25 to 21..24. This changes
+an algebraic test bound. It does not reduce a physical supplier's paid cost.
+The sharp two-axis cutoff six in PR #5522 remains stronger in that dimension.
+No least representation cutoff for n>=3 is claimed here.
+
+## A nonalternating Gram form saves one column
+
+A phase character has statistics (r,u,v), where r and u_j are modulo four and
+v_jk are modulo two. As in the predecessor, set the binary symmetric matrix M
+by M_jj=u_j mod 2 and M_jk=v_jk. A tuple of points must have Gram matrix M,
+coordinate counts u modulo four, length r modulo four and full affine span.
+
+Choose an invertible binary matrix B whose column sum s differs from u modulo
+two. This is possible for n>=2: use B=I unless u mod 2 is the all-ones vector;
+in that case replace its first column e_1 by e_1+e_2. Start the tuple with zero
+and the n columns of B. It already has full affine span. The residual Gram
+matrix R=M+BB^t has diagonal u+s, which is nonzero. Thus R is nonalternating.
+
+Every nonalternating symmetric binary matrix R has a factor YY^t=R with
+exactly rank(R)<=n columns. Here is an explicit proof and algorithm. Symmetric
+elimination splits the form into unit lines, hyperbolic pairs and a radical.
+There is at least one unit line. A unit z and a hyperbolic pair e,f can be
+replaced by z+e, z+f, z+e+f; these three vectors are orthonormal. Repeat to
+obtain an orthonormal basis v_i for a complement to the radical. Then
+
+```text
+R = sum_i (R v_i)(R v_i)^t.
+```
+
+Indeed the orthonormal vectors resolve the bilinear form on the quotient by
+its radical. This gives the columns of Y and uses polynomial binary linear
+algebra. Nonalternation is essential: a nonzero alternating form can require
+an extra Gram column. The rank lower bound also proves that this factor width
+is exact for the chosen R. Binary symmetric factorization is classical.
+
+Append the columns of Y. The tuple now has the required Gram matrix and length
+at most 2n+1. If its coordinate counts are w modulo four, then u-w is even.
+Append two copies of the single vector z with coordinates (u_j-w_j)/2 modulo
+two, unless z is zero. This changes the coordinate counts as required and
+preserves all pair parities. The length is at most 2n+3.
+
+For any f>=2n+3 with f congruent to r modulo four, append zero points to reach
+f. They preserve coordinate counts, pair counts and affine span. The resulting
+tuple realizes every character at every such f. This proves the improved
+constructive bound.
+
+## Why character witnesses decide the complete endpoint
+
+The predecessor's Fourier argument is retained. Write P as a sum over affine
+maps g and diagonal phases. At a fixed residue r, combine the constant phase
+coefficients. If P is outside I_r, finite Fourier inversion gives an affine
+bucket and a nonconstant phase character with a nonzero Fourier coefficient.
+Use a tuple X with that character and full affine span, and put Y=gX.
+A different affine map cannot send X to Y. The matrix entry from X to Y is
+therefore exactly the nonzero Fourier coefficient. Conversely every element
+of I_r evaluates to zero at residue r. This proves the displayed kernel bounds.
+The four residue ideals have zero intersection, which proves the four-test
+statement. This step neither assumes nor proves that full affine span is
+necessary for representation faithfulness.
+
+## Exact three-axis character calculation
+
+For n=3 there are 2048 characters including the constant residue. For a
+multiplicity vector m on the eight binary addresses, write m=a+4t with
+0<=a_x<=3 and t_x>=0. Define its character by
+
+```text
+r = sum_x a_x modulo 4,
+u_j = sum_x a_x x_j modulo 4,
+v_jk = sum_x a_x x_j x_k modulo 2.
+```
+
+Let d(a) be the affine dimension of its positive support, with d=-1 for the
+empty support. The exact shortest full-span realization of this residue vector
+has length
+
+```text
+L(a) = sum_x a_x + 4(3-d(a)).
+```
+
+Each new supported point requires four copies and increases affine dimension
+by at most one. Conversely any affine subspace extends to the full space by
+exactly 3-d new points. These two facts prove the formula, including empty
+support. Therefore the exact minimum for a character is the minimum of L(a)
+over its residue vectors a in {0,1,2,3}^8. Four-copy zero padding preserves the
+character and full span at every later width of that residue.
+
+The executable checks all 65536 residue vectors and all 2048 characters. The
+maxima of these exact minima, ordered by residue 0,1,2,3, are
+
+```text
+(8,9,10,7).
+```
+
+A separate enumeration of all 43758 nonnegative multiplicity vectors of total
+width at most ten gives exactly the same 2048 minima. Every minimum also has
+an explicit full-span witness. This finite exact certificate and the padding
+argument prove that the three-axis representation has stabilized by width
+seven. They do not exclude stabilization before the full-span witness bound;
+that would require a separate analysis of nontrivial affine stabilizers.
+
+## Evidence and reproduction
+
+```sh
+python3.12 -B scripts/research_package.py --package research/shorter-native-phase-witness
+```
+
+Python 3.12 and the standard library suffice. Normal and optimized warning-strict
+runs print `PASS_SHORTER_NATIVE_PHASE_WITNESS`; the launcher prints
+`PASS_REGISTERED_RESEARCH_PACKAGE`. Each run checks 1023 nonalternating binary
+forms through dimension four, 2624 constructed characters through 17 axes,
+17408 literal Gaussian-phase identities, the two complete three-axis censuses
+above and seven controls. The controls reject an alternating input and show
+that Gram parity alone misses a two-unit linear phase change.
+
+No predecessor executable is imported. These finite checks corroborate the
+all-dimension written proof; no independent human or proof-kernel acceptance
+is claimed. The selected cold replay, native physical emission, full compiler,
+precision, stock, movement and outer-transfer checks were not run.
+
+## Sources and related work
+
+Ali Romman's [pinned PR #5369 proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/native-tensor-cutoff/PROOF.md)
+supplies the exact grammar, Fourier reduction, pair correction, four residues
+and full endpoint contract. It retains Jose Manuel (@jmbarrancoml), Douglas
+Colkitt, ywz65, Chris R (@Clear1nsight), JoyboyBrian, Cinna Davis and the native
+source lineage. The adaptive initial basis is the change to that construction.
+
+Hiroki KUMAZAKI (@kumagi) supplies the sharp two-axis result in
+[PR #5522](https://github.com/CrocSwap/integer-mult-bounds/pull/5522) and its
+[pinned proof](https://github.com/kumagi/integer-mult-bounds/blob/ffb5adf6a2509a7c99f564d13b74fc82a51b5adc/research/two-axis-native-cutoff/PROOF.md).
+Its multiplicity method and warning about the representation-kernel gap guide
+the three-axis calculation. [PR #5521](https://github.com/CrocSwap/integer-mult-bounds/pull/5521)
+audits the general proof and settles one axis. [PR #5526](https://github.com/CrocSwap/integer-mult-bounds/pull/5526)
+treats the larger full-Clifford group; the present grammar excludes Hadamards.
+No result or source in those contributions is edited.
+
+## Open next questions
+
+Determine whether the three-axis representation already stabilizes before
+width seven. Start with the affine pointwise stabilizers for characters whose
+full-span minimum exceeds the width, and compute their common group-algebra
+kernel. A character-realization minimum alone is not a lower bound for the
+complete representation. Physical application still needs a source-bound
+complete endpoint and its full paid invoice.
+
+## Credit
+
+Finite Fourier inversion, binary form classification and affine basis methods
+are classical. Predecessor methods retain the credit above. New proof and
+checks by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0.
+No general literature-priority claim is made.
diff --git a/research/three-axis-sharp-cutoff/verify.py b/research/three-axis-sharp-cutoff/verify.py
new file mode 100644
index 0000000000..91a49b18e6
--- /dev/null
+++ b/research/three-axis-sharp-cutoff/verify.py
@@ -0,0 +1,197 @@
+#!/usr/bin/env python3
+"""Exact certificates for the sharp three-axis monomial cutoff.
+
+Joseph Anglada with substantial OpenAI Codex assistance. Apache-2.0.
+No predecessor executable or floating-point acceptance.
+"""
+from collections import Counter
+from hashlib import sha256
+from itertools import combinations, product
+from pathlib import Path
+import json
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+THRESHOLDS = (8, 9, 10, 7)
+WEIGHTS = {1: 6, 2: -2, 3: 0, 4: 2, 7: -1}
+IDENTITY = tuple(range(8))
+SOURCE_PINS = {
+    'research/native-tensor-cutoff/PROOF.md': 'b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041',
+    'research/three-axis-sharp-cutoff/inputs/PR5529-README.md': 'abc1224cb79a7056d476636522100a375dbe7d51f2e9a985e667d0d7729f3212',
+}
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+def binary_rank(vectors):
+    pivots = {}
+    for value in vectors:
+        while value:
+            bit = value.bit_length() - 1
+            if bit in pivots:
+                value ^= pivots[bit]
+            else:
+                pivots[bit] = value
+                break
+    return len(pivots)
+
+def compose(g, h):
+    return tuple(g[h[x]] for x in range(8))
+
+def linear_group():
+    result = []
+    for columns in product(range(1, 8), repeat=3):
+        if binary_rank(columns) != 3:
+            continue
+        result.append(tuple((columns[0] if x & 1 else 0)
+                            ^ (columns[1] if x & 2 else 0)
+                            ^ (columns[2] if x & 4 else 0) for x in range(8)))
+    require(len(result) == len(set(result)) == 168, 'GL3 inventory')
+    return result
+
+def element_order(g):
+    power = IDENTITY
+    for order in range(1, 8):
+        power = compose(power, g)
+        if power == IDENTITY:
+            return order
+    raise ValueError('unexpected GL3 order')
+
+def planes():
+    return [tuple(x for x in range(8) if (x & normal).bit_count() % 2 == 0)
+            for normal in range(1, 8)]
+
+def coefficient_certificate(group, weights=WEIGHTS):
+    coefficients = {g: weights[element_order(g)] for g in group}
+    expected = {(1, 2, 2, 2): 1, (2, 2, 4, 4): 3,
+                (2, 3, 3, 4): 12, (3, 3, 3, 3): 2, (3, 4, 7, 7): 24}
+    coset_checks = 0
+    for plane in planes():
+        subgroup = [g for g in group if all(g[x] == x for x in plane)]
+        require(len(subgroup) == 4, 'plane stabilizer')
+        unseen, types = set(group), Counter()
+        while unseen:
+            g = min(unseen)
+            coset = {compose(g, h) for h in subgroup}
+            require(len(coset) == 4 and coset <= unseen, 'coset partition')
+            unseen -= coset
+            types[tuple(sorted(element_order(h) for h in coset))] += 1
+            require(sum(coefficients[h] for h in coset) == 0, 'nonzero plane coset sum')
+            coset_checks += 1
+        require(types == expected, 'coset order census')
+    convolution = Counter()
+    for g, a in coefficients.items():
+        for h, b in coefficients.items():
+            convolution[compose(g, h)] += a * b
+    require(all(convolution[g] == 56 * coefficients[g] for g in group), 'idempotent identity')
+    require(coefficients[IDENTITY] == 6, 'nonzero identity coefficient')
+    return coefficients, coset_checks, expected
+
+def statistics(counts):
+    return (sum(counts) % 4,
+            *(sum(counts[x] for x in range(8) if x >> j & 1) % 4 for j in range(3)),
+            *(sum(counts[x] for x in range(8) if (x >> j & 1) and (x >> k & 1)) % 2
+              for j, k in combinations(range(3), 2)))
+
+def multiplicities(width):
+    for bars in combinations(range(width + 7), 7):
+        ends = (-1,) + bars + (width + 7,)
+        yield tuple(ends[j + 1] - ends[j] - 1 for j in range(8))
+
+def support(counts):
+    return tuple(x for x in range(8) if counts[x])
+
+def affine_rank(points):
+    return binary_rank([x ^ points[0] for x in points]) if points else -1
+
+def literal_coset_sums(group, coefficients, points):
+    sums = Counter()
+    for g in group:
+        sums[tuple(g[x] for x in points)] += coefficients[g]
+    return sums
+
+def phase_projector(counts, residue, quadratic=True):
+    total = [0, 0]
+    for constant, a0, a1, a2 in product(range(4), repeat=4):
+        for b01, b02, b12 in product(range(2), repeat=3):
+            exponent = -residue * constant
+            for x, count in enumerate(counts):
+                bits = [(x >> j) & 1 for j in range(3)]
+                q = constant + a0 * bits[0] + a1 * bits[1] + a2 * bits[2]
+                if quadratic:
+                    q += 2 * (b01 * bits[0] * bits[1] + b02 * bits[0] * bits[2]
+                              + b12 * bits[1] * bits[2])
+                exponent += count * q
+            re, im = ((1, 0), (0, 1), (-1, 0), (0, -1))[exponent % 4]
+            total[0] += re
+            total[1] += im
+    return tuple(total)
+
+def census(group, coefficients):
+    minima = {}
+    total = zero_phase = literal_fibers = 0
+    quadratic_control = None
+    for width in range(11):
+        for counts in multiplicities(width):
+            total += 1
+            key, points = statistics(counts), support(counts)
+            if affine_rank(points) == 3:
+                minima.setdefault(key, width)
+            if width <= 6 and not any(key[1:]):
+                zero_phase += 1
+                weights = [sum(counts[x] for x in range(8) if (x & word).bit_count() % 2)
+                           for word in range(1, 8)]
+                require(all(w % 4 == 0 for w in weights), 'doubly even code')
+                require(sum(weights) == 4 * sum(counts[1:]), 'codeword mass identity')
+                require(binary_rank(points) <= 2, 'short code rank')
+                sums = literal_coset_sums(group, coefficients, points)
+                require(not any(sums.values()), 'lower-width operator fiber')
+                literal_fibers += len(sums)
+            if width == 6 and not any(key[1:4]) and any(key[4:]) and binary_rank(points) == 3:
+                quadratic_control = counts
+    require(total == 43758 and len(minima) == 2048, 'complete composition/character census')
+    maxima = tuple(max(v for k, v in minima.items() if k[0] == r) for r in range(4))
+    require(maxima == THRESHOLDS, 'full-span upper thresholds')
+    require(quadratic_control is not None, 'quadratic control fixture')
+    return minima, zero_phase, literal_fibers, quadratic_control
+
+def main():
+    for name, digest in SOURCE_PINS.items():
+        require(sha256((ROOT / name).read_bytes()).hexdigest() == digest, 'source drift: ' + name)
+    group = linear_group()
+    require(Counter(map(element_order, group)) == {1: 1, 2: 21, 3: 56, 4: 42, 7: 48}, 'element orders')
+    coefficients, coset_checks, types = coefficient_certificate(group)
+    minima, zero_phase, fibers, bad_quadratic = census(group, coefficients)
+    for residue, width in enumerate(THRESHOLDS):
+        counts = (width - 7,) + (1,) * 7
+        require(statistics(counts) == (residue, 0, 0, 0, 0, 0, 0), 'threshold phase')
+        require(phase_projector(counts, residue) == (2048, 0), 'literal phase projector')
+        require(phase_projector(counts, (residue + 1) % 4) == (0, 0), 'wrong-residue rejection')
+        require(literal_coset_sums(group, coefficients, support(counts))[support(counts)] == 6,
+                'nonzero threshold matrix entry')
+    controls = 0
+    for order in (1, 2, 3, 4, 7):
+        try:
+            coefficient_certificate(group, {**WEIGHTS, order: WEIGHTS[order] + 1})
+        except ValueError:
+            controls += 1
+        else:
+            raise ValueError('coefficient mutation escaped')
+    require(phase_projector(bad_quadratic, 2) == (0, 0), 'quadratic rejection')
+    require(phase_projector(bad_quadratic, 2, quadratic=False) == (2048, 0), 'quadratic omission control')
+    require(literal_coset_sums(group, coefficients, support(bad_quadratic))[support(bad_quadratic)] == 6,
+            'quadratic omission changes operator')
+    controls += 1
+    report = dict(status='PASS_THREE_AXIS_SHARP_CUTOFF', cutoff=7,
+                  residue_thresholds=list(THRESHOLDS), sufficient_and_sharp_window=[7, 8, 9, 10],
+                  gl3_elements=168, plane_cosets=coset_checks,
+                  coset_order_types={','.join(map(str, k)): v for k, v in sorted(types.items())},
+                  multiplicities=43758, phase_characters=len(minima), lower_zero_phase_multisets=zero_phase,
+                  exact_lower_image_fibers=fibers, threshold_entries=4,
+                  rejection_controls=controls, no_new_kappa=True)
+    require(report == json.loads((PACKAGE / 'RESULT.json').read_text(encoding='utf-8')), 'complete result mismatch')
+    print('PASS_THREE_AXIS_SHARP_CUTOFF ' + json.dumps(report, sort_keys=True))
+
+if __name__ == '__main__':
+    main()