For the affine semiprime family n=p (2p+3) and a Lucas parameter pair (P, Q) withQ=-1, in the mixed character regime (ₚ, q) = (-1, +1), the strong-Lucaspseudoprimality of n is equivalent (Corollary 2 of the companion paper) to the2-adic rank diagonal (ₚ) = (q), where _ is the rank ofapparition. We prove that the density of this diagonal is exactly 12, moduloa single equidistribution hypothesis on the Lucas ratio zq=/among the squares of q^ --- a 2²-division-field Chebotarev input. Thereduction rests on three structural facts: the rank-valuation rule (_) = (-_) =-1 (``Lemma 1''), theaffine 2-adic alignment sq=sₚ+1, and an elementary group-counting identity --- ina finite cyclic group of order divisible by 4, the fourth powers are exactly halfthe squares. All three, and the resulting diagonal reductions, are formalized inLean~4 / Mathlib and are axiom-clean. We confirm the theorem on 2. 210⁶mixed-regime pairs (D=5, 50. 02\%, residual 0. 45) and isolate thecomplementary Q=+1 column, where the diagonal is a D-dependent rational (34 for D=5, 38 for D=21) governed by the power structure of thefundamental unit of Q (D). Finally we reduce the hypothesis itself: forD=5 it splits into a provable Chebotarev density --- the governing field Q (i), of minimal polynomial x⁸+3x⁴+1, is non-abelian (D₄) over Q, so ``z is a fourth power'' is not a congruence and is equidistributedover the family's residue class --- and a single residual independence between thatFrobenius condition and the twin-prime condition p= (q-3) /2, the only unconditional gapremaining.
John Janik (Fri,) studied this question.