Function project_gf4_certificate_to_gf2 

pub fn project_gf4_certificate_to_gf2(
    cert: &NsCertificateGfp,
) -> Option<NsCertificateGfp>

The GF(4) → GF(2) coefficient projection — the constructive half of the extension-field collapse. λ : a + b·ω ↦ a is the GF(2)-linear functional fixing 1; because every clause polynomial has prime-subfield (0/1) coefficients, applying λ coefficient-wise to a GF(4) certificate identity Σ_C p_C · g_C = 1 commutes with the clause factors and lands on a GF(2) certificate of no larger degree. So nothing proved over GF(4) needed the extension: NS degree depends only on the characteristic. Returns None unless the certificate is over Gf4.