Operator-Level Boolean Computation with Correspondence Matrices

   1 \documentclass[10pt]{article}
   2 
   3 \usepackage[letterpaper,margin=0.86in]{geometry}
   4 \usepackage{amsmath,amssymb,amsthm,mathtools}
   5 \usepackage{booktabs,tabularx,array,multirow}
   6 \usepackage{microtype}
   7 \usepackage{enumitem}
   8 \usepackage{listings}
   9 \usepackage{xcolor}
  10 \usepackage{hyperref}
  11 \usepackage{url}
  12 \usepackage{fancyhdr}
  13 \usepackage{graphicx}
  14 \usepackage{float}
  15 \usepackage{tikz}
  16 \usetikzlibrary{arrows.meta,positioning,fit}
  17 
  18 \definecolor{accent}{HTML}{234A73}
  19 \definecolor{soft}{HTML}{F4F6F8}
  20 \definecolor{rulegray}{HTML}{D7DCE2}
  21 \hypersetup{colorlinks=true,linkcolor=accent,citecolor=accent,urlcolor=accent,pdftitle={Operator-Level Boolean Computation with Correspondence Matrices},pdfauthor={Brian Theory}}
  22 \setlength{\parindent}{1.05em}
  23 \setlength{\parskip}{0pt}
  24 \setlist{nosep,leftmargin=*}
  25 \pagestyle{fancy}
  26 \fancyhf{}
  27 \fancyhead[L]{\small Operator-Level Boolean Computation with Correspondence Matrices}
  28 \fancyhead[R]{\small Semantic audit, 13 October 2026}
  29 \fancyfoot[C]{\thepage}
  30 \setlength{\headheight}{14pt}
  31 \emergencystretch=2em
  32 
  33 \newcommand{\B}{\mathbb B}
  34 \newcommand{\Ftwo}{\mathbb F_2}
  35 \newcommand{\bxor}{\mathbin{\Updownarrow}}
  36 \newcommand{\ptop}[1]{\widehat{#1}}
  37 \newcommand{\Pair}{\operatorname{Pair}}
  38 \newcommand{\supp}{\operatorname{supp}}
  39 \newcommand{\eval}{\mathcal E}
  40 \newcommand{\IR}{\mathrm{IR}}
  41 \newcommand{\AST}{\mathrm{AST}}
  42 \newcommand{\true}{\mathrm{T}}
  43 \newcommand{\false}{\mathrm{F}}
  44 
  45 \theoremstyle{plain}
  46 \newtheorem{theorem}{Theorem}
  47 \newtheorem{lemma}{Lemma}
  48 \newtheorem{proposition}{Proposition}
  49 \theoremstyle{definition}
  50 \newtheorem{definition}{Definition}
  51 \theoremstyle{remark}
  52 \newtheorem{remark}{Remark}
  53 
  54 \lstset{
  55   basicstyle=\ttfamily\small,
  56   backgroundcolor=\color{soft},
  57   frame=single,
  58   rulecolor=\color{rulegray},
  59   columns=fullflexible,
  60   keepspaces=true,
  61   breaklines=true,
  62   xleftmargin=0.5em,
  63   xrightmargin=0.5em,
  64   aboveskip=0.7em,
  65   belowskip=0.7em
  66 }
  67 
  68 \title{\vspace{-1.3em}\textbf{Operator-Level Boolean Computation with Correspondence Matrices}\\[0.35em]
  69 \large Typed operand frames, local operator folding, fallback semantics, and empirical boundaries}
  70 \author{Brian Theory}
  71 \date{Compiler contract and evidence revision --- 26 September 2026\\Semantic-boundary addition and audit --- 13 October 2026}
  72 
  73 \begin{document}
  74 \maketitle
  75 
  76 \begin{abstract}
  77 Correspondence matrices encode a binary Boolean connective as four bits in a declared operand frame. We specify a restricted compiler that normalizes signed and swapped variable occurrences, fuses tokens with matching frames, and distinguishes structural, tabulated, and hybrid derivations. An ordered strategy selects among those admissible derivations; failure of the selected strategy need not mean that no derivation exists. Soundness and completeness for an explicitly generated structural fragment are established using classical truth-function identities. The implementation contract separates syntactic variable occurrence from essential dependence, root pair success from discarded child constructions, and compact tokens from dense outputs over retained ambient axes. A pinned source snapshot and executable regression suite make these boundaries checkable. Recovered S1/S2 records show local reductions but a generic-optimizer tie; a separate ANF-dispatch study is negative overall. A prospectively frozen synthetic pair-token comparison on 64 held-out signed formulas also fails its primary utility rule: median direct-packed/CM production time is 0.248 (95\% hierarchical bootstrap interval 0.246--0.249). A separate correctness screen of 71 admitted original EPFL primary-output cones found four pure structural roots, one fully retabulated root, and 66 fallbacks. In a subsequently frozen descriptive secondary timing run, 70 cones completed paired full-bitset Python timing and one failed calibration; the complete-case median direct-packed/CM producer ratio was 0.0376, with direct evaluation faster on every complete case. ABC/AIG truth checking completed for all 71, but its subprocess wall time is not a matched producer comparison. The broader protocol-v3 systems comparison remains open. The contribution is a bounded compiler specification and reproducible negative systems boundary, not a new truth-table algebra or a demonstrated performance advantage.
  78 
  79 \end{abstract}
  80 
  81 \noindent\textbf{Draft status.} This is the revised compiler-focused manuscript after the deliberate CM/LM publication split. The companion foundations paper \emph{Correspondence and Logical Matrices: A Boolean Operator Calculus} owns the formula-valued LM theory, valuation, logical pairing, higher-arity tensors/maps, and the broader coherence calculus \cite{TheoryFoundations2026}. The present paper imports only the numeric binary contract required by the compiler. A narrower synthetic protocol-v4 confirmation is complete and negative. A natural-circuit admission/correctness gate and a separate, incomplete descriptive secondary timing run have since completed; the full timed protocol-v3 comparison has not.
  82 
  83 \section{Introduction and claim boundary}
  84 
  85 A binary Boolean connective contains four output values. A correspondence matrix stores those four values as a $2\times2$ array whose row and column axes are tied to declared operands. In isolation, that is only a reshaping of a truth table. The computational question is different: can a compiler use the small operator as a first-class token, normalize the token's operand frame, and combine compatible local operators before evaluating or expanding their operands?
  86 
  87 The key example is deliberately simple. Consider
  88 \begin{equation}
  89  (X\Rightarrow Y)\bxor(Y\Rightarrow X).
  90  \label{eq:mismatch-expression}
  91 \end{equation}
  92 Both inner connectives are implication, but they do not initially refer to the same ordered operand frame. Treating their four-bit arrays as if corresponding entries described the same assignment would be a type error. Once the second occurrence is transported from frame $(Y,X)$ to frame $(X,Y)$ by transpose, entrywise XOR is sound:
  93 \begin{equation}
  94  [\Rightarrow]\,\ptop{\bxor}\,[\Rightarrow]^T=[\bxor].
  95  \label{eq:mismatch-fold}
  96 \end{equation}
  97 The resulting token represents $X\bxor Y$. Equation~\eqref{eq:mismatch-fold} is not important because XOR of two truth tables is difficult; it is important because it makes the \emph{admission condition} explicit. A local table may be fused only when its coordinates have a common logical meaning.
  98 
  99 This paper therefore treats operand-frame metadata as part of the compiler type. A successful pair compilation returns not just four bits, but a token tied to canonical row and column operands. Swaps and input polarities are normalized by fixed reindexings. Compatible tokens can then be fused by an outer Boolean connective before repeated operand work or polynomial expansion. If structural recognition fails, the implementation can exactly retabulate an admitted two-variable subtree, can combine such a retabulated descendant with structural parents while marking the result hybrid, or can pass the original expression to the ordinary builder. Successful child pair constructions are not retained when the root pair attempt fails.
 100 
 101 The component operations have substantial prior art. Boolean matrices predate this work \cite{Edwards1972}; matrix and vector logics represent logical operators algebraically \cite{Stern1988,Mizraji1992,Mizraji2008}; Cheng, Zhao, and Xu explicitly combine truth vectors entrywise under an arbitrary outer Boolean operation \cite{Cheng2011}; small truth functions, NPN transformations, LUTs, and DAG-aware rewriting are standard synthesis techniques \cite{Mishchenko2006,Zhou2019,Testa2019}; and bit-parallel evaluators compute several assignments simultaneously \cite{Lee2022}. Bricken's internally dated 1997 technical note is also a close antecedent for $2\times2$ logical matrices and bra--matrix--ket evaluation \cite{Bricken1997}. The present paper does not claim those ingredients as new.
 102 
 103 The narrower contribution is computational and testable:
 104 \begin{enumerate}
 105   \item a \textbf{typed frame-aware compiler rule} in which a four-bit CM token is paired with operand metadata and normalized before same-frame fusion;
 106   \item \textbf{sound multi-path semantics} separating pure structural compilation, local retabulation, hybrid composition, and ordinary fallback;
 107   \item an \textbf{executable implementation contract} separating compact tokens, framed surrogates, general IR, lowered programs, and ambient dense outputs, with regression tests for strategy selection, fixed axes, and discarded child constructions;
 108   \item \textbf{matched mechanism and negative evidence}: exploratory folding can reduce pre-expansion work, an equally capable generic optimizer can reproduce the same reductions, and frozen ANF-dispatch and synthetic pair-token studies show that local wins need not amortize; and
 109   \item a \textbf{preserved broader evaluation design} with natural admission, correctness, and bounded secondary producer timing now checked, while synthesis comparability, reuse, alternative outputs, memory, and fallback costs still require matched measurement.
 110 \end{enumerate}
 111 
 112 The scientific claim does not depend on CM folding being uniquely capable of a reduction. If a generic local truth-function optimizer reaches the same reduced form, that locates the mechanism in a broader family of small-function rewrites. The remaining CM-specific question is whether the representation and its frame metadata make recognition, legality, transformation, caching, or reuse sufficiently direct and inexpensive to matter in a full compiler.
 113 
 114 \section{Minimal CM compiler contract}
 115 \label{sec:minimal-contract}
 116 
 117 The companion foundations paper develops the CM/LM calculus in detail \cite{TheoryFoundations2026}. Only the following binary numeric contract is required here.
 118 
 119 Let
 120 \begin{equation}
 121  \B=\{0,1\}\cong\Ftwo,
 122 \end{equation}
 123 with multiplication interpreted as conjunction and addition written as XOR, $\bxor$. For a bit $x\in\B$, use the true-first state
 124 \begin{equation}
 125  |x\rangle=\begin{bmatrix}x\\ \neg x\end{bmatrix},
 126  \qquad
 127  \langle x|=\begin{bmatrix}x&\neg x\end{bmatrix}.
 128  \label{eq:state}
 129 \end{equation}
 130 For a binary logical connective variable $\Theta$, define the compact correspondence matrix
 131 \begin{equation}
 132  [\Theta]
 133  :=
 134  \begin{bmatrix}
 135   \Theta_{11}&\Theta_{10}\\
 136   \Theta_{01}&\Theta_{00}
 137  \end{bmatrix}
 138  =
 139  \begin{bmatrix}
 140   1\Theta1&1\Theta0\\
 141   0\Theta1&0\Theta0
 142  \end{bmatrix}.
 143  \label{eq:cm}
 144 \end{equation}
 145 The row and column assignment order $(1,0)$ is part of the representation contract.
 146 
 147 For $C\in\B^{2\times2}$, define the XOR--AND contraction
 148 \begin{equation}
 149  \eval_C(x,y)=\langle x|C|y\rangle
 150  =\mathop{\bxor}_{r,s\in\{1,0\}}
 151  \chi_x(r)\wedge C_{rs}\wedge\chi_y(s),
 152  \label{eq:contraction}
 153 \end{equation}
 154 where $\chi_x(r)=1$ exactly when $r=x$.
 155 
 156 \begin{proposition}[Selection]
 157 For every binary connective $\Theta$ and $x,y\in\B$,
 158 \begin{equation}
 159  \langle x|[\Theta]|y\rangle=x\Theta y.
 160  \label{eq:selection}
 161 \end{equation}
 162 \end{proposition}
 163 
 164 \begin{proof}
 165 Both states are one-hot. Every term in Equation~\eqref{eq:contraction} vanishes except the term at $(r,s)=(x,y)$.
 166 \end{proof}
 167 
 168 The compiler packs the four coefficients into a constant-size token. That token is not by itself sufficient to authorize a rewrite. An occurrence is also typed by an \emph{operand frame}: the row expression, column expression, their signed polarities, and the truth-state order. In the implementation considered here, a successful pair surrogate ultimately records canonical row and column variable names together with the normalized token.
 169 
 170 \section{Typed normalization and same-frame fusion}
 171 \label{sec:alignment}
 172 
 173 Let
 174 \begin{equation}
 175  P=\begin{bmatrix}0&1\\1&0\end{bmatrix}=[\bxor].
 176 \end{equation}
 177 Define $\Theta^\tau(x,y):=y\Theta x$. With the true-first convention,
 178 \begin{align}
 179  [\Theta^\tau]&=[\Theta]^T, \\
 180  [\Theta(\neg X,Y)]&=P[\Theta], \\
 181  [\Theta(X,\neg Y)]&=[\Theta]P,
 182  \label{eq:input-transforms}
 183 \end{align}
 184 where products with $P$ are XOR--AND products and therefore act as row/column permutations. Output negation is entrywise complement.
 185 
 186 For a binary outer connective $\Phi$, define same-position fusion by
 187 \begin{equation}
 188  \bigl([\Theta_1]\ptop{\Phi}[\Theta_2]\bigr)_{rs}
 189  :=(\Theta_1)_{rs}\Phi(\Theta_2)_{rs}.
 190  \label{eq:pointwise}
 191 \end{equation}
 192 This is not matrix multiplication.
 193 
 194 \begin{theorem}[Same-frame fusion]
 195 If $[\Theta_1]$ and $[\Theta_2]$ are expressed in the same ordered operand frame, then for all $x,y\in\B$,
 196 \begin{equation}
 197  (x\Theta_1 y)\Phi(x\Theta_2 y)
 198  =\left\langle x\middle|
 199  \left([\Theta_1]\ptop{\Phi}[\Theta_2]\right)
 200  \middle|y\right\rangle.
 201  \label{eq:fusion-theorem}
 202 \end{equation}
 203 \end{theorem}
 204 
 205 \begin{proof}
 206 Both sides select position $(x,y)$; the right-hand side stores the outer operation on exactly those two selected coefficients. No distributive law for $\Phi$ over XOR is required.
 207 \end{proof}
 208 
 209 The pointwise identity itself is classical; Cheng, Zhao, and Xu give the direct truth-vector antecedent in Proposition~3.3 \cite{Cheng2011}. The compiler-specific rule is therefore:
 210 
 211 \begin{quote}
 212 \textbf{Admission rule.} Transport signed/swapped occurrences to one declared frame. Apply Equation~\eqref{eq:fusion-theorem} only after row operand, column operand, polarity interpretation, and truth-state order agree.
 213 \end{quote}
 214 
 215 Figure~\ref{fig:compiler-flow} summarizes the resulting local pipeline.
 216 
 217 \begin{figure}[H]
 218 \centering
 219 \begin{tikzpicture}[
 220  node distance=4mm and 4mm,
 221  box/.style={draw=rulegray,rounded corners,fill=soft,align=center,minimum height=10mm,text width=0.19\linewidth,inner sep=5pt},
 222  arrow/.style={-{Latex[length=2mm]},thick,draw=accent}
 223 ]
 224 \node[box] (recognize) {Recognize signed\\binary occurrence};
 225 \node[box,right=of recognize] (align) {Normalize to\\canonical $(R,C)$ frame};
 226 \node[box,right=of align] (fuse) {Fuse matching\\four-bit tokens};
 227 \node[box,right=of fuse] (out) {Return pair token\\with provenance};
 228 \draw[arrow] (recognize)--(align);
 229 \draw[arrow] (align)--(fuse);
 230 \draw[arrow] (fuse)--(out);
 231 \node[box,below=8mm of fuse,text width=0.30\linewidth] (fallback) {If structural construction fails:\\local four-assignment retabulation when admitted, otherwise ordinary IR fallback};
 232 \draw[arrow] (align.south) |- (fallback.west);
 233 \draw[arrow] (fallback.east) -| node[pos=0.22,above,font=\scriptsize]{pair success} (out.south);
 234 \end{tikzpicture}
 235 \caption{The compiler transformation. The operation performed on the four-bit token is trivial; the semantic work is the typed recognition and normalization that determines when fusion is legal and what fallback is required.}
 236 \label{fig:compiler-flow}
 237 \end{figure}
 238 
 239 \subsection{Why frame metadata matters}
 240 
 241 Return to Equation~\eqref{eq:mismatch-expression}. The two implication tokens are numerically equal before typing, but the second occurrence's array coordinates refer to $(Y,X)$ rather than $(X,Y)$. Naively XORing the two unaligned arrays would return the zero token. Transposition moves the second operator into the target frame, after which Equation~\eqref{eq:mismatch-fold} correctly yields $[\bxor]$. The error is therefore not a deficiency of truth tables; it is a failure to track which assignment each stored bit denotes.
 242 
 243 This distinction is closely related to established NPN-style input permutation/negation and output-negation operations \cite{Mishchenko2006,Zhou2019}. The present use is intentionally narrower than a general NPN canonicalizer. It treats frame transport as a local typing obligation for a particular rewrite.
 244 
 245 \section{Pair compiler and soundness}
 246 \label{sec:compiler}
 247 
 248 \subsection{Judgment, invariant, and provenance}
 249 
 250 Let expressions use the grammar
 251 \begin{equation}
 252  e ::= Z\mid \neg e\mid e\,\Phi\,e,
 253  \label{eq:grammar}
 254 \end{equation}
 255 where $Z$ is a variable and $\Phi$ is one of the currently supported binary connectives AND, OR, XOR, implication, and equivalence. Fix distinct canonical variables $R$ and $C$ and a fixed-substitution map $F$ that binds neither variable on a returned pair path. Write $\Gamma=(R,C,F)$.
 256 
 257 Let $\operatorname{Vars}(e)$ collect variable names occurring in the source syntax, recursively by singleton, identity through negation, and union through a binary node. Define
 258 \begin{equation}
 259  \supp_F(e):=\operatorname{Vars}(e)\setminus\operatorname{dom}(F).
 260  \label{eq:syntactic-support}
 261 \end{equation}
 262 This is \emph{syntactic unfixed occurrence}, not essential functional dependence. No Boolean simplification is implicit: $X\lor(Y\bxor Y)$ still has support $\{X,Y\}$ when $F$ is empty, although its value depends only on $X$. Fixed names are excluded from this set and their values are supplied during evaluation.
 263 
 264 An admissible typed pair derivation has judgment
 265 \begin{equation}
 266  \Gamma\vdash e\Downarrow^p \Pair(R,C,t),
 267  \qquad p\in\{S,T,H\},
 268  \label{eq:judgment}
 269 \end{equation}
 270 with the intended invariant
 271 \begin{equation}
 272  \eval_t(r,c)=e[r/R,c/C]
 273  \quad\text{for all }r,c\in\B,
 274  \label{eq:invariant}
 275 \end{equation}
 276 interpreted after the fixed substitutions in $F$.
 277 
 278 Equation~\eqref{eq:judgment} can be read as follows: under compiler environment $\Gamma$, expression $e$ admits a derivation of the four-bit token $t$ in canonical frame $(R,C)$, and $p$ records how that token was obtained. Equation~\eqref{eq:invariant} is the semantic contract. Each of the four token positions must return exactly the value of the original expression under the corresponding assignment to $R$ and $C$. The pair therefore carries both a compact Boolean function and the frame metadata needed to interpret its bit positions.
 279 
 280 The provenance values are:
 281 \begin{itemize}
 282  \item \textbf{$S$ --- structural:} the returned subtree used signed primitive recognition, token complement, and/or same-frame fusion only.
 283  \item \textbf{$T$ --- tabulated root:} the returned subtree itself was produced by evaluating all four assignments. The symbol $T$ avoids overloading $R$, which already denotes the row variable.
 284  \item \textbf{$H$ --- hybrid:} structural steps occur above at least one tabulated descendant.
 285 \end{itemize}
 286 The judgment is a relation, not a deterministic strategy. For example, $X\land Y$ admits both an $S$ primitive derivation and a $T$ tabulation derivation, with the same token $1000_2$. Section~\ref{sec:selection} specifies which derivation is selected. The token API returns \texttt{None} with diagnostic \texttt{ordinary\_fallback} if the selected procedure returns no pair; it does not itself execute the ordinary builder.
 287 
 288 \subsection{Rules, built up one step at a time}
 289 
 290 The inference-rule bar is read as implication: if the premises above the bar hold, the compiler may derive the conclusion below it. The rules perform four conceptually distinct jobs: create a normalized primitive token, complement an already compiled token, fuse two already aligned tokens, and tabulate an exact two-variable subtree. Their validity is independent of the order in which an implementation attempts them.
 291 
 292 \paragraph{Primitive normalization.}
 293 Let $\ell_1,\ell_2$ be signed literals whose underlying variables are exactly $R$ and $C$ in either order. If the declared normalization procedure transports the primitive occurrence $\Theta(\ell_1,\ell_2)$ into the canonical frame and returns token $t$, then the compiler may derive
 294 \[
 295 \frac{
 296   \operatorname{Norm}_{\Gamma}(\Theta(\ell_1,\ell_2))=t
 297 }{
 298   \Gamma\vdash \Theta(\ell_1,\ell_2)\Downarrow^S \Pair(R,C,t)
 299 }.
 300 \]
 301 Normalization consists only of the declared operand exchange and row/column polarity transforms from Equation~\eqref{eq:input-transforms}. This is the structural base case: it establishes a token whose four bit positions already refer to the canonical assignments $(R,C)=(1,1),(1,0),(0,1),(0,0)$.
 302 
 303 \paragraph{Negation: Equation~\eqref{eq:neg-rule}.}
 304 Once a child has a correct token in the canonical frame, negating the expression requires only bitwise complement of that token:
 305 \begin{equation}
 306 \frac{\Gamma\vdash a\Downarrow^p\Pair(R,C,t_a)}
 307 {\Gamma\vdash \neg a\Downarrow^{\nu(p)}\Pair(R,C,\neg t_a)}.
 308 \label{eq:neg-rule}
 309 \end{equation}
 310 The frame does not change. Here $\neg t_a$ means complement each of the four token bits. Provenance changes only to report ancestry: $\nu(S)=S$ and $\nu(T)=\nu(H)=H$. Thus a structural NOT above a locally tabulated child is correct but explicitly reported as hybrid.
 311 
 312 \paragraph{Same-frame fusion: Equation~\eqref{eq:fuse-rule}.}
 313 Two compiled children may be fused only when their pair metadata name the same canonical frame:
 314 \begin{equation}
 315 \frac{\Gamma\vdash a\Downarrow^p\Pair(R,C,t_a)
 316 \qquad
 317 \Gamma\vdash b\Downarrow^q\Pair(R,C,t_b)}
 318 {\Gamma\vdash a\Phi b\Downarrow^{p\sqcup q}\Pair(R,C,t_a\ptop{\Phi}t_b)}.
 319 \label{eq:fuse-rule}
 320 \end{equation}
 321 The token operation $t_a\ptop{\Phi}t_b$ applies $\Phi$ independently to corresponding token positions. The repeated $\Pair(R,C,\cdot)$ in the two premises is the essential admission certificate: position $11$ in one child denotes the same assignment as position $11$ in the other, and similarly for $10,01,00$. Define $S\sqcup S=S$; every other combination is $H$ because tabulated ancestry is present below a structural fusion.
 322 
 323 \paragraph{Exact local tabulation.}
 324 If the syntactic unfixed support $\supp_F(e)$ is exactly $\{R,C\}$, define the true-first token
 325 \begin{equation}
 326  t_e:=\bigl(e(1,1),e(1,0),e(0,1),e(0,0)\bigr).
 327  \label{eq:tab-token}
 328 \end{equation}
 329 Then the exact tabulation rule is
 330 \[
 331 \frac{
 332   \supp_F(e)=\{R,C\}
 333   \qquad t=t_e
 334 }{
 335   \Gamma\vdash e\Downarrow^T\Pair(R,C,t)
 336 }.
 337 \]
 338 This rule re-evaluates a two-variable subtree on its complete four-assignment domain. It is an exact semantic base case. Its rule has no premise requiring structural failure; that restriction belongs to the ordered hybrid procedure.
 339 
 340 \paragraph{Worked derivation.}
 341 Let $\Gamma=(X,Y,\varnothing)$ and
 342 \begin{equation}
 343  e=(X\Rightarrow\neg Y)\bxor(\neg Y\Rightarrow X).
 344  \label{eq:worked-expression}
 345 \end{equation}
 346 In true-first order $(11,10,01,00)$, implication has token $1011_2$. For the left child, the variables are already in $(X,Y)$ order but the column literal is negated, so the column-polarity transform gives
 347 \[
 348  X\Rightarrow\neg Y\quad\longmapsto\quad 0111_2.
 349 \]
 350 For the right child, the source operands arrive as $(\neg Y,X)$. Operand exchange followed by polarity alignment gives
 351 \[
 352  \neg Y\Rightarrow X\quad\longmapsto\quad 1110_2.
 353 \]
 354 Both children now carry frame $(X,Y)$, so Equation~\eqref{eq:fuse-rule} is legal:
 355 \begin{equation}
 356  0111_2\ \bxor\ 1110_2=1001_2.
 357  \label{eq:worked-fusion}
 358 \end{equation}
 359 Hence
 360 \[
 361  \Gamma\vdash e\Downarrow^S\Pair(X,Y,1001_2).
 362 \]
 363 The token $1001_2$ is $[\Leftrightarrow]$ in true-first order, so the compiler has established
 364 \[
 365  (X\Rightarrow\neg Y)\bxor(\neg Y\Rightarrow X)=X\Leftrightarrow Y
 366 \]
 367 without first expanding the source expression into an ANF or another larger symbolic representation. Applying Equation~\eqref{eq:neg-rule} once more complements $1001_2$ to $0110_2$, the XOR token.
 368 
 369 An $S$ derivation uses no tabulation; a $T$ derivation ends with tabulation; an $H$ derivation uses structural composition above a tabulated descendant. These are derivation properties. In particular, the strategy named \texttt{hybrid} can select an $S$, $T$, or $H$ result, depending on the expression.
 370 
 371 \begin{theorem}[Pure structural soundness]
 372 If $\Gamma\vdash e\Downarrow^S\Pair(R,C,t)$, then Equation~\eqref{eq:invariant} holds and no four-assignment tabulation was used.
 373 \end{theorem}
 374 
 375 \begin{proof}
 376 Induct on the derivation. A signed primitive is correct by the frame transforms in Equation~\eqref{eq:input-transforms}; complementing a correct child represents negation; and fusing two correct children with identical metadata is sound by Theorem~1.
 377 \end{proof}
 378 
 379 \begin{definition}[Declared pure-structural fragment]
 380 Fix canonical variables $R,C$. Let $\mathcal S_{R,C}$ be the smallest expression class containing every supported primitive $\Theta(\ell_1,\ell_2)$ whose signed literals have underlying variables exactly $R,C$ in either order, and closed under negation and the five supported binary connectives.
 381 \end{definition}
 382 
 383 \begin{theorem}[Completeness for the declared pure-structural fragment]
 384 For every $e\in\mathcal S_{R,C}$, the \texttt{pure\_structural} strategy derives a unique canonical-frame token $t$ such that
 385 \[
 386  \Gamma\vdash e\Downarrow^S\Pair(R,C,t)
 387 \]
 388 and Equation~\eqref{eq:invariant} holds.
 389 \end{theorem}
 390 
 391 \begin{proof}
 392 Induct on the construction of $e$. Every primitive in $\mathcal S_{R,C}$ is admitted by primitive normalization. Negation preserves the frame and remains structural by Equation~\eqref{eq:neg-rule}. If two children belong to $\mathcal S_{R,C}$, induction gives tokens in the same canonical frame, so Equation~\eqref{eq:fuse-rule} applies. Uniqueness follows because a Boolean function on fixed variables $R,C$ has one four-bit truth token in the declared true-first order.
 393 \end{proof}
 394 
 395 \begin{remark}
 396 This is syntactic completeness for the deliberately declared compiler fragment, not semantic completeness for all formulas with two-variable support. A semantically equivalent expression outside $\mathcal S_{R,C}$ may still require exact tabulation or ordinary fallback.
 397 \end{remark}
 398 
 399 \begin{lemma}[Exact pair tabulation]
 400 Suppose the syntactic unfixed support $\supp_F(e)$ is exactly one distinct row variable $R$ and one distinct column variable $C$. Evaluating $e$ at $(1,1),(1,0),(0,1),(0,0)$ and storing those four outputs in true-first order produces the unique token satisfying Equation~\eqref{eq:invariant}.
 401 \end{lemma}
 402 
 403 \begin{theorem}[Soundness of admitted pair compilation]
 404 Every derivable pair result with provenance $p\in\{S,T,H\}$ satisfies Equation~\eqref{eq:invariant}. Separately, if the selected procedure returns no pair, the dense wrapper delegates correctness to the unchanged ordinary IR evaluator on the original expression, assuming that evaluator's contract.
 405 \end{theorem}
 406 
 407 \begin{proof}
 408 The cases $S$ and $T$ are the preceding theorem and lemma. For $H$, use structural induction with exact local tabulation as an additional sound base case; token complement and same-frame fusion preserve the invariant. Provenance changes the reported construction path, not the represented function. The fallback statement is an interface contract rather than a theorem about the pair compiler itself.
 409 \end{proof}
 410 
 411 \subsection{Admissibility boundary}
 412 
 413 The current pure structural rule does not claim semantic recognition of arbitrary equivalent compound operands. Repeated-variable forms such as $X\Theta X$, opaque compound operands, and incompatible variable pairs remain outside the pure rule. Duplicate axes and overlapping row/column layouts are invalid inputs and raise an error; they are not ordinary pair misses. A retabulation rule may cover some two-variable cases exactly, but it is intentionally classified as a different mechanism.
 414 
 415 This conservative boundary is useful. It allows the compiler to refuse a local rewrite rather than infer an unproved equivalence. It also gives the experiment a measurable fallback frequency instead of hiding unsupported cases in preprocessing.
 416 
 417 \subsection{Semantic boundary under real-valued relaxation}
 418 \label{sec:soft-boundary}
 419 
 420 The invariant in Equation~\eqref{eq:invariant} is Boolean. A real-valued interpretation requires a separate contract. For a truth table $C=\left(\begin{smallmatrix}a&b\\c&d\end{smallmatrix}\right)\in\B^{2\times2}$ and $p,q\in[0,1]$, ordinary real contraction gives
 421 \begin{equation}
 422  B_C(p,q)=[p,1-p]C[q,1-q]^T
 423  =d+(b-d)p+(c-d)q+(a-b-c+d)pq.
 424  \label{eq:soft-contraction}
 425 \end{equation}
 426 For independent Bernoulli inputs this is the probability of the represented Boolean event. More generally, let $e$ be a finite propositional expression over $n$ distinct base-event identities and let $B_e$ be the unique multilinear polynomial interpolating its Boolean truth table. Under the product Bernoulli model with marginal vector $p$, $B_e(p)=\Pr_p(e=1)$. For a correlated model $\mu$, the probability is instead $\sum_x e(x)\mu(x)$; marginals alone need not determine it. Weighted model counting supplies the established model-sum interpretation, and semantic loss uses the negative logarithm of the satisfying-assignment probability~\cite{Kimmig2017,Xu2018}. These are ordinary real operations, distinct from the XOR--AND contraction.
 427 
 428 This whole-table interpretation need not agree with recursively applying soft kernels to subexpressions with shared variables. PALO's approximate propositional semantics uses $pq$ for conjunction, $p+q-pq$ for disjunction, $1-p+pq$ for implication, and $1-p-q+2pq$ for primitive equivalence; it explicitly recognizes the independence approximation and the failure of several classical laws~\cite[Sections~3.2, 3.5--3.6]{Stehr2022}. In particular, the Boolean fusion already established in Equation~\eqref{eq:worked-fusion},
 429 \[
 430  (X\Rightarrow\neg Y)\bxor(\neg Y\Rightarrow X)\equiv X\Leftrightarrow Y,
 431 \]
 432 does not preserve recursive soft evaluation with negation $1-p$ and XOR kernel $u+v-2uv$. At $p=q=1/2$, both implications have value $3/4$, so the source has value $3/8$, whereas the fused equivalence has value $1/2$. This compares the declared propositional kernels, not PALO's full quantified, batched, or learning semantics.
 433 
 434 For expressions built from the bilinear kernels in Equation~\eqref{eq:soft-contraction} and negation $1-p$, let $s_e$ be the recursive polynomial with one free coordinate per distinct base-event identity. A sufficient condition for $s_e=B_e$ is disjoint syntactic base-variable supports at every binary composition. More generally, equality on the full cube $[0,1]^n$ holds exactly when $s_e$ is affine separately in every coordinate, after coefficient cancellation. Both polynomials agree at the Boolean corners; uniqueness of multilinear interpolation proves sufficiency, and equality on the full cube implies polynomial identity, proving necessity. This full-cube criterion need not be necessary on a restricted parameter image. Distinct independent events may share a parameter $t$: their conjunction then has probability $t^2$, whereas repeating one event gives probability $t$. Event identity must therefore be kept separate from parameter identity. Polynomial expansion can grow exponentially; same-frame metadata alone does not establish this additional contract.
 435 
 436 A future numerical backend should distinguish Boolean equivalence, equality of the recursive soft function, almost-sure event equality under a specified joint model, and thresholded-decision equality on a declared domain. Equal marginals alone do not authorize contextual replacement: independent fair events $X,Y$ both have probability $1/2$, but $\Pr(X\land X)=1/2$ and $\Pr(X\land Y)=1/4$. Almost-sure equality permits replacement in Boolean contexts evaluated under that same model. A decision contract must specify its threshold, tie rule, and placement. PALO inserts crispification at each propositional interpretation~\cite[Section~3.7]{Stehr2022}; at threshold $1/2$ with a $\geq$ tie rule, inputs $p=q=3/5$ give crisp conjunction $1$, while thresholding their final soft product $9/25$ gives $0$.
 437 
 438 For a common differentiable parameterization $p=\phi(\theta)$, identity $s_e\circ\phi=s_f\circ\phi$ on an open parameter domain is sufficient for equality of mathematical parameter gradients there. Equality only at selected points or on a lower-dimensional input set does not guarantee equality of ambient input gradients: $p$ and $pq$ agree on $q=1$, but have gradients $(1,0)$ and $(1,p)$ there. Function equality is not necessary for gradient equality; an additive constant is a counterexample. Custom backward rules and floating-point evaluation need separate contracts. These distinctions bound possible extensions of this Boolean compiler; no integrated differentiable backend, training improvement, or CM-specific advantage is claimed. Ordinary framed truth tables support the same checks.
 439 
 440 \section{Implementation architecture and cost model}
 441 \label{sec:implementation}
 442 
 443 \subsection{Five artifacts, not one}
 444 
 445 Table~\ref{tab:artifacts} separates implementation objects that are easily conflated when all are described informally as a ``CM.''
 446 
 447 \begin{table}[t]
 448 \centering
 449 \small
 450 \begin{tabularx}{\linewidth}{@{}>{\raggedright\arraybackslash}p{0.18\linewidth}>{\raggedright\arraybackslash}X >{\raggedright\arraybackslash}p{0.24\linewidth}@{}}
 451 \toprule
 452 \textbf{Artifact} & \textbf{Meaning} & \textbf{Role}\\
 453 \midrule
 454 CM operator token & One binary truth function packed into four true-first bits $(11,10,01,00)$. & Constant-size transform and fusion.\\
 455 Pair surrogate & Token plus canonical row and column operand names/frame metadata. & Carries the legality invariant.\\
 456 General CM/Boolean IR & Interned expression DAG for arbitrary supported formulas. & General symbolic fallback and compilation.\\
 457 Flat program & Backend-dependent instruction sequence lowered from the IR. & Repeated packed/array evaluation.\\
 458 Explicit dense output & Materialized truth relation over all retained ambient row/column axes. & $2^m$ entries for $m$ retained axes; one byte per NumPy Boolean entry.\\
 459 \bottomrule
 460 \end{tabularx}
 461 \caption{Compiler artifacts and their semantic boundaries. Only the first is the constant-size binary operator token.}
 462 \label{tab:artifacts}
 463 \end{table}
 464 
 465 A token-only endpoint cannot be compared as if it had already paid to construct an explicit $2^m$-entry ambient result. Conversely, a comparator that has already prepared a reusable DAG or program should not be charged for that preparation on every query when the CM arm is allowed resident reuse. Endpoint equality is part of benchmark correctness.
 466 
 467 \subsection{Ordered, strategy-dependent selection}
 468 \label{sec:selection}
 469 
 470 The source snapshot is pinned to commit \texttt{0ab8ffd0c23ffa71ee951d375b1c170ffdcc084b} of the public implementation \cite{CompilerSnapshot2026}. Let $\mathcal R,\mathcal C$ be ordered ambient row/column name lists, each duplicate-free and mutually disjoint. A pair frame consists of one unfixed name $R\in\mathcal R$ and one unfixed name $C\in\mathcal C$; these names are discovered from the expression, not chosen by lexicographic order. The full supported AST is validated and its occurrence, identity-node, and height statistics are computed before strategy selection. The intended input domain supplies every occurring name through a layout or $F$; other errors are not silently converted into pair misses.
 471 
 472 \begin{lstlisting}
 473 Pair(e, row_layout, column_layout, F, allowRetab):
 474     if e is a supported binary connective over signed literals
 475        with distinct unfixed names on opposite layout sides:
 476         normalize operand order and polarities
 477         return Pair(R, C, token, S)
 478     if e = NOT a:
 479         child = Pair(a, ..., allowRetab)
 480         if child succeeds: return its complement, with nu provenance
 481     else if e = a Phi b:
 482         left  = Pair(a, ..., allowRetab)
 483         right = Pair(b, ..., allowRetab)  # attempted even if left fails
 484         if both succeed on the same frame:
 485             return their fusion, with joined provenance
 486     else if e is a variable: return NoPair
 487     else: raise unsupported-node error
 488     if allowRetab and supp_F(e) has exactly one row and one column name:
 489         return four-assignment token with provenance T
 490     return NoPair
 491 
 492 Select(e, strategy):
 493     pure_structural -> Pair(e, ..., allowRetab=false)
 494     hybrid          -> Pair(e, ..., allowRetab=true)
 495     retabulate      -> tabulate root if support admits a pair, else NoPair
 496 \end{lstlisting}
 497 
 498 The compatibility name \texttt{structural} aliases \texttt{hybrid}, not \texttt{pure\_structural}. For valid input and fixed strategy, the procedure selects one outcome. Every successful return supplies a derivation of Equation~\eqref{eq:judgment}: this follows by induction over the executed recursive calls, using the corresponding inference rule at each return. Thus the relational soundness theorems apply to the selected result. A \texttt{NoPair} return means failure of that strategy, not non-derivability in the entire relation. For example, $X\lor(Y\land Y)$ has a $T$ derivation but the pure strategy returns \texttt{NoPair}. Recursion terminates on finite acyclic ASTs/DAGs; the recursive pair walk can revisit identity-shared nodes.
 499 
 500 \paragraph{Selection, diagnostics, and commitment.}
 501 The public token artifact stores the two names and token; provenance is returned in accompanying metrics. Selected $S,T,H$ map respectively to \texttt{pure\_structural}, \texttt{full\_retabulation}, and \texttt{hybrid\_pair}. \texttt{None} maps to \texttt{ordinary\_fallback}, even in the token-only API, where no builder is called. The dense wrapper first checks the ambient output budget, then obtains the token result. On success it lifts that token to the ambient layout; on failure it calls the ordinary builder on the \emph{original expression}.
 502 
 503 Consequently, $e=(X\land Y)\lor Z$, with no fixed variables and layouts $[X,Z]$ and $[Y]$, constructs an $S$ child for $X\land Y$ but returns no root pair. The successful child is discarded when the dense wrapper invokes the builder. The builder may independently optimize the original expression; this wrapper does not pass it a partially rewritten tree. Likewise, a root retabulation can supersede earlier child attempts. Counters such as \texttt{pair\_collapses} measure local work performed, including discarded work, not committed rewrites in the returned object. Root outcome must accompany these counters; committed contributions require separate instrumentation. Persistent child rewriting would be a different compiler version.
 504 
 505 \subsection{Layout conversion and ownership}
 506 
 507 The compact token uses true-first order while the historical dense array path uses false-first axes. The conversion is an explicit reindexing. If $T$ denotes the true-first $2\times2$ view and $D$ the false-first view indexed by array positions $a,b\in\{0,1\}$, then
 508 \begin{equation}
 509  D_{ab}=T_{1-a,1-b}.
 510  \label{eq:layout-conversion}
 511 \end{equation}
 512 The dense contract retains \emph{every supplied ambient axis}, including fixed names and names on which the residual function is independent. Writing $m=|\mathcal R|+|\mathcal C|$, the returned shape is
 513 \begin{equation}
 514  2^{|\mathcal R|}\times2^{|\mathcal C|},\qquad\text{with }2^m\text{ Boolean entries}.
 515  \label{eq:ambient-shape}
 516 \end{equation}
 517 For each false-first row/column index, decode its ambient assignment, override fixed names by $F$, and evaluate $e$. This defines the corresponding entry. Fixed values affect evaluation, while their axis positions remain and repeat that value; irrelevant axes are also broadcast. A fixed variable may be supplied by $F$ without appearing in the layout.
 518 
 519 For example, $(X\land Y)\lor Z$ with $F=\{Z\mapsto0\}$, $\mathcal R=[X,Z]$, and $\mathcal C=[Y]$ returns
 520 \begin{equation}
 521  M=\begin{bmatrix}0&0\\0&0\\0&1\\0&1\end{bmatrix},
 522  \label{eq:fixed-axis-example}
 523 \end{equation}
 524 whose rows are $(X,Z)=00,01,10,11$. The residual function is $X\land Y$, but the result has eight entries. A projected four-entry relation would require the caller to request a reduced layout or a separately specified projection API. The current dense wrapper neither drops fixed axes nor minimizes essential support.
 525 
 526 The materialized dense result is an owned writable array, not a writable broadcast view. Its NumPy Boolean entries occupy one byte each; a bit-packed relation is a different output representation. Expression nodes and pair surrogates are immutable under the compiler contract, and caller-owned layouts/fixed maps are read-only.
 527 
 528 \subsection{Cost model}
 529 
 530 Let $N$ be AST occurrences, $U$ unique DAG nodes, $H$ AST height, $S$ occurrences in a subtree sent to retabulation, $D$ its evaluation depth, $k$ the length of a signed literal's negation chain, and $m$ the number of retained ambient output axes. The counts $|\supp_F(e)|$ and the number of essential variables can both be smaller than $m$.
 531 
 532 \begin{itemize}
 533  \item Inspecting a signed literal costs $O(k)$ followed by an $O(1)$ four-bit transform.
 534  \item A four-bit token fusion is $O(1)$.
 535  \item One exact pair retabulation costs $O(4S)$ time plus the evaluator's stack/workspace requirements.
 536  \item A fully successful structural pair tree is ordinarily $O(N)$ time and $O(H)$ stack space, although the current support-discovery strategy can rescan rejected subtrees and therefore has an $O(N^2)$ worst case.
 537  \item A sharing-aware evaluator may scale with $U$ rather than $N$, which is why DAG-preserving packed/CSE comparators are mandatory.
 538  \item The current dense wrapper budgets and materializes $2^m$ entries even if many are repeated. Its output allocation/copy costs $\Theta(2^m)$ time and bytes; additional compiler workspace is separate. Projected or bit-packed outputs require separate accounting.
 539 \end{itemize}
 540 
 541 The last point prevents a common category error: constant-time token fusion is a local kernel fact, not an end-to-end complexity theorem.
 542 
 543 \section{Closest prior art and matched comparators}
 544 \label{sec:related}
 545 
 546 The compiler should be compared with operations that possess equivalent local information, not with deliberately weaker baselines.
 547 
 548 \paragraph{Boolean matrices and truth vectors.}
 549 Edwards developed Boolean-matrix logic well before the present work \cite{Edwards1972}. Cheng, Zhao, and Xu use XOR as addition and AND as multiplication and state the same-variable entrywise outer-operation law in Proposition~3.3 \cite{Cheng2011}. Reshaping such a vector into $2\times2$ form does not make that pointwise identity new.
 550 
 551 \paragraph{Matrix/vector logic.}
 552 Stern and Mizraji provide established operator/matrix representations of logic \cite{Stern1988,Mizraji1992,Mizraji2008}. Bricken's technical note explicitly places logical matrices between two-component states in bra--matrix--ket form \cite{Bricken1997}. The companion foundations paper contains the appropriate broader comparison; the computational manuscript needs only enough of this history to prevent novelty from being attached to notation or representation alone.
 553 
 554 \paragraph{NPN, LUT, and AIG practice.}
 555 Small truth functions are routinely packed into machine words, transformed under input permutation/negation and output negation, classified up to NPN equivalence, and used in cut-based rewriting. DAG-aware AIG rewriting specifically exploits graph sharing rather than treating a formula as an unshared tree \cite{Mishchenko2006,Zhou2019,Testa2019}. CM transposition, row/column reversal, complement, and four-bit storage are therefore familiar small-function operations. Kitty directly provides truth-table Boolean operations, variable swaps/flips, dependence tests, cofactors, and base expansion \cite{KittyOperations}. These primitives do not distinguish this compiler.
 556 
 557 The closest architectural comparison also carries operand identity: mockturtle cut rewriting supplies a truth table together with an ordered iterator range of leaves \cite{MockturtleCut}. An explicit frame is therefore not an unprecedented addition to a truth function. DAG-aware AIG rewriting evaluates candidate replacement gain against shared graph structure before committing a selected replacement \cite{Mishchenko2006}. The present wrapper instead attempts a restricted variable-pair root and abandons child constructions on root failure; it neither enumerates general cuts nor selects network replacements by sharing-aware area gain.
 558 
 559 \begin{table}[H]
 560 \small\centering
 561 \begin{tabularx}{\linewidth}{@{}p{0.23\linewidth}XX@{}}
 562 \toprule
 563 \textbf{Comparison} & \textbf{Shared capability} & \textbf{Boundary in this paper}\\
 564 \midrule
 565 Cheng et al.; kitty & Aligned truth-function combination and table manipulation. & No algebraic or primitive-operation novelty claim.\\
 566 Cut/AIG rewriting & Truth functions with leaf identities, input transforms, local candidates. & No general cut enumeration, gain search, or persistent graph replacement here.\\
 567 Direct packed/DAG evaluator & Same four values; identity sharing can be preserved. & Primary end-to-end comparator; recognition overhead must be paid.\\
 568 This contract artifact & Frame, strategy, provenance, failure, ownership, and output size specified together. & Regression-tested integration; synthetic primary and bounded natural secondary comparisons are negative.\\
 569 \bottomrule
 570 \end{tabularx}
 571 \caption{Closest comparisons and the remaining, deliberately limited methods contribution. No kitty or AIG runtime comparison was executed for this revision.}
 572 \end{table}
 573 
 574 \paragraph{Direct packed evaluation.}
 575 A strong simple comparator evaluates the AST once over four packed masks to obtain all four assignments in parallel. With identity memoization it also preserves explicit DAG sharing. It returns exactly the same four-bit function required by a pair-token endpoint and does not need CM-specific frame metadata. This is the closest baseline for deciding whether structural recognition pays for itself.
 576 
 577 \paragraph{Generic local truth-function optimization.}
 578 A generic optimizer given the same local support/function information can tabulate or combine a small cut without using CM notation. The S1/S2 evidence below shows why this comparator is scientifically necessary: it reaches the same reduced symbolic outputs as CM folding on the admitted all-arm cases.
 579 
 580 \paragraph{ROBDDs and broader rewrite search.}
 581 ROBDDs provide canonical function representations for a fixed variable order \cite{Bryant1986}. Equality saturation and synthesis-driven superoptimization retain or search broader classes of equivalent expressions \cite{Willsey2021,Sasnauskas2017}. These systems solve a more general problem than the fixed two-operand rule; comparison should therefore charge recognition/search/extraction and compare delivered artifacts appropriate to the task.
 582 
 583 \section{Experimental questions and evidence hierarchy}
 584 \label{sec:evaluation}
 585 
 586 The computational claim is meaningful only if the benchmark answers the same question for every arm. Four distinctions are especially important.
 587 
 588 \begin{enumerate}
 589  \item \textbf{Kernel versus compiler.} Four-bit fusion time is not compilation time.
 590  \item \textbf{Prepared versus one-shot.} A resident token/program may amortize setup; one-shot use may not.
 591  \item \textbf{Compact versus materialized output.} A token endpoint is not a complete $2^m$-entry ambient truth relation.
 592  \item \textbf{Task contract.} ANF production, complete truth-vector evaluation, repeated restriction, counting, and multi-root output are different tasks and cannot share one headline ratio.
 593 \end{enumerate}
 594 
 595 Figure~\ref{fig:evidence-levels} shows the evidence levels used in this draft.
 596 
 597 \begin{figure}[H]
 598 \centering
 599 \begin{tikzpicture}[
 600  node distance=4.5mm,
 601  level/.style={draw=rulegray,rounded corners,fill=soft,align=left,text width=0.88\linewidth,inner sep=5pt},
 602 ]
 603 \node[level] (a) {\textbf{1. Formal/finite correctness:} frame transforms, fusion invariant, retabulation, provenance, implementation tests.};
 604 \node[level,below=of a] (b) {\textbf{2. Exploratory mechanism:} S1/S2 pre-expansion work reductions and exact tie with matched generic local optimization.};
 605 \node[level,below=of b] (c) {\textbf{3. Completed different endpoint:} P14-PY0 ANF dispatcher, negative overall under its frozen primary rule.};
 606 \node[level,below=of c] (d) {\textbf{4. Separate project context:} later current-source complete-relation/restriction/multi-root campaigns; useful for methodology, not pair-compiler attribution.};
 607 \node[level,below=of d] (e) {\textbf{5. Pair-token evidence:} frozen synthetic v4 primary comparison is negative; bounded natural v5 secondary timing is negative; broader v3 scope remains open.};
 608 \end{tikzpicture}
 609 \caption{Evidence hierarchy. A favorable result on a different endpoint is not promoted into pair-compiler evidence.}
 610 \label{fig:evidence-levels}
 611 \end{figure}
 612 
 613 \subsection{Confirmatory workload design}
 614 
 615 The preserved, pre-freeze protocol-v3 design \cite{ProtocolV3} separates exact-frame formulas, signed/swapped frames, local retabulation cases, hybrid mixed-child cases, multiple operand pairs, compound-operand cases outside the structural claim, and natural formulas/circuits. Balanced generated trees use AST occurrence counts $15,63,255,1023,4095$; skewed trees stop at 255 occurrences and measured height at most 128. Cases cross the five supported outer connectives, reuse counts $1,10,100,1000$, and sharing conditions that distinguish identity-shared nodes, structurally equal but separately allocated subtrees, and no sharing. Every case records both $N$ and $U$.
 616 
 617 Requested outputs include compact tokens, scalar evaluation, packed batches, and dense outputs where the output budget permits them. Preparation and query costs are reported separately. Once two arms have produced the same four-bit token and call the same lookup function, the query cost is common; any advantage must arise earlier or through a measured reuse policy.
 618 
 619 The sole primary cell is intentionally narrow: signed/permuted pure-structural balanced formulas with $N=1023$, $U=N$, no fixed variables, token output, reuse one, compared end to end with direct packed AST evaluation. The proposed primary success rule requires zero correctness disagreements, a median competitor-to-CM ratio of at least $1.20$ whose 95\% interval lies entirely above one, and no more than a 10\% median peak-memory increase. The interval requirement establishes superiority, not a lower confidence guarantee of $1.20\times$. All other cells are secondary. This prevents a favorable post hoc workload from replacing a failed primary comparison.
 620 
 621 A dated protocol-v4 successor fixed the synthetic primary case count and seeds, resident cache-reset timing, formula-level aggregation, and resampling before timing held-out formulas; Section~\ref{sec:v4-primary} reports its negative result. A separately frozen EPFL primary-output admission and correctness screen reports root outcomes by strategy (Section~\ref{sec:natural-gate}). A later frozen descriptive v5 run measures matched Python full-bitset production on 70 of the 71 selected cones, retaining one calibration failure; ABC process wall remains an unmatched diagnostic. Admission addresses applicability rather than timing superiority.
 622 
 623 The $1.20\times$ ratio and 10\% memory allowance are engineering acceptance targets, not consequences of soundness or a power calculation. Their purpose is to demand a material gain while limiting memory growth; a $1.20\times$ ratio corresponds to 16.7\% less elapsed time. The preserved plan did not establish an empirical power calculation. The v4 pilot used disjoint seeds and met the 5\% repeatability criterion on its eight cases; the 64 formula/case seeds, rather than timing repetitions, supply the independent units for the reported synthetic interval. Its negative result is retained under the originally declared threshold.
 624 
 625 \paragraph{Initialization and cache regimes.}
 626 The source builds composition lookup tables when \path{cm_token} is imported, memoizes \path{cm_compose}, and caches permutation/lift metadata in \path{cm_normalize}. A fresh-process one-shot measurement must charge startup/import and table initialization. V4 instead uses a fresh process per formula but times repeated calls after common imports, clearing the CM memoization before each CM call and the bitset-environment cache before each direct call. The direct timed call builds its environment; imported lookup tables remain resident and their setup is recorded separately. This is a post-import cache-reset comparison, not a full process-start comparison. Warm regimes require a declared priming workload and cache lifetime. Charge support discovery, recognition, unsuccessful pair work, retabulation, fallback, and required materialization to their respective production arms; separate common token queries from preparation.
 627 
 628 \section{Current evidence}
 629 \label{sec:results}
 630 
 631 \subsection{Correctness and implementation assurance}
 632 \label{sec:fresh-checks}
 633 
 634 The historical record reports 116 focused tests on 19 September 2026 and a separate 1,048,576-case signed-fusion check. Those reports do not by themselves bind that historical execution to the source revision inspected here. This revision supplies a fresh, separately identified run against the unmodified pinned source: 90 upstream tests from \texttt{test\_cm\_pair\_alignment.py} and \texttt{test\_output\_budget.py}, plus 33 contract regression cases, all passed. The latter include an exhaustive comparison over all 16 input tokens in each of eight signed frames, both children, all five supported outer connectives, and all four assignments: 327,680 scalar comparisons. This is implementation correctness evidence, not a timing campaign or a rerun of the historical 116-test selection.
 635 
 636 \begin{table}[H]
 637 \small\centering
 638 \begin{tabularx}{\linewidth}{@{}p{0.34\linewidth}XXX@{}}
 639 \toprule
 640 \textbf{Expression / boundary} & \textbf{Pure} & \textbf{Hybrid} & \textbf{Retabulate}\\
 641 \midrule
 642 $X\land Y$ & $S$, $1000$ & $S$, $1000$ & $T$, $1000$\\
 643 $X\lor(Y\land Y)$ & NoPair & $T$, $1110$ & $T$, $1110$\\
 644 $\neg(X\lor(Y\land Y))$ & NoPair & $H$, $0001$ & $T$, $0001$\\
 645 $X\lor(Y\bxor Y)$ & NoPair & $T$, $1100$ & $T$, $1100$\\
 646 $(X\land Y)\lor(Z\bxor Z)$ & NoPair & NoPair & NoPair\\
 647 $(X\land Y)\lor Z$, $F(Z)=0$ & Builder & $T$, $1000$ & $T$, $1000$\\
 648 \bottomrule
 649 \end{tabularx}
 650 \caption{Contract examples. Tokens use true-first order. Layouts are $[X],[Y]$ for the first four rows and $[X,Z],[Y]$ for the last two. ``Builder'' means the dense wrapper executes ordinary fallback; its token API returns NoPair. All dense strategies in the last row return the eight-entry matrix in Equation~\eqref{eq:fixed-axis-example}.}
 651 \label{tab:regressions}
 652 \end{table}
 653 
 654 The suite also checks constant-valued redundant formulas, identity-shared versus separately allocated equal trees, invalid layouts, retained irrelevant axes, owned output, input nonmutation, budget refusal before pair compilation, token failure without builder execution, and identity of the original expression passed to fallback after successful child construction. These finite checks make the operational boundary reusable and falsifiable. They neither prove unrestricted program correctness nor demonstrate an advantage over existing synthesis libraries.
 655 
 656 The subsequently supplied full audit includes a separate standard-library mathematical/reference-model checker. Rerunning its unmodified script reproduces the supplied results exactly: 1,048,576 fusion assignment checks over all 16 abstract outer functions, 8,080 bounded structural expressions, and 15,000 seeded strategy runs with 6,615 successful tokens. These are reference-model checks, not additional production-source tests. The audit archive and its 21 verified member hashes are preserved separately from the implementation evidence.
 657 
 658 \subsection{S1/S2: mechanism evidence and the generic tie}
 659 
 660 A fresh recount of the recovered canonical exploratory S1/S2 CSV confirms 10,500 generated cases. Of these, 10,389 completed in all four arms: direct ANF, sharing-aware common-subexpression evaluation, a generic local truth-function optimizer, and CM folding. The all-arm population contains 3,750 S1 and 6,639 S2 cases. The remaining 111 are retained rather than silently filtered: 108 fail in all arms, two complete only in the generic and CM arms, and one only in the sharing arm. No completed correctness disagreement was recorded.
 661 
 662 On every admitted all-arm case, CM and generic local optimization agree on seven principal symbolic-output metrics: final degree, final monomial count, multiplication count, output unique nodes, pair terms, peak monomials, and serialized bytes. The generic arm records more folds on 6,010 cases and CM more on none; fold count is not runtime. For corrected S2, median direct/CM multiplication counts at requested sharing fractions $0$, $0.25$, and $0.5$ are respectively $35/35$, $17/12$, and $9/0$.
 663 
 664 The correct interpretation is therefore two-sided. Local small-function folding can remove work before polynomial expansion in some structures. The observed reduction is not uniquely CM-specific: an equally capable generic local optimizer reaches the same reduced outputs. This is mechanism evidence, not an end-to-end speed result.
 665 
 666 \subsection{P14-PY0: a completed negative dispatcher boundary}
 667 
 668 P14-PY0 measures a different endpoint: recipe-to-owned-ANF compilation. Direct lowering (D) lowers the ordinary source DAG; a minimal observer (F) records dispatch information; exact dispatch (E) decides whether to lower directly or construct folding metadata; always-fold (A) and a generic signature optimizer (G) are diagnostics. Preparation required by an arm is included in its production timer. This is not the direct packed token task of protocol v3.
 669 
 670 The recovered historical campaign report used 384 synthetic cases from 12 families and 107 natural cones from 14 previously uninspected EPFL design families, for 491 frozen cases. Three fresh sequential workers produced 51,102 measured rows including diagnostics/canonicalization; equality checks passed the 491 frozen cases and 512 targeted correctness cases. Exact dispatch selected folding on five synthetic cases and no natural cone.
 671 
 672 \begin{table}[H]
 673 \centering
 674 \small
 675 \begin{tabular}{@{}llcc@{}}
 676 \toprule
 677 \textbf{Corpus} & \textbf{Ratio} & \textbf{Geometric mean} & \textbf{98.75\% marginal interval}\\
 678 \midrule
 679 Synthetic & E/F & 0.9606 & [0.9455, 0.9811]\\
 680 Synthetic & E/D & 1.0508 & [0.9683, 1.1075]\\
 681 Natural & E/F & 0.9610 & [0.9411, 1.0001]\\
 682 Natural & E/D & 1.0607 & [1.0176, 1.0927]\\
 683 \bottomrule
 684 \end{tabular}
 685 \caption{Historical P14-PY0 ANF recipe endpoint, not the pair-token protocol. Ratios below one favor the numerator. Bonferroni-adjusted 98.75\% marginal bootstrap intervals target 95\% familywise coverage over the four primary comparisons, subject to component coverage.}
 686 \label{tab:p14}
 687 \end{table}
 688 
 689 The frozen primary rule required E/F geometric mean at most 0.99, E/D at most 0.95, and the relevant multiplicity-adjusted upper bound below one on both corpora. It did not pass. At this endpoint exact dispatch was about 5.1\% slower than direct lowering on the synthetic corpus and 6.1\% slower on the natural corpus. The five selected synthetic cases themselves were highly profitable, with E/D ratios between 0.075 and 0.389, but those local wins did not offset aggregate policy overhead. The preregistered case-balanced geometric mean is retained even though an alternative ratio of summed synthetic medians was favorable. This revision reconstructs the four point estimates and all 17 reported interval sets from the 51,102 raw timing rows using the archived 10,000-draw bootstrap seed, resampling order, and quantile rule. The frozen analysis uses the 0.00625 and 0.99375 quantiles for each primary comparison, clarifying the coverage label in Table~\ref{tab:p14}.
 690 
 691 The recovered freeze records Windows 10, Python 3.10.11, 12 logical CPUs, Balanced power mode, and uncontrolled affinity. The local freeze reduced the draft's 30 workers/100 ms batches to three workers/10 ms target batches with a 40 ms slow-arm cap. Preserved amendments cover a pre-timing per-arm correctness timeout, an extended wall-time budget after the first worker, and an analyzer indexing optimization. The original analyzer and holdout hashes match the recovered freeze. These records improve traceability but do not establish the complete historical runtime dependency closure or reproduce its timing on a new host.
 692 
 693 \subsection{Frozen synthetic pair-token confirmation: negative utility boundary}
 694 \label{sec:v4-primary}
 695 
 696 The disclosed protocol-v4 successor \cite{ProtocolV4} preserved v3's sole synthetic primary cell and four-part decision rule while limiting the executed claim to signed/permuted, unshared two-variable formulas. An eight-formula pilot with disjoint seeds met the 5\% within-case repeatability target before the 64 held-out formula seeds and analysis were frozen. Every held-out formula has $N=U=1023$ AST nodes, 205 primitive row/column operators, 204 signed literal occurrences, balanced combination, and token output at reuse one. Independent scalar evaluation of all four assignments and both production arms agreed; every CM root was pure structural with zero local retabulations.
 697 
 698 One fresh process per formula supplied 30 randomized paired repetitions, yielding 3,840 arm/repetition rows, plus 128 separate process-memory observations and no recorded failures. The compared timer begins after common imports and expression construction. Before each CM call, composition and normalization memoization are cleared; before each direct call, the bitset-environment cache is cleared and environment construction is timed. Import-time CM lookup-table setup is recorded but excluded, so this is a resident post-import comparison and not a process-start one-shot claim. Both producers return the same four-bit token and use the same query function; query cost is excluded from both production timers.
 699 
 700 The formula-median direct-packed/CM time ratio is $0.2479$, with a 95\% hierarchical bootstrap interval $[0.2462,0.2495]$ from 10,000 prespecified draws. The median absolute formula times are 0.588~ms for direct packed evaluation and 2.377~ms for CM compilation; these separate medians are descriptive and their quotient is not the primary statistic. The median CM peak-working-set increase is $-1.56\%$ under the declared fresh-process metric. Common interpreter/import memory dominates these small allocations, so that metric does not prove a material memory advantage. The premeasurement environment record omitted the power scheme; a post-run read showed Windows Balanced but does not establish that setting throughout the run. Correctness and the memory tolerance passed, but both the $1.20$ timing threshold and the interval-above-one criterion failed. Under this exact implementation, grammar, output, and cache regime, direct packed evaluation is about four times faster; the measurements do not isolate which compiler phase causes the gap.
 701 
 702 This is a negative result on the actual pair-token endpoint, distinct from P14's ANF endpoint. It does not measure natural circuits, ABC/AIG competition, identity-shared graphs, dense output, full process startup, or prepared reuse. The separate natural correctness and descriptive timing work below do not retroactively widen this frozen primary comparison.
 703 
 704 \subsection{Later project-wide results: relevant context, different contracts}
 705 \label{sec:later-context}
 706 
 707 Later project reports distinguish favorable small kernels from costly wrappers and show that evaluator rankings change with output and reuse contracts \cite{ProjectCorrection20260825,ProjectArchitecture20260903}. Their methodological relevance is to require direct packed/CSE controls, explicit preparation costs, and matched outputs. Their numerical ratios are not reproduced here because they measure other tasks and do not fill the protocol-v3 pair-compiler result table.
 708 
 709 \subsection{Natural-circuit admission, correctness, and secondary timing}
 710 \label{sec:natural-gate}
 711 
 712 The narrow synthetic primary cell has a negative answer under v4's post-import cache-reset policy. A separate, prospective natural admission screen fixed its rule before any CM compilation \cite{NaturalAdmission2026}. It screened all 2,861 original primary outputs of 20 arithmetic and random/control EPFL BLIFs at a pinned Git revision. Cones with two to twelve syntactic support variables, at most 128 source nodes and depth at most 128 were eligible; up to eight were hash-ranked per design, with no internal cone substitution or post-selection backfill. This admitted 71 original primary-output cones from ten designs. Ten designs had no eligible primary output. Because the source families overlap prior P1--P14 work, this is an applicability cohort, not an independent uninspected-family holdout.
 713 
 714 The copied BLIF bytes match the pinned upstream Git blobs. Translation to the immutable AST and one-output cone export were checked exhaustively against each source BLIF. An ABC 1.01 executable from the pinned 29 July 2026 OSS CAD Suite Windows release imported, structurally hashed, optimized with \texttt{dc2}, and exported an AIG for all 71 cones. Exhaustive AIG truth tables matched the original BLIFs. Before the first CM compilation, a separate correctness run froze the source closure, scripts, executable, input corpus, AIGs, case timeout, and initially empty result file. In fresh case processes, direct packed AST evaluation, ordinary CM IR packed evaluation, and every returned pair token agreed with the BLIF truth table on all 71 cases; there were no failures or timeouts.
 715 
 716 Under the requested \texttt{hybrid} strategy, four of 71 selected roots were pure structural, one was a whole-root retabulation, and 66 returned ordinary fallback. All five non-fallback roots had two syntactic support variables; the other 66 had three to twelve. Under \texttt{pure\_structural}, the outcome counts were four pure and 67 fallback; under explicit \texttt{retabulate}, they were five whole-root retabulations and 66 fallback. These fractions describe the prespecified selected cohort, not all EPFL outputs or circuits generally.
 717 
 718 A separate v5 protocol was frozen before natural-case timing. It compares resident Python production of the \emph{full packed truth bitset} from the unchanged AST: direct packed evaluation against hybrid pair compilation and, where the root has no pair, ordinary CM IR construction and evaluation. Both arms include their own production and clear documented caches outside the timer; every timed invocation checks the complete bitset against the source BLIF oracle. Each case was assigned 15 randomized paired repetitions after warm-up and calibration. One adder output, \texttt{f[1]}, failed the frozen 100~ms calibration floor after its single allowed retarget and has no timed repetitions. The failure remains in the denominator. The other 70 cases have 2,100 complete arm/repetition rows, and no truth disagreement or timed-process timeout. This is a descriptive secondary result: cases cluster within ten designs, overlap earlier P1--P14 families, and do not supply independent population draws or a new primary utility test.
 719 
 720 Across the 70 complete cases, the median of case-level direct/CM producer-time ratios is 0.0376; direct packed evaluation is faster on all 70. Within the frozen hybrid-root strata, the median ratios are 0.240 for four pure structural cases, 0.112 for the one whole-root retabulation, and 0.0360 for 65 ordinary fallbacks. These are ratios of each case's median per-call times, not a ratio of pooled time totals. Fresh-process peak working set was recorded for both Python arms on all 71 cases; the median relative CM increase is $-0.15\%$, too small against shared interpreter/import memory to establish an allocation advantage. Power scheme and affinity matched the before/after records, without proving constancy throughout measurement.
 721 
 722 The pinned ABC executable also ran fresh-process \texttt{read\_blif; strash; dc2; write\_aiger} for 15 repetitions on each of the 71 cones. All 1,065 exported AIGs passed exhaustive truth checking. The median case-level ABC subprocess wall time is 304~ms, including startup and export; the coarse per-phase diagnostics often round to zero. Python AIGER parsing and exhaustive simulation were measured separately and are not native ABC query time. These ABC measurements cannot form a speed ratio with the resident Python producer times. ABC process memory, an applicable ROBDD/generic comparator, sharing, prepared reuse, alternative output contracts, independent natural families, and a complete matched protocol-v3 systems campaign remain open. No secondary result replaces the failed synthetic primary rule.
 723 
 724 S1/S2, P14-PY0, and later project-wide architecture runs answer other questions; none is used to overwrite the failed synthetic primary rule.
 725 
 726 \section{Discussion}
 727 \label{sec:discussion}
 728 
 729 \subsection{What the CM representation specifically contributes}
 730 
 731 The raw four truth values are not new. The computationally useful structure is the combination of a compact token with an explicit frame. That representation provides four practical properties.
 732 
 733 First, \emph{Boolean legality is local}: for valid child tokens, equality of canonical row/column metadata certifies same-frame Boolean fusion. The numerical contracts in Section~\ref{sec:soft-boundary} require additional checks. Second, signed normalization is fixed and cheap after recognition: transpose and row/column swaps act directly on four bits. Third, the fused result remains another four-bit token in the same frame, so the rewrite composes without expanding the operands. Fourth, provenance can say whether the token was derived structurally, retabulated, or assembled from both mechanisms.
 734 
 735 A generic optimizer can implement the same semantic reduction with a different representation. The question is therefore not whether CM has exclusive access to the reduction, but whether the CM/frame organization lowers the engineering cost of recognizing and composing it in a larger compiler. That engineering benefit is a research question, not an established result. The demonstrated contribution here is the explicit contract plus regression cases that expose otherwise easy-to-miss integration errors; the elementary identities and fragment induction do not establish substantial algorithmic novelty.
 736 
 737 \subsection{When folding can help}
 738 
 739 Folding is most plausible when the same two live operands recur through multiple signed/order variants, when expansion would otherwise repeat symbolic work, when the result will be reused, or when an admitted root can be collapsed before an expensive downstream representation is built. Exploiting pair children below a rejected root would require a persistent rewrite pass beyond this wrapper. The S1/S2 sharing strata provide a direct illustration: the largest observed reductions occur where repeated/local structure gives the small-function rewrite something to eliminate.
 740 
 741 The same mechanism becomes less attractive when compatible pairs are rare, support discovery rescans rejected subtrees, a sharing-aware baseline evaluates unique DAG nodes once, a one-shot call cannot amortize preparation, or the requested output forces a much larger materialization. The later project-wide wrapper and BitSet results show that these overheads are not theoretical nuisances; they can dominate otherwise favorable kernel operations.
 742 
 743 \subsection{Retabulation is useful but conceptually different}
 744 
 745 Evaluating four assignments is exact for a two-variable function, but it should not be allowed to make a structural recognition rule look more powerful than it is. Retabulation consumes the subtree as a black box and reconstructs its local truth function. Structural folding instead proves that a token can be derived compositionally from recognized children and frame transforms. Both are valid compiler techniques; their costs and explanatory value differ.
 746 
 747 This is why the hybrid path has its own provenance. It allows the practical compiler to continue after a local retabulation while preserving an auditable distinction between recognition and re-evaluation.
 748 
 749 \subsection{Sharing and output type change the break-even point}
 750 
 751 An AST occurrence count can dramatically overstate work when a comparator preserves identity sharing. Reporting both $N$ and $U$ is therefore mandatory. Equal-but-separately-allocated subtrees must also be distinguished from identity-shared nodes because hash-consing or structural CSE may discover the former while simple identity memoization does not.
 752 
 753 Output type matters just as much. A four-bit token is a legitimate endpoint for a small-function compiler decision; it is not equivalent to returning a dense relation over many variables. The dense wrapper retains fixed and irrelevant ambient axes, so its allocation can exceed the table over essential variables. Conversely, if a caller asks for repeated scalar or residual queries, preserving a prepared compact representation may be more important than materializing the full vector. Break-even reuse should therefore be derived from measured setup and per-query costs, not from an isolated token-fusion benchmark.
 754 
 755 In particular, if both arms return the same token and use the same lookup cost $L$, then
 756 \[
 757  T_{\rm CM}(q)=C_{\rm CM}+qL,\qquad
 758  T_{\rm base}(q)=C_{\rm base}+qL.
 759 \]
 760 Their difference is $C_{\rm CM}-C_{\rm base}$ for every $q$: more lookups alone cannot reverse the preparation-time ordering. A genuine reuse crossover requires different retained work or per-query costs, not simply amortizing two equal lookup routines.
 761 
 762 \subsection{What the negative synthetic result means}
 763 
 764 The negative v4 result does not invalidate the soundness theorem or the observation that local folding can reduce symbolic work. It shows that, for this synthetic signed grammar and token-output task, the current frame-aware implementation does not repay its production cost against direct packed evaluation. The separate natural v5 result shows an even wider descriptive gap for full-bitset production in the selected cohort, dominated by ordinary fallback. Neither comparison isolates which compiler phase causes the gap. Together they narrow the useful engineering claim and make the paper a compiler-mechanism and evaluation-boundary study.
 765 
 766 Conversely, a positive result should remain scoped to the exact output, reuse, sharing, and workload region that passes the frozen rule. The later architecture campaigns demonstrate why a task map is more informative than a universal ratio.
 767 
 768 \section{Limitations}
 769 
 770 The current compiler intentionally recognizes a narrow class of two-operand local structure. It does not solve general Boolean equivalence, NPN canonicalization, LUT mapping, AIG rewriting, or broad superoptimization. Its support-discovery implementation can have a quadratic worst case on rejected structures. The implementation uses a host-language recursive traversal and therefore imposes an explicit height bound on skewed benchmark cells rather than relying on an increased recursion limit.
 771 
 772 The S1/S2 corpus is synthetic/exploratory and contains only sixteen possible semantic functions on a fixed two-variable support; large two-variable trees measure syntactic redundancy and compiler behavior rather than growing semantic complexity. The v4 primary cases are likewise synthetic, deliberately unshared and restricted to two live variables; their narrow negative comparison does not establish the effect on natural circuits or prepared workloads. V4 excludes import/startup time from both production timers and uses process peak working set, which is insensitive to small allocations beneath a shared interpreter baseline. P14-PY0 measures ANF lowering rather than the packed-token endpoint. The later August/September project records use still other task contracts. The selected EPFL cohort supplies one bounded natural admission and secondary producer-timing result, but not a general prevalence or performance estimate. One of 71 cones failed timing calibration, and ABC startup-inclusive process wall is not task-matched to Python production time.
 773 
 774 Finally, a full relation over $n$ unfixed variables has $2^n$ entries, but this API retains $m$ ambient axes and materializes $2^m$ entries, even when fixed or irrelevant coordinates repeat. This is an output-contract cost, not a claim that the repeated data are information-theoretically necessary. CM layout does not remove the cost of the requested explicit representation. Compression, symbolic sharing, and partial-query benefits must be evaluated as separate representation or task properties.
 775 
 776 \section{Conclusion}
 777 
 778 The computational role of correspondence matrices is most defensible when stated narrowly. A four-bit binary operator token becomes useful to a compiler when its operand frame is typed. Signed and swapped occurrences can then be transported to a canonical frame, compatible tokens can be fused before operand evaluation or expansion, and unsupported structures can be retabulated or returned to an ordinary IR without compromising correctness.
 779 
 780 The evidence draws an equally important boundary. Local small-function folding can reduce pre-expansion work, but a matched generic optimizer can reproduce the same symbolic reductions. A frozen dispatcher campaign shows that even very profitable local choices can lose overall once decision overhead is charged. The frozen synthetic pair-token comparison now adds a direct negative result: on its $N=U=1023$ signed primary cell, the direct packed evaluator produces the same token at roughly one quarter of CM's time. Later project-wide benchmarks reinforce the need for task-matched endpoints, but none changes this primary outcome.
 781 
 782 The next empirical question is therefore precise: whether a different natural corpus admits this structural path often enough to matter, and whether any output, sharing, or reuse regime repays its recognition and preparation costs. The selected EPFL cohort shows limited root admission and slower CM full-bitset production on every timed cone under the present wrapper. A completed broader, task-matched circuit study can test other contracts without requiring any claim that the underlying truth-table operations are uniquely CM-specific.
 783 
 784 \appendix
 785 
 786 \section{Compact proof details}
 787 
 788 \subsection{Signed transformations}
 789 
 790 Left multiplication by $P$ exchanges the two rows of $[\Theta]$, so the row-$x$, column-$y$ entry becomes the original row-$\neg x$, column-$y$ entry, which is $(\neg x)\Theta y$. Right multiplication exchanges columns. Transposition exchanges the two assignments. Because $P$ is a permutation matrix under XOR--AND multiplication, no multi-term cancellation occurs in these reindexings.
 791 
 792 \subsection{Hybrid induction}
 793 
 794 For pure structural derivations, primitive normalization is the base case and Equations~\eqref{eq:neg-rule}--\eqref{eq:fuse-rule} preserve Equation~\eqref{eq:invariant}. For a hybrid derivation, exact local tabulation supplies an additional sound base case. Every parent above that base is again token complement or same-frame fusion. Thus hybrid provenance records how the token was obtained but does not alter its denotation.
 795 
 796 \subsection{Uniqueness of tabulated token}
 797 
 798 Fix $R,C$. Any binary Boolean function on those two variables is determined by its four values on $(1,1),(1,0),(0,1),(0,0)$. Storing those values in the declared true-first token order therefore produces the unique token that agrees with the source expression on every assignment.
 799 
 800 \section{Artifact availability, evidence status, and remaining gate}
 801 \label{sec:availability}
 802 
 803 The dated revision package contains this source/PDF, the received summary and full audit bundle, a finding-ID resolution matrix, and a \texttt{reproducibility} directory. The latter includes a source/import closure at the pinned commit (Git blob and SHA-256 checks), the immutable protocol-v3 plan, 33 contract cases, two upstream test files, byte-preserved historical evidence, and fresh test/recount logs with environment versions. A separate \path{03_STUDY_DESIGN_20260926} directory contains the frozen v4 protocol, 64-case manifest, source/environment hashes, append-only timing and memory rows, analyzer, independent recount, and historical P14 bootstrap replay. The \path{04_NATURAL_CIRCUIT_EXTENSION_20260926} directory contains the original EPFL source files, admission screen, pinned ABC tool, 71 exported AIGs, and frozen raw correctness outcomes. The \path{05_NATURAL_TIMING_20260926} directory contains the frozen v5 secondary protocol, raw Python and ABC timing rows, retained failure, descriptive analysis, and an independent row recount. From the revision's reproducibility directory, the portable correctness/recount command is:
 804 \begin{lstlisting}
 805 python run_checks.py
 806 \end{lstlisting}
 807 The runner verifies snapshot hashes, runs the 123 selected tests, recounts the recovered records, and reruns the supplied reference checker without executing historical timing workers. The complete runner passed in a fresh Python 3.10.11 virtual environment without system site packages or optional backends; \texttt{requirements-checks-lock.txt} records its transitive dependency versions. Separate analysis and reference-check commands are \texttt{python check\_historical.py} and \texttt{python check\_audit.py}. The P14 interval replay uses the archived seed and raw rows without importing its historical compiler; the v4 study has its own frozen run and analysis files. V5's \texttt{verify\_run001.py} independently checks raw-row counts, pair coverage, truth digests, hashes, and the reported median. \texttt{verify\_manifest.py}, run from the revision directory, checks the delivered file manifest; \texttt{build.py} builds the manuscript with pdfLaTeX. The obsolete checker under the preserved historical manuscript is not the entry point for this revision.
 808 
 809 A separate supplementary diagnostic under \path{reproducibility/semantic_boundary_20261013} contains \texttt{semantic\_contract\_checker.py} and its exact-rational result record. It checks 12,288 bounded compositions and examples supporting Section~\ref{sec:soft-boundary}; its 42,918 assertions concern these elementary semantic bridges, not the pinned compiler implementation, training, novelty, or a numerical performance advantage. Run \texttt{python semantic\_contract\_checker.py} from that supplementary directory. The original 123-test compiler suite and historical freezes retain their distinct scope. A subsequent adversarial audit is recorded under \path{reproducibility/semantic_boundary_audit_20261013}, including exact checks of the domain, event-identity, gradient and crispification distinctions; it preserves the preceding supplement as historical evidence.
 810 
 811 \begin{table}[H]
 812 \small\centering
 813 \begin{tabularx}{\linewidth}{@{}p{0.25\linewidth}XX@{}}
 814 \toprule
 815 \textbf{Evidence} & \textbf{Established in this revision} & \textbf{Still not established}\\
 816 \midrule
 817 Compiler contract & Pinned source, 123 passing selected tests, explicit failures and output shapes. & Historical 116-test execution identity; unrestricted runtime assurance.\\
 818 S1/S2 & Corrected CSV, generators/scripts recovered; counts and seven-metric tie recounted. & New timing evidence or CM-specific superiority.\\
 819 P14-PY0 & Raw rows, freezes and analyzers recovered; all 17 bootstrap interval sets reproduced; eight freeze hashes match. & Historical imported-runtime execution identity remains uncertified.\\
 820 Protocol v4 & 64 held-out synthetic cases, 3,840 timing rows, 128 memory rows; failed primary utility rule. & Natural findings cannot replace this primary result; sharing, reuse and full process-start costs.\\
 821 Natural gate and v5 & 2,861 original outputs screened; 71 admitted cones and ABC timing/correctness complete; 70 paired Python timing cases, one calibration failure, all 70 favor direct packed. & Matched ABC/ROBDD producer costs and memory, broader prevalence, alternative contracts, independent families.\\
 822 Protocol v3 & Original broad plan preserved. & Natural/circuit campaign and broader workload map.\\
 823 \bottomrule
 824 \end{tabularx}
 825 \caption{Evidence recovery is distinguished from new experimental execution.}
 826 \end{table}
 827 
 828 The current package closes the local manuscript--contract-test--source chain, the historical raw-record--bootstrap analysis, the synthetic v4 primary study, and a bounded natural admission, correctness, and secondary producer-timing gate. It is not a complete natural-circuit performance artifact release. Before serious submission, measure task-matched synthesis comparators and other secondary contracts on separately frozen runs, identify the historical imported runtime used for P14 timing, and provide a stable public archive identifier with dependency and corpus licensing/provenance. No public release was performed for this revision.
 829 
 830 \begin{thebibliography}{99}
 831 \raggedright
 832 
 833 \bibitem{Bricken1997}
 834 William Bricken.
 835 \newblock \emph{Notes on Matrix Techniques for Logic}.
 836 \newblock Technical note internally dated March 1997; original public-release date and peer-reviewed status not established.
 837 \newblock \url{https://wbricken.com/pdfs/01bm/01math/03math-supporting/math-tangential/04matrix-tech.pdf}.
 838 
 839 \bibitem{Bryant1986}
 840 Randal E. Bryant.
 841 \newblock Graph-based algorithms for Boolean function manipulation.
 842 \newblock \emph{IEEE Transactions on Computers}, C-35(8):677--691, 1986.
 843 \newblock doi:10.1109/TC.1986.1676819.
 844 
 845 \bibitem{Cheng2011}
 846 Daizhan Cheng, Yin Zhao, and Xiangru Xu.
 847 \newblock Matrix approach to Boolean calculus.
 848 \newblock In \emph{Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference}, pages 6950--6955, 2011.
 849 \newblock doi:10.1109/CDC.2011.6160289.
 850 
 851 \bibitem{Droncheff2018}
 852 Brian Droncheff.
 853 \newblock \emph{Correspondence Matrices; Algorithms for Propositional Logic}.
 854 \newblock ResearchGate preprint, 2018.
 855 \newblock doi:10.13140/RG.2.2.28036.37764.
 856 
 857 \bibitem{Edwards1972}
 858 C. R. Edwards.
 859 \newblock The logic of Boolean matrices.
 860 \newblock \emph{The Computer Journal}, 15(3):247--253, 1972.
 861 \newblock doi:10.1093/comjnl/15.3.247.
 862 
 863 \bibitem{Lee2022}
 864 Siang-Yun Lee, Heinz Riener, Alan Mishchenko, Robert K. Brayton, and Giovanni De Micheli.
 865 \newblock A simulation-guided paradigm for logic synthesis and verification.
 866 \newblock \emph{IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems}, 41(8):2573--2586, 2022.
 867 \newblock doi:10.1109/TCAD.2021.3108704.
 868 
 869 \bibitem{Mishchenko2006}
 870 Alan Mishchenko, Satrajit Chatterjee, and Robert K. Brayton.
 871 \newblock DAG-aware AIG rewriting: A fresh look at combinational logic synthesis.
 872 \newblock In \emph{Proceedings of the 43rd Design Automation Conference}, pages 532--535, 2006.
 873 \newblock doi:10.1145/1146909.1147048.
 874 
 875 \bibitem{KittyOperations}
 876 Kitty project.
 877 \newblock \emph{Operations: truth-table predicates and manipulation}.
 878 \newblock Official documentation, accessed 26 September 2026; documentation version is not a benchmarked binary version.
 879 \newblock \url{https://libkitty.readthedocs.io/en/latest/operations.html}.
 880 
 881 \bibitem{MockturtleCut}
 882 Mockturtle project.
 883 \newblock \emph{Cut rewriting}.
 884 \newblock Official documentation, accessed 26 September 2026.
 885 \newblock \url{https://mockturtle.readthedocs.io/en/latest/algorithms/cut_rewriting.html}.
 886 
 887 \bibitem{CompilerSnapshot2026}
 888 Correspondence Matrices Project.
 889 \newblock \emph{Pair compiler implementation}, commit \texttt{0ab8ffd0c23ffa71ee951d375b1c170ffdcc084b}.
 890 \newblock \url{https://github.com/Relative0/Correspondence_Matrices/tree/0ab8ffd0c23ffa71ee951d375b1c170ffdcc084b}.
 891 \newblock Source closure and hash manifest included in this revision package.
 892 
 893 \bibitem{ProtocolV3}
 894 Correspondence Matrices Project.
 895 \newblock \emph{Evaluation protocol v3}, 15 September 2026, pre-freeze/unexecuted.
 896 \newblock \path{paper_program/01_audit/EVALUATION_PROTOCOL_V3.md}, at the commit in \cite{CompilerSnapshot2026}; byte-identical copy included in the source snapshot.
 897 
 898 \bibitem{ProtocolV4}
 899 Brian Theory.
 900 \newblock \emph{Protocol v4: signed pair compiler, synthetic primary cell}, 26 September 2026.
 901 \newblock Dated local study package \path{03_STUDY_DESIGN_20260926}; frozen plan, manifest, raw rows and analysis included.
 902 
 903 \bibitem{NaturalAdmission2026}
 904 Brian Theory.
 905 \newblock \emph{Natural-circuit admission and correctness gate}, 26 September 2026.
 906 \newblock Dated local study package \path{04_NATURAL_CIRCUIT_EXTENSION_20260926}; source, admission screen, ABC/AIG exports, frozen correctness run and raw outcomes included.
 907 
 908 \bibitem{Mizraji1992}
 909 Eduardo Mizraji.
 910 \newblock Vector logics: The matrix--vector representation of logical calculus.
 911 \newblock \emph{Fuzzy Sets and Systems}, 50(2):179--185, 1992.
 912 \newblock doi:10.1016/0165-0114(92)90216-Q.
 913 
 914 \bibitem{Mizraji2008}
 915 Eduardo Mizraji.
 916 \newblock Vector logic: A natural algebraic representation of the fundamental logical gates.
 917 \newblock \emph{Journal of Logic and Computation}, 18(1):97--121, 2008.
 918 \newblock doi:10.1093/logcom/exm057.
 919 
 920 \bibitem{ProjectCorrection20260825}
 921 Correspondence Matrices Project.
 922 \newblock \emph{CM benchmark audit correction --- 2026-08-25}.
 923 \newblock Public technical record, 25 August 2026.
 924 \newblock \url{https://github.com/Relative0/Correspondence_Matrices/blob/main/deliverables_n22_24/corrections_2026_08_25/CM_BENCHMARK_AUDIT_CORRECTION_REPORT_2026-08-25.md}.
 925 
 926 \bibitem{ProjectArchitecture20260903}
 927 Correspondence Matrices Project.
 928 \newblock \emph{Architecture-aware CM comparison refresh after C37}.
 929 \newblock Public technical record, 3 September 2026; updated 4 September 2026.
 930 \newblock \url{https://github.com/Relative0/Correspondence_Matrices/blob/main/docs/research/CM_ARCHITECTURE_AWARE_COMPARISON_REFRESH_AFTER_C37_2026_09_03.md}.
 931 
 932 \bibitem{Sasnauskas2017}
 933 Raimondas Sasnauskas et al.
 934 \newblock Souper: A synthesizing superoptimizer.
 935 \newblock arXiv:1711.04422, 2017.
 936 
 937 \bibitem{Stern1988}
 938 August Stern.
 939 \newblock \emph{Matrix Logic: Theory and Applications}.
 940 \newblock North-Holland, 1988.
 941 
 942 \bibitem{Testa2019}
 943 Eleonora Testa, Mathias Soeken, Luca Gaetano Amar\`u, and Giovanni De Micheli.
 944 \newblock Logic synthesis for established and emerging computing.
 945 \newblock \emph{Proceedings of the IEEE}, 107(1):165--184, 2019.
 946 \newblock doi:10.1109/JPROC.2018.2869760.
 947 
 948 \bibitem{TheoryFoundations2026}
 949 Brian Theory.
 950 \newblock \emph{Correspondence and Logical Matrices: A Boolean Operator Calculus: Formula-valued logical matrices, valuation, pairing, and coherent operator superposition}.
 951 \newblock Companion research draft, 22 September 2026.
 952 
 953 \bibitem{Willsey2021}
 954 Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha.
 955 \newblock egg: Fast and extensible equality saturation.
 956 \newblock \emph{Proceedings of the ACM on Programming Languages} (POPL), 2021.
 957 \newblock arXiv:2004.03082.
 958 
 959 \bibitem{Zhou2019}
 960 Xuegong Zhou, Lingli Wang, and Alan Mishchenko.
 961 \newblock Fast adjustable NPN classification using generalized symmetries.
 962 \newblock \emph{ACM Transactions on Reconfigurable Technology and Systems}, 12(2):7, 2019.
 963 \newblock doi:10.1145/3313917.
 964 
 965 \bibitem{Kimmig2017}
 966 Angelika Kimmig, Guy Van den Broeck, and Luc De Raedt.
 967 \newblock Algebraic model counting.
 968 \newblock \emph{Journal of Applied Logic}, 22:46--62, 2017.
 969 \newblock doi:10.1016/j.jal.2016.11.031.
 970 
 971 \bibitem{Stehr2022}
 972 Mark-Oliver Stehr, Minyoung Kim, and Carolyn L. Talcott.
 973 \newblock A probabilistic approximate logic for neuro-symbolic learning and reasoning.
 974 \newblock \emph{Journal of Logical and Algebraic Methods in Programming}, 124:100719, 2022.
 975 \newblock doi:10.1016/j.jlamp.2021.100719.
 976 
 977 \bibitem{Xu2018}
 978 Jingyi Xu, Zilu Zhang, Tal Friedman, Yitao Liang, and Guy Van den Broeck.
 979 \newblock A semantic loss function for deep learning with symbolic knowledge.
 980 \newblock \emph{Proceedings of Machine Learning Research}, 80:5502--5511, 2018.
 981 \newblock \url{https://proceedings.mlr.press/v80/xu18h.html}.
 982 
 983 \end{thebibliography}
 984 
 985 \end{document}