Prove Lemma 3.3 in Rocq, shorten the abstract, and set the paper in the format of the Stellarocq paper

README.md

@@ -600,7 +600,8 @@ proves for every window of 2^α cells, number of banks, bank and tape. `rocq/`
 also proves that the host family computes SUBLEQ at every word width, with its
 depth and its numbers of units and edges, the same for the family of depth 11 that
 folds the address decoders into the reads, that the levelization of every clocked
-netlist computes its step, that a read and the branch need two ternary levels, that
+netlist computes its step, that two ternary units compute the branch and a read and
+the branch need two ternary levels, that
 the recipes and their encoder have the stated lengths, that the 21- and
 27-instruction programs do what the paper states at every word width from 8 on, and
 that the H_8 it defines is the netlist of the published serialization.

paper/runs/paper_rocq.json

@@ -1,7 +1,7 @@
 {
  "rocq": "The Rocq Prover, version 9.1.1",
  "files": 66,
- "build_seconds": 102.9,
+ "build_seconds": 101.6,
  "theorems": {
   "PhysSem.netlist_step": "closed",
   "PhysMain.network_orbit": "closed",
@@ -94,6 +94,7 @@
   "Lower.read_needs_two_levels": "reals",
   "Lower.onehot_needs_two_levels": "reals",
   "Lower.branch_not_ternary": "closed",
+  "Lower.branch_unit": "closed",
   "Margin.margin": "reals",
   "Margin.margin_tight": "reals",
   "Margin.mismatch_all": "reals",
@@ -144,7 +145,7 @@
   "AmpHost.amp_selfrep": "closed"
  },
  "extraction_identical": true,
- "lines": 24178,
+ "lines": 24230,
  "host_extraction": {
   "members": [
    {

paper/universal_construction_ternary.pdf

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:305f38033584a59bc3532f2d7e92bf7fa8d96afbf75a9eebebaf387766b41b01
-size 369468
+oid sha256:dc252d176a48dce307c85088813dd89a501c9ef564d9a50d8929e4643cc16cb6
+size 350822

paper/universal_construction_ternary.tex

@@ -1,19 +1,26 @@
 % !TEX program = pdflatex
-\documentclass[11pt]{amsart}
-
-\usepackage[utf8]{inputenc}
-\IfFileExists{lmodern.sty}{\usepackage[T1]{fontenc}\usepackage{lmodern}}{}
+\documentclass[11pt]{article}
+\setlength{\textwidth}{6.5in}
+\setlength{\oddsidemargin}{0pt}
+\setlength{\evensidemargin}{0pt}
+\setlength{\textheight}{9in}
+\setlength{\topmargin}{0pt}
+\addtolength{\topmargin}{-\headheight}
+\addtolength{\topmargin}{-\headsep}
+\ifdefined\pdfpagewidth \pdfpagewidth=8.5in \pdfpageheight=11in \fi
+\ifdefined\pagewidth \pagewidth=8.5in \pageheight=11in \fi
 \usepackage{amsmath,amssymb,amsthm,mathtools}
-\usepackage{booktabs,tabularx,array}
-\usepackage{cite}
+\usepackage{tabularx,array}
 \usepackage{enumitem}
 \usepackage{tikz}
 \usetikzlibrary{arrows.meta,calc}
 \usepackage{pgfplots}
 \pgfplotsset{compat=1.18}
-\usepackage[margin=1in]{geometry}
-\setlength{\emergencystretch}{2em}
-\usepackage[colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}
+\emergencystretch=3em
+\makeatletter
+\def\tc@slash{/}
+\newcommand{\link}[1]{\texttt{\@tfor\tc@t:=#1\do{\tc@t\ifx\tc@t\tc@slash\allowbreak\fi}}}
+\makeatother
 
 % ---- theorem environments ---------------------------------------------------
 \newtheorem{theorem}{Theorem}[section]
@@ -50,57 +57,32 @@
 \DeclareMathOperator{\popcount}{popcount}
 
 % ---- front matter -----------------------------------------------------------
-\title[Universal construction and self-reproduction in ternary threshold networks]
-      {Universal Construction and Exact Self-Reproduction\\ in Ternary McCulloch--Pitts Networks}
-
+\title{Universal Construction and Exact Self-Reproduction\\ in Ternary McCulloch--Pitts Networks}
 \author{Charles Norton}
-\date{\today}
-
-\subjclass[2020]{Primary 68Q06; Secondary 68T07, 92B20, 94C11}
-\keywords{McCulloch--Pitts networks, threshold circuits, ternary weights,
-self-reproducing automata, universal constructor, noise margin}
+\date{}
 
 \begin{document}
+\maketitle
 
 \begin{abstract}
-We study recurrent networks of McCulloch--Pitts threshold units with weights in
-$\{-1,0,1\}$ and integer thresholds, iterated as a fixed composition of ternary
-matrix--vector products and Heaviside steps, and construct networks of this kind
-that carry out von Neumann's universal construction and self-reproduction exactly.
-A SUBLEQ computer of $17{,}598$ units belongs to a family whose step has depth $13$
-and is proved in Rocq to be the step of SUBLEQ at every word width. It runs a
-program of $21$ instructions that emits any byte string from a run-length
-description, and one of $27$ instructions that decodes a description and then
-copies it; both are proved in Rocq for every word width from $8$ on. With the
-second, the computer emits the serialization of its own weights, memory and tape.
-A second network, fixed once and for all, interprets stored networks: its state
-holds a ring of $K$ banks of records and $K$ tapes, each step evaluates one record,
-and its netlist is proved in Rocq to compute this machine for every number and size
-of banks and tapes. Stored in the ring as $36{,}080$ records of two inputs, the
-SUBLEQ computer decodes a description of its own records into the next bank, copies
-the description onto the next tape and hands control to the copy. The fixed network
-thus rebuilds the stored computer, weights included, in every generation. For every
-word width from $8$ on and every ring it is proved in Rocq that the stored computer
-builds every
-image that fits a bank from a description of it, and that, started on its own, it
-reproduces: the copies accumulate until every bank holds one, and from then on the
-whole state repeats every $K$ generations. A constructor of $143$ records with a
-description code of its own does the same, also proved in Rocq.
-Every pre-activation is an integer, so every orbit survives perturbations below
-$1/2$ of each pre-activation. Under independent Gaussian noise on the
-pre-activations, a bound computed from the orbit lies within the $95\%$ interval of
-the measured failure rate at every noise level at which failures were observed.
-Replicating every unit $r$ times multiplies every margin by $r$: under noise on the
-pre-activations, which does not grow with fan-in, every noise level is survived
-with $r=O(s\sqrt{\log(TM/\delta)})$. Under von Neumann's independent output flips a
-threshold appears: the same redundancy is reliable for flip probabilities below
-$1/(2ek)$, $k$ the largest fan-in, and above $1/(2k)$ a disjunction of fan-in $k$
-fails with a probability that tends to one as $r$ grows. The margin, the noise bounds
-and the threshold are proved in Rocq.
+We construct networks of McCulloch--Pitts threshold units with weights in
+$\{-1,0,1\}$ that carry out von Neumann's universal construction and
+self-reproduction exactly. A SUBLEQ computer of $17{,}598$ units, the eight-bit
+member of a family of depth $13$, runs a program of $21$ instructions that builds
+any byte string from a run-length description, and one of $27$ instructions with
+which it emits the serialization of its own weights, memory and tape. A second,
+fixed network holds threshold networks as records in a ring of banks and tapes and
+evaluates one record per step. Stored in it as $36{,}080$ records, the SUBLEQ
+computer builds any image that fits a bank from a description of it and, started on
+its own description, rebuilds itself, weights included, in every generation; a
+constructor of $143$
+records with a description code of its own does the same. Integer pre-activations
+give every orbit a margin of $1/2$, and replicating each unit $r$ times multiplies
+it by $r$. That suffices against noise of any size on the pre-activations, but
+against von Neumann's output flips only below a threshold inversely proportional to
+the fan-in. These results are proved in Rocq.
 \end{abstract}
 
-\maketitle
-
 % =============================================================================
 \section{Introduction}\label{sec:intro}
 % =============================================================================
@@ -214,13 +196,13 @@ of the threefold host where the first-order bound exceeds one
 \begin{table}[ht]
 \centering\small
 \begin{tabularx}{\textwidth}{@{}>{\raggedright\arraybackslash}p{0.36\textwidth}>{\raggedright\arraybackslash}p{0.2\textwidth}>{\raggedright\arraybackslash}X@{}}
-\toprule
+\hline
 Claim & Where & Evidence\\
-\midrule
+\hline
 Levelization; the sizes of $\Lev(\Nhost)$ & Lem.~\ref{lem:lev}, Rem.~\ref{rem:levsizes} & Rocq\\
 The step of $H_A$ is the step of $\mathrm{SUBLEQ}_A$, every $A\ge3$ & Prop.~\ref{prop:host} & Rocq; the netlists extracted for $A=8,9,10$ equal the generator's\\
 Depth $13$, units, edges, weights and biases of $H_A$, every $A\ge3$ & Prop.~\ref{prop:host} & Rocq; rebuilt independently for $A=3$ to $12$\\
-A read and the branch need two ternary levels & Lem.~\ref{lem:muxdepth}, Rem.~\ref{rem:ternarydepth} & Rocq; exhaustive search on eight inputs\\
+The branch unit; a read and the branch need two ternary levels & Lems.~\ref{lem:branch}, \ref{lem:muxdepth}, Rem.~\ref{rem:ternarydepth} & Rocq; exhaustive search on eight inputs\\
 The folded host: its step, depth $11$, units and edges, every $A\ge3$ & Rem.~\ref{rem:fold} & Rocq; random states for $A=3$ to $12$\\
 Length and optimality of the recipes and of $\describe$ & Lems.~\ref{lem:complete}, \ref{lem:describe}, Prop.~\ref{prop:optimal} & Rocq; checked on $971$ MB and on $68{,}061$ boundary strings\\
 $P$ builds every string, in the stated steps, every $A\ge8$ & Thm.~\ref{thm:univ} & Rocq; $29$ recipes run on the reference and four on the netlist\\
@@ -235,7 +217,7 @@ A pass of the stored host, every $A\ge8$ & Prop.~\ref{prop:storedpass} & Rocq, b
 Construction and reproduction by the stored host: copies, period, network, counts, every $A\ge8$ & Thms.~\ref{thm:storedconstruct}--\ref{thm:widths} & Rocq; the extracted image equal to the generator's for $A=8,9$; six generations of $\mathcal S_8$ run\\
 The stored host under noise & Cor.~\ref{cor:storednoise} & Rocq\\
 The organism: code, pass, construction, copies, period, network & Lem.~\ref{lem:code}, Prop.~\ref{prop:pass}, Thms.~\ref{thm:construct}, \ref{thm:organism} & Rocq; six generations run, one on the netlist\\
-\bottomrule
+\hline
 \end{tabularx}
 \caption{The claims of the paper and the evidence for each: the proof checked in Rocq,
 and the computations and runs recorded in the artifact.}
@@ -388,9 +370,9 @@ point; $F$ treats the device cells as ordinary memory.
 \begin{table}[ht]
 \centering\small
 \begin{tabular}{@{}llll@{}}
-\toprule
+\hline
 Address & Symbol & Role & Effect \\
-\midrule
+\hline
 \cell{0xF9} & $c_{\mathrm{wr}}$  & write request     & value $1$ emits $R_{\mathrm{out}}$ and clears it\\
 \cell{0xFA} & $c_{\mathrm{eot}}$ & end-of-tape status& set by a read at $h=|\tau|$, cleared by a read at $h<|\tau|$\\
 \cell{0xFB} & $c_{\mathrm{rw}}$  & rewind request    & value $1$ sets $h=0$\\
@@ -398,7 +380,7 @@ Address & Symbol & Role & Effect \\
 \cell{0xFD} & $R_{\mathrm{in}}$  & input register    & written by the device\\
 \cell{0xFE} & $R_{\mathrm{out}}$ & output register   & written by the program, cleared on emit\\
 \cell{0xFF} & --                 & halt              & the machine halts when $p=255$\\
-\bottomrule
+\hline
 \end{tabular}
 \caption{Memory-mapped device cells of the host transducer.}
 \label{tab:device}
@@ -555,7 +537,8 @@ the branch condition $[r\le 0]$ equals $\Hv(r_7+z(r)-1)$.
 
 \begin{proof}
 $-\sum_i r_i\ge 0$ holds exactly when every $r_i=0$. The value $r$ is at most $0$
-exactly when $r=0$ or $r_7=1$, so $[r\le 0]=\mathrm{OR}(r_7,z(r))$.
+exactly when $r=0$ or $r_7=1$, so $[r\le 0]=\mathrm{OR}(r_7,z(r))$. The lemma is
+proved in Rocq for words of every width.
 \end{proof}
 
 \begin{remark}[Ternary weights cost one level at the branch]\label{rem:ternarydepth}
@@ -645,9 +628,9 @@ The host is $\Nhost=H_8$.
 \begin{table}[ht]
 \centering\small
 \begin{tabular}{@{}lrcl@{}}
-\toprule
+\hline
 Block & Units & Layer & Computes\\
-\midrule
+\hline
 $P_j$ & $2^A$ & 1 & decode lines of $p$\\
 $HP_i$ & $A$ & 1 & $h\wedge p_i$\\
 $FA_{o,t,j}$ & $3A2^A$ & 2 & $\mu_{j+o,t}\wedge P_j$\\
@@ -665,7 +648,7 @@ $\mathrm{LEQ}$ & $1$ & 11 & $[r\le0]$\\
 $TA_i$, $TB_i$, $NP_i$ & $3A$ & 12--13 & next counter\\
 $HA$, $HB$, $NH$ & $3$ & 12--13 & next halt bit\\
 $WR_{j,t}$, $NM_{j,t}$ & $2A2^A$ & 12--13 & next memory (9--10 for $t=0$)\\
-\bottomrule
+\hline
 \end{tabular}
 \caption{The blocks of $H_A$ in the order of the netlist. The layer is the depth
 of the block's units.}
@@ -942,9 +925,9 @@ elsewhere, and let
 
 \begin{table}[t]\centering\small
 \begin{tabular}{@{}rlllll@{}}
-\toprule
+\hline
 $k$ & addr & $A$ & $B$ & $C$ & effect\\
-\midrule
+\hline
 0 & \cell{0x00} & \cell{T2} & \cell{T2} & \cell{0x03} & $M[\cell{T2}]\leftarrow 0$\\
 1 & \cell{0x03} & \cell{T1} & \cell{T1} & \cell{0x06} & $M[\cell{T1}]\leftarrow 0$\\
 2 & \cell{0x06} & \cell{NEG1} & $c_{\mathrm{rd}}$ & \cell{0x09} & read request\\
@@ -973,7 +956,7 @@ $k$ & addr & $A$ & $B$ & $C$ & effect\\
 24 & \cell{0x48} & \cell{Z} & $R_{\mathrm{out}}$ & \cell{0x4B} & $M[R_{\mathrm{out}}]\leftarrow b$\\
 25 & \cell{0x4B} & \cell{NEG1} & $c_{\mathrm{wr}}$ & \cell{0x4E} & write request\\
 26 & \cell{0x4E} & \cell{Z} & \cell{Z} & \cell{0x3F} & $M[\cell{Z}]\leftarrow0$; goto \textsc{b}\\
-\bottomrule
+\hline
 \end{tabular}
 \caption{The constructor $P$ of Construction~\ref{con:P}, instructions $0$ to $20$ at
 \cell{0x00}--\cell{0x3E}, and the self-reproducing program $P^\ast$ of
@@ -1162,10 +1145,11 @@ Let the perturbations be independent centred Gaussians of standard deviation
 $s$, let $(x_t)$ be the orbit of $F$ from $x_0$, and for $t\ge0$ and each row $i$
 of each layer let $z_{t,i}$ be the pre-activation of row $i$ on the input
 $x_t$ and $d_{t,i}=|z_{t,i}+\tfrac12|$. Put
-\[
+\begin{gather*}
 b'(t)=1-\prod_i\Bigl(1-Q\bigl(d_{t,i}/s\bigr)\Bigr),\qquad
-b(t)=\sum_i Q\bigl(d_{t,i}/s\bigr),\qquad Q(u)=\Pr(\mathcal N(0,1)>u)=\tfrac12\erfc(u/\sqrt2).
-\]
+b(t)=\sum_i Q\bigl(d_{t,i}/s\bigr),\\
+Q(u)=\Pr(\mathcal N(0,1)>u)=\tfrac12\erfc(u/\sqrt2).
+\end{gather*}
 Given that a perturbed trajectory from $x_0$ agrees with the orbit up to step $t$,
 the probability that it differs from it at step $t+1$ is at most $b'(t)$, the
 probability that some row of the step fails while it reads the values of the orbit;
@@ -2500,10 +2484,11 @@ the product form does not.
 
 \begin{table}[ht]
 \centering\small
+\setlength{\tabcolsep}{5pt}
 \begin{tabular}{@{}lrrllll@{}}
-\toprule
+\hline
 $s$ & Deviated & Exposure & Measured rate, $95\%$ interval & $b'$ & $b$ & $Mp$\\
-\midrule
+\hline
 $0.06$ & 0/256 & 768{,}000 & $0$, $[0,\,4.80\times10^{-6}]$ & $1.21\times10^{-12}$ & $1.21\times10^{-12}$ & $3.30\times10^{-12}$\\
 $0.08$ & 7/256 & 1{,}008{,}916 & $6.94\times10^{-6}$, $[2.79,\,14.3]\times10^{-6}$ & $6.34\times10^{-6}$ & $6.34\times10^{-6}$ & $1.72\times10^{-5}$\\
 $0.09$ & 202/256 & 496{,}131 & $4.07\times10^{-4}$, $[3.53,\,4.67]\times10^{-4}$ & $4.27\times10^{-4}$ & $4.27\times10^{-4}$ & $1.16\times10^{-3}$\\
@@ -2512,7 +2497,7 @@ $0.11$ & 256/256 & 3{,}325 & $7.70\times10^{-2}$, $[6.79,\,8.70]\times10^{-2}$ &
 $0.12$ & 256/256 & 714 & $3.59\times10^{-1}$, $[3.16,\,4.05]\times10^{-1}$ & $3.77\times10^{-1}$ & $4.73\times10^{-1}$ & $1.30$\\
 $0.15$ & 256/256 & 256 & $1.00$, $[0.88,\,1]$ & $1.00$ & $1.30\times10^{1}$ & $3.60\times10^{1}$\\
 $0.20$ & 256/256 & 256 & $1.00$, $[0.88,\,1]$ & $1.00$ & $1.89\times10^{2}$ & $5.21\times10^{2}$\\
-\bottomrule
+\hline
 \end{tabular}
 \caption{The per-step probability that $\Lev(\Nhost)$ leaves the exact orbit under
 read noise of standard deviation $s$. One noise-free copy and $256$ noisy copies
@@ -2563,9 +2548,9 @@ $20{,}000$ steps, against $5$ of the $64$ copies.
 \begin{table}[ht]
 \centering\small
 \begin{tabular}{@{}lrrlll@{}}
-\toprule
+\hline
 $s$ & Failed & Exposure & Measured rate, $95\%$ interval & Restoration bound & $rM\erfc(r/2\sqrt2s)$\\
-\midrule
+\hline
 $0.10$ & --- & --- & --- & $8.62\times10^{-59}$ & $9.24\times10^{-46}$\\
 $0.15$ & --- & --- & --- & $4.02\times10^{-25}$ & $1.92\times10^{-18}$\\
 $0.20$ & --- & --- & --- & $3.59\times10^{-13}$ & $8.03\times10^{-9}$\\
@@ -2575,7 +2560,7 @@ $0.27$ & 5/64 & 1{,}237{,}505 & $4.04\times10^{-6}$, $[1.31,\,9.43]\times10^{-6}
 $0.30$ & 63/64 & 295{,}163 & $2.13\times10^{-4}$, $[1.64,\,2.73]\times10^{-4}$ & $2.26\times10^{-4}$ & $7.22\times10^{-2}$\\
 $0.33$ & 64/64 & 17{,}472 & $3.66\times10^{-3}$, $[2.82,\,4.68]\times10^{-3}$ & $4.34\times10^{-3}$ & $6.90\times10^{-1}$\\
 $0.36$ & 64/64 & 2{,}188 & $2.93\times10^{-2}$, $[2.25,\,3.74]\times10^{-2}$ & $4.30\times10^{-2}$ & $3.89$\\
-\bottomrule
+\hline
 \end{tabular}
 \caption{The per-step probability that the state of $N_3$ read by majority leaves the orbit under read noise of standard deviation $s$: $64$ noisy copies stepped beside an exact one from the initial state of the self-describing instance for up to $20{,}000$ steps, each stopped at its first wrong majority-read state, with the exact $95\%$ interval for a Poisson count over the exposure, against the bound $b(t)$ of Proposition~\ref{prop:restore} along the same orbit, weighted by the steps each copy ran where copies ran and averaged over the $20{,}000$ steps elsewhere, and the first-order bound of Theorem~\ref{thm:amplify}(ii).}
 \label{tab:bound3}
@@ -2612,7 +2597,7 @@ on the accelerator; it gives the sizes, depths and exact runs stated here, and n
 runs within sampling error.
 
 The Rocq development, \texttt{rocq/} in the artifact, has $66$ files and
-$24{,}178$ lines and builds with Rocq 9.1.1 in about two minutes on the machine
+$24{,}230$ lines and builds with Rocq 9.1.1 in about two minutes on the machine
 below, most of it in the kernel's evaluation of the $15{,}872$ abstract passes of
 Proposition~\ref{prop:pass} and in the device records of the stored host. It proves
 Lemma~\ref{lem:lev} for every clocked netlist. It defines the host family $H_A$
@@ -2621,7 +2606,7 @@ $A\ge3$, with its depth, its numbers of units, memory units and edges, its weigh
 and biases and the sizes of $\Lev(H_A)$ (Proposition~\ref{prop:host},
 Remark~\ref{rem:levsizes}), and does the same for the step, the depth and the
 numbers of units and edges of the folded host (Remark~\ref{rem:fold}). It proves
-Lemma~\ref{lem:muxdepth} and Remark~\ref{rem:ternarydepth}. It defines the recipes, $\describe$, the device of
+Lemmas~\ref{lem:branch} and~\ref{lem:muxdepth} and Remark~\ref{rem:ternarydepth}. It defines the recipes, $\describe$, the device of
 Definition~\ref{def:transducer} and the programs $P$ and $P^\ast$ in $2^A$ words, and
 proves Lemmas~\ref{lem:complete} and~\ref{lem:describe},
 Proposition~\ref{prop:optimal}, Theorems~\ref{thm:univ} and~\ref{thm:selfrep} and
@@ -2747,362 +2732,306 @@ with $20$ hardware threads and $31$ GiB of memory and an NVIDIA GeForce RTX 3070
 Ti Laptop GPU with $8$ GiB of memory.
 
 % =============================================================================
-\begin{thebibliography}{99}
-\setlength{\itemsep}{0pt}
+\begin{thebibliography}{99}\small\raggedright
+\setlength{\itemsep}{1pt}
 
-\bibitem{AgueraYArcas2024}
-B.~Ag\"uera y Arcas, J.~Alakuijala, J.~Evans, B.~Laurie, A.~Mordvintsev,
-E.~Niklasson, E.~Randazzo, and L.~Versari,
-\emph{Computational life: How well-formed, self-replicating programs emerge from
-simple interaction}, arXiv:2406.19108, 2024.
+\bibitem{McCullochPitts1943}
+W.~S. McCulloch and W.~Pitts, A logical calculus of the ideas immanent in nervous
+activity, \emph{Bull. Math. Biophys.} \textbf{5}, 115 (1943).
 
-\bibitem{AlonDewdneyOtt1991}
-N.~Alon, A.~K.~Dewdney, and T.~J.~Ott,
-\emph{Efficient simulation of finite automata by neural nets},
-J. ACM \textbf{38} (1991), no.~2, 495--514.
+\bibitem{vonNeumann1945}
+J.~von~Neumann, \emph{First Draft of a Report on the EDVAC} (Moore School of
+Electrical Engineering, University of Pennsylvania, Philadelphia, 1945).
 
-\bibitem{Arbib1966}
-M.~A.~Arbib,
-\emph{A simple self-reproducing universal automaton},
-Information and Control \textbf{9} (1966), 177--189.
+\bibitem{vonNeumann1966}
+J.~von~Neumann, \emph{Theory of Self-Reproducing Automata}, edited by A.~W. Burks
+(University of Illinois Press, Urbana, 1966).
 
-\bibitem{BeiuQuintanaAvedillo2003}
-V.~Beiu, J.~M.~Quintana, and M.~J.~Avedillo,
-\emph{VLSI implementations of threshold logic---a comprehensive survey},
-IEEE Trans. Neural Networks \textbf{14} (2003), no.~5, 1217--1243.
+\bibitem{Arbib1966}
+M.~A. Arbib, A simple self-reproducing universal automaton, \emph{Inf. Control}
+\textbf{9}, 177 (1966).
 
-\bibitem{BoldoLelayMelquiond2015}
-S.~Boldo, C.~Lelay, and G.~Melquiond,
-\emph{Coquelicot: A user-friendly library of real analysis for Coq}, Math. Comput.
-Sci. \textbf{9} (2015), no.~1, 41--62.
+\bibitem{Codd1968}
+E.~F. Codd, \emph{Cellular Automata} (Academic Press, New York, 1968).
 
-\bibitem{Burks1970}
-A.~W.~Burks (ed.),
-\emph{Essays on Cellular Automata}, University of Illinois Press, Urbana, 1970.
+\bibitem{Langton1984}
+C.~G. Langton, Self-reproduction in cellular automata, \emph{Physica D}
+\textbf{10}, 135 (1984).
 
-\bibitem{CabessaSiegelmann2014}
-J.~Cabessa and H.~T.~Siegelmann,
-\emph{The super-Turing computational power of plastic recurrent neural
-networks}, Int. J. Neural Systems \textbf{24} (2014), no.~8, 1450029.
+\bibitem{Pesavento1995}
+U.~Pesavento, An implementation of von Neumann's self-reproducing machine,
+\emph{Artif. Life} \textbf{2}, 337 (1995).
 
-\bibitem{ChangLipson2018}
-O.~Chang and H.~Lipson,
-\emph{Neural network quine}, ALIFE 2018, MIT Press, 2018; arXiv:1803.05859.
+\bibitem{PerrierSipperZahnd1996}
+J.-Y. Perrier, M.~Sipper and J.~Zahnd, Toward a viable, self-reproducing universal
+computer, \emph{Physica D} \textbf{97}, 335 (1996).
 
-\bibitem{ChungSiegelmann2021}
-S.~Chung and H.~T.~Siegelmann,
-\emph{Turing completeness of bounded-precision recurrent neural networks},
-Advances in Neural Information Processing Systems \textbf{34} (2021),
-28431--28441.
+\bibitem{Sipper1998}
+M.~Sipper, Fifty years of research on self-replication: An overview, \emph{Artif.
+Life} \textbf{4}, 237 (1998).
 
-\bibitem{CoatesLewis1964}
-C.~L.~Coates and P.~M.~Lewis~II,
-\emph{DONUT: A threshold gate computer},
-IEEE Trans. Electronic Computers \textbf{EC-13} (1964), no.~3, 240--247.
+\bibitem{CotlerHonglerHudcova2025}
+J.~Cotler, C.~Hongler and B.~Hudcov\'a, Self-replication and computational
+universality, arXiv:2510.08342 (2025).
 
-\bibitem{Codd1968}
-E.~F.~Codd, \emph{Cellular Automata}, Academic Press, New York, 1968.
+\bibitem{MavaddatParhami1988}
+F.~Mavaddat and B.~Parhami, URISC: The ultimate reduced instruction set computer,
+\emph{Int. J. Electr. Eng. Educ.} \textbf{25}, 327 (1988).
 
-\bibitem{CotlerHonglerHudcova2025}
-J.~Cotler, C.~Hongler, and B.~Hudcov\'a,
-\emph{Self-replication and computational universality}, arXiv:2510.08342, 2025.
+\bibitem{Pierce1965}
+W.~H. Pierce, \emph{Failure-Tolerant Computer Design} (Academic Press, New York,
+1965).
 
-\bibitem{DobrushinOrtyukov1977}
-R.~L.~Dobrushin and S.~I.~Ortyukov,
-\emph{Upper bound on the redundancy of self-correcting arrangements of unreliable
-functional elements}, Problems Inform. Transmission \textbf{13} (1977), no.~3,
-203--218.
+\bibitem{Muroga1971}
+S.~Muroga, \emph{Threshold Logic and Its Applications} (Wiley-Interscience, New
+York, 1971).
 
-\bibitem{Denneau1982}
-M.~M.~Denneau,
-\emph{The Yorktown simulation engine}, Proceedings of the 19th Design Automation
-Conference, 1982, 55--59.
+\bibitem{Kleene1956}
+S.~C. Kleene, Representation of events in nerve nets and finite automata, in
+\emph{Automata Studies}, edited by C.~E. Shannon and J.~McCarthy, Ann. Math. Stud.
+34 (Princeton University Press, Princeton, 1956), 3.
 
-\bibitem{DurbeckMacias2001}
-L.~J.~K.~Durbeck and N.~J.~Macias,
-\emph{The Cell Matrix: an architecture for nanocomputing},
-Nanotechnology \textbf{12} (2001), 217--230.
+\bibitem{Minsky1967}
+M.~L. Minsky, \emph{Computation: Finite and Infinite Machines} (Prentice-Hall,
+Englewood Cliffs, NJ, 1967).
 
-\bibitem{EvansSchulman1999}
-W.~S.~Evans and L.~J.~Schulman,
-\emph{Signal propagation and noisy circuits}, IEEE Trans. Inform. Theory
-\textbf{45} (1999), no.~7, 2367--2373.
+\bibitem{AlonDewdneyOtt1991}
+N.~Alon, A.~K. Dewdney and T.~J. Ott, Efficient simulation of finite automata by
+neural nets, \emph{J. ACM} \textbf{38}, 495 (1991).
 
-\bibitem{Gabor2022}
-T.~Gabor, S.~Illium, M.~Zorn, C.~Lenta, A.~Mattausch, L.~Belzner, and
-C.~Linnhoff-Popien,
-\emph{Self-replication in neural networks},
-Artificial Life \textbf{28} (2022), no.~2, 205--223.
+\bibitem{Indyk1995}
+P.~Indyk, Optimal simulation of automata by neural nets, in \emph{STACS 95}, LNCS
+900, 337 (1995).
 
-\bibitem{GiannouEtAl2023}
-A.~Giannou, S.~Rajput, J.-y.~Sohn, K.~Lee, J.~D.~Lee, and D.~Papailiopoulos,
-\emph{Looped transformers as programmable computers}, Proceedings of the 40th
-International Conference on Machine Learning, PMLR \textbf{202} (2023),
-11398--11442.
+\bibitem{Lee1963}
+C.~Y. Lee, A Turing machine which prints its own code script, in
+\emph{Proceedings of the Symposium on Mathematical Theory of Automata} (Polytechnic
+Press, Brooklyn, 1963), 155.
 
-\bibitem{GoldmannHastadRazborov1992}
-M.~Goldmann, J.~H\aa stad, and A.~Razborov,
-\emph{Majority gates vs.\ general weighted threshold gates},
-Comput. Complexity \textbf{2} (1992), 277--300.
+\bibitem{Thatcher1963}
+J.~W. Thatcher, The construction of a self-describing Turing machine, in
+\emph{Proceedings of the Symposium on Mathematical Theory of Automata} (Polytechnic
+Press, Brooklyn, 1963), 165.
 
-\bibitem{GoldmannKarpinski1998}
-M.~Goldmann and M.~Karpinski,
-\emph{Simulating threshold circuits by majority circuits},
-SIAM J. Comput. \textbf{27} (1998), no.~1, 230--246.
+\bibitem{vonNeumann1956}
+J.~von~Neumann, Probabilistic logics and the synthesis of reliable organisms from
+unreliable components, in \emph{Automata Studies}, edited by C.~E. Shannon and
+J.~McCarthy, Ann. Math. Stud. 34 (Princeton University Press, Princeton, 1956), 43.
 
-\bibitem{Goto1959}
-E.~Goto,
-\emph{The parametron, a digital computing element which utilizes parametric
-oscillation}, Proc. IRE \textbf{47} (1959), no.~8, 1304--1316.
+\bibitem{DobrushinOrtyukov1977}
+R.~L. Dobrushin and S.~I. Ortyukov, Upper bound on the redundancy of
+self-correcting arrangements of unreliable functional elements, \emph{Probl. Inf.
+Transm.} \textbf{13}, 203 (1977).
 
-\bibitem{GruauEtAl1995}
-F.~Gruau, J.-Y.~Ratajszczak, and G.~Wiber,
-\emph{A neural compiler}, Theoret. Comput. Sci. \textbf{141} (1995), 1--52.
+\bibitem{Pippenger1985}
+N.~Pippenger, On networks of noisy gates, in \emph{26th Annual Symposium on
+Foundations of Computer Science}, 30 (1985).
 
 \bibitem{HajekWeller1991}
-B.~Hajek and T.~Weller,
-\emph{On the maximum tolerable noise for reliable computation by formulas},
-IEEE Trans. Inform. Theory \textbf{37} (1991), no.~2, 388--391.
+B.~Hajek and T.~Weller, On the maximum tolerable noise for reliable computation by
+formulas, \emph{IEEE Trans. Inf. Theory} \textbf{37}, 388 (1991).
 
-\bibitem{HaDaiLe2017}
-D.~Ha, A.~M.~Dai, and Q.~V.~Le,
-\emph{HyperNetworks}, International Conference on Learning Representations, 2017.
+\bibitem{EvansSchulman1999}
+W.~S. Evans and L.~J. Schulman, Signal propagation and noisy circuits, \emph{IEEE
+Trans. Inf. Theory} \textbf{45}, 2367 (1999).
 
-\bibitem{IbanezEtAl1995}
-J.~Ib\'a\~nez, D.~Anabitarte, I.~Azpeitia, O.~Barrera, A.~Barrutieta, H.~Blanco,
-and F.~Echarte,
-\emph{Self-inspection based reproduction in cellular automata}, Advances in
-Artificial Life (ECAL 1995), Lecture Notes in Comput. Sci. \textbf{929}, Springer,
-1995, 564--576.
+\bibitem{MooreShannon1956}
+E.~F. Moore and C.~E. Shannon, Reliable circuits using less reliable relays,
+\emph{J. Franklin Inst.} \textbf{262}, 191 and 281 (1956).
 
-\bibitem{Indyk1995}
-P.~Indyk,
-\emph{Optimal simulation of automata by neural nets}, STACS 95, Lecture Notes in
-Comput. Sci. \textbf{900}, Springer, 1995, 337--348.
+\bibitem{WinogradCowan1963}
+S.~Winograd and J.~D. Cowan, \emph{Reliable Computation in the Presence of Noise}
+(MIT Press, Cambridge, MA, 1963).
 
-\bibitem{IrieEtAl2022}
-K.~Irie, I.~Schlag, R.~Csord\'as, and J.~Schmidhuber,
-\emph{A modern self-referential weight matrix that learns to modify itself},
-Proceedings of the 39th International Conference on Machine Learning, PMLR
-\textbf{162} (2022), 9660--9677.
+\bibitem{Pierce1964}
+W.~H. Pierce, Interwoven redundant logic, \emph{J. Franklin Inst.} \textbf{277}, 55
+(1964).
 
-\bibitem{Kleene1956}
-S.~C.~Kleene,
-\emph{Representation of events in nerve nets and finite automata}, Automata
-Studies (C.~E.~Shannon and J.~McCarthy, eds.), Annals of Mathematics Studies
-\textbf{34}, Princeton University Press, 1956, 3--41.
+\bibitem{Denneau1982}
+M.~M. Denneau, The Yorktown simulation engine, in \emph{19th Design Automation
+Conference}, 55 (1982).
 
-\bibitem{Langton1984}
-C.~G.~Langton,
-\emph{Self-reproduction in cellular automata}, Physica D \textbf{10} (1984),
-135--144.
+\bibitem{RiosWilsonTheyssier2024c}
+M.~R\'ios-Wilson and G.~Theyssier, Intrinsic universality in automata networks III:
+On symmetry versus asynchrony, \emph{Theor. Comput. Sci.} \textbf{1022}, 114890
+(2024).
 
-\bibitem{Lee1963}
-C.~Y.~Lee,
-\emph{A Turing machine which prints its own code script}, Proceedings of the
-Symposium on Mathematical Theory of Automata, Polytechnic Press, Brooklyn, 1963,
-155--164.
+\bibitem{Goto1959}
+E.~Goto, The parametron, a digital computing element which utilizes parametric
+oscillation, \emph{Proc. IRE} \textbf{47}, 1304 (1959).
 
-\bibitem{LiangEtAl2025}
-Y.~Liang, Z.~Sha, Z.~Shi, Z.~Song, and Y.~Zhou,
-\emph{Looped ReLU MLPs may be all you need as practical programmable computers},
-Proceedings of the 28th International Conference on Artificial Intelligence and
-Statistics, PMLR \textbf{258} (2025), 2647--2655.
+\bibitem{MurogaTakashima1959}
+S.~Muroga and K.~Takashima, The parametron digital computer MUSASINO-1, \emph{IRE
+Trans. Electron. Comput.} \textbf{EC-8}, 308 (1959).
 
-\bibitem{LindnerEtAl2023}
-D.~Lindner, J.~Kram\'ar, S.~Farquhar, M.~Rahtz, T.~McGrath, and V.~Mikulik,
-\emph{Tracr: Compiled transformers as a laboratory for interpretability},
-Advances in Neural Information Processing Systems, 2023.
+\bibitem{Okoma2002}
+S.~Okoma, The first Japanese computers and their software simulators, in \emph{The
+First Computers: History and Architectures}, edited by R.~Rojas and U.~Hashagen
+(MIT Press, Cambridge, MA, 2002), 419.
 
-\bibitem{LiuAndoniHsu2026}
-J.~Liu, A.~Andoni, and D.~Hsu,
-\emph{Fixed universal transformers}, arXiv:2605.31423, 2026.
+\bibitem{CoatesLewis1964}
+C.~L. Coates and P.~M. Lewis~II, DONUT: A threshold gate computer, \emph{IEEE
+Trans. Electron. Comput.} \textbf{EC-13}, 240 (1964).
 
-\bibitem{MaassOrponen1998}
-W.~Maass and P.~Orponen,
-\emph{On the effect of analog noise in discrete-time analog computations},
-Neural Computation \textbf{10} (1998), no.~5, 1071--1095.
+\bibitem{BeiuQuintanaAvedillo2003}
+V.~Beiu, J.~M. Quintana and M.~J. Avedillo, VLSI implementations of threshold
+logic---a comprehensive survey, \emph{IEEE Trans. Neural Netw.} \textbf{14}, 1217
+(2003).
 
-\bibitem{MangeEtAl1998}
-D.~Mange, E.~Sanchez, A.~Stauffer, G.~Tempesti, P.~Marchal, and C.~Piguet,
-\emph{Embryonics: A new methodology for designing field-programmable gate arrays
-with self-repair and self-replicating properties}, IEEE Trans. VLSI Systems
-\textbf{6} (1998), no.~3, 387--399.
+\bibitem{GoldmannHastadRazborov1992}
+M.~Goldmann, J.~H\aa stad and A.~Razborov, Majority gates vs.\ general weighted
+threshold gates, \emph{Comput. Complexity} \textbf{2}, 277 (1992).
 
-\bibitem{MavaddatParhami1988}
-F.~Mavaddat and B.~Parhami,
-\emph{URISC: The ultimate reduced instruction set computer}, Int. J. Electrical
-Engineering Education \textbf{25} (1988), no.~4, 327--334.
+\bibitem{GoldmannKarpinski1998}
+M.~Goldmann and M.~Karpinski, Simulating threshold circuits by majority circuits,
+\emph{SIAM J. Comput.} \textbf{27}, 230 (1998).
 
-\bibitem{McCullochPitts1943}
-W.~S.~McCulloch and W.~Pitts,
-\emph{A logical calculus of the ideas immanent in nervous activity}, Bull. Math.
-Biophys. \textbf{5} (1943), 115--133.
+\bibitem{SiuRoychowdhuryKailath1995}
+K.-Y. Siu, V.~Roychowdhury and T.~Kailath, \emph{Discrete Neural Computation: A
+Theoretical Foundation} (Prentice Hall, Englewood Cliffs, NJ, 1995).
 
-\bibitem{Melquiond2008}
-G.~Melquiond,
-\emph{Proving bounds on real-valued functions with computations}, Automated
-Reasoning (IJCAR 2008), Lecture Notes in Comput. Sci. \textbf{5195}, Springer, 2008,
-2--17.
+\bibitem{SiegelmannSontag1995}
+H.~T. Siegelmann and E.~D. Sontag, On the computational power of neural nets,
+\emph{J. Comput. Syst. Sci.} \textbf{50}, 132 (1995).
 
-\bibitem{Minsky1967}
-M.~L.~Minsky,
-\emph{Computation: Finite and Infinite Machines}, Prentice-Hall, Englewood Cliffs,
-NJ, 1967.
+\bibitem{SimaOrponen2003}
+J.~{\v S}\'ima and P.~Orponen, General-purpose computation with neural networks: A
+survey of complexity theoretic results, \emph{Neural Comput.} \textbf{15}, 2727
+(2003).
 
-\bibitem{Moore1962}
-E.~F.~Moore,
-\emph{Machine models of self-reproduction}, Proc. Sympos. Appl. Math.
-\textbf{14}, Amer. Math. Soc., Providence, RI, 1962, 17--33.
+\bibitem{GruauEtAl1995}
+F.~Gruau, J.-Y. Ratajszczak and G.~Wiber, A neural compiler, \emph{Theor. Comput.
+Sci.} \textbf{141}, 1 (1995).
 
-\bibitem{MooreShannon1956}
-E.~F.~Moore and C.~E.~Shannon,
-\emph{Reliable circuits using less reliable relays}, J. Franklin Inst.
-\textbf{262} (1956), 191--208 and 281--297.
+\bibitem{LindnerEtAl2023}
+D.~Lindner, J.~Kram\'ar, S.~Farquhar, M.~Rahtz, T.~McGrath and V.~Mikulik, Tracr:
+Compiled transformers as a laboratory for interpretability, in \emph{Advances in
+Neural Information Processing Systems} (2023).
 
-\bibitem{Muroga1971}
-S.~Muroga,
-\emph{Threshold Logic and Its Applications}, Wiley-Interscience, New York, 1971.
+\bibitem{GiannouEtAl2023}
+A.~Giannou, S.~Rajput, J.-y. Sohn, K.~Lee, J.~D. Lee and D.~Papailiopoulos, Looped
+transformers as programmable computers, in \emph{40th International Conference on
+Machine Learning}, PMLR 202, 11398 (2023).
 
-\bibitem{MurogaTakashima1959}
-S.~Muroga and K.~Takashima,
-\emph{The parametron digital computer MUSASINO-1}, IRE Trans. Electronic
-Computers \textbf{EC-8} (1959), no.~3, 308--316.
+\bibitem{LiangEtAl2025}
+Y.~Liang, Z.~Sha, Z.~Shi, Z.~Song and Y.~Zhou, Looped ReLU MLPs may be all you need
+as practical programmable computers, in \emph{28th International Conference on
+Artificial Intelligence and Statistics}, PMLR 258, 2647 (2025).
 
-\bibitem{Myhill1964}
-J.~Myhill,
-\emph{The abstract theory of self-reproduction}, Views on General Systems Theory
-(M.~D.~Mesarovi\'c, ed.), Wiley, New York, 1964, 106--118.
+\bibitem{LiuAndoniHsu2026}
+J.~Liu, A.~Andoni and D.~Hsu, Fixed universal transformers, arXiv:2605.31423
+(2026).
 
-\bibitem{Norton2026}
-C.~Norton,
-\emph{threshold-computers: a family of threshold-logic machines}, Hugging Face
-repository, 2026, \url{https://huggingface.co/phanerozoic/threshold-computers}.
+\bibitem{Turkcan2026}
+M.~K. Turkcan, Loom: A scalable analytical neural computer architecture,
+arXiv:2604.08816 (2026).
 
-\bibitem{Okoma2002}
-S.~Okoma,
-\emph{The first Japanese computers and their software simulators}, The First
-Computers: History and Architectures (R.~Rojas and U.~Hashagen, eds.), MIT Press,
-Cambridge, MA, 2002, 419--449.
+\bibitem{Valiant1976}
+L.~G. Valiant, Universal circuits (preliminary report), in \emph{8th Annual ACM
+Symposium on Theory of Computing}, 196 (1976).
 
-\bibitem{PerrierSipperZahnd1996}
-J.-Y.~Perrier, M.~Sipper, and J.~Zahnd,
-\emph{Toward a viable, self-reproducing universal computer}, Physica D
-\textbf{97} (1996), 335--352.
+\bibitem{RiosWilsonTheyssier2024a}
+M.~R\'ios-Wilson and G.~Theyssier, Intrinsic universality in automata networks I:
+Families and simulations, \emph{Theor. Comput. Sci.} \textbf{997}, 114511 (2024).
 
-\bibitem{Pesavento1995}
-U.~Pesavento,
-\emph{An implementation of von Neumann's self-reproducing machine}, Artificial
-Life \textbf{2} (1995), no.~4, 337--354.
+\bibitem{SimaWiedermann1998}
+J.~{\v S}\'ima and J.~Wiedermann, Theory of neuromata, \emph{J. ACM} \textbf{45},
+155 (1998).
 
-\bibitem{Pierce1964}
-W.~H.~Pierce,
-\emph{Interwoven redundant logic}, J. Franklin Inst. \textbf{277} (1964), no.~1,
-55--85.
+\bibitem{ChungSiegelmann2021}
+S.~Chung and H.~T. Siegelmann, Turing completeness of bounded-precision recurrent
+neural networks, in \emph{Advances in Neural Information Processing Systems}
+\textbf{34}, 28431 (2021).
 
-\bibitem{Pierce1965}
-W.~H.~Pierce,
-\emph{Failure-Tolerant Computer Design}, Academic Press, New York, 1965.
+\bibitem{CabessaSiegelmann2014}
+J.~Cabessa and H.~T. Siegelmann, The super-Turing computational power of plastic
+recurrent neural networks, \emph{Int. J. Neural Syst.} \textbf{24}, 1450029 (2014).
 
-\bibitem{Pippenger1985}
-N.~Pippenger,
-\emph{On networks of noisy gates}, Proceedings of the 26th Annual Symposium on
-Foundations of Computer Science, IEEE, 1985, 30--38.
+\bibitem{Burks1970}
+A.~W. Burks (ed.), \emph{Essays on Cellular Automata} (University of Illinois
+Press, Urbana, 1970).
 
-\bibitem{RandazzoVersariMordvintsev2021}
-E.~Randazzo, L.~Versari, and A.~Mordvintsev,
-\emph{Recursively fertile self-replicating neural agents}, ALIFE 2021, MIT Press,
-2021.
+\bibitem{MaassOrponen1998}
+W.~Maass and P.~Orponen, On the effect of analog noise in discrete-time analog
+computations, \emph{Neural Comput.} \textbf{10}, 1071 (1998).
 
-\bibitem{Ray1991}
-T.~S.~Ray,
-\emph{An approach to the synthesis of life}, Artificial Life II (C.~G.~Langton
-et al., eds.), Addison-Wesley, 1991, 371--408.
+\bibitem{Moore1962}
+E.~F. Moore, Machine models of self-reproduction, \emph{Proc. Sympos. Appl. Math.}
+\textbf{14}, 17 (1962).
 
-\bibitem{RiosWilsonTheyssier2024a}
-M.~R\'ios-Wilson and G.~Theyssier,
-\emph{Intrinsic universality in automata networks I: Families and simulations},
-Theoret. Comput. Sci. \textbf{997} (2024), 114511.
+\bibitem{Myhill1964}
+J.~Myhill, The abstract theory of self-reproduction, in \emph{Views on General
+Systems Theory}, edited by M.~D. Mesarovi\'c (Wiley, New York, 1964), 106.
 
-\bibitem{RiosWilsonTheyssier2024c}
-M.~R\'ios-Wilson and G.~Theyssier,
-\emph{Intrinsic universality in automata networks III: On symmetry versus
-asynchrony}, Theoret. Comput. Sci. \textbf{1022} (2024), 114890.
+\bibitem{IbanezEtAl1995}
+J.~Ib\'a\~nez, D.~Anabitarte, I.~Azpeitia, O.~Barrera, A.~Barrutieta, H.~Blanco and
+F.~Echarte, Self-inspection based reproduction in cellular automata, in
+\emph{Advances in Artificial Life (ECAL 1995)}, LNCS 929, 564 (1995).
 
-\bibitem{Schmidgall2021}
-S.~Schmidgall,
-\emph{Self-replicating neural programs}, arXiv:2109.12786, 2021.
+\bibitem{MangeEtAl1998}
+D.~Mange, E.~Sanchez, A.~Stauffer, G.~Tempesti, P.~Marchal and C.~Piguet,
+Embryonics: A new methodology for designing field-programmable gate arrays with
+self-repair and self-replicating properties, \emph{IEEE Trans. VLSI Syst.}
+\textbf{6}, 387 (1998).
 
-\bibitem{Schmidhuber1993}
-J.~Schmidhuber,
-\emph{A self-referential weight matrix}, Proceedings of the International
-Conference on Artificial Neural Networks (ICANN 1993), Springer, 1993, 446--451.
+\bibitem{DurbeckMacias2001}
+L.~J.~K. Durbeck and N.~J. Macias, The Cell Matrix: an architecture for
+nanocomputing, \emph{Nanotechnology} \textbf{12}, 217 (2001).
 
-\bibitem{ShvartzmanRam2024}
-B.~Shvartzman and Y.~Ram,
-\emph{Self-replicating artificial neural networks give rise to universal
-evolutionary dynamics}, PLoS Comput. Biol. \textbf{20} (2024), no.~3, e1012004.
+\bibitem{Ray1991}
+T.~S. Ray, An approach to the synthesis of life, in \emph{Artificial Life II},
+edited by C.~G. Langton et al. (Addison-Wesley, 1991), 371.
 
-\bibitem{SiegelmannSontag1995}
-H.~T.~Siegelmann and E.~D.~Sontag,
-\emph{On the computational power of neural nets}, J. Comput. System Sci.
-\textbf{50} (1995), no.~1, 132--150.
+\bibitem{AgueraYArcas2024}
+B.~Ag\"uera y Arcas, J.~Alakuijala, J.~Evans, B.~Laurie, A.~Mordvintsev,
+E.~Niklasson, E.~Randazzo and L.~Versari, Computational life: How well-formed,
+self-replicating programs emerge from simple interaction, arXiv:2406.19108 (2024).
 
-\bibitem{SimaOrponen2003}
-J.~{\v S}\'ima and P.~Orponen,
-\emph{General-purpose computation with neural networks: A survey of complexity
-theoretic results}, Neural Computation \textbf{15} (2003), no.~12, 2727--2778.
+\bibitem{ChangLipson2018}
+O.~Chang and H.~Lipson, Neural network quine, in \emph{ALIFE 2018} (MIT Press,
+2018), arXiv:1803.05859.
 
-\bibitem{SimaWiedermann1998}
-J.~{\v S}\'ima and J.~Wiedermann,
-\emph{Theory of neuromata}, J. ACM \textbf{45} (1998), no.~1, 155--178.
+\bibitem{Gabor2022}
+T.~Gabor, S.~Illium, M.~Zorn, C.~Lenta, A.~Mattausch, L.~Belzner and
+C.~Linnhoff-Popien, Self-replication in neural networks, \emph{Artif. Life}
+\textbf{28}, 205 (2022).
 
-\bibitem{Sipper1998}
-M.~Sipper,
-\emph{Fifty years of research on self-replication: An overview}, Artificial Life
-\textbf{4} (1998), no.~3, 237--257.
+\bibitem{RandazzoVersariMordvintsev2021}
+E.~Randazzo, L.~Versari and A.~Mordvintsev, Recursively fertile self-replicating
+neural agents, in \emph{ALIFE 2021} (MIT Press, 2021).
 
-\bibitem{SiuRoychowdhuryKailath1995}
-K.-Y.~Siu, V.~Roychowdhury, and T.~Kailath,
-\emph{Discrete Neural Computation: A Theoretical Foundation}, Prentice Hall,
-Englewood Cliffs, NJ, 1995.
+\bibitem{ShvartzmanRam2024}
+B.~Shvartzman and Y.~Ram, Self-replicating artificial neural networks give rise to
+universal evolutionary dynamics, \emph{PLoS Comput. Biol.} \textbf{20}, e1012004
+(2024).
 
-\bibitem{Thatcher1963}
-J.~W.~Thatcher,
-\emph{The construction of a self-describing Turing machine}, Proceedings of the
-Symposium on Mathematical Theory of Automata, Polytechnic Press, Brooklyn, 1963,
-165--171.
+\bibitem{Schmidgall2021}
+S.~Schmidgall, Self-replicating neural programs, arXiv:2109.12786 (2021).
 
-\bibitem{Turkcan2026}
-M.~K.~Turkcan,
-\emph{Loom: A scalable analytical neural computer architecture},
-arXiv:2604.08816, 2026.
+\bibitem{HaDaiLe2017}
+D.~Ha, A.~M. Dai and Q.~V. Le, HyperNetworks, in \emph{International Conference on
+Learning Representations} (2017).
 
-\bibitem{Valiant1976}
-L.~G.~Valiant,
-\emph{Universal circuits (preliminary report)}, Proceedings of the 8th Annual ACM
-Symposium on Theory of Computing, 1976, 196--203.
+\bibitem{Schmidhuber1993}
+J.~Schmidhuber, A self-referential weight matrix, in \emph{International Conference
+on Artificial Neural Networks (ICANN 1993)}, 446 (1993).
 
-\bibitem{vonNeumann1945}
-J.~von Neumann,
-\emph{First Draft of a Report on the EDVAC}, Moore School of Electrical
-Engineering, University of Pennsylvania, 1945.
+\bibitem{IrieEtAl2022}
+K.~Irie, I.~Schlag, R.~Csord\'as and J.~Schmidhuber, A modern self-referential
+weight matrix that learns to modify itself, in \emph{39th International Conference
+on Machine Learning}, PMLR 162, 9660 (2022).
 
-\bibitem{vonNeumann1956}
-J.~von Neumann,
-\emph{Probabilistic logics and the synthesis of reliable organisms from unreliable
-components}, Automata Studies, Annals of Mathematics Studies \textbf{34},
-Princeton University Press, 1956, 43--98.
+\bibitem{BoldoLelayMelquiond2015}
+S.~Boldo, C.~Lelay and G.~Melquiond, Coquelicot: A user-friendly library of real
+analysis for Coq, \emph{Math. Comput. Sci.} \textbf{9}, 41 (2015).
 
-\bibitem{vonNeumann1966}
-J.~von Neumann,
-\emph{Theory of Self-Reproducing Automata} (A.~W.~Burks, ed.), University of
-Illinois Press, Urbana, 1966.
+\bibitem{Melquiond2008}
+G.~Melquiond, Proving bounds on real-valued functions with computations, in
+\emph{IJCAR 2008}, LNCS 5195, 2 (2008).
 
-\bibitem{WinogradCowan1963}
-S.~Winograd and J.~D.~Cowan,
-\emph{Reliable Computation in the Presence of Noise}, MIT Press, Cambridge, MA,
-1963.
+\bibitem{Norton2026}
+C.~Norton, threshold-computers: a family of threshold-logic machines, Hugging Face
+repository (2026), \link{https://huggingface.co/phanerozoic/threshold-computers}.
 
 \end{thebibliography}
 

rocq/Assumptions.v

@@ -100,6 +100,7 @@ Print Assumptions PhysLev.phys_lev_rows_S.
 Print Assumptions Lower.read_needs_two_levels.
 Print Assumptions Lower.onehot_needs_two_levels.
 Print Assumptions Lower.branch_not_ternary.
+Print Assumptions Lower.branch_unit.
 Print Assumptions Margin.margin.
 Print Assumptions Margin.margin_tight.
 Print Assumptions Margin.mismatch_all.

rocq/Lower.v

@@ -210,3 +210,55 @@ Proof.
   replace (2 ^ Z.of_nat (n - 1) - 1 - 1 * 2 ^ Z.of_nat (n - 1) <=? 0) with true in H by (symmetry; apply Z.leb_le; lia).
   apply Z.leb_le in H. specialize (Hw (n - 1)%nat). lia.
 Qed.
+
+(* ---- Lemma 3.3 --------------------------------------------------------------------------------------------- *)
+(* z(r) = H(-(r_0 + ... + r_(n-1))) *)
+Definition zunit (n : nat) (r : nat -> bool) : bool := zfire n (fun _ => -1) 0 r.
+
+Lemma zsum_neg_le : forall r l, zsum (fun _ => -1) r l <= 0.
+Proof. intros r l. induction l as [|i t IH]; cbn [zsum]; [lia|]. destruct (r i); lia. Qed.
+
+Lemma zsum_neg : forall r l, Z.leb 0 (zsum (fun _ => -1) r l) = forallb (fun i => negb (r i)) l.
+Proof.
+  intros r l. induction l as [|i t IH]; cbn [zsum forallb]; [reflexivity|].
+  pose proof (zsum_neg_le r t). destruct (r i); cbn [negb andb].
+  - apply Z.leb_gt. lia.
+  - rewrite Z.add_0_l. exact IH.
+Qed.
+
+Lemma uval_bound : forall r k, 0 <= uval r k < 2 ^ Z.of_nat k.
+Proof.
+  intros r k. induction k as [|k IH]; cbn [uval]; [cbn; lia|].
+  rewrite Nat2Z.inj_succ, Z.pow_succ_r by lia. destruct (r k); cbn [Z.b2z]; lia.
+Qed.
+
+Lemma uval_zero : forall r k, Z.eqb (uval r k) 0 = forallb (fun i => negb (r i)) (seq 0 k).
+Proof.
+  intros r k. induction k as [|k IH]; [reflexivity|]. cbn [uval]. rewrite seq_S, forallb_app, <- IH.
+  cbn [forallb Nat.add]. pose proof (uval_bound r k) as B.
+  assert (P : 0 < 2 ^ Z.of_nat k) by (apply Z.pow_pos_nonneg; lia).
+  destruct (r k); cbn [Z.b2z negb andb].
+  - rewrite andb_false_r. apply Z.eqb_neq. lia.
+  - rewrite andb_true_r, Z.mul_0_l, Z.add_0_r. reflexivity.
+Qed.
+
+(* z(r) is 1 exactly when r = 0, and [r <= 0] = H(r_(n-1) + z(r) - 1): the branch takes two ternary units *)
+Theorem branch_unit : forall n r, (1 <= n)%nat ->
+  zunit n r = Z.eqb (tval n r) 0 /\ branch n r = Z.leb 0 (Z.b2z (r (n - 1)%nat) + Z.b2z (zunit n r) - 1).
+Proof.
+  intros n r Hn.
+  assert (Hz : zunit n r = Z.eqb (uval r (n - 1)) 0 && negb (r (n - 1)%nat)).
+  { unfold zunit, zfire. rewrite Z.add_0_r, zsum_neg.
+    replace (seq 0 n) with (seq 0 (n - 1) ++ [(n - 1)%nat])
+      by (replace n with (S (n - 1)) at 3 by lia; rewrite seq_S; reflexivity).
+    rewrite forallb_app, <- uval_zero. cbn [forallb]. rewrite andb_true_r. reflexivity. }
+  unfold branch, tval. rewrite Hz. pose proof (uval_bound r (n - 1)) as B.
+  assert (P : 0 < 2 ^ Z.of_nat (n - 1)) by (apply Z.pow_pos_nonneg; lia).
+  set (u := uval r (n - 1)) in *.
+  destruct (r (n - 1)%nat); cbn [negb]; rewrite ?andb_false_r, ?andb_true_r; cbn [Z.b2z].
+  - split; [symmetry; apply Z.eqb_neq; lia|].
+    rewrite (proj2 (Z.leb_le (u - 1 * 2 ^ Z.of_nat (n - 1)) 0)) by lia. reflexivity.
+  - replace (u - 0 * 2 ^ Z.of_nat (n - 1)) with u by lia. split; [reflexivity|].
+    destruct (Z.eqb_spec u 0) as [E|E]; cbn [Z.b2z]; [rewrite E; reflexivity|].
+    rewrite (proj2 (Z.leb_gt u 0)) by lia. reflexivity.
+Qed.