Franel numbers at 1/8: proof of a conjecture of Z.-W. Sun and a multiplicative q-congruence

Let f_k = Σ_j C(k,j)³ be the Franel numbers (OEIS A000172) and S(N) = Σ_{k=0}^{N−1} f_k/8^k. In Remark 1.1 of "Congruences for Franel numbers" (Adv. in Appl. Math. 51, 2013), Z.-W. Sun conjectured, as part of a chain of congruences, that S(p) = Σ_{k=0}^{p−1} f_k/8^k ≡ (p/3) (mod p²) for every prime p > 3, where (p/3) is the Legendre symbol. In his list of open conjectures (2019, Conjecture 57, congruence (4.6)) he proposed a p-adic tower containing it: for every prime p > 2 and every n ≥ 1, S(pn) ≡ (p/3)·S(n) (mod p^(2+2ν_p(n))), where ν_p is the p-adic valuation. F. Beukers ("Supercongruences using modular forms", arXiv:2403.03301, Theorem 1.5) obtained the first congruence as one case of a general theorem on supercongruences explained by modular forms, but his argument uses a factorization of a certain polynomial that he states he will not prove; he also expects congruences of this Dwork type modulo p^(2r) to hold in general and reports that an attempt to prove them in one case failed. This preprint proves the first congruence for every odd prime p, and the whole tower (4.6) for every odd prime p and every n. Main results. Theorem 1.1. For every odd prime p, Σ_{k=0}^{p−1} f_k/8^k ≡ (p/3) (mod p²). Theorem 1.2. For every odd prime p and every m ≥ 1, S(mp) ≡ S(m)·S(p) (mod p²). Corollary 1.3. For every odd prime p and every m ≥ 1, S(mp) ≡ (p/3)·S(m) (mod p²); this is (4.6) for every n not divisible by p. Theorems 1.4 and 1.5 (q-analogue). For the q-analogue F_N(q) = Σ_{i+j<N} q^(i+2j) [ (q;q)_{i+j} / ((q²;q²)_i (q²;q²)_j) ]³, which satisfies F_N(1) = S(N), we prove that for every odd n and every m ≥ 1 F_{mn}(q) ≡ F_m(q^(n²)) F_n(q) (mod Φ_n(q)²), and F_n(q) ≡ (n/3) q^((n²−1)/3) (mod Φ_n(q)) when 3 does not divide n (F_n(q) ≡ 0 when 3 divides n). Theorem 1.6 (new in this version). For every prime p > 2 and every n ≥ 1, S(pn) ≡ (p/3)·S(n) (mod p^(2+2ν_p(n))), that is, Sun's congruence (4.6) holds for every odd prime p and every n. Theorem 6.1 (the case p = 3, in a stronger form). For every N ≥ 1, the polynomial T_N(x) = Σ_{k<N} f_k x^k satisfies T_N(−1+9v) = N²·P_N(v) with P_N a polynomial whose coefficients are 3-adic integers. Hence Σ_{k<N} f_k x^k ≡ 0 (mod 3^(2ν_3(N))) for every 3-adic integer x ≡ −1 (mod 9); x = 1/8 gives (4.6) for p = 3, and x = −1 gives again the case p = 3 of the tower for alternating sums. Method. The proof of Theorem 1.1 starts from Strehl's identity f_k = Σ_j C(k,j) C(j,k−j) C(2j,j). Summing over k first produces values of Legendre polynomials at 5/4, and their generating function turns S(p) into a triple sum of the numbers x_m = C(2m,m)/4^m, which can be truncated modulo p² to a square of side (p−1)/2. Since x_m is the value at a = 1/2 of the polynomial (a)_m/m!, and 1/2 = −(p−1)/2 + p/2, a first-order Taylor expansion at the negative integer −(p−1)/2 reduces everything to two binomial sums, evaluated with a partial-sum identity; the Fermat quotients that appear cancel exactly. Theorems 1.4 and 1.5 come from a "diagonal deformation" of the q-sum at a primitive n-th root of unity: the deformed sum satisfies a first-order functional equation, solved in closed form, whose constant is a quadratic Gauss sum. For p ≥ 5, Theorem 1.6 is proved with the q-analogue. A residue formula expresses P(1) modulo N², for N = p^r, through the values and first derivatives of P at the N-th roots of unity. Applied to P(q) = q^e(F_{mp^r}(q) − (p/3) q^((p²−1)/3) F_{mp^(r−1)}(q^(p²))), Theorems 1.4 and 1.5 determine all these data except one Galois trace σ_j for each level j, and these traces do not depend on m. This gives a linear relation, modulo p^(2r), between the numbers S(mp^i) with coefficients independent of m (Theorem 5.2). The values alone, through the analogous formula modulo N, give the weaker congruence S(mp^s) ≡ (p/3)·S(mp^(s−1)) (mod p^s) for all m and s (Lemma 5.9), which is (4.6) with half of the exponent. Taking m = p^r in the linear relation, the weak congruence forces the traces to be divisible by the right powers of p, and an induction on r gives the full exponent. The same argument gives a second proof of Theorem 1.1 for p ≥ 5 that uses only the q-analogue. For p = 3 this argument breaks down (no S(3^r) is a unit), and Theorem 1.6 is proved by a different method, independent of the q-analogue (Section 6). Let f̃_k be the solution of Franel's recurrence with f̃_0 = 0, f̃_1 = 1. A Christoffel–Darboux argument gives the exact identity Σ_{k<N} f_k x^k = N²·(f_N·Z_N(x) + 8 f_{N−1}·Z_{N+1}(x)), where Z_N = (f_{N−1} Σ_{k<N} f̃_k x^k − f̃_{N−1} Σ_{k<N} f_k x^k)/(−8)^(N−1); so the factor N² comes out exactly, and it remains to show that the polynomials Z_N are 3-integral near x = −1. Their expansions at the singular point x = −1 are governed by the recurrence of Zagier's sporadic sequence F (1, 6, 42, 312, …), and a variation-of-constants formula shows that Z_N(−1+9v) has 3-integral coefficients as soon as the second solution 0, 1, 10, 88, 750, 158124/25, … of that recurrence is 3-integral. An involution of Franel's differential equation, x ↦ −(1+x)/(1−8x), which exchanges the singular points 0 ↔ −1 and 1/8 ↔ ∞, identifies the generating function of this second solution with the solution Ψ of an inhomogeneous Franel equation at 0. In the modular parametrization of level 6, Ψ = f·D^(−2)(E(τ) + E(2τ)), where D = q d/dq and E is the Eisenstein series of weight 3 with coefficients Σ_{d|n} (n/d over 3)·d²; the coefficients of D^(−2)E are the sums Σ_{e|n} (e/3)/e², which have no factor 3 in their denominators. The modular identities involved are checked with Sturm's bound. Open questions. The first congruence of Sun's chain in Remark 1.1, Σ_{n<p} (−1)^n Σ_k C(n,k)³ (−8)^k ≡ Σ_{k<p} f_k/8^k (mod p²), remains open (numerically the two sums agree even modulo p³ for 5 ≤ p < 60). We conjecture that Theorem 1.5 holds modulo Φ_n(q)², which is verified at all primitive roots of unity for odd n ≤ 25. Numerically, Σ_{k<N} f_k x^k ≡ 0 (mod 3^(2ν_3(N))) even for every 3-adic integer x ≡ −1 (mod 3). Verification. Every step was checked by computer, in finite ranges: by the certificate module of SyntheticMind and by three independent Python scripts included here. verify_franel8.py (standard library only, about 20 seconds; 7451 checks, no failures) checks the classical part in exact rational arithmetic for all primes 5 ≤ p ≤ 109, Theorem 1.1 for all odd primes p < 760, and the q-congruences exactly at every primitive n-th root of unity in finite fields for all odd n ≤ 25. verify_tower_powers.py (Python with gmpy2, about 13 minutes) checks the 505 congruences S(p^k) ≡ (p/3)·S(p^(k−1)) (mod p^(2k)) with p^k ≤ 2·10^6, in exact integer arithmetic; the valuation is exactly 2k in every case. verify_p3.py (standard library only, about 15 seconds; 5481 checks, no failures) checks every identity of Section 6 in exact arithmetic: the Christoffel–Darboux identity, the operator identities, the variation-of-constants formula, the involution, the three modular identities up to q^150 (far beyond the Sturm bounds q^3 and q^6), the 3-integrality of the relevant series up to index 1500, and ν_3(S(N)) ≥ 2ν_3(N) for all N ≤ 30000. Apart from the comparison of finitely many Fourier coefficients required by Sturm's bound, the proofs do not depend on any computation. Authorship. The author of this work is Roberto Blanco Gómez. The results were obtained with SyntheticMind, the mathematical reasoning engine that the author created, designed and programmed himself. The AI system Claude (Anthropic) collaborated as an assistant, under the author's direction, in the derivation and checking of the proofs, the literature search, the verification scripts and the writing. The author has checked the arguments and takes full responsibility for the content. Files: Blanco_Gomez_2026_Franel_one_eighth_Sun_EN.pdf: the paper (version 2). Blanco_Gomez_2026_Franel_one_eighth_Sun_ES.pdf: the Spanish version, with the same content. verify_franel8.py: the first verification script (Python 3, standard library only). verify_log.txt: its output. verify_tower_powers.py: the second verification script (Python 3 with gmpy2). verify_tower_powers_log.txt: its output. verify_p3.py: the third verification script (Python 3, standard library only). verify_p3_log.txt: its output. sources_tex.zip: the LaTeX sources.