pub fn incompressible_string_exists(n: u32) -> Option<CountingCert>Expand description
The incompressibility lemma for length n, as a re-checkable counting certificate: 2ⁿ
strings (pigeons) against 2ⁿ − 1 shorter programs (holes) ⇒ an incompressible string exists.
None only when n is out of the exact-u128 range (1 ≤ n ≤ 127). Re-check with
crate::pigeonhole::check_counting_cert.