Base series of Conjecture 3.4: $\frac{\binom{2k}{k}^2\binom{4k}{2k}}{(-12288)^k}(28k+3)=\frac{16}{\sqrt3\,\pi}$

Lean: SunConj.base3_4 in lean/Theorems/Thm_SunConj_base3_4.lean.

Proved Ramanujan-type series; Conjecture 3.4 adds harmonic-number weights to its summand.

Notation: $\binom nk$ is the binomial coefficient; $H_n=\sum_{j=1}^n 1/j$ is the $n$-th harmonic number ($H_0=0$); $G=\sum_{n\ge0}(-1)^n/(2n+1)^2$ is Catalan's constant (Prove2Me's FCP.Constants.catalanConstant); $\zeta(3)=\sum_{n\ge1}1/n^3$; $L_{-8}(2)=\sum_{n\ge1}\left(\frac{-8}{n}\right)/n^2$ with the Kronecker symbol $\left(\frac{-8}{n}\right)$ ($=1$ for $n\equiv1,3$, $=-1$ for $n\equiv5,7 \pmod 8$, $=0$ for even $n$); $L_{-3}(2)=\sum_{n\ge0}\bigl(\frac1{(3n+1)^2}-\frac1{(3n+2)^2}\bigr)$. All series are over integers $k\ge0$ and converge absolutely (geometrically); "$\sum a_k=S$" is stated in Lean as HasSum, i.e. the series is summable with sum $S$.

Status. Proved in the literature; cited as a foundation (foundations/SunConj_base3_4.md), not proved here.

Source. Z.-W. Sun, "Various conjectural series identities", arXiv:2603.29973v3 (13 April 2026), https://arxiv.org/abs/2603.29973, quoted as the known base series of Conjecture 3.4 (original reference to be confirmed by the citation check).