No currently checkable implication from known neighborhood theorems to NP ⊄ P/poly
Let K be the catalog of published, expert-accepted theorems in circuit complexity, proof complexity, fine-grained complexity, and independence / bounded arithmetic that are encoded (as statements, finite models, and…