trureturingGitHub MATHEMATICAL ATLAS

RESEARCH / Focused target

Tebni's prime and dyadic row-divisibility conjectures for A341724

Literature status: not recheckedRepository record: proved

RELEASED FOUNDATIONS / PROPOSED CONNECTION

Research connections

0 released anchors
All source anchors (1)

Problem

The question

The Comments block of OEIS A341724, revision 26, attributes these conjectures to Mélika Tebni in 2023:

For 0 < k < p and p prime, T(p,k) == 0 (mod p).

For 0 <= k < n and n = 2^m (m natural number), T(n,k) == 0 (mod n).

The Formula block specifies the column EGF as $x^k/(k!(1-2\sinh(-x)))$. The conjectures concern $T(n,k)=n![x^n]x^k/(k!(1-2\sinh(-x)))$ over the rationals. The 2021 Shannon–Ollerton paper describes the array, rather than stating these 2023 conjectures.

Motivation

Our foothold

This is a tier-one external open-problem settlement under preregistration #23158. The source EGF and both full domains, including p=2, m=0 and dyadic k=0, are preserved. Integrality is a conclusion, supplied before the integer numerator is used as the witness. There is no finite row bound.

Gap

Missing bridges

No exact prior settlement was found in the bounded source and library screen in #23158. Repository searches include public and private D5 statements and theory/digestion correspondence. The pinned Mathlib and GitHub Lean-code searches have no exact A341724 settlement in the searched scope. These negative searches do not establish exhaustive originality.

Route

Proposed approach

Set $H=1-2\sinh(-X)=1+2\sinh X$ and $C_k=X^k/(k!H)$. Then $C_k H=X^k/k!$, and the factorial-normalized convolution gives

$$ T(n,k)=\mathbf{1}{n=k} -2\sum{\substack{1\le j\le n\j\text{ odd}}} \binom nj T(n-j,k). $$

The forcing term is present for all n and k. The column support gives $T(n,k)=0$ for n<k and the diagonal is one. Strong induction proves all coefficients integral. The recurrence is transferred to integers only after this bridge is established.

For n>k the forcing term vanishes. At a prime row, the interior binomial coefficients are divisible by p. The j=p endpoint is zero because $k>0$ implies $T(0,k)=0$. At a dyadic row, every odd-index binomial coefficient is divisible by $2^m$; this includes m=0 without an extra hypothesis. The original suppliers are IntegralEGFComposition.eCoeff_mul, TebniA364822.eCoeff_sinh, TebniA364822PowerOfTwo.pow_two_dvd_choose_odd, and Nat.Prime.dvd_choose_self.

Falsifier

What would falsify this route

A nonintegral original-array coefficient at an allowed row and column, or an allowed integer coefficient not divisible by its row modulus, would refute the corresponding assertion. A recurrence with reversed sign or without the exact EGF correspondence is a different object.

Evidence

Evidence to collect

The Lean result proves both integer-witness clauses in one result : claim. The Blueprint contains the complete formulas, and the source note records the source attribution and locator. The proof has only the standard axiom closure; no finite table is a premise.

Triage

Scope assessment

What the settlement shows

  • Proved (D5/S1/Recurrence/Residue/TebniA341724RowDivisibility.result): both original divisibility assertions for every prime and every dyadic exponent, within their exact column ranges.
  • Proved internally: integrality for all natural n,k, zero support for n<k, diagonal value one, and the complete delta-forced recurrence. These are proof ingredients of the single public result.
  • Mechanism: denominator cancellation gives the binomial recurrence; integrality makes integer divisibility meaningful; prime interior binomials and odd-index dyadic binomials make the relevant terms vanish.
  • Nearest retained ranges: the prime case includes two and requires positive k; the dyadic case includes exponent zero and column zero. Both require k strictly below the row. The diagonal value one explains the exclusion for row modulus greater than one.
  • Unresolved boundary: the public result does not settle arbitrary composite rows, exact valuations, or any stronger modulus. The recurrence suggests further statements, but no such public theorem is claimed here.
  • Open — impact on other source results and questions: no further dependence or consequence has been established in this delivery, so no additional source assertion is certified by this settlement.
  • Literature: the source definitions are literature-attested; the settlement is repo-derived with status not-found-in-searched-scope. Global novelty and exhaustive search completeness remain unverified.

ASSUMED-UNVERIFIED

Unverified assumptions

Exhaustive literature priority and search completeness are not established. The proved prime and dyadic claims have no extra assumed mathematical premise. Arbitrary composite-row divisibility, exact valuations, stronger moduli, and downstream conclusions are not established here.

Dossier & anchor history

Loading release observations...