Function lift_prime_witness_to_zm 

pub fn lift_prime_witness_to_zm(
    m: u64,
    p: u64,
    witness_p: &[(Mono, u64)],
) -> Vec<(Mono, u64)>

Lift a prime-field pseudo-expectation to the ring: for p | m, the functional L(x) = (m/p) · L_p(x mod p) satisfies every ℤ/m constraint — (m/p)·c·v depends on c only mod p, so each pairing is (m/p) · ⟨L_p, prod mod p⟩ = 0 — and carries the zero-divisor normalization L(1) = m/p ≠ 0. One prime witness therefore certifies the ring lower bound: the composite modulus inherits the hardness of each of its prime parts (the witness face of the CRT conjunction).