Certified Design Regions under Parametric Plant Uncertainty with Application to Antithetic Integral Feedback

Kinetic parameters in engineered biomolecular circuits are typically known only within intervals and are not precisely tunable; controller synthesis is therefore naturally posed over sets of gains rather than at a single nominal design. We formulate robust controller tuning under parametric plant uncertainty as a universally quantified set-inversion problem: given a plant-parameter box, compute the controller gains that stabilize every plant in the box. Robust stability is decided by Hurwitz sign conditions, which are bounded over the joint gain-parameter domain using validated range enclosures, yielding machine-checkable certificates of local exponential stability of the deterministic equilibrium. Numerical experiments show that the certified region depends strongly on the range enclosure. For an antithetic integral feedback (AIF) controller acting on a two-species gene-expression cascade, a tensor-product Bernstein enclosure certifies 83.2% of the design plane at bisection tolerance epsilon=0.05 with 324 terminal boxes, whereas four baseline enclosures certify between 50.9% and 58.9% on the same paving. For a fifth-order loop, the certified fraction increases from 34.4% to 73.8%, and the certified and excluded terminal boxes confine the robustly stabilizing area to a window of about 2.1 percentage points. Finally, for a refining variant of the algorithm in which the plant box is refined alongside the design box, the undecided area satisfies |U(epsilon)|=O(epsilon) under a non-degeneracy assumption on the stability boundary.