The even quadratic continued fraction family: uniform effective irrationality and a sinh growth constant

For integers A, C ≥ 1 we study the generalized continued fraction V(A,C) = 1 + Kn≥1 1/(An²+C), the even (B=0) slice of the quadratic catalogue of Zenodo 10.5281/zenodo.19491767. Main results: Irrationality with explicit bracket. V(A,C) is irrational for all A,C ≥ 1, with a two-sided approximation bracket valid for every convergent. Growth law with a closed-form constant. The convergent denominators satisfy log Q_n = 2n log n − 2n + log(2πn) + n log A + K(A,C) + o(1), where K(A,C) = log( sinh(π√(C/A)) / (π√(C/A)) ) is given by the Euler sine product and depends only on the discriminant Δ = −4AC. Irrationality measure. μ(V(A,C)) = 2 exactly, with an effective measure function (explicit threshold q₀). Effective constant on C ≤ A. An exact four-term 1/n-expansion with a rigorous, parameter-dependent remainder envelope from the Stirling-series error bounds. The contribution is uniformity in (A,C) and effectivity, not a small measure (μ=2 is the generic value). A finitary core of the irrationality argument (determinant identity, denominator growth, irrationality from the error bracket) is formally verified in Lean 4 / Mathlib, with axiom cone {propext, Classical.choice, Quot.sound} and no sorryAx; the convergence/exact-error input is supplied as an analytic hypothesis, not available in current Mathlib.