pub fn realized_tower_families(n: usize) -> BTreeMap<String, Vec<Vec<Lit>>>Expand description
The realization frontier at n — the lower-bound companion to family_tower. For each certified
family that actually OCCURS among the minimal-UNSAT covers over n variables, one witness cover’s
clauses. Where family_tower is the proven upper envelope (families ⊆ tower), this shows which
rungs are realized at scale n, with a witness. A tower family absent here is simply not yet realized at
this n — e.g. counting needs enough variables to host a pigeonhole, so it is empty at small n.