note_e8_gaussian_code.tex

\documentclass[11pt,a4paper]{article}
\usepackage[margin=2.6cm]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{booktabs}
\usepackage{microtype}
\usepackage{xcolor}
\usepackage[colorlinks=true,linkcolor=blue!50!black,citecolor=blue!50!black,urlcolor=blue!50!black]{hyperref}

\emergencystretch=2em

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\F}{\mathbb F}
\newcommand{\Z}{\mathbb Z}
\newcommand{\C}{\mathbb C}
\newcommand{\Cst}{C^{*}}
\newcommand{\ip}[2]{\langle #1,#2\rangle}
\DeclareMathOperator{\Deg}{Deg}
\DeclareMathOperator{\Exp}{Exp}
\DeclareMathOperator{\GL}{GL}
\DeclareMathOperator{\Jac}{Jac}
\DeclareMathOperator{\wt}{wt}

\title{The Gaussian code bridge: $E_8$ over $\Z[i]$, the extended
Hamming code, and a four-bit information layer}
\author{Stefan Hamann\thanks{Working note of the verification program
of Topological Fixed-Point Theory (TFPT),
\url{https://fixpoint-theory.com}.  Every number quoted in this note
is produced by a machine-checked artefact named in the text: the
exact-arithmetic discovery probes
\texttt{experiments/tfpt-discovery/gaussian\_code\_bridge\_probe.py}
($26/26$ checks) and \texttt{quartic\_half\_probe.py} ($22/22$
checks), promoted to the permanent verification suite as the modules
\texttt{v689}/\texttt{v690}, and the Lean~4 proof modules
\texttt{TfptCarrier/GaussianCodeBridge.lean} and
\texttt{TfptCarrier/QuarticHalf.lean} ($44+21=65$ kernel-checked
theorems, no \texttt{sorry}, no \texttt{native\_decide}).  No number
is quoted that was not printed by an executed run or certified by the
Lean kernel.}}
\date{August 3, 2026}

\begin{document}
\maketitle

\begin{abstract}
Build the $E_8$ lattice by Construction~A over the extended Hamming
code $[8,4,4]$, placed equivariantly with respect to four fixed
coordinate pairs, and let $J$ be the complex structure that rotates
each pair ($J^2=-1$, $\mu_4=\langle J\rangle$).  Then $L$ becomes a
unimodular Hermitian $\Z[i]$-lattice of rank~$4$, and reduction modulo
the ramified Gaussian prime $1+i$ produces a canonical four-bit
quotient $L/(1+i)L\cong\F_2^4$.  We prove: the $240$ roots avoid the
zero class --- by the two-line norm argument
$|(1+J)x|^2=2|x|^2$ against the doubly-even minimum $4$ --- and
distribute exactly $15\times16$ over the fifteen nonzero classes, each
class being a union of exactly $4$ of the $60$ Gaussian root lines.
On this quotient the pair $3$-cycle $\sigma$ (order $3$, commuting
with $J$) acts as a family $3$-cycle with a fixed anchor bit --- the
information-bit action of the Reed--Muller code $\mathrm{RM}(1,3)$ ---
with residual identification gauge of order exactly $18$, and the
sixteen coordinate roots $\pm2e_i$ form precisely one class, the
$\sigma$-fixed label $F_1{+}F_2{+}F_3$.  The classes cut across the
Construction-A codeword fibers: the code that builds the lattice
returns, after Gaussian reduction, as its \emph{message space}.  A
quartic companion theorem types the invariant-theoretic shadow: the
restrictions of the Weyl-invariant root power sums $F_8,F_{12},
F_{20},F_{24}$ to the holomorphic eigenspace $\ker(J-i)$ are
algebraically independent invariants of the complex reflection group
$G_{31}$ and hence, by Chevalley's theorem, a system of basic
invariants --- while the vanishing of the complementary degrees
$\{2,14,18,30\}$ is proved but honestly typed as the trivial
$\mu_4$-orbit factor $1+(-i)^d+(-1)^d+i^d=0$ ($d\not\equiv0\bmod4$),
with no $G_{31}$ content.  Every statement is certified by two
exact-arithmetic probes ($26/26$ and $22/22$ checks, no floats) and
$65$ kernel-checked Lean~4 theorems, with must-fail controls
(non-equivariant placements, non-integral complex structures,
$\Z[i]^4$) that kill or trivialize the structure exactly as demanded.
No claim beyond the stated algebra is made.
\end{abstract}

\medskip
\noindent\textbf{MSC 2020.} 11H06 (primary); 11H71, 20F55, 94B05,
68V20 (secondary).\\
\textbf{Keywords.} $E_8$ lattice; Construction A; extended Hamming
code; Reed--Muller code; Gaussian integers; complex reflection group
$G_{31}$; basic invariants; Lean 4.

\section{The three objects}\label{sec:setup}

\subsection{The code and its equivariant placement}
Let $C\subset\F_2^8$ be the extended Hamming code $[8,4,4]$ --- the
unique doubly-even self-dual binary code of length $8$, permutation
equivalent to the first-order Reed--Muller code $\mathrm{RM}(1,3)$
\cite[Ch.~1, 13--14]{MS77}.  Its automorphism group has order
$|{\rm AGL}(3,2)|=1344$, so $C$ admits exactly
$8!/1344=30$ distinct placements (coordinate images) inside $\F_2^8$.
Fix the four \emph{$\mu_4$ pairs}
$(0,1),(2,3),(4,5),(6,7)$ and the two permutations
\[
\pi_J=(01)(23)(45)(67)\quad(\text{in-pair swap}),\qquad
\pi_\sigma:\ (0,1)\to(2,3)\to(4,5)\to(0,1),\ (6,7)\ \text{fixed}
\]
(the pair $3$-cycle).  A machine census of all $30$ placements shows
that \emph{exactly two} are invariant under both $\pi_J$ and
$\pi_\sigma$ (probe check I0.1); we call $\Cst$ the one containing
the indicator vector of $\{0,2,4,6\}$, and note that the other is its
image under the single transposition $(67)$.  The fourteen weight-$4$
supports of $\Cst$ have a closed description: the six
\emph{pair unions} (three family--family:
$\{0,1,2,3\},\{0,1,4,5\},\{2,3,4,5\}$; three family--anchor:
$\{0,1,6,7\},\{2,3,6,7\},\{4,5,6,7\}$) and the eight \emph{even
transversals} $t(d)=\{2k+d_k:k=0,\dots,3\}$ with
$d\in\F_2^4$, $\sum_kd_k$ even --- one coordinate from each pair.

\subsection{The lattice}
Let $L=A(\Cst)=\{x\in\Z^8:\ x\bmod 2\in\Cst\}$ be the Construction-A
lattice of $\Cst$ \cite[Ch.~5]{CS99}, with the standard inner product
$\ip xy$ of $\Z^8$.  Then $[\Z^8:L]=2^4=16$, and since $\Cst$ is
doubly even, writing $x=c+2m$ with $c\in\{0,1\}^8$ a codeword lift
gives
\begin{equation}\label{eq:douleven}
\ip xx=\wt(c)+4(c\cdot m+m\cdot m)\equiv\wt(c)\equiv0 \pmod 4 ,
\end{equation}
so every nonzero $x\in L$ has $\ip xx\ge4$: the minimum of $L$ is
$4$, attained by exactly $240$ vectors (the $16$ coordinate vectors
$\pm2e_i$ and the $224$ lifts $c+2m$ of weight-$4$ codewords with
support-confined sign choices).  Rescaled by $1/\sqrt2$, $L$ is a copy
of the even unimodular root lattice $E_8$; we work integrally in $L$
throughout and call the $240$ minimal vectors the \emph{roots}.

\subsection{The complex structure and the clock}
Let $J\in O_8(\Z)$ rotate each $\mu_4$ pair,
$e_{2k}\mapsto e_{2k+1}\mapsto-e_{2k}$, and let $\sigma\in O_8(\Z)$
be the pair $3$-cycle $e_0\mapsto e_2\mapsto e_4\mapsto e_0$,
$e_1\mapsto e_3\mapsto e_5\mapsto e_1$, fixing $e_6,e_7$.  Then
(machine checks I0.2--I0.3; Lean theorems \texttt{J\_sq},
\texttt{J\_skew}, \texttt{sigma\_cubed\_ambient},
\texttt{J\_sigma\_commute}, \texttt{lattice\_J},
\texttt{lattice\_sigma})
\[
J^2=-1,\qquad J^{\mathsf T}=-J,\qquad \sigma^3=1,\qquad
[J,\sigma]=0,\qquad JL=L,\qquad \sigma L=L ,
\]
where the last two use precisely the $\pi_J$- and
$\pi_\sigma$-invariance of the placement $\Cst$ (sign changes are
invisible mod $2$).  Both $J$ and $\sigma$ preserve the root set, so
both lie in the Weyl group $W(E_8)$ ($E_8$ has no diagram
automorphisms).  Setting $i\cdot x:=Jx$ makes $L$ a torsion-free
$\Z[i]$-module of rank $4$, and $\sigma$ is $\Z[i]$-linear.  In the
source modules of the verification program, $\sigma$ arises as the
fourth power of an order-$12$ ``clock'' element; here it is simply
the explicit matrix above.

\begin{lemma}[Hermitian unimodularity]\label{lem:herm}
Define $h(x,y):=\tfrac12\bigl(\ip xy+i\,\ip x{Jy}\bigr)$.  Then $h$ is
a $\Z[i]$-valued Hermitian form on $L$ with $h(x,x)=\tfrac12\ip xx$,
minimum $2$, and $(L,h)$ is \emph{unimodular}: the Hermitian dual of
$L$ is $L$ itself.  Moreover $|(1+J)x|^2=2\,|x|^2$ for all $x$, i.e.\
multiplication by $1+i$ doubles norms exactly.
\end{lemma}

\begin{proof}
By \eqref{eq:douleven} and polarization, $\ip xy\in2\Z$ for all
$x,y\in L$; since $JL=L$, also $\ip x{Jy}\in2\Z$, so $h$ takes values
in $\Z[i]$.  Sesquilinearity is the two identities
$\ip{Jx}y=-\ip x{Jy}$ (skewness) and $\ip{Jx}{Jy}=\ip xy$
(orthogonality), which give $h(Jx,y)=i\,h(x,y)$; skewness also gives
$\ip x{Jx}=0$, hence $h(x,x)=\tfrac12\ip xx\ge2$.  For unimodularity:
the $\Z$-dual of $L$ is $L^{\sharp}=\tfrac12L$ (determinant
$16^2=256$), and $h(x,L)\subseteq\Z[i]$ is equivalent, using $JL=L$,
to $\ip xL\subseteq2\Z$, i.e.\ $x\in2L^{\sharp}=L$.  Finally
$|(1+J)x|^2=|x|^2+2\ip x{Jx}+|Jx|^2=2|x|^2$; in matrix form
$(1+J)^{\mathsf T}(1+J)=2\cdot\mathbf 1$, certified by the Lean kernel
(theorem \texttt{one\_add\_J\_gram}).
\end{proof}

\section{The four-bit quotient and the
\texorpdfstring{$15\times16$}{15 x 16} census}\label{sec:census}

All checks of this section are from
\texttt{gaussian\_code\_bridge\_probe.py} ($26$ checks, $0$ failures,
verdict \textsc{gaussian-code-bridge-exact}; exact integer and
\texttt{Fraction} arithmetic throughout, \texttt{sympy} only for the
Smith normal form), with the finite certificates re-proved by the
Lean kernel in \texttt{GaussianCodeBridge.lean}.

\begin{theorem}[the Gaussian code bridge, part I: the census]
\label{thm:census}
Let $L=A(\Cst)$ with the $\Z[i]$-structure of
Section~\ref{sec:setup}, and let $(1+i)L=(1+J)L$.
\begin{enumerate}
\item[(i)] $2L\subseteq(1+i)L$, the index is
$[L:(1+i)L]=\det(1+J)=2^4=16=N(1+i)^4$, and
\[
L/(1+i)L\;\cong\;\F_2^4
\]
as an $\F_2$-vector space; the elementary divisors of
$(1+i)L\subseteq L$ are $(1,1,1,1,2,2,2,2)$.
\item[(ii)] \textbf{The zero class is empty on roots}: no root lies
in $(1+i)L$.  Indeed $\min L=4$ by \eqref{eq:douleven}, and by
Lemma~\ref{lem:herm} $\min\,(1+i)L=2\cdot4=8>4$.
\item[(iii)] \textbf{Equidistribution}: each of the $15$ nonzero
classes contains exactly $16$ roots, $240=15\times16$
(finite kernel certificate).
\item[(iv)] \textbf{$\mu_4$-stability}: $Jx\equiv x \bmod (1+i)L$ for
every $x\in L$; in particular every class is $\mu_4$-stable.
\item[(v)] $J$ acts freely on the roots, partitioning them into $60$
\emph{lines} $\{\pm x,\pm Jx\}$ (the Gaussian root lines); each
nonzero class is a union of exactly $4$ lines, $60=15\times4$.
\end{enumerate}
\end{theorem}

\begin{proof}
(i) $2=-i\,(1+i)^2$ in $\Z[i]$, so $2L\subseteq(1+i)L$ and the
quotient is elementary $2$-abelian.  On each pair, $1+J$ acts by
$\bigl(\begin{smallmatrix}1&-1\\1&1\end{smallmatrix}\bigr)$ of
determinant $2$, so $\det(1+J)=2^4=16$ and the quotient has order
$16$, hence $\F_2$-dimension $4$.  The elementary divisors are
certified in Lean by an explicit Smith certificate: integer matrices
$P,Q$, unimodular in both directions
($PP^{-1}=P^{-1}P=QQ^{-1}=Q^{-1}Q=\mathbf 1$), with
$PAQ=\mathrm{diag}(1,1,1,1,2,2,2,2)$ and the converse ingredient
$DQ^{-1}=PA$, where $A$ expresses $(1+i)b_j$ in a $\Z$-basis
$(b_j)$ of $L$ (theorems \texttt{smith\_certificate},
\texttt{P\_unimodular}, \texttt{Q\_unimodular},
\texttt{smith\_converse\_ingredient}, \texttt{index\_sixteen},
\texttt{snf\_exponent\_two}).

(ii) is the displayed two-line argument; the probe additionally
enumerates all vectors of norm $<4$ (none) and finds $0$ roots in the
zero class (check I2.2); the Lean census re-proves it exactly
(\texttt{census\_zero\_class\_empty}).

(iii) is a finite decision: the probe reduces all $240$ roots
(check I2.3, census $\{16\colon15\}$), and the Lean kernel certifies,
over the explicit list of the $240$ root coordinate vectors (pairwise
distinct, norm $4$, congruent to codewords mod $2$), that the SNF
residue map hits every nonzero label exactly $16$ times
(\texttt{census\_equidistribution}).

(iv) $i-1=i(1+i)$, so $(J-1)x=J(1+J)x\in(1+i)L$ for all $x\in L$.
(Lean: the $\mu_4$ transport acts as the identity on the label block,
\texttt{mu4\_acts\_trivially\_on\_labels}, and relabeling all $240$
roots after the $J$-action reproduces the label list verbatim,
\texttt{census\_mu4\_stable}.)

(v) $Jx=\pm x$ forces $x=0$ (apply $J$ once more and use $J^2=-1$),
so the $\mu_4$-orbits $\{\pm x,\pm Jx\}$ of roots have size $4$ and
there are $240/4=60$ of them (check I2.5).  Given (iii) and (iv),
each class contains $16/4=4$ complete lines.
\end{proof}

\begin{remark}[what needs the placement and what does not]
\label{rem:placement}
Parts (i)--(v) use only the $\pi_J$-invariance of the placement: the
probe re-runs the census over the \emph{non-equivariant} naive
placement (which is $\pi_J$- but not $\pi_\sigma$-invariant) and
finds the same $15\times16$ equidistribution and $4$-lines-per-class
structure (check I4.2).  The census is a property of the pair
$(E_8,J)$ alone.  What dies without $\pi_\sigma$-equivariance is
exactly the semantics of Section~\ref{sec:info} (control I4.1).  The
census is also presentation independent: re-run in the standard
$E_8$ coordinates (doubled model, basis determinant $256=2^8$), it
returns the same Smith form and the same $15\times16$ census
(check I5.1).
\end{remark}

\section{The information layer}\label{sec:info}

Since $\sigma$ is $\Z[i]$-linear and preserves $L$, it preserves
$(1+i)L$ and descends to an $\F_2$-linear map $\bar\sigma$ on
$L/(1+i)L\cong\F_2^4$.  (Well-definedness is itself a kernel
certificate: the transport matrix of $\sigma$ into Smith coordinates
has even top-right block, Lean theorem \texttt{sigma\_label\_block}.)

\begin{theorem}[the Gaussian code bridge, part II: the information
layer]\label{thm:info}
\begin{enumerate}
\item[(i)] $\bar\sigma^3=1$, $\bar\sigma\neq1$, and the fixed space
of $\bar\sigma$ has dimension $2$ (exactly $4$ fixed labels, $3$ of
them nonzero).
\item[(ii)] On the $15$ root-bearing classes, $\bar\sigma$ acts with
orbit census $3$ fixed classes $+$ $4$ three-cycles.
\item[(iii)] There is a basis $(F_1,F_2,F_3,A)$ of $\F_2^4$ with
\[
\bar\sigma:\ F_1\to F_2\to F_3\to F_1,\qquad \bar\sigma A=A :
\]
$\bar\sigma$ is the \emph{family $3$-cycle with fixed anchor} --- the
information-bit action of the equivariant $\mathrm{RM}(1,3)$
placement, in which each $\mu_4$ pair carries one message bit, the
three moving pairs are the families and the fixed pair is the anchor.
The identification with the $\mathrm{RM}(1,3)$ message space is
unique up to the centralizer of $\bar\sigma$ in $\GL(4,\F_2)$, which
has order exactly $18=|\GL_2(\F_2)|\cdot|\F_4^\times|=6\times3$.
\item[(iv)] \textbf{The coordinate-class law}: the $16$ coordinate
roots $\pm2e_i$ form exactly one class, and that class contains
nothing else; it is $\sigma$-fixed and equals $F_1+F_2+F_3$.  Thus
$240=14\times16+16$ with the coordinate block as the fifteenth
message label, the ``sum of the families''.
\end{enumerate}
\end{theorem}

\begin{proof}
\sloppy
(i) and (iv) are finite kernel certificates (Lean theorems
\texttt{sigma\_cubed}, \texttt{sigma\_nontrivial},
\texttt{sigma\_fixed\_space}, \texttt{sigma\_fixed\_nontrivial},
\texttt{family\_three\_cycle}, \texttt{anchor\_fixed},
\texttt{family\_anchor\_spans}, \texttt{coord\_root\_ambient},
\texttt{coord\_class\_eq\_family\_sum},
\texttt{coord\_class\_sigma\_fixed}; probe checks I2.6a--d, I3.1--2),
including the direct census equivariance: relabeling all $240$ roots
after the $\sigma$-action equals the $M_{\bar\sigma}$-image of the
label list (\texttt{census\_sigma\_equivariant}).  (ii) is probe
check I2.6c (orbit census $\{1\colon3,\,3\colon4\}$).  For the gauge
count in (iii): since $|\langle\bar\sigma\rangle|=3$ is odd, the
$\F_2\langle\bar\sigma\rangle$-module $\F_2^4$ is semisimple and
decomposes as (trivial)$^2\oplus\F_4$, so the centralizer is
$\GL_2(\F_2)\times\F_4^\times$ of order $6\times3=18$; the probe
confirms by enumerating all of $\GL(4,\F_2)$ (check I2.6e).  The
$\mathrm{RM}(1,3)$ reading of (iii) is the content of the equivariant
placement: $\pi_\sigma$ permutes the three family pairs cyclically
and fixes the anchor pair, and $\bar\sigma$ realizes exactly this
permutation matrix on the message space.  (This last identification,
up to the order-$18$ gauge, is verified numerically in the probe; the
Lean layer formalizes (i), (ii) --- via the fixed-label count ---,
(iv) and the transport certificates, but not the gauge statement:
see the honest scope in Section~\ref{sec:verification}.)
\end{proof}

\begin{remark}[the bridge is not the mod-2 reduction]
\label{rem:notmod2}
The Gaussian classes cut \emph{across} the Construction-A fibers
(probe check I3.3): every class mixes codeword fibers, as the
following complete census shows (probe I3.2 table; each fiber entry
means $8+8$ roots over the two named weight-$4$ codewords, except the
coordinate class).  Here $t(d)$ is the even transversal with in-pair
digits $d$, and $\bar d$ its complement.
\begin{center}
\small
\begin{tabular}{@{}lll@{}}
\toprule
classes (basis $F_1,F_2,F_3,A$) & $\bar\sigma$-action &
codeword fibers of the $16$ roots\\
\midrule
$F_1,\ F_2,\ F_3$ & $3$-cycle &
$8$ over a family--anchor $+$ $8$ over a family--family word\\
$F_1{+}F_2,\ F_2{+}F_3,\ F_3{+}F_1$ & $3$-cycle &
$8$ over a family--anchor $+$ $8$ over a family--family word\\
$F_1{+}A,\ F_2{+}A,\ F_3{+}A$ & $3$-cycle &
$8+8$ over a complementary pair $t(d),t(\bar d)$\\
$F_i{+}F_j{+}A$ (three classes) & $3$-cycle &
$8+8$ over a complementary pair $t(d),t(\bar d)$\\
$A$ and $F_1{+}F_2{+}F_3{+}A$ & fixed &
$8+8$ over $t(0000)$ and $t(1111)$\\
$F_1{+}F_2{+}F_3$ (coordinate class) & fixed &
all $16$ over the zero codeword: the roots $\pm2e_i$\\
\bottomrule
\end{tabular}
\end{center}
The three $\bar\sigma$-fixed nonzero classes are the coordinate class
$F_1{+}F_2{+}F_3$, the anchor class $A$, and their sum.  The code
that \emph{builds} the lattice (as fiber data of Construction A)
reappears after Gaussian reduction as the \emph{message space} of its
own lattice --- with the fibers redistributed.
\end{remark}

\section{The quartic companion:
\texorpdfstring{$G_{31}$}{G31} as the holomorphic
\texorpdfstring{$\mu_4$}{mu4} shadow}\label{sec:quartic}

All checks of this section are from \texttt{quartic\_half\_probe.py}
($22$ checks, $0$ failures, verdict \textsc{quartic-half-alive};
exact Gaussian-integer and Gaussian-rational arithmetic, no floats
anywhere), run in the standard doubled-coordinate model of $E_8$
(roots $2(\pm e_i\pm e_j)$ and $(\pm1)^8$ with an even number of
minus signs; norm $8$), which by Remark~\ref{rem:placement} carries
the same bridge.  The provable core is formalized in
\texttt{QuarticHalf.lean}.

\subsection{The degree bookkeeping}
The exponents of $W(E_8)$ are
$\Exp(E_8)=\{1,7,11,13,17,19,23,29\}$, the totatives of the Coxeter
number $h=30$ \cite{Bou68}.  The character $\chi_{-4}$ (residue mod
$4$) splits them: the exponents $\equiv3\bmod4$ are $\{7,11,19,23\}$,
and shifted by $+1$,
\[
\{7,11,19,23\}+1=\{8,12,20,24\}=\Deg(G_{31}),
\]
the degree quadruple of the rank-$4$ complex reflection group
$G_{31}$ in the Shephard--Todd classification \cite{ST54,LT09}.  Both
the split sum and its complement sum equal
$7+11+19+23=1+13+17+29=60$, the number of mirror lines of $G_{31}$,
and $8\cdot12\cdot20\cdot24=46080=|G_{31}|$.  Equivalently, the
degrees $\Deg W(E_8)=(2,8,12,14,18,20,24,30)$ split mod $4$ into the
$G_{31}$ half $\{8,12,20,24\}$ ($\equiv0$) and the complement
$\{2,14,18,30\}$ ($\equiv2$).  Conceptually this is Springer's theory
of regular elements \cite{Spr74}: $J$ is a $\zeta_4$-regular element
of $W(E_8)$ (it acts freely on the roots, so its $i$-eigenspace
contains regular vectors), and the centralizer of $J$ acts on
$V^{1,0}=\ker(J-i)\subset\C^8$ ($\dim_\C=4$) as the reflection group
with degrees the $W(E_8)$-degrees divisible by $4$ --- that is,
$G_{31}$.  The $60$ mirror lines of this action are spanned by the
$60$ Gaussian root lines of Theorem~\ref{thm:census}(v), and the
probe verifies exactly that the $60$ Hermitian reflections in these
lines are involutions permuting the $240$ roots (check II3.1).

\subsection{The restriction theorem}
For $d\ge1$ let $F_d(x)=\sum_{\alpha}\ip\alpha x^d$, summed over the
$240$ roots, and let $F_d|$ denote the restriction to $V^{1,0}$,
computed in the holomorphic weights
$\ip\alpha{b_k}$, $b_k=e_{2k}-ie_{2k+1}$.  Write
$q(x)=\ip xx$.

\begin{theorem}[quartic invariant restriction, honestly layered]
\label{thm:quartic}
\begin{enumerate}
\item[(a)] \emph{(Vanishing half: true but trivial.)}  For every
$d\not\equiv0\bmod4$, $F_d|=0$ identically.  Proof: the weight law
$W(J\alpha)=-i\,W(\alpha)$ holds for all $240$ roots, so each
$\mu_4$-orbit $\{\alpha,J\alpha,-\alpha,-J\alpha\}$ contributes
$t^d\bigl(1+(-i)^d+(-1)^d+i^d\bigr)=0$; the orbit factor vanishes if
and only if $d\not\equiv0\bmod4$.  This proves the vanishing of the
degrees $\{2,14,18,30\}$ --- but equally of $6,10,22,26$: the pattern
is $\mu_4$-trivial and carries no $G_{31}$ content.
\item[(b)] \emph{(Isotropy layer: still no $G_{31}$ content.)}
$V^{1,0}$ is $q$-isotropic, and the symbolic $8$-variable identities
\[
f_4=576\,q^2,\qquad f_6=1920\,q^3
\]
hold for the (doubled) root power sums --- $W(E_8)$ has no basic
invariant in degrees $4,6$ --- so $F_4|=F_6|=F_{10}|=0$ on \emph{any}
$q$-isotropic subspace, whether or not the complex structure is
root-compatible (the degree-$10$ case because every degree-$10$
invariant is a combination of $q^5$ and $q f_8$).
\item[(c)] \emph{(The load-bearing content.)}  The restrictions
$F_8|,F_{12}|,F_{20}|,F_{24}|$ are nonzero (exact-point evaluation),
invariant under all $60$ Hermitian reflections and under
$\sigma$ and $J$, and \emph{algebraically independent} (exact Jacobian
$\neq0$).  Since their degrees $(8,12,20,24)$ multiply to
$46080=|G_{31}|$, Chevalley's theorem \cite{Che55,LT09} makes them a
system of \emph{basic invariants} of $G_{31}$: the restriction of the
$W(E_8)$-invariant ring to $V^{1,0}$ generates the full
$G_{31}$-invariant ring.
\item[(d)] \emph{(Jacobian mirror factorization.)}
$\deg\Jac(F_8|,F_{12}|,F_{20}|,F_{24}|)=\sum(d_i-1)=60$, the number
of mirror lines; the Jacobian vanishes at exact generic points on
each of the $60$ mirrors and is nonzero off them, consistent with the
standard factorization $\Jac=c\prod_{60}(\text{mirror forms})$
\cite[Ch.~9]{LT09} --- the full symbolic degree-$60$ expansion was
not performed and is recorded as a named residual.
\end{enumerate}
\end{theorem}

The certification levels are: (a) is proved symbolically (probe
II2.1--II2.2; Lean theorems \texttt{weight\_pair\_J},
\texttt{orbit\_factor\_iff}, \texttt{orbit\_powersum\_vanishes} over
$\C$, with the mod-$4$ degree bookkeeping
\texttt{deg\_we8\_mod\_four\_split}).  In (b), $f_4=576\,q^2$ is a
kernel-checked polynomial identity over \emph{any} commutative ring,
assembled from the two explicit root blocks ($112$ D8-type roots
contributing $448\sum x_i^4+384\sum_{i<j}x_i^2x_j^2$ and $128$ spinor
roots contributing $384\,q^2-256\sum x_i^4$; Lean theorems
\texttt{quartic\_d8\_block}, \texttt{quartic\_spinor\_block},
\texttt{quartic\_powersum}), and $F_4|=0$ follows by the isotropy
collapse $1+(-i)^2=0$ (\texttt{holomorphic\_isotropy},
\texttt{quartic\_restriction\_vanishes}); $f_6=1920\,q^3$ and the
all-$35$-coefficients check of $F_4|$ are exact symbolic computations
in the probe (II2.3, II2.5).  In (c), nonvanishing is rigorous by a
nonzero exact value at the Gaussian point
$z=(-3+3i,\,-3+2i,\,-3+2i,\,-3)$ for all
$d\in\{8,12,16,20,24,28\}$ (II2.6 --- honestly including the
non-degrees $16,28$: nonvanishing alone is generic mod-$4$ behaviour;
the $G_{31}$ content is invariance $+$ independence); invariance is
exact at a $4\Z[i]$-point for all $60$ reflections and at $3$ exact
points for each clock generator (II3.2); independence is the exact
Jacobian at $3$ exact random points off all mirrors, with $10$ small
integer points honestly rejected because they landed \emph{on}
mirrors, where the Jacobian must vanish (II3.3).  In (d) the mirror
vanishing is verified at $2$ exact generic points on each of the
$60$ mirrors, $60/60$ (II3.5).  The generation statement ``the $60$
reflections generate $G_{31}$'' is cited (Springer theory
\cite{Spr74,LT09}; repository module \texttt{v634}), not re-proved.

\subsection{Must-fail controls}
A structure claim needs controls that destroy it.  Four are run
(probe II4, all firing as demanded):
\begin{itemize}
\item[(0)] \emph{Honest negative first.}  The natural candidate
control --- flipping the orientation of one pair,
$J'=S_7JS_7$ --- does \emph{not} fire: $J'=J\circ S_{67}$ with the
even sign flip $S_{67}\in W(D_8)\subset W(E_8)$, so $J'$ preserves
all $240$ roots.  No signed-permutation complex structure can break
root compatibility; a genuine control must leave the integral
orthogonal group.
\item[(a)] $J'=RJR^{\mathsf T}$ with $R$ the exact rational
$(3,4,5)$-rotation crossing two $\mu_4$ pairs: an orthogonal complex
structure ($J'^2=-1$) that preserves only $24/240$ roots.  The
trivial layers persist ($F'_2=F'_4=F'_6=F'_{10}=0$: isotropy and
$q$-powers, exactly as (b) predicts), but the informative half
breaks: $F'_d\neq0$ for all $d\in\{14,18,22,26,30\}$.  The vanishing
pattern of Theorem~\ref{thm:quartic}(a) is a property of
\emph{root-compatible} complex structures, not of orthogonal complex
structures per se.
\item[(b)] The root-preserving twin $J''=S_{57}JS_{57}$
($240/240$ roots kept): the full vanishing pattern survives on
$\ker(J''-i)$ --- the theorem is about the $W(E_8)$-conjugacy class
of $J$, not one matrix.
\item[(c)] A random non-isotropic $4$-space: already
$F_2=-56880-61440\,i\neq0$ --- even the first layer needs an
orthogonal complex structure.
\end{itemize}
On the bridge side (probe I4): the naive (non-equivariant) placement
keeps the $\Z[i]$-module and the census but loses the
$\sigma$-semantics --- $\sigma$ maps the codeword lift
$(0,0,0,1,1,1,1,0)$ off the lattice, so step (iii) of
Theorem~\ref{thm:info} is \emph{undefined} there (I4.1--I4.2);
$16$ of the $30$ placements are not even $\pi_J$-invariant, and for
those no $\Z[i]$-module exists at all (witness root
$(-1,-1,-1,0,-1,0,0,0)$ with $J$-image off the lattice, I4.3); and on
the \emph{other} unimodular Hermitian $\Z[i]$-lattice of rank $4$,
the standard $\Z[i]^4$, the census trivializes: only $16$ minimal
vectors, occupying $4$ of the $15$ nonzero classes with $4$ each,
$11$ classes empty --- no $240$, no $15\times16$, no
$\mathrm{RM}(1,3)$ (I4.4).  The bridge needs $E_8$.

\section{Machine verification}\label{sec:verification}

\subsection{The two probes}
\begin{center}
\footnotesize
\setlength{\tabcolsep}{4pt}
\begin{tabular}{@{}lccl@{}}
\toprule
probe & checks & verdict & arithmetic\\
\midrule
\texttt{gaussian\_code\_bridge\_probe.py} & $26/26$ &
\textsc{gaussian-code-bridge-exact} &
exact $\Z$/\texttt{Fraction}; SNF via \texttt{sympy}\\
\texttt{quartic\_half\_probe.py} & $22/22$ &
\textsc{quartic-half-alive} &
exact $\Z[i]$/$\mathbb Q(i)$; no floats\\
\bottomrule
\end{tabular}
\end{center}
Both probes cross-validate their own machinery: the class map is
computed twice (Hermite-normal-form labels versus the direct
membership test $(1-J)(x-y)/2\in L$, $300$ random cases, I1.5), the
census is re-run in a second coordinate model (I5.1), and the
Jacobian points are rejection-sampled off the mirrors with the
rejections printed (II3.3).  Both files are promoted unchanged to the
permanent verification suite of the repository \cite{TFPT} as the
modules \texttt{v689\_gaussian\_code\_bridge} and
\texttt{v690\_quartic\_half}.

\emph{Dated pointer (2026-08-07).}  The four roles of the ramified
prime $\pi_2=1+i$ documented across the program --- the norm-doubling
/ empty-zero-class census of this note (Theorem~\ref{thm:census}),
the $4$-bit address $L/(1+i)L\cong\mathbb F_2^4$, the non-split jet
$L/2L$ over $\Z[i]/(2)\cong\mathbb F_2[\epsilon]/(\epsilon^2)$ with
deck $=1+\epsilon$ (repository module \texttt{v803}), and the
metaplectic lift $\zeta_8=(1+i)/\sqrt2$ with the two-qubit Clifford
coset (\texttt{v783}/\texttt{v798}) --- have since been re-certified
from scratch as \emph{one} machine-checked ladder in the suite module
\texttt{v833\_gaussian\_ramification\_ladder} ($33/33$ exact,
verdict \textsc{ramification-ladder-exact}); this note's census is
rebuilt there unchanged.

\subsection{The Lean layer}
The algebraic cores are formalized in two Lean~4 modules over
Mathlib \cite{Moura21,mathlib}, committed to the repository's Lean
project (\texttt{lake build} green, no \texttt{sorry}, no
\texttt{native\_decide}): \texttt{GaussianCodeBridge.lean}
($44$ theorems) and \texttt{QuarticHalf.lean} ($21$ theorems), $65$
kernel-checked theorems in total.  The finite certificates are proved
by the kernel-checked \texttt{decide} tactic over explicit integer
data --- notably the code-equivariance of $\Cst$, the norm-doubling
Gram identity $(1+J)^{\mathsf T}(1+J)=2\cdot\mathbf1$, the full Smith
certificate with bidirectionally unimodular transforms, the census of
the explicit $240$ root coordinate vectors (pairwise distinct, norm
$4$, in the code mod $2$; zero class empty; every nonzero label hit
exactly $16$ times), the $\mu_4$- and $\sigma$-transport certificates
with the explicit label-block matrix $M_{\bar\sigma}$, the family
$3$-cycle with anchor, and the coordinate-class law
$\mathrm{label}(2e_0)=F_1+F_2+F_3$.  The polynomial identity
$f_4=576\,q^2$ is proved by \texttt{ring} over an arbitrary
commutative ring after unfolding the explicit $240$-element root
list.

\emph{Honest scope of the formal layer.}  The quotient $L/(1+i)L$ is
not built as a Mathlib quotient module; the Lean statements concern
the explicit Smith residue map and explicit matrices, and the
standard SNF argument identifying the quotient is cited, not
formalized.  Completeness of the $240$-element root list (that these
are \emph{all} norm-$4$ vectors) is the probe's exhaustive-enumeration
job, re-used, not re-proved, in Lean.  The identification of
$\bar\sigma$ with the $\mathrm{RM}(1,3)$ family permutation up to the
order-$18$ gauge, and the entire $G_{31}$ layer of
Theorem~\ref{thm:quartic}(c)--(d) beyond $f_4=576\,q^2$ and the
$\mu_4$-orbit mechanism, rest on the probes' exact-point
computations plus the cited Chevalley and factorization theorems.

\section{Scope and outlook}\label{sec:scope}

What is established is finite algebra, fully certified: the pair
$(E_8,\mu_4)$ carries a canonical four-bit quotient on which the
$240$ roots equidistribute as $15$ messages $\times$ $16$ roots
(${}=4$ Gaussian lines) each, with a distinguished coordinate block;
the clock $\sigma$ equips the quotient with the family/anchor
semantics of the code that built the lattice; and the holomorphic
$\mu_4$ shadow of the $W(E_8)$ invariant ring is exactly the
$G_{31}$ invariant ring, with the vanishing half of the degrees typed
honestly as the trivial $\mu_4$-orbit factor.  We find the
combination noteworthy: Construction A uses the $[8,4,4]$ code as
\emph{fiber} data, and the Gaussian reduction returns the same code's
four-bit \emph{message} space as an intrinsic invariant of the
lattice-with-clock, with the fibers redistributed across the classes
(Remark~\ref{rem:notmod2}).  Within the verification program that
produced it, this note is typed as structure --- an information layer
of the $E_8$ compiler datum --- and moves no status marker.  No claim
is made beyond the stated algebra: no physical readout, no arithmetic
consequence, and nothing about any open conjecture is asserted or
implied.

\small
\begin{thebibliography}{9}
\bibitem{CS99} J.~H.~Conway and N.~J.~A.~Sloane,
\emph{Sphere Packings, Lattices and Groups}, 3rd ed.,
Grundlehren der mathematischen Wissenschaften 290, Springer, New York
(1999).
\bibitem{MS77} F.~J.~MacWilliams and N.~J.~A.~Sloane,
\emph{The Theory of Error-Correcting Codes}, North-Holland,
Amsterdam (1977).
\bibitem{ST54} G.~C.~Shephard and J.~A.~Todd,
\emph{Finite unitary reflection groups},
Canad.\ J.\ Math.\ 6 (1954), 274--304.
\bibitem{Che55} C.~Chevalley,
\emph{Invariants of finite groups generated by reflections},
Amer.\ J.\ Math.\ 77 (1955), 778--782.
\bibitem{Spr74} T.~A.~Springer,
\emph{Regular elements of finite reflection groups},
Invent.\ Math.\ 25 (1974), 159--198.
\bibitem{LT09} G.~I.~Lehrer and D.~E.~Taylor,
\emph{Unitary Reflection Groups}, Australian Mathematical Society
Lecture Series 20, Cambridge University Press, Cambridge (2009).
\bibitem{Bou68} N.~Bourbaki,
\emph{Groupes et alg\`ebres de Lie, Chapitres 4--6},
Hermann, Paris (1968).
\bibitem{Moura21} L.~de~Moura and S.~Ullrich,
\emph{The Lean 4 theorem prover and programming language},
in: Automated Deduction -- CADE 28, Lecture Notes in Computer
Science 12699, Springer (2021), 625--635.
\bibitem{mathlib} The mathlib Community,
\emph{The Lean mathematical library},
in: Proc.\ 9th ACM SIGPLAN Int.\ Conf.\ on Certified Programs and
Proofs (CPP 2020), ACM (2020), 367--381.
\bibitem{TFPT} TFPT repository
(\url{https://fixpoint-theory.com}): discovery probes
\texttt{experiments/tfpt-discovery/gaussian\_code\_bridge\_probe.py}
and \texttt{quartic\_half\_probe.py}; suite modules
\texttt{v689\_gaussian\_code\_bridge},
\texttt{v690\_quartic\_half} (and the predecessor modules
\texttt{v626}, \texttt{v634}, \texttt{v638} for the Construction-A
code layer, the $G_{31}$ structure and the equivariant placement);
Lean~4 proof modules
\texttt{lean4-carrier-rigidity/TfptCarrier/GaussianCodeBridge.lean}
and \texttt{QuarticHalf.lean} (2026).
\end{thebibliography}

\end{document}