If N=2M>0 and A>=1, (2NA+1)^N>(4N²A²+1)^M. Prove the base inequality by ring normalization and lift through positive powers.
Method: native-ring. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.