Metadata
bibkey: hanna2024a369673
authors: Paul D. Hanna; N. J. A. Sloane; Reinhard Zumkeller
year: 2024
title: "OEIS A369673, square classification and five-adic orders, with A127428 and A112765"
doi: null
url: https://oeis.org/A369673/internal
claim: "A369673 conjectures C.1-C.4 classify square values and give exact five-adic orders using the factorial valuation difference A127428."
strata_touched:
- D5/S3/Arith/FactorialRatio/HannaA369673
license: citation-only
triage: anchor
Verified locator
Source: https://oeis.org/A369673/internal
Auxiliary sources: https://oeis.org/A127428/internal and https://oeis.org/A112765/internal. The main entry is revision #21, February 8, 2024, 07:38:13, authored by Paul D. Hanna on February 6, 2024. It has no DOI or arXiv identifier and is unpaginated. A127428 is revision #21, October 3, 2026, 07:21:35; A112765 is revision #97, October 20, 2026, 11:26:17.
Source statements
OEIS A369673, NAME and COMMENTS, verbatim (unpaginated):
a(n) = Product_{k=0..n} (2^k + 2^(n-k)).
Conjectures:
(C.1) a(n) is a square iff n is not divisible by 4.
(C.2) a(2*n+1) is not divisible by 5 for n >= 0.
(C.3) exponent of highest power of 5 dividing a(4*n) = 2*A127428(n).
(C.4) exponent of highest power of 5 dividing a(4*n+2) = 2*A127428(n+1).
OEIS A127428, NAME, verbatim (unpaginated):
v_5( (10n)! ) - v_5( (5n)! ), where v_p(N) is the p-adic valuation defined in A112765.
OEIS A112765, NAME, verbatim (unpaginated):
Exponent of highest power of 5 dividing n. Or, 5-adic valuation of n.
The product includes both endpoints. The offsets of A369673 and A127428 are zero,
so the assertions include the index zero. The Lean function b takes the factorial
valuation difference in the integers. IsSquare and padicValNat are Mathlib’s
existing notions; all product and factorial arguments to the valuation are positive.
Mathematical scope
Pairing the product factors leaves, at even indices, the factorization
a(2m) = 2^(m²+1) Q(m)², where Q(m) = Product_{j=1..m}(1+4^j) is odd.
The parity of m²+1 determines the square classification. At five, the existing
lifting-the-exponent theorem evaluates the odd-exponent factors, and factorial
valuation identities identify their sum with A127428. The Lean result proves all
four universal assertions, including zero. No general-base classification,
other-prime formula or asymptotic assertion is included.
Literature completeness is ASSUMED-UNVERIFIED: the partial screen in issue #21915 includes rate-limited author and citation discovery. No claim of exhaustive novelty is made. Classical lifting and factorial valuation identities are reused results.