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) New in this version: 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. 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.