When does the dominant coefficient of a polynomial continued fraction vanish? A monotone positivity criterion (machine-checked core), an unconditional bound for a positive family, and an explicit vanishing witness

For a real polynomial b of degree d with leading coefficient β_d>0, let q_n be the continuant denominators with q_0=1, q_1=b(1), q_n=b(n)q_n-1+q_n-2. With P_n=∏_k≤nb(k) and Q_n=q_n/P_n, the scaled limit C=R_∞=lim Q_n is the dominant (connection) coefficient of the seed (1,b(1)); C≠0 iff q is not minimal. Results. (1) A ratio criterion: once b>0 on a tail and two consecutive q are positive, q_n/q_n-1>b(n)→+∞, so q is dominant and C≠0 (elementary). (2) A positivity-persistence lemma: if u_n=1/(b(n-1)b(n))>0 from some index and the scaled sequence is then positive, Q_n is nondecreasing and C≥Q_N0>0; the monotone–bounded core is verified in Lean 4 (Mathlib) with a clean axiom cone (no sorryAx). Corollary: b(n)>0 for all n≥1 forces C≥1; in particular the family b(n)=An^2+Bn+C_0, integers A,B,C_0≥1, has C≥1 unconditionally, recovering the strict positivity δ=log R_∞>0 of the companion quadratic growth-law deposit. (3) Sharpness (falsification-first): the universal claim "C≠0 for every β_d>0" is FALSE — an explicit quadratic b(n)=n^2−6.2803109563277…n+8.4205764270426… has C=0 to more than forty digits at 50-digit precision, with dominant scale ∏|b|>10^43000 at the same index (a genuine minimal seed). The vanishing is produced by the sign-varying transient (b(2),b(3)<0), not the tail; b(1)>0 does not imply C≠0. Only ≥1 zero is claimed: (α,β)↦R_∞ has genuine poles wherever b has an integer root, so a sign-change count is not a zero count; the witness sits in a verified pole-free bracket with a single monotone crossing. Epistemic status (SIARC four-class). PROVEN — the monotone/bounded-below engine and the Casoratian identity are machine-checked in Lean 4 (cones ⊆ {propext, Classical.choice, Quot.sound}, no sorryAx). STRUCTURAL — the ratio criterion and the shifted (N0>1) form of the lemma are complete elementary hand proofs, not yet formalized; the all-positive C≥1 bound is the Lean engine plus a one-line reduction. VERIFIED — the vanishing witness and the no-seed-index-leak check are mpmath at 50 digits, reported above the floor. FALSE — the universal C≠0 claim, disproved by the witness. Open: whether C=0 implies the associated generating function is entire requires a separate unique-nearest-singularity analysis (stated, not claimed); literature locators (Perron, Pincherle, Frobenius radius bound) are flagged unverified and no result depends on them.