Function max_ns_degree_at 

pub fn max_ns_degree_at(n: usize) -> usize

The degree-growth wall, measured. The deepest minimum-Nullstellensatz degree among the minimal-UNSAT families at n whose weakest certified refutation is algebraic (families caught by a cheaper lens — counting, parity — contribute nothing, correctly). This is a lean pass: only the certified proof-complexity ladder (weakest_crushing_rung) per orbit, none of the full router’s symmetry/algebraic machinery — so it reaches n=4 where the full census times out. As n grows this climbs (bounded-degree Nullstellensatz is incomplete — Tseitin/expander families force degree Ω(n)), so any fixed-degree lens is eventually outrun. That climb is the honest wall, not a fixed residue.