\section{Machine checks}\label{app:checks}

Every finite quantity used in the proofs is recomputed by programs in the archive \cite{BB26code}, and the combinatorial and arithmetic statements among them are also proved in Lean~4. No statement of the paper rests on these checks; they guard against slips in the hand computations.

\paragraph{Lean.} The file \path{lean/HodgeClosure.lean} (Lean~4.24.0, no Mathlib) contains forty-seven theorems. Section~1 encodes the eight statements and the rule set of Table~\ref{tab:rules} as data, computes closures by iteration, and proves by evaluation that the closures of $\{\mathrm{F2},\mathrm{F3}'\}$, $\{\mathrm{F3}\}$, $\{\mathrm{L},\mathrm{M}\}$, $\{\mathrm{L},\mathrm{F3}'\}$ and $\{\mathrm{V},\mathrm{F3}'\}$ contain $\HC$, that the closures of $\{\mathrm{F2}\}$, $\{\mathrm{F3}'\}$, $\{\mathrm{L}\}$, $\{\mathrm{M}\}$, $\{\mathrm{V}\}$, $\{\AB\}$, $\{\mathrm{L},\mathrm{V}\}$ and $\{\mathrm{M},\mathrm{F3}'\}$ do not, and that the list of minimal sufficient sets, computed from the rule set alone, has exactly six members, those of Proposition~\ref{prop:minimal}. Section~2 works in $\ZZ[\sqrt{-d}]$ and proves that the hermitian form $\eta$ transforms under $\tau$ by $N(\tau)$, that the norm is multiplicative, that $\eta$ is not $K^{\times}$-invariant, and that the characters $N(\tau)^{n}$ and $\tau^{2n}$ differ at explicit $\tau$ (Section~\ref{sec:earlier}). Section~3 proves the dimension counts of Section~\ref{sec:f2}: $3n<n^{2}$ for $n\ge4$, $m^{2}+m'^{2}<(m+m')^{2}$ for $m,m'\ge1$ with $2mm'$ mixed directions, the values $r=57$ and $104$ of the lower bound, and the Hodge class count $26$ of Theorem~\ref{thm:link}(i) as a sum of K\"unneth contributions. Section~4 proves the polynomial identities behind the Fricke families of Section~\ref{ssec:fricke}: $c_{4}^{3}-c_{6}^{2}=1728\,t\,(t^{2}+13t+49)^{2}$ at level $7$ and $1728\,t\,(t^{2}+22t+125)^{3}$ at level $5$, by exact arithmetic on coefficient lists, together with the root products $7^{2}$ and $5^{3}$, the Euler numbers $12$ and $24$, the Shioda--Tate counts giving Picard number at least $16$, the transcendental rank $6$, and the dimensions $(n+1)/2$ of the dihedral Hecke algebras. Section~5 proves the Dickson identities $p_{7}(t+t^{-1})=t^{7}+t^{-7}$ and $p_{9}(t+t^{-1})=t^{9}+t^{-9}$ behind the families of Theorem~\ref{thm:zeta9}, that $2$ has order three in $(\ZZ/7)^{\times}/\pm1$ and in $(\ZZ/9)^{\times}/\pm1$, so that $2$ is inert in both cubic fields, and the sign pattern of the conjugates of $\theta$ at the three real places. Section~6 proves the finite statements of Appendix~\ref{app:cmpoint}: the binomial identity $\sum_{q}\binom{3}{q}\binom{3}{k-q}=\binom{6}{k}$, the intersection numbers $(C_{\zeta}\cdot C_{\zeta'})=|\zeta-\zeta'|^{2}$ and $\theta\cdot C_{\zeta}=2$ in the basis of the $(1,1)$-forms of $B_{j}$ with the pairing $a_{j}b_{j}=1$, $c_{j}\bar c_{j}=-1$, the twisted sums $T_{m,j}$, the identity $S(1)-S(-1)=32(\alpha+\bar\alpha)$ as an equality of the $64$ coefficients of the triple products over $\ZZ[i]$, the counts $48$, $8$, $75$ and $18$ with the Euler characteristics, and the two chain statements of Proposition~\ref{prop:twostep} over the twelve pieces of Appendix~\ref{app:extdims}, each by \texttt{decide}. Every theorem is checked by \texttt{\#print\,axioms}: forty-five use no axiom, and the two inequalities proved with the arithmetic tactic use \texttt{propext} and \texttt{Quot.sound}.

The Lean certificate of \cite{BMB26}, \texttt{HodgeObstruction.lean} (Lean~4.34.0, \leancount{} theorems, each axiom-free or depending on \texttt{propext} only), carries the finite computations of that paper; it is cited and not repeated here. The reduction of Section~\ref{sec:reduction} uses only the hand-proved parts of \cite{BMB26}.

\paragraph{Python.} \path{code/sqrt6_chain.py} (sympy) implements Hilbert symbols and Hasse invariants exactly, verifies the product formula on random pairs, classifies $U_{\QQ}$, $E_{8}(-1)_{\QQ}$ and the invariant lattices, reproduces Varesco's embedding results for $\sqrt2$ and $\sqrt3$ as controls, searches the $165$ sign-admissible small forms $q_{E}$ over $\QQ(\sqrt6)$ ($98$ embed in $V_{3}$, $67$ do not), exhibits the complements $\langle1,-10\rangle$ and $\langle1,-1,-1,-1,-3,-30\rangle$, and checks both orders of the chain: twenty-five checks. \path{code/fricke_families.py} computes the fibre types, Euler numbers and Picard bounds of the Fricke curves and their twists at levels $5$ and $7$, checks numerically that the roots of $j(t)=j(\tau)$ are carried by $t\mapsto N^{k}/t$ to the $j$-invariants of the $N$-isogenous curves, verifies the twist identity $u_{p,q}(w(t))=pq\,u_{w(p),w(q)}(t)/t^{2}$, the M\"obius transformations preserving the labelled points, the embedding of every rank-six form of signature $(2,4)$ in $V_{2}$ and $V_{3}$ after any scaling, and the Hecke algebras of $(D_{n},\langle\tau\rangle)$ for $n=5,7,9,11$: forty-one checks. \path{code/product_object.py} builds the exterior-algebra model of $H^{*}(A\times A')$ for $(m,m')=(2,1),(2,2)$, the tangent space of $\cD_{n,n}$ and of the product locus, the first-order Hodge loci of the exterior products and of the object of Theorem~\ref{thm:product}, the Vandermonde determinant, the vanishing of the cross terms, and the Hankel rank and $r(\gamma)$ of the final class; \path{code/convolution_checks.py} computes in the same model the rank of $v\mapsto v\lrcorner\theta_{A}$ on $T\cD_{n,n}$, the contraction ranks of $\ch(\mathcal{E}')$ and $\ch(\mathcal{E}'')$ in Proposition~\ref{prop:convolution}(iii), and the trace of an upper triangular times a strictly upper triangular block matrix. In these two programs ranks are computed in floating point with a relative tolerance of $10^{-7}$ and agree with the closed formulas. \path{code/sixfold_link.py} checks the alternation and invariances of $\psi_{c}$, the decomposition of the $K^{1}$-invariants, the ratio of the induced forms at the three places, the symmetry of $T_{X}(-1)$, the count $26$ and the weight support of $\xi$; \path{code/link_weights.py} computes the Hodge classes of degree four on $X\times X\times Z_{K}$ under the three groups of Section~\ref{ssec:f2stop2} and the vanishing of $\Hom(X_{c},Z_{K,c})$ at the compositum CM point. \path{code/zeta9_invariants.py} computes the rank, signature, discriminant and Hasse invariants of the trace form $\Tr_{F/\QQ}(-\theta\,\mathrm{nrd})$ on the quaternion algebra $(-1,-\theta)_{F}$, $F=\QQ(\zeta_{9})^{+}$, and of the transcendental lattice of the dihedral family of Theorem~\ref{thm:zeta9} for $n=9$, and checks that they agree while three contrasting algebras fail; \path{code/zeta7_invariants.py} does the same for $n=7$, with $(-1,\theta)_{F}$, $F=\QQ(\zeta_{7})^{+}$, the lattice $U^{2}\oplus E_{8}(-1)$ and the competing algebras ramified at $7$ or $43$, and checks the Dickson identity of \eqref{eq:dickson7}; \path{code/annihilator_exact.py} verifies in exact arithmetic over $\QQ(\sqrt{-3})$, at $(m,m')=(2,1)$ and $(2,2)$, the formula \eqref{eq:chEprime} and the dimension $m^{2}+m'^{2}$ of the annihilator in Theorem~\ref{thm:annihilator}, component by component; \path{code/riemann_roch_pieces.py} computes the polynomial \eqref{eq:rrpoly} and the thirty-one supports of Proposition~\ref{prop:noorth}; \path{code/cm_point_ext.py} checks Lemma~\ref{lem:cmext} and Proposition~\ref{prop:twostep}: the identity $\sum\binom{3}{q}\binom{3}{p}=\binom{6}{k}$, the Koszul cohomology of a transverse intersection in exact arithmetic, the Euler characteristics of the twisted groups, the enumeration of the closed chains of two and three pieces with their degrees, and the identities of Lemma~\ref{lem:cmcurves} in the exterior algebra of the twelve real one-forms of $E_{0}^{6}$. \path{code/closure_graph.py} recomputes the closures and the minimal sets, and \path{code/bypass_checks.py} the Horn closure with the facts of the literature on abelian varieties adjoined and the blow-up bookkeeping of Proposition~\ref{prop:bypass}(ii).

\paragraph{Julia, C, C\texttt{++} and shell.} \path{code/closure_graph.jl}, \path{code/closure_graph.c} and \path{code/closure_graph.cpp} recompute the closures of all $256$ subsets of the eight statements and the six minimal sets by three independent implementations of the fixed-point iteration; \path{code/eigencharacter.jl} recomputes the characters of Section~\ref{sec:earlier} in exact integer arithmetic, and \path{code/hilbert.c} the Hilbert symbols and the invariants of Table~\ref{tab:invariants}; \path{code/run_all.sh} runs every program and the Lean file and prints a line per check. The expected outputs are recorded in \path{code/EXPECTED.md}.