bibkey: hanna2023a365771
authors: Paul D. Hanna
year: 2023
title: "OEIS A365771: Catalan-binomial residues modulo five"
doi: null
url: https://oeis.org/A365771
claim: "The three conjectures of A365771 give residues 4 at 5m, 2 at 5m+1 for positive sums m of distinct powers of five, and 0 outside the stated exceptional set."
strata_touched:
  - D5/S1/Recurrence/Residue/HannaA365771
  - D5/S1/Recurrence/Residue/HannaA365771Two
  - D5/S1/Recurrence/Residue/HannaA365771Zero
license: citation-only
triage: anchor

Hanna’s three residues modulo five

Verified locator

Source: https://oeis.org/A365771

A365771 revision 23 contains the following name and comments; an OEIS entry has no page numbers. A033042 supplies the digit-set interpretation.

Source statements

a(n) = binomial(2n+1, n)/(2n+1) * binomial(3*n-1, n) for n >= 0.

Conjectures: given A033042 is the sums of distinct powers of 5, then

(1) a(5*A033042(n)) == 4 (mod 5) for n > 0,

(2) a(5*A033042(n) + 1) == 2 (mod 5) for n > 0,

(3) a(n) == 0 (mod 5) for n > 0 except when n or n-1 equals 5*A033042(k) for some k >= 0.

The name of https://oeis.org/A033042 is “Sums of distinct powers of 5.” Its offset is zero and its initial values are 0, 1, 5, 6, 25. Membership is expressed by all digits in Nat.digits 5 m being at most one. Natural division and subtraction are used in the literal sequence formula; the quotient is exact, and natural subtraction gives a(0)=1.

Mathematical scope

The repository proofs use Lucas decomposition of the binomial product Nat.choose (3*n) n * Nat.choose (2*n) n. Its residue is the indicator of the base-five digit set, by strong induction through division by five. For positive n the exact identity 3*(n+1)*a(n)=2*M(n) determines the residue unless n has last digit four; in that case a separate Lucas factor vanishes. This proves the three conjectures and the complete positive-index classification modulo five. It asserts no result for higher prime powers.

The preregistration literature screen did not find a prior settlement; its completeness is ASSUMED-UNVERIFIED.

Computed comparison

The independent checker in trureturing-experiments, docs/reports/oeis-a365771-catalan-binomial-mod-five/check.py, is identified by commit 83566d1f13edd7b294f423fc865cc3cd179bf84e and SHA256 63334973c39e39270e57afc105b332ccb943469dbee57d215bee93c3f9802408. The command python3 check.py 6000 exits 0 and prints RESULT PASS. It compares the published data, checks the scaled identity for 1 <= n < 3000, and checks the three congruences and the valuation comparison through n=6000. These are computed observations; the Lean proofs establish the unbounded congruences and do not formalize the stronger valuation comparison.