Bala A347855: integrality at every natural index

Abstract

Bala A347855 integrality.

Definition 1.1 (c).

$$\forall n\in \mathbb{N},c\left(n\right)=\frac{(\mathrm{Nat}.\mathrm{factorial}\left(12\cdot n+8\right):\mathbb{Q})}{(\mathrm{Nat}.\mathrm{factorial}\left(6\cdot n+4\right):\mathbb{Q})\cdot (\mathrm{Nat}.\mathrm{factorial}\left(3\cdot n+1\right):\mathbb{Q})\cdot {\prod }_{k\in \mathrm{Finset}.\mathrm{range}\left(3\cdot n+3\right)}((3\cdot n+3\cdot k+2:\mathbb{Q}))}$$

Formalization. D5/S3/Arith/FactorialRatio/OeisA347855BalaAuxCIntegral.c (✓ std3).

Citation. Peter Bala (2021). OEIS A347854–A347858: fractional factorial ratios. URL: https://oeis.org/A347854.

Commentary.

OEIS A347855, FORMULA (unpaginated): “a(3n+2) = 3^(3n+2) * c(n), where c(n) = (12n+8)!/( (6n+4)!(3n+1)!Product_{k = 0..3n+2} (3n+3k+2) ) appears to be integral. (End)” The product includes both endpoints given by the source; Finset.range uses an exclusive upper endpoint.

Definition 1.2 (claim).

$$\mathrm{claim}=(\forall n\in \mathbb{N},\exists z\in \mathbb{Z},(z:\mathbb{Q})=c\left(n\right))$$

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

Citation. Peter Bala (2021). OEIS A347854–A347858: fractional factorial ratios. URL: https://oeis.org/A347854.

Commentary.

OEIS A347855, FORMULA (unpaginated): “a(3n+2) = 3^(3n+2) * c(n), where c(n) = (12n+8)!/( (6n+4)!(3n+1)!Product_{k = 0..3n+2} (3n+3k+2) ) appears to be integral. (End)” Integrality means that for every natural index, including zero, the value is the cast of an integer.

Theorem 1.3 (result).

$$\forall n\in \mathbb{N},\exists z\in \mathbb{Z},(z:\mathbb{Q})=c\left(n\right)$$

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

Resolves. Problems/oeis-a347855-bala-aux-c-integrality (proved) by D5/S3/Arith/FactorialRatio/OeisA347855BalaAuxCIntegral.result.

Source. Repository-derived.

Acknowledgement. Peter Bala (2021). OEIS A347854–A347858: fractional factorial ratios. URL: https://oeis.org/A347854.

Commentary.

Every natural index has an integer value. The Gamma recurrence and the divisible factorial denominator give an integer cast.

References

• Truth anchor: D5/S3/Arith/FactorialRatio/OeisA347855BalaAuxCIntegral.c
• Truth anchor: D5/S3/Arith/FactorialRatio/OeisA347855BalaAuxCIntegral.claim
• Truth anchor: D5/S3/Arith/FactorialRatio/OeisA347855BalaAuxCIntegral.result
• Dependency: D5/S3/Arith/FactorialRatio/OeisA347855BalaThirdIndexIntegral