A Discrete-Wronskian Pearl: One Order-2 Casoratian Certificate, Reused at Catalan's Constant and ζ(4)

A homogeneous order-2 linear recurrence lead(n)·s(n+2) + mid(n)·s(n+1) + trail(n)·s(n) = 0 has, for any two solutions u, v, a discrete Wronskian (Casoratian) W_n = u_n vₙ₊₁ − uₙ₊₁ v_n obeying the first-order step law lead(n)·Wₙ₊₁ = trail(n)·W_n — in which the middle coefficient cancels identically. The pearl is the consequence: trail(n) ≠ 0 for all n together with W_0 ≠ 0 already force W_n ≠ 0 for all n (so (u, v) is a fundamental system at every index), with no closed form, no determinant, and no hypothesis on the leading coefficient. We give this as one field-general Lean 4 / Mathlib theorem (PROVEN, clean cone) and reuse it unchanged at two deliberately mismatched Apéry-like recurrences: W. Zudilin's equation for Catalan's constant G (irrationality open) and the Schneider–Zudilin recurrence for ζ(4) = π⁴/90 (known irrational, degree-13 coefficient polynomials). In the latter the heavy degree-13 middle polynomial is carried as an opaque atom and provably never enters the proof term. Both instances are re-derived as a single exact application of the abstraction and add zero axioms; both are fully sorry-free. We make no claim on the irrationality of G (it stays CONJECTURED); ζ(4) = π⁴/90 is cited, not reproved.