\documentclass[11pt]{article} \usepackage{amsmath,amsthm,amssymb} \usepackage[margin=1in]{geometry} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage{aliascnt} \usepackage{array} \usepackage{tikz} \usepackage{float} \usetikzlibrary{arrows.meta} \usepackage[protrusion=true,expansion=false]{microtype} \newtheorem{theorem}{Theorem}[section] \newaliascnt{proposition}{theorem} \newtheorem{proposition}[proposition]{Proposition} \aliascntresetthe{proposition} \newaliascnt{lemma}{theorem} \newtheorem{lemma}[lemma]{Lemma} \aliascntresetthe{lemma} \newaliascnt{corollary}{theorem} \newtheorem{corollary}[corollary]{Corollary} \aliascntresetthe{corollary} \newcommand{\Z}{\mathbb Z} \newcommand{\Q}{\mathbb Q} \newcommand{\mat}[1]{\left(\begin{matrix}#1\end{matrix}\right)} \newcommand{\la}{\langle} \newcommand{\ra}{\rangle} % Compact parenthesized moduli, including in displays; keep \bmod unchanged. \renewcommand{\pmod}[1]{\allowbreak\nonscript\;(\mathrm{mod}\,#1)} \title{A Fibonacci Analogue of the Fifteen Theorem} \date{November 11, 2026} \author{Scott Duke Kominers% \thanks{% \textsc{Harvard Business School; Department of Economics and Center of Mathematical Sciences and Applications, Harvard University; and a16z Frontier Research.} }} \usepackage[hidelinks]{hyperref} \hypersetup{ pdftitle={A Fibonacci Analogue of the Fifteen Theorem}, pdfauthor={Scott Duke Kominers} } \providecommand*{\theHproposition}{\theHtheorem} \providecommand*{\theHlemma}{\theHtheorem} \providecommand*{\theHcorollary}{\theHtheorem} \usepackage[capitalize,noabbrev]{cleveref} \crefname{theorem}{Theorem}{Theorems} \crefname{proposition}{Proposition}{Propositions} \crefname{lemma}{Lemma}{Lemmas} \crefname{corollary}{Corollary}{Corollaries} \crefformat{section}{\S#2#1#3} \Crefformat{section}{Section~#2#1#3} \newcommand{\creflastconjunction}{, and~} \Crefname{section}{Section}{Sections} \begin{document} \maketitle \vspace*{-.15in} \begin{abstract} We prove that a positive-definite quadratic form with integral Gram matrix represents every Fibonacci number if and only if it represents the first forty-two of them. The unique minimal criterion set consists of ten Fibonacci numbers, the largest of which is $F_{42}=267914296$. \end{abstract} \section{Introduction}\label{sec:intro} The Conway--Schneeberger Fifteen Theorem \cite{Conway,Bhargava15} states that a positive-definite quadratic form with integral Gram matrix represents every positive integer if and only if it represents \[ \{1,2,3,5,6,7,10,14,15\}. \] We ask the corresponding question for the Fibonacci numbers. Put $F_0=0$, $F_1=1$, and $F_{n+2}=F_{n+1}+F_n$, and write $\mathcal F=\{F_n:n\ge1\}$. A form representing every element of $\mathcal F$ is called \emph{Fibonacci-universal}. For a set $S\subseteq\Z_{>0}$, an \emph{$S$-criterion set} is a finite subset $D\subseteq S$ such that every positive-definite quadratic form with integral Gram matrix representing every element of $D$ also represents every element of $S$. An $\mathcal F$-criterion set is called a \emph{Fibonacci criterion set}. Every $S\subseteq\Z_{>0}$ has a finite criterion set \cite{KKO}, and its minimal criterion set is unique \cite[Theorem~2.2]{KLO}. We identify this set explicitly for the Fibonacci numbers $\mathcal F$. \begin{theorem}[Fibonacci criterion] \label{thm:main} A positive-definite quadratic form with integral Gram matrix is Fibonacci-universal if and only if it represents every element of \[ \begin{aligned} C&=\{1,2,3,5,21,55,610,987,832040,267914296\}\\ &=\{F_1,F_3,F_4,F_5,F_8,F_{10},F_{15},F_{16},F_{30},F_{42}\}. \end{aligned} \] Moreover, every Fibonacci criterion set contains $C$. Thus $C$ is the unique minimal Fibonacci criterion set with respect to inclusion. \end{theorem} \begin{corollary}[The index $42$] \label{cor:forty-two} A positive-definite quadratic form with integral Gram matrix is Fibonacci-universal if and only if it represents $F_1,\ldots,F_{42}$. The index $42$ cannot be lowered: the form $x^2+y^2+2z^2$ represents $F_1,\ldots,F_{41}$ but not $F_{42}$. \end{corollary} The size of the endpoint reflects a local obstruction: $x^2+y^2+2z^2$ omits exactly the positive integers of the form $4^a(16b+14)$, with $a,b\ge0$, and the first Fibonacci number in that family is $F_{42}$. Compared with the integers, the odd integers, or the primes, the Fibonacci numbers are sparse: as $X\to\infty$, Binet's formula gives \[ \#\bigl(\mathcal F\cap[1,X]\bigr) =\frac{\log X}{\log\phi}+O(1), \qquad \phi=\frac{1+\sqrt5}{2}. \] Sparsity alone need not make finding a criterion set difficult: for example, representing $1$ gives every square, and representing $1$ and $2$ gives every power of $2$, simply by scaling vectors. But the Fibonacci criterion is not of this kind. It forces, for example, representation of $F_{13}=233$, although $233$ is not an integer square multiple of any member of $C$. We have formalized our results in Lean~4, with no unproven hypotheses; \hyperref[sec:lean]{the Lean development} closely follows the argument in the sequel. \subsection*{The argument} \paragraph{Escalation.} We use Conway's \emph{escalation} method, as developed in Bhargava's proof of the Fifteen Theorem \cite{Bhargava15}. The \emph{Fibonacci truant} of a lattice is the least Fibonacci number it does not represent. Throughout the paper, \emph{truant} means Fibonacci truant unless explicitly qualified as ordinary. We \emph{escalate} a lattice by adjoining a vector whose norm is its truant; the resulting lattice is an \emph{escalation} of the original lattice. Starting from the zero lattice and making every possible such choice gives the \emph{Fibonacci escalators}. Thus an escalator is a lattice in this construction, whereas an escalation specifies its relation to the preceding lattice. Up to integral isometry, there is one at rank $1$, two at rank $2$, and nine at rank $3$. The truants encountered through rank $2$ are $1,2,3,5$; the ternaries contribute six further distinct values, giving exactly the ten elements of $C$. A useful coincidence connects our argument with the Fifteen Theorem: the ordinary truants (least omitted positive integers) at ranks $0$, $1$, and $2$ are $1,2,3,$ and $5$, all Fibonacci numbers. Thus ordinary and Fibonacci escalation produce exactly the same ternary lattices. At rank $3$, however, their truants differ. For example, $\la1,1,1\ra$ first omits the positive integer $7$, but its first omitted Fibonacci number is $55$. The next Fibonacci escalation therefore adjoins a vector of norm $55$, rather than $7$. We can consequently reuse the initial ternary classification, but must analyze different quaternary extensions. \paragraph{Reduction to quaternary extensions.} Suppose a form represents every element of $C$. Starting with the zero lattice inside it, we can adjoin a vector whose norm is the current truant because each truant encountered through rank $3$ belongs to $C$. We will prove that each step increases the lattice rank (\cref{lem:no-rational-truant}). After four steps, the form therefore contains a quaternary escalator obtained by escalating one of the nine ternaries. To prove sufficiency, it is enough to show that every such quaternary escalator is Fibonacci-universal. We prove that every quaternary extension $M=T+\Z v$ of a ternary escalator $T$ is Fibonacci-universal if it represents the truant of $T$. Here $v\notin T\otimes\Q$; its norm need not itself be the truant. Such an extension contains an orthogonal sublattice $T\perp\la q\ra$ with $q$ bounded in terms of $T$ alone. Since $F_n=(F_n-qk^2)+qk^2$, it is enough to choose an integer $k$ for which the difference \[ F_n-qk^2 \] is nonnegative and represented by $T$. The difference need not itself be a Fibonacci number---it only needs to satisfy the representation criterion for $T$. A positive-definite integral form is \emph{regular} if it represents every positive integer represented locally at every prime. Eight of our nine ternaries are regular; the ninth is not. This distinction determines how we choose $k$. In the regular cases, valuation formulas locate the omitted Fibonacci numbers and bound their prime-power parts by a constant times the index. Exponential growth of $F_n$ then makes their unit parts large enough for the required subtraction. In the irregular case, congruences give a uniform bound on the subtraction, so growth leaves only a finite initial range to check. In both cases, periodic Fibonacci residues supply the needed congruence information; sparsity alone supplies neither these congruences nor the size bounds. \paragraph{The regular escalators.} For each of the eight regular ternaries, the omitted positive integers are described by a valuation and a residue condition at one prime. In most cases, subtracting a suitable $qk^2$ removes this local obstruction, and Fibonacci growth keeps the difference positive. For three ternaries we also use vectors outside the orthogonal sublattice: $\la1,2,2\ra$, $\la1,1,3\ra$, and $\la1,2,5\ra$. For the latter two, quadratic polynomials derived from their representation criteria represent every nonnegative integer. These arguments establish Fibonacci-universality of the extensions without exhaustive searches over quaternary forms. \paragraph{The irregular escalator $f$.} The ninth escalator, \[ f=x^2+2y^2+2yz+4z^2, \] is not regular, so a local condition does not guarantee representation by $f$ alone. Call a positive integer \emph{eligible} if its $7$-adic valuation is even or its $7$-adic unit part is a square modulo $7$. Two auxiliary-prime constructions show that every eligible integer is represented by $f$ or by $h=x^2+y^2+7z^2$ (\cref{prop:det7-local}). To pass from $h$ back to $f$, we use explicit integral matrices $B_p$, for a finite set of primes $p\ne7$, satisfying \[ f(B_pv)=p^2h(v). \] Division by $p^2$ preserves eligibility. Consequently an eligible positive difference divisible by $p^2$ is represented by $f$: if its quotient is represented by $f$, scale the vector by $p$; if it is represented by $h$, apply $B_p$. The square $p^2$ must divide the difference, not $F_n$: it is created by the choice of $k$, so the argument applies equally when $F_n$ is squarefree. The form $f$ represents every Fibonacci number through $F_{47}$ except its truant $21$, which the extension represents by hypothesis. For the later terms, we treat the possible values of $q$. The form $f\perp\la7\ra$ is universal by a short argument using the transfer maps for $p=2,3$. For the other values of $q$, small subtractions give eligible differences outside $7,10\pmod{12}$, which are represented directly by $f$. A finite periodic \emph{congruence cover} supplies square factors for the remaining residue pairs. The Chinese remainder theorem bounds the subtraction, and growth reduces the argument to a short finite check. \subsection*{Context} For a prescribed set $S\subseteq\Z_{>0}$, Kim, Lee, and Oh \cite[Theorem~2.2]{KLO} identify the minimal criterion set with the values that occur as the least element of $S$ omitted by an integral lattice; their Remark~2.3 credits an earlier unpublished result of Bhargava. Kala, Kr\'asensk\'y, and Romeo \cite[Theorem~3.3]{KKR} develop the corresponding theory over totally real number fields. Our minimality argument follows their extension principle \cite[Proposition~3.1]{KKR}, using Kim--Lee--Oh's four-square construction \cite[Proposition~2.1]{KLO} for the explicit Fibonacci escalators. The contributions here are the identification of the criterion and the proof that every quaternary extension arising in the escalation is Fibonacci-universal: by local arguments for the eight regular ternary escalators and, for the irregular escalator $f$, by square transfers and a finite congruence cover, without analytic estimates for representations by the irregular ternary. Related explicit criteria include the $290$-theorem for integer-valued quadratic forms \cite{BhargavaHanke} and Rouse's $451$-theorem for forms representing all odd positive integers \cite{Rouse}. Ju, Kim, Kim, Kim, and Oh prove a $67$-theorem for diagonal forms representing all primes \cite[Theorem~1.1]{Prime67}. Studies of individual Fibonacci numbers represented by binary quadratic forms include \cite{BLM,BallotLuca}. The irregular form $f$ belongs to Kaplansky's first nontrivial ternary genus \cite{Kaplansky,Kelley}. Analytic treatments of this genus \cite{Reinke,Chandee} use modular forms and bounds for $L$-functions, following the approach of Ono--Soundararajan \cite{OnoSound}. For example, under GRH for the relevant $L$-functions, Chandee \cite[\S4]{Chandee} proves that both genus classes represent every locally represented squarefree integer $N\ge2\cdot10^8$. For the Fibonacci extensions, our square transfers and congruence cover supply the needed differences unconditionally. The representation input is the elementary statement in \cref{prop:det7-local}; we do not need to classify all integers omitted by $f$. \subsection*{Organization} The paper follows the reductions outlined above. \Cref{sec:fib} collects the Fibonacci arithmetic, \cref{sec:tree} determines the ternary escalators, and \cref{sec:quat} constructs and bounds orthogonal sublattices of their extensions. \Cref{sec:regular-closure,sec:irregular} prove that extensions representing the corresponding truant are Fibonacci-universal. In \cref{sec:criterion}, an elementary four-square construction shows that none of the ten truants can be omitted from any Fibonacci criterion set. \Cref{sec:conclusion} states the general transfer principle and discusses its application to other sequences. After the main text, we briefly describe the Lean formalization and some history of our argument. \subsection*{Notation and conventions} By a \emph{quadratic form} (or just \emph{form}) we mean an expression $Q(x)=x^{\mathsf T}Gx$ with $G$ integral, symmetric, and positive definite. Thus all cross-terms have even coefficients. A lattice is a free abelian group of finite rank carrying such a form. The \emph{norm} of a vector $x$ is $Q(x)$, and the determinant of a lattice is the determinant of a Gram matrix. For a lattice $L$, write $Q_L$ for its quadratic form and $\beta_L$ for its associated bilinear pairing; in a basis with Gram matrix $G$, these are $Q_L(x)=x^{\mathsf T}Gx$ and $\beta_L(x,y)=x^{\mathsf T}Gy$. We identify forms with their based lattices, and say that a form \emph{represents} $N$ when $Q(x)=N$ for an integral vector $x$. A form is \emph{universal} if it represents every positive integer. The notation $\langle a_1,\ldots,a_r\rangle$ denotes the diagonal lattice $a_1x_1^2+\cdots+a_rx_r^2$, and $L\perp K$ denotes an orthogonal direct sum. Two lattices are in the same \emph{genus} if they are isometric over $\mathbb R$ and over every $\Z_p$. Write $L_p=L\otimes\Z_p$. A positive integer is \emph{locally represented} by $L$ if every $L_p$ represents it. A form is \emph{regular} if it represents every locally represented positive integer, and \emph{irregular} otherwise. For a prime $p$ and a positive integer $N$, let $v_p(N)$ denote its $p$-adic valuation and $u_p(N)=N/p^{v_p(N)}$ its \emph{$p$-adic unit part}, or prime-to-$p$ part. For $p=2$, we also call this the \emph{odd part}. We use the same valuation on $\Q_p$, with $v_p(0)=+\infty$. For positive odd $m$, $(a/m)$ denotes the Jacobi symbol, including the convention $(a/1)=1$; when $m$ is prime, this is the Legendre symbol. We write $T$ for a ternary escalator and $M$ for a quaternary extension. Finally, $E(L)\subseteq\Z$ denotes the integers not represented by $L$; it includes all negative integers and excludes $0$. This convention lets us say that a difference lies outside $E(L)$ without separately requiring nonnegativity. The \emph{Fibonacci exceptions} of $L$ are $\mathcal F\cap E(L)$. \section{Fibonacci arithmetic preliminaries}\label{sec:fib} We use the classical valuation formulas of Lengyel \cite[Lemmas~1--2 and the theorem in \S3]{Lengyel} and the modular periodicity studied by Wall \cite{Wall}. For completeness, we recall the formulas and their specializations here, together with the short Fibonacci recurrence calculations needed in the proof. The representation criteria in \cref{sec:tree} depend on two pieces of information about an integer $N$: the valuation $v_p(N)$ at one prime, and the residue of its unit part $u_p(N)$. We begin with a growth estimate, which turns a bound at one index into a bound at every later index, and then record the Fibonacci identities that determine these two quantities. \begin{lemma}[Monotonicity of $F_n/n$] \label{lem:fib-ratio-monotonicity} The sequence $F_n/n$ is strictly increasing for $n\ge2$. \end{lemma} \begin{proof} The inequality $nF_{n+1}>(n+1)F_n$ is equivalent to $nF_{n-1}>F_n$. It holds directly for $n=2$; for $n\ge3$, use $F_n=F_{n-1}+F_{n-2}\le2F_{n-1}=Stealth, lattice/.style={fill=white,inner sep=3pt,font=\small}, edge label/.style={fill=white,inner sep=1.5pt,font=\small}] \node[font=\small] at (0,1) {Rank $0$}; \node[font=\small] at (1.8,1) {Rank $1$}; \node[font=\small] at (4,1) {Rank $2$}; \node[font=\small] at (7.2,1) {Rank $3$}; \node[font=\small,align=center] at (11,1) {Fibonacci truant\\of the ternary}; \node[lattice] (zero) at (0,-3.2) {$0$}; \node[lattice] (one) at (1.8,-3.2) {$\la1\ra$}; \node[lattice] (a) at (4,-.45) {$\la1,1\ra$}; \node[lattice] (b) at (4,-4.6) {$\la1,2\ra$}; \node[font=\scriptsize,anchor=south] at (a.north) {truant $3$}; \node[font=\scriptsize,anchor=north east] at (b.south west) {truant $5$}; \draw[->] (zero) -- node[edge label,above] {$1$} (one); \draw[->] (one) -- node[edge label,pos=.65] {$2$} (a); \draw[->] (one) -- node[edge label,pos=.65] {$2$} (b); \node[lattice] (t0) at (7.2,-0.0) {$\la1,1,3\ra$}; \draw[->] (a) -- (t0.west); \node[font=\small,anchor=west] at (9,-0.0) {$F_{16}=987$}; \node[lattice] (t1) at (7.2,-0.9) {$\la1,1,1\ra$}; \draw[->] (a) -- (t1.west); \draw[->] (b) -- (t1.west); \node[font=\small,anchor=west] at (9,-0.9) {$F_{10}=55$}; \node[lattice] (t2) at (7.2,-1.8) {$\la1,1,2\ra$}; \draw[->] (a) -- (t2.west); \draw[->] (b) -- (t2.west); \node[font=\small,anchor=west] at (9,-1.8) {$F_{42}=267914296$}; \node[lattice] (t3) at (7.2,-2.7) {$\la1,2,2\ra$}; \draw[->] (b) -- (t3.west); \node[font=\small,anchor=west] at (9,-2.7) {$F_{10}=55$}; \node[lattice] (t4) at (7.2,-3.6) {$\la1,2,3\ra$}; \draw[->] (b) -- (t4.west); \node[font=\small,anchor=west] at (9,-3.6) {$F_{30}=832040$}; \node[lattice] (t5) at (7.2,-4.5) {$\la1,2,4\ra$}; \draw[->] (b) -- (t5.west); \node[font=\small,anchor=west] at (9,-4.5) {$F_{42}=267914296$}; \node[lattice] (t6) at (7.2,-5.4) {$\la1,2,5\ra$}; \draw[->] (b) -- (t6.west); \node[font=\small,anchor=west] at (9,-5.4) {$F_{15}=610$}; \node[lattice] (t7) at (7.2,-6.3) {$f$}; \draw[->] (b) -- (t7.west); \node[font=\small,anchor=west] at (9,-6.3) {$F_8=21$}; \node[lattice] (t8) at (7.2,-7.2) {$g$}; \draw[->] (b) -- (t8.west); \node[font=\small,anchor=west] at (9,-7.2) {$F_{10}=55$}; \end{tikzpicture} \caption{Fibonacci escalation through rank $3$, with one vertex for each integral isometry class. Each arrow adjoins a vector whose norm is the truant of its source: $1$, $2$, $3$, or $5$. These are also ordinary truants, so the same diagram describes ordinary escalation through rank $3$. Both $\la1,1,1\ra$ and $\la1,1,2\ra$ arise from each binary lattice; $f$ and $g$ are defined in \cref{prop:ternary-list}. The rightmost column records the Fibonacci truants proven in \cref{prop:regular-table,prop:first-fibonacci-exceptions}; these determine the subsequent quaternary escalations, which are not drawn.} \label{fig:escalation-tree} \end{figure} \subsection{The nine ternary escalators} Recall that escalation adjoins a vector of truant norm. Formally, if $L$ has Fibonacci truant $\tau$, an escalation is a positive-definite integral lattice $M\supseteq L$ with $M=L+\Z u$ for some vector $u$ of norm $\tau$. A Fibonacci-universal lattice has no truant and is not escalated. A lattice obtained by successive escalations from the zero lattice is a \emph{Fibonacci escalator}. We classify these lattices up to integral isometry. In computing their Gram matrices, we may replace the new generator $u$ by $u+x$ with $x\in L$ without changing the lattice. The zero lattice has truant $1$ and escalates to $\la1\ra$. Its truant is $2$, and a vector of norm $2$ cannot lie in its rational span because $2$ is not a rational square. A binary escalation has Gram matrix \[ \mat{1&a\\a&2},\qquad a=0,\pm1. \] The case $a=0$ gives $\la1,2\ra$; subtracting the norm-$1$ vector from the new vector when $a=1$, or adding it when $a=-1$, gives $\la1,1\ra$. Checking $1,2,3,5$ gives the binary truants \[ \la1,1\ra:\ 3,\qquad \la1,2\ra:\ 5. \] Neither binary truant is represented by the rational quadratic space of its escalator. Indeed, a rational representation would give $x^2+y^2=3d^2$ or $x^2+2y^2=5d^2$ after clearing denominators. Reduction modulo $3$ or $5$, respectively, forces that prime to divide $x,y$, and then $d$. Dividing all three by the prime gives an infinite descent. Thus adjoining a vector of either truant norm produces a ternary lattice. \begin{proposition}[The nine ternaries] \label{prop:ternary-list} The escalations of the two binary escalators are, up to integral isometry, the seven diagonal lattices \[ \begin{gathered} \la1,1,1\ra,\quad\la1,1,2\ra,\quad\la1,1,3\ra,\\ \la1,2,2\ra,\quad\la1,2,3\ra,\quad\la1,2,4\ra,\quad\la1,2,5\ra, \end{gathered} \] together with $f=x^2+2y^2+2yz+4z^2$ and $g=x^2+2y^2+2yz+5z^2$, whose Gram matrices are \[ G_f=\mat{1&0&0\\0&2&1\\0&1&4},\qquad G_g=\mat{1&0&0\\0&2&1\\0&1&5}. \] \end{proposition} \begin{proof} Since $\la1,1\ra$ is unimodular, subtracting integral multiples of the two old basis vectors makes the new vector orthogonal to them. Its norm becomes $3-r$, where $r$ is a sum of two squares with $0\le r<3$. The possibilities $r=0,1,2$ give $\la1,1,3\ra$, $\la1,1,2\ra$, and $\la1,1,1\ra$. For $\la1,2\ra$, first remove the pairing with the norm-$1$ vector. Subtracting multiples of the norm-$2$ vector reduces the remaining pairing modulo $2$, so we may take $b\in\{0,1\}$. The reduced form is \[ Q(x,y,z)=x^2+2y^2+2byz+mz^2. \] The original vector of norm $5$ still has new coordinate $z=1$. Since $2y^2+2by\ge0$ for integral $y$ and $b\in\{0,1\}$, its representation gives $m\le5$; positive definiteness gives $m\ge1$. If $b=0$, the five values of $m$ give $\la1,1,2\ra$ and the four forms $\la1,2,m\ra$ with $2\le m\le5$. If $b=1$ and $m=1$, the identity \[ x^2+2y^2+2yz+z^2=x^2+y^2+(y+z)^2 \] gives $\la1,1,1\ra$. The cases $m=2$ and $m=3$ do not represent $5$: the values at most $5$ of their binary parts are, respectively, $\{0,2\}$ and $\{0,2,3\}$; subtracting any of these values from $5$ never gives a square. Finally, $m=4$ gives $f$, with $5=f(1,0,1)$, and $m=5$ gives $g$, with $5=g(0,0,1)$. Each of the diagonal possibilities also has a representation of the truant with new coordinate $1$, so all listed lattices do occur as escalations. Their determinants, in the displayed order, are $1,2,3,4,6,8,10,7,9$. They are therefore pairwise inequivalent. \end{proof} \subsection{The regular escalators}\label{sec:regular} Eight ternary escalators are regular: the positive integers they omit are exactly those excluded by a local obstruction. The table groups forms with the same exceptional set. Comparing these sets with \cref{lem:first-exceptional-members} gives their Fibonacci truants; later, the same criteria will determine whether a difference $F_n-qk^2$ is represented. \begin{proposition}[Regular ternaries] \label{prop:regular-table} The eight forms below are regular, with the indicated positive exceptional sets and Fibonacci truants. Here $a,b\ge0$ are integers. \[ \begin{array}{c|c|c} T&E(T)\cap\Z_{>0}&\hbox{Fibonacci truant}\\\hline \la1,1,1\ra,\ \la1,2,2\ra,\ g&4^a(8b+7)&F_{10}=55\\ \la1,1,2\ra,\ \la1,2,4\ra&4^a(16b+14)&F_{42}=267914296\\ \la1,2,3\ra&4^a(16b+10)&F_{30}=832040\\ \la1,1,3\ra&9^a(9b+6)&F_{16}=987\\ \la1,2,5\ra&\substack{5\cdot25^a(5b+r)\\r\in\{2,3\}}&F_{15}=610. \end{array} \] \end{proposition} \begin{proof} Ramanujan \cite[\S3, formulas (3.11)--(3.71)]{Ramanujan} records the exceptional sets of the seven diagonal forms, without giving the ternary proofs. For $\la1,1,3\ra$, $\la1,2,3\ra$, and $\la1,2,5\ra$, Jones and Pall \cite[Table~I, p.~190]{JonesPall} establish sufficiency. Again for completeness, we prove the obstructions and derive the other rows from the Gauss--Legendre three-square theorem. The Gauss--Legendre three-square theorem gives the criterion for $\la1,1,1\ra$. Over $\Z_2$, a sum of three squares is never $7$ modulo $8$, and divisibility by $4$ forces all three coordinates to be even. Hence no integer $4^a(8b+7)$ is a sum of three squares over $\Z_2$, so $\la1,1,1\ra$ is regular. The identity \[ x^2+2y^2+2z^2=x^2+(y+z)^2+(y-z)^2 \] shows that every value of $\la1,2,2\ra$ is a sum of three squares. Conversely, two coordinates in any three-square representation have the same parity; they can therefore be written as $y+z$ and $y-z$. Thus these two forms represent exactly the same integers. The same holds for $g$, since \[ g(x,y,z)=x^2+(y+2z)^2+(y-z)^2. \] Given a sum of three squares, choose two coordinates $r_1,r_2$ that are congruent modulo $3$, changing a sign if necessary. This is always possible: either at least two coordinates are divisible by $3$, or at least two are units. Then \[ y=(r_1+2r_2)/3,\qquad z=(r_1-r_2)/3 \] are integers, and $r_1=y+2z$, $r_2=y-z$ give a representation by $g$. Both displayed embeddings into three squares hold over every $\Z_p$. Hence any positive integer locally represented by $\la1,2,2\ra$ or $g$ is locally represented by three squares and therefore represented integrally by all three forms. This also proves their regularity. For the next row, let $N$ be a positive integer. If $N=x^2+y^2+2z^2$, then $2N=(x+y)^2+(x-y)^2+(2z)^2$. Conversely, if $2N=r_1^2+r_2^2+r_3^2$, then the number of odd coordinates is even; after a permutation, $r_1$ and $r_2$ have the same parity and $r_3$ is even, so \[ N=\left(\frac{r_1+r_2}2\right)^2+\left(\frac{r_1-r_2}2\right)^2 +2\left(\frac{r_3}{2}\right)^2. \] Thus $\la1,1,2\ra$ represents $N$ exactly when $2N$ is a sum of three squares, that is, when $N$ is not of the form $4^a(16b+14)$. Every value of $\la1,2,4\ra$ is a value of $\la1,1,2\ra$, since $x^2+2y^2+4z^2=x^2+(2z)^2+2y^2$. For the converse, first let $N$ be odd. In a representation $N=a^2+b^2+2c^2$, one of $a,b$ is even, which gives a representation by $\la1,2,4\ra$. Now let $N$ be even. A three-square representation of $2N\equiv0\pmod{4}$ has all coordinates even, so by the identity above $\la1,1,2\ra$ represents $N$ exactly when $N/2$ is a sum of three squares. In a representation $N=x^2+2y^2+4z^2$ the coordinate $x$ is even and $N/2=y^2+2(x/2)^2+2z^2$; so $\la1,2,4\ra$ represents $N$ exactly when $\la1,2,2\ra$ represents $N/2$, that is, when $N/2$ is a sum of three squares. Thus $\la1,1,2\ra$ and $\la1,2,4\ra$ represent the same integers. These criteria also prove regularity: a local representation by either form gives a local three-square representation of $2N$ through the integral identities above. The three-square obstruction at $2$ therefore excludes precisely the displayed exceptional set. For $\la1,2,3\ra$, squares modulo $16$ lie in $\{0,1,4,9\}$, so $x^2+2y^2+3z^2\not\equiv10\pmod{16}$. If $N=x^2+2y^2+3z^2$ is divisible by $4$, then $y$ is even and $x\equiv z\pmod{2}$. If $x$ and $z$ are even, all three coordinates are already even. When $x$ and $z$ are odd, replace $z$ by $-z$ if necessary so that $x\equiv z\pmod{4}$; then $X=(x+3z)/2$ and $Z=(x-z)/2$ are even and $X^2+3Z^2=x^2+3z^2$. In either case all three coordinates can be taken even, so $N/4$ is represented. Repeating this, a representation of $4^a(16b+10)$ would give one of $16b+10$, which is impossible modulo $16$. For the odd-prime rows, write the form as $x^2+\alpha y^2+pz^2$, with $(\alpha,p)=(1,3)$ or $(2,5)$. The binary form $x^2+\alpha y^2$ is anisotropic modulo $p$, meaning that its only zero over $\mathbb F_{p}$ is $(0,0)$. Consequently, if a represented integer $N$ is divisible by $p$, then $x=pX$, $y=pY$, and \[ N=p\bigl(pX^2+\alpha pY^2+z^2\bigr). \] At valuation $1$, the unit part of $N$ must therefore be a nonzero square modulo $p$. If $p^2\mid N$, the same identity forces $p\mid z$; dividing all coordinates by $p$ divides the represented value by $p^2$. Repeated division therefore excludes every integer with odd valuation and nonsquare unit part. The nonsquares are $\{2\}$ modulo $3$ and $\{2,3\}$ modulo $5$, giving the last two rows. The classical representation criteria supply sufficiency. The congruence and descent arguments also hold over $\Z_2$, $\Z_3$, or $\Z_5$, respectively, so the excluded integers are locally obstructed. This proves regularity for $\la1,2,3\ra$, $\la1,1,3\ra$, and $\la1,2,5\ra$. The Fibonacci truants now follow from \cref{lem:first-exceptional-members}. \end{proof} \subsection{The determinant-\texorpdfstring{$7$}{7} ternary}\label{sec:det7} For the ninth ternary $f=x^2+2y^2+2yz+4z^2$, local conditions do not characterize representation by $f$ alone. We first characterize representation by at least one of $f$ and $h=\la1,1,7\ra$ using a condition at $7$, then give two changes of variables that convert many $h$-representations into $f$-representations. Together with a few explicit witnesses, these determine the first two Fibonacci exceptions of $f$. To prove Fibonacci-universality of the extensions in \cref{sec:irregular}, we combine this representation input with square transfers. \begin{proposition}[Representation by $f$ or $h$] \label{prop:det7-local} Put $h=\la1,1,7\ra$. Call a positive integer $N$ \emph{eligible}~if \[ v_7(N)\text{ is even} \quad\hbox{or}\quad u_7(N)\equiv1,2,4\pmod{7}. \] Then $N$ is represented by $f$ or by $h$ if and only if $N$ is eligible. \end{proposition} \begin{proof} We first reduce to three isometry classes and distinguish one of them by a residue invariant. Sufficiency will then follow by constructing a positive-definite Gram matrix of determinant $7$ that represents $N$ and has the invariant of $f$ and $h$. \emph{The three classes.} A positive-definite integral ternary lattice of determinant $7$ has a Minkowski-reduced Gram matrix \[ G=\mat{a&r&s\\r&b&t\\s&t&c},\qquad 1\le a\le b\le c,\quad 2|r|,2|s|\le a,\quad 2|t|\le b. \] The classical ternary reduction bound gives $abc\le2\det G=14$; see Mahler \cite[p.~193, (3)]{Mahler}. Hence $a\in\{1,2\}$. If $a=1$, then $r=s=0$ and $bc-t^2=7$. Since $b\le c$ and $|t|\le b/2$, we have $3b^2\le28$, so $b\le3$. The only possibilities are $(b,c,t)=(1,7,0)$ and $(2,4,\pm1)$, giving $h$ and $f$. If $a=2$, then $b=2$ and $c\in\{2,3\}$, with $|r|,|s|,|t|\le1$. The case $c=2$ has even determinant: modulo $2$, a symmetric matrix of odd size with zero diagonal is alternating and singular. For $c=3$, the determinant equation gives \[ r^2=1,\qquad s^2+t^2-rst=1. \] If one of $s,t$ vanishes, changing signs and interchanging the first two basis vectors gives the Gram matrix of a third lattice $K_7$: \[ G_{K_7}=\mat{2&-1&-1\\-1&2&0\\-1&0&3}. \] Otherwise $rst=1$; changing signs makes $r=s=t=1$, and the basis $(e_1,-e_2,e_3-e_1)$, where $e_i$ are the standard basis vectors, again gives $G_{K_7}$. Thus every positive-definite integral ternary lattice of determinant $7$ is isometric to $f$, $h$, or $K_7$. \emph{The residue invariant.} A Gram matrix of determinant $7$ has rank $2$ modulo $7$: rank at most $1$ would force its determinant to be divisible by $49$. Its form over $\mathbb F_7$ therefore has a one-dimensional radical, the subspace pairing to zero with every vector. The induced form on the quotient by this radical is a nonsingular binary form. The determinant of its Gram matrix has a well-defined square class: changing basis multiplies it by the square of the basis-change determinant. Any nonsingular principal $2\times2$ minor lies in this square class: the corresponding coordinate plane meets the radical trivially and maps isomorphically onto the quotient. For $f$, $h$, and $K_7$, the leading principal minors of order $2$ are $2$, $1$, and $3$, respectively. Thus the invariant is a square for $f$ and $h$ and a nonsquare for $K_7$. \emph{Necessity.} Modulo $7$, we have $f(x,y,z)\equiv x^2+2(y+4z)^2$. Since $-2$ is a nonsquare modulo $7$, $7\mid f(x,y,z)$ forces $x=7X$ and $y=-4z+7Y$, giving \[ f(x,y,z)=7\bigl(7X^2+14Y^2-14Yz+4z^2\bigr). \] At valuation $1$ the unit part is congruent to $4z^2$ modulo $7$, a nonzero square. If $49$ divides the value, then $7\mid z$, hence $7\mid x,y,z$, and the value divided by $49$ is again represented. For $h$, the same descent applies: since $-1$ is a nonsquare modulo $7$, $7\mid x^2+y^2+7z^2$ forces $x=7X$, $y=7Y$, and $h(x,y,z)=7(7X^2+7Y^2+z^2)$. Hence every value of $f$ or $h$ is eligible whenever it is positive. \emph{Sufficiency.} Scaling a vector by $7$ multiplies its value by $49$ for both $f$ and $h$. Since division by $49$ preserves eligibility, it suffices to consider an eligible $N$ with $49\nmid N$. We construct the required Gram matrix separately according as $7\nmid N$ or $N=7u$. In each case, we put $N$ in the first diagonal entry, choose a leading binary minor using an auxiliary prime, and solve the determinant equation by a quadratic congruence. We choose the auxiliary prime so that this congruence is solvable and the resulting matrix has the required square class modulo $7$. Suppose first that $7\nmid N$, and write $N=2^em$ with $m$ odd. By the Chinese remainder theorem and Dirichlet's theorem choose a prime $\ell>7N$ with \[ \ell\equiv-1\pmod{8N},\qquad \ell\equiv1\pmod{7}. \] The two moduli are coprime, and the prescribed class is prime to both. Also, $(2/\ell)=1$ because $\ell\equiv7\pmod{8}$, and $(-7/\ell)=(\ell/7)=1$. Since $\ell\equiv3\pmod{4}$ and $\ell\equiv-1\pmod{m}$, Jacobi reciprocity gives $(m/\ell)=(-1/m)(\ell/m)=(-1/m)^2=1$. Hence $(-7N/\ell)=1$; choose $\lambda$ with $\lambda^2\equiv-7N\pmod{\ell}$. Put $a_0=(\ell+1)/N$ and $c_0=(7+a_0\lambda^2)/\ell$. The congruence for $\ell$ makes $a_0$ integral, and $c_0$ is integral because $a_0N\equiv1\pmod{\ell}$ gives $a_0\lambda^2\equiv-7\pmod{\ell}$. The matrix \[ G=\mat{N&1&\lambda\\1&a_0&0\\\lambda&0&c_0} \] has $\det G=c_0(a_0N-1)-a_0\lambda^2=c_0\ell-a_0\lambda^2=7$ and leading minors $N$ and $\ell$. Thus $G$ is positive definite of determinant $7$ and represents $N$. Its leading binary minor is $\ell\equiv1\pmod{7}$, so its residue invariant is a square. Suppose next that $N=7u$ with $u\equiv1,2,4\pmod{7}$, and write $u=2^em$ with $m$ odd. Since $7\nmid u$, Dirichlet's theorem supplies a prime $\ell>7u$ with $\ell\equiv-7\pmod{8u}$. Then $\ell\equiv1\pmod{8}$, so \[ \left(\frac{-u}{\ell}\right)=\left(\frac{m}{\ell}\right) =\left(\frac{\ell}{m}\right)=\left(\frac{-7}{m}\right) =\left(\frac{m}{7}\right)=\left(\frac{u}{7}\right)=1. \] Since $\ell>7$, choose $\eta$ with $49\eta^2\equiv-u\pmod{\ell}$, and put $a_0=(\ell+7)/u$ and $c_0=(1+7a_0\eta^2)/\ell$. Since $a_0u\equiv7\pmod{\ell}$ and $49\eta^2\equiv-u\pmod{\ell}$, we have $7(1+7a_0\eta^2)\equiv7-a_0u\equiv0\pmod{\ell}$. As $\ell\ne7$, this proves that $c_0$ is integral. The matrix \[ G=\mat{7u&7&-7\eta\\7&a_0&0\\-7\eta&0&c_0} \] has $\det G=7(\ell c_0-7a_0\eta^2)=7$ and leading minors $7u$ and $7\ell$. These are positive, so $G$ is positive definite; its first diagonal entry shows that it represents $N$. Modulo $7$ it is $\operatorname{diag}(0,a_0,c_0)$. Since $a_0u\equiv\ell$ and $\ell c_0\equiv1\pmod{7}$, its nonzero principal minor satisfies $a_0c_0\equiv u^{-1}\pmod{7}$, a square. In both cases the invariant excludes $K_7$, so $G$ is isometric to $f$ or to $h$, and $N$ is represented by $f$ or by $h$. \end{proof} The example $7=h(0,0,1)$ shows that eligibility does not imply representation by $f$ alone. Indeed, $2y^2+2yz+4z^2=2\left(y+\frac z2\right)^2+\frac{7z^2}{2}$ takes only the values $0,2,4$ below $8$ at integral $(y,z)$, and $7$, $5$, and $3$ are not squares. Nevertheless, $7$ is locally represented by $f$: for every odd prime $p$, the vector $(0,-2,1/2)\in\Z_p^3$ has value $7$; over $\Z_2$, choose $\theta$ with $\theta^2=-15$, which exists because $-15\equiv1\pmod{8}$, and use $f(\theta,1,2)=7$. Thus $f$ is irregular (see also \cite{Kaplansky,Kelley}). The next lemma converts an $h$-representation into an $f$-representation in most residue classes modulo $12$. Six additional witnesses will then determine the first two Fibonacci exceptions of $f$. \begin{lemma}[From $h$ to $f$ modulo $12$] \label{lem:f-mod-twelve} Let $N\in\Z$. If $N$ is represented by $f$ or $h$ and $N\not\equiv7,10\pmod{12}$, then $N$ is represented by $f$. \end{lemma} \begin{proof} Only an $h$-representation $N=a^2+b^2+7c^2$ needs consideration. The first change of variables below is integral under a parity condition; the second is integral under a condition modulo $3$. Direct calculation gives \begin{align*} f\left(-b,2c,-\frac{a+c}{2}\right)&=a^2+b^2+7c^2,\\ f\left(\frac{-a-b+7c}{3},\frac{-a+2b+c}{3}, \frac{-a-b-2c}{3}\right)&=a^2+b^2+7c^2. \end{align*} If $N\equiv0,1\pmod{4}$, one of $a,b$ has the same parity as $c$: otherwise both have parity opposite to $c$, giving $N\equiv2$ or $3\pmod{4}$. Interchange $a,b$ if necessary and use the first identity. If $N\not\equiv1\pmod{3}$, the number of nonzero coordinates among $a,b,c$ modulo 3 is zero, two, or three. Change their signs so that $-a-b+c\equiv0\pmod{3}$. This is possible in each of those three cases; all numerators in the second identity are then divisible by 3. The only residue classes modulo 12 satisfying neither condition are 7 and 10. \end{proof} The modulo-$12$ sufficient condition in \cref{lem:f-mod-twelve} also appears, in terms of local representability, in Bhargava's proof of the Fifteen Theorem \cite[\S4, p.~30]{Bhargava15}. The two identities in our proof are the maps $B_2/2$ and $B_3/3$ from our \cref{tab:seven-square-transfers} in \cref{app:seven-transfers}. \begin{proposition}[First Fibonacci exceptions] \label{prop:first-fibonacci-exceptions} The Fibonacci truant of $f$ is $F_8=21$, and its next Fibonacci exception is $F_{48}=4807526976$. \end{proposition} \begin{proof} The representations \[ \begin{array}{c|cccccc} N&1&2&3&5&8&13\\\hline (x,y,z)&(1,0,0)&(0,1,0)&(1,1,0)&(1,0,1)&(0,2,0)&(3,0,1) \end{array} \] cover $F_1,\ldots,F_7$, while $21=7\cdot3$ is locally obstructed. For $9\le n\le47$, the Fibonacci recurrence modulo $7$ shows that the only multiples of $7$ occur at $n=16,24,32,40$. Their residues modulo $49$ are $7,14,14,7$, respectively, so every term in the interval is eligible. Modulo $12$, the only terms congruent to $7$ or $10$ occur at $n=9,10,15,33,34,39$. Thus \cref{prop:det7-local,lem:f-mod-twelve} show that $f$ represents $F_n$ at all other indices in the interval. The six remaining representations are \[ \begin{array}{c|l} n&(x,y,z)\\\hline 9&(4,3,0)\\ 10&(3,3,2)\\ 15&(12,7,8)\\ 33&(12,1051,368)\\ 34&(9,1473,322)\\ 39&(12,5289,568) \end{array} \] and are verified by substitution into $f$. Finally, $F_{48}\equiv21\pmod{49}$, so it has valuation $1$ at $7$ and nonsquare unit part $3\pmod{7}$; \cref{prop:det7-local} excludes it. \end{proof} The truants encountered through rank $3$ are exactly the elements of $C$. \Cref{tab:criterion-truants} collects one escalator for each value. These same escalators will provide the omission examples in the minimality proof. \begin{table}[htbp] \setlength{\belowcaptionskip}{8pt} \centering \caption{The criterion values and escalators having them as truants. The last two columns give an independent congruence check: the values of $P_t$ modulo $m_t$ omit $t\bmod m_t$.} \label{tab:criterion-truants} \begin{tabular}{r l r r} \hline Truant $t$ & Escalator $P_t$ & $m_t$ & $t\bmod m_t$ \\ \hline $1$ & zero lattice & $2$ & $1$ \\ $2$ & $\la1\ra$ & $4$ & $2$ \\ $3$ & $\la1,1\ra$ & $4$ & $3$ \\ $5$ & $\la1,2\ra$ & $8$ & $5$ \\ $21$ & $f$ & $49$ & $21$ \\ $55$ & $\la1,1,1\ra$ & $8$ & $7$ \\ $610$ & $\la1,2,5\ra$ & $25$ & $10$ \\ $987$ & $\la1,1,3\ra$ & $9$ & $6$ \\ $832040$ & $\la1,2,3\ra$ & $64$ & $40$ \\ $267914296$ & $\la1,1,2\ra$ & $64$ & $56$ \\ \hline \end{tabular} \end{table} \subsection{Each truant raises the rank} For the unary and binary escalators we already checked that adjoining a vector of truant norm raises the rank. The local criteria give the same conclusion for all nine ternaries. This ensures that an escalation inside an ambient lattice reaches rank $4$, rather than merely enlarging a sublattice of the same rational space. \begin{lemma}[No same-rank escalation] \label{lem:no-rational-truant} Let $T$ be a Fibonacci escalator of rank at most $3$, with truant $\tau_T$, and let $L$ be an integral lattice containing $T$. Then $\tau_T$ is not represented by $T\otimes\Q$. In particular, if $u\in L$ has norm $\tau_T$, then $u\notin T\otimes\Q$, so $T+\Z u$ has rank one larger than $T$. \end{lemma} \begin{proof} The zero, unary, and binary cases were established above. For a ternary escalator, its truant lies in the local obstruction described in \cref{prop:regular-table,prop:det7-local}. Each obstruction is unchanged by multiplication by a nonzero integer square: its valuation changes by an even integer, and its unit part changes by a square. At $2$, an odd square is $1\pmod{8}$; at the odd primes occurring in the obstructions, square multiplication preserves whether a unit is a square or nonsquare. Thus every nonzero integer-square multiple of the truant is still locally obstructed. Clearing denominators in a rational representation would produce an integral representation of one of these multiples, a contradiction. \end{proof} \section{Extensions of the ternary escalators}\label{sec:quat} To prove sufficiency, it remains to show that every positive-definite integral quaternary lattice containing one of the nine ternary escalators and representing its Fibonacci truant is Fibonacci-universal. \Cref{sec:regular-closure,sec:irregular} prove this for the regular and irregular ternaries, respectively. This section supplies the common reduction to orthogonal sublattices and bounds the norm of the adjoined orthogonal vector. Let $M$ be such a lattice, containing the ternary escalator $T$ and a vector $w$ of truant norm. By \cref{lem:no-rational-truant}, $T+\Z w$ has rank $4$, and $M$ represents every integer that this sublattice represents. It is therefore enough to treat lattices of the form $T+\Z v$; no primitivity assumption on $T$ is needed. The generator $v$ need not be perpendicular to $T$. We construct an orthogonal sublattice $T\perp\la q\ra$ of $T+\Z v$ and bound $q$; representing $F_n-qk^2$ by $T$ then gives a representation of $F_n$ by the extension. \subsection{Extensions and their orthogonal sublattices} Let $T$ be a ternary escalator with basis $b_1,b_2,b_3$, Gram matrix $G_T$, and Fibonacci truant $\tau_T$. An \emph{extension} of $T$ is a positive-definite integral lattice of rank $4$ of the form \[ M=T+\Z v,\qquad \operatorname{Gram}(M)= \begin{pmatrix}G_T&c\\c^{\mathsf T}&m\end{pmatrix}, \qquad c_i=\beta_M(v,b_i),\quad m=Q_M(v). \] We must prove Fibonacci-universality for the extensions that represent $\tau_T$. An extension need not satisfy this representation condition unless it is explicitly imposed. Every escalation of $T$ is an extension that represents $\tau_T$. For an arbitrary extension representing $\tau_T$, however, a vector $w$ of that norm need not generate $M$ together with $T$: the sublattice $T+\Z w$ may be proper because the coordinate of $w$ along $v$ need not be $\pm1$. Identify vectors of $T$ with their coordinate columns in this basis. Replacing $v$ by $v+x$ with $x\in T$ changes $c$ to $c+G_Tx$ without changing $M$. We may therefore choose $c$ from a finite set of representatives for $\Z^3/G_T\Z^3$. The chosen generator $v$ need not have norm $\tau_T$, even when $M$ was originally obtained by escalation. The representatives are chosen as follows. If $T$ is diagonal, with $G_T=\operatorname{diag}(1,a_2,a_3)$, then the quotient $\Z^3/G_T\Z^3$ is the product of the coordinate quotients $\Z/a_2\Z$ and $\Z/a_3\Z$. Let $e_i$ denote the standard basis vectors of $\Z^3$. For $f$, the columns of $G_f$ give $[e_1]=0$, $2[e_2]+[e_3]=0$, and $[e_2]+4[e_3]=0$ in $\Z^3/G_f\Z^3$. Thus $[e_2]=-4[e_3]$ and $7[e_3]=0$. Since the quotient has order $\det G_f=7$, it is cyclic of order $7$, generated by $[e_3]$. For $g$, the same computation gives $[e_2]=-5[e_3]$ and $9[e_3]=0$, so the quotient is cyclic of order $9$, generated by $[e_3]$. \Cref{tab:extension-representatives} lists the resulting representatives for the nine escalators. Extend the bilinear pairing to $M\otimes\Q$. The orthogonal projection of $v$ onto $T\otimes\Q$ has coordinate column $G_T^{-1}c$. Hence \[ v_\perp=v-\sum_{i=1}^3(G_T^{-1}c)_i b_i \] is perpendicular to $T$, and its norm is the Schur complement \[ \delta=Q_M(v_\perp)=m-c^{\mathsf T}G_T^{-1}c>0. \] Let $d$ be the least positive integer for which $dG_T^{-1}c\in\Z^3$, that is, the least common denominator of the entries of $G_T^{-1}c$, and put $q=d^2\delta$. Thus $m$ is the norm of the chosen generator, $\delta$ is the norm of its rational perpendicular component, and $q$ is the norm of the integral vector obtained by clearing denominators. It is $q$, rather than the diagonal entry $m$ of $M$, that appears in the orthogonal summand $\la q\ra$. \Cref{tab:extension-representatives} gives $G_T^{-1}c$ and $c^{\mathsf T}G_T^{-1}c$ for each representative. For example, for $T=\la1,2,2\ra$ and $c=(0,1,1)$ it gives $d=2$ and $q=4(m-1)$. \begin{table}[htbp] \setlength{\belowcaptionskip}{8pt} \centering \caption{Representatives $c=(0,c_2,c_3)$ for $\Z^3/G_T\Z^3$ and the quantities used to compute $d$ and $q$.} \label{tab:extension-representatives} \small \setlength{\tabcolsep}{5pt} \renewcommand{\arraystretch}{1.25} \begin{tabular}{c l c c} \hline $T$ & representatives & $G_T^{-1}c$ & $c^{\mathsf T}G_T^{-1}c$\\ \hline $\la1,1,1\ra$ & $c=0$ & $0$ & $0$\\ $\la1,1,2\ra$ & $c_2=0$, $c_3\in\{0,1\}$ & $(0,0,c_3/2)$ & $c_3^2/2$\\ $\la1,1,3\ra$ & $c_2=0$, $c_3\in\{0,1,2\}$ & $(0,0,c_3/3)$ & $c_3^2/3$\\ $\la1,2,2\ra$ & $c_2,c_3\in\{0,1\}$ & $(0,c_2/2,c_3/2)$ & $(c_2^2+c_3^2)/2$\\ $\la1,2,3\ra$ & $c_2\in\{0,1\}$, $c_3\in\{0,1,2\}$ & $(0,c_2/2,c_3/3)$ & $c_2^2/2+c_3^2/3$\\ $\la1,2,4\ra$ & $c_2\in\{0,1\}$, $c_3\in\{0,1,2,3\}$ & $(0,c_2/2,c_3/4)$ & $c_2^2/2+c_3^2/4$\\ $\la1,2,5\ra$ & $c_2\in\{0,1\}$, $c_3\in\{-2,\dots,2\}$ & $(0,c_2/2,c_3/5)$ & $c_2^2/2+c_3^2/5$\\ $f$ & $c_2=0$, $c_3\in\{0,\dots,6\}$ & $(0,-c_3/7,2c_3/7)$ & $2c_3^2/7$\\ $g$ & $c_2=0$, $c_3\in\{0,\dots,8\}$ & $(0,-c_3/9,2c_3/9)$ & $2c_3^2/9$\\ \hline \end{tabular} \end{table} \begin{lemma}[The orthogonal sublattice] \label{lem:orthogonal-sublattice} Let $M=T+\Z v$ be an extension of $T$. \begin{enumerate} \item [\textup{(i)}] $q$ is a positive integer, and $M$ contains $T\perp\la q\ra$ with index $d$. \item [\textup{(ii)}] For every $x\in T$ and every $k\in\Z$, \begin{equation}\label{eq:integral-identity} d^2\,Q_M(x+kv)=Q_T\bigl(dx+k\,dG_T^{-1}c\bigr)+qk^2. \end{equation} \item [\textup{(iii)}] For every integer $N$, if there is an integer $k\ge0$ such that $N-qk^2\notin E(T)$, then $M$ represents $N$. \end{enumerate} \end{lemma} \begin{proof} Multiplying $v_\perp$ by $d$ gives the integral vector \[ w_\perp=dv_\perp=dv-\sum_{i=1}^3(dG_T^{-1}c)_i b_i\in M. \] This vector is orthogonal to $T$ and has norm $d^2\delta=q$. Since $M$ has integral Gram matrix, $q\in\Z_{>0}$. Moreover, $T+\Z w_\perp$ has index $d$ in $T+\Z v$, as is seen from the coefficient of $v$. This proves \textup{(i)}. For \textup{(ii)}, write \[ d(x+kv)=\bigl(dx+k\,dG_T^{-1}c\bigr)+kw_\perp, \] where the first summand lies in $T$ and the second is orthogonal to $T$, and take norms. For \textup{(iii)}, if $Q_T(x)=N-qk^2$, then $x+kw_\perp$ represents $N$ in $M$. \end{proof} The condition in part~\textup{(iii)} is sufficient but not necessary: the sublattice $T\perp\Z w_\perp$ has index $d$ in $M$, and vectors of $M$ outside it can represent integers that the sublattice omits. We use such vectors in \cref{prop:large-v2-extensions,prop:three-adic-closure,prop:five-adic-closure}. In the other direction, part~\textup{(ii)} shows that $T\perp\la q\ra$ represents $d^2N$ whenever $M$ represents $N$. Applied to the truant, this bounds $q$. \begin{lemma}[Extensions representing the truant] \label{lem:truant-equation} Let $M$ be an extension of $T$. Then $d$ divides $\det G_T$. If $M$ represents $\tau_T$, then there are a vector $y\in T$ and an integer $k\ge1$ such that \begin{equation}\label{eq:truant-equation} d^2\tau_T=Q_T(y)+qk^2. \end{equation} In that case \begin{equation}\label{eq:schur-truant} \delta\le\tau_T \end{equation} and \begin{equation}\label{eq:q-global-bound} q\le\tau_T(\det G_T)^2. \end{equation} \end{lemma} \begin{proof} The matrix $(\det G_T)G_T^{-1}$ is the adjugate of $G_T$ and is integral, so $(\det G_T)G_T^{-1}c\in\Z^3$ and $d\mid\det G_T$. Suppose that $Q_M(x+kv)=\tau_T$ with $x\in T$ and $k\in\Z$. Then $k\ne0$, since $T$ omits $\tau_T$, and after replacing the vector by its negative we may assume $k\ge1$. Now \eqref{eq:integral-identity} gives \eqref{eq:truant-equation} with $y=dx+k\,dG_T^{-1}c$. Since $Q_T(y)\ge0$ and $k\ge1$, we obtain $q\le d^2\tau_T$, which is \eqref{eq:schur-truant}; and \eqref{eq:q-global-bound} follows because $d\le\det G_T$. \end{proof} For an extension representing $\tau_T$ and a fixed representative $c$, \eqref{eq:schur-truant} gives $m\le\lfloor\tau_T+c^{\mathsf T}G_T^{-1}c\rfloor$. Over all representatives, this gives $m\le56$ for $\la1,2,2\ra$, $m\le988$ for $\la1,1,3\ra$, $m\le611$ for $\la1,2,5\ra$, and $m\le31$ for $f$. \subsection{Values of \texorpdfstring{$q$}{q} for \texorpdfstring{$\la1,1,3\ra$}{<1,1,3>}, \texorpdfstring{$\la1,2,5\ra$}{<1,2,5>}, and \texorpdfstring{$f$}{f}} The subtraction arguments also require divisibility information about $q$. For extensions of $\la1,1,3\ra$ and $\la1,2,5\ra$ representing the truant, we prove $v_3(q)\le1$ and $v_5(q)\le1$, respectively. For $f$, we determine a finite set containing every possible $q$; \cref{sec:irregular} treats this set. \begin{lemma}[Valuation bound] \label{lem:valuation-bound} Let $T$ be $\la1,1,3\ra$ or $\la1,2,5\ra$, and let $p$ be $3$ or $5$, respectively. Every extension of $T$ that represents $\tau_T$ satisfies $v_p(q)\le1$. \end{lemma} \begin{proof} Use the representatives for $c$ in \cref{tab:extension-representatives}. First suppose $c_3\ne0$. For $\la1,1,3\ra$ we have $d=3$ and \[ q=9m-3c_3^2, \] so $v_3(q)=1$. For $\la1,2,5\ra$, we have $d\in\{5,10\}$ and \[ q=d^2m-\frac{d^2c_2^2}{2}-\frac{d^2c_3^2}{5}. \] The first two terms are divisible by $25$ (when $d=5$, we have $c_2=0$), and the last has valuation $1$ at $5$, so $v_5(q)=1$. Now suppose $c_3=0$, so that $p\nmid d$, and suppose that $p^2\mid q$. By \cref{lem:truant-equation} there are $y\in T$ and $k\ge1$ with \[ Q_T(y)=d^2\tau_T-qk^2\equiv d^2\tau_T\pmod{p^2}. \] The truant has valuation $1$ at $p$ and nonsquare unit part modulo $p$: \[ 987=3\cdot329,\quad 329\equiv2\pmod{3};\qquad 610=5\cdot122,\quad 122\equiv2\pmod{5}. \] Since $p\nmid d$, the integer $Q_T(y)$ therefore has valuation $1$ at $p$, and its unit part is $d^2u_p(\tau_T)$ modulo $p$, a nonsquare. By \cref{prop:regular-table}, such an integer is not represented by $T$, a contradiction. Hence $v_p(q)\le1$. \end{proof} \begin{lemma}[Possible values of $q$ for $f$] \label{lem:q-values-for-f} Every quaternary extension of $f$ representing $21$ contains $f\perp\la q\ra$ with $q$ in the set \begin{equation}\label{eq:q-set-for-f} \begin{split} \mathcal Q_7={}&\{q\in\Z:1\le q\le21,\ 7\nmid q\}\\&\cup\{7\}\\ &{}\cup\{7s:s\in\Z,\ 1\le s\le147,\ s\equiv3,5,6\pmod{7}\}. \end{split} \end{equation} The set $\mathcal Q_7$ has $82$ elements, and its largest element is $1022$. \end{lemma} \begin{proof} By \cref{tab:extension-representatives}, $c=(0,0,c_3)$ with $0\le c_3\le6$. If $c_3\ne0$, then $d=7$ and $q=49m-14c_3^2=7s$ with $s=7m-2c_3^2$. The bound \eqref{eq:q-global-bound} is $q\le21\cdot7^2=1029$, so $s\le147$, and $s\equiv-2c_3^2\equiv3,5,6\pmod{7}$. If $c_3=0$, then the extension is $f\perp\la m\ra$, and $q=m\le21$ by \eqref{eq:schur-truant}. Among the multiples of $7$ in this range, the values $7$ and $21$ belong to the displayed set. The value $14$ is impossible: a representation of $21$ by $f\perp\la14\ra$ would require $f$ to represent $21$ or $7$. Both values are omitted by $f$, as shown in \cref{sec:det7}. The three sets in \eqref{eq:q-set-for-f} are disjoint and have $18$, $1$, and $63$ elements; the largest element is $7\cdot146=1022$. \end{proof} \section{Extensions of the regular ternaries}\label{sec:regular-closure} Let $M$ be a quaternary extension of one of the eight regular ternaries $T$, and suppose that $M$ represents the truant of $T$. Any Fibonacci number already represented by $T$ is also represented by $M$, so only the Fibonacci exceptions of $T$ require attention. We usually represent such an exception $F_n$ by choosing $k$ so that $F_n-qk^2$ is nonnegative and lies outside the exceptional set in \cref{prop:regular-table}. When the orthogonal sublattice does not suffice, we use vectors of $M$ outside it. We treat the six ternaries with obstructions at $2$ together, and then $\la1,1,3\ra$ and $\la1,2,5\ra$. \subsection{Ternaries with obstructions at \texorpdfstring{$2$}{2}} The six ternaries in the first three rows of \cref{prop:regular-table} have obstructions at $2$. We treat their extensions together. \begin{proposition}[Fibonacci-universality in the $2$-adic cases] \label{prop:two-adic-closure} Let $T$ be one of the six ternaries with obstructions at $2$. Every quaternary extension of $T$ representing $\tau_T$ is Fibonacci-universal. \end{proposition} The proof occupies this subsection. Throughout, $T\perp\la q\ra$ is the orthogonal sublattice supplied by \cref{lem:orthogonal-sublattice}, and the argument divides according to $v_2(q)$. If $v_2(q)\le v_2(\tau_T)+2$, then subtracting a suitable $qk^2$ from a Fibonacci exception larger than $\tau_T$ leaves an integer represented by $T$ (\cref{lem:two-adic-subtraction,lem:two-adic-exception-bounds}); the one pair $(g,F_{22})$ that this leaves open is treated in \cref{lem:g-f22-representation}. If $v_2(q)\ge v_2(\tau_T)+3$, the orthogonal sublattice does not represent the truant. In this case \cref{lem:odd-denominator-obstruction,lem:no-large-v2-one-two-four} and the hypothesis on the truant leave exactly fourteen extensions, all of $\la1,2,2\ra$; \cref{prop:large-v2-extensions} lists them and constructs representations of the odd Fibonacci exceptions of $\la1,2,2\ra$ using vectors outside their orthogonal sublattices. For $\varepsilon\in\{0,1\}$ and odd $r$, put \[ \mathcal E_{\varepsilon,r} =\{N\in\Z_{>0}:v_2(N)\equiv\varepsilon\pmod{2}, \ u_2(N)\equiv r\pmod{8}\}. \] By \cref{prop:regular-table,lem:first-exceptional-members}, the positive integers omitted by each of these six ternaries $T$ form the family $\mathcal E_{\varepsilon,r}$ with \[ \begin{array}{c|c} T& (\varepsilon,r)\\\hline \la1,1,1\ra,\ \la1,2,2\ra,\ g &(0,7)\\ \la1,1,2\ra,\ \la1,2,4\ra &(1,7)\\ \la1,2,3\ra &(1,5). \end{array} \] Subtracting $qk^2$ can leave such a family in either of two ways: it can change the parity of the valuation, or change the odd part modulo $8$. The next lemma gives explicit choices of $k$ and identifies when the subtraction cannot remove the obstruction. \begin{lemma}[$2$-adic subtraction] \label{lem:two-adic-subtraction} Let $N=2^au\in\mathcal E_{\varepsilon,r}$ and $q=2^s\omega\in\Z_{>0}$, where $a,s$ are nonnegative integers and $u,\omega$ are odd integers. \begin{enumerate} \item [\textup{(i)}] If $s\ge a+3$, then for every integer $k$, \[ v_2(N-qk^2)=a,\qquad 2^{-a}(N-qk^2)\equiv r\pmod{8}. \] In particular, every positive difference $N-qk^2$ remains in $\mathcal E_{\varepsilon,r}$. \item [\textup{(ii)}] If $s\le a+2$ and $N\ge2^{\max(4,a)}q$, then there is an integer $k\ge1$ such that \[ 0\le N-qk^2\quad\hbox{and}\quad N-qk^2\notin\mathcal E_{\varepsilon,r}. \] \end{enumerate} \end{lemma} \begin{proof} For \textup{(i)}, $qk^2$ is divisible by $2^{a+3}$, so subtraction preserves the valuation and the odd part modulo $8$. For \textup{(ii)}, put $e=s-a$. All choices below satisfy $k^2\le\max(16,2^a)$, so the size hypothesis gives $N-qk^2\ge0$. The displayed odd factors exclude zero, making the differences positive and their unit parts well defined. When $-2\le e\le2$, the following choices suffice. Write $R=N-qk^2$ in the table. The final column identifies the condition defining $\mathcal E_{\varepsilon,r}$ that fails. \[ \begin{array}{c|c|c|l} e&k&N-qk^2&\hbox{change in the difference}\\\hline 2&1&2^a(u-4\omega)&u_2(R)\equiv r-4\pmod{8}\\ 1&1&2^a(u-2\omega)&u_2(R)\equiv r-2\omega\not\equiv r\pmod{8}\\ 0&2&2^a(u-4\omega)&u_2(R)\equiv r-4\pmod{8}\\ -1&1&2^{a-1}(2u-\omega)&v_2(R)=a-1\not\equiv\varepsilon\pmod{2}\\ -2&4&2^a(u-4\omega)&u_2(R)\equiv r-4\pmod{8}. \end{array} \] Every parenthesized factor is odd, giving the displayed valuations and residues of the odd parts. In the second row, $2\omega\equiv2$ or $6\pmod{8}$. For $e\le-3$, write $j=a-s\ge3$. If $j$ is odd, take $k=1$: \[ N-q=2^s(2^ju-\omega),\qquad v_2(N-q)=s\not\equiv a\pmod{2}. \] If $j$ is even, compare $k=1$ and $k_0=2^{(j-2)/2}$: \[ \begin{array}{c|c|c} k&v_2(N-qk^2)&u_2(N-qk^2)\bmod 8\\\hline 1&s&-\omega\\ k_0&a-2&4-\omega. \end{array} \] The valuations have the same parity as $a$, but the residues of the odd parts differ by $4$ modulo $8$, so at least one is not $r$. The stated bound on $k^2$ holds for the fixed choices $1,2,4$; for $k_0$, it follows from $k_0^2=2^{a-s-2}\le2^a$, since $s\ge0$. \end{proof} The next lemma supplies the valuation and size bounds needed to apply \cref{lem:two-adic-subtraction}\,\textup{(ii)} to Fibonacci exceptions. We write $\overline q_T$ for the uniform upper bound on $q$ in \eqref{eq:q-global-bound}. \begin{lemma}[Fibonacci exceptions for obstructions at $2$] \label{lem:two-adic-exception-bounds} Let $T$ be one of the six ternaries with obstructions at $2$, put \[ \overline q_T=\tau_T(\det G_T)^2, \] and let $N$ be a Fibonacci exception of $T$. \begin{enumerate} \item [\textup{(i)}] We have $v_2(N)\ge v_2(\tau_T)$. \item [\textup{(ii)}] If $N>\tau_T$, then \[ N\ge2^{\max(4,v_2(N))}\overline q_T, \] except when $(T,N)=(g,F_{22})$. \end{enumerate} \end{lemma} \begin{proof} Write $N=F_n$. For \textup{(i)}, if $(\varepsilon,r)=(0,7)$, the truant $55$ has valuation $0$, so $v_2(N)\ge v_2(55)$. In the other two cases an exception has odd valuation, and the truant has valuation $3$ by \cref{lem:valuations}. Valuation $1$ occurs only at $n\equiv3\pmod{6}$, where the Fibonacci recurrence modulo $16$ gives $F_n\equiv2\pmod{16}$ and hence unit part $1\pmod{8}$, so that $F_n$ is not an exception. For \textup{(ii)}, we first note that, for $n\ge4$, \eqref{eq:fibonacci-prime-parts} gives \[ 2^{\max(4,v_2(F_n))}\le4n. \] Thus an inequality $F_n\ge4n\overline q_T$ at one index proves the desired bound at every later index, by monotonicity of $F_n/n$. For the family $\mathcal E_{0,7}$, the first two exceptions after $F_{10}$ are $F_{22}$ and $F_{34}$, by \cref{lem:valuations,lem:periods}. Indeed, modulo $8$ the period is $12$, and $F_n\equiv7\pmod{8}$ exactly when $n\equiv10\pmod{12}$. Among $1\le n\le34$, the only index with positive even $2$-adic valuation is $n=12$, where $u_2(F_{12})=9\equiv1\pmod{8}$. The bounds $\overline q_T$ for $\la1,1,1\ra$, $\la1,2,2\ra$, and $g$ are $55$, $880$, and $4455$, respectively. We have \[ F_{22}>4\cdot22\cdot55,\qquad F_{34}>4\cdot34\cdot4455. \] The second inequality proves the required bound for all three ternaries from index $34$ onward. At $F_{22}$, the first proves it for $\la1,1,1\ra$, and $F_{22}>16\cdot880$ proves it for $\la1,2,2\ra$, since $v_2(F_{22})=0$. This proves the bound for that family apart from $(g,F_{22})$. For the other two families, exceptions have odd valuation at least $3$, by part~\textup{(i)}. For these three escalators, $\overline q_T\le64F_{42}$, and \[ F_{64}=10610209857723>4\cdot64\cdot(64F_{42}). \] Thus the required bound holds for every $n\ge64$. By \cref{lem:valuations}, the only indices $30\tau_T$, apart from the possible case $(g,F_{22})$. Indeed, $v_2(q)\le v_2(N)+2$ by \cref{lem:two-adic-exception-bounds}\,\textup{(i)}, and $q\le \overline q_T$ by \eqref{eq:q-global-bound}, so \cref{lem:two-adic-exception-bounds}\,\textup{(ii)} gives the size hypothesis of \cref{lem:two-adic-subtraction}\,\textup{(ii)}; \cref{lem:orthogonal-sublattice} then applies to the resulting difference. To prove representation in the case $(g,F_{22})$ and classify the extensions with $v_2(q)\ge v_2(\tau_T)+3$, we first show that such an extension cannot represent the truant when $d$ is odd. \begin{lemma}[The obstruction for odd $d$] \label{lem:odd-denominator-obstruction} Let $T$ be one of the six ternaries with obstructions at $2$. If an extension of $T$ has odd $d$ and $v_2(q)\ge v_2(\tau_T)+3$, then it does not represent $\tau_T$. In particular, an extension with $c=0$ and $v_2(q)\ge v_2(\tau_T)+3$ does not represent $\tau_T$. \end{lemma} \begin{proof} Suppose that it represents $\tau_T$. By \cref{lem:truant-equation} there are $y\in T$ and $k\ge1$ with $Q_T(y)=d^2\tau_T-qk^2$. Since $d$ is odd, $d^2\equiv1\pmod{8}$, so $d^2\tau_T$ has the same valuation as $\tau_T$ and the same odd part modulo $8$; thus $d^2\tau_T\in\mathcal E_{\varepsilon,r}$. As $v_2(q)\ge v_2(d^2\tau_T)+3$, part~\textup{(i)} of \cref{lem:two-adic-subtraction} shows that $d^2\tau_T-qk^2$ has the same valuation and the same odd part modulo $8$. Since it equals $Q_T(y)\ge0$ and has finite valuation, it is positive and thus lies in $\mathcal E_{\varepsilon,r}$. This contradicts its representation by $T$. When $c=0$ we have $d=1$. \end{proof} \begin{lemma}[Representation of $F_{22}$ by extensions of $g$] \label{lem:g-f22-representation} Every quaternary extension of $g$ representing $55$, the truant of $g$, also represents $F_{22}=17711$. \end{lemma} \begin{proof} By \cref{tab:extension-representatives}, $c=(0,0,c_3)$ with $0\le c_3\le8$, and $d$ divides $9$; by \eqref{eq:schur-truant}, $\delta\le55$. If $d\le3$, then $q\le495$. If $d=9$, then $3\nmid c_3$ and \[ q=81m-18c_3^2. \] Thus $9\mid q$ when $d=9$. In every case, $q=d^2\delta\le81\cdot55=4455$. Since $d$ is odd, \cref{lem:odd-denominator-obstruction} gives $v_2(q)\le2$. Put $N=17711\equiv7\pmod{8}$. If $q$ is even, its valuation is $1$ or $2$, and $N-q>0$ is odd with residue different from $7$ modulo $8$. If $q$ is odd and $q\le N/4$, then $N-4q>0$ has residue $3$ modulo~$8$. Each difference is represented by $g$. The only remaining case is odd $q>N/4$. It requires $d=9$, and the only odd multiples of $9$ in $(17711/4,4455]$ are $4437$ and $4455$. The corresponding differences $N-q$ are \[ 17711-4437=2\cdot6637,\qquad 17711-4455=2^3\cdot1657. \] Both have odd $2$-adic valuation and are represented by $g$. Apply \cref{lem:orthogonal-sublattice} in each case. \end{proof} It remains to classify the extensions with $v_2(q)\ge v_2(\tau_T)+3$. Such an extension can require vectors outside the orthogonal sublattice. For example, the extension of $T=\la1,2,2\ra$ with $c=(0,1,1)$ and $m=55$ has $q=216$, and \[ F_{22}-216k^2\equiv7\pmod{8} \] for every integer $k$. This extension represents $55$, the truant of $T$, as \cref{prop:large-v2-extensions} will show, but its orthogonal sublattice omits $F_{22}$. For $T=\la1,2,4\ra$, the remaining extensions have even $d$ and require a parity argument. \begin{lemma}[The remaining extensions for $\la1,2,4\ra$] \label{lem:no-large-v2-one-two-four} For $T=\la1,2,4\ra$, no quaternary extension of $T$ representing $\tau_T$ has $v_2(q)\ge v_2(\tau_T)+3$. \end{lemma} \begin{proof} By \cref{tab:extension-representatives}, $c=(0,c_2,c_3)$ with $c_2\in\{0,1\}$ and $c_3\in\{0,1,2,3\}$. For odd $c_3$ we have $d=4$ and $q=16m-8c_2^2-4c_3^2$, so $v_2(q)=2$. For even $c_3$ and $c_2=1$ we have $d=2$ and $q=4m-2-c_3^2$, so $v_2(q)=1$. After the case $c=0$ is excluded by \cref{lem:odd-denominator-obstruction}, the only possibility with $v_2(q)\ge6$ is therefore $c=(0,0,2)$. In this case $q=4(m-1)$, so $m\equiv1\pmod{16}$, and \[ Q(x,y,z,w)=x^2+2y^2+(2z+w)^2+(m-1)w^2. \] The truant satisfies $F_{42}\equiv8\pmod{16}$. If $w$ is odd, then $(2z+w)^2$ is $1$ or $9$ modulo $16$ and $(m-1)w^2\equiv0\pmod{16}$, whereas $x^2+2y^2$ is never $7$ or $15$ modulo $16$. Thus no vector with odd $w$ represents $F_{42}$. If $w=2w'$, write instead \[ Q=x^2+2y^2+4(z+w')^2+4(m-1)w'^2. \] The final term is divisible by $64$. Since $v_2(F_{42})=3$, subtracting it preserves the valuation and the odd part modulo $8$. In a representation of $F_{42}$, the difference would equal $x^2+2y^2+4(z+w')^2\ge0$; its valuation would force it to be positive. It would therefore lie in $\mathcal E_{1,7}$, contradicting the representation criterion for $\la1,2,4\ra$. Neither parity of $w$ permits a representation of $F_{42}$, contrary to the hypothesis on the extension. \end{proof} \begin{proposition}[Extensions with large $v_2(q)$] \label{prop:large-v2-extensions} Among the six ternaries $T$ with obstructions at $2$, only $\la1,2,2\ra$ has quaternary extensions that represent the truant and have $v_2(q)\ge v_2(\tau_T)+3$. With the representatives of \cref{tab:extension-representatives}, the fourteen extensions are given by \[ c=(0,1,1),\qquad m\equiv3\pmod{4},\qquad 3\le m\le55. \] Each of them is Fibonacci-universal. \end{proposition} \begin{proof} We use the representatives of \cref{tab:extension-representatives} throughout, and first show that the other five ternaries have no such extensions. For $\la1,1,1\ra$ and $g$, the integer $d$ is always odd, so \cref{lem:odd-denominator-obstruction} applies. For $\la1,1,2\ra$, the only nonzero representative for $c$ is $c=(0,0,1)$; it gives $q=4m-2$ and $v_2(q)=1$. Extensions with $c=0$ and the stated valuation bound are excluded by \cref{lem:odd-denominator-obstruction}, and \cref{lem:no-large-v2-one-two-four} excludes such extensions of $\la1,2,4\ra$. For $\la1,2,3\ra$, if $c_2=1$ then $d\in\{2,6\}$ and $q=d^2m-d^2/2-d^2c_3^2/3$ has valuation $1$. The remaining nonzero representatives for $c$ are $(0,0,1)$ and $(0,0,2)$, with $d=3$ and respective values \[ q=3(3m-1),\qquad q=3(3m-4). \] Since $d$ is odd for these and for $c=0$, \cref{lem:odd-denominator-obstruction} excludes every extension with $v_2(q)\ge v_2(\tau_T)+3$. Now let $T=\la1,2,2\ra$. A representative $c$ with exactly one of $c_2,c_3$ nonzero gives $q=4m-2$, of valuation $1$; extensions with $c=0$ are already excluded. Thus only $c=(0,1,1)$ remains, with \[ q=4(m-1),\qquad \delta=m-1. \] The bounds $0<\delta\le55$ give $2\le m\le56$, and $v_2(q)\ge3$ is equivalent to $m$ being odd. The quadratic form of the extension is $Q=x^2+2y^2+2z^2+2(y+z)w+mw^2$. If $m\equiv1\pmod{4}$, it omits $55$. For even $w=2r$, completing squares in $y,z$ gives \[ Q=x^2+2(y+r)^2+2(z+r)^2+4(m-1)r^2, \] which cannot be $7\pmod{8}$: the first three terms form a value of $\la1,2,2\ra$, and $4(m-1)r^2\equiv0\pmod{8}$ because $m$ is odd. For odd $w$, use $w^2\equiv1\pmod{8}$ to obtain \[ Q\equiv x^2+m+2y(y+w)+2z(z+w)\pmod{8}. \] Each of the last two terms is $0$ or $4\pmod{8}$; since $m\equiv1$ or $5\pmod{8}$, the sum again cannot be $7\pmod{8}$. For $m\equiv3\pmod{4}$, $3\le m\le55$, a single construction proves both that the extension represents $55$ and that it represents all odd Fibonacci exceptions of $T$. At $w=1$ its value is \[ Q(x,y,z,1)=x^2+(y+z+1)^2+(y-z)^2+m-1. \] If $N\ge55$ and $N\equiv7\pmod{8}$, then $N-(m-1)>0$ is $1$ or $5\pmod{8}$, so it is a sum of three squares. Since it is also $1\pmod{4}$, any such representation has one odd coordinate and two even coordinates. Place an even coordinate last and write \[ N-(m-1)=X^2+Y^2+4Z^2. \] The integers $X,Y$ have opposite parity. Assign $2Z$ to $x$ and solve $y+z+1=X$, $y-z=Y$. This gives the integral representing vector \[ x=2Z,\qquad y=\frac{X+Y-1}{2},\qquad z=\frac{X-Y-1}{2},\qquad w=1. \] Taking $N=55$ proves that all fourteen extensions represent the truant of $T$. These vectors have $w=1$, whereas vectors in the orthogonal sublattice have even $w$; the vectors outside the sublattice supply the missing representations. It remains to represent the even Fibonacci exceptions of $T$. For each of the fourteen extensions, $m-1\equiv2\pmod{4}$, hence $v_2(q)=3$. An exception of $\la1,2,2\ra$ that is even has even valuation, and \cref{lem:valuations} rules out valuation $2$ for a Fibonacci number, so its valuation is at least $4$. It therefore satisfies the valuation hypothesis of \cref{lem:two-adic-subtraction}\,\textup{(ii)}, and \cref{lem:two-adic-exception-bounds}\,\textup{(ii)}, with \eqref{eq:q-global-bound}, gives the size hypothesis. By \cref{lem:two-adic-subtraction}\,\textup{(ii)} and \cref{lem:orthogonal-sublattice}, the extension represents these even exceptions as well. Together with the odd exceptions just represented, these exhaust the Fibonacci exceptions of $\la1,2,2\ra$, so the extension is Fibonacci-universal. \end{proof} \begin{proof}[Proof of \cref{prop:two-adic-closure}] The truant is represented by hypothesis, and every Fibonacci number that is not an exception is represented by the escalator. If $v_2(q)\le v_2(\tau_T)+2$, the paragraph following \cref{lem:two-adic-exception-bounds}, together with \cref{lem:g-f22-representation}, shows that the extension represents every Fibonacci exception larger than the truant. If $v_2(q)\ge v_2(\tau_T)+3$, the extension is one of those in \cref{prop:large-v2-extensions}. \end{proof} \subsection{Tools for obstructions at odd primes} For $T=\la1,1,3\ra$ and $\la1,2,5\ra$, extensions with $c_3\ne0$ are treated by fixing the coordinate $w$ along the new generator: $w=1$ for $\la1,1,3\ra$ and $w=2$ for $\la1,2,5\ra$, where the even value makes the completion of the square in $y$ integral. The extension's form then becomes a constant plus a polynomial $\Phi_{p,a}$ as in the next lemma. Since $\Phi_{p,a}$ represents every nonnegative integer, the extension represents every integer at least that constant. \begin{lemma}[Representation by quadratic polynomials] \label{lem:quadratic-polynomial-representation} Let $(p,\alpha)$ be $(3,1)$ or $(5,2)$, and let $a\in\Z$ with $p\nmid a$. Then \[ \Phi_{p,a}(x,y,z)=x^2+\alpha y^2+pz^2+2az \] represents every nonnegative integer. \end{lemma} \begin{proof} For an integer $r\ge0$, the integer $p^2r+pa^2$ has valuation $1$ at $p$ and square unit part modulo $p$. By \cref{prop:regular-table}, write \[ p^2r+pa^2=X^2+\alpha Y^2+pZ^2. \] In both cases, $X^2+\alpha Y^2\equiv0\pmod{p}$ forces $p\mid X,Y$. Put $X=px$ and $Y=py$ and divide by $p$: \[ pr+a^2=px^2+\alpha py^2+Z^2. \] Thus $Z\equiv\pm a\pmod{p}$. After changing its sign, write $Z=pz+a$. Substitution and division by $p$ give $r=\Phi_{p,a}(x,y,z)$. \end{proof} When $c_3=0$, we instead subtract $qk^2$ for a suitable $k$. The next lemma is used to choose $k$ when $p=5$; we will also use it with $p=7$ in \cref{sec:irregular}. \begin{lemma}[A quadratic congruence over $\mathbb F_p$] \label{lem:finite-field-quadratic-congruence} Let $p\ge5$ be prime and let $u_0,q_0\in\mathbb F_p^\times$. There is an integer $t$, with $|t|\le(p-1)/2$, such that $u_0-q_0t^2$ is a nonzero square modulo $p$. If $u_0$ is a nonsquare, then $t\ne0$. \end{lemma} \begin{proof} Write $\chi$ for the quadratic character of $\mathbb F_p$, extended by $\chi(0)=0$. For $\xi\ne0$, the equation $y^2=t^2-\xi$ is equivalent to $(t-y)(t+y)=\xi$, which has $p-1$ solutions. Counting instead for each $t$ gives $\sum_t(1+\chi(t^2-\xi))=p-1$, hence $\sum_t\chi(t^2-\xi)=-1$. Taking $\xi=u_0/q_0$ shows that the conic $x^2+q_0t^2=u_0$ has \[ p+\sum_{t\in\mathbb F_p}\chi(u_0-q_0t^2) =p-\chi(-q_0)\ge p-1 \] points. At most two have $x=0$. Since $p-1\ge4$, some point therefore has $x\ne0$. Choose the least absolute representative of its $t$-coordinate. If $u_0$ is a nonsquare, the equation rules out $t=0$. \end{proof} \begin{lemma}[Removing an odd-prime obstruction] \label{lem:odd-prime-obstruction-removal} Let $p\in\{3,5\}$, and let $T$ be $\la1,1,3\ra$ or $\la1,2,5\ra$, respectively. Let $a,u,b$ be positive integers, with $a$ odd, $p\nmid ub$, and $u$ a nonsquare modulo $p$. Put $N=p^a u$ and $q=pb$. If $u>4b$, then $T\perp\la q\ra$ represents $N$. \end{lemma} \begin{proof} We choose $t\in\{1,2\}$ to remove the obstruction. Putting $k=p^{(a-1)/2}t$, we have $N-qk^2=p^a(u-bt^2)>0$. For $p=5$, \cref{lem:finite-field-quadratic-congruence} supplies $t$ with $u-bt^2$ a nonzero square modulo $5$ (replace $t$ by its absolute value). For $p=3$, we have $u\equiv2\pmod{3}$. If $b\equiv1\pmod{3}$, take $t=1$. If $b\equiv2\pmod{3}$, both $u-b$ and $u-4b$ are divisible by $3$, but their difference $3b$ is not divisible by $9$; choose $t$ so that $v_3(u-bt^2)=1$. In this last case, $v_3(N-qk^2)=a+1$ is even. In every case $N-qk^2$ lies outside the exceptional set of $T$ in \cref{prop:regular-table}, proving the assertion. \end{proof} \subsection{Extensions of \texorpdfstring{$\la1,1,3\ra$}{<1,1,3>}} The escalator $\la1,1,3\ra$ omits a positive integer precisely when its $3$-adic valuation is odd and its unit part is $2\pmod{3}$. For extensions with $c_3\ne0$, \cref{lem:quadratic-polynomial-representation} gives representations with coordinate $1$ along the new generator. For those with $c_3=0$, which are orthogonal sums $\la1,1,3\ra\perp\la m\ra$, a small subtraction changes the parity of the valuation or the class of the unit part. \begin{proposition}[Fibonacci-universality of extensions of $\la1,1,3\ra$] \label{prop:three-adic-closure} Every quaternary extension of $\la1,1,3\ra$ representing $F_{16}=987$ is Fibonacci-universal. \end{proposition} \begin{proof} By \cref{tab:extension-representatives}, the extension has the form \[ Q=x^2+y^2+3z^2+2c_3zw+mw^2,\qquad c_3\in\{0,1,2\}. \] It represents the truant $F_{16}=987$ of $\la1,1,3\ra$ by assumption. Every later Fibonacci exception has index divisible by $4$, so it is at least $F_{20}=6765$. The bound \eqref{eq:schur-truant} gives $m\le987+c_3^2/3$, hence $m\le988$. If $c_3\ne0$, then \[ Q(x,y,z,1)=m+\Phi_{3,c_3}(x,y,z). \] By \cref{lem:quadratic-polynomial-representation}, the polynomial $Q(x,y,z,1)$ represents every integer at least $m$, and therefore every remaining Fibonacci exception. Suppose $c_3=0$. Then $q=m\le987$ and $v_3(m)\le1$ by \cref{lem:valuation-bound}. If $3\nmid m$, subtract $m$ from each remaining exception; the difference is positive and prime to $3$, so the escalator represents it. Adding the unary coordinate $1$ represents the exception by the extension. It remains to consider $m=3b$, where $3\nmid b$ and $b\le329$. Write a remaining exception as $N=F_n=3^au$, with $a$ odd and $u\equiv2\pmod{3}$. At $N=F_{20}$ we have $u=2255>4\cdot329$. Every other remaining exception has index $n\ge28$, since its index is divisible by $4$ and $F_{24}$ has even $3$-adic valuation. For $n\ge28$, \eqref{eq:fibonacci-prime-parts} and \cref{lem:fib-ratio-monotonicity} give \[ u\ge\frac{F_n}{3n}\ge\frac{F_{28}}{84}>4\cdot329\ge4b. \] Thus $u>4b$ in every case, and by \cref{lem:odd-prime-obstruction-removal} the form $\la1,1,3\ra\perp\la m\ra$ represents each remaining exception. \end{proof} \subsection{Extensions of \texorpdfstring{$\la1,2,5\ra$}{<1,2,5>}} For $\la1,2,5\ra$, the obstruction is an odd $5$-adic valuation with nonsquare unit part. We use \cref{lem:quadratic-polynomial-representation} when $c_3\ne0$. For the remaining extensions, we subtract $qk^2$ to change the valuation or the unit part. Only $F_{20}$ requires more: there we use again the hypothesis that the extension represents the truant. \begin{proposition}[Fibonacci-universality of extensions of $\la1,2,5\ra$] \label{prop:five-adic-closure} Every quaternary extension of $\la1,2,5\ra$ representing $F_{15}=610$ is Fibonacci-universal. \end{proposition} \begin{proof} Let $M$ be an extension of $\la1,2,5\ra$ representing $610$. By \cref{tab:extension-representatives}, its form is \[ Q(x,y,z,w)=x^2+2y^2+5z^2+2c_2yw+2c_3zw+mw^2, \] where $c_2\in\{0,1\}$ and $c_3\in\{-2,-1,0,1,2\}$. The extension represents the truant $F_{15}=610$ of $\la1,2,5\ra$, so \eqref{eq:schur-truant} gives $m\le611$. Every Fibonacci exception has index divisible by $5$, so every later one is at least $F_{20}=6765$. Let $N=F_n$ be such an exception. If $c_3\ne0$, set $w=2$. Completing the square in $y$ gives \[ Q(x,y,z,2)=\Phi_{5,2c_3}(x,y+c_2,z)+4m-2c_2^2. \] Here $5\nmid2c_3$, so \cref{lem:quadratic-polynomial-representation} shows that $\Phi_{5,2c_3}$ represents $N-(4m-2c_2^2)>0$, since $4m-2c_2^2\le2444<6765$. Thus $M$ represents $N$. Suppose now that $c_3=0$. The bound $\delta\le610$ gives $m\le610$, and the norm $q$ of the orthogonal vector in \cref{lem:orthogonal-sublattice} is \[ q=\begin{cases} m,&c_2=0,\\ 4m-2,&c_2=1. \end{cases} \] In particular, $04b$, \cref{lem:odd-prime-obstruction-removal} shows that $\la1,2,5\ra\perp\la q\ra\subseteq M$ represents $N$. For $N>F_{20}$, its index is at least $25$, and \eqref{eq:fibonacci-prime-parts} and \cref{lem:fib-ratio-monotonicity} give \[ u\ge\frac{F_n}{n}\ge\frac{F_{25}}{25}>4\cdot488>4b. \] For $N=F_{20}$ we have $a=1$ and $u=1353$. If $b\le338$, then $u>4b$, so \cref{lem:odd-prime-obstruction-removal} again proves representation. It remains to treat $N=F_{20}=6765$ with $338610$ rules out $|w|\ge2$. Consequently the escalator represents \[ 2440-q=5(488-b). \] This excludes $b\equiv1\pmod{5}$, since the displayed value would then have valuation $1$ and nonsquare unit part $2\pmod{5}$. Together with $5\nmid b$, this leaves $b\equiv2,3,4\pmod{5}$. We claim that $\la1,2,5\ra$ represents $N-q$, so that \cref{lem:orthogonal-sublattice} applies with $k=1$. The difference is $R=6765-5b=5(1353-b)>0$. If $b\equiv2$ or $4\pmod{5}$, its unit part is a nonzero square modulo $5$. If $b\equiv3\pmod{5}$ but $b\not\equiv3\pmod{25}$, then $v_5(R)=2$. Finally, if $b\equiv3\pmod{25}$, the condition $b\equiv2\pmod{4}$ gives $b\equiv78\pmod{100}$. The range $3380$ with $r$ eligible, we represent $r$ by $f$ or $h$. Scaling in the first case, or a square transfer in the second, gives a representation of $F_n-qk^2$ by $f$. \subsection{The universal form \texorpdfstring{$f\perp\la7\ra$}{f plus 7w squared}} The case $q=7$ requires separate treatment. For a positive integer $N$ divisible by $49$, if $7\nmid k$, then $N-7k^2$ has valuation $1$ and nonsquare unit part $-k^2\pmod{7}$; if $7\mid k$, the difference remains divisible by $49$. Thus the construction used for the other values of $q$, which produces eligible differences of valuation $0$ or $1$, does not apply. Instead we use induction and scaling by $7$. \begin{proposition}[Universality of $f\perp\la7\ra$] \label{prop:f-seven-universal} The form $Q(x,y,z,w)=f(x,y,z)+7w^2$ is universal. \end{proposition} \begin{proof} Use strong induction on the positive integer $N$. If $49\mid N$, the induction hypothesis gives a representation of $N/49$ by $Q$; multiplying every coordinate by $7$ gives a representation of $N$. Hence suppose $49\nmid N$. If $7\nmid N$, take $w=0$ when $N\not\equiv7,10\pmod{12}$ and $w=1$ otherwise. The difference $R=N-7w^2$ is positive and prime to 7, and $R\not\equiv7,10\pmod{12}$. Indeed, in the second case its residue modulo $12$ is $0$ or $3$, and it is positive because the least $N$ prime to $7$ in the classes $7$ and $10$ modulo $12$ are $19$ and $10$, respectively. By \cref{prop:det7-local,lem:f-mod-twelve}, $f$ represents $R$, so $Q$ represents $N$. It remains to consider $N=7u$ with $7\nmid u$. We seek $w$ such that $u-w^2$ is a nonzero square modulo $7$ and is not $1$ or $10$ modulo $12$. When $u>w^2$, these conditions make $7(u-w^2)$ eligible and exclude the residues $7$ and $10$ modulo $12$. Choose $w$ from the following table: use the value in the second column unless $u\bmod12$ is one of the residues named in the third. \begin{center} \begin{tabular}{ccl} \hline $u\bmod7$&$w$&Exceptions, by $u\bmod12$\\\hline 1&0&$w=2$ if $u\equiv1,10$\\ 2&0&$w=1$ if $u\equiv1,10$\\ 3&1&$w=3$ if $u\equiv2,11$\\ 4&0&$w=3$ if $u\equiv1$; $w=4$ if $u\equiv10$\\ 5&1&$w=6$ if $u\equiv2$; $w=2$ if $u\equiv11$\\ 6&2&$w=3$ if $u\equiv2,5$\\\hline \end{tabular} \end{center} Each row gives \[ u-w^2\equiv1,2,4\pmod{7}, \qquad u-w^2\not\equiv1,10\pmod{12}. \] Since $w\le6$, we have $u-w^2>0$ for $u>36$. Checking the prescribed choices for $1\le u\le36$ with $7\nmid u$ leaves only $u=1,26$ for which $u\le w^2$. For every other $u$, the positive difference \[ R=N-7w^2=7(u-w^2) \] is eligible and is not $7$ or $10$ modulo $12$. Again \cref{prop:det7-local,lem:f-mod-twelve} show that $f$ represents $R$, and adjoining the coordinate $w$ gives a representation of $N$ by $Q$. Finally, the two remaining values $N=7$ and $N=182$ have explicit representations: \[ Q(0,0,0,1)=7,\qquad Q(7,3,-6,1)=182.\qedhere \] \end{proof} \paragraph{Remark.} Universality also follows from the Conway--Schneeberger Fifteen Theorem \cite{Conway,Bhargava15}, since $Q$ represents $1,2,3,5,6,7,10,14,15$. We include the short proof for completeness; it uses only \cref{prop:det7-local,lem:f-mod-twelve}. \subsection{Small subtractions} The small-subtraction and square-transfer arguments both choose $k$ in a residue class modulo $7$ for which every positive difference $N-qk^2$ is eligible. \begin{lemma}[A class modulo $7$] \label{lem:eligible-class-mod-seven} Let $q\in\mathcal Q_7\setminus\{7\}$, and let $N$ be a positive integer. There is a residue class modulo $7$ such that, for every integer $k$ in this class, the difference $N-qk^2$ is eligible whenever it is positive. \end{lemma} \begin{proof} We choose the class so that every positive difference $R=N-qk^2$ with $k$ in the class satisfies \[ 7\nmid R\quad\hbox{or}\quad v_7(R)=1\ \hbox{and}\ R/7\equiv1,2,4\pmod{7}; \] such an $R$ is eligible. If $7\nmid q$, avoid the at most two roots of $qk^2\equiv N\pmod{7}$. If $7\mid q$ but $7\nmid N$, then $R\equiv N\not\equiv0\pmod{7}$ for every $k$. Otherwise write $q=7s$ and $N=7u$; here $s\equiv3,5,6\pmod{7}$ by \eqref{eq:q-set-for-f}. For $7\nmid u$, \cref{lem:finite-field-quadratic-congruence} supplies a class with $u-sk^2$ a nonzero square modulo $7$. For $7\mid u$, take $k\equiv1\pmod{7}$; then $u-sk^2\equiv-s\equiv1,2,4\pmod{7}$. \end{proof} \begin{lemma}[Small subtraction] \label{lem:small-subtraction} Let $q\in\mathcal Q_7\setminus\{7\}$ and let $N$ be an integer with $N>441q$. Then $f\perp\la q\ra$ represents $N$ unless $(q\bmod12,N\bmod12)$ is one of \begin{equation}\label{eq:remaining-residues} (0,7),\quad(0,10),\quad(3,10),\quad(9,7). \end{equation} \end{lemma} \begin{proof} If $N\not\equiv7,10\pmod{12}$, impose $k\equiv0\pmod{6}$, so that $N-qk^2\equiv N\pmod{12}$. Otherwise impose $k\equiv1\pmod{6}$; then $N-qk^2\equiv N-q\pmod{12}$, which is not $7$ or $10$ except in the four displayed cases. Combine this class with the class modulo $7$ of \cref{lem:eligible-class-mod-seven}. The resulting class modulo $42$ contains an integer $k$ with $|k|\le21$, so $N-qk^2>0$. This difference is eligible and is not $7$ or $10$ modulo $12$; hence $f$ represents it by \cref{prop:det7-local,lem:f-mod-twelve}. \end{proof} Since $441\cdot1022=4507020}$. Suppose that there are $p\in\mathcal P_7$ and $k_0\in\Z$ with $qk_0^2\equiv N\pmod{p}$ and $p\nmid qk_0$. If \[ N>q\left\lfloor\frac{7p^2}{2}\right\rfloor^2, \] then $f\perp\la q\ra$ represents $N$. \end{lemma} \begin{proof} Since $p$ is odd and $p\nmid qk_0$, Hensel's lemma lifts $k_0$ to a solution of $qk^2\equiv N\pmod{p^2}$. Combine its class modulo $p^2$ with the class modulo $7$ of \cref{lem:eligible-class-mod-seven}, and choose $k$ in the resulting class modulo $7p^2$ with $|k|\le\lfloor7p^2/2\rfloor$. Then $R=N-qk^2$ is positive, eligible, and divisible by $p^2$. Since $p\ne7$, division by $p^2$ preserves eligibility, so $R/p^2$ is represented by $f$ or by $h$ (\cref{prop:det7-local}). In the first case, multiplying the representing vector by $p$ represents $R$ by $f$; in the second, applying $B_p$ does so, by \eqref{eq:seven-square-transfer}. With $k$ as the last coordinate, this represents $N$ by $f\perp\la q\ra$. \end{proof} It remains to find, for the pairs in \eqref{eq:remaining-residues} with $N=F_n$, a prime of $\mathcal P_7$ to which \cref{lem:square-transfer-subtraction} applies once its size bound holds. The next lemma gives a \emph{congruence cover}: every relevant pair $(q,n)$ satisfies the required congruence for at least one prime in $\mathcal P_7$. \begin{lemma}[Congruence cover] \label{lem:congruence-cover} Let $q\in\mathcal Q_7\setminus\{7\}$ and let $n\ge0$ be an integer. Suppose that $(q\bmod12,F_n\bmod12)$ is one of the pairs in \eqref{eq:remaining-residues}. Then there is a prime $p\in\mathcal P_7$ with $p\nmid q$ and $F_n\bmod p\in q(\mathbb F_p^\times)^2$; that is, $F_n\equiv qk^2\pmod{p}$ for some $k\not\equiv0\pmod{p}$. \end{lemma} \begin{proof} The Fibonacci recurrence modulo $12$ gives \[ F_n\equiv10\pmod{12}\iff n\equiv9,15\pmod{24},\qquad F_n\equiv7\pmod{12}\iff n\equiv10\pmod{24}. \] Thus the relevant odd indices are multiples of $3$, and the relevant even indices are $10\pmod{24}$. We group the twenty values of $q$ in $f\perp\la q\ra$ that are congruent to $0$, $3$, or $9$ modulo $12$ by their quadratic characters at suitable primes, and use the fact that the quotient of two nonzero residues modulo $p$ is a square precisely when their quadratic characters agree. In the following table, an entry $p:+$ says that each value of $q$ in the row is a nonzero square modulo $p$, and an entry $p:-$ that each is a nonsquare. \begin{center}\small \renewcommand{\arraystretch}{1.12} \begin{tabular}{l l l} \hline Values of $q$ & Parities of $n$ treated & Characters of $q$\\\hline $\{3,\,903\}$ & odd & $5:-;\ 11:+$\\ $\{12,\,168,\,672\}$ & odd and even & $5:-;\ 11:+;\ 31:-$\\ $\{15,\,231,\,483,\,819\}$ & odd & $19:-$\\ $\{21,\,84,\,189,\,336,\,525,\,756\}$ & odd and even & $17:+;\ 19:-$\\ $\{9,\,777\}$ & even & $13:+;\ 83:+$\\ $315$ & odd & $107:+$\\ $609$ & even & $17:-;\ 53:-;\ 109:+$\\ $924$ & odd and even & $19:-;\ 53:-$\\\hline \end{tabular} \end{center} The table includes exactly the elements of $\mathcal Q_7\setminus\{7\}$ congruent to $0,3,9\pmod{12}$. For $q\equiv0\pmod{12}$, both the odd and even index classes above are needed. If $q\equiv3\pmod{12}$, the hypothesis requires $n\equiv9,15\pmod{24}$; if $q\equiv9\pmod{12}$, it requires $n\equiv10\pmod{24}$. Some rows prove the congruence for both parities, although only one is needed for certain values of $q$. The character entries are found by reducing the values of $q$ modulo the indicated primes and comparing with the squares of the nonzero residues. It remains to find, in every index class that the row requires, a prime of the row at which $F_n$ is nonzero and has the same character as the values of $q$ in that row. The periods of the Fibonacci sequence modulo the primes of $\mathcal P_7$ are listed in \cref{tab:seven-square-transfers}; each is a period because $(F_{\pi_p},F_{\pi_p+1})\equiv(0,1)\pmod{p}$ for the listed value $\pi_p$, and the Fibonacci recurrence gives the residues below. For each group we use only the periods of its own primes. \paragraph{Values of $q$ in $\{3,\,903\}$ and $\{12,\,168,\,672\}$.} For every odd $n$, at least one of $p=5,11$ gives $F_n\bmod p\in q(\mathbb F_p^\times)^2$ whenever $q$ is a nonsquare modulo $5$ and a nonzero square modulo $11$. Indeed, if $n\equiv3,7\pmod{10}$, then $F_n\equiv2$ or $3\pmod{5}$, both nonsquares. In the other odd classes $n\equiv1,5,9\pmod{10}$, the residues modulo $11$ are $1,5,1$, all squares. This proves the required congruence for $q\in\{3,\,903\}$ and, at odd indices, for $q\in\{12,\,168,\,672\}$. For the latter group, a relevant even index is $10,34,58,82$, or $106$ modulo $120$. For the classes $34,106$ modulo $120$, the Fibonacci residues modulo $5$ are $2,3$; for the class $82$, the residue modulo $11$ is $1$. For the classes $10,58$, use $31$: the Fibonacci residues are respectively $24,30\pmod{31}$, both nonsquares. \paragraph{The two groups using $p=19$.} Consider the third and fourth rows of the table. For an odd multiple of $3$, the index is $3,9$, or $15$ modulo $18$. The Fibonacci residues modulo $19$ are respectively $2,15,2$, all nonsquares. Thus $p=19$ gives the required congruence at all relevant odd indices for both groups. For the latter group and $n\equiv10\pmod{24}$, split according to $n\equiv10,34,58\pmod{72}$. At $10,34$, the residues modulo $17$ are $4,16$, both squares; at $58$, the residue modulo $19$ is $3$, a nonsquare. \paragraph{Values of $q$ in $\{9,\,777\}$.} Here $n\equiv10\pmod{24}$, so \[ n\bmod28\in\{2,6,10,14,18,22,26\}. \] In the classes $2,10,18,26$ modulo $28$, the Fibonacci residues modulo $13$ are $1,3,10,12$, all nonzero squares. Combining the remaining classes modulo $28$ with $n\equiv10\pmod{24}$ gives $n\equiv34,106,154\pmod{168}$. Their Fibonacci residues modulo $83$ are $40,51,38$, respectively, with square roots $17,36,11$. \paragraph{The value $q=315$.} The relevant odd indices are $9,15,33,39,57,63$ modulo $72$. Their Fibonacci residues modulo $107$ are \[ 34,\quad75,\quad105,\quad105,\quad75,\quad34, \] respectively. The three distinct values $34$, $75$, and $105$ have square roots $26$, $17$, and $31$, respectively, modulo $107$. Also $315\equiv101\equiv23^2\pmod{107}$. \paragraph{The value $q=609$.} Among the indices $n\equiv10\pmod{24}$, those with $n\equiv58\pmod{72}$ have $F_n\equiv14\pmod{17}$, a nonsquare. Since $609$ is also a nonzero nonsquare modulo $17$, the quotient $F_n/609$ is a nonzero square modulo $17$. For the other classes of $n\equiv10\pmod{24}$, the calculation modulo $53$ is \[ \begin{array}{c|rrrrrr} n\bmod216&10&34&82&106&154&178\\\hline F_n\bmod53&2&34&30&52&21&20. \end{array} \] All entries except $52$ are nonsquares. At the remaining class $n\equiv106\pmod{216}$, use $109$: since $106\equiv-2\pmod{108}$, \[ F_n\equiv-1\equiv33^2\pmod{109},\qquad 609\equiv64\equiv8^2\pmod{109}. \] The residue $F_{108-2}\equiv-1\pmod{109}$ follows by running the Fibonacci recurrence backward from $(F_{108},F_{109})\equiv(0,1)\pmod{109}$. \paragraph{The value $q=924$.} As above, $p=19$ gives the required congruence at the relevant odd indices. It also does so for $n\equiv34,58\pmod{72}$, where the Fibonacci residues are $18,3$, both nonsquares. The remaining indices satisfy $n\equiv10\pmod{72}$, that is, $n\equiv10,82,154\pmod{216}$. The residues modulo $53$ are $2,30,21$, all nonsquares. In each case $q$ and $F_n$ are nonzero modulo $p$ and have the same character. Hence $F_n/q$ is a nonzero square modulo $p$, as required. \end{proof} \begin{proof}[Proof of \cref{prop:f-extension-universality}] By the reduction at the start of the section, it suffices to show that $f\perp\la q\ra$ represents $F_n$ for every $q\in\mathcal Q_7$ and every $n\ge48$. For $q=7$, this follows from \cref{prop:f-seven-universal}. For every other value of $q$, \cref{lem:small-subtraction} proves representation for every $F_n$ whose pair $(q\bmod12,F_n\bmod12)$ is outside \eqref{eq:remaining-residues}. In the remaining cases, \cref{lem:congruence-cover} supplies a prime $p\in\mathcal P_7$, and \cref{lem:square-transfer-subtraction} applies to it as soon as $F_n>B_*$, where \begin{equation}\label{eq:irregular-tail-bound} \overline{k}=\left\lfloor\frac{7\cdot109^2}{2}\right\rfloor=41583, \qquad B_*=1022\overline{k}^2=1767187098558; \end{equation} here $109$ is the largest prime in $\mathcal P_7$ and $1022$ the largest element of $\mathcal Q_7$. Since $F_{61}=2504730781961>B_*$, the required representation follows for every $n\ge61$. For $48\le n\le60$, we have $F_n\equiv10\pmod{12}$ only at $n=57$ and $F_n\equiv7\pmod{12}$ only at $n=58$. For these two indices, we apply \cref{lem:square-transfer-subtraction} with $p\le19$. The following table supplies a prime satisfying its congruence hypothesis for every remaining pair $(q,n)$: \begin{center} \small \renewcommand{\arraystretch}{1.12} \begin{tabular}{c|l|l} $p$ & $q$ for $n=57$ & $q$ for $n=58$\\\hline $5$ & $\{3,\,12,\,168,\,483,\,672,\,903\}$ & $\{9,\,21,\,84,\,189,\,336,\,609,\,756,\,924\}$\\ $11$ & $\{84,\,315,\,336,\,756\}$ & $\{525,\,777\}$\\ $13$ & $\{231,\,924\}$ & $\{12,\,168,\,672\}$\\ $17$ & $15$ & ---\\ $19$ & $819$ & --- \end{tabular} \end{center} The two columns contain exactly the elements of $\mathcal Q_7$ with $q\equiv0,3\pmod{12}$ and $q\equiv0,9\pmod{12}$, respectively. In each entry, $p\nmid q$ and $F_n\bmod p\in q(\mathbb F_p^\times)^2$, as one checks by reducing $q$ modulo $p$ and using the residues \[ \begin{array}{c|rrrrr} p&5&11&13&17&19\\\hline F_{57}\bmod p&2&2&1&15&2\\ F_{58}\bmod p&4&10&1&\text{---}&\text{---} \end{array} \] (the last two entries are not needed). Since $p\le19$ and \[ q\left\lfloor\frac{7p^2}{2}\right\rfloor^2 \le1022\cdot1263^2=1630262718t$. Choose the unique $j\in\{t+1,\ldots,2t+1\}$ congruent to $N$ modulo $t+1$. This is the least integer greater than $t$ in its residue class, so $j\le N$ and $N-j=(t+1)m$ with $m\ge0$. Write $m=a_1^2+\cdots+a_4^2$ by Lagrange's four-square theorem. The four equal summands then represent $(t+1)m$, and the unary summand $\la j\ra$ supplies $j$. Thus $V_t$ represents $N$. Since $P_t$ already represents every Fibonacci number below $t$, the lattice $V_t$ represents every Fibonacci number except $t$. If a Fibonacci criterion set omitted $t$, then $V_t$ would represent every element of that set without being Fibonacci-universal. Hence every criterion set contains every $t\in C$. Together with sufficiency, this proves that $C$ is the unique minimal Fibonacci criterion set. \end{proof} \begin{proof}[Proof of \cref{cor:forty-two}] The numbers $F_1,\ldots,F_{42}$ include every member of $C$, so \cref{thm:main} proves sufficiency. \Cref{prop:regular-table} shows that $\la1,1,2\ra$ has Fibonacci truant $F_{42}$, proving sharpness. \end{proof} \section{Concluding remarks}\label{sec:conclusion} The proof of \cref{thm:main} combines sequence-specific calculations with more general representation arguments. The truants and escalators, and the residue calculations used to prove universality of their extensions, depend on the Fibonacci sequence. Periodicity, growth, and the bounds \eqref{eq:fibonacci-prime-parts} on prime-power parts make these calculations sufficient for all indices. We conclude by isolating the square-transfer principle and explaining what would be needed to apply the strategy to other sequences. In \cref{sec:irregular}, every eligible integer is represented by $f$ or by $h$, and the maps $B_p$ turn representations by $h$ into representations by $f$ after multiplication by $p^2$. More generally, let $L,L'$ be positive-definite integral lattices, and let $\mathcal A\subseteq\Z_{>0}$ consist of integers represented by $L$ or $L'$. Fix a finite nonempty set $\mathcal P$ of primes. For each $p\in\mathcal P$, suppose there is a $\Z$-linear map $B_p:L'\to L$ such that \[ Q_L(B_pv)=p^2Q_{L'}(v)\qquad(v\in L'), \] and suppose $R/p^2\in\mathcal A$ whenever $R\in\mathcal A$ and $p^2\mid R$. Let $\mu\ge1$ be coprime to every prime in $\mathcal P$. In \cref{sec:irregular}, these data are $L=f$, $L'=h$, the eligible integers $\mathcal A$, $\mathcal P=\mathcal P_7$, and $\mu=7$. For $q\in\mathcal Q_7\setminus\{7\}$, \cref{lem:eligible-class-mod-seven} supplies the class modulo $\mu$ required below. The proposition abstracts \cref{lem:square-transfer-subtraction}. \begin{proposition}[Representation using congruences] \label{prop:finite-cover-principle} In the setting above, let $N,q\in\Z_{>0}$ and $p\in\mathcal P$. Suppose that $N\equiv qk_p^2\pmod{p^2}$ for some integer $k_p$. Suppose also that there is a residue class $k_\mu$ modulo $\mu$ such that every positive difference $N-qk^2$ with $k\equiv k_\mu\pmod{\mu}$ belongs to $\mathcal A$. If \[ N>q\left\lfloor\frac{\mu p^2}{2}\right\rfloor^2, \] then $L\perp\la q\ra$ represents $N$. \end{proposition} \begin{proof} As in \cref{lem:square-transfer-subtraction}, the Chinese remainder theorem gives $k\equiv k_p\pmod{p^2}$ and $k\equiv k_\mu\pmod{\mu}$ with $|k|\le\lfloor\mu p^2/2\rfloor$. Hence $R=N-qk^2$ is positive, belongs to $\mathcal A$, and is divisible by $p^2$. Since $R/p^2\in\mathcal A$, represent it by $L$ or $L'$ and then scale by $p$ or apply $B_p$, respectively. This represents $R$ by $L$; the coordinate $k$ supplies $qk^2$. \end{proof} When $p$ is odd and $p\nmid qN$, the hypothesis modulo $p^2$ follows by Hensel's lemma from a solution of $N\equiv qk^2\pmod{p}$ with $p\nmid k$; this is the form used in \cref{lem:square-transfer-subtraction}. To turn this representation principle into a criterion for another sequence $(s_n)$, one must first determine its escalators and prove universality of the relevant extensions. The stopping rank need not be four, or even the same on every branch; varying depths already occur in the Fifteen Theorem \cite{Bhargava15}. Moreover, unlike the Fibonacci case of \cref{lem:no-rational-truant}, a truant may be represented over $\Q$ by its escalator. An escalation can then enlarge the lattice without raising its rank. For steps that do raise the rank, the bound on $q$ remains available. The proof of \cref{lem:truant-equation} uses neither the rank of $T$ nor any property of the Fibonacci numbers: an extension of an escalator $T$ by one dimension that represents its truant contains $T\perp\la q\ra$ with $q\le\tau_T(\det G_T)^2$. Thus, for each such $T$, only finitely many values of $q$ need be considered. What remains is to find a usable criterion for representation by $T$. In the regular cases of this paper, local conditions reduce the problem to residue calculations and lower bounds on the prime-to-$p$ parts of the sequence terms. In the irregular case, representation by $f$ or $h$ and the square-transfer maps provide a substitute. If $(s_n)$ tends to infinity and is periodic modulo the relevant moduli, a congruence cover for fixed transfer data can be checked over a common period. Once that cover and the required classes modulo $\mu$ have been established, growth gives the size bound in \cref{prop:finite-cover-principle} beyond a finite initial range. Periodicity does not itself guarantee that a cover exists, however, and the initial terms still require separate treatment. Lucas sequences are natural candidates, because their arithmetic provides analogues of the periodicity, growth, and valuation bounds used here. Consider $t_0=0$, $t_1=1$, and $t_{n+2}=at_{n+1}+bt_n$, with coprime integers $a,b$, and suppose that the roots $\alpha,\beta$ of $X^2-aX-b$ satisfy $\alpha>\max(1,|\beta|)$. For $n\ge1$, the terms $t_n=(\alpha^n-\beta^n)/(\alpha-\beta)$ are positive and grow exponentially. Modulo an integer $m$ coprime to $b$, the pair recurrence is invertible on a finite set, so the sequence is periodic. For each fixed prime $p$, the valuation formulas of Sanna \cite[Theorem~1.5]{Sanna} give $v_p(t_n)\le v_p(n)+C_p$ for a constant $C_p$ depending on the recurrence; if $p\mid b$, all terms of positive index are $p$-units. Thus $p^{v_p(t_n)}\le p^{C_p}n$, and the unit part $t_n/p^{v_p(t_n)}$ still grows exponentially, which is what the regular-case subtractions require. The sequence-specific inputs, however, can change from the start. In the Fibonacci case, the ordinary and Fibonacci truants agree through rank~$2$, so the ternary escalators are the classical ones. For the Pell numbers ($a=2$, $b=1$), this fails already at rank~$2$: the least Pell number omitted by $\la1,1\ra$ is $12$, whereas its ordinary and Fibonacci truants are $3$. Pell escalation therefore produces different ternary lattices, and an explicit criterion would require their classification, along with associated representation results and the corresponding congruence arguments. It would also be interesting to know whether the number of initial terms that suffices for universality with respect to the sequence can be bounded uniformly over these Lucas sequences. It is not clear whether this method can yield such a bound, because the escalation, including the rank at which it stops, and the arithmetic thresholds all depend on the recurrence. In the meantime, the Fibonacci criterion gives one further instance in which $42$ is the answer to everything. \begin{quote} \textit{``The Answer to the Great Question... Of Life, the Universe and Everything... Is... Forty-two''} \smallskip \hfill ---Douglas Adams, \emph{The Hitchhiker's Guide to the Galaxy} \end{quote} \phantomsection \addcontentsline{toc}{section}{Lean formalization} \label{sec:lean} \section*{Lean formalization} \begingroup \emergencystretch=3em \Cref{thm:main} has been formalized in Lean~4. The formalization proves sufficiency, the indispensability of every member of $C$, the uniqueness of the minimal criterion set, and \cref{cor:forty-two}. As in this paper, the statement concerns positive-definite forms with integral symmetric Gram matrices, in arbitrary finite rank. The final theorem is \nolinkurl{fibonacci_criterion} in \nolinkurl{FibonacciCriterion/Criterion/Theorem.lean}. The complete formal development and instructions for reproducing its verification are available in the public accompanying repository at \url{https://github.com/scduko/Fibonacci-Universality-Criterion}. It has no unproven hypotheses: the classical representation criteria and the Fibonacci valuation formulas used in the proof are proven in the formal development or in the libraries on which it depends. The same file restates the criterion for an integer matrix that is positive definite in the sense of Lean's mathematical library Mathlib (\nolinkurl{fibonacci_criterion_matrix}), so the statement can be read against standard definitions. \paragraph{Organization.} The formal proof uses the reductions, case divisions, representatives, and cutoffs of this paper, and its files are grouped by section: \nolinkurl{Fibonacci/} for \cref{sec:fib}, \nolinkurl{Escalation/} for \cref{sec:tree}, \nolinkurl{Forms/} for \cref{sec:quat}, \nolinkurl{Regular/} for \cref{sec:regular-closure}, \nolinkurl{Irregular/} for \cref{sec:irregular}, and \nolinkurl{Criterion/} for \cref{sec:criterion}. The square-transfer matrices of Appendix~\ref{app:seven-transfers} are included with the formalization of \cref{sec:irregular}. The classical inputs are kept separate. The file \nolinkurl{ClassicalInputs/Definitions.lean} collects them: the three-square theorem, the criteria of \cref{prop:regular-table} for $\la1,1,3\ra$, $\la1,2,3\ra$, and $\la1,2,5\ra$, the sufficiency direction of \cref{prop:det7-local}, and \cref{lem:valuations}. \nolinkurl{Criterion/Proof.lean} proves the criterion from these inputs, and \nolinkurl{ClassicalInputs/Theorems.lean} proves the inputs. The file \nolinkurl{docs/READING_GUIDE.md} maps the manuscript's results to the corresponding Lean modules. \paragraph{Differences from the paper.} The formalization follows the argument needed for the criterion, rather than formalizing every auxiliary assertion in the paper. The principal differences are as follows. The file \nolinkurl{docs/PAPER_CORRESPONDENCE.md} gives the complete list. \begin{itemize} \item \emph{Gram matrices in place of lattices.} Lean works with forms given by Gram matrices and does not construct the lattices $L_i$. The escalation of \cref{prop:ternary-list} produces three vectors whose Gram matrix is that of one of the nine ternary escalators, and an extension $T+\Z v$ is recorded by the pair $(c,m)$ of \cref{sec:quat}. Lean proves the identity \eqref{eq:integral-identity} and the containment of $T\perp\la q\ra$ in $M$, but not that the index is $d$, which the proof does not use. It also proves the truant equation \eqref{eq:truant-equation}, including $k\ge1$, and derives the bounds of \cref{lem:truant-equation} from it. \item \emph{The regular ternaries.} \Cref{prop:regular-table} is proven as a list of criteria for integral representation; regularity, as a local--global statement, is not formalized. The three-square theorem is taken from the library atlas-lean. For $\la1,1,3\ra$, $\la1,2,3\ra$, and $\la1,2,5\ra$, where this paper cites Jones--Pall \cite{JonesPall}, Lean proves sufficiency by the Mordell-type construction of Blackwell, Durham, Thompson, and Treece \cite{BDTT}, together with Minkowski reduction and lists of the reduced ternary forms of determinants $3$, $6$, and $10$. The determinant-$10$ argument includes the even-valued class among the four reduced classes; for even integers it chooses the parameters of the construction so that the resulting form represents an odd integer, which excludes that class. \item \emph{The forms $f$ and $h$.} Lean proves the direction of \cref{prop:det7-local} that the criterion uses: every eligible positive integer is represented by $f$ or by $h$. The construction is stated for integers not divisible by $49$. This is all the applications need: the Fibonacci numbers of \cref{prop:first-fibonacci-exceptions} and the differences of \cref{sec:irregular} are not divisible by $49$, and \cref{prop:f-seven-universal} treats multiples of $49$ by scaling by $7$. This does not require $7$-adic Fibonacci valuation estimates. Lean follows the two auxiliary-prime constructions of the proof, with Minkowski reduction from the library TauCeti, and it excludes reduced forms outside the classes of $f$ and $h$ by counting their zeros modulo $7$ rather than by the square class of a binary determinant. Of the converse, it proves only the $7$-adic obstruction for $f$. \item \emph{Fibonacci arithmetic.} \Cref{lem:valuations} is proven from the formulas for $F_{2m}$, $F_{3m}$, and $F_{5m}$. The $2$-adic rows of \cref{lem:first-exceptional-members} and the Fibonacci numbers needed in \cref{lem:two-adic-exception-bounds} are read from a table of $v_2(F_n)$ and $u_2(F_n)$ for $1\le n\le64$. Lean proves that the Fibonacci residues return after the periods it uses, but not that these periods are the least ones of \cref{lem:periods}. \item \emph{The congruence cover.} For \cref{lem:congruence-cover}, Lean uses the same eight groups of values of $q$ and the same ten primes. In place of the calculation with quadratic characters, it checks the residue classes required by \eqref{eq:remaining-residues} over a common period for each group, of length at most $216$, and proves that this implies the statement for every index. \end{itemize} \paragraph{Finite checks.} The principal finite assertions of the formal proof are the table and the residue checks just described, the twelve identities of \cref{tab:seven-square-transfers}, the witnesses and the eligibility checks of \cref{prop:first-fibonacci-exceptions}, the small-prime table for $n=57,58$ in the proof of \cref{prop:f-extension-universality}, the congruences of \cref{tab:criterion-truants}, and the lists of reduced ternary forms; the file \nolinkurl{docs/PAPER_CORRESPONDENCE.md} lists all of them. The residue and enumeration checks are evaluated by the Lean kernel, with soundness and coverage lemmas giving the statements needed for all integers or indices. The transfer identities are proven by \texttt{ring}, whose proofs are also checked by the kernel. The formal proof uses no external certificates, data files, or scripts. \paragraph{Verification.} The version described here is commit \href{https://github.com/scduko/Fibonacci-Universality-Criterion/commit/% 499b60d88ab035addae42b3a3a1a7a541c63f29c}{% \texttt{499b60d88ab0}} of \href{https://github.com/scduko/Fibonacci-Universality-Criterion} {the public accompanying repository}. It uses Lean~4.35.0 and pinned versions of Mathlib, TauCeti, and atlas-lean. \href{https://github.com/scduko/Fibonacci-Universality-Criterion/actions/runs/43099379799}{% The verification run} at this commit passed the complete build, an independent replay of every module in the Lean kernel by \texttt{leanchecker}, and an audit of the axioms used by all $2{,}960$ declarations. The audit allows only Lean's standard axioms \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound}. The repository includes the full source and instructions for reproducing these checks. \endgroup \phantomsection \addcontentsline{toc}{section}{Provenance of the argument} \label{sec:provenance} \section*{Provenance of the argument} The first version of the argument established the Fibonacci criterion conditional on the Generalized Riemann Hypothesis (GRH), using an analytic representation result for the irregular ternary $f$. An attempt to remove that hypothesis by means of OpenAI's quasi-Riemann-hypothesis work \cite{OpenAIQRH} led instead to the square-transfer and congruence argument of \cref{sec:irregular}, which uses no analytic representation estimates. Neither GRH nor the quasi-Riemann-hypothesis result is assumed in the present proof. The paper and the formalization were developed together, and each shaped the other. Automated proof development in Lean suggested the direct construction for determinant $7$ in \cref{prop:det7-local}, the congruence obstructions of \cref{tab:criterion-truants}, and the reductions to three squares in \cref{prop:regular-table}; after these arguments were checked in Lean and their mathematical content reviewed, they were adopted here. Refinements of the manuscript subsequently informed the formalization. Comparing the paper with the formal proof led to the smaller set of possible values of $q$ in \cref{lem:q-values-for-f} and the short proof of \cref{prop:f-seven-universal}, which together removed the need for $7$-adic Fibonacci valuation estimates. The case analysis in \cref{lem:congruence-cover} replaced an exhaustive computer check of the congruence cover. These refinements were then incorporated into the Lean, so the formal proof follows the revised argument. Following a preliminary draft of this paper, the elements of $C$ were also recorded in the On-Line Encyclopedia of Integer Sequences as \href{https://oeis.org/A401169}{A401169}. \section*{Acknowledgments} I thank V\'it\v{e}zslav Kala and Glenn Bruda for helpful comments. This work was conducted while I was visiting the Technological Innovation, Entrepreneurship, and Strategic Management (TIES) Group at the MIT Sloan School of Management; I greatly appreciate their hospitality. \section*{Use of Generative AI Technology} I used LLMs to assist with coding, computations, analysis, and revision, including GPT-6 Astra, GPT-5.2 Pro, GPT-5.5 Pro, GPT-5.6 Sol, and Claude Fable 5 (all accessed in part via Poe with the support of Quora, where I am an advisor). The Lean formalization was developed using Claude Opus 5.5, Claude Fable 5.2, and GPT-6 Astra. GPT-6 Astra identified a key step that made it possible to make my earlier conditional argument unconditional. The problem, methods, and final written form are my own, and any errors remain my responsibility. \bigskip \appendix \section{Square-transfer matrices}\label{app:seven-transfers} Kneser's neighbor construction gives a structural source of the square-transfer maps in \eqref{eq:seven-square-transfer}; see \cite{Chenevier}. If lattices $L_f,L_h$, isometric to $f,h$ respectively, are $p$-neighbors in the same rational quadratic space, their intersection has index $p$ in each. Hence $pL_h\subseteq L_f$, and writing this inclusion in integral bases gives a matrix satisfying \eqref{eq:seven-square-transfer}. For the chosen primes, the displayed matrix identities provide the complete verification needed here. \Cref{tab:seven-square-transfers} gives the matrices in \eqref{eq:seven-square-transfer} by their rows. Periods are listed modulo $p$ for the ten primes in $\mathcal P_7$. The rows $p=2,3$ supply the coordinate maps in \cref{lem:f-mod-twelve} and are not used in \cref{lem:congruence-cover}. Each period and matrix identity can be checked independently of the others. \begin{table}[htbp] \setlength{\belowcaptionskip}{8pt} \centering \caption{Integral square transfers and Fibonacci periods.} \label{tab:seven-square-transfers} \normalsize \setlength{\tabcolsep}{6pt} \renewcommand{\arraystretch}{1.08} \begin{tabular}{r r l l l} \hline $p$ & Period & Row $1$ & Row $2$ & Row $3$\\ \hline $2$ & --- & $(0,-2,0)$ & $(0,0,4)$ & $(-1,0,-1)$ \\ $3$ & --- & $(-1,-1,7)$ & $(-1,2,1)$ & $(-1,-1,-2)$ \\ $5$ & $20$ & $(-3,-3,7)$ & $(-2,3,3)$ & $(-1,-1,-6)$ \\ $11$ & $10$ & $(-3,-7,-21)$ & $(-1,-6,15)$ & $(-5,3,-2)$ \\ $13$ & $28$ & $(-5,-9,-21)$ & $(-6,-3,19)$ & $(-3,5,-10)$ \\ $17$ & $36$ & $(-1,-15,-21)$ & $(-3,6,-29)$ & $(9,-1,2)$ \\ $19$ & $18$ & $(-3,-3,49)$ & $(-6,13,3)$ & $(-7,-7,-6)$ \\ $31$ & $30$ & $(-15,-13,63)$ & $(-2,21,27)$ & $(-13,-3,-26)$ \\ $53$ & $108$ & $(-21,-39,77)$ & $(-14,27,69)$ & $(-19,-5,-54)$ \\ $83$ & $168$ & $(-9,-9,217)$ & $(-26,57,9)$ & $(-31,-31,-18)$ \\ $107$ & $72$ & $(-35,-51,-231)$ & $(-30,-59,123)$ & $(-39,41,-22)$ \\ $109$ & $108$ & $(-3,-105,-77)$ & $(-41,-18,183)$ & $(-37,13,-114)$ \\ \hline \end{tabular} \end{table} \clearpage \begingroup \small \raggedright \providecommand{\bysame}{\leavevmode\hbox to3em{\hrulefill}\thinspace} \providecommand{\href}[2]{#2} \begin{thebibliography}{10} \bibitem{BallotLuca} C.~Ballot and F.~Luca, \emph{On the equation {$x^2+dy^2=F_n$}}, Acta Arith. \textbf{127} (2007), 145--155. \bibitem{BLM} P.~Berrizbeitia, F.~Luca, and A.~Mendoza, \emph{Quadratic forms representing the $p$-th {F}ibonacci number}, preprint, 2015, arXiv:1502.04346. \bibitem{Bhargava15} M.~Bhargava, \emph{On the {C}onway--{S}chneeberger {F}ifteen {T}heorem}, Quadratic forms and their applications, Contemp. Math., vol. 272, Amer. Math. Soc., 2000, pp.~27--37. \bibitem{BhargavaHanke} M.~Bhargava and J.~Hanke, \emph{Universal quadratic forms and the $290$-theorem}, preprint, 2011. \bibitem{BDTT} Sarah Blackwell, Gabriel Durham, Katherine Thompson, and Tiffany Treece, \emph{A generalization of a method of {M}ordell to ternary quadratic forms}, Int. J. Number Theory \textbf{12} (2016), no.~8, 2081--2105. \bibitem{Chandee} V.~Chandee, \emph{Explicit upper bounds for {$L$}-functions on the critical line}, Proc. Amer. Math. Soc. \textbf{137} (2009), no.~12, 4049--4063. \bibitem{Chenevier} G.~Chenevier, \emph{Statistics for {K}neser $p$-neighbors}, Bull. Soc. Math. France \textbf{150} (2022), no.~3, 473--516. \bibitem{Conway} J.~H. Conway, \emph{Universal quadratic forms and the {F}ifteen {T}heorem}, Quadratic forms and their applications, Contemp. Math., vol. 272, Amer. Math. Soc., 2000, pp.~23--26. \bibitem{JonesPall} B.~W. Jones and G.~Pall, \emph{Regular and semi-regular positive ternary quadratic forms}, Acta Math. \textbf{70} (1939), 165--191. \bibitem{Prime67} J.~Ju, D.~Kim, K.~Kim, M.~Kim, and B.-K. Oh, \emph{Prime-universal diagonal quadratic forms}, Bull. Aust. Math. Soc. \textbf{103} (2021), 390--404. \bibitem{KKR} V.~Kala, J.~Kr{\'a}sensk{\'y}, and G.~Romeo, \emph{Universality criterion sets for quadratic forms over number fields}, Adv. Math. \textbf{500} (2026), Paper No.~111080. \bibitem{Kaplansky} I.~Kaplansky, \emph{The first nontrivial genus of positive definite ternary forms}, Math. Comp. \textbf{64} (1995), no.~209, 341--345. \bibitem{Kelley} J.~Kelley, \emph{{K}aplansky's ternary quadratic form}, Int. J. Math. Math. Sci. \textbf{25} (2001), no.~5, 289--292. \bibitem{KKO} B.~M. Kim, M.-H. Kim, and B.-K. Oh, \emph{A finiteness theorem for representability of quadratic forms by forms}, J. Reine Angew. Math. \textbf{581} (2005), 23--30. \bibitem{KLO} K.~Kim, J.~Lee, and B.-K. Oh, \emph{Minimal universality criterion sets on the representations of binary quadratic forms}, J. Number Theory \textbf{238} (2022), 37--59. \bibitem{Lengyel} T.~Lengyel, \emph{The order of the {F}ibonacci and {L}ucas numbers}, Fibonacci Quart. \textbf{33} (1995), 234--239. \bibitem{Mahler} K.~Mahler, \emph{On reduced positive definite ternary quadratic forms}, J. London Math. Soc. \textbf{15} (1940), no.~3, 193--195. \bibitem{OnoSound} K.~Ono and K.~Soundararajan, \emph{{R}amanujan's ternary quadratic form}, Invent. Math. \textbf{130} (1997), no.~3, 415--454. \bibitem{OpenAIQRH} {OpenAI}, \emph{The quasi-{R}iemann hypothesis}, \url{https://github.com/openai/math/tree/main/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026}, 2026, preprint, September 30, 2026. \bibitem{Ramanujan} S.~Ramanujan, \emph{On the expression of a number in the form $ax^2+by^2+cz^2+du^2$}, Proc. Cambridge Philos. Soc. \textbf{19} (1917), 11--21. \bibitem{Reinke} T.~Reinke, \emph{{Darstellbarkeit ganzer Zahlen durch Kaplanskys tern\"are quadratische Form}}, Ph.D. thesis, Westf\"alische Wilhelms-Universit\"at M\"unster, 2002. \bibitem{Rouse} J.~Rouse, \emph{Quadratic forms representing all odd positive integers}, Amer. J. Math. \textbf{136} (2014), no.~6, 1693--1745. \bibitem{Sanna} C.~Sanna, \emph{The $p$-adic valuation of {L}ucas sequences}, Fibonacci Quart. \textbf{54} (2016), no.~2, 118--124. \bibitem{Wall} D.~D. Wall, \emph{{F}ibonacci series modulo $m$}, Amer. Math. Monthly \textbf{67} (1960), 525--532. \end{thebibliography} \endgroup \end{document}