The whole positive coefficient anti-recurrence conjecture

Robbert Fokkink and Gandhar Joshi, Anti-Recurrence Sequences, arXiv:2506.13337v1, Conjecture 4; journal version, INTEGERS 26, A24, DOI 10.5281/zenodo.18305140, Conjecture 2:

Let a = (a₁,…,aₖ) be positive and integral of dimension k > 1. Let Aₙ be the anti-recurrence sequence generated by the linear form f(x) = a·x. Then Aₙ − κn is τ-automatic for κ = kτ+1 and τ the trace of the linear form.

Here τ = Σ aⱼ. The strictly increasing positive sequences A and B partition the positive integers and satisfy Aₙ = Σⱼ₌₁ᵏ aⱼ Bₖ₍ₙ₋₁₎₊ⱼ for every n ≥ 1.

The theorem constructs a source for every such vector, proves its uniqueness, and supplies a finite DFAO with integer output computing Aₙ − (kτ+1)n on the standard base-τ digits read most significant first. Its equality includes every positive index and the exact initial segment. The auxiliary zero terms and negative padding used inside the proof are separate from the positive source indexing.

The published source proves the conjecture for all-ones vectors and under an additional restriction on the linear form. Those families, including the earlier anti-Fibonacci, anti-Tribonacci and anti-Tetranacci results, receive no separate new credit. The whole-family literature qualification concerns the unrestricted positive coefficient vector. Its bounded search does not certify worldwide priority.

The formal statement imposes neither an A₁ bound nor a restriction to a finite coefficient catalogue. It constructs the source rather than assuming the existence of sequences satisfying its equations.

1. A finite-history complement enumeration constructs successive A terms. Each new term lies beyond its generating B block, so stabilization defines the infinite complement and proves uniqueness.
2. Counting A terms below Bₘ gives Bₘ = m+t and the exact inverse interval Aₜ−t < m ≤ Aₜ₊₁−(t+1).
3. The weighted inverse identities yield a uniform discrepancy bound by strong induction. All inverse ranks used beyond a fixed initial segment are earlier indices.
4. Bounded inverse offsets give an exact local rule: equal bounded discrepancy windows at sufficiently large quotient indices give equal discrepancies after the same base-τ digit.
5. A finite feature stores the padded window and a capped index. The cap preserves every small index exactly. The local rule makes the feature transition well defined, producing a native finite DFAO. Word evaluation and the standard digit-value identity prove the exact output at every index.

The paired Blueprint gives the identities, bounds and window radii.

A mismatch between the source's complement convention, coefficient ordering, block indices, slope, digit order or positive-index output would invalidate the claimed correspondence. An unproved boundedness or finite-window premise would leave the whole conjecture unresolved.

The mathematical result is D5/S1/Recurrence/AntiRecurrenceAutomaticity.result. Its quantified conclusion contains source existence, source uniqueness and a native finite output automaton for the full integer discrepancy. Its axiom closure is contained in {propext, Classical.choice, Quot.sound}. The Lean and exposition are independently authored. The Library entry records the primary-source attribution and rights.

Proved: the whole positive coefficient conjecture, with the actual inhabited unique complementary source, unshifted integer discrepancy and every positive index, follows from D5/S1/Recurrence/AntiRecurrenceAutomaticity.result. The two publication numbers designate this one question. The source's all-ones and other restricted automaticity theorems remain known special cases; no coefficient or A₁ restriction is required by the whole result.

Proved mechanism: complement stabilization supplies the source, and counting below each complementary term determines its inverse rank. The weighted rank identity gives a uniform discrepancy bound for each fixed vector. Bounded rank offsets then make equal finite discrepancy windows have equal digit successors. A capped index retains the exact small-index behavior, allowing one finite DFAO to handle the entire sequence.

Proved weaker consequence: the source's bounded-discrepancy question holds for every positive coefficient vector. This bound is an intermediate result of the proof, rather than a replacement for automaticity or a separate independent problem resolution. The whole result removes the restriction on applying the source's automaticity conjecture; it does not alter the hypotheses or conclusions of the source's other theorems.

Unresolved here: a uniform machine construction across coefficient vectors, minimal state counts, an executable machine generator and runtime bounds. The constants and finite state space in the theorem may depend on the vector. No optimal discrepancy bound or extension to zero or negative coefficients, or to dimension one, is established. No additional independent neighbouring theorem is asserted.

Prospective resolution issue: https://github.com/the-omega-institute/trureturing/issues/17371.

There is no additional unverified mathematical premise in the theorem. The bounded literature and ownership qualification inspected the original arXiv and journal statements, the earlier restricted results, and relevant repository, pinned-library and public Lean suppliers. It found no earlier whole-family answer or exact supplier within that scope. Unindexed, differently worded, later, private or unpublished results and ownership remain unexcluded. No worldwide absence, priority or independent-invention claim follows from that search. The Library note records the source identity, rights and inspected literature boundaries. Independent review and release verification are separate from the mathematical conclusion.