Function occurrences_in_term 

pub fn occurrences_in_term(body: &Term, name: &str) -> Occurrences

occurrence_count_in_term, classified — everything an occurrence-gated ζ rule needs, and strictly CHEAPER than the count, because it stops at the second occurrence.

This is the gate reduction.rs’s Term::Let arm and type_checker.rs’s Term::Let rule are missing. Both ζ-substitute UNCONDITIONALLY today, so a value bound once and used n times is written n times and checked n times — which is exactly what lean_conformance_t00_terms::a_shared_subterm_is_checked_once_and_not_once_per_occurrence measures.