A one-half density theorem for the strong-Lucas 2-adic rank diagonal in the Lucas--PSW mixed regime, modulo a single equidistribution

For the affine semiprime family $n=p(2p+3)$ and a Lucas parameter pair $(P,Q)$ with$Q=-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(₎=(-₎Q=-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.2×10⁶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: for$D=5$ it splits into a provable Chebotarev density --- the governing fieldQ(√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.