The Oliveira--Pich--Santhanam Anti-Checker Lemma

Public aggregation module for the rounded finite parameters, typed multi-output generator contract, semantic approximate-selection rounds, and the explicit conditional approximate-counter circuit and estimator interfaces. The randomized-counter layer isolates the finite union-bound and hardwiring step, and the fixed-width domain layer counts canonical binary gate-slot descriptions directly without changing the survivor count. A specialized hash-cell layer exposes the precise existential occupancy query, while the hashing bridge turns any bounded relative-counting circuit on that domain into the required deterministic counter. Constructing the adaptive query circuit and discharging its bound under NP ⊆ P/poly remain open.