Cubic supercongruences for a Dixon-type sum, fractional factorial ratios and two Apéry-like sequences

We prove several supercongruences of the form a(np^r) ≡ a(npʳ⁻¹) (mod p³ʳ), p ≥ 5, conjectured by P. Bala on the OEIS. For the Dixon-type sum a(n) = Σ_k (−1)^k C(n,k)^2 C(n−2,k) (A361711) we prove the tower for every odd n, from an exact product identity over the units below np^k/2, and show that it fails for even n. We prove that the fractional factorial ratios A364172, A364178 and A364179 are integers, which was conjectural, and, through a unit-product principle that reduces the towers for A364172–A364184 to integrality, that these and A364175 satisfy the tower. For the Apéry-like sequence A363983 we prove the tower by the method of Osburn, Sahu and Straub. For the two-index sum A376462 we prove both the tower and the shifted congruence A(np^r − 1) ≡ A(npʳ⁻¹ − 1) (mod p³ʳ); the latter extends Beukers' 1985 block induction with carry labels, carry-restricted harmonic sums and moment kernels. Along the way we repair two steps of Beukers' printed argument. The main theorems are formalised in Lean 4 with Mathlib. Scripts, numerical outputs and Lean 4 formalisations: https://github.com/Ahmedouyahya/bala-supercongruences