Differentiable Horn Programs: A Constructive Expressivity Theorem for Latent Rule Operators

We introduce $\text{textsc}LatentGamma$, a differentiable operator on the unit cube $[0,1{]}^M$ designed as a smooth surrogate of Tarski’s immediate consequence operator $\text{TP}$ associated with a definite Horn program $P$ on $M$ atoms. The operator is built as a five-stage composition combining sigmoidal gating, softmax routing, and a residual update that enforces monotonicity by construction. We establish four theoretical results. First, the iterated sequence is coordinate-wise non-decreasing and bounded by $\text{ind}$, hence converges to a fixed point of $\text{textsc}LatentGamma$; the operator itself is lattice-monotone on $[0,1{]}^M$. Second, our \emph{constructive expressivity theorem} shows that for every definite Horn program $P$ there exists a closed-form parameter assignment ${\theta }^{\ast }(P)$ and an explicit time bound $T_{\max }(P)$ such that the iterated sequence \emph{exactly} reproduces $\text{TPinf}(F_0)$ for every initial fact set $F_0$ throughout the window $[D(P,F_0),T_{\max }(P)]$, where $D(P,F_0)\le M$ is the derivation depth. The window $T_{\max }$ is large in practice ($\ge {10}^5$ for sparse programs) and reflects the finite-time nature of computation by smooth sigmoidal gates. Third, the oracle is robust to Gaussian noise on its body and head logits, with explicit non-asymptotic bounds. Fourth, we prove a matching information-theoretic lower bound on the parameter count. We provide a complete numerical validation on programs ranging from $M=33$ to $M=504$ atoms: oracle accuracy reaches $1.0000$ on $2000$ test cases with zero false-positive and false-negative rates, and the empirical noise tolerance ${\sigma }_{\max }$ scales precisely as the union bound $RM\cdot \mathrm{\Phi }(-10\mathrm{/}{\sigma }_{\eta })$ predicts.