Narayan's expanded-generator delta-set conjecture

Ashwin Narayan, The Delta Set of a Numerical Monoid Generated by a Generalized Arithmetic Sequence, arXiv:2610.02495v1, Conjecture 18.3, p. 22, states:

For $S_h=\langle a,ah,ah+d,ah+2d,\ldots,ah+kd\rangle$, $\Delta(S_h)=E(e,d)$.

Section 3 assumes $\gcd(a,d)=1$, $1<k<a$, $h>1$, and puts $e=h-1$. All four parameters are positive integers. Every displayed generator, including the redundant $ah$, is retained as a separate nonnegative factorization coordinate. The delta set is the union over represented natural numbers of positive differences between consecutive distinct lengths. The subtractive Euclidean algorithm starts at $(e,d)$; its final equal pair may be repeated without adding visited positive coordinates. These interpretations resolve the unbound $s$, omitted endpoint order and malformed initialization in Definitions 3.1–3.2, as fixed by #23185.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | All positive $a,h,d,k$ | The four natural-number binders and four positivity premises of claim | No parameter restriction is omitted. | | $\gcd(a,d)=1$, $1<k<a$, $h>1$ | Nat.Coprime a d and the three strict inequalities of claim | Literal restrictions. | | $(a,ah,ah+d,\ldots,ah+kd)$ | generators, indexed by Fin (k + 2) | The $ah$ coordinate is retained. | | Nonnegative coordinate factorizations with weighted sum $n$ | Z | The complete coordinate equation is retained. | | Length is the coordinate sum; $L(n)$ contains all such lengths | The image in L | No minimal-generator substitution. | | Positive successive length differences, over represented $n$ | delta | Strict endpoint order and no intermediate member are explicit. | | Subtractive Euclidean states and visited positive coordinates | euclidStep, euclidState, E | The initial and terminal coordinates are included. | | $\Delta(S_h)=E(h-1,d)$ | The equality in claim; result proves its universal assertion false | The witness is $(3,2,2,2)$. |

The displayed finite sums use Mathlib directly; no separate coordinate-sum alias is introduced. The implementation carrier is a product of a natural number and a finite list. Every public definition displays its complete body in the Blueprint. There are no additional source-independent hypotheses in the public claim.

The settling GID is D5/S3/Arith/Additive/NarayanExpandedGeneratorDeltaRefutation.result, with admission_basis: open-problem-resolution (#23185; Refuted). The source note is narayan2026deltaset. The Scribe attaches exactly one Refuted OpenProblemResolutionClaim to that settling theorem.

Adding $ah$ changes factorization lengths despite leaving the generated monoid unchanged. In particular, $2a$ admits both a single $2a$ coordinate and two $a$ coordinates. A finite calculation cannot exclude larger gaps at larger represented values. The proof therefore establishes complete normalization and intermediate-length realization for the whole family, without a cutoff in the represented value.

For $a>0$ coprime to $2$, put $b_i=2a+2i$ for $0\le i<a$ and use the tuple $(a,b_0,\ldots,b_{a-1})$. A configuration consists of $x$ copies of $a$ and a list of occurrences $b_i$. The rules replace $b_0$ by two copies of $a$, replace $b_i+b_j$ by $a+a+b_{i+j}$ when $i+j<a$, and replace it by $b_0+b_0+b_{i+j-a}$ otherwise. Each rule preserves value and raises length by one (rewrite_value, rewrite_size). Positive generators bound length by value (size_le_value). Strong induction on value minus length produces a terminal configuration (normalizes).

A terminal list is empty or consists of one positive index. Its residue modulo $a$ determines that index because multiplication by $2$ is cancellable modulo $a$ under coprimality (cancel_residue, using Nat.ModEq.cancel_left_of_coprime; terminal_unique). Induction over the actual rewrite trace supplies every intervening length (trace_interval). Coordinate packing and expansion preserve value and length (pack_value, pack_size, pack_expand, expand_value, expand_size, lengths_iff). Thus any length between two represented lengths is represented (family_intermediate). At value $2a$, lengths $1$ and $2$ occur, giving global delta set ${1}$ (family_delta). These helper declarations are private in the settling module.

At $a=3$, generators_three identifies $(3,6,8,10)$ with this family. The proof of result instantiates the universal assertion at $(a,h,d,k)=(3,2,2,2)$ and contradicts its initial Euclidean coordinate $2\in E(1,2)$.

The source equality predicts a gap $2$ for $(3,6,8,10)$. Complete interval realization excludes that gap for every represented value; finite-window agreement alone would not suffice. The conclusion concerns the displayed expanded tuple, not the invariant obtained by first deleting redundant generators.

D5.S3.Arith.Additive.NarayanExpandedGeneratorDeltaRefutation.result proves the literal negation of claim. Its public surface consists of the eight necessary definitions and this single theorem; all auxiliary declarations are private and consumed. It imports Mathlib only and has no D5 frozen prerequisite.

The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

Exact-arithmetic experiment

The checker is the experiments directory at revision 23c744d471f53c63a530ec05520a55c2902f2050, file check.py. Its SHA-256 is 6e39c9873b672007c385e46c4af6973fd500dbe17f6b37dc47fe46a2da1ab89a. The implementation seat verified that Git object and reran its exact bytes with python3 /Users/auric/.sshx/e7c0965424bb6ad207361044/attempt-1/experiment-check.py, exit 0, final result ALL_CHECKS_OK.

The tested scope is 87,175 rewrite identities and residue bijections for odd $a=3,\ldots,101$; 27,803 coordinate factorizations at $a\in{3,5,7,9,11}$, $0\le n\le120$; and 74,415 represented values for odd $a=3,\ldots,31$, $0\le n\le5000$. Every tested nonempty family length set is an interval and each observed delta union is ${1}$. The checker also gives $E(1,2)={1,2}$ and observes delta union ${1,2,3,4}$ for the unexpanded tuple $(3,8,10)$ through $n=2000$. These are finite computations, not the unbounded proof.

1. Proved, kernel-checked: the binding universal Conjecture 18.3 claim is false, with witness $(3,2,2,2)$ (result).
2. Proved, kernel-checked: for every positive $a$ coprime to $2$, all represented family length sets are integer intervals (family_intermediate) and the global delta set is ${1}$ (family_delta). For odd $a\ge3$, the parameters $h=d=2$, $k=a-1$ meet the source restrictions.
3. Proved: value preservation and unit length increments are kernel-checked by rewrite_value and rewrite_size; terminal reachability is kernel-checked by normalizes, and uniqueness by terminal_unique. Termination of every rewrite sequence also follows in prose: value stays fixed, length increases by one at every step, and size_le_value bounds it above by that value, so an infinite sequence is impossible.
4. Computed: $E(1,2)={1,2}$, with terminating trace $(1,2)\to(1,1)$, by the exact-arithmetic experiment above. The formal refutation uses only initial-state membership $2\in E(1,2)$, constructed directly inside result.
5. Computed: the same verified checker validates 87,175 rewrite identities, 27,803 bounded coordinate factorizations and 74,415 represented values, with the exact windows given above and final result ALL_CHECKS_OK. These windows are not the unbounded proof.
6. Computed: without the redundant $6$ coordinate, $(3,8,10)$ has observed delta union ${1,2,3,4}$ for $0\le n\le2000$, by the same checker. The paper's main theorem for the unexpanded tuple remains a separate assertion.
7. Open: classification for other $h,d,k$, sharpness of the coprimality hypothesis, and catenary Conjectures 18.1 and 18.2 are not settled here.

What the settlement shows

The failure mechanism is the extra factorization coordinate $ah$: for $h=2$ the family-specific replacements fill all intermediate lengths, while the Euclidean prediction still includes $2$. The positive coprime family above survives as the precise interval and singleton-delta statements proved by the private helpers. The computational assertion about the tuple omitting $ah$ has only the stated finite scope. The refutation supplies no conclusion about the catenary conjectures or the main theorem for unexpanded generators; an application of the expanded equality requires an independent valid replacement. No classification outside this family or sharpness of coprimality is asserted.

Literature status

The preregistration records the versioned arXiv source and earlier Narayan Zenodo preprints: the expanded equality is still a conjecture in record 22740972, while record 22888273 treats the tuple without $ah$. The screen also covers nonminimal-generator and presentation literature and the searched repository and external formalization scopes. No settlement was located within that recorded scope. Source fidelity and the mathematical proof do not establish worldwide novelty; completeness remains ASSUMED-UNVERIFIED.

Completeness of the external literature search is unverified. The preregistration records exhausted OpenAlex budget, Semantic Scholar HTTP 429, unusable general-web challenge pages, incomplete MathDB coverage and the unrecovered Banks et al. work. No exhaustive absence or priority claim is made. Classification outside the stated family, sharpness of coprimality, and catenary Conjectures 18.1–18.2 remain open.