[fluorine]

Change and mathematical scope

This settles the sharpness question explicitly left open in #5529: for the full three-axis affine/quadratic Gaussian monomial grammar, the least stabilized cutoff is F=7, with exact central-residue thresholds (8,9,10,7). Thus the sufficient window 7,8,9,10 is optimal. A fixed nonzero residual is zero at every width 1..9 and has a diagonal entry equal to six at width ten. The selected multiplication κ is unchanged.

The new ingredient is an explicit stabilizer-kernel witness, rather than another affine-span census. Zero nonconstant phase makes the three binary row words a doubly even code. Three independent rows would give seven nonzero codewords of total weight at least 28, but the columns contribute at most 4f<=24 below seven. An explicit GL(3,2) group-algebra element then annihilates every remaining tuple: its coefficients by element order (1,2,3,4,7) are (6,-2,0,2,-1), and every plane-stabilizer coset has coefficient sum zero. Four phase projectors give the four sharp residuals.

PROOF.md states the complete test-set criterion and quantifiers. This adds necessity to Ali Romman's sufficient upper bound; it does not classify the entire low-width kernel. Fixed external coefficients, the input-phase convention and every dirty input/returned role remain essential. Hadamards, width-dependent program families, physical costs and supplier/compiler admission are excluded. This is a written computer-assisted algebraic proof, not independent human or proof-kernel acceptance.

Task and overlap

The donor explicitly requested a mathematical attempt after a tooling round. Scope changed from the formal-interface-lemma card to this written interface theorem; no Lean formalization is claimed. TASK.json retains the original card and records the scoped decision. Base/refreshed canonical main: 32890bc, priority revision 7. Contribution: dc2b1ff.

Nearest work: #5529 (sufficient three-axis window, exact head 0fac48c); #5522 (sharp two-axis result); #5521 (one-axis/general audit); #5369 (grammar/Fourier theorem). The original grammar proof is source-pinned at main. A byte-exact, Git-blob/SHA256-bound snapshot of #5529's README retains its proof, scope and attribution; no predecessor executable is imported or changed. Targeted all-state searches for three-axis cutoff/kernel/sharpness and doubly-even work, the current source PR and handoffs, and Discussion #5354 were checked. Broader Discussion history, arbitrary diffs and unpublished work were not exhaustively searched; no global novelty claim is made.

Validation

Python 3.12, standard library only:

python -B scripts/research_package.py --package research/three-axis-sharp-cutoff
python -B scripts/check_research_commit.py --package research/three-axis-sharp-cutoff

Registered normal and optimized, isolated and warning-strict replays pass locally on Windows and in hosted Linux and Windows checks, checking the immutable contribution commit. The manual workflow is separately maintained on the contributor fork.

• Primary certificate: all 168 GL3 maps, 294 plane cosets, exact A²=56A, all 43758 multiplicity vectors through ten, all 2048 characters, literal Gaussian phase sums and all four nonzero threshold entries. Five coefficient-class mutations and an omitted-quadratic-phase control are rejected.
• Separately written audit: enumerate XOR-preserving permutations, rederive the coefficients by rational linear solves, check all 65536 base-four normal forms and all 299593 ordered inputs through six, including 784 zero-phase words and 27496 exact output fibers. This is a second implementation in the same agent context, not a separate human reviewer.
• All 11 package/input payloads match the published commit. Official committed export and integrity checks pass; all four commands pass from the Git-free export with empty PATH/PYTHONPATH and unchanged hashes for its 12 files including the export receipt.

No full selected cold replay, physical/native supplier execution, compiler/precision/stock/outer admission, Lean or Docker run is claimed. Full-history provenance checking refuses the shallow checkout and was not completed; exact source objects, payload bytes and the direct canonical-base parent were checked.

Credit

Prepared for Joseph Anglada (@fluorine), with substantial OpenAI Codex assistance in derivation, programming, checking and writing. Credit Ali Romman for #5369/#5529 and the open question; Hiroki KUMAZAKI for #5522's two-axis sharpness and representation-kernel distinction; Mihir Srivastava for #5521; Jose Manuel, ywz65, Chris R and the retained native/phase/compiler lineage. GL(3,2), finite Fourier inversion and doubly-even/simplex-code methods are classical. New work Apache-2.0; the source snapshot retains its original notice. No general literature-priority claim.

Open next questions

The README and TASK.json give bounded first steps for higher-axis stabilizer annihilators and binding a complete physical three-axis endpoint. Neither is supplied here. κ remains 605457647/200000000000.