DONE: four widths decide affine-quadratic native identities

[aliromman]

Status: DONE / author-checked / 2026-10-23 19:50 UTC / priority revision 7. Claim released.

For fixed n-axis binary affine/quadratic Gaussian monomials, a complete scalar register identity holds at all positive tensor widths if and only if it holds at 2n+4 through 2n+7. The proof constructs a nonzero basis entry for every false identity, with input/output addresses encoded in O(n²) bits, and proves phase-residue kernel stabilization by 2n+4. Four widths are necessary for the full group; the least cutoff remains open. Public artifact: PR #5369, exact head 18354f41de4dc7bfda4692e814cf1d91a6d619ef. The selected κ is unchanged. This is a written uniform proof with separate implementation checks, not independent human or proof-kernel acceptance. No further claim is reserved.

Read the proof, contributor guide and exact replay receipt. The new endpoint checker uses actual native inverse, commutation, finite-order and phase relations. It preserves every dirty input and return. It does not construct the four large tensor matrices. Sparse support can still be exponential.

The result includes two limits on finite testing and computation. A rank-projector family is zero at all widths below n and nonzero at n. Complete identity testing is coNP-complete even for five arbitrary dirty roles with reversible instructions and commuting native sign generators. The latter uses Barrington's classical width-five construction and an explicit five-step controlled swap; it requires no zero input or erase.

The actual event8814 recipe gives a positive complete conjugation identity. Removing its global sign passes the even-width probes and fails at the generated width-25 witness. Normal and optimized CPython 3.12.14 replays agree. The registered replay, 37 rejection controls, eight mathematical code-mutation rejections, committed-byte checks, official export integrity, and normal/optimized Git-free replays in a fresh read-only export pass. Exact domains and counts are in the receipt.

The theorem excludes nonmonomial Hadamard operators, arbitrary width-dependent programs, nonlinear leaves, external aliases and rectangular types. It does not supply a physical native invoice, a complete packet/dispatcher binding, compiler admission, precision/tape implementation or a new multiplication exponent. No selected cold replay, Lean, Docker or full-history ancestry check was run. The shallow checkout's recorded source objects and retained bytes were checked.

Next useful task: independently review the phase-character construction, its affine-basis separation, the residue quantifiers and the reversible complexity reduction. Start with proof Sections 2, 3, 5 and 6 and the direct replay. A later mathematical extension could determine the least stabilized width, or supply a quantitative theorem for a specified nonmonomial Clifford group. These are open questions, not a reservation or an admitted supplier.

The PR records exact source pins and predecessor credit: Jose Manuel's native recipe and earlier phase-sector construction; the binary-stream affine-basis proof prepared for ywz65; Chris R's general tensor-separation arguments; JoyboyBrian and Cinna Davis's fixture/caller lineage; and zxv and Krzysztof Wójt's independent/inverse certificate interfaces. Lempel, Fourier inversion, Burnside-Brauer, Pauli conjugation, SAT completeness and Barrington retain their classical credit. New work by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. No global literature priority is claimed.

The final refreshed snapshot covered 316 open PRs and 4,648 Discussion records with complete remote pagination. Canonical main remained 7c472563474e60185e6ca101a17622133d047e56. The physical-stack, CRT-entry and p16 fusion claims remain separate. Arbitrary historical diffs and unpublished work were outside the overlap coverage.

Original prospective claim, retained for history

CLAIM — a constructive finite tensor cutoff for affine-quadratic native identities

Question: Can complete scalar register identities over the exact binary affine/Gaussian-phase monomial family be decided for all positive column multiplicities, with a counterexample using at most 2n+7 columns when they fail? Here a native map is |x> -> i^(c+a.x+2 sum b_ij x_i x_j)|Ax+t>, on n binary axes, with A invertible. Scalar coefficients stay outside tensor powers; all dirty input and return roles remain independent. This is the exact monomial recipe grammar in PR2250, not the full Clifford group with Hadamard gates.

I will prove or refute an explicit short witness construction. Group residual terms by their affine map, choose a nonzero Fourier character of the quadratic phase coefficients, and realize that character on an affinely spanning tuple using a binary symmetric Gram factorization and two-copy phase correction. The tentative cutoff is linear in n, independent of program length or expanded residual support. A complementary rank-projector family should show that tests of any fixed small set of widths are insufficient as n grows. These statements are prospective until checked.

Expected artifact: a dimension-uniform proof, exact canonical native composition/inversion and complete dirty endpoint checker, compact concrete input/output witness construction, an independently transcribed witness checker, source binding to the actual PR2250 recipe convention and event8814 recipe, and exact rejecting controls. Word expansion may be exponential; no polynomial-time circuit identity test, full native compiler, physical invoice, new kappa or selected-frontier change is promised. The target is a general reusable algebraic interface, not one additional circuit identity.

Base: refreshed canonical main 7c472563474e60185e6ca101a17622133d047e56, priority revision7. The public snapshot covered 304 open PRs and 4,621 Discussion records; a live newest-discussion check followed it. Exact cutoff/faithful-tensor/phase-character searches and the relevant native source were inspected. The independent/inverse operator packages have a different grammar; the finite-alphabet separation arguments in PR4928/4978 are retained predecessors. The active physical-stack, CRT entry and p16 block-fusion claims are outside this scope. Arbitrary historical diffs and unpublished work remain coverage limits.

Credit Jose Manuel/jmbarrancoml and Douglas Colkitt for PR2250 and its recipe interface; JoyboyBrian and Cinna Davis for the source-bound event fixture and retained caller; zxv and Krzysztof Wojt for the related complete dirty-circuit certificate line; the source authors of PR4928/4978 for their tensor-separation use. Binary symmetric Gram factorization (Lempel), finite Fourier inversion and Burnside-Brauer tensor generation are classical. No global mathematical priority is claimed. New work by Ali Romman (@aliromman) with substantial OpenAI Codex assistance. Author-checked evidence only; no independent human or proof-kernel review. Claim expires 2026-10-23T21:15:00Z and will be renewed if needed.

[aliromman]

DONE — the complementary full-Clifford result in PR #5376 is extended at 5370f4465388dbbfff3ba45d5d6ae99d447b1766. The extension proof gives eight selected widths for n>=2, a sharp one-axis maximum cutoff eight, 75/76 separation over the full width range, and compact phase-exact native certificates with bitwise witnesses. It includes Hadamard gates. Fixed coefficients across widths remain essential; expanded support can still be exponential.

This thread's monomial four-width criterion has its own stronger cutoff within that smaller class. Its phase-character argument, complexity result and event fixture remain distinct, credited and unchanged. No new kappa or complete supplier admission is claimed. Canonical DONE and evidence. Local verification, export replays and hosted CI pass. The claim is released. Ali Romman with substantial OpenAI Codex assistance.

[mihir-s-05]

DONE / 2026-10-25 06:30 UTC / priority revision 7. Claim released. PR #5521, head 5fe6693dd023cedddb0972f1006d7fa50ba94595, completes the scoped audit of PR5369 Sections 2, 3 and 5 and proves the sharp one-axis monomial test at widths 3,4,5,6. Both four tests and maximum width six are necessary. The separate exact checker imports no predecessor executable. Normal/optimized registered checks, twelve mutation rejections, committed-byte checks and read-only Git-free exported replays pass locally. This is agent-assisted mathematical review with an independently written checker, not independent human or proof-kernel acceptance. Section 6, the general implementation/source adapter and physical admission remain outside the audit. No new kappa or selected-frontier change.

Proof and scope · package and commands · exact receipt · mutation receipt

The audit finds no gap in the stated phase-character construction, affine-bucket separation and fixed-residue implication. It spells out singular binary forms, the two-copy modulo-four repair, and the need for a single fixed group-algebra residual across widths. The code independently enumerates all 391,275 bounded multisets for 2,192 characters through three axes, checks 29,760 literal phase-generator values and 200,378 affine restrictions, and computes the one-axis ranks from 2,044 literal matrix-entry rows.

For one axis the rank is 2 min(f+1,4). The first two four-width windows have ranks 26 and 30; widths 3..6 have rank 32. An explicit central-phase/weight projector vanishes at every positive width below six and has entry 16 at width six. This sharpens a sufficient specialization; it does not contradict Ali Romman's general cutoff or apply to the larger full Clifford group.

Hiroki KUMAZAKI's two-axis investigation is complementary. Our n=2 character minima are corroboration, not a competing representation-kernel theorem. The smallest remaining audit tasks are (1) Section 6's dirty controlled-swap/CNF reduction and exact size bounds, and (2) the predecessor compiler/native grammar at a named source-bound caller, keeping every dirty input and return. Neither is reserved by this completed claim.

Canonical main remained 32890bc5de034ab8fc93ac88ead7279a6a416d04. Final overlap at 06:22 UTC reported complete pagination/inventory for 378 open PRs, 4,797 Discussion records and all 7,402 tracked base notes; arbitrary diffs and unpublished work are outside it. Selected metadata orientation passes. No selected cold replay or full-history ancestry preflight was run. Hosted CI planning and the scoped package replay also pass at the published head: GitHub Actions run.

Ali Romman retains the general theorem and witness construction. Credit Jose Manuel, ywz65, Chris R, Douglas Colkitt, JoyboyBrian, Cinna Davis, zxv, Krzysztof Wójt and the retained source lineage. Binary symmetric factorization, Fourier inversion and projectors are classical. Prepared for Mihir Srivastava with substantial OpenAI Codex assistance, one agent; Apache-2.0.

Original prospective claim prose, retained verbatim

CLAIM / 2026-10-25 06:11 UTC / priority revision 7. I am taking the independent-review handoff for PR #5369, restricted to proof Sections 2, 3 and 5: phase-character realization, affine-bucket separation and the fixed-residue quantifiers. Source: Ali Romman's 18354f41de4dc7bfda4692e814cf1d91a6d619ef; current canonical main is 32890bc5de034ab8fc93ac88ead7279a6a416d04. No result or public artifact is claimed yet. Expiry: 2026-10-25T08:11:00Z.

The artifact will pair a written obligation-by-obligation audit with a code-disjoint exact multiset enumerator for all characters through three axes, literal phase/affine checks, and a direct Gaussian matrix-rank check of the one-axis representation. I will also prove or refute the tentative one-axis cutoff of widths 3,4,5,6; this smaller monomial group is distinct from PR5376's one-axis full-Clifford cutoff. No predecessor verifier or arithmetic implementation will be imported.

This is a changed scope from the formal-interface-lemma card: the live handoff requests a mathematical audit before formalization. Section 6's complexity reduction, the actual event8814 recipe adapter, physical admission, and the least cutoff for n>=2 are outside this claim. Stop after the scoped audit, bounded positive/rejection controls and reproducible evidence, or a concrete gap. No new kappa or selected-frontier change.

Overlap: read this canonical thread and the central handoff, the partially reviewed ledger entry, relevant local notes and current PR searches. The full repository overlap refresh is running; its coverage/limits will be recorded before submission. Related full-Clifford work and the predecessor's own finite checks retain their credit. Ali Romman, Jose Manuel, ywz65, Chris R and the retained classical/source lineage are credited. Prepared for Mihir Srivastava with substantial OpenAI Codex assistance, one agent; Apache-2.0.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"formal-interface-lemma","scope":"Independent audit of PR5369 Sections 2/3/5 and exact one-axis monomial cutoff","base":"32890bc5de034ab8fc93ac88ead7279a6a416d04","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/5521"}

[kumagi]

DONE — the sharp two-axis native tensor cutoff is F=6. The scoped claim is released.

PR #5522, exact head ffb5adf6a2509a7c99f564d13b74fc82a51b5adc, supplies the proof, exact receipt and verification record.

For PR5369's full two-axis affine/quadratic Gaussian monomial grammar, the exact per-central-residue thresholds are (8,9,6,7). Hence 6,7,8,9 decide every fixed group-algebra/register identity, improving the sufficient two-axis window 8–11. More generally a test set is complete exactly when it reaches the appropriate threshold in every residue. This is a central-quotient kernel theorem, not just a character-realization table.

Sharpness uses AGL(2,2)=S4: pointwise stabilizers of tuples using at most two addresses contain an odd permutation. A normalized phase projector followed by the affine alternating sum supplies four explicit obstruction residuals. The residue-one residual is zero at every width 1–8 and has diagonal entry 1 at width 9 on (0,2,2,2,2,3,3,3,3). Three distinct addresses give trivial stabilizers and expose individual Fourier coefficients. Exact multiplicity congruences plus an analytic case split prove sufficiency for all widths; finite checks corroborate it.

Evidence: registered normal and optimized Python 3.12 replay; committed-byte/source-history preflight; official 14-file export and optimized Git-free replay with PATH=/nonexistent, all passing. Separate implementations cover 128 character minima against 625 count normal forms, 24 affine maps, 128 phases, all 15 stabilizers, 1,364 below-threshold ordered tuples, 2,856 phase sums, all four threshold witnesses and semantic controls. Hosted CI is running at publication; the PR links its status. No predecessor evaluator is imported.

Scope/limits: two-axis monomial algebra over Q(i) or C, fixed external coefficients and complete dirty input/output endpoints. This does not change the general-axis theorem, the selected nine-axis supplier or κ. Physical implementation costs, full supplier admission and n>=3 remain separate. The necessity proof depends on S4's sign representation and is not silently generalized. No independent human or proof-kernel acceptance, global literature priority, or full producer/compiler/outer/selected cold replay is claimed.

This complements Mihir Srivastava's active one-axis/general-proof audit, whose claim excludes least cutoffs for n>=2. Small-character enumeration is overlapping corroboration, not the new theorem claimed here. The remaining mathematical handoff is to identify the phase-fiber stabilizer coset-sum kernels for n>=3; another affine-span census alone would not prove necessity.

Base main 32890bc5de034ab8fc93ac88ead7279a6a416d04; PR5369 head 18354f41de4dc7bfda4692e814cf1d91a6d619ef, unchanged at the publication refresh. Submission overlap through 06:27:01 UTC covers 379 open PR bodies, 4,797 Discussion records and all 7,402 base local notes. No matching two-axis theorem appeared in that coverage; arbitrary diffs and unpublished work remain outside it.

Credit Ali Romman's uniform theorem and open question, Jose Manuel's native/phase conventions, ywz65's affine-basis argument, Chris R's tensor-separation lineage, Douglas Colkitt and retained source contributors. Fourier inversion and symmetric-group sign representations are classical. Prepared by Hiroki KUMAZAKI with substantial OpenAI Codex assistance, including separate automated proof, checker and adversarial-review subagents. Frozen predecessor files and the selected frontier remain unchanged.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"formal-interface-lemma","scope":"Sharp two-axis affine-quadratic tensor kernel cutoff and phase-sign lower-bound witnesses, complementary to the one-axis audit","base":"32890bc5de034ab8fc93ac88ead7279a6a416d04","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/5522"}

[fluorine]

DONE / author-checked — PR #5542, head dc2b1ff, settles the three-axis sharpness question left by #5529. The exact representation thresholds are (8,9,10,7), so F=7 and the window 7–10 is optimal. No new κ.

The lower witness uses classical doubly-even binary codes: zero nonconstant phase forces the three row words to be doubly even and self-orthogonal. At f<=6, three independent rows would have seven nonzero words of total weight >=28, whereas the columns contribute at most 4f<=24. Thus their address span lies in a linear plane. An explicit GL(3,2) sum with order-class coefficients (6,-2,0,2,-1) has zero sum on each pointwise-plane-stabilizer coset. Composing with four phase projectors gives fixed residuals; the residue-two residual vanishes at every width 1..9 and has diagonal entry six at ten. This supplies necessity beyond the full-span character census; it does not classify the entire low-width kernel.

Proof and scope. Registered normal/optimized CPython3.12 checks pass locally and on hosted Linux and Windows. Separately written implementations reconstruct all 168 linear maps, 2048 characters, 65536 residue vectors and 299593 ordered words; exact committed/export bytes and Git-free replays pass. Same-agent corroboration is not independent human or proof-kernel acceptance. No physical supplier, compiler/precision/stock/outer admission or selected cold replay is claimed.

Credit Ali Romman for #5369/#5529 and the upper bound/open question, Hiroki KUMAZAKI for #5522 and the stabilizer-kernel distinction, Mihir Srivastava for #5521, and the retained native/phase lineage. Classical Fourier/group/code methods retain their credit. Prepared for Joseph Anglada (@fluorine) with substantial OpenAI Codex assistance; Apache-2.0. PR #5542 is the canonical artifact; no ongoing claim is reserved.