Hanna’s A369673 conjectures

Abstract

Hanna A369673 square classification and five-adic orders.

Definition 1.1 (a).

$$\forall N\in \mathbb{N},a\left(N\right)=\prod _{k\in \mathrm{Finset}.\mathrm{range}\left(N+1\right)}((2:\mathbb{N}{)}^k+2^{N-k})$$

Formalization. D5/S3/Arith/FactorialRatio/HannaA369673.a (✓ std3).

Citation. Paul D. Hanna; N. J. A. Sloane; Reinhard Zumkeller (2024). OEIS A369673, square classification and five-adic orders, with A127428 and A112765. URL: https://oeis.org/A369673/internal.

Commentary.

OEIS A369673, NAME (unpaginated): “a(n) = Product_{k=0..n} (2^k + 2^(n-k)).” The natural index N includes zero. Finset.range (N + 1) includes exactly k = 0 through k = N; subtraction in the exponent is natural subtraction.

Definition 1.2 (b).

$$\forall n\in \mathbb{N},b\left(n\right)=(\mathrm{padicValNat}\left(5,\mathrm{Nat}.\mathrm{factorial}\left(10\cdot n\right)\right):\mathbb{Z})-(\mathrm{padicValNat}\left(5,\mathrm{Nat}.\mathrm{factorial}\left(5\cdot n\right)\right):\mathbb{Z})$$

Formalization. D5/S3/Arith/FactorialRatio/HannaA369673.b (✓ std3).

Citation. Paul D. Hanna; N. J. A. Sloane; Reinhard Zumkeller (2024). OEIS A369673, square classification and five-adic orders, with A127428 and A112765. URL: https://oeis.org/A369673/internal.

Commentary.

OEIS A127428, NAME (unpaginated): “v_5( (10n)! ) - v_5( (5n)! ), where v_p(N) is the p-adic valuation defined in A112765.” The difference is in the integers, and factorials are natural factorials. OEIS A112765, NAME (unpaginated): “Exponent of highest power of 5 dividing n. Or, 5-adic valuation of n.” All valuation arguments here are positive.

Definition 1.3 (claim).

$$\mathrm{claim}=((\forall N\in \mathbb{N},\mathrm{IsSquare}\left(a\left(N\right)\right)\iff \left(\neg ((4:\mathbb{N})\mid N)\right))\wedge ((\forall n\in \mathbb{N},\neg ((5:\mathbb{N})\mid a\left(2\cdot n+1\right)))\wedge ((\forall n\in \mathbb{N},(\mathrm{padicValNat}\left(5,a\left(4\cdot n\right)\right):\mathbb{Z})=2\cdot b\left(n\right))\wedge (\forall n\in \mathbb{N},(\mathrm{padicValNat}\left(5,a\left(4\cdot n+2\right)\right):\mathbb{Z})=2\cdot b\left(n+1\right)))))$$

Formalization. D5/S3/Arith/FactorialRatio/HannaA369673.claim (✓ std3).

Citation. Paul D. Hanna; N. J. A. Sloane; Reinhard Zumkeller (2024). OEIS A369673, square classification and five-adic orders, with A127428 and A112765. URL: https://oeis.org/A369673/internal.

Commentary.

OEIS A369673, COMMENTS (unpaginated): “Conjectures:” “(C.1) a(n) is a square iff n is not divisible by 4.” “(C.2) a(2n+1) is not divisible by 5 for n >= 0.” “(C.3) exponent of highest power of 5 dividing a(4n) = 2A127428(n).” “(C.4) exponent of highest power of 5 dividing a(4n+2) = 2*A127428(n+1).” The four natural quantifiers include zero. IsSquare uses a natural square root; padicValNat values are cast to integers in the last two clauses, and b denotes A127428.

Theorem 1.4 (result).

$$(\forall N\in \mathbb{N},\mathrm{IsSquare}\left(a\left(N\right)\right)\iff \left(\neg ((4:\mathbb{N})\mid N)\right))\wedge ((\forall n\in \mathbb{N},\neg ((5:\mathbb{N})\mid a\left(2\cdot n+1\right)))\wedge ((\forall n\in \mathbb{N},(\mathrm{padicValNat}\left(5,a\left(4\cdot n\right)\right):\mathbb{Z})=2\cdot b\left(n\right))\wedge (\forall n\in \mathbb{N},(\mathrm{padicValNat}\left(5,a\left(4\cdot n+2\right)\right):\mathbb{Z})=2\cdot b\left(n+1\right))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FactorialRatio/HannaA369673.result (✓ std3). ∎

Resolves. Problems/h369673 (proved) by D5/S3/Arith/FactorialRatio/HannaA369673.result.

Source. Repository-derived.

Acknowledgement. Paul D. Hanna; N. J. A. Sloane; Reinhard Zumkeller (2024). OEIS A369673, square classification and five-adic orders, with A127428 and A112765. URL: https://oeis.org/A369673/internal.

Commentary.

All four assertions hold at every natural index. Removing the equal boundary factors gives a two-step product recurrence. At even indices its power of two determines squareness. Lifting the exponent at five and splitting factorials identify the exact five-adic orders with b.

References

• Truth anchor: D5/S3/Arith/FactorialRatio/HannaA369673.a
• Truth anchor: D5/S3/Arith/FactorialRatio/HannaA369673.b
• Truth anchor: D5/S3/Arith/FactorialRatio/HannaA369673.claim
• Truth anchor: D5/S3/Arith/FactorialRatio/HannaA369673.result