\section{Introduction}
Coverage design asks three different questions. Is a specified target covered? Which failures destroy that coverage? Which design or protection policy meets a quantitative requirement? Computing the topology of the union of footprints answers part of the first question but not the target question itself, since a contractible covered region can be disjoint from the asset that must be monitored.

We work in a finite model in which all of the geometry can be certified exactly. Physical footprints are closed disks, the target is a finite union of closed nondegenerate triangles, and failure rules are monotone with respect to additional functioning contacts. In this model one canonical geometric certificate connects exact failure budgets, common-radius design, placement uncertainty and the assignment of contacts to fault domains.

\subsection{Two certificates}
For a point $x$ of the target $T$, let $S(x)$ be the set of contacts whose footprints contain $x$. Define
\begin{equation}\label{eq:overview-antichain}
\mathcal A_T=\Min\{S(x):x\in T\},
\end{equation}
where $\Min$ removes every strict superset of another member. For the regular closed targets considered here, every member has a representative away from all disk and target boundaries, and a vertical-slice construction produces a rational representative for each member using only exact sign decisions.

The first certificate is this antichain together with its witnesses. If $\F$ is a downward-closed family of allowed failures, then
\begin{equation}\label{eq:overview-universal}
T\subseteq R_{\F}\quad\Longleftrightarrow\quad
A\notin\F\text{ for every }A\in\mathcal A_T.
\end{equation}
One geometric computation therefore answers every such failure query. The antichain is the minimal-cut family of the target-coverage reliability system in the sense of Barlow and Proschan~\cite{barlow}; its geometric origin attaches an explicit target location to each cut.

The second certificate concerns common-radius design. Fix sites and target and let all primitive disk radii equal an unknown $r$. We construct a finite set $Q_T$ of rational points, independent of the winning rule. For every monotone rule $w$ that wins on the full contact set, put
\[
\rho_w(x)=\min_{\sigma:\,w(\sigma)=1}\max_{i\in\sigma}\|x-c_i\|.
\]
Then the critical radius satisfies
\begin{equation}\label{eq:overview-radius}
(r_w^*)^2=\max_{q\in Q_T}\rho_w(q)^2\in\mathbb Q.
\end{equation}
The support set consists of target vertices, bisector--edge intersections and three-site circumcenters, $O(n^3+n^2h+h)$ points in all, and it serves all rules and all common radii at once. In dimension $d$ a maximiser on an $f$-dimensional face of the target is fixed by at most $f+1$ sites.\footnote{For the rule ``at least one contact'' this recovers the classical description of the largest empty circle centred in a polygon, whose candidate centres are Voronoi vertices, crossings of Voronoi edges with the boundary, and polygon vertices~\cite{toussaint}. For ``at least $k$ contacts'' it recovers the order-$k$ Voronoi test for $k$-coverage~\cite{leekvoronoi,soye}. The theorem below treats every monotone rule and a shared convex term in one statement.}

\subsection{Contents}
The structural part identifies the canonical antichain, proves that it is the smallest certificate answering all downward-closed failure queries, describes its behaviour under monotone label maps and relates the geometry to nerve and Dowker models. The general support theorem covers functions with a common continuous convex part and affine differences; its finite support set works for every monotone rule and every common convex term. The radius function is a lattice polynomial in the contact distances~\cite{lattice,reliability-lattice}.

The analytic part gives exact arithmetic, finite procedures, uncertainty reductions and optimisation certificates. For product uncertainty sets, robustification commutes with every monotone Boolean contact rule, so independent displacement balls reduce to disk erosion and independent polygonal displacement sets reduce to finite intersections of disks at their vertices. Protection allocation is a linear program whose optimum is certified by rational primal and dual vectors.

The worked examples derive coverage, failure budgets, wiring choices and uncertain placement in exact arithmetic. In the four-corner example, changing the domain assignment changes the coverage reliability from $81/100$ to $99/100$ at domain failure probability $1/10$, with positions, radii and contact count unchanged; the squared radius needed to survive the loss of one domain drops from $89/25$ to $68/25$.

\begin{figure}[tb]
\centering
\begin{tikzpicture}[>=Latex,b/.style={draw=blue!50!black,rounded corners,align=center,font=\scriptsize,inner sep=3pt,text width=21mm},node distance=6mm and 3mm]
\node[b] (geo) {Sites and target};
\node[b,right=of geo] (cuts) {Target antichain and witnesses};
\node[b,right=of cuts] (radius) {Support set and critical radii};
\node[b,below=of geo] (logic) {Monotone logic and topology};
\node[b,below=of cuts] (opt) {Uncertainty and duality};
\node[b,below=of radius] (eng) {Budgets and wiring};
\draw[->] (geo)--(cuts);\draw[->] (geo) to[bend left=25] (radius);
\draw[->] (cuts)--(logic);\draw[->] (cuts)--(opt);\draw[->] (radius)--(eng);\draw[->] (opt)--(eng);
\end{tikzpicture}
\caption{The two finite geometric certificates and their uses. The geometry is computed before a failure rule or a protection allocation is chosen.}
\end{figure}

\subsection{Related work}
Arrangements of algebraic curves and exact geometric predicates are standard tools in computational geometry~\cite{arrangements}. Coverage tests based on circle intersections and local geometry are due to Huang and Tseng and to Wang et al.~\cite{coverage2003,integrated}, and $k$-coverage via generalised Voronoi diagrams to So and Ye~\cite{soye}. Homological sensor criteria and multicover nerves are developed in~\cite{ghrist,desilva,controlled,sheehy,corbet,alonso}; we include the maps and proofs we need because the failure semantics and boundary conventions matter for the certificates.

Minimal cut sets and structure functions belong to reliability theory~\cite{barlow}. Cover decomposition and polychromatic hypergraph colouring are the natural setting for fault-domain assignment~\cite{polychromatic}. Max--min functions built from monotone logic are lattice polynomials~\cite{lattice,reliability-lattice}, and Boolean combinations of balls with generalised Voronoi decompositions appear in the work of Csik\'os~\cite{csikos}. The protection program uses linear programming duality, the treatment of uncertain geometry follows robust optimisation~\cite{robustbook}, and marginal-only probability bounds are instances of Hailperin's logical probability programs~\cite{hailperin}.

What is new here is the support theorem for all monotone rules with a shared convex term, the canonical antichain with rational witnesses, the exact uncertainty reductions and the radius--budget frontier, combined under one failure interface. The contact-intersection model goes back to~\cite{original}; the separation of exact predicates from continuous target certificates follows~\cite{ecog}; related topological constructions appear in~\cite{topoi,suspension,linkage}.

\subsection{Conventions}
All planar targets are finite unions of nondegenerate closed triangles with rational vertices. They are regular closed, $T=\overline{\operatorname{int}T}$, and may be disconnected or have holes. Wire targets and isolated points require a lower-dimensional treatment and are excluded from the full-dimensional sampling theorem.\footnote{Regular closed does not mean convex or simply connected. The condition ensures that failure of a closed coverage set at a boundary point of the target is witnessed arbitrarily nearby in its interior.}

Disk centres and radii are rational. Masks retain physical contact labels, including coincident footprints. Homology is over $\FF$ unless another field is specified; the target certificates do not depend on the coefficients. The appendices contain the comparison homotopies, the closed-cover chain argument, arithmetic derivations, dual certificates, worked examples and boundary counterexamples. Every statement is proved in the text.