A cubic supercongruence tower for [xcN]((1+x)^a(1−x)^b)^N, the prime 3, and two further conjectures of Bala

For integers a, b and c ≥ 1 let A(N) = [xcN]((1+x)^a(1−x)^b)^N. We give a complete proof that A(np^r) ≡ A(npʳ⁻¹) (mod p³ʳ) for every prime p ≥ 5; this was claimed earlier in unreviewed drafts. Our main new result concerns p = 3: the tower holds modulo 3³ʳ⁻¹ for all (a, b, c), and modulo 3³ʳ whenever 3 | c, or a + b ≡ c (mod 3), or a ≡ b ≡ 0 (mod 3); in every other class we give the leading 3-adic digit of the difference explicitly. We also show, by an involution argument, that the residue classes do not tell the whole story: for even c with c = a + 2b and 3 | a (or c = 2a + b and 3 | b) the tower holds modulo 3³ʳ, although most of these triples lie outside the classes above. As corollaries we prove Bala's conjectures for OEIS A333561, A333562 and A352373, his two general conjectures on A352373 and A333715 for p ≥ 5, and his conjecture for A333565 at every prime p ≥ 3. We also prove two further conjectures of Bala: a(n) = [x^n]((1−x)/(1−x+x^2))^n (A386548) satisfies a(np^k) ≡ a(npᵏ⁻¹) (mod p²ᵏ) for p ≥ 5, with optimal exponent; and the sequence with e.g.f. 2e^x/(1+e^x+e²ˣ−e³ˣ) (A370092) is integral and, for every k > 2, eventually periodic modulo k with period dividing φ(k), which is the minimal period for k = 2^α. Theorem 1.1, the corollaries for p ≥ 5, the case p = 3 of A333565, and the theorems on A386548 and A370092 (except the minimality of the period) are formalised in Lean 4 with Mathlib. Scripts, numerical outputs and Lean 4 formalisations: https://github.com/Ahmedouyahya/bala-supercongruences