\section{Two formal routes}\label{sec:gap}

Comparator checks two theorems for the SiegelZeros challenge: exists\_absolute\_real\_zero\_gap and dirichletRealZeroBound\_proof.
Their statements are not the same Lean proposition: the first takes 0 < beta, beta < 1 and the vanishing of the L-function as three successive implications, the second as one conjunction.
ChallengeEquivalence.statements\_equivalent, in a Mathlib-only file, proves the two statements equivalent, with the axioms [propext, Classical.choice, Quot.sound].
OAI's catalogue lean/formalization.yaml names exists\_absolute\_real\_zero\_gap as the main result for the SiegelZeros config; neither it nor lean/docs/003.md names the paper's Theorem 1.
OAI proves the two theorems by two routes, the main route and the second route below.

\subsection{The main route}

Listing~\ref{lst:main-route} quotes the proof of exists\_absolute\_real\_zero\_gap and the theorem it applies.
uniform\_exclusion\_of\_local\_isolated\_bezout applies uniform\_exclusion\_of\_actual\_cutoff and obtains its spanning hypothesis from W28.actualCutoffSpanning\_of\_localBezout.
uniform\_exclusion\_of\_actual\_cutoff argues by contradiction: it takes W63.exists\_good\_mass\_for\_actual\_zeros\_normalized, fixes H := 86713344, takes a contrary sequence of genuine zeros, and closes with false\_of\_eventual\_exists\_pivot\_master and exists\_actual\_character\_pivot\_master.

\begin{listing}[tbp]
\caption{The main route: OAI/\allowbreak NumberTheory/\allowbreak SiegelZeros/\allowbreak Conclusions/\allowbreak Theorem.lean:18-19 and Intersection/BezoutBoundary.lean:13-19 (openai/math fd4aeeb).}\label{lst:main-route}
\begin{Verbatim}
  exact SiegelZerosAwei.W50.uniform_exclusion_of_local_isolated_bezout
    (W22.localIsolatedBezout_of_actual_regular_selection ℂ)
\end{Verbatim}
\begin{Verbatim}
theorem uniform_exclusion_of_local_isolated_bezout
    (hBezout : W22.LocalIsolatedBezoutStatement ℂ) :
    UniformSiegelZeroExclusion := by
  apply uniform_exclusion_of_actual_cutoff
  intro H N hH hHN _hN d a hd hd1 hd2 ha
  exact W28.actualCutoffSpanning_of_localBezout hBezout H N (by omega) hHN
    d hd hd1 hd2 a ha
\end{Verbatim}
\end{listing}

The spanning hypothesis is W50.ActualCutoffSpanning (Listing~\ref{lst:cutoff-spanning}).
It states that, over L = rootField a sqrtTwo, the weighted theta rows of the box exponents span when restricted to the weighted cutoff W62.cutoff H (sourceCutoff H N).
The cutoff is the set of indices with a.coords 0 + H a.coords 1 + H a.coords 2 at most sourceCutoff H N, the floor of 96 H\textasciicircum(2/3) N\textasciicircum(4/3).
actualCutoffSpanning\_of\_localBezout proves it for 0 < H <= N and squarefree d != 1, 2 from W22.LocalIsolatedBezoutStatement C, by mapping to C with rowSpan\_top\_of\_field\_map and applying actual\_complex\_cutoff\_spanning.
That theorem combines cutoff\_span\_of\_rectangularAssertion with actual\_rectangularAssertion\_of\_localBezout.
RectangularAssertion (Listing~\ref{lst:rect-assertion}) is a zero test with Corollary 4's bounds, 32 H\textasciicircum(2/3) N\textasciicircum(4/3) and 32 H\textasciicircum(-1/3) N\textasciicircum(4/3).
So the main route does not use actual\_biquadratic\_rectangle\_span, but it proves a zero test with the same constants as Corollary 4, from the local Bezout statement.

\begin{listing}[tbp]
\caption{The main route's spanning statement, OAI/\allowbreak NumberTheory/\allowbreak SiegelZeros/\allowbreak Structure/\allowbreak ArithmeticCutoffTransport.lean:356-366 (openai/math fd4aeeb).}\label{lst:cutoff-spanning}
\begin{Verbatim}
def ActualCutoffSpanning (H N : ℕ) (d : ℤ) (a : ℂ) (ha : a ^ 2 = (d : ℂ)) : Prop :=
  let L := SiegelZeros.W10.rootField a W60.sqrtTwo
  let f := algebraMap (𝓞 L) L
  let u := W37.integralRootA a W60.sqrtTwo d ha W60.sqrtTwo_sq
  let v := W37.integralRootB a W60.sqrtTwo d ha W60.sqrtTwo_sq
  let n : Fin (N ^ 4) → Fin 4 → ℤ := fun j i => (boxExponents N j i : ℤ)
  W29.rowSpan (K := L)
    (W60.weightedRow f (fun j => Awei.W39.theta u v (n j))
      (fun j => Awei.W39.theta (-u) v (n j))
      (fun j => Awei.W39.theta (-u) (-v) (n j)))
    (W62.cutoff H (sourceCutoff H N)) = ⊤
\end{Verbatim}
\end{listing}

\begin{listing}[tbp]
\caption{The zero test on the main route, OAI/\allowbreak NumberTheory/\allowbreak SiegelZeros/\allowbreak Determinants/\allowbreak RectangleDeterminant.lean:31-37 (openai/math fd4aeeb).}\label{lst:rect-assertion}
\begin{Verbatim}
def RectangularAssertion (v : Fin 3 → Fin 4 → K) (H N : ℕ) : Prop :=
  ∀ p : MvPolynomial (Fin 4) K, InBox N p →
    (∀ a : Fin 3 → ℕ,
      (a 0 : ℝ) ≤ 32 * (H : ℝ) ^ (2 / 3 : ℝ) * (N : ℝ) ^ (4 / 3 : ℝ) →
      (a 1 : ℝ) ≤ 32 * (H : ℝ) ^ (-(1 / 3 : ℝ)) * (N : ℝ) ^ (4 / 3 : ℝ) →
      (a 2 : ℝ) ≤ 32 * (H : ℝ) ^ (-(1 / 3 : ℝ)) * (N : ℝ) ^ (4 / 3 : ℝ) →
      MvPolynomial.eval (fun _ => (1 : K)) (mixedInvariant v a p) = 0) → p = 0
\end{Verbatim}
\end{listing}

At fd4aeeb the closure of exists\_absolute\_real\_zero\_gap has 107760 constants.
It contains no constant from the 7/8 development, and neither dirichletRealZeroBound\_proof nor actual\_biquadratic\_rectangle\_span.
It contains 9434 CategoryTheory and 3024 AlgebraicGeometry names.

\subsection{The second route}

dirichletRealZeroBound\_proof is exact WeightedTorusJets.dirichlet\_real\_zero\_bound, proved from source\_real\_zero\_uniform\_master\_bound.
This route reaches the paper's Corollary 4 as the theorem actual\_biquadratic\_rectangle\_span, stated at OAI/NumberTheory/SiegelZeros/Structure/InvariantJetLinearMap.lean:471-484.
The file is identical at adc7f12 and fd4aeeb, with LF sha256 \hash{09b8bd7fa82365e69caebfad466d039d85084595376766a731945fa5c11a2bdc}.
Listing~\ref{lst:oai-cor4} quotes the statement.

\begin{listing}[tbp]
\caption{OAI's Corollary 4, OAI/\allowbreak NumberTheory/\allowbreak SiegelZeros/\allowbreak Structure/\allowbreak InvariantJetLinearMap.lean:471-484 (LF sha256 09b8bd7f\ldots, identical at adc7f12 and fd4aeeb).}\label{lst:oai-cor4}
\begin{Verbatim}
theorem actual_biquadratic_rectangle_span
    {K κ : Type*} [Field K] [NumberField K] [Fintype κ]
    (a b : K) (v : Module.Basis (Fin 4) ℚ K)
    (hv : ∀ i, v i = ![1, a, b, a * b] i) (σ τ : K ≃ₐ[ℚ] K)
    (hσa : σ a = -a) (hσb : σ b = b) (hτa : τ a = a) (hτb : τ b = -b)
    (H N : ℕ) (hH : 0 < H) (hHN : H ≤ N)
    (n : κ → Fin 4 → ℕ) (hninj : Function.Injective n) (hn : ∀ j i, n j i < N) :
    let θ := fun j => ∑ i : Fin 4, (n j i : K) * ![1, a, b, a * b] i
    Submodule.span K
      ((fun α : Fin 3 → ℕ => fun j => θ j ^ α 0 * σ (θ j) ^ α 1 *
        (σ * τ) (θ j) ^ α 2) '' {α : Fin 3 → ℕ |
          (α 0 : ℝ) ≤ 32 * (H : ℝ) ^ (2 / 3 : ℝ) * (N : ℝ) ^ (4 / 3 : ℝ) ∧
          (α 1 : ℝ) ≤ 32 * (H : ℝ) ^ (-(1 / 3 : ℝ)) * (N : ℝ) ^ (4 / 3 : ℝ) ∧
          (α 2 : ℝ) ≤ 32 * (H : ℝ) ^ (-(1 / 3 : ℝ)) * (N : ℝ) ^ (4 / 3 : ℝ)}) = ⊤ := by
\end{Verbatim}
\end{listing}

Inside its proof, line 493 applies Geometry.source\_rectangle\_span\_of\_polynomial\_zero\_test and line 496 applies Geometry.uniform\_rectangular\_multiplicity; a text search of lines 485-511 finds no other line naming either lemma.
So on this route OAI proves Corollary 4 by a multiplicity estimate, uniform\_rectangular\_multiplicity, and not by the paper's argument for Lemma 3.
Within the SiegelZeros tree, actual\_biquadratic\_rectangle\_span is used only at CharacterGlobalGreedyDeterminantMasterBounds.lean:138, by a text search of all OAI .lean sources.
After line 138 is replaced, the closure of dirichletRealZeroBound\_proof no longer contains actual\_biquadratic\_rectangle\_span, so line 138 was its only use in that closure.
The control scan of dirichletRealZeroBound\_proof finds 116314 constants in its closure, among them actual\_biquadratic\_rectangle\_span, uniform\_rectangular\_multiplicity and source\_rectangle\_span\_of\_polynomial\_zero\_test, at adc7f12 and again at fd4aeeb.
exists\_good\_mass\_for\_actual\_zeros\_normalized, false\_of\_eventual\_exists\_pivot\_master and exists\_actual\_character\_pivot\_master are in the closure of exists\_absolute\_real\_zero\_gap and in neither the control nor the rerouted closure of dirichletRealZeroBound\_proof.

Three further configurations load modules from a separate copy of this code (namespace OAI.Erdos970), with its own multiplicity estimate.
The reroute concerns the SiegelZeros chain only.
The three are Jacobsthal, JacobsthalImproved and OstmannPrimes, each with a module under OAI.NumberTheory.Jacobsthal.Siegel in its solution import closure (3 of 416 configs); this is an import closure, not a declaration closure.

Rerouting removes 9936 (6901 + 3035) names in the CategoryTheory and AlgebraicGeometry namespaces from route 2, the closure of dirichletRealZeroBound\_proof, counting the names reachable from the root through types and values, as \#find\_deps does.
Counted by first name component in the closures, dirichletRealZeroBound\_proof has 9454 and 3035 such names in the control and 2553 and 0 in the reroute; the difference, 6901 and 3035, equals that figure.
\footnote{Counted over the full lean4export dumps, every declaration in the dump including unreferenced recursors and constructors, the removal is 10107 (7048 + 3059).
}

\subsection{The three spanning statements compared}

Table~\ref{tab:spanning} compares the main route's spanning statement with Lemma3.rectangle and with OAI's actual\_biquadratic\_rectangle\_span, by reading the statements (INFERRED).
By that reading, Lemma3.rectangle, applied with A the directions matrix and c = omegaCoefficients, plus the inclusion of the rectangle in the weighted cutoff and OAI's own rowSpan\_top\_of\_field\_map and boxEnumeration reindexing, would plausibly give ActualCutoffSpanning without the local Bezout statement.
No such proof was written or run.

\begin{table}[tbp]
\caption{The spanning statements, by reading the source (INFERRED).}\label{tab:spanning}
\small
\begin{tabularx}{\textwidth}{@{}l>{\raggedright\arraybackslash}X@{}}
\toprule
aspect & comparison \\
\midrule
rows & all three use products of the three conjugate linear forms of n with exponents a 0, a 1, a 2; after mapping to C the main route's rows are those of A = the directions matrix, whose kernel is spanned by omegaCoefficients \\
exponents & Lemma3.rectangle and actual\_biquadratic\_rectangle\_span: the rectangle a 0 <= 32 H\textasciicircum(2/3) N\textasciicircum(4/3), a 1, a 2 <= 32 H\textasciicircum(-1/3) N\textasciicircum(4/3); the main route: the weighted cutoff a 0 + H a 1 + H a 2 <= floor(96 H\textasciicircum(2/3) N\textasciicircum(4/3)), which contains that rectangle \\
field & Lemma3.rectangle: C; actual\_biquadratic\_rectangle\_span: the number field K; the main route: L = rootField a sqrtTwo, reached from C by rowSpan\_top\_of\_field\_map \\
differences & index set (rectangle versus weighted cutoff), form (span versus the zero test RectangularAssertion), field (C versus L), indexing (Index H, Fin (N\textasciicircum4)) \\
\bottomrule
\end{tabularx}
\end{table}