A kernel-checked symmetric-square structure theorem for Cooper's sporadic Apery-like operators, and the monodromy lattice of the s7 family

Cooper's three sporadic Apéry-like sequences s7, s10, s18 satisfy order-3 recurrences belonging to a four-parameter template. We prove — uniformly in the template parameters (a,b,c,d) ∈ Q4, with the proof verified by the Lean 4 kernel — that the associated order-3 operator L3 factors as P2·Sym²(L2) for an order-2 partner operator L2 whose coefficients are determined explicitly by the template, and, independently, that the Almkvist–van Straten symmetric-square criterion W ≡ 0 holds identically on the template. The partner separates the three sporadic candidates arithmetically: only the s7 partner has an integral holomorphic solution (OEIS A279619), and we make precise the mechanism — a normalized integral uniformizer — underlying that integrality. We further prove, exactly over Q, that L2 and L3 are irreducible and that L3 is the minimal-order annihilator of its holomorphic solution. Finally, we compute the monodromy of the s7 family numerically to 60 digits, recognize the entries exactly (largest residual ≈ 10-59), and derive — by an exact integer pipeline verified by two independently written implementations — that the joint monodromy-invariant lattice is isometric over Z to U ⊕ ⟨14⟩, in exact agreement with the lattice (M7)⊥ of Dolgachev's Mn-polarized K3 framework. Epistemic status is labelled throughout The paper is explicit about which statements are kernel-checked, which are exact symbolic computation, which are numerically supported, and which are classical results cited. It also reports what the kernel did not check. Specifically: The Lean 4 development builds at toolchain v4.34.0-rc2 against mathlib4 pinned at tag v4.34.0-rc2 (commit 85e3a25e006c35636f0e53b0e9296caca2685bc0). 165 theorems audited in the Agora library; 162 depend only on Lean's three standard axioms (propext, Classical.choice, Quot.sound). The remaining 3 depend on two declared and registered axioms: a literature citation (O'Brien 2016, Thm 6.2), and one flagged DISCLOSED-VACUOUS which carries no content. Exactly one sorry remains, as a named open goal in the directory reserved for them. native_decide is confined to the golden numeric tests; results proved that way are kernel-checked modulo compiler trust, and are labelled as such rather than as plain kernel results. All computations are reproducible from the accompanying repository, which is archived alongside this record. Files: main.pdf (37 pp.), main.tex, and paper-latex-source.tar.gz containing the complete LaTeX sources (main.tex, sections/, references.bib, main.bbl) needed to rebuild the PDF with pdfLaTeX. Prepared with AI assistance; all mathematical statements are either machine-checked by the Lean 4 kernel or explicitly labelled with their weaker epistemic status.