Function weakest_crushing_rung_with_char 

pub fn weakest_crushing_rung_with_char(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    ns_budget: usize,
    primes: &[u64],
) -> ProofRung

weakest_crushing_rung with the characteristic rungs enabled — the same cascade, plus, between the parity probe and the algebraic ascent, a certified mod-p cut per prime in primes: when the CNF is a recognized one-hot encoding of a GF(p) linear system (crate::modp::recover_from_cnf, which declines rather than guesses) and the GF(p) Gaussian refutation re-checks (crate::modp::is_refutation), the instance lands on ProofRung::ModCount. This is the ladder rung the census’s router_beats_ladder audit flagged as missing: the structured router’s Route::ModP specialist finally has a certified proof system the ladder can name. With primes = &[] the cascade is exactly the legacy one.