% Options for packages loaded elsewhere \PassOptionsToPackage{unicode}{hyperref} \PassOptionsToPackage{hyphens}{url} \PassOptionsToPackage{dvipsnames,svgnames,x11names}{xcolor} \documentclass[ 11pt, ]{article} \usepackage{xcolor} \usepackage[margin=24mm]{geometry} \usepackage{amsmath,amssymb} \setcounter{secnumdepth}{-\maxdimen} % remove section numbering \usepackage{iftex} \ifPDFTeX \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{textcomp} % provide euro and other symbols \else % if luatex or xetex \usepackage{unicode-math} % this also loads fontspec \defaultfontfeatures{Scale=MatchLowercase} \defaultfontfeatures[\rmfamily]{Ligatures=TeX,Scale=1} \fi \usepackage{lmodern} \ifPDFTeX\else % xetex/luatex font selection \fi % Use upquote if available, for straight quotes in verbatim environments \IfFileExists{upquote.sty}{\usepackage{upquote}}{} \IfFileExists{microtype.sty}{% use microtype if available \usepackage[]{microtype} \UseMicrotypeSet[protrusion]{basicmath} % disable protrusion for tt fonts }{} \makeatletter \@ifundefined{KOMAClassName}{% if non-KOMA class \IfFileExists{parskip.sty}{% \usepackage{parskip} }{% else \setlength{\parindent}{0pt} \setlength{\parskip}{6pt plus 2pt minus 1pt}} }{% if KOMA class \KOMAoptions{parskip=half}} \makeatother \usepackage{longtable,booktabs,array} \newcounter{none} % for unnumbered tables \usepackage{calc} % for calculating minipage widths % Correct order of tables after \paragraph or \subparagraph \usepackage{etoolbox} \makeatletter \patchcmd\longtable{\par}{\if@noskipsec\mbox{}\fi\par}{}{} \makeatother % Allow footnotes in longtable head/foot \IfFileExists{footnotehyper.sty}{\usepackage{footnotehyper}}{\usepackage{footnote}} \makesavenoteenv{longtable} \usepackage{graphicx} \makeatletter \newsavebox\pandoc@box \newcommand*\pandocbounded[1]{% scales image to fit in text height/width \sbox\pandoc@box{#1}% \Gscale@div\@tempa{\textheight}{\dimexpr\ht\pandoc@box+\dp\pandoc@box\relax}% \Gscale@div\@tempb{\linewidth}{\wd\pandoc@box}% \ifdim\@tempb\p@<\@tempa\p@\let\@tempa\@tempb\fi% select the smaller of both \ifdim\@tempa\p@<\p@\scalebox{\@tempa}{\usebox\pandoc@box}% \else\usebox{\pandoc@box}% \fi% } % Set default figure placement to htbp \def\fps@figure{htbp} \makeatother \setlength{\emergencystretch}{3em} % prevent overfull lines \providecommand{\tightlist}{% \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}} \usepackage{bookmark} \IfFileExists{xurl.sty}{\usepackage{xurl}}{} % add URL line breaks if available \urlstyle{same} % fallback for those not using the hyperref driver hyperxmp: \makeatletter \@ifundefined{xmpquote}{\newcommand{\xmpquote}[1]{#1}}{} \makeatother \hypersetup{ colorlinks=true, linkcolor={Maroon}, filecolor={Maroon}, citecolor={Blue}, urlcolor={Blue}, pdfcreator={LaTeX via pandoc}} \author{} \date{} \usepackage{etoolbox} \AtBeginEnvironment{longtable}{\small} \setlength{\emergencystretch}{3em} \begin{document} \section{Polynomial Fault Detection Without Bounded Width: Exact Reachable Sets in Priority Controllers}\label{polynomial-fault-detection-without-bounded-width-exact-reachable-sets-in-priority-controllers} Idris Ali Shaik\\ Independent researcher (unaffiliated)\\ shaikidris@apache.org \textbf{Preprint, version 1.1, 22 October 2026.} \subsection{Abstract}\label{abstract} Circuit-width restrictions explain several polynomial cases of automatic test pattern generation. We give a different explanation for an arbitrary-size extension of the c432 priority controller, including a subfamily with linear treewidth and net cut-width in its native layout. For a specified first-stage bridge fault, we characterize exactly the reachable qualifier sets and construct a primary input realizing each one. On drive-one inputs where the first selector flag changes, the healthy set is the target singleton; the faulty sets are precisely the target-containing sets with one request bus and all nonempty sets with at least two buses. Drive zero is undetectable. This image reduces detection to comparing decoder values on sets. For supplied guarded decoders, built from zero, positive channel leaves, disjunction and conjunction of one computed child with negative channel literals, supporting paths and dual-Horn reasoning find a detecting set in \(O((n+q)G)\) time for \(n\) channels, \(q\) outputs and counted decoder size \(G\), or \(O(G)\) for formula forests. Unsatisfiable instances of the complete guarded native CNF encoding have resolution refutations with \(O(N^3)\) inferences, where \(N\) is the encoding size. Detection is P-complete, while minimum-set optimization and counting detecting sets are NP-hard and \#P-complete, respectively. A specified final-qualifier stuck-at fault makes detection NP-complete on shared guarded decoders. The exact first-stage bridge-image statements are formalized in Lean and registered as PALOMAR-2026-10-19-000010, version 1. \subsection{1. Introduction}\label{introduction} Automatic test pattern generation asks for a primary input on which a fault-free circuit and its faulty copy disagree at an observed output. The decision problem is NP-complete for general combinational circuits {[}IS75, FT82{]}. Several polynomial cases are explained by structural restrictions: fanout-free logic, Fujiwara's \(k\)-bounded circuits, and bounded-input blocks with bounded block-graph treewidth {[}Fuj90, CAB90{]}. Under bounded fan-in and fan-out assumptions, {[}PCK99{]} obtains polynomial time for logarithmic net cut-width. The question here is whether detection can remain polynomial in a natural controller family whose native circuits escape these width restrictions. We study an arbitrary-size extension of the c432 selector. The published description calls c432 a 27-channel interrupt controller: three 9-bit request buses sharing nine enable bits {[}HYH99{]}. These give \(n=9\), \(b=3\) in our notation. Hansen and Hayes used that high-level description for test generation on the fixed netlist {[}HH95{]}. We retain its selector recurrence for every channel count \(n\) and bus count \(b\). The qualifier set contains every enabled channel with a lexicographically maximal request vector. Our outputs are supplied decoders of these qualifiers, before the later channel encoder in the published model. The fault is the first-stage bridge interface extracted from the Nemesis encodings {[}FL91, Lar92{]}. It has a target channel \(t\), a disjoint nonempty set of driver channels, and a drive \(d \in \{0,1\}\). Section 3 specifies its equations and the otherwise unrestricted primary inputs. We call the fault-free copy \emph{healthy} and the specified complete gate encoding the \emph{native encoding}. The width obstruction already occurs in a one-bus, single-output subfamily with no shared internal decoder gates. Proposition 6.11 gives native layouts of size \(N\) with treewidth and net cut-width \(\Omega(N)\). For every partition into blocks with at most \(K\) input signals and block-graph treewidth \(w\), it also gives \(K(w+1)=\Omega(N)\). These instances therefore lie outside fixed \((K,w)\) and logarithmic cut-width restrictions, while their supplied-structure detection problem is solvable in linear time. Proposition 6.10 gives a separate \(K_{n,b}\) minor in the native CNF's primal and incidence graphs. These comparisons concern the specified layouts and encodings; they do not assert width lower bounds for every equivalent representation. The central contribution is an exact, size-uniform description of the fault's image, together with a primary input realizing every admissible qualifier set. It removes the need to search the physical controller when deciding which decoder values can change. For the guarded decoder syntax, this comparison is solved by supporting paths and the classical linear-time Horn algorithm {[}DG84{]}. The contribution is the image characterization and its constructive composition with those methods. The two-copy SAT encoding {[}Lar92{]}, Horn satisfiability, and the source hardness results used below are established tools. Section 10 gives the precise attribution and the limits of the priority assessment. The exact first-stage bridge-image statements have a registered Lean formalization {[}Sha26a{]}. Registered selections also cover supplied-structure detection and extensions {[}Sha26b{]}; Section 13 lists their precise scope and the other formal packages, separately from whole-statement correspondence. \subsubsection{1.1. From the image to detection and its boundaries}\label{from-the-image-to-detection-and-its-boundaries} Theorem 4.1 supplies the common interface. An eligible set is the set of channels whose qualifiers are one. The first selector flag records whether the first bus has an enabled requester in the healthy copy. Drive zero leaves the observed qualifiers unchanged. If the first flags agree, all subsequent stages and qualifiers agree as well. For drive one, whenever those flags differ, the healthy set is the target singleton \(\{t\}\). The faulty set can be any set containing \(t\) with one bus, or any nonempty set with at least two buses. The realization part of the theorem produces a primary input for each set. Corollary 4.2 therefore reduces detection to finding a reachable set on which a decoder differs from its value on \(\{t\}\). \pandocbounded{\includegraphics[keepaspectratio,alt={Dependencies of the bridge results}]{figures/dependency-figure.pdf}} \emph{Figure 1. Main dependencies. The image is the common interface; the branches require the additional ingredients named on the arrows. The native refutation branch also uses the guarded-decoder argument. The width constructions in Propositions 6.10 and 6.11 provide the structural comparison independently of the decision procedure.} A guarded decoder is an acyclic circuit built from zero, positive channel leaves, disjunction, and conjunction of one computed child with negative channel guards. For a healthy-zero output, every true evaluation has a supporting path ending at one positive channel. This reduces the search to singletons, with the forced target adjoined in the one-bus case. For a healthy-one output, making it false is a dual-Horn condition, solved by a greatest-model computation. Theorem 5.1 constructs a detecting eligible set in \(O((n+q)G)\) time; the realization step writes a primary-input test in an additional \(O(N)\). Theorem 5.6 reduces the decoder work to \(O(G)\) when internal gates are not shared. Repeated channel leaves are allowed. Thus even the linear-width subfamily above admits linear-time detection and test construction once its circuit roles are supplied. The image also makes the boundaries precise. Proposition 5.3 combines the dual-Horn embedding with monotone circuit-value P-completeness {[}Gol77; GHR95, Theorem 6.2.2{]}. It already applies to one healthy-one formula with at most two negative guards per term. Together with the polynomial upper bound, this gives P-completeness under logspace reductions. Uniform polylogarithmic parallel time with polynomially many processors would imply \(\mathrm{P}=\mathrm{NC}\), and deterministic logarithmic space would imply \(\mathrm{P}=\mathrm{L}\); no superlinear sequential lower bound follows. Separately, the graph-cover embedding transfers classical vertex-cover optimization and counting hardness and the expander-CNF representation bound {[}Kar72, PB83, BCMS15{]}. These use additional reductions on the reachable sets. The native resolution bound uses explicit gate derivations of the selector invariants and guarded comparison, rather than only the semantic equivalence. The remaining results delimit the model. Section 7 classifies the basis consisting of disjunction, conjunction of two computed children, and negative channel guarding; it also bounds the effect of limiting the number of those conjunctions. Proposition 4.5 extends the image to a specified stage-local bridge. Theorem 4.6 describes the exact pairs for a final-qualifier stuck-at fault, generalizing the fixed observation in Theorem 4.4. On this pair image guarded-DAG detection is NP-complete, whereas unshared formulas remain polynomial (Theorems 7.8 and 7.9). Appendix D gives a compatible-path algorithm parameterized by the multi-positive clauses of the opposite zero encoding. Appendix A specifies how to verify a supplied representation against a CNF; acceptance permits the guarded decision procedure. Failure to recover or verify a representation returns \texttt{OPEN} and establishes neither nonmembership nor unsatisfiability. The worst-case cost of finding the roles remains open. The table lists one theorem for each question. The bounds that decide, extend, or enumerate take the selector roles and the decoder as input. {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{} >{\raggedright\arraybackslash}p{(\linewidth - 4\tabcolsep) * \real{0.3333}} >{\raggedright\arraybackslash}p{(\linewidth - 4\tabcolsep) * \real{0.3333}} >{\raggedright\arraybackslash}p{(\linewidth - 4\tabcolsep) * \real{0.3333}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedright Question \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Result \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Statement \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot Which faulty qualifier sets occur? & Exact sets and a primary input for each & Theorem 4.1 \\ Does a detecting test exist for the first-stage bridge? & \(O((n+q)G)\); unshared formulas \(O(G)\) & Theorems 5.1, 5.6 \\ Which images extend to other specified fault interfaces? & Stage-local bridge image; exact final-qualifier stuck-at pairs & Proposition 4.5, Theorem 4.6 \\ Does final-qualifier stuck-at detection remain polynomial? & NP-complete on guarded DAGs; \(O(G^2)\) on formula forests & Theorems 7.8, 7.9 \\ Do bounded-width conditions cover the family? & Native treewidth at least \(\min(n,b)\); a linear-width subfamily with \(K(w+1)=\Omega(N)\) for every gate partition & Propositions 6.10, 6.11 \\ How hard is this polynomial decision? & P-complete under logspace reductions, for one healthy-one formula & Proposition 5.3 \\ Can a partial qualifier assignment be extended, and can the sets be enumerated? & Polynomial extension and polynomial-delay enumeration & Theorem 5.4, Corollary 5.5 \\ Can detecting eligible sets be minimized or counted, full native models counted, or all detecting inputs compactly represented? & NP-hard eligible-set minimization, \#P-complete eligible-set and native-model counting, exponential DNNF lower bound & Corollary 6.5, Theorems 6.8, 6.9 \\ Which added gates preserve a polynomial algorithm? & Each proper subset of the three operations is polynomial; all three are NP-complete; \(k\) binary conjunctions of computed children give XP, with an FPT/W{[}1{]} split by the healthy value & Theorems 7.4--7.6 \\ Do UNSAT instances of the guarded family's specified native encoding have short proofs? & An ordinary resolution refutation of \(O(N^3)\) inferences & Theorem B.1 \\ \end{longtable} } Here \(G\) counts all \(n\) channel inputs, decoder nodes, and child, guard and output incidences; \(N\) counts variables and literal occurrences in the native CNF. The formula-forest and bounded-conjunction algorithms read an indexed decoder DAG and are separate from native CNF recognition and proof export. Their indices occupy logarithmic-size machine words. The bounds count word operations and working words. Bit-level reading, the bit cost of weights, and the size of the written output are charged where the statements say so. The upper bounds and the P-completeness, NP-completeness, \#P-completeness, and representation bounds are unconditional. Reading W{[}1{]}-hardness as the absence of an FPT algorithm requires \(\mathrm{FPT} \ne \mathrm{W}[1]\). Corollary 7.7 uses the Exponential Time Hypothesis for its exponent, through the hypothesis of {[}CHKX06, Theorem 5.5{]} recorded in Section 2. No result separates P from NP. \subsubsection{1.2. Scope}\label{scope} Two companions use the qualifier sets as an application and are not required here. The reachability companion {[}Sha26B{]} studies paths that avoid channel-specific vertices and gives conditional fine-grained bounds under separately named hypotheses. The factor companion {[}Sha26C{]} studies conjunctions of guarded factors and transfers binary-CSP and graph-class bounds to that representation. The SATLIB audit {[}Sha26U{]} and the structural note {[}Sha26S{]} record benchmark and width comparisons. Neither those comparisons nor the timing panel proves the uniform theorems. On every generated decision instance in Section 9, MiniSat and Glucose were faster than the family implementation. The panel checks the implementation and records its cost. Section 2 fixes the notation used in the reductions and the proof bound. Section 3 defines the controller. Section 4 proves the reachable sets. Section 5 gives the decision procedure and its P-completeness. Sections 6 and 7 give the boundaries for optimization, counting, compilation, width, and gate basis, including the stuck-at boundary. Appendix D studies compatible paths and zero constraints. Section 8 and Appendices A and B give the CNF contract and the resolution construction. Section 9 reports the finite checks. Section 10 matches each cited theorem with the use made of it. Section 11 lists the open obligations. \subsection{2. Preliminaries}\label{preliminaries} \textbf{Circuits and CNF.} The symbol \(\oplus\) denotes XOR and multiplication denotes AND. Gates are AND, OR, and XOR with bounded fan-in, encoded by the standard complete clause blocks (Tseitin encoding). A \emph{detection formula} conjoins a healthy copy, a faulty copy, a fault-activation constraint, and the requirement that some observed output differs {[}Lar92{]}. The bridge interface is an abstract Boolean model extracted from the SATLIB/Nemesis encodings {[}FL91, Lar92{]}. Admitting both drive values is a mathematical generalization; it does not assert that a particular physical CMOS bridge has both behaviors. For signed input literals \(l_j\) and a fresh output variable \(z\), the complete gate blocks are as follows. Constants use a unit clause. {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.5000}} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.5000}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedright Gate \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Clauses \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot \(z = \bigwedge_j l_j\) & \(\neg z \lor l_j\) for each \(j\); \(z \lor \bigvee_j \neg l_j\) \\ \(z = \bigvee_j l_j\) & \(z \lor \neg l_j\) for each \(j\); \(\neg z \lor \bigvee_j l_j\) \\ \(z = x \oplus y\) & \(x \lor y \lor \neg z\); \(\neg x \lor \neg y \lor \neg z\); \(x \lor \neg y \lor z\); \(\neg x \lor y \lor z\) \\ \(z = l\) & \(\neg z \lor l\); \(z \lor \neg l\) \\ \end{longtable} } Larger conjunctions and disjunctions use acyclic bounded-fan-in trees. Complete blocks specify both directions of a gate identity; an isolated implication is insufficient for role recovery. Signed aliases can be contracted after their two-clause equality or disequality is checked. \textbf{Functional extension.} In a finite acyclic circuit with one complete defining gate per internal variable, every valuation of all free roots extends uniquely to the defined gate variables. Topological evaluation constructs the extension; induction in the same order proves uniqueness. Appending fixed-drive and observation assertions either retains that extension or excludes it. Optional activity variables and other existentially projected private auxiliaries may have multiple extensions. The native-model counting theorem uses the complete functional miter. \textbf{Compilation.} A DNNF is a negation-normal-form circuit whose AND children have disjoint variable sets. OR children need not be disjoint or deterministic. Its size here is its wire count. An OBDD tests variables in one fixed order along every path. These representations encode all satisfying assignments, rather than only a decision or one witness. \textbf{Horn and dual-Horn.} A clause is \emph{Horn} if it has at most one positive literal and \emph{dual-Horn} if it has at most one negative literal. A formula is \emph{renamable Horn} if consistently complementing some variables makes every clause Horn. A \emph{2-CNF} has at most two literals per clause, including unit and empty clauses. A satisfiable dual-Horn formula has a unique greatest model, which is computable in linear time by downward propagation from the all-true assignment {[}DG84{]}. \textbf{Width parameters.} \begin{itemize} \tightlist \item \emph{Treewidth} and \emph{pathwidth} are taken on the primal graph of a formula or the undirected producer-consumer graph of a circuit. The latter has vertices for gates, primary inputs and primary outputs, with an edge for each signal connection; signs do not affect adjacency. \item \emph{Cut-width} is defined on a circuit hypergraph whose vertices are gates, primary inputs and outputs, and whose hyperedges are signal nets. Under a linear vertex order it is the maximum number of nets crossing a cut {[}PCK99{]}. \item The \emph{two-section graph} of a hypergraph has the same vertices and joins exactly those pairs of distinct vertices that share a hyperedge. \item For a linear vertex order, its \emph{vertex separation} is the maximum number of vertices to the left of a cut that have a neighbor to the right. The vertex separation of a graph is the minimum over all such orders; it equals pathwidth {[}Kin92{]}. \item We distinguish blocks with at most \(K\) inputs and a block graph of treewidth at most \(w\) {[}CAB90{]} from Fujiwara's \(K\)-bounded circuits, which also restrict reconvergent paths in the block DAG {[}Fuj90, PCK99{]}. The quantitative block obstruction below applies to each fixed \((K,w)\). For a partition of the gates, the block graph joins distinct blocks whenever a gate in one supplies a signal to a gate in the other. A block input is a distinct signal entering from outside the block, including a primary-input signal; repeated uses of that signal count once. If a block-graph convention also joins consumers sharing an external signal, the resulting graph contains this producer-consumer block graph. Adding such edges cannot decrease treewidth, so Proposition 6.11 applies to that convention as well. \end{itemize} \textbf{Resolution.} Refutations are DAG-like with no extension variables. A clause passes the \emph{reverse unit propagation} (RUP) test when adding units that falsify all its literals to the current clauses yields a unit-propagation contradiction. For a non-tautological requested clause, reversing this propagation conflict gives an ordinary-resolution derivation of a subclause of that clause. Stronger subclauses are retained. Tautological goals are omitted; weakening is not used to force an exact requested clause. \textbf{Parameterized bounds.} FPT means a running time \(f(k)G^c\) for a computable function \(f\) and a constant \(c\) independent of \(k\); XP allows the exponent to depend on \(k\). Parameterized Clique is W{[}1{]}-complete. The Exponential Time Hypothesis (ETH) asserts that 3-SAT on \(v\) variables has no \(2^{o(v)}\)-time algorithm, apart from a polynomial input-length factor. Chen, Huang, Kanj and Xia {[}CHKX06, Theorem 5.5{]} exclude \(f(r)m^{o(r)}\) time for Clique, for any computable \(f\), unless every SNP problem is solvable in subexponential time; \(m\) is the input length. ETH implies the required non-collapse assumption. Since a graph on \(p\) vertices has polynomial encoding length, this supplies the \(f(r)p^{o(r)}\) exclusion under ETH. \begin{center}\rule{0.5\linewidth}{0.5pt}\end{center} \subsection{3. The controller family}\label{the-controller-family} The model follows the high-level c432 description {[}HYH99{]}. Channel \(i\), with \(1 \le i \le n\), has an enable \(e_i\) and requests \(r_{ij}\) on buses \(1 \le j \le b\), where \(n,b \ge 1\). All of these are independent primary inputs, with no additional restrictions. Write \(x_i = e_i r_{i1}\) and \(P_1 = \bigvee_i x_i\). \textbf{Selector stages.} The flags and masks of one copy are \[ \begin{aligned} q_{i1}&=P_1\oplus\neg x_i,\\ t_{ij}&=e_i r_{ij}\land\bigwedge_{k{\raggedleft\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.0700}} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.9300}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedleft Line \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Operation \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot 1 & If \(d=0\), return UNSAT. \\ 2 & Set \(c_k\gets F_k(\mathbf{1}_{\{t\}})\) for every \(k\). \\ 3 & For each channel \(i\ne t\), unless every \(c_k=1\): \\ 4 & \(\quad K\gets\{i\}\) if \(b\ge2\), and \(K\gets\{i,t\}\) if \(b=1\). \\ 5 & \(\quad\)If some \(k\) has \(c_k=0\) and \(F_k(\mathbf{1}_K)=1\): \\ 6 & \(\qquad\)Return SAT\((K)\). \\ 7 & For each \(k\) with \(c_k=1\): \\ 8 & \(\quad\)Form the dual-Horn system \(Z_k\) with the following clauses. \\ 9 & \(\quad\neg a_u\lor a_v\), for each child \(u\) of an OR node \(v\). \\ 10 & \(\quad\neg a_u\lor\bigvee_{j\in B}h_j\lor a_v\), for a guard node \(v\) with child \(u\) and guards \(B\). \\ 11 & \(\quad\neg a_{\mathrm{root}}\), \(\bigvee_i h_i\), and \(h_t\) when \(b=1\). \\ 12 & \(\quad\)At leaves use \(a_v=h_i\); at a constant-zero node use \(\neg a_v\). \\ 13 & \(\quad M\gets\operatorname{GREATEST\_MODEL}(Z_k)\), by linear-time downward propagation. \\ 14 & \(\quad\)If \(M\) exists, return SAT\((\{i:M(h_i)=1\})\). \\ 15 & Return UNSAT. \\ \end{longtable} } The returned eligible set \(K\) is realized as a primary-input test by Theorem 4.1. This subsequent step writes \(nb+n\) primary values; lifting them to a full native-CNF model takes a topological pass. Theorem 5.1 charges the additional output cost separately from the decoder kernel. \textbf{Theorem 5.1.} Algorithm 1 correctly decides detection and constructs a detecting eligible set in \(O((n+q)G)\) time and \(O(G)\) working space, where \(G\) counts decoder nodes, child, guard and output incidences, and all \(n\) channel inputs. Writing the primary test input or a full native-CNF model takes total time \(O(N+(n+q)G)\) and space \(O(N+G)\), where \(N\) is the native encoded size. \emph{Proof.} By Corollary 4.2 it suffices to decide, for each bit \(k\), whether some reachable \(K\) has \(F_k(K) \ne c_k\). \emph{Bits with \(c_k = 0\).} If \(F_k(K) = 1\), follow a true child at every OR and the live child through every guard. The path ends at a leaf \(h_i\) whose guards all lie outside \(K\). The terminal cannot be the target: otherwise the same path would already make the healthy target singleton true. Then the set \(\{i\}\), or \(\{i, t\}\) when \(b = 1\), is reachable and keeps the path true. Lines 3--6 test exactly these at most \(n\) sets, and each evaluation serves all bits at once. \emph{Bits with \(c_k = 1\).} Projected to \(h\), the models of \(Z_k\) are exactly the reachable \(h\) with \(F_k(h) = 0\): \begin{itemize} \tightlist \item Given such an \(h\), setting every \(a_v\) to the node's value satisfies \(Z_k\). \item Conversely, if evaluation makes a node true, its activity variable is forced true by induction. A true root contradicts \(\neg a_{\mathrm{root}}\). \end{itemize} Each clause of \(Z_k\) has at most one negative literal, so \(Z_k\) is dual-Horn. The greatest model therefore exists exactly when \(Z_k\) is satisfiable, and it is computed in time linear in \(G\) {[}DG84{]}. \emph{Cost.} At most \(n\) evaluations of the graph, plus at most \(q\) fixed points. Reuse their working arrays. Realization writes \(nb+n\) primary values; a topological pass lifts these to all native gate variables in \(O(N)\) time. \ensuremath{\square} \textbf{Proposition 5.2 (dual-Horn transfer).} For any dual-Horn CNF \(H\) on \(x_1,\ldots ,x_m\), including unit and empty clauses, a one-bus controller with channels \(t,s,1,\ldots ,m\), driver \(\{s\}\), and guarded decoder of size \(O(m+\lvert H\rvert)\) has detecting eligible sets exactly \(\{t,s\} \cup \{i:x_i=1\}\) for \(x\) satisfying \(H\). Here \(\lvert H\rvert\) includes clause and literal counts. \emph{Proof.} For \(C = \neg x_i \lor \bigvee_{j \in A} x_j\), use the violation term \(V_C = h_i \land \bigwedge_{j \in A} \neg h_j\). For a positive clause use \(V_C = h_t \land \bigwedge_{j \in A} \neg h_j\). Set \[ F_H=(h_t\land\neg h_s)\lor\bigvee_{C\in H}V_C. \] The healthy value is one. Every reachable faulty set has \(h_t=1\), on which \(F_H=0\) is exactly \(h_s=1 \land H\). An empty positive clause contributes \(h_t\), making detection impossible. Theorem 4.1 realizes every permitted set, giving the claimed bijection. \ensuremath{\square} For each healthy-one output, the greatest model in Algorithm 1 projects to the inclusion-wise greatest detecting set for that output. Such a greatest set exists because these detecting sets are closed under union: if \(F(A)=F(B)=0\) but \(F(A\cup B)=1\), a true path on \(A\cup B\) has its head in \(A\) or \(B\) and no guard in \(A\cup B\), so it is already true on the set containing its head. The greatest set maximizes every nonnegative linear weight on those sets. Minimum cardinality is a different task, as the graph construction below shows. The sparse implementation in Theorem 5.6 may return a smaller witness when an unused channel suffices; its contract is to find a witness, not the greatest one. \textbf{Proposition 5.3 (P-completeness).} Detection on supplied guarded representations is P-complete under deterministic logspace many-one reductions, even for one bus, one driver and one healthy-one output that is a guarded-term formula with at most two negative guards per term. Here internal gates have fanout at most one; channel variables may occur more than once. \emph{Proof.} Membership follows from Theorem 5.1. Reduce the monotone circuit value problem {[}Gol77; GHR95, Theorem 6.2.2{]}. Give each circuit input and gate a variable and fix the input variables by units. For \(z=x \land y\), impose \(\neg z \lor x\) and \(\neg z \lor y\); for \(z=x \lor y\), impose \(\neg z \lor x \lor y\). Finally require the output to be one. These clauses are dual-Horn. Every model is componentwise at most the actual circuit evaluation, by topological induction; the actual evaluation itself satisfies the gate constraints. Thus this system is satisfiable exactly when the given circuit outputs one. Apply Proposition 5.2. Each violation term has at most two negative guards. Use private internal gates for each term and an OR tree; repeated channel leaves are permitted in a formula forest. Both transformations have linear output size and can be emitted using logarithmic counters and input scans. This proves logspace hardness. \ensuremath{\square} This transfers classical P-completeness through the guarded representation. A uniform parallel algorithm with polylogarithmic time and polynomially many processors would imply \(\mathrm{P}=\mathrm{NC}\); a deterministic logarithmic-space algorithm would imply \(\mathrm{P}=\mathrm{L}\). The result excludes neither all parallel speedups nor arbitrary sublinear working space. It gives no superlinear sequential-time lower bound: a single healthy-one output takes one linear-time dual-Horn pass. \textbf{Theorem 5.4 (extension of eligibility assignments).} For a drive-one controller with supplied guarded outputs, deciding whether an arbitrary partial assignment \(\alpha\) to eligibility coordinates extends to a detecting eligible set, and constructing one, takes \(O((n+q)G)\) time and \(O(G)\) working words. Healthy output values are still evaluated at \(\{t\}\). \emph{Proof.} For one bus impose \(h_t=1\), rejecting \(\alpha\) if it fixes \(h_t=0\). Let \(T\) be the fixed-true channels. A true path of any healthy-zero output under an extension ends at a positive head \(p\). Keeping \(T\) and that head, and clearing the other free channels, preserves the path. Thus evaluate \(T\) and \(T \cup \{p\}\) for every unfixed head; each pass serves all healthy-zero outputs. A true guarded output guarantees nonemptiness, since the grammar evaluates to zero when all channels are false. For a healthy-one output, append both positive and negative fixed units to its dual-Horn zero system, retaining the reachable-image constraints. Units of either sign are dual-Horn. The greatest model exists exactly when a reachable zero extends \(\alpha\). At most \(n+1\) graph evaluations and \(q\) fixed points give the bound, reusing working arrays. \ensuremath{\square} This theorem constrains eligibility coordinates, not arbitrary physical enable or request assignments. Native input lifting adds \(O(N)\). \textbf{Corollary 5.5 (polynomial-delay enumeration).} All distinct detecting eligible sets can be enumerated without repetition with delay \(O(n(n+q)G)\) and \(O(G)\) working words, including initial search and termination. Emitting a canonical primary input or native model adds \(O(N)\) time and output storage per result. \emph{Proof.} Traverse the binary prefix tree of eligibility assignments in lexicographic order and prune a prefix exactly when Theorem 5.4 rejects it. Every nonempty surviving subtree contains a result. Between successive results, at most \(O(n)\) prefixes and rejected siblings are inspected. Store one mutable prefix and a linear stack. Results are streamed; the bound excludes storage of a retained output list. This enumerates eligible sets and their canonical realizations, not all native-CNF models. \ensuremath{\square} \textbf{Theorem 5.6 (formula forests).} If the guarded outputs form a formula forest with no shared internal nodes, detection and an eligible-set witness take \(O(G)\) time and working space. Channel leaves may repeat. Native model construction adds \(O(N)\) time and space. \emph{Proof.} Evaluate the target singleton once. At a healthy-zero root, a depth-first traversal keeps a counter for every guard on the current root-to-leaf path. A leaf \(h_i\) supplies a witness exactly when \(i\) is not blocked, and, for one bus, \(t\) is not blocked. Increment and decrement the counters on entering and leaving each guard. Each incidence is visited a constant number of times; the witness is \(\{i\}\) or \(\{i,t\}\). At a healthy-one root, build the dual-Horn system on its own cone. For one bus, the target unit already ensures nonemptiness. For at least two buses, mark the channel indices occurring as leaves or guards. Every expression in the guarded grammar is zero when all its channel inputs are zero, by structural induction. If a channel is unmarked, its singleton therefore makes this entire formula zero. The first unmarked index is found after scanning at most one more index than the number marked. Otherwise all \(n\) indices occur in the cone, so the global nonemptiness clause costs at most the cone size. Use sparse maps or a single timestamp array to avoid \(n\) initialization steps per output. Since internal cones are disjoint and repeated leaves are counted as incidences, the total fixed-point work is \(O(G)\). \ensuremath{\square} \subsection{6. Witnesses, representations and width}\label{witnesses-representations-and-width} Section 5 decides whether any detecting qualifier set exists. This section keeps that decision procedure and changes the question. Minimum cardinality, counting, and a compact representation of every detecting input can be hard for the same decoders. The width bounds exhibit tractable instances of unbounded treewidth and cut-width, so the fixed-width conditions cited in Section 1 do not cover the whole family. Section 7 uses the same sets for a different extension, the gate basis. \subsubsection{6.1. Why explicit syntax matters}\label{why-explicit-syntax-matters} \textbf{Example 6.1 (why a simultaneous set is needed).} Take the cycle decoder \(F = \bigvee_i (h_i \land \neg h_{i+1 \bmod n})\). Every proper nonempty set gives output 1. The only nonempty zero set is all \(n\) channels. The fixed point finds it in one linear pass. Tests restricted to sets of cardinality below \(n\) cannot detect this fault. Since every proper nonempty set gives the same output as the healthy set, adding channels one at a time changes the output only at the last step. \textbf{Proposition 6.2 (exponentially many critical sets).} For every \(K \in R_{n,b,t}\) with \(K \ne \{t\}\) there is an \(O(n)\)-node guarded decoder \(F_K\) whose detecting inputs produce faulty eligible set exactly \(K\). Take a cyclic successor map \(s\) on \(K\) and set \[ F_K(h)=\bigvee_{i\in K}(h_i\land\neg h_{s(i)})\lor\bigvee_{j\notin K}h_j. \] For a singleton \(K\), omit its identically false cycle term. Consequently, a list of test inputs that must work for every such decoder without reading it needs at least \(2^{n-1} - 1\) entries (\(b = 1\)) or \(2^n - 2\) entries (\(b \ge 2\)). Algorithm 1 reads the decoder and recovers \(K\) in \(O(n)\). \emph{Proof.} The unconditional terms exclude every channel outside \(K\). Inside \(K\), a zero cycle term requires each selected channel's successor to be selected, and the only nonempty successor-closed subset is \(K\). Each test input produces a single eligible set, so it detects at most one \(F_K\). \ensuremath{\square} \textbf{Corollary 6.3 (adaptive query bound).} Suppose a decoder is accessible only through queries of its value on eligible sets. On the promise class consisting of the decoders \(F_K\) of Proposition 6.2 and the undetectable decoder \(F_{\bot} = \bigvee_i h_i\), deterministic detection needs at least \(M\) queries in the worst case, where \(M=2^{n-1}-1\) for one bus and \(M=2^n-2\) otherwise. Randomized detection with error at most \(1/3\) on every input needs \(\Omega(M)\) queries in the worst case. \emph{Proof.} Over nonempty sets, \(F_K\) differs from \(F_{\bot}\) only at \(K\). All these decoders are zero on the empty set. On the answer transcript for \(F_{\bot}\), an unqueried \(K\) remains indistinguishable, proving the deterministic bound even for adaptive queries. Put probability \(1/2\) on \(F_{\bot}\) and distribute the rest uniformly over the \(M\) critical decoders. Every deterministic decision tree making at most \(r\) queries has success probability at most \(1/2+r/(2M)\): until it queries the hidden \(K\), it sees the \(F_{\bot}\) transcript. Averaging over random coins gives \(r \ge M/3\) for error at most \(1/3\). This access model excludes inspection of the syntax. \ensuremath{\square} \subsubsection{6.2. Optimization, counting and compilation}\label{optimization-counting-and-compilation} \textbf{Proposition 6.4 (graph-cover representation).} Let \(J=(V,E)\) be a finite simple graph with at least one edge. Take one bus, channels \(V \cup \{t\}\), any vertex as the single driver, and the guarded decoder \[ F_J=\bigvee_{uv\in E}(h_t\land\neg h_u\land\neg h_v). \] The detecting eligible sets are exactly \(\{t\} \cup C\) for vertex covers \(C\) of \(J\). The construction has size \(O(\lvert V\rvert+\lvert E\rvert)\). \emph{Proof.} The healthy value is one. On reachable sets \(h_t=1\), and \(F_J=0\) is precisely \(\bigwedge_{uv \in E}(h_u \lor h_v)\). Theorem 4.1 realizes every such set. Each term has one live child and two negative guards, so it belongs to the original grammar. Give each edge term its own two-guard chain and combine the terms with a private OR tree. No internal decoder node is shared; repeated channel leaves are permitted. This gives a formula-forest decoder of the same asymptotic size. \ensuremath{\square} Figure 3 illustrates Proposition 6.4 on a triangle. Each uncovered edge contributes a true guarded term; covering every edge makes the output zero. \pandocbounded{\includegraphics[keepaspectratio,alt={Triangle graph-cover decoder evaluated on three eligible sets}]{figures/graph-cover-transition.pdf}} \emph{Figure 3. One bus, target \(t\), driver \(a\), and triangle graph \(J\). The healthy output is one. For \(K=\{t\}\), \(\{t,a\}\), and \(\{t,a,b\}\), the faulty outputs are respectively one, one, and zero. Dashed edges are uncovered and contribute true terms; solid edges are covered. Detection occurs precisely when \(K=\{t\} \cup C\) for a vertex cover \(C\). The arrows compare chosen evaluations, not an algorithmic search order. Choosing every graph vertex gives a detecting set; finding a smallest one is a separate task.} \textbf{Corollary 6.5 (minimum witnesses and counting).} Within the guarded class, already with one bus, one driver and one output, deciding whether there is a detecting set of size at most a supplied bound is NP-complete. Counting distinct detecting eligible sets is \#P-complete under polynomial-time Turing reductions. \emph{Proof.} Proposition 6.4 gives the exact minimum \(1+\tau(J)\), so a vertex-cover bound \(k\) becomes \(k+1\). The same construction is a bijection for counting. Cardinality-bounded vertex cover is NP-complete {[}Kar72{]}, and counting vertex covers is \#P-complete {[}PB83{]}, even for bipartite graphs in the latter case. Membership follows by guessing a set and checking reachability and decoder evaluation. The imported counting hardness uses counting reductions; the transfer from a particular graph to its controller preserves the count. \ensuremath{\square} This counts eligible sets, equivalently their canonical inputs in Theorem 4.1. It does not count all native-CNF models. In the activated one-bus cofactor, a cover \(C\) has \(2^{\lvert V\rvert-\lvert C\rvert}\) primary realizations because a disabled non-target channel's request is free. The complete native gate values are uniquely determined by the primary input and fault interface. \textbf{Proposition 6.6 (maximum witnesses and healthy-zero counting).} For one bus, one driver and one healthy-zero guarded output, the threshold problem of finding a detecting eligible set of size at least a supplied bound is NP-complete. Counting such eligible sets is \#P-complete under polynomial-time Turing reductions, even with one distinct positive head. \emph{Proof.} For a graph \(J=(V,E)\), use channels \(V \cup \{t,s\}\), target \(t\) and driver \(\{s\}\). Start at \(f_0=h_s\). For each edge \(e_j=\{u,v\}\), append \[ f_j=(f_{j-1}\wedge\neg h_u)\vee(f_{j-1}\wedge\neg h_v). \] Store \(f_{j-1}\) once. Each new AND has only one live child, and the total size is \(O(\lvert V\rvert+\lvert E\rvert)\). The resulting output is \(h_s \land \bigwedge_{uv \in E}(\neg h_u \lor \neg h_v)\), with healthy value zero. Detecting eligible sets are exactly \(\{t,s\} \cup I\) for independent sets \(I\) of \(J\). Thus the maximum is \(2+\alpha(J)\). Complementation transfers the vertex-cover decision and counting hardness used in Corollary 6.5; membership follows by checking a proposed eligible set. \ensuremath{\square} For a single output the cardinality classification is therefore: {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{} >{\raggedright\arraybackslash}p{(\linewidth - 4\tabcolsep) * \real{0.3333}} >{\raggedright\arraybackslash}p{(\linewidth - 4\tabcolsep) * \real{0.3333}} >{\raggedright\arraybackslash}p{(\linewidth - 4\tabcolsep) * \real{0.3333}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedright Healthy value \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Minimum detecting-set cardinality \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Maximum detecting-set cardinality \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot 0 & Exactly 2 for one bus, 1 for at least two buses, when detectable & NP-complete threshold problem \\ 1 & NP-complete threshold problem & Polynomial: greatest zero model \\ \end{longtable} } For a detectable healthy-zero output, a true path remains true on its positive head, together with the target for one bus. This proves the upper bounds in the table. Nonemptiness gives the multi-bus lower bound; the only reachable one-bus singleton is the healthy target singleton, which does not detect. The minimum is undefined for an undetectable output. Cardinality here counts eligible channels, not primary-input Hamming weight. Counting detecting eligible sets is \#P-complete for either healthy value. The polynomial directions also optimize nonnegative channel weights: shrinking to a positive support cannot increase weight, and the greatest zero set maximizes it. \textbf{Corollary 6.7 (maximum weight for formula forests).} For supplied healthy-zero formula-forest outputs, a maximum nonnegative-weight detecting set can be found with \(O(G)\) arithmetic operations and \(O(G)\) working words, apart from the encoded-weight and output costs. \emph{Proof.} Traverse each leaf-occurrence path with a counter per blocked channel, maintaining the weight of their union. A path ending at \(h_i\) is feasible if it blocks neither \(i\) nor the forced target, when present. Its best set contains every unblocked channel and has weight \(W_{\mathrm{total}}-W_{\mathrm{blocked}}\). Each guard incidence is entered and left once; weight changes occur only on counter transitions to or from zero. Record the best leaf occurrence, then reconstruct its path once, avoiding a copy of the whole blocked set at every improvement. \ensuremath{\square} \textbf{Theorem 6.8 (full native-model counting).} Counting satisfying assignments of the complete native guarded bridge CNF is \#P-complete under polynomial-time Turing reductions, already on the one-bus, one-output graph-cover subfamily, without extra primary restrictions. \emph{Proof.} Let \(m=\lvert V\rvert\) and assume \(J\) has an edge. Use the drive-one construction of Proposition 6.4. For a vertex cover \(C\) and an arbitrary bit vector \(\rho\) indexed by \(V\smallsetminus C\), set \[ e_t=r_{t1}=1,\qquad (e_v,r_{v1})=\begin{cases}(1,0),&v\in C,\\(0,\rho_v),&v\notin C.\end{cases} \] These inputs satisfy the drive interface and make \(P_1=1,P'_1=0\). The healthy eligible set is \(\{t\}\) and the faulty set is \(\{t\} \cup C\), so the graph-cover output differs. Conversely, every detecting input has different first flags, since equal first flags propagate equal outputs through the identical tails. The drive interface then forces the target enable and request to one and every non-target product \(e_v r_{v1}\) to zero. Its enabled non-target set must be a cover, and its request values have exactly the displayed form. Thus \((C,\rho)\) is in bijection with detecting primary inputs. Complete native gate definitions give each such input a unique extension to all internal variables (Section 2). Therefore the full count is \[ \#\operatorname{Mod}(\Phi_J) =\sum_{C\text{ cover}}2^{m-|C|} =\sum_{I\text{ independent}}2^{|I|}=P_J(2), \quad P_J(z)=\sum_{I\text{ independent}}z^{|I|}. \] Replace each vertex by \(r\) independent clones and each edge by all edges between its two clone groups, obtaining \(J^{[r]}\). An independent set of \(J^{[r]}\) is an independent set \(I\) of \(J\) together with a nonempty set of clones for each vertex of \(I\). A nonempty occupied group has total weight \(\sum_{\varnothing\ne A\subseteq[r]}2^{\lvert A\rvert}=3^r-1\), so \(P_{J^{[r]}}(2)=P_J(3^r-1)\). Native counting queries for \(r=1,\ldots ,m+1\) give distinct evaluations of the degree-at-most-\(m\) polynomial. Exact interpolation recovers \(P_J(1)\), the number of independent sets and covers. Edgeless source graphs are counted directly. Query graphs have \(O(m^2)\) vertices and \(O(m^2 \lvert E\rvert)\) edges, and values and rational interpolation intermediates have polynomial bit length. Membership in \#P follows by guessing a complete CNF assignment and checking its clauses. \ensuremath{\square} Eligible-set counts and native-model counts differ; this reduction proves hardness despite their different multiplicities. It is a Turing reduction, not a claim of a parsimonious native-model correspondence. \textbf{Theorem 6.9 (DNNF and OBDD size).} There is an infinite one-bus, one-output subfamily of the guarded native encoding with \(N=\Theta(n)\) and formula-forest decoders, each term having one positive head and at most two negative guards, for which the primary detection function and the full native CNF each require DNNF size \(2^{\Omega(N)}\). Repeated channel leaves are allowed. Every variable order also requires exponentially many OBDD nodes. \emph{Proof.} Use the bounded-degree vertex-expander graphs of {[}BCMS15, Theorems 4--5{]}. Their graph CNFs \(C_J(x)=\bigwedge_{uv \in E}(x_u \lor x_v)\) require \(2^{\Omega(\lvert V\rvert)}\) DNNF size. In the controller of Proposition 6.4 fix \[ e_t=r_{t1}=1,\qquad r_{v1}=0\quad(v\in V). \] and leave \(e_v\) free. These settings satisfy the drive-one interface and give \(P_1=1\), \(P'_1=0\), healthy set \(\{t\}\), and faulty set \(\{t\} \cup \{v:e_v=1\}\). The detection cofactor is exactly \(C_J(e)\). Conditioning cannot enlarge a DNNF. For the full native CNF, condition in the same way and existentially forget gate and observation variables. Forgetting preserves decomposability and does not increase size: it distributes over OR, and over AND because the children's variable sets are disjoint. The result again represents \(C_J\). This proves both lower bounds. An OBDD has a linear-size translation to DNNF, so the OBDD bound follows for every order. Use the private term chains and OR tree of Proposition 6.4. Bounded degree preserves linear size, and the same conditioning and projection apply. The one-bus circuit and complete bounded-fan-in encoding have size \(\Theta(\lvert V\rvert)=\Theta(n)\). The forest restriction applies to the decoder, not to the complete physical circuit or its CNF interaction graph. \ensuremath{\square} DNNF size counts wires; for bounded fan-in this agrees with gate count up to constant factors. The exponent uses the combinatorial encoded size \(N\), not file bytes. Dense binary identifiers give bit length \(L=\Theta(N \log N)\), and hence the corresponding bound is \(2^{\Omega(L/\log L)}\). The expander lower bound is imported; the physical restriction and exact projection above transfer it to this family. \subsubsection{6.3. Circuit width and syntactic backdoors}\label{circuit-width-and-syntactic-backdoors} \textbf{Proposition 6.10 (treewidth).} The primal and incidence graphs of the native encoding contain a \(K_{n,b}\) minor, so their treewidth is at least \(\min(n, b)\). \emph{Proof.} Work inside one copy of the uncontracted native layout. Write \(g_{ij}=\neg P_j \lor r_{ij}\). For channel \(i\), take the outputs of its private qualifier-AND tree together with all its factor variables \(g_{ij}\) as a branch set \(C_i\); the tree edges make this set connected. Take \(D_j=\{P_j\}\) for each bus. These sets are pairwise disjoint. The complete OR block for \(g_{ij}\) contains \(g_{ij} \lor P_j\), so the primal graph has an edge from \(C_i\) to \(D_j\) for every pair \((i,j)\). In the incidence graph, connect each qualifier-tree output to its non-primary child through the private binary clause of that AND gate. Assign these clause vertices to \(C_i\). Also assign the distinct clause vertex for \(g_{ij} \lor P_j\) to \(C_i\); it joins \(g_{ij}\) to the bus branch \(D_j\). Thus the incidence branch sets are disjoint and connected and have every required cross-edge. Explicit inverter wires, if present instead of signed inputs, and their connecting definition clauses can be absorbed into the corresponding bus branch. Contracting the branch sets gives \(K_{n,b}\) in both graphs. The treewidth lower bound follows. This argument uses the complete native layout before simplification or elimination of native variables. \ensuremath{\square} \textbf{Proposition 6.11 (linear width obstruction).} The subfamily in Theorem 6.9 has an explicit native gate layout with treewidth and net cut-width \(\Omega(N)\). For every partition of its gates into blocks having at most \(K\) input signals, if the undirected block graph has treewidth \(w\), then \(K(w+1)=\Omega(N)\). \emph{Proof.} Orient the edges arbitrarily. For every oriented edge \(v\to u\), create private gates \(a_{vu}=h_t \land \neg h_v\) and \(d_{vu}=a_{vu} \land \neg h_u\). A private binary OR tree joins the edge terms. No internal decoder gate is shared; channel leaves may repeat. For each \(v\), let \(B_v\) contain its faulty qualifier \(h_v\) and all its outgoing gates \(a_{vu},d_{vu}\). Signed negative inputs require no additional inverter gates. These sets are disjoint and connected through \(h_v\); each connection from \(h_u\) to \(d_{vu}\) gives the required edge between \(B_u\) and \(B_v\). Hence \(J\) is a minor. Each gate of \(B_v\) is reachable from the primary enable \(e_v\) along a path of signals belonging only to \(v\), first through the channel's private qualifier tree and then through its private edge term. Each edge contributes two guards, so bounded degree preserves linear total size. A bounded-degree vertex expander on \(m\) vertices has treewidth \(\Omega(m)\). To see this, remove a balanced-separator bag of a tree decomposition. If the bag is small, components of size at most \(m/2\) can be grouped into a set of size between \(m/4\) and \(m/2\); all its outside neighbors lie in the bag, so vertex expansion forces a linear-size bag. If the bag is already large, the conclusion holds directly. The minor therefore gives the circuit treewidth bound. Complete gate clauses also give the corresponding native primal-graph minor; binary output-to-input clauses supply the subdivided edges for an incidence-graph minor. For net cut-width, retain the vertices in \(\bigcup_v B_v\), and delete entire shared target and selector nets before restricting the remaining nets. Deleting just a shared net's producer would leave a large hyperedge. The retained two-section graph still has the \(J\) minor. If \(D\) bounds the degree of \(J\), each retained net has at most \(D+3\) vertices. Under every ordering, each vertex counted by vertex separation belongs to a crossing net; therefore \(\operatorname{pathwidth}\le (D+3)\operatorname{cut\text{-}width}\) {[}Kin92{]}. Net/vertex deletion does not increase cut-width, proving the linear bound for the full circuit. Finally, a block with at most \(K\) inputs meets at most \(K\) of the \(B_v\): follow the \(v\)-owned path from primary \(e_v\) to a gate in that block and take its first entering signal. Primary signals count as block inputs. Different \(v\) give distinct input signals. Replace every bag of a block-graph decomposition by the vertices whose \(B_v\) meets a block in that bag. The blocks meeting a connected branch set \(B_v\) form a connected subgraph of the block graph. Their bag subtrees have a connected union, because adjacent blocks occur together in a bag. Thus the replacement bags satisfy the running-intersection property for \(v\). Each edge of \(J\) has endpoints in the same block or in adjacent blocks, so a replacement bag covers it. The resulting decomposition of \(J\) has bags of size at most \(K(w+1)\). Thus \(\operatorname{tw}(J)+1 \le K(w+1)\). Since \(N=\Theta(m)\), all bounds follow. \ensuremath{\square} These are bounds for the specified gate layout and encoding, not for all equivalent representations or for the running times of {[}CAB90, Fuj90, PCK99{]}. They exclude every fixed \((K,w)\) and logarithmic cut-width bound while detection remains linear after role recovery on this single-output, healthy-one subfamily. The explicit grid comparison used by the timing panel is given in the structural companion {[}Sha26S{]}. The native CNF also contains a simple obstruction to small syntactic backdoors. For a CNF class \(C\), a \emph{strong backdoor} is a variable set \(B\) such that every assignment to \(B\), followed only by deleting satisfied clauses and false assigned literals, leaves a formula in \(C\). A \emph{deletion backdoor} is a set whose literals can be removed from every clause to leave a formula in \(C\). Here the base classes are purely syntactic: the presence of an empty clause does not excuse other clauses from their class conditions {[}DGS14, OSS24{]}. \textbf{Proposition 6.12 (syntactic backdoors).} Every strong or deletion backdoor of the native complete-gate encoding into Horn, renamable Horn, or 2-CNF has size at least \(b\). \emph{Proof.} The complete encoding of \(x \oplus y \oplus z = c\) consists of four ternary clauses. Any complementation of its three variables merely switches between two parities of clause-sign patterns. One contains the all-positive clause; the other contains three clauses with two positive literals. Thus the block is never renamable Horn, and it is not 2-CNF. Fix one healthy channel and take its mask XOR at each bus. The three variables in each block are the bus flag, its local complemented contribution, and a fresh mask output. In the native encoding these \(b\) triples are pairwise disjoint. If a backdoor \(B\) misses one triple, all four clauses of that block survive unchanged under every assignment to \(B\) or deletion of the \(B\)-literals. No renaming of the whole residual formula can make this subformula Horn. A backdoor must therefore hit every triple, requiring at least \(b\) variables. The Horn and 2-CNF claims follow from the same obstruction. \ensuremath{\square} This comparison concerns the complete blocks retained by the native encoding. Taking \(n=b\) makes both the treewidth and these backdoor sizes unbounded while the family remains polynomially decidable. Propagation, algebraic rewriting, and richer backdoor measures can exploit other constraints; their running times are not bounded below by this argument. \subsection{7. Gate-basis and live-conjunction boundaries}\label{gate-basis-and-live-conjunction-boundaries} The algorithm in Section 5 allows disjunction and conjunction of one computed child with negative channel guards. This section classifies detection when a conjunction may also have two computed children. The original guarded syntax remains the polynomial case already proved; the lower bounds below apply only after those conjunctions are added. \textbf{Theorem 7.1 (NP-completeness).} If the grammar allows an unbounded number of binary ANDs with two live children, detection is NP-complete, even with \(b = 1\), a one-channel driver set, and one output bit. \emph{Proof.} Reduce from 3-SAT. Use channels \(t\), a marker \(s\), and \(z_1,\ldots,z_k\), with \(s\) as the single driver. The marker makes the healthy value zero, because \(s\) is not eligible in the healthy set \(\{t\}\). \begin{itemize} \tightlist \item Translate a positive literal \(z_j\) as \(h_{z_j}\). \item Translate \(\neg z_j\) as the guarded term \(h_t \land \neg h_{z_j}\). \item Join the literals of each clause with OR, and the clauses with the new ANDs, giving \(\Phi\). Observe \(F = h_s \land \Phi\). \end{itemize} The healthy value is \(F(\{t\}) = 0\). Every reachable faulty set contains \(t\), so each translated literal takes its literal's value. A detecting set therefore exists exactly when \(\phi\) is satisfiable, as witnessed by \(\{t,s\}\cup\{\text{true variables}\}\). Membership in NP is immediate. \ensuremath{\square} Figure 4 shows the reduction on three clauses. Changing \(z\) from zero to one satisfies the second clause while preserving the other two, and the added live-AND gates propagate this change to the output. \pandocbounded{\includegraphics[keepaspectratio,alt={Three-clause 3-SAT translation with values before and after changing z}]{figures/3sat-live-and-transition.pdf}} \emph{Figure 4. Translation of \((x \lor \neg y \lor z) \land (\neg x \lor y \lor z) \land (x \lor y \lor \neg z)\) from Theorem 7.1, with one bus and drive one. Blue operations belong to the original guarded grammar; orange gates conjoin two live children. Each annotation compares \(K_0=\{t,s,x\}\) with \(K_1=\{t,s,x,z\}\). The healthy set \(\{t\}\) has output zero; \(K_1\) has output one and detects the fault. The NP-completeness theorem concerns the extension allowing an unbounded number of the orange gates.} \textbf{Lemma 7.2 (bounded positive support).} Extend the guarded grammar by \(k\) distinct binary live-AND nodes in the whole DAG. If an output is true on an eligible set \(K\), it is true on some subset of \(K\) of size at most \(k+1\). If \(K\) contains the target, adjoining the target to that subset preserves truth and gives a reachable set of size at most \(k+2\). \emph{Proof.} In the true subgraph rooted at the output, choose one true child at each OR, the live child at each guard, and both children at each AND. Choose the same child whenever a shared OR is encountered. Every internal node has outdegree one, except at most \(k\) nodes of outdegree two. If there are \(I\) internal nodes and \(l\) distinct leaves, connectedness gives \(I+l-1\le\text{number of edges}\le I+k\), hence \(l \le k+1\). A true leaf is a channel. Retain just these channels from \(K\): all chosen positive leaves stay true and every chosen negative guard remains satisfied. Adjoining \(t\) is safe when \(t\) was already in \(K\). \ensuremath{\square} \textbf{Lemma 7.3 (guarded expansion).} At each binary live AND of a decoder \(F\), select one of its two children and replace the node by that child. Writing \(F_\sigma\) for the resulting guarded DAG, with one consistent choice per shared node, one has \(F = \bigwedge_\sigma F_\sigma\) pointwise. At most \(2^k\) choices are needed, where \(k\) counts the live ANDs in its cone. \emph{Proof.} All surrounding operations are monotone in their live children, so removing either child of a conjunction gives \(F \le F_\sigma\). For a fixed channel assignment, choose a false child at every false AND and either child at every true AND, using values in the original DAG. Topological induction shows that this choice preserves every node value. Thus some \(F_\sigma\) equals \(F\) on that assignment, proving the identity. \ensuremath{\square} \textbf{Theorem 7.4 (bounded live conjunction).} Put \(B_k(n)=\sum_{j=0}^{\min(k+1,n)}\binom{n}{j}\). For supplied decoder DAGs with at most \(k\) additional binary live ANDs, detection and an eligible-set witness can be found in \[ O\bigl((B_k(n)+q2^k)G\bigr)\text{ time},\qquad O(G)\text{ working space}. \] Writing and lifting a native model adds \(O(N)\) time and space. For each fixed \(k\) this is polynomial; for \(k=1\) the time is \(O((n^2+q)G+N)\) including lifting. The parameterized bound is XP in \(k\). The branch for healthy-one outputs alone has time \(O(q 2^k G)\) and is FPT in \(k\). \emph{Proof.} For healthy-zero outputs, enumerate the nonempty supports of size at most \(k+1\). For one bus, adjoin \(t\), including the empty support as a candidate. Each evaluation checks all relevant outputs simultaneously. Lemma 7.2 proves completeness. For a healthy-one output, Lemma 7.3 says that some reachable zero of \(F\) exists exactly when some guarded expansion has a reachable zero. Test these expansions with Algorithm 1's dual-Horn branch. Generate one support or expansion at a time and reuse the working arrays. The model realization of Theorem 4.1 is unchanged. \ensuremath{\square} Thus one extra live AND does not yield the hardness of Theorem 7.1. The extension is an algorithm for a supplied decoder representation; Appendix A's native recognition guarantee concerns the original guarded grammar. \textbf{Theorem 7.5 (typed gate-basis dichotomy).} Let \(B\) be a fixed subset of the following three operations: OR of live children, binary AND of two live children, and a negative channel guard \(f \land \neg h_i\). Let \(D(B)\) contain all finite acyclic decoder DAGs made from zero and positive channel leaves using operations in \(B\), with unrestricted sharing and repeated input occurrences. Detection on supplied \(D(B)\) representations is polynomial for every proper subset \(B\), and NP-complete when all three operations are available. The hard case already has one bus, one driver and one output. \emph{Proof.} Multi-channel guards are chains of single-channel guards, so their admission makes no difference to the classification. \begin{itemize} \tightlist \item \textbf{No live AND.} This is the guarded class of Theorem 5.1. \item \textbf{No negative guard.} Every output is monotone. A healthy-zero output has a reachable one exactly when its value on the full channel set is one. A healthy-one output has a reachable zero exactly when it is zero on a minimal reachable set: \(\{t\}\) for one bus, or one of the singletons for at least two buses. Evaluate these at most \(n+1\) sets for all outputs in \(O(nG)\) time. \item \textbf{No OR.} Every output is zero or one conjunction of positive and negative channel literals. Compute these literal sets by topological union, marking a node zero if a child is zero or both signs of a channel occur. This takes \(O(nG)\) time and space. To find a reachable one, retain all positive literals and the forced target and reject any negative conflict. If no channel has been selected, add one channel that does not occur negatively; if every channel does, no reachable one exists. To find a reachable zero, falsify one conjunct while obeying the target/nonemptiness condition. These tests are polynomial for all outputs. \end{itemize} Every proper subset omits an operation and is covered by one of these cases. Theorem 7.1 supplies NP-hardness for the full basis; evaluating a guessed reachable set proves membership in NP. \ensuremath{\square} The negative input of a guard is a channel literal, not an arbitrary subdecoder. The theorem classifies eight syntax languages. It does not classify every further graph restriction of the full language, or assign hardness to individual inputs containing all three gate types. \textbf{Theorem 7.6 (live-AND parameter hardness).} Detection for supplied decoders with \(k\) binary live ANDs is W{[}1{]}-hard parameterized by \(k\), even with one healthy-zero output, one bus and one driver. This holds when every internal gate has fanout at most one, every guard has one negative channel literal, and the live ANDs form a binary tree joining guarded subformulas. \emph{Proof.} Let a graph \(J=(V,E)\) have a partition into \(r \ge 2\) nonempty color classes \(V_1,\ldots ,V_r\). Multicolored Clique asks for a clique containing exactly one vertex of each class. Use channels \(V \cup \{t\}\) and one bus. For \(v \in V_i\), set \[ \begin{aligned} B_v&=(V_i\smallsetminus\{v\})\cup\{u\in V\smallsetminus V_i:uv\notin E\},\\ T_v&=h_v\land\bigwedge_{u\in B_v}\neg h_u,\\ A_i&=\bigvee_{v\in V_i}T_v,\\ F_J&=\bigwedge_{i=1}^r A_i. \end{aligned} \] Each \(T_v\) is guarded; binary OR trees build the \(A_i\). A binary tree joining their roots uses exactly \(k=r-1\) live ANDs. Use separate internal gates for each term, so internal fanout is at most one. Negative guards can be implemented one literal at a time. The decoder has size \(O(\lvert V\rvert^2)\). The healthy value \(F_J(\{t\})\) is zero. Suppose \(F_J(K)=1\). For each class choose a true term \(T_v\). Its same-class guards exclude every other vertex of that class from \(K\); its other guards exclude all its nonneighbors. Consequently \(K \smallsetminus \{t\}\) contains exactly one vertex per class and these vertices form a clique. Conversely, every such clique \(C\) makes all its chosen terms true on \(\{t\} \cup C\). By Theorem 4.1 these sets are reachable. Thus the detecting eligible sets are in bijection with multicolored cliques. Any vertex may serve as the single driver, whose enable can be one while its first request is zero. For completeness, ordinary \(r\)-Clique reduces to this colored problem by making \(r\) copies of the input vertex set. Vertices in distinct copies are adjacent exactly when their original vertices are adjacent. The graph is simple, so a colored clique cannot reuse an original vertex. The construction preserves \(r\), and \(k=r-1\) is a parameter-preserving reduction from the W{[}1{]}-complete Clique problem. \ensuremath{\square} In this construction every detecting set has exactly \(k+2\) channels including the target. Every true set needs \(k+1\) vertex channels. Thus the positive-support and target-adjoining bounds of Lemma 7.2 are attained. In particular, internal gate sharing and guards with multiple negative inputs are unnecessary for the parameterized hardness. Repeated channel occurrences across different terms remain essential to this construction. \textbf{Corollary 7.7 (conditional exponent lower bound).} Unless \(\mathrm{FPT}=\mathrm{W}[1]\), the full problem of Theorem 7.4 has no FPT algorithm in \(k\). Under ETH it has no algorithm of time \(f(k)G^{o(k)}\) for any computable \(f\). The latter bound also holds with the size \(N\) of a complete native controller encoding in place of \(G\), even when its circuit roles are supplied. \emph{Proof.} The first assertion follows from Theorem 7.6. For an \(r\)-Clique instance on \(p\) vertices, its colored graph has \(rp\) vertices and the decoder has size \(G=O(r^2 p^2)\). With one bus the complete native encoding also has \(N=O(r^2 p^2)\). A hypothetical algorithm of either stated form, including the polynomial construction cost, would solve Clique in \(f'(r)p^{o(r)}\) time. Under ETH, not every SNP problem admits a subexponential algorithm, so {[}CHKX06, Theorem 5.5{]}, with the polynomial encoding-length conversion stated in Section 2, excludes this Clique algorithm. \ensuremath{\square} The corollary rules out a sublinear dependence on \(k\) in the polynomial exponent under ETH. It does not establish the optimal constant in that exponent. Its lower bound concerns the live-AND extension; it supplies no quadratic or cubic lower bound for decision in the original guarded class. Fine-grained bounds for the original guarded class are treated in the guarded-reachability companion {[}Sha26B{]} under their own named hypotheses. \subsubsection{7.1. A fault-model boundary inside the guarded grammar}\label{a-fault-model-boundary-inside-the-guarded-grammar} The preceding results vary the decoder gates while keeping the first-stage bridge interface fixed. The exact pair image in Theorem 4.6 permits a second comparison: retain the guarded grammar and change the fault to the specified final-qualifier occurrence. Here a witness must make one cofactor true and the other false on the same non-target channel set. \textbf{Theorem 7.8 (stuck-at detection on guarded DAGs).} For either fixed stuck value, detection of a final-qualifier stuck-at fault by a supplied guarded DAG is NP-complete, even with one bus and one observed output. No conjunction of two computed children is required. \emph{Proof.} Membership in NP follows by guessing a primary input and evaluating the controller and decoder. For hardness, let \(\phi\) be a 3-SAT formula on variables \(x_1,\ldots ,x_m\). Introduce channels \(t,s\) and pairs \(p_i,q_i\). Replace each positive source literal by \(p_i\) and each negative literal by \(q_i\), and append all positive pair clauses \(p_i \lor q_i\). Call the resulting clause list \(C\). Construct \[ \begin{aligned} A&=\bigvee_{C\text{ in the list}}\left(h_s\land\bigwedge_{u\in C}\neg h_u\right),\\ B_0&=h_s,\\ B_i&=(B_{i-1}\land\neg h_{p_i})\lor(B_{i-1}\land\neg h_{q_i}),\\ F&=A\lor(B_m\land\neg h_t). \end{aligned} \] The two uses of \(B_{i-1}\) share a node. Every gate is allowed by the guarded grammar, and the size is linear in the source variable and literal counts. Induction gives \(B_m = h_s \land \bigwedge_i (\neg h_{p_i} \lor \neg h_{q_i})\). The two target cofactors are \(F_0=A \lor B_m\) and \(F_1=A\). They differ precisely when \(B_m=1\) and \(A=0\). The first condition requires \(s\) and forbids selecting both channels of any pair. Given \(s\), the second requires at least one of each pair and at least one translated literal of every source clause. Thus the detecting sets choose exactly one channel per source variable and encode precisely the satisfying assignments of \(\phi\), with \(s\) included. Conversely each satisfying assignment gives such a set. It is nonempty, so Theorem 4.6 realizes the discrepancy with one bus for either stuck value. \ensuremath{\square} The reduction uses the target only in one negative guard. Its source formula is encoded in the simultaneous truth and falsity conditions; either condition alone admits the guarded reasoning used in Section 5. \textbf{Theorem 7.9 (path-parameter algorithm and unshared formulas).} For a single supplied guarded output with \(P\) structural root-to-leaf paths, final-qualifier stuck-at detection has an exact algorithm taking \(O((P+1)G)\) time and \(O(G)\) working words. For an output formula forest with no shared internal gates and total counted size \(G\), detection takes \(O(G^2)\) time and \(O(G)\) working words. Writing a physical test adds \(O(nb)\) time; constructing a complete native model adds \(O(N)\). \emph{Proof.} Search the two directions \(F_v(K)=1\), \(F_{1-v}(K)=0\), for \(v=0,1\). Build the one-way dual-Horn zero encoding of Algorithm 1 (lines 8--12) for the opposite copy, require its root false, and fix its target to \(1-v\). For stuck value zero add the nonemptiness clause \(\bigvee_{i \ne t} h_i\). Every true evaluation of the first copy has a supporting path: choose one true OR child and retain the live child at each guard. Enumerate such structural paths with the target fixed to \(v\). A target guard kills a path when \(v=1\) and disappears when \(v=0\). A target leaf is false when \(v=0\); when \(v=1\) it is a constant-true terminal and supplies no head unit to the opposite copy. A non-target leaf supplies a positive head unit. Every non-target path guard supplies a negative unit. Reject paths whose head is also guarded. Append these path units to the opposite zero system and compute its greatest model. All clauses remain dual-Horn. A consistent model supplies a common set \(K\) making the path true and the opposite cofactor false. Conversely any detecting \(K\) has a true support path in one direction, and its actual opposite-copy gate values extend it to a model of that path's zero system. Testing all paths in both directions is therefore sound and complete. Theorem 4.6 lifts any returned \(K\) to a physical test. Each path test costs \(O(G)\). A depth-first traversal with reversible guard counts streams paths without retaining all guard sets, using \(O(G)\) working words and \(O((P+1)G)\) total work. In an unshared formula each path ends at a distinct leaf occurrence. For a forest, the total number of paths and outputs is \(O(G)\). Process the outputs sequentially, retaining at most one zero system and path state; each test costs at most \(O(G)\). This gives the asserted total time and space. \ensuremath{\square} For a single direction only the true cofactor's path count enters: the opposite cofactor may remain an arbitrary shared DAG. Both directions must still be resolved to conclude undetectability. Appendix D gives counterexamples to immediate shortcuts and a second algorithm whose parameter is the number and width of multi-positive zero-system clauses. {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{}ll@{}} \toprule\noalign{} Fault and supplied decoder & Detection complexity \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot First-stage bridge; guarded DAG & \(O((n+q)G)\) (Theorem 5.1) \\ First-stage bridge; formula forest & \(O(G)\) (Theorem 5.6) \\ Final-qualifier stuck-at; guarded DAG & NP-complete (Theorem 7.8) \\ Final-qualifier stuck-at; formula forest & \(O(G^2)\) (Theorem 7.9) \\ \end{longtable} } The table concerns the specified Boolean interfaces and qualifier observations. It does not classify arbitrary physical bridge or stuck-at faults elsewhere in a circuit. \subsection{8. Native encodings and independent answer certificates}\label{native-encodings-and-independent-answer-certificates} The guarded algorithm in Section 5 receives the selector roles and the decoder. To apply it to an unannotated CNF, the implementation must establish that the clauses describe this guarded family. The live-AND extension of Section 7 remains a separate supplied-DAG algorithm. Checking a supplied description of those roles and discovering the roles are separate tasks; a worst-case discovery bound remains open. Appendix A gives a recognition contract for exposed complete gate blocks, including the physical recurrences, shared primary inputs, drive interface, paired outputs and exact auxiliary projection. Every input clause must be accounted for. Failure to recover or verify a permitted representation returns \texttt{OUTSIDE} (or implementation status \texttt{OPEN}). These statuses mean that no representation was verified; they establish neither nonmembership nor unsatisfiability. For a recovered SAT member, the eligible-set witness lifts by Theorem 4.1 to a primary test. Topological evaluation supplies the functional gate values. The bridge and observation projection records supply any private auxiliary extensions. Inverse alias transport gives an assignment to the original variables, and every original clause is then checked. Standard SAT solvers also return models with this interpretation on a complete native encoding. The family algorithm supplies the explicit semantic route to the witness. For an UNSAT member of the guarded family's specified native encoding, Theorem B.1 gives an ordinary DAG-resolution refutation with \(O(N^3)\) inferences and no extension variables. Its proof first derives the selector image inside the native clauses, then compiles the guarded decision argument. The implementation emits the derivation and an independent checker replays it. Appendix B states the exact encoding, local derivation rules, inference bound and executable contract. The \(O(N^3)\) bound counts inferences, not the byte size or wall time of the compiler. An optional-activity observation uses auxiliary activity variables whose assertion requires a corresponding output discrepancy; a requirement circuit selects the activities that must hold. These variables need not be functional gate outputs. The optional-activity observation theorem (Theorem B.2) extends the proof bound over a native physical core, with a separate wrapper term. Its full general implementation remains open. The accompanying formalization contains an independent supplied-record checker: an accepted complete record establishes the recovered family projection of the exact original indexed CNF and provides model lifting. Discovering such a record and proving total discovery costs are separate obligations. Section 13 states the formalization coverage and remaining integration boundaries. Proof-producing CDCL already supports independently checkable UNSAT certificates {[}WHH14{]}, and resolution simulation results relate it to the native upper bound {[}PD11{]}. The specific result here is a guaranteed polynomial proof-generation schedule for the stated family. It supplies no lower bound on the runtime of CDCL or other general SAT solvers. \subsection{9. Experiments}\label{experiments} The measurements compare a Python family implementation, including role recovery, with general SAT solvers on retained generated inputs. They validate executable behavior and document cost; the uniform complexity claims follow from the proofs. Appendix C records the exhaustive small checks, reduction checks and certificate controls. \textbf{Timed decoder families.} The scaling panel uses drive one, target \(t=1\) and the single driver \(s=2\). With channel labels \(1,\ldots ,n\), its decoders are {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.5000}} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.5000}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedright Label \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Decoder \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot cycle & \(\bigvee_{i=1}^n (h_i \land \neg h_{i+1})\), with \(h_{n+1}=h_1\) \\ chain & \(h_n \lor \bigvee_{i=1}^{n-1} (h_i \land \neg h_{i+1})\) \\ all-OR & \(\bigvee_{i=1}^n h_i\) \\ grid & \((h_t \land \neg h_s) \lor \bigvee_{uv \in E, u \in L} (h_u \land \neg h_v)\) \\ \end{longtable} } For the grid, \(n=k^2+2\); the grid channels are \(v(a,b)=3+ak+b\) for \(0\le a,b{\raggedright\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1034}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1379}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1379}} >{\raggedright\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1034}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1379}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1379}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1379}} >{\raggedright\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1034}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedright Decoder (answer) \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft Buses \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft Channels \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Variables / clauses \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft Native family route \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft MiniSat \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft Glucose \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Probing \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot cycle (SAT) & 1 & 8 & 158 / 428 & 0.03 s & 0.01 s & 0.01 s & undecided \\ cycle (SAT) & 1 & 32 & 614 / 1,628 & 0.12 s & 0.01 s & 0.01 s & undecided \\ cycle (SAT) & 1 & 128 & 2,438 / 6,428 & 1.33 s & 0.01 s & 0.01 s & undecided \\ cycle (SAT) & 3 & 8 & 418 / 1,158 & 0.05 s & 0.01 s & 0.01 s & undecided \\ cycle (SAT) & 3 & 32 & 1,642 / 4,518 & 0.30 s & 0.02 s & 0.01 s & undecided \\ cycle (SAT) & 3 & 128 & 6,538 / 17,958 & 3.75 s & 0.19 s & 0.14 s & undecided \\ chain (UNSAT) & 1 & 8 & 156 / 422 & 0.03 s & 0.01 s & 0.01 s & refutes \\ chain (UNSAT) & 1 & 32 & 612 / 1,622 & 0.12 s & 0.01 s & 0.01 s & refutes \\ chain (UNSAT) & 1 & 128 & 2,436 / 6,422 & 1.35 s & 0.01 s & 0.01 s & refutes \\ chain (UNSAT) & 3 & 8 & 416 / 1,152 & 0.05 s & 0.01 s & 0.01 s & undecided \\ chain (UNSAT) & 3 & 32 & 1,640 / 4,512 & 0.30 s & 0.02 s & 0.02 s & undecided \\ chain (UNSAT) & 3 & 128 & 6,536 / 17,952 & 3.73 s & 0.18 s & 0.16 s & undecided \\ all-OR (UNSAT) & 1 & 8 & 142 / 380 & 0.03 s & 0.01 s & 0.01 s & refutes \\ all-OR (UNSAT) & 1 & 32 & 550 / 1,436 & 0.10 s & 0.01 s & 0.01 s & refutes \\ all-OR (UNSAT) & 1 & 128 & 2,182 / 5,660 & 1.13 s & 0.01 s & 0.01 s & refutes \\ all-OR (UNSAT) & 3 & 8 & 402 / 1,110 & 0.05 s & 0.01 s & 0.01 s & undecided \\ all-OR (UNSAT) & 3 & 32 & 1,578 / 4,326 & 0.29 s & 0.02 s & 0.02 s & undecided \\ all-OR (UNSAT) & 3 & 128 & 6,282 / 17,190 & 3.54 s & 0.13 s & 0.14 s & undecided \\ grid (SAT) & 1 & 11 & 223 / 602 & 0.04 s & 0.01 s & 0.01 s & undecided \\ grid (SAT) & 1 & 38 & 820 / 2,204 & 0.18 s & 0.01 s & 0.01 s & undecided \\ grid (SAT) & 1 & 123 & 2,735 / 7,354 & 1.52 s & 0.02 s & 0.01 s & undecided \\ \end{longtable} } \textbf{Reading the table.} \begin{itemize} \tightlist \item \textbf{Native family route.} It decides every input and constructs a model whenever one exists. Its Python time includes recognition and reaches 3.75 s. This finite panel establishes no average-case or asymptotic exponent. \item \textbf{CDCL.} MiniSat and Glucose are faster on every input, at most 0.2 s. Theorem B.1 gives short proofs for UNSAT instances of the specified guarded native encoding; it does not predict a solver's search time or explain performance on SAT instances. The scaling harness records answers and statistics, not resolution traces. \item \textbf{Probing.} It refutes only the one-bus UNSAT inputs. It cannot establish SAT. \end{itemize} The experiment establishes correctness on the retained finite panel and an end-to-end runtime comparison. The polynomial guarantees come from the structural proofs. This panel does not measure the separate extension kernels, and it does not separate parsing, discovery, decision and lifting costs or report repeated timing distributions. \textbf{Graph-cover expanders.} A second panel uses Proposition 6.4 with the Margulis--Gabber--Galil construction {[}HLW06, Construction 8.1, Theorem 8.2{]}. For modulus \(a\), its vertices are \(\mathbb{Z}_a^2\); each \((x,y)\) is joined to \((x+2y,y)\), \((x+2y+1,y)\), \((x,y+2x)\), and \((x,y+2x+1)\), with undirected edges and arithmetic modulo \(a\). We delete loops and merge parallel edges before making the graph-cover controller. The resulting simple graphs retain every external vertex neighbourhood and have maximum degree eight. The multigraph spectral bound gives at least \((8-5\sqrt{2})\lvert S\rvert/2\) crossing edges when \(\lvert S\rvert\) is at most half the vertices. Each outside vertex receives at most eight such edges, so the simple graph has vertex expansion at least \((8-5\sqrt{2})/16\). These inputs therefore belong to a uniform bounded-degree expander family. We use all six moduli \(3,4,5,6,8,10\), giving 9 through 100 graph vertices and one extra target channel. All controllers have one bus, drive one, a single driver, and no auxiliary Horn chain. Every input is SAT. Three fresh, sequential processes per method and size run under the environment above, with a 10-second wall limit per worker and a rotating method order. No run times out. Inputs and all Python sources are retained with hashes. The decision methods receive the native CNF. RC2 {[}IMS19{]} minimizes the number of true faulty qualifiers on that same CNF by giving each negative qualifier a unit-weight soft clause. A second RC2 run receives the exact projected vertex-cover formula, with hard clauses \(h_u \lor h_v\) and soft clauses \(\neg h_v\); one is added to its optimum for the target. Both use Glucose3 as their SAT oracle. This compares two formulations of the same minimum-eligible-set objective. Each returned native model is checked against every clause. All six optimum values also pass a separate MiniSat check that no smaller cover exists, and each minimum cover lifts to a clause-checked native model. These optimum cross-checks use a second solver; they do not export lower-bound proof certificates. The table gives medians in seconds, including imports, parsing, solver setup, decision or optimization, and witness checking. Interpreter startup, input generation, and the separate optimum cross-check are excluded. Raw repetitions and their minima and maxima are in the retained summary. {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1290}} >{\raggedright\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.0968}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1290}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1290}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1290}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1290}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1290}} >{\raggedleft\arraybackslash}p{(\linewidth - 14\tabcolsep) * \real{0.1290}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedleft Graph vertices \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Native variables / clauses \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft Native family decision \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft MiniSat \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft Glucose \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft RC2 minimum, native CNF \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft RC2 minimum, graph formula \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedleft Minimum eligible size \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot 9 & 225 / 644 & 0.0376 & 0.0099 & 0.0099 & 0.0129 & 0.0099 & 7 \\ 16 & 418 / 1,195 & 0.0699 & 0.0108 & 0.0113 & 0.0141 & 0.0097 & 11 \\ 25 & 673 / 1,924 & 0.1332 & 0.0123 & 0.0132 & 0.0173 & 0.0101 & 18 \\ 36 & 988 / 2,825 & 0.2392 & 0.0133 & 0.0136 & 0.0227 & 0.0106 & 25 \\ 64 & 1,804 / 5,161 & 0.6615 & 0.0176 & 0.0182 & 0.1807 & 0.0126 & 44 \\ 100 & 2,870 / 8,215 & 1.5580 & 0.0235 & 0.0243 & 1.8598 & 0.1459 & 67 \\ \end{longtable} } CDCL remains faster than the native family route on this panel. Minimum witness solving becomes more expensive at the larger sizes, especially on the native encoding, while all instances still finish within the limit. Neither this finite growth nor the NP-hardness theorem implies exponential runtime on this particular sequence. Corollary 6.5 establishes hardness over arbitrary embedded graphs; it does not establish optimization hardness for the fixed Margulis--Gabber--Galil sequence. The representation lower bound applies uniformly to its growing expander controllers by Theorem 6.9. \subsection{10. Related work and attribution}\label{related-work-and-attribution} The comparisons are separated by the circuit, the decision procedure, and the tasks that remain hard after the reachable sets are known. Each citation is used for the theorem named with it. \begin{itemize} \item \textbf{Origin of the instances and encoding.} The SATLIB SSA and BF files were generated by Nemesis {[}Lar92{]}, using the bridge-fault model of {[}FL91{]}. We analyze their compact CNFs and use complete Tseitin gate blocks for the native generalized family. \item \textbf{The c432 model.} The architecture comes from the reverse engineering in {[}HYH99{]}, which {[}HH95{]} used for high-level test generation of the fixed circuit. We extend the qualifier recurrence to every \(n\) and \(b\). The reachable-set theorem applies to that qualifier vector, before the channel encoder. \item \textbf{Tractable test-generation classes.} We compare against {[}IS75, FT82, Fuj90, CAB90, PCK99{]} in Sections 6--7. The original guarded controller result uses its semantic image; the circuit-width obstructions concern the specified native layout. \item \textbf{Untestability identification.} FIRE {[}IA96{]} and related implication methods are sound but incomplete. Algorithm 1 is complete for the grammar. \item \textbf{Regular structures.} C-testability of iterative arrays {[}Fri73{]} and the CAM priority-encoder test {[}Li05{]} bound test-set size for different devices and questions. \item \textbf{Horn tools.} The fixed point is {[}DG84{]}. More precisely, for a guarded decoder \(F\), the transformation \(H(x)=\neg F(\neg x_1,\ldots,\neg x_n)\) is Horn-NNF {[}Ima21{]}. OR nodes become conjunctions, while a guarded child becomes its transformed child disjoined with negative channel literals. Each disjunction has at most one nonnegative disjunct. This syntax connection does not assert a polynomial-size clausal expansion on the original variables. The direct union-closure argument behind the greatest-zero-set construction follows Proposition 5.2. \item \textbf{Backdoors.} Proposition 6.12 uses static syntactic classes. Dynamic sub-solvers {[}DGS14{]} and backdoor DNFs {[}OSS24{]} distinguish other measures of distance from tractability; the proposition supplies no runtime comparison with them. \item \textbf{Optimization and compilation.} Vertex-cover decision and counting hardness are classical {[}Kar72, PB83{]}. Theorem 6.9 imports the expander-CNF DNNF lower bound {[}BCMS15{]}. Proposition 6.4 embeds the graph relation into a physically realizable controller image; the restriction and projection justify applying those results to both primary detection and native CNF. \item \textbf{Proof complexity.} The resolution simulation in {[}PD11{]} applies to Theorem B.1's native bridge encoding. Proof-producing CDCL solvers already support independent UNSAT checking, for example through DRAT {[}WHH14{]}. Their SAT models also give primary-input tests for the complete native encoding. The family-specific result here is the semantic construction and its guaranteed polynomial native proof-generation schedule. The DNNF-hard controllers are satisfiable and concern representation of all models, so their bound is compatible with short refutations of UNSAT native members. \item \textbf{Parameterized lower bounds.} Clique hardness and its ETH-based exponent lower bound are classical {[}CHKX06{]}. Theorem 7.6 transfers them through an exact eligible-set bijection using \(r-1\) live ANDs, single negative guards and no shared internal gates. Theorem 7.5 is a classification of the three typed operations used here, rather than a classification of arbitrary Boolean constraint languages. \end{itemize} Proposition 5.3 is a transfer of monotone circuit-value P-completeness {[}Gol77; GHR95, Theorem 6.2.2{]}. Proposition 6.6 transfers independent-set optimization and counting, and Theorem 6.8 uses clone interpolation to handle native-model multiplicities. The extension oracle and prefix enumeration specialize standard self-reduction. These are applications to the controller representation; the general source hardness and algorithmic methods are classical. The stuck-at reduction of Theorem 7.8 specializes classical SAT hardness to the exact pair image, with shared guarded gates and one target guard. Theorem 7.9 combines support paths with the classical dual-Horn algorithm; Theorem D.2 uses elementary clause strengthening and implication-graph reachability. These supplied-structure results have separate scope from the first-stage native proof compiler. The central contribution is the size-uniform description of the reachable qualifier sets, together with its composition with decision, test lifting, and native refutation. The graph-cover restriction gives the task and representation boundaries for those same sets. The literature search is bounded: priority for the exact reachable-set theorem, the controller embeddings and these structural characterizations remains unestablished. \subsection{11. Limitations and open problems}\label{limitations-and-open-problems} \begin{enumerate} \def\labelenumi{\arabic{enumi}.} \tightlist \item \textbf{Fault model.} The native recognition and proof contract concerns the first-stage bridge of Section 3. Proposition 4.5 covers a specified stage-local bridge with unrestricted primary inputs. Theorem 4.6 covers only the final-qualifier request occurrence, and Theorems 7.8--7.9 use supplied guarded decoders. Their general CNF recovery and proof export are not established. Other physical bridges, enable-wire faults and decoder faults require separate image characterizations. \item \textbf{Recognition.} The supplied-record checker verifies the exposed representation and exact projection contract of Appendix A. Discovery completeness on an explicit syntactic input class and total worst-case discovery time and space bounds remain open. Equivalent CNF rewrites can defeat recovery. The cubic raw-interface candidate count does not settle these obligations; every original clause and any restriction on primary inputs must still be accounted for. \item \textbf{Proof translation.} Theorem B.2 covers optional-activity observations over a native physical core. Translation for every accepted compact physical encoding, and full implementation of the general wrapper theorem, remain open. Formula-forest and bounded-AND kernels operate on supplied DAGs and are separate from CNF recognition and native proof export for the original grammar. \item \textbf{Engineering comparisons.} The reported family implementation is slower than MiniSat and Glucose on the generated decision panels. The measurements do not isolate recognition cost or establish an asymptotic solver comparison. The scaling and expander panels exercise healthy-one outputs; healthy-zero SAT and UNSAT cases and phase-separated costs need their own timing panel. Direct comparisons with FIRE and recursive learning have not been reported. \item \textbf{Tighter family bounds.} The native \(O(N^3)\) resolution bound may admit improvements. A total discovery bound must first be established for the recognition procedure. The live-AND ETH bound controls the order of dependence on \(k\) in the exponent, not its optimal constant. Neither result supplies an unconditional superpolynomial time lower bound. \end{enumerate} \subsection{12. Conclusion}\label{conclusion} The controller recurrence admits an exact description of its reachable qualifier sets, and every set in that description has an explicit primary input. Composing these sets with guarded decoders gives constructive polynomial detection. The native resolution construction explains why unsatisfiable members of the specified functional encoding have short proofs, while optimization, counting and representation tasks can remain hard on the same architecture. The exact stuck-at pair image marks a further boundary: a supplied shared guarded decoder gives an NP-complete problem, while an unshared formula forest remains polynomial. The observation interface and encoding contract determine which conclusions apply; formal and experimental coverage is specified separately below. \subsection{13. Reproducibility}\label{reproducibility} The source archive on \href{https://doi.org/10.5281/zenodo.23400056}{Zenodo} contains this manuscript, four vector figures, a finite-check supplement for the fault-model extensions, and an amendment verification supplement. Their READMEs give replay commands and coverage. The finite checks establish reported finite behavior; uniform statements are proved in the manuscript. \textbf{Registered Lean formalizations.} Eight Palomar entries record selected Lean statements at immutable source commits. Their theorem names, hypotheses, definition implementations and verification evidence are specified by the versioned records below. The scope column summarizes those selections; it does not identify every manuscript statement with a selected declaration. {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.5000}} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.5000}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedright Record \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Selected formal scope \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot {[}Sha26a{]} & Exact first-stage bridge images, observation equivalence, nonemptiness obstruction and a specified qualifier-only stuck-at classification \\ {[}Sha26b{]} & Supplied guarded-DAG detection correctness and completeness, constrained extensions and native cold-detector execution \\ {[}Sha26c{]} & Canonical enumeration, iterator and streaming execution, emitted witnesses and selected delay and storage bounds \\ {[}Sha26d{]} & Formula-forest execution and attained nonnegative-weight maxima for healthy-zero observations \\ {[}Sha26e{]} & Dual-Horn and vertex-cover embeddings, counted decoder size and detecting eligible-set counts \\ {[}Sha26f{]} & Critical sets, test-list and query bounds, source recovery, native width and backdoor bounds; cover-layout width under the selected hypotheses \\ {[}Sha26g{]} & Bounded-support and selector expansion, bounded-conjunction and proper-basis execution, with selected XP and healthy-one FPT inequalities \\ {[}Sha26h{]} & Ordinary-resolution construction for native encodings and supported observation wrappers, with inference and derived-literal storage bounds \\ \end{longtable} } Each entry verifies its selected formal statements at its recorded commit. The workspace correspondence table below separately records which complete statements of this manuscript have an accepted paper-to-Lean match. Registry verification does not extend that correspondence automatically, and companion source declarations are not additional selected registry targets. \textbf{Formalization coverage.} The workspace coverage map records statement-level acceptance separately from acceptance of component tasks. The following table accounts for all 41 numbered items using this paper's numbering. {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.5000}} >{\raggedright\arraybackslash}p{(\linewidth - 2\tabcolsep) * \real{0.5000}}@{}} \toprule\noalign{} \begin{minipage}[b]{\linewidth}\raggedright Recorded coverage \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright Statements \end{minipage} \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot Statement-level acceptance (6) & 4.1, 4.2, 4.3, 4.4, 6.3, 6.4 \\ All directly listed component tasks accepted; whole-statement correspondence not certified (19) & 5.1, 5.2, 5.4, 5.5, 5.6, 6.1, 6.2, 6.7, 6.10, 6.12, 7.2, 7.3, 7.4, A.1, A.2, A.3, A.4, B.1, B.2 \\ Required component tasks incomplete; source-level full statements (10) & 5.3, 6.5, 6.6, 6.8, 6.9, 6.11, 7.1, 7.5, 7.6, 7.7 \\ Source proofs without recorded formal coverage (6) & 4.5, 4.6, 7.8, 7.9, D.1, D.2 \\ \end{longtable} } The amendment supplement contains a snapshot of the workspace correspondence records. Acceptance of a component checks its stated contract; a full paper statement additionally requires matching its hypotheses, conclusion and resource bounds. No P-, NP-, or \#P-completeness, W{[}1{]}-hardness, ETH consequence or DNNF lower bound is claimed as formally verified. The public Lean sources and selected verification evidence are available at the immutable commits linked by the Palomar records above. This archive does not include the separate Lean repository, the Python native compiler and answer checker, or a complete reproduction package for the timing panels. The formal Lean selections and the reported Python experiments are distinct artifacts. The amendment supplement reconstructs the canonical manuscript from its pinned baseline and 40 declared replacements. It checks the declared changed blocks, recorded coverage and preservation of all 41 numbered statement/proof blocks in this deposit source. It checks document integrity, not mathematical proofs or Lean execution. \subsection{Appendix A. Recognition from exposed CNF encodings}\label{appendix-a.-recognition-from-exposed-cnf-encodings} \textbf{Algorithm 2 (RECOGNIZE-AND-DECIDE)} receives only a CNF file. \begin{enumerate} \def\labelenumi{\arabic{enumi}.} \tightlist \item Enumerate at most \(O(N^3)\) raw bridge-interface candidates, as counted below. Check that their bounded signed blocks project exactly to \(U = 1-d, D = d, W = d\). \item Recover the functional circuit from complete local gate blocks, orienting each producer along the DAG. The unique-producer route fixes AND/OR outputs first, then orients each XOR by its sole variable not among those outputs. Infer roots as variables with no producer and check acyclicity. For a route admitting alternative producers, verify the descendant condition of Lemma A.4 on the recovered DAG itself. \item Recognize the selector chain: \begin{itemize} \tightlist \item the first flag is an OR of disjoint two-primary products; \item each later stage is the unique continuation by one fresh request per channel. \end{itemize} Then check both copies against the physical XOR recurrence and the qualifiers. \item Normalize the paired observed expressions to a common guarded decoder. \item Project the remaining auxiliary clauses (Theorem A.1). They must reduce to the single requirement that the observed outputs differ. \item For a candidate passing all representation checks, run Algorithm 1. Return its decision, lifting any detecting set to a full model checked against every original clause. \item If every candidate fails the representation checks, return \texttt{OUTSIDE} (or implementation status \texttt{OPEN}): no representation was verified. Neither status certifies nonmembership or unsatisfiability. \end{enumerate} \textbf{Accepted representation.} The native route requires complete exposed gate blocks. Primary inputs are not candidate outputs; each XOR block has exactly one variable not produced by an AND/OR block, its output. The selector continuation and final qualifier expressions must be recoverable from their factor footprints, and paired outputs must normalize to the same guarded DAG. Private residual auxiliaries have, after a consistent polarity choice, Horn pure clauses and only negative auxiliary occurrences in signal attachments. Their least-model projection must consist of units requiring the detected output discrepancy. The optional-activity grammar of Theorem A.2 instead supplies checked constant extensions. All clauses must belong to recovered definitions or the verified projection; no unexplained constraints may remain. These are sufficient representation conditions, not a recognizer for arbitrary equivalent CNFs. The complete local templates are the blocks of Section 2, their signed variants and bounded truth-table compositions. A local table is accepted only after every row agrees with its defining clause block. A selector role map labels distinct free roots as the enables and requests and matches both copies to every displayed recurrence in Section 3. It also records the target, the disjoint driver and remaining-channel sets, and the bridge cofactor. Unused roots may serve only as private projection auxiliaries; an additional restriction on a primary input is not admitted. \textbf{Permitted normalization.} Expression nodes are interned after constant evaluation, associative/commutative flattening of AND/OR, duplicate removal, complement-pair simplification, and cancellation of repeated XOR operands modulo two. OR is represented by De Morgan complementation when convenient. Disjoint factoring of a bounded-support truth table is allowed only when all its rows verify the proposed factors. The decoder parser accepts the grammar in Section 5 and requires identical canonical node descriptions on the two sides after qualifiers have been replaced by corresponding channel atoms. Equality under these operations is a sufficient acceptance test; arbitrary Boolean equivalence is not invoked. \textbf{Representation-certificate contract.} A checkable recovery record contains the following data, all indexed to the original clause list: \begin{enumerate} \def\labelenumi{\arabic{enumi}.} \tightlist \item The interface clause IDs, signed alias substitutions and their defining clauses, and the exact bounded projection table relative to the retained driver definitions, including both directions of the extension property. \item The gate output/input map, defining clause IDs and local truth tables, a topological order, and the inferred roots. If a producer has an alternative, list its inputs and check that at least one is a proper descendant of the output in this recovered order's DAG. This makes Lemma A.4's premise checkable without an external intended circuit. \item The selector/qualifier role map and the paired decoder normalization described above, with the bounded factor identities used in matching. \item The auxiliary polarity choice and projection evidence. For negative Horn attachments, supply the least auxiliary model and its propagation reasons. For optional activities, supply the tree and the constant extensions of Theorem A.2. The general semantic condition in Theorem A.1 is not itself a polynomial certificate for arbitrary definitions. \item A clause-coverage table. Every original clause must be a verified gate, interface or auxiliary clause, or become a tautology under a justified alias substitution. Retain every duplicate clause ID. Reject a record with any unexplained clause or unproved transformation. \end{enumerate} To justify the negative-Horn projection in item 4, orient the private auxiliaries so that their pure clauses are Horn and every signal-bearing attachment has only negative auxiliary literals. Let \(L\) be the least model of the pure clauses. In an attachment, if all its auxiliary premises belong to \(L\), its signal clause is necessary in every extension. Otherwise \(L\) satisfies the attachment independently of the signals. Hence these necessary signal clauses are exactly the existential projection. Verify that the resulting clauses require the accepted output discrepancy. Replaying these checks proves equisatisfiability with the recovered controller and its exact observation condition. Algorithm 1 therefore justifies an UNSAT answer as well as a SAT answer. Checking a single returned SAT model is a separate, weaker validation. The implementation records recovered roles, projection data and clause coverage and checks models. The certified entry point additionally exports a model or an ordinary-resolution refutation and checks it against the original CNF (Appendix B). This certifies the SAT/UNSAT answer without trusting role recovery. The formalized supplied-record checker separately validates complete representation payloads, including original clause identities, family projection and model lifting. This soundness statement consumes a supplied record; it is not a completeness theorem for the discovery procedure. The accepted representation conditions are those stated above. \textbf{Theorem A.1 (observation projection).} Let \(D(Z, X)\) be acyclic gate definitions. Let \(H(A, X)\) be the remaining clauses, with private auxiliaries \(A\), activity literals \(s_i\) over \(A\), and guarded observations \[ s_i\to(u_i\oplus v_i). \] Suppose two conditions hold for a set \(J\) of these observations. \begin{enumerate} \def\labelenumi{\arabic{enumi}.} \tightlist \item The auxiliary-only clauses together with \(\{\neg s_i : i \in J\}\) have a unit-propagation contradiction. \item For each \(i \in J\) and each unequal orientation of \((u_i, v_i)\), either the orientation contradicts \(D\), or there is a constant assignment \(a_{i,\mathrm{orientation}}\) to all of \(A\) such that \textbf{every} assignment to \(Z,X\) satisfying \(D\) and that orientation satisfies \(H(a_{i,\mathrm{orientation}},X)\). \end{enumerate} Then \(D\models\bigl[(\exists A\,H)\leftrightarrow\bigvee_{i\in J}(u_i\oplus v_i)\bigr]\). \emph{Proof.} By (1), any model makes some accepted activity true, and its guard clauses force the discrepancy. Conversely, a realized discrepancy cannot contradict \(D\), so (2) supplies an extension. \ensuremath{\square} The next grammar makes both conditions structural. Its connectivity graph can be arbitrarily complicated because its internal activities can all remain inactive; the requirement to observe a discrepancy is carried by a separate tree. \textbf{Theorem A.2 (optional activities).} In the setting of Theorem A.1, partition the auxiliaries into internal activities \(a_v\), observed activities \(s_1,\ldots ,s_r\) with \(r \ge 1\), and requirement-tree variables. After one consistent choice of auxiliary polarity, let \(H\) consist exactly of the following clauses: \begin{enumerate} \def\labelenumi{\arabic{enumi}.} \tightlist \item Discrepancy guards \(a_v \to (u_v \oplus v_v)\) and \(s_i \to (u_i \oplus v_i)\), each encoded by its two clauses. \item Clauses \(\neg a_v\lor\bigl(\text{disjunction of positive auxiliary literals}\bigr)\lor C(X)\), where \(C(X)\) is any clause on signal literals and may be empty. In particular, connectivity clauses \(\neg a_v \lor \bigvee_{w \in S} a_w\) are allowed without restrictions on cycles, shared successors, or overlapping successor sets. \item A rooted binary requirement tree whose leaves are exactly the distinct observed activities, whose internal nodes are fresh auxiliary variables, and whose clauses are \(\neg p\lor\mathrm{child}_1\lor\mathrm{child}_2\), together with the positive root unit. For one observation the root may be that leaf. \end{enumerate} Then, at every size, \[ D\models\left[(\exists A\,H)\leftrightarrow\bigvee_{i=1}^r(u_i\oplus v_i)\right]. \] A realizing assignment to the auxiliaries can be constructed in time linear in their representation size once a discrepant observed pair is known. \emph{Proof.} If all observed activities are false, unit propagation forces each requirement-tree node false from its children, contradicting the root unit. This establishes condition 1 of Theorem A.1. For condition 2, choose one discrepant observed pair. Set every internal activity false, set its observed leaf and the path to the root true, and set all other observed leaves and off-path tree nodes false. Every clause of type 2 is satisfied by its negative internal premise. Each active tree node has an active child, and the only active discrepancy guard is true by the chosen unequal pair. The assignment is independent of every other signal value, so it is a constant extension under either unequal orientation. The construction visits each auxiliary and tree edge at most a constant number of times. \ensuremath{\square} \textbf{Corollary A.3 (selected observations).} For any nonempty \(J \subseteq \{1,\ldots ,r\}\), append the clause \(\bigvee_{i \in J} s_i\) to the grammar of Theorem A.2 and retain all its clauses. Its exact projection is \(\bigvee_{i \in J} (u_i \oplus v_i)\). \emph{Proof.} The added clause and guards force a discrepancy in \(J\). Conversely, the extension in Theorem A.2 for a discrepant pair in \(J\) satisfies the added clause as well. It imposes no equality on unobserved signal pairs. \ensuremath{\square} Theorem A.2 allows arbitrary numbers of activities and edges. Requiring an internal fault-site activity to become true or to traverse a full path would change its hypotheses. For composition with Algorithm 2, the added clauses must also preserve the exposed selector and qualifier recovery conditions. \textbf{Lemma A.4 (producer recovery).} Suppose the candidate producers contain the intended acyclic producer for every non-root signal and none for a root. Suppose every alternative producer for a signal depends on a proper descendant of that signal in the intended DAG. Starting with the roots, repeatedly select any candidate whose inputs are known and whose output is unknown. This recovers all intended producers, independently of the candidate iteration order. \emph{Proof.} Maintain that known signals contain all their intended ancestors and were computed by their intended producers. An alternative for an unknown signal cannot be ready: its known descendant would already require that signal to be known. Selecting an intended producer preserves the invariant. If any signal remains unknown, the earliest unknown signal in a topological order has a ready intended producer. Thus the process terminates with the entire DAG recovered. \ensuremath{\square} \textbf{Raw-interface candidate count.} Fix an absolute constant maximum clause width \(w\), let \(M\) count input clause occurrences, and let \(g\) be the number of extracted raw gates. Each distinct clause and head produces at most one gate, so \(g\le wM\). The pairing routine emits each unordered gate pair at most once, with at most \(w-1\) common-input choices per pair. A yielded record has three distinct absolute variables for \(U,W,D\): signed alias relaxation cannot separate literals of the same variable. Thus at most one vertex-biconnected alias block can contain all three. Indeed, two distinct maximal vertex-biconnected blocks share at most one vertex; if they shared two, their union would remain connected after any single-vertex deletion and would form one block. Finally there are at most \(g\) driver choices. Clones are collected deterministically, and final deduplication can only reduce the count. The number of yielded records is therefore at most \[ (w-1)\binom{g}{2}g=O(M^3)=O(N^3). \] This argument assumes the alias graph's vertex-biconnected decomposition and consistent signed aliases; inconsistent aliases are rejected. It is a count of yielded candidates, not a bound on the time spent scanning failed candidates, rebuilding aliases or constructing each record. \textbf{Discovery scope.} The implementation restricts local gate supports to five inputs and normalized bridge interfaces to ten variables, rejecting candidates exceeding these limits. These are independent representation restrictions. Discovery uses exposed gate pairs, alias blocks, bounded local tables and selector-factor matches. The native and compact routes use different recovery promises. The compact fallback checks at most three buses; increasing this limit exposes a \(2^{2b}\) local-table factor, while the growing-bus route uses native factor footprints. No complete worst-case discovery-time or space bound is established here. Such a bound requires a schedule accounting for all searches, intermediate representations and failed candidates, together with a precise syntactic class on which discovery is complete. The supplied-record checker proves correctness of accepted records, including exact projection and model lifting; it does not supply that discovery theorem. Condition 2 of Theorem A.1 uses explicit projection evidence, not a general test for arbitrary Boolean definitions. Variable renaming, checked signed aliases and permutations are supported; arbitrary equivalent rewrites may prevent recovery. \textbf{Transfer to the SATLIB anchor.} On the compact \texttt{bf0432-007} encoding, the implementation recovers channel roles and selector recurrences without source names. It abstracts 20 paired guarded signal functions: eight standalone qualifier pairs, eight intermediate guarded expressions and four decoder sinks. The observation projection selects seven discrepancies: four guarded decoder pairs and three bus-flag discrepancies. The signed observation table below is in normalized alias coordinates. For decoder pairs, swapping the listed pair and complementing both entries gives the healthy and faulty instances of the same guarded function. Bus rows identify equality of pair-XOR functions; they do not identify the individual literals with historical PA/PB/PC wires. Bus numbers in this table are one-based. {\def\LTcaptype{none} % do not increment counter \begin{longtable}[]{@{}rll@{}} \toprule\noalign{} Activity literal & Signed pair & Observed function \\ \midrule\noalign{} \endhead \bottomrule\noalign{} \endlastfoot 56 & \((-57, -55)\) & Guarded decoder, replay DAG root 11 \\ 53 & \((-54, -52)\) & Guarded decoder, replay DAG root 15 \\ 50 & \((-51, -49)\) & Guarded decoder, replay DAG root 17 \\ 47 & \((-48, -46)\) & Guarded decoder, replay DAG root 18 \\ 44 & \((-45, -43)\) & Bus-3 healthy/faulty flag discrepancy \\ 41 & \((-42, -40)\) & Bus-2 healthy/faulty flag discrepancy \\ 38 & \((-39, -37)\) & Bus-1 healthy/faulty flag discrepancy \\ \end{longtable} } The implementation handles bus discrepancies directly and applies Algorithm 1 when the observation interface contains only the guarded decoder pairs. The full anchor therefore uses the combined bus-or-decoder route. The main image-based detection theorem retains its qualifier-only observation hypothesis. The signed map and its decoder DAG are retained with the exact CNF hash \nolinkurl{ff22b8c5c381229a7ec7ff2f8d93afc7219a73034c4180b056b8a5594af1a75a}. The replay accounts for all 3,668 clauses and returns UNSAT for the fixed drive-zero anchor. Independent SAT checks of the recovered functional definitions and residual clauses verify 65 projection implications, exclude three impossible orientations and refute the all-observations-equal necessity miter. These projection checks omit the bridge-interface constraints. They establish the finite anchor projection, not a uniform discovery-cost theorem. A separate cofactor-congruence simplifier also refutes it directly. For \texttt{ssa0432-003}, an analogous recognizer applies Theorem 4.4. Its current exposed representation guarantee requires exactly three buses and \(n \ge 2\); the semantic classification of Theorem 4.4 holds at every stated \(n,b\). \begin{center}\rule{0.5\linewidth}{0.5pt}\end{center} \subsection{Appendix B. Native resolution bounds and proof compilation}\label{appendix-b.-native-resolution-bounds-and-proof-compilation} \textbf{Theorem B.1.} Every UNSAT member of the native bridge encoding with guarded decoders has an ordinary DAG-resolution refutation with \(O(N^3)\) inferences and no extension variables. Here the native encoding consists of complete bounded-fan-in gate blocks for Section 3, explicit drive units \(U=1-d,D=W=d\), two identical guarded decoder DAGs, and the asserted OR of their output XORs. There are no extra primary restrictions. Any auxiliary wrapper requires its own proof translation. \emph{Proof.} We separate the selector derivations from decoder reasoning. All local premises are the complete blocks in Section 2; signed wires stand for their native literals. The following elementary expansion rules will be used throughout. \textbf{Local derivation rules.} For an AND tree with root \(a\) and leaves \(l_1,\ldots ,l_s\), resolving down the tree gives every \(\neg a \lor l_j\) and \(a \lor \neg l_1 \lor \ldots \lor \neg l_s\). The dual clauses hold for an OR tree. For a guard chain these give \(\neg a \lor u\), every \(\neg a \lor \neg h_j\), and \(\neg u \lor \bigvee_{j \in B} h_j \lor a\), where \(u\) is its live child. They use existing gate variables and at most linear work per path or combined clause. For a non-tautological requested clause whose falsification gives a unit-propagation contradiction, resolve the final conflict with its reasons in reverse propagation order. This derives a subclause of the request in at most \(O(N)\) inferences. Retain the stronger subclause and omit tautological goals. When a fixed number of correlated gate inputs requires case splitting, branch on those inputs and resolve the resulting constant-size tree. No tautological clause is introduced as an axiom. \textbf{Selector nonemptiness.} First take drive one and restrict to \(P'_1=0\). The interface forces \(e_t=r_{t1}=1\) and every non-target first local request to zero. Write \(p_j=P'_j\), \(z_{ij}=t'_{ij}\), \(g_{ik}=\neg p_k \lor r_{ik}\), and \(H=\bigvee_i h'_i\). The symbols \(g\) and \(h'\) are existing gate outputs; \(H\) below denotes a clause, not a new variable. For \(j\ge 2\), derive \[ \begin{aligned} &\neg z_{ij}\lor g_{ik} &&(k\le j),\\ &\neg z_{ij}\lor p_{j+1}\lor\cdots\lor p_b\lor h'_i,\\ &\neg p_j\lor p_{j+1}\lor\cdots\lor p_b\lor H. \end{aligned} \] For the first clause, assuming \(z_{ij}=1,g_{ik}=0\) forces \(p_k=1\) and \(r_{ik}=0\). The earlier mask then forces the earlier local request true, a contradiction; \(k=j\) uses the direct request factor and \(k=1\) uses \(p_1=0\). These are RUP derivations. The first clauses and zero later flags force every factor of \(h'_i\), giving the second clause. Resolving through the OR tree for \(p_j\) gives the third. Descending induction on \(j\) eliminates the later flags and yields \(\neg p_j \lor H\). The known target enable also gives \(p_2 \lor \ldots \lor p_b \lor H\), since zero suffix flags force \(h'_t\). Resolving these clauses derives \(H\); for one bus it derives \(h'_t\). There are \(O(nb^2)=O(N^2)\) such macro clauses. Each RUP macro expands into at most \(O(N)\) ordinary resolutions along its reason trail. \textbf{Healthy singleton.} The healthy first flag is one. Its non-target first masks are zero, killing every later non-target local contribution. The target mask is one. Inductively, the target's local contribution at stage \(j\) equals \(r_{tj}\), the flag equals that contribution, and the target's next mask is \(r_{tj} \oplus \neg r_{tj}=1\). Each correlation uses only the constant local XOR/OR truth table after preceding identities have been derived. Every target qualifier factor is therefore one. For \(i\ne t\), assuming \(h_i=1\) forces \(e_i=r_{i1}=1\) through its first qualifier factor, contradicting \(x_i=0\) from the interface and first-flag cofactor. Thus derive \(h_t=1\) and \(h_i=0\) for \(i\ne t\), and evaluate the healthy decoder to obtain each \(c_k\). At most \(O(N)\) such gate identities suffice; each identity is represented by its two clause directions, and evaluation then follows the gate order. \textbf{Healthy-one decoder outputs.} If \(c_k=1\), the forward decoder clauses, \(H\), and \(\neg a_{\mathrm{root}}\) form the dual-Horn system of Algorithm 1; add \(h'_t\) for one bus. An UNSAT family member has no detecting set, so this system is inconsistent. Complementing every variable makes it a Horn system. Mark variables true by the propagation of {[}DG84{]}: whenever every negative literal of a clause is marked, mark its positive literal. When this stops, the marked set satisfies every clause that has a positive literal, so an unsatisfiable system contains a clause without one whose variables are all marked. Resolving each fired clause against the units of its negative literals derives its positive literal, and the final clause then yields the empty clause. Each clause is used at most once, so this refutation has at most one inference per literal occurrence. Without the premise \(\neg a_{\mathrm{root}}\), the same inferences derive \(a_{\mathrm{root}}\) or a subclause of it, as in the cofactor lifting below, in \(O(N)\) inferences. Decoder variables here are existing gate outputs. Clauses for a multi-guard node are obtained by resolving along its native AND tree. \textbf{Healthy-zero decoder outputs.} If \(c_k=0\), associate a support \(A_v\) with each faulty decoder node. A channel leaf has support \(\{i\}\), zero has empty support, OR takes unions, and a guard removes its blocked indices. In the one-bus case a guard on \(t\) gives empty support. Derive \[ \neg a_v\lor\bigvee_{i\in A_v}h'_i. \] For a channel leaf the displayed summary is the tautology \(\neg h'_i \lor h'_i\); omit it. At its parent, the definition already contains the leaf literal needed by the summary induction. A constant zero uses its defining negative unit. At OR nodes, resolve the output-to-children clause with nonleaf child summaries, retaining leaf literals directly. At guards, transfer the child summary and remove blocked leaves using \(a_v \to \neg h'_j\); if the child is a leaf, start from \(\neg a_v \lor h'_i\) in the guard definition. A one-bus guard on \(t\) immediately yields \(\neg a_v\) from \(h'_t\). A surviving root leaf supplies a true path for the reachable singleton or target-plus-singleton. Since none detects, \(A_{\mathrm{root}}\) is empty and the summary gives \(\neg a_{\mathrm{root}}\). Shared nodes reuse their summaries. Thus all paired outputs agree, contradicting detection. \textbf{Cofactor assembly and cost.} For drive zero, or drive one with \(P'_1=1\), the first flags agree. Derive equality of corresponding gate outputs in topological order from the common inputs. Bounded fan-in makes each step a constant-size derivation. The two cofactors in drive one lift to complementary clauses and resolve to the empty clause. Assumption discharge and restriction lifting can be made weakening-free: keep the derived subclause whenever a pivot disappears. Equivalently, lifting a refutation under \(P'_1=\varepsilon\) yields a subclause of the complementary literal. Either it is empty already, or the two cofactor literals resolve to the empty clause. The selector, decoder summaries and equality steps fit \(O(N^2)\) macros, each costing at most \(O(N)\) resolutions. There are only two global cofactors. This proves the inference bound; total derived literal occurrences are at most \(O(N^4)\). Encoded proof size and compiler running time require separate accounting; neither is identified with the cubic inference count. \ensuremath{\square} \textbf{Theorem B.2 (native core with optional observations).} Retain the native physical core, drive interface and paired guarded decoders of Theorem B.1, replacing its final observation assertion by the wrapper of Theorem A.2. Observed pairs are decoder outputs. Every UNSAT such formula has an ordinary-resolution refutation using \(O(N_0^3+L_H)\) inferences and no extension variables. Here \(N_0\) counts the native core and observed output incidences, and \(L_H\) counts the wrapper. The selected-observation variant of Corollary A.3 has the same bound. \emph{Proof.} Observation projection makes an UNSAT wrapper equivalent to the absence of any accepted output discrepancy. Fix a native cofactor. When the first flags agree, gate congruence derives output agreement from the common inputs. In the differing cofactor, the physical clauses derive the healthy singleton and faulty nonemptiness, with \(h'_t\) in the one-bus case. For a healthy-one accepted output, its zero system is inconsistent: otherwise Theorem 4.1 would realize a detecting input. Unit resolution and discharge of the zero-root assumption therefore derive the faulty root true. For a healthy-zero accepted output, the support-summary argument of Theorem B.1 gives empty root support and derives the faulty root false. Healthy evaluation supplies the matching unit in each case. These derivations use only native physical and decoder clauses within the cofactor, before any observation clause is used. They establish equality of each accepted output pair, or stronger subclauses, within the stated cubic budget. In Corollary A.3, this argument is applied only to selected outputs; unselected outputs may still differ. For an output pair \((u,v)\) with equality clauses \(\neg u \lor v\) and \(u \lor \neg v\), and activity \(s\), resolve its discrepancy clauses \(\neg s \lor u \lor v\) and \(\neg s \lor \neg u \lor \neg v\) against these equalities. Two resolutions give \(\neg s \lor v\) and \(\neg s \lor \neg v\); a third gives \(\neg s\). Propagate these units through the requirement tree with two resolutions per internal node, then against its positive root unit. For \(q\) leaves this suffix has at most \(3q+2(q-1)+1=5q-1\) inferences after the equality clauses; an identical-wire pair needs only its guard clauses to derive the negative activity. In the selected variant, resolve the selected negative activities against the added disjunction instead. For a weakening-free construction, append the same suffix inside each native cofactor, use stronger subclauses whenever a resolution pivot disappears, and lift the two resulting refutations as in Theorem B.1. The constant number of cofactors changes only the constant in \(O(L_H)\). Internal optional-activity clauses need not be used, so their arbitrary connectivity, including cycles, causes no additional proof cost. \ensuremath{\square} This theorem requires the native core variables and definitions. It does not establish a simulation for compact physical rewrites eliminating those wires. The finite suffix check validates its new local resolutions; it does not constitute an implementation of a general wrapper compiler. By {[}PD11{]}, CDCL with restarts polynomially simulates resolution, so the family has no proof-length separation from CDCL. That does not mean a fixed solver heuristic finds the proof. The SATLIB anchors have checked ordinary refutations of 12,100 inferences (\texttt{bf0432-007}) and 887 inferences (\texttt{ssa0432-003}). \textbf{Executable answer certificates.} The certified entry point runs the structural solver and requires independent validation before returning SAT or UNSAT. SAT certificates contain a complete assignment. The native proof compiler implements Theorem B.1 using gate congruence, last-active-bus induction, guarded-decoder summaries, and the two first-flag cofactors. It uses no SAT solver. Correlated gate identities split on at most five local inputs; all assumptions are discharged into proved clauses. Shared physical DAGs are traversed with memoization rather than unfolded into paths. A supplied native circuit description is checked against every original clause, or the exposed-wrapper recognizer recovers the roles. Aliases and projected observation units are themselves derived. The compiler emits ordinary resolution over the original clauses and variables. The checker uses only Python's standard library: it verifies the input and proof hashes, every signed pivot and exact binary resolvent, and the final empty clause. It imports neither the recognizer nor a SAT solver and uses explicit validation that remains active under \texttt{python\ -O}. No extension variables are accepted. The native compiler's schedule has \(O(N^2)\) macros, each with a constant local case tree and \(O(N)\) resolution expansion. It therefore realizes the \(O(N^3)\) inference and \(O(N^4)\) literal-storage bounds. These are proof-size bounds. For propagation, the active database contains the original clauses and completed lemma conclusions, including the constant-size local case trees: \(O(N^2)\) clauses of width at most \(O(N)\). Intermediate resolution clauses are stored in the proof DAG and are not automatically activated. Each RUP check initially scans the active database, then revisits a clause only when one of its literals becomes false. Each literal can trigger this revisit once, so a clause is inspected at most \(O(N)\) times, at \(O(N)\) literal cost per inspection. One check therefore costs at most \(O(N^4)\), and \(O(N^2)\) checks give a conservative \(O(N^6)\) kernel allowance with constant-cost hash operations. This is a word-operation allowance, not an unconditional worst-case bound for Python hashing; recognition is charged separately. The Python native compiler and its input-format documentation are not included in this source archive; the selected Lean resolution results are available through the records in Section 13. Structural-only certification uses this compiler and returns OPEN on unsupported representations. Automatic mode can instead use a bounded Glucose3 run, expanded from RUP into ordinary resolution, for compact or other recognized representations outside the native compiler. That fallback has no polynomial proof-discovery guarantee. If proof production exceeds its budget or checking fails, the entry point returns OPEN. Answer certification and independent verification of recovered family membership remain separate contracts. \begin{center}\rule{0.5\linewidth}{0.5pt}\end{center} \subsection{Appendix C. Finite validation and certificate controls}\label{appendix-c.-finite-validation-and-certificate-controls} \textbf{Correctness checks.} These were run on the reference implementation; the evidence is listed in Section 13. \begin{itemize} \tightlist \item 17 exhaustive reachability checks on small circuits. \item 200 random guarded decoders, with 4,162 eligible-set rows and 1,200 fixed points. \item All 512 qualifier assignments of the c432 decoder. \item 86 complete generated CNFs (32 SAT, 54 UNSAT) up to 16 channels, 32 buses, and 22,820 variables. Every SAT model was checked against every clause. \item 494 unique-set decoders. \item 138 compact-composition cases. \item 336 translated formulas for the NP-completeness reduction. \end{itemize} The separate extension module checks the constructions against exhaustive Boolean evaluation. The deterministic seed is \texttt{20261009}: \begin{itemize} \tightlist \item All 1,094 nonempty simple graphs on two through five vertices: 33,804 set evaluations confirm the exact graph-cover bijection, counts and minima. \item 250 dual-Horn inputs, including units, tautologies and empty clauses: 1,890 assignment rows confirm Proposition 5.2. \item 400 bitset, 400 formula-forest and 400 bounded-AND decision checks, compared with exhaustive evaluation over 22,698 reachable-set rows; 1,200 additional checks of sparse zero-output compilation. \item 13,932 rows check the guarded-expansion identity on random DAGs with at most three live ANDs; a fixed two-leaf conjunction requires the predicted nonsingleton witness. Four malformed/out-of-scope decoder controls reject. \item Seven native CNFs from the graph and dual-Horn generators (five SAT, two UNSAT) agree with the existing recognizer, MiniSat and Glucose. All 15 SAT models satisfy every clause. Both UNSAT inputs also have independently replayed ordinary resolution proofs with no extension variables. The graph restriction used in Theorem 6.9 is checked on all 28 enable assignments for three small graphs. An unexplained primary restriction is rejected by the recognizer. \end{itemize} These finite checks exercise the semantic algorithms and the native embedding. They do not test an exponential DNNF lower bound empirically. The extension kernels take supplied DAG roles; they are separate from the native recognizer used for the timing panel in Section 9. \textbf{Certificate checks.} The certified entry point checks four generated SAT models and ten generated UNSAT refutations, covering one, three and five buses, both drives, auxiliary chains, and a signed variable renaming. The UNSAT proofs have 16 to 33,321 resolution inferences. Both SATLIB anchors also pass through the certified dispatch. Out-of-scope input and a forced proof timeout return OPEN. The standalone checker passes 21 controls, including rejection of 18 corrupted proofs, models or bindings; every control is repeated with Python assertions disabled. These checks establish the reported executable behavior, while the correctness theorem remains the argument in Sections 4--7 and Appendices A--B. \textbf{Native structural proof compilation.} A separate suite checks 80 native CNFs: 48 UNSAT refutations and 32 SAT models, all agreeing with MiniSat. Fifty-six drive-one answers are also compared with exhaustive reachable-set evaluation; 19 use the drive-zero rule and five larger chain instances use the family theorem. The suite includes 48 seeded guarded DAGs, shared nodes, overlapping guards, multiple outputs and driver channels, both drives, and signed renaming. Channel and bus counts grow independently, up to 64 channels and 16 buses. The emitted refutations contain 9 to 24,767 inferences. Every producer runs with SAT library imports blocked, and every certificate is replayed with Python assertions disabled. The 14 exposed-wrapper inputs also pass through the compiler. Additional controls check five-input gates, depth 2,200, and Fibonacci DAG sharing; malformed records, two live children and extra primary restrictions return OPEN. These finite checks validate the tested proofs; the uniform inference bound follows from the construction. \textbf{Gate-basis and parameterized-boundary checks.} \texttt{check\_decoder\_complexity\_boundary.py} checks Theorems 7.5--7.6 through independent graph and truth-table oracles. It exhausts all labeled graphs with edges only between color classes of sizes (1), (2), (1,1), (1,2), (2,2), (1,1,1), (1,2,2), and (2,2,2): 4,384 graphs in total. For every graph it tests every target-containing eligible set, giving 270,702 graph/set pairs. All detecting sets match the clique bijection. The existing bounded-AND algorithm agrees in 8,768 decisions across one and two buses. A further 146 decisions check the ordinary-to- colored Clique reduction. The suite also checks all seven proper gate bases on 1,680 generated decisions against 29,328 reachable truth-table rows, plus explicit boundary and rejection controls. On 24 native controller CNFs, MiniSat and Glucose agree with the graph oracle in every case (16 SAT, 8 UNSAT). Each solver's SAT model satisfies every original clause, and every supplied-DAG SAT witness also has a clause-checked native realization with its faulty qualifiers fixed. The native proof compiler's guarded scope is unchanged. These finite checks validate the constructions and algorithms; the hardness and asymptotic bounds follow from the reductions above. \subsection{Appendix D. Compatible paths and zero constraints}\label{appendix-d.-compatible-paths-and-zero-constraints} This appendix studies the simultaneous cofactor test in Theorem 7.9. All algorithms receive their guarded DAGs and constraints explicitly. \subsubsection{D.1. Limits of two immediate shortcuts}\label{d.1.-limits-of-two-immediate-shortcuts} For \(F=(s \land \neg p) \lor (s \land \neg q \land \neg t)\), the set \(K=\{s,p\}\) distinguishes the target cofactors, but the empty set and every non-target singleton do not. The greatest zero model of \(F_1=s \land \neg p\) sets all of \(s,p,q\) true, where \(F_0\) is also zero. Thus neither singleton testing nor evaluating only the greatest zero model decides the simultaneous condition. \textbf{Proposition D.1 (an exact dual-Horn projection obstruction).} A stuck-at discrepancy relation of an unshared guarded formula need not have a dual-Horn CNF representation on the same channel variables, even with existential auxiliary variables. \emph{Proof.} Take \[ \begin{aligned} Q={}&(s\land\neg p\land\neg q)\\ &\lor(s\land\neg p\land\neg t)\\ &\lor(s\land\neg q\land\neg t). \end{aligned} \] Its discrepancy relation is \(s \land (p \oplus q)\). The sets \(\{s,p\}\) and \(\{s,q\}\) belong to it but their union does not. Models of a dual-Horn formula are closed under coordinatewise union: for a clause with a negative literal, a union making its variable true contains a constituent model making that variable true, which supplies a positive literal. Positive-only clauses are preserved as well. Existential projection preserves this property by taking the union of two satisfying extensions. The discrepancy relation therefore has no such representation. \ensuremath{\square} The obstruction concerns an exact representation of all witnesses on these coordinates. It does not exclude decision reductions, several Horn queries, or other algorithms. \subsubsection{D.2. Branching on multi-positive zero clauses}\label{d.2.-branching-on-multi-positive-zero-clauses} Let \(C\) be a guarded DAG, with target value \(v\) on the true side, and let \(Z\) be an explicitly supplied dual-Horn system on the channels and private auxiliary variables, with its target fixed to \(1-v\). Compatibility asks for a non-target channel set \(K\) such that \(C_v(K)=1\) and \(K\) extends to a model of \(Z\); nonemptiness of \(K\) may additionally be required. The two copies share only the non-target channels. For detection use the opposite cofactor's exact zero system as \(Z\). Let \(G\) include the channel count, all nodes and incidences of \(C\), and all variables and literal incidences of \(Z\). Normalize duplicate literals and remove tautological clauses. Let \(k\) count its clauses with at least two positive literals, and let their positive-literal counts be \(d_1,\ldots ,d_k\). Set \(D=\prod_i d_i\), with empty product one. Auxiliary activity literals count toward these parameters. \textbf{Theorem D.2 (few multi-positive clauses).} Compatibility is decidable, with a witness, in \(O(D(n+1)G)\) time and \(O(G)\) working words. If every \(d_i\le d\), this is \(O(d^k(n+1)G)\). For full single-output stuck-at detection, the costs of the two directions add. \emph{Proof.} An empty clause immediately rejects. For each multi-positive clause use the identity \[ (\neg a\lor b_1\lor\cdots\lor b_d)=\bigvee_j(\neg a\lor b_j). \] For a positive-only clause use the corresponding choice of a positive unit. Distributing the choices across clauses expresses the system as an existential choice of \(D\) strengthened systems. A branch implies \(Z\). Every model of \(Z\) satisfies a branch: choose a true positive when \(a\) is true, and any positive when \(a\) is false. Keeping the negative literal is essential in the latter case. Stream these choices rather than materializing their disjunction. Every strengthened system consists of units and implications \(\neg a \lor b\). Draw an edge \(b \to a\) for propagation of false values. Let \(S\) contain negative-unit variables and \(R\) positive-unit variables, including the opposite target fixing. Write \(\operatorname{Reach}(X)\) for the vertices reachable from \(X\), including \(X\). Added negative units \(B\) and positive units \(H\) are consistent exactly when \[ \operatorname{Reach}(S\cup B)\cap(R\cup H)=\varnothing. \] Necessity follows by propagation; for sufficiency set exactly the complement of the reachability set true. This satisfies every implication and unit and is the greatest model. Reject any branch with \(\operatorname{Reach}(S) \cap R\) nonempty. For a candidate non-target head \(s\), take \(H=\{s\}\). Reject it if the base closure reaches a required positive. A reverse traversal from \(R \cup H\) computes all variables \(U\) whose falsification would force a required positive false. Delete every guard node containing a non-target guard in \(U\). Treat target guards according to \(v\), independently of the opposite target coordinate. A topological traversal then determines whether the root has a path to a leaf labelled \(s\). This deletion is exact because graph reachability is additive: \(\operatorname{Reach}(S \cup B) = \operatorname{Reach}(S) \cup \bigcup_{j \in B} \operatorname{Reach}(\{j\})\). Any surviving path's guard units are consistent with the required head and the binary system. Recover the path, propagate its negative units, and take the greatest model to construct \(K\). A true target leaf is a constant terminal, permitted only when \(v=1\). If nonemptiness is required, for each non-target channel \(s\) require it true and allow either leaf \(s\) or that constant terminal. Every nonempty constant-terminal witness supplies such an \(s\). If empty \(K\) is permitted, add one pass with \(H\) empty and only the constant terminal allowed. Thus at most \(n+1\) traversals suffice per branch. An existing compatible model selects a strengthened branch and a support path surviving the appropriate pass, proving completeness. Soundness follows from the recovered path and its model of the strengthened system. Each traversal and witness reconstruction costs \(O(G)\). Branches and heads are processed sequentially, with \(O(G)\) working storage. \ensuremath{\square} This is fixed-parameter tractable in \((k,d)\), and in \(k\) for fixed \(d\). With unbounded \(d\le G\) it supplies an XP bound in \(k\). Equivalently, \(r=\sum_i\lceil\log_2 d_i\rceil\) gives the bound \(O(2^r(n+1)G)\). Nonemptiness is handled by candidate enumeration and need not be charged as an extra wide clause. For two cofactors with products \(D_0,D_1\), full detection costs \(O((D_0+D_1)(n+1)G)\); a cheap direction alone is insufficient when it finds no witness. The case \(k=0\) is a binary implication system with units, a stricter condition than dual-Horn 2-CNF, which can contain positive clauses of size two. It is also stricter than unary channel guards: the zero encoding of a unary guard is \(\neg a_{\mathrm{child}} \lor h_{\mathrm{guard}} \lor a_{\mathrm{parent}}\), with two positive literals. For example, requiring \((s \land \neg p) \land \neg q\) to be zero forces \(s\) false when both \(p\) and \(q\) are false, but not when only one is false. Unary guards therefore do not imply additive closure. \subsection{AI assistance}\label{ai-assistance} OpenAI Codex assisted with mathematical exploration, Lean formalization, and manuscript preparation. The author reviewed the AI-assisted material and takes full responsibility for the manuscript. \subsection{References}\label{references} \begin{itemize} \tightlist \item {[}Sha26a{]} I. A. Shaik. Exact fault images in priority controllers. Lean 4 formalization, Palomar Registry, PALOMAR-2026-10-19-000010, version 1, 2026. \href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-19-000010&version=1}{Immutable registry record}. \item {[}Sha26b{]} I. A. Shaik. Guarded detection and constrained eligible-set extensions. Lean 4 formalization, Palomar Registry, PALOMAR-2026-10-19-000014, version 1, 2026. \href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-19-000014&version=1}{Immutable registry record}. \item {[}Sha26c{]} I. A. Shaik. Canonical streaming enumeration of eligible detections. Lean 4 formalization, Palomar Registry, PALOMAR-2026-10-19-000016, version 2, 2026. \href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-19-000016&version=2}{Immutable registry record}. \item {[}Sha26d{]} I. A. Shaik. Forest detection and attained healthy-zero maximum weight. Lean 4 formalization, Palomar Registry, PALOMAR-2026-10-20-000013, version 1, 2026. \href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-20-000013&version=1}{Immutable registry record}. \item {[}Sha26e{]} I. A. Shaik. Dual-Horn models and vertex covers in priority controllers. Lean 4 formalization, Palomar Registry, PALOMAR-2026-10-20-000015, version 1, 2026. \href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-20-000015&version=1}{Immutable registry record}. \item {[}Sha26f{]} I. A. Shaik. Critical recovery, query lower bounds and binary-native width. Lean 4 formalization, Palomar Registry, PALOMAR-2026-10-22-000011, version 1, 2026. \href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-22-000011&version=1}{Immutable registry record}. \item {[}Sha26g{]} I. A. Shaik. Bounded conjunction and proper-basis algorithms. Lean 4 formalization, Palomar Registry, PALOMAR-2026-10-21-000014, version 1, 2026. \href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-21-000014&version=1}{Immutable registry record}. \item {[}Sha26h{]} I. A. Shaik. Ordinary resolution for native encodings and observation wrappers. Lean 4 formalization, Palomar Registry, PALOMAR-2026-10-21-000016, version 1, 2026. \href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-21-000016&version=1}{Immutable registry record}. \item {[}BCMS15{]} S. Bova, F. Capelli, S. Mengel, F. Slivovsky. A strongly exponential separation of DNNFs from CNF formulas. arXiv:1411.1995v3, revised 19 February 2015. \href{https://arxiv.org/pdf/1411.1995v3}{Author paper, Theorems 4--5}. \item {[}CAB90{]} S. Chakradhar, V. Agrawal, M. Bushnell. Polynomial time solvable fault detection problems. FTCS 1990. \item {[}CHKX06{]} J. Chen, X. Huang, I. A. Kanj, G. Xia. Strong computational lower bounds via parameterized complexity. JCSS 72(8), 1346--1367, 2006. \href{https://www.cs.lafayette.edu/~gexia/research/jcss72_8.pdf}{Author manuscript, Theorems 4.5 and 5.5}. \item {[}DG84{]} W. Dowling, J. Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Logic Programming 1(3), 1984. \item {[}DGS14{]} B. Dilkina, C. P. Gomes, A. Sabharwal. Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search. Annals of Mathematics and Artificial Intelligence 70, 399--431, 2014. \href{https://www.cs.cornell.edu/gomes/pdf/2014_dilkina_amai_dynamic.pdf}{Paper}. \item {[}FL91{]} F. J. Ferguson, T. Larrabee. Test pattern generation for realistic bridge faults in CMOS ICs. ITC 1991. \item {[}FT82{]} H. Fujiwara, S. Toida. The complexity of fault detection problems for combinational logic circuits. IEEE Trans. Computers C-31(6), 1982. \item {[}Fri73{]} A. D. Friedman. Easily testable iterative systems. IEEE Trans. Computers C-22(12), 1973. \item {[}Fuj90{]} H. Fujiwara. Computational complexity of controllability/observability problems for combinational circuits. IEEE Trans. Computers 39(6), 1990. \item {[}GHR95{]} R. Greenlaw, H. J. Hoover, W. L. Ruzzo. Limits to Parallel Computation: P-Completeness Theory. Oxford University Press, 1995. \href{https://homes.cs.washington.edu/~ruzzo/papers/limits.pdf}{Author copy, Theorem 6.2.2 and proof}. \item {[}Gol77{]} L. M. Goldschlager. The monotone and planar circuit value problems are log space complete for P. ACM SIGACT News 9(2), 25--29, 1977. \href{https://doi.org/10.1145/1008354.1008356}{Paper}. \item {[}HH95{]} M. C. Hansen, J. P. Hayes. High-level test generation using symbolic scheduling. ITC 1995. \item {[}HLW06{]} S. Hoory, N. Linial, A. Wigderson. Expander graphs and their applications. Bulletin of the AMS 43(4), 439--561, 2006. \href{https://www.cs.huji.ac.il/~nati/PAPERS/expander_survey.pdf}{Author paper, Construction 8.1 and Theorem 8.2}. \item {[}HYH99{]} M. C. Hansen, H. Yalcin, J. P. Hayes. Unveiling the ISCAS-85 benchmarks: a case study in reverse engineering. IEEE Design \& Test 16(3), 1999. \href{https://tumbleweed.nu/r/iscas.restore/doc/trunk/c432b.v}{Author behavioral model}. \item {[}IA96{]} M. A. Iyer, M. Abramovici. FIRE: a fault-independent combinational redundancy identification algorithm. IEEE Trans. VLSI 4(2), 1996. \item {[}IMS19{]} A. Ignatiev, A. Morgado, J. Marques-Silva. RC2: An efficient MaxSAT solver. Journal on Satisfiability, Boolean Modeling and Computation 11(1), 53--64, 2019. \href{https://pysathq.github.io/docs/html/api/examples/rc2.html}{Implementation and documentation}. \item {[}IS75{]} O. Ibarra, S. Sahni. Polynomially complete fault detection problems. IEEE Trans. Computers C-24(3), 1975. \item {[}Ima21{]} G. E. Imaz. The Horn non-clausal class and its polynomiality. arXiv:2108.13744, 2021. \item {[}Kar72{]} R. M. Karp. Reducibility among combinatorial problems. In \emph{Complexity of Computer Computations}, 85--103, 1972. \href{https://doi.org/10.1007/978-1-4684-2001-2_9}{Paper}. \item {[}Kin92{]} N. G. Kinnersley. The vertex separation number of a graph equals its path-width. IPL 42(6), 1992. \item {[}Lar92{]} T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Trans. CAD 11(1), 1992. \item {[}Li05{]} J.-F. Li. Testing priority address encoder faults of content addressable memories. ITC 2005. \item {[}OSS24{]} S. Ordyniak, A. Schidler, S. Szeider. Backdoor DNFs. JCSS 144, Article 103547, 2024. \href{https://doi.org/10.1016/j.jcss.2024.103547}{Published paper}. \item {[}PB83{]} J. S. Provan, M. O. Ball. The complexity of counting cuts and of computing the probability that a graph is connected. SIAM Journal on Computing 12(4), 777--788, 1983. \href{https://doi.org/10.1137/0212053}{Paper}. \item {[}PCK99{]} M. R. Prasad, P. Chong, K. Keutzer. Why is ATPG easy? DAC 1999. \item {[}PD11{]} K. Pipatsrisawat, A. Darwiche. On the power of clause-learning SAT solvers as resolution engines. AIJ 175, 2011. \item {[}Sha26B{]} I. A. Shaik. Guarded Reachability: Algorithms, Conditional Bounds, and Selector Costs. Manuscript, 2026. \item {[}Sha26C{]} I. A. Shaik. Explicit and Compact Guarded Factors: Interaction Graphs and Shared Interfaces. Manuscript, 2026. \item {[}Sha26S{]} I. A. Shaik. Structural SAT Algorithms and Resolution: Companion Results. Technical note, 2026. \item {[}Sha26U{]} I. A. Shaik. What Decides SATLIB? A Certified Structural Audit and an Exact Tractable Family of Priority-Controller Fault Formulas. Research manuscript, 2026. \item {[}WHH14{]} N. Wetzler, M. J. H. Heule, W. A. Hunt, Jr.~DRAT-trim: Efficient checking and trimming using expressive clausal proofs. SAT 2014, LNCS 8561, 422--429. \href{https://www.cs.utexas.edu/~marijn/publications/drat-trim.pdf}{Author paper, Sections 1--3}. \end{itemize} \end{document}