const DEFAULT_NUMERIC_WITNESS_ITERATION: usize = 4;
Conservative first numeric witness when an index obligation is known to be induction-sensitive but the current summary cannot yet recover a concrete symbolic bound.