A kernel-checked symmetric-square structure theorem for Cooper's sporadic Apéry-like operators, and the monodromy lattice of the s₇ family

Stream 1 of the Dual-Scale program: a Lean 4 formalization, kernel-checked with Lean's three standard axioms (propext, Classical.choice, Quot.sound), no sorry, no native_decide outside the golden tests. Principal results. (i) The order-3 Picard–Fuchs operator of Cooper's sporadic Apéry-like sequences is the symmetric square of an explicitly determined order-2 operator, proved uniformly in the template parameters (a,b,c,d), together with the Almkvist–van Straten criterion W ≡ 0 on the same template. (ii) 4 divides s₇(n) for n ≥ 1 by an elementary termwise argument, so s₇-partner integrality follows with no literature axiom; the s₁₀ and s₁₈ partners are non-integral by finite witness. (iii) Γ₀(N)⁺, with all its Atkin–Lehner elements, acts on U ⊕ ⟨2N⟩ by an explicit integer 3×3 representation with the weight-2 automorphy factor as a hypothesis-free polynomial identity; the swap e ↔ f is the Fricke involution on the period. (iv) The embedding witness for U ⊕ ⟨14⟩ inside U³ ⊕ E₈(−1)² and the rank-22 assembly. (v) The two singular points {−1, 1/27} of the s₇ operator are the images of the Fricke fixed points of X₀(7)⁺, the leading coefficient becoming a perfect square on the h-line. (vi) The rank-jump classes of U ⊕ ⟨14⟩ and U ⊕ ⟨20⟩ with their exact orthogonal complements — (e−f)^⊥ ≅ ⟨2⟩⊕⟨2N⟩ of index 2; the integral isometry U ⊕ ⟨14⟩ ≅ ⟨−2⟩ ⊕ [[2,1],[1,4]]; the discriminant-3 class with complement A₂ (index 3); the discriminant-4 class in U ⊕ ⟨20⟩ with complement ⟨2⟩⊕⟨2⟩ — all kernel-checked, independently re-verified by a second team of the program on the exact commits, and stated independently in a second Lean development with agreeing statements. Version 5 (2026-10-08). The version-4 text is unchanged and the Lean 4 development is identical to version 4 (no .lean file changed). A dated addendum (Section 12) records results obtained since then in companion repositories of the programme, each with its status: certified ball-arithmetic enclosures of the monodromy (unique rational below a stated denominator bound, not an exact proof); explicit Inose models at the Picard-number-20 points of the s₇ family (root lattices A₁, A₁, A₂; no fibre types assigned); the names of the two selected singular K3 surfaces (X₃ and X₄); and an exact computation of the transcendental lattice of E×E′ for a cyclic n-isogeny (U ⊕ ⟨2n⟩ for n = 7, 10). The addendum adds no kernel-checked statement and does not close the rescaling gap of the paper's conjecture. Release gates re-run on the tagged commit by a session that did not write the Lean code: build OK, 421 theorems audited with the 3 registered axioms, statement lock OK. Epistemic scope. The Lean results are Tier A and may be stated as fact. That U ⊕ ⟨14⟩ is the transcendental lattice of the s₇ family is Tier B: it rests on a numerically computed, now certified, monodromy lattice and on the Dolgachev–Doran framework, both cited. No physical observable exists anywhere in this program and nothing here supplies one.