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) = Σₖ₌₀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) = Σₖ₌₀ᵖ⁻¹ f_k/8^k ≡ (p/3) (mod p²) for every prime p > 3, where (p/3) is the Legendre symbol. F. Beukers ("Supercongruences using modular forms", arXiv:2403.03301, Theorem 1.5) obtained this 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. This preprint gives a complete and elementary proof, valid for every odd prime p. Main results. Theorem 1.1. For every odd prime p, Σₖ₌₀ᵖ⁻¹ 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 proves congruence (4.6) of Sun's Conjecture 57 ("Open conjectures on congruences", 2019), namely n⁻²( Σk<pn f_k/8^k − (p/3) Σk<n f_k/8^k ) ≡ 0 (mod p²), 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)ᵢ₊ⱼ / ((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ₘₙ(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). 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 harmonic number H_h, h = (p−1)/2, cancels between the two pieces, leaving (−3/4)^h (1 − pT/2) with T = Σk≤h (−1/3)^k/k; evaluated in Z_(p)[√−3], T ≡ q_p(3) − 2q_p(2) (mod p), and these Fermat quotients cancel exactly against those of (−3/4)^h. 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. Its value gives Theorem 1.5, and its logarithmic derivative gives exactly the cancellation needed, after a block decomposition of q-Lucas type, for Theorem 1.4. Letting q → 1 gives Theorem 1.2. Open questions. The full tower (4.6), i.e. the congruence modulo p^(2+2ν_p(n)) when p divides n, remains open; it holds in all cases we tested. 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²), also 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. Verification. Every step was checked by computer, in finite ranges: by the certificate module of SyntheticMind and by the independent Python script included here (7451 checks, no failures; standard library only, about 20 seconds). The classical part is checked in exact rational arithmetic, step by step, for all primes 5 ≤ p ≤ 109, and Theorem 1.1 for all odd primes p < 760 (with the exponent 2 sharp for 5 ≤ p < 400); the q-congruences are checked exactly at every primitive n-th root of unity in finite fields, for all odd n ≤ 25. 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 script 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. Blanco_Gomez_2026_Franel_one_eighth_Sun_ES.pdf: the Spanish version, with the same content. verify_franel8.py: the verification script (Python 3, standard library only). verify_log.txt: its output. sources_tex.zip: the LaTeX sources.