A formal-group proof of a conjecture of Z.-H. Sun for an Apéry-like sequence

Let G_n = sum_{k=0}^n 4^k binom(2n-2k,n-k)^2 binom(2k,k). This preprint proves a conjecture of Z.-H. Sun asserting a three-term congruence for G_{(mp^r-1)/2} when p is congruent to 1 modulo 4. After an integral strict change of parameter, the formal logarithm becomes the Eichler integral of the CM newform eta(4z)^6. Its Hecke recurrence and a formal-group coefficient-transfer theorem yield the congruence for every positive odd m, including p dividing m, and every r at least 2. The archive includes the manuscript, an exact power-series verification, SHA-256 manifests, an OpenPGP signature, and a DigiCert RFC 3161 timestamp response. The proof presented in this article was found by OpenAI Codex.