Hanna’s Catalan-binomial residues modulo five

Abstract

Base-five digit descent proves Hanna’s first residue and the shared classification.

The sequence is a product of a Catalan quotient and a binomial coefficient. All indices and arithmetic operations below are in Nat. Nat.div denotes natural integer division; subtraction is truncated at zero. The quotient in a is exact. The digit predicate includes zero. OEIS entries have no page numbers; quotations refer to A365771 revision 23, Name and Comments, and A033042, Name.

Definition 1.1 (The sequence).

$$\forall n\in \mathbb{N},a\left(n\right)=Nat.div\left(Nat.choose\left(2\cdot n+1,n\right),2\cdot n+1\right)\cdot Nat.choose\left(3\cdot n-1,n\right)$$

Formalization. D5/S1/Recurrence/Residue/HannaA365771.a (✓ std3).

Citation. Paul D. Hanna (2023). OEIS A365771: Catalan-binomial residues modulo five. URL: https://oeis.org/A365771.

Commentary.

a(n) = binomial(2n+1, n)/(2n+1) * binomial(3*n-1, n) for n >= 0. The index n is a natural number, including zero; Nat.choose denotes binomial.

Definition 1.2 (Sums of distinct powers of five).

$$\forall m\in \mathbb{N},(InA033042\left(m\right))\iff (\forall d\in \mathbb{N},(d\in Nat.digits\left(5,m\right))\Rightarrow (d\le 1))$$

Formalization. D5/S1/Recurrence/Residue/HannaA365771.InA033042 (✓ std3).

Citation. Paul D. Hanna (2023). OEIS A365771: Catalan-binomial residues modulo five. URL: https://oeis.org/A365771.

Commentary.

Sums of distinct powers of 5. The value m is in A033042 exactly when every digit in Nat.digits 5 m is zero or one. The offset is zero: 0, 1, 5, 6, 25.

Definition 1.3 (Hanna’s first conjecture).

$$claim\iff (\forall m\in \mathbb{N},(0<m)\Rightarrow ((InA033042\left(m\right))\Rightarrow ((a\left(5\cdot m\right))\mathrm{mod}5=4)))$$

Formalization. D5/S1/Recurrence/Residue/HannaA365771.claim (✓ std3).

Citation. Paul D. Hanna (2023). OEIS A365771: Catalan-binomial residues modulo five. URL: https://oeis.org/A365771.

Commentary.

Conjectures: given A033042 is the sums of distinct powers of 5, then (1) a(5*A033042(n)) == 4 (mod 5) for n > 0, Here m ranges over the positive values of A033042, rather than their enumeration indices.

Theorem 1.4 (Removing the last base-five digit).

$$\forall n\in \mathbb{N},(0<n)\Rightarrow ((InA033042\left(n\right))\iff (((n)\mathrm{mod}5\le 1)\wedge (InA033042\left(Nat.div\left(n,5\right)\right))))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Residue/HannaA365771.digits_step (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A365771: Catalan-binomial residues modulo five. URL: https://oeis.org/A365771.

Commentary.

For positive n the digit condition separates into the last digit being at most one and the same condition on Nat.div n 5.

Theorem 1.5 (The complete positive-index classification).

$$\forall n\in \mathbb{N},(0<n)\Rightarrow ((a\left(n\right))\mathrm{mod}5=\mathrm{if}(InA033042\left(n\right))\mathrm{then}(\mathrm{if}((n)\mathrm{mod}5=0)\mathrm{then}(4)\mathrm{else}(2))\mathrm{else}(0))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Residue/HannaA365771.residue_classification (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A365771: Catalan-binomial residues modulo five. URL: https://oeis.org/A365771.

Commentary.

Lucas decomposition makes Nat.choose (3n) n * Nat.choose (2n) n congruent to the indicator of the digit predicate. Strong induction on n proves this through division by five. The exact identity 3*(n+1)a(n)=2M(n), where M is that binomial product, determines the residue at last digits zero through three. At last digit four, Nat.choose (3*n-1) n vanishes modulo five directly by Lucas. The resulting classification is used by all three congruences.

Theorem 1.6 (Hanna’s first congruence).

$$\forall m\in \mathbb{N},(0<m)\Rightarrow ((InA033042\left(m\right))\Rightarrow ((a\left(5\cdot m\right))\mathrm{mod}5=4))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Residue/HannaA365771.result (✓ std3). ∎

Resolves. Problems/hanna365771-mod5 (proved) by D5/S1/Recurrence/Residue/HannaA365771.result.

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A365771: Catalan-binomial residues modulo five. URL: https://oeis.org/A365771.

Commentary.

Multiplication by five appends a zero base-five digit. The classification therefore gives residue four for every positive m with digits zero or one.

References

• Truth anchor: D5/S1/Recurrence/Residue/HannaA365771.InA033042
• Truth anchor: D5/S1/Recurrence/Residue/HannaA365771.a
• Truth anchor: D5/S1/Recurrence/Residue/HannaA365771.claim
• Truth anchor: D5/S1/Recurrence/Residue/HannaA365771.digits_step
• Truth anchor: D5/S1/Recurrence/Residue/HannaA365771.residue_classification
• Truth anchor: D5/S1/Recurrence/Residue/HannaA365771.result