\chapter{Introduction}\label{ch:intro}

Let $G=(V,\mathcal{H})$ be a finite hypergraph.
We say that $G$ \emph{contains a partition of size $m$} if there are $D\subseteq V$ and $\mathcal{P}\subseteq \mathcal{H}$ with $|D|=m$ such that every vertex of $D$ belongs to exactly one edge of $\mathcal{P}$.
Write $H(n)$ for the largest $k\in\mathbb{N}$ such that there exists a finite edge family $\mathcal{H}$ with $|\bigcup \mathcal{H}|=k$ and no partition of size greater than $n$.
This is the edge-set presentation that we formalize: the ``no isolated vertices'' clause is built in because the vertex set is taken to be the union of the edges.
In the accompanying formalization, finite edge families are abbreviated as \texttt{Hypergraph V}, and indexed families as \texttt{HypergraphFamily}.

Define a sequence $k_n$ by $k_0=0$, $k_1=1$, and
\[
  k_n=\lfloor n/2\rfloor+k_{\lfloor n/2\rfloor}+k_{\lfloor(n+1)/2\rfloor}
  \quad(n\ge 2).
\]

\begin{theorem}\label{thm:main}
  \lean{HypergraphLowerBound.thm_main}
  \leanok%
  \uses{def:H_n, def:k_n, thm:constructive_An, thm:uniform_26_25}
  There exists a sequence of hypergraphs ${\left(G_n\right)}_{n\ge 1}$ with the following properties.
  For every $n\ge 1$, the hypergraph $G_n$ has exactly $n$ distinct edges and contains no partition of size greater than $n$.
  In the formalization attached to this blueprint, the vertex set is the union of the edges, so the paper's ``no isolated vertices'' clause is implicit.
  Moreover, for every $n\ge 15$,
  \[
    |V(G_n)|\ge \frac{26}{25}\,k_n.
  \]
  Consequently,
  \[
    H(n)\ge \frac{26}{25}\,k_n
    \qquad(n\ge 15).
  \]
\end{theorem}

The explicit recursive construction itself is developed in the witness-building results culminating in Theorem~\ref{thm:constructive_An}; the theorem linked here is the packaged sequence-level consequence obtained by choosing one witness for each $n$.
In the formalization, the resulting data are bundled in the structure \texttt{HypergraphLowerBound.WitnessFamily}.

\begin{corollary}\label{cor:main_H_lower_bound}
  \lean{HypergraphLowerBound.thm_main_H_lower_bound}
  \leanok%
  \uses{def:H_n, thm:main}
  For every $n\ge 15$,
  \[
    H(n)\ge \frac{26}{25}\,k_n.
  \]
\end{corollary}
\begin{proof}
  This is the final conclusion packaged into Theorem~\ref{thm:main}.
\end{proof}

The first strict improvement already occurs at $n=15$, and the minimum ratio in the finite bootstrap window $15\le n<60$ is attained at $n=17$:
\[
  A_{15}=45>43=k_{15},
  \qquad
  A_{17}=52=\frac{26}{25}k_{17}.
\]

\begin{theorem}\label{thm:asymptotic}
  \lean{HypergraphLowerBound.thm_asymptotic}
  \leanok%
  \uses{def:H_n, def:k_n, thm:fixed_t, thm:asymptotic_proof}
  The formal theorem linked here packages the two asymptotic theorems proved later in the file.
  First, for every fixed $t\ge 2$, Theorem~\ref{thm:fixed_t} gives
  \[
    H(n)\ge \frac{h_t-1}{\log_2 t}\,n\log_2 n - O_t(n),
    \qquad
    h_t:=1+\frac12+\cdots+\frac1t.
  \]
  Second, Theorem~\ref{thm:asymptotic_proof} yields
  \[
    \liminf_{n\to\infty}\frac{H(n)}{k_n}\ge 2\ln 2.
  \]
  This is the formal counterpart of the paper's introductory asymptotic theorem; both the recursive Lubell-family lower bound and the liminf argument are carried out completely in the accompanying Lean development.
\end{theorem}


\chapter{Support gadgets and substitution}\label{ch:substitution}

For a hypergraph $G=(V,\mathcal{H})$ and a chosen edge family $\mathcal{P}\subseteq \mathcal{H}$, define
\[
  u_G(\mathcal{P}):=|\{v\in V:\text{$v$ belongs to exactly one edge of }\mathcal{P}\}|.
\]
The partition problem is equivalent to a uniform bound on $u_G$.

\begin{definition}\label{def:H_n}
  \lean{HypergraphLowerBound.H}
  \leanok%
  Write $H(n)$ for the largest $k\in\mathbb{N}$ such that there exists a finite edge family $\mathcal{H}$ with $|\bigcup \mathcal{H}|=k$ and no partition of size greater than $n$.
  Equivalently, this is the paper's definition with the ``no isolated vertices'' condition built into the edge-set encoding.
\end{definition}

\begin{definition}\label{def:k_n}
  \lean{HypergraphLowerBound.k}
  \leanok%
  Define the sequence $k:\mathbb{N}\to\mathbb{N}$ by $k(0)=0$, $k(1)=1$, and
  \[
    k(n)=\lfloor n/2\rfloor+k(\lfloor n/2\rfloor)+k(\lfloor(n+1)/2\rfloor)
    \quad(n\ge 2).
  \]
\end{definition}

\begin{definition}\label{def:u_G}
  \lean{HypergraphLowerBound.uniqueCoverage}
  \leanok%
  For a hypergraph $G=(V,\mathcal{H})$ and a chosen edge family $\mathcal{P}\subseteq \mathcal{H}$, define
  \[
    u_G(\mathcal{P}):=|\{v\in V:\text{$v$ belongs to exactly one edge of }\mathcal{P}\}|.
  \]
\end{definition}

\begin{lemma}\label{lem:partition_u}
  \lean{HypergraphLowerBound.partition_iff_uniqueCoverage}
  \leanok%
  \uses{def:u_G}
  A hypergraph $G$ contains no partition of size greater than $n$ if and only if
  \[
    u_G(\mathcal{P})\le n
    \qquad\text{for every }\mathcal{P}\subseteq \mathcal{H}.
  \]
\end{lemma}
\begin{proof}
  If $(D,\mathcal{P})$ is a partition of size $m$, then every vertex of $D$ is counted by $u_G(\mathcal{P})$, so $u_G(\mathcal{P})\ge m$.
  Conversely, if $u_G(\mathcal{P})>n$, let $D$ be the set of vertices counted by $u_G(\mathcal{P})$; then $(D,\mathcal{P})$ is a partition of size $u_G(\mathcal{P})$.
\end{proof}

\begin{definition}\label{def:support_pattern}
  \lean{HypergraphLowerBound.SupportPattern}
  \leanok%
  Fix $t\ge 2$.
  A \emph{support pattern} on $[t]:=\{1,\dots,t\}$ is a subset of $[t]$ of size at least $2$.
\end{definition}

\begin{definition}\label{def:omega}
  \lean{HypergraphLowerBound.omega_count}
  \leanok%
  Let $\mathcal{F}$ be a finite multiset of support patterns on $[t]$.
  For $I\subseteq T\subseteq [t]$, define
  \[
    \omega_{\mathcal{F}}(T,I):=
    |\{S\in \mathcal{F}:\ S\subseteq T\text{ and }|S\cap I|=1\}|,
  \]
  counting multiplicity.
\end{definition}

\begin{definition}\label{def:n_frame}
  \lean{HypergraphLowerBound.IsFrame}
  \leanok%
  \uses{def:omega}
  Let $\mathbf{n}=(n_1,\dots,n_t)\in\mathbb{N}^t$.
  We say that $\mathcal{F}$ is an \emph{$\mathbf{n}$-frame} if
  \[
    \omega_{\mathcal{F}}(T,I)\le \sum_{j\in T\setminus I} n_j
    \qquad\text{for every }I\subseteq T\subseteq [t].
  \]
\end{definition}

\begin{definition}\label{def:substitution}
  \lean{HypergraphLowerBound.substitutionHypergraph}
  \leanok%
  \uses{def:support_pattern}
  Let $\mathcal{F}$ be a support multiset on $[t]$.
  Let $G_i=(V_i,\mathcal{H}_i)$, $1\le i\le t$, be hypergraphs with pairwise disjoint vertex sets and pairwise disjoint edge sets.
  The \emph{substitution hypergraph}
  \[
    \mathcal{F}[G_1,\dots,G_t]
  \]
  has edge set $\mathcal{H}_1\sqcup\cdots\sqcup\mathcal{H}_t$, and its vertex set consists of $V_1\sqcup\cdots\sqcup V_t$ together with one new vertex $x_S$ for each occurrence of a support pattern $S\in \mathcal{F}$.
  The new vertex $x_S$ is incident to every edge of $\mathcal{H}_i$ for every $i\in S$.
  In the formalization this is realized by tagging the block vertices and the support-vertex occurrences, so the disjointness is built into the construction itself.
  The surrounding indexed block family is packaged by the alias \texttt{HypergraphLowerBound.BlockFamily}, and support occurrences are indexed by \texttt{HypergraphLowerBound.SupportOcc}.
\end{definition}

\begin{theorem}\label{thm:substitution}
  \lean{HypergraphLowerBound.substitution_theorem}
  \leanok%
  \uses{def:n_frame, def:substitution, lem:partition_u}
  Let $\mathbf{n}=(n_1,\dots,n_t)\in\mathbb{N}^t$, and let $\mathcal{F}$ be an $\mathbf{n}$-frame on $[t]$.
  Assume that each $G_i$ contains no partition of size greater than $n_i$.
  Then the substituted hypergraph
  \[
    G:=\mathcal{F}[G_1,\dots,G_t]
  \]
  contains no partition of size greater than $n_1+\cdots+n_t$.
  Equivalently,
  \[
    u_G(\mathcal{P})\le n_1+\cdots+n_t
    \qquad\text{for every }\mathcal{P}\subseteq \mathcal{E}(G).
  \]
  The corresponding formal statement bundles the block-side assumptions into the structure \texttt{HypergraphLowerBound.PartitionedBlocks}.
\end{theorem}
\begin{proof}
  \uses{lem:partition_u, def:n_frame, def:substitution, def:u_G}
  Fix $\mathcal{P}\subseteq \mathcal{E}(G)$, and write $\mathcal{P}_i:=\mathcal{P}\cap \mathcal{H}_i$.
  Define
  \[
    T:=\{i:|\mathcal{P}_i|\le 1\},
    \qquad
    I:=\{i:|\mathcal{P}_i|=1\}.
  \]
  If $i\notin T$, then $|\mathcal{P}_i|\ge 2$, and the vertices of $V_i$ counted by $u_G(\mathcal{P})$ are counted by $u_{G_i}(\mathcal{P}_i)$, hence contribute at most $n_i$.
  If $i\in T\setminus I$, then $|\mathcal{P}_i|=0$, so the block $V_i$ contributes nothing.
  If $i\in I$, then again block $V_i$ contributes at most $n_i$.
  So the total contribution from the old block vertices is at most
  \[
    \sum_{i\notin T} n_i + \sum_{i\in I} n_i.
  \]

  Now consider a new support vertex $x_S$.
  It lies in exactly one selected edge if and only if $S\subseteq T$ and $|S\cap I|=1$.
  Hence the total contribution from support vertices is exactly
  \[
    \omega_{\mathcal{F}}(T,I)\le \sum_{j\in T\setminus I} n_j,
  \]
  because $\mathcal{F}$ is an $\mathbf{n}$-frame.
  Adding the two estimates gives
  \[
    u_G(\mathcal{P})\le
    \sum_{i\notin T} n_i + \sum_{i\in I} n_i + \sum_{j\in T\setminus I} n_j
    =
    \sum_{i=1}^t n_i.
  \]
  Lemma~\ref{lem:partition_u} finishes the proof.
\end{proof}

\begin{corollary}\label{cor:frame_recurrence}
  \lean{HypergraphLowerBound.frame_recurrence}
  \leanok%
  \uses{thm:substitution, def:n_frame}
  Suppose that for $1\le i\le t$ there is a hypergraph $G_i$ with exactly $n_i$ edges, no partition of size greater than $n_i$, and $a_i$ vertices.
  If $\mathcal{F}$ is an $(n_1,\dots,n_t)$-frame, then $\mathcal{F}[G_1,\dots,G_t]$ has exactly $n_1+\cdots+n_t$ edges, no partition of size greater than $n_1+\cdots+n_t$, and
  \[
    a_1+\cdots+a_t+|\mathcal{F}|
  \]
  vertices.
  In the edge-set formalization this is the version of the paper's statement in which the ``no isolated vertices'' condition is implicit.
  The corresponding formal statement packages these count assumptions into the structure \texttt{HypergraphLowerBound.CountedBlocks}.
\end{corollary}
\begin{proof}
  \uses{thm:substitution}
  The edge set is the disjoint union of the edge sets of the blocks, so the edge count is additive.
  Every old vertex remains non-isolated, and every new support vertex meets every edge in at least one block from its support.
  The vertex count is immediate, and the partition bound is Theorem~\ref{thm:substitution}.
\end{proof}


\chapter{The uniform factor $26/25$}\label{ch:uniform}

We now describe the explicit family proving Theorem~\ref{thm:main}.
There are three ingredients: a finite bank of exact small frames on at most five blocks, seven higher-arity boosters, and the balanced four-way family.

\begin{proposition}\label{prop:finite_bank}
  \lean{HypergraphLowerBound.finite_bank_valid}
  \leanok%
  \uses{def:n_frame}
  Every exact small frame listed in the paper, every booster, and every residue gadget $R_r$ is a valid frame for its stated capacity vector.
\end{proposition}
\begin{proof}
  This is a finite exhaustive check of the frame inequalities
  $\omega_{\mathcal{F}}(T,I)\le \sum_{j\in T\setminus I} n_j$
  for all $I\subseteq T\subseteq [t]$.
  In the formalization each row is packaged as a \texttt{HypergraphLowerBound.FrameSpec}, and the three finite collections are represented by the lists \texttt{exactSmallFrames}, \texttt{boosters}, and \texttt{residueGadgets}.
  The finite bootstrap choices for $A_n$ are then organized by the auxiliary table \texttt{under60Choices} of \texttt{ChoiceSpec} records.
\end{proof}

\begin{definition}\label{def:A_n}
  \lean{HypergraphLowerBound.A}
  \leanok%
  \uses{def:k_n}
  Define integers $A_n$ recursively as follows.
  Set $A_0:=0$ and $A_1:=1$.
  For $2\le n<60$, let $A_n$ be the value given by the finite bootstrap table.
  For $n\ge 60$, write $n=4m+r$, $0\le r\le 3$,
  and let $(a,b,c,d)$ be the nondecreasing balanced partition of $n$ into four positive parts:
  \[
    (a,b,c,d)=
    \begin{cases}
      (m,m,m,m),       & r=0, \\
      (m,m,m,m+1),     & r=1, \\
      (m,m,m+1,m+1),   & r=2, \\
      (m,m+1,m+1,m+1), & r=3.
    \end{cases}
  \]
  Then define
  \[
    A_n:=A_a+A_b+A_c+A_d+e_r(m),
  \]
  where
  \begin{align*}
    e_0(m) & :=\lfloor 13m/3\rfloor,     \\
    e_1(m) & :=\lfloor (13m+1)/3\rfloor, \\
    e_2(m) & :=\lfloor (13m+5)/3\rfloor, \\
    e_3(m) & :=\lfloor (13m+6)/3\rfloor.
  \end{align*}
  In the formalization these correction terms are collected by the helper \texttt{HypergraphLowerBound.e_bonus}.
\end{definition}

\begin{theorem}\label{thm:constructive_An}
  \lean{HypergraphLowerBound.constructive_An}
  \leanok%
  \uses{def:A_n, cor:frame_recurrence, prop:finite_bank}
  For every $n\ge 1$ there exists a hypergraph $G$ with exactly $n$ distinct edges, no partition of size greater than $n$, and $|V(G)|=A_n$.
  In the formalization, the data of such a witness are packaged in the structure \texttt{HypergraphLowerBound.Witness}, and then unwrapped into the existential statement recorded here.
  The corresponding development also exposes the intermediate public witness theorems \texttt{HypergraphLowerBound.A_witness} and \texttt{HypergraphLowerBound.thm_main_pointwise}.
  By choosing one such witness for each $n$, one obtains an explicit recursive family; as above, the paper's ``no isolated vertices'' clause is implicit in the edge-set encoding.
\end{theorem}
\begin{proof}
  \uses{cor:frame_recurrence, prop:finite_bank, def:A_n}
  We argue by induction on $n$.
  For $n=1$, take a single edge containing a single vertex.
  For $2\le n<60$, each row of the finite bootstrap table specifies one of four possibilities
  (binary, exact-frame, booster, balanced four-way), and Corollary~\ref{cor:frame_recurrence}
  applied to the smaller witnesses yields the stated vertex count.
  For $n\ge 60$, the balanced four-way split with $\lfloor n/12\rfloor$ copies of the $13$-vertex
  four-way core and one residue gadget gives $A_n$ vertices by the same corollary.
\end{proof}

\begin{lemma}\label{lem:k_four_way}
  \lean{HypergraphLowerBound.k_four_way}
  \leanok%
  \uses{def:k_n}
  For every $m\ge 1$,
  \begin{align*}
    k_{4m}   & =4k_m+4m,            \\
    k_{4m+1} & =3k_m+k_{m+1}+4m,    \\
    k_{4m+2} & =2k_m+2k_{m+1}+4m+1, \\
    k_{4m+3} & =k_m+3k_{m+1}+4m+2.
  \end{align*}
\end{lemma}
\begin{proof}
  \uses{def:k_n}
  The defining recurrence for $k_n$ immediately gives
  $k_{2m}=m+2k_m$ and $k_{2m+1}=m+k_m+k_{m+1}$.
  Applying these identities once more gives the displayed four-way formulas.
\end{proof}

\begin{lemma}\label{lem:floor_26_25}
  \lean{HypergraphLowerBound.floor_26_25}
  \leanok%
  \uses{def:A_n}
  For every integer $m\ge 15$,
  \begin{align*}
    e_0(m) & \ge \frac{26}{25}\cdot 4m, \\
    e_1(m) & \ge \frac{26}{25}\cdot 4m, \\
    e_2(m) & \ge \frac{26}{25}(4m+1),   \\
    e_3(m) & \ge \frac{26}{25}(4m+2).
  \end{align*}
\end{lemma}
\begin{proof}
  Using $\lfloor x\rfloor\ge x-1$ and direct calculation, each difference is at least $(13m-75)/75$, $(13m-50)/75$, $(13m-28)/75$, $(13m-52)/75$ respectively, all nonneg for $m\ge 15$.
\end{proof}

\begin{proposition}\label{prop:bootstrap_26_25}
  \lean{HypergraphLowerBound.bootstrap_26_25}
  \leanok%
  \uses{def:A_n, def:k_n}
  For every integer $n$ with $15\le n<60$,
  \[
    25A_n\ge 26k_n,
  \]
  and equality holds if and only if $n=17$.
  Equivalently, with $\Delta_n:=25A_n-26k_n$, one has $\Delta_n\ge 0$ for every $15\le n<60$, with equality only at $n=17$.
\end{proposition}
\begin{proof}
  This is the finite table check.
\end{proof}

\begin{theorem}\label{thm:uniform_26_25}
  \lean{HypergraphLowerBound.uniform_26_25}
  \leanok%
  \uses{prop:bootstrap_26_25, lem:floor_26_25, lem:k_four_way, def:A_n, def:k_n}
  For every integer $n\ge 15$,
  \[
    A_n\ge \frac{26}{25}\,k_n.
  \]
  Together with Theorem~\ref{thm:constructive_An}, this yields the sequence-level statement Theorem~\ref{thm:main}; Corollary~\ref{cor:main_H_lower_bound} is its extracted $H(n)$ consequence.
\end{theorem}
\begin{proof}
  \uses{prop:bootstrap_26_25, lem:floor_26_25, lem:k_four_way}
  The range $15\le n<60$ is Proposition~\ref{prop:bootstrap_26_25}.
  For $n\ge 60$, write $n=4m+r$ with $0\le r\le 3$ and note $m\ge 15$.
  Each case follows from Definition~\ref{def:A_n}, Lemma~\ref{lem:floor_26_25}, Lemma~\ref{lem:k_four_way}, and the inductive hypothesis.
\end{proof}


\chapter{Lubell frames and asymptotic context}\label{ch:lubell}

We now record the general Lubell family.

\begin{definition}\label{def:M_t}
  \lean{HypergraphLowerBound.M}
  \leanok%
  For $t\ge 2$, define
  \[
    M_t:=\operatorname{lcm}\left\{\binom{t-1}{r}:1\le r\le t-1\right\}.
  \]
\end{definition}

\begin{definition}\label{def:lubell_frame}
  \lean{HypergraphLowerBound.lubellFrame}
  \leanok%
  \uses{def:M_t}
  Let $\mathcal{L}_t$ be the support multiset on $[t]$ that contains every $j$-subset of $[t]$ with multiplicity
  \[
    \frac{M_t}{\binom{t-1}{j-1}}
    \qquad(2\le j\le t).
  \]
\end{definition}

\begin{proposition}\label{prop:lubell}
  \lean{HypergraphLowerBound.lubell_is_frame}
  \leanok%
  \uses{def:lubell_frame, def:n_frame, def:M_t}
  For every $t\ge 2$, the support multiset $\mathcal{L}_t$ is an $(M_t,\dots,M_t)$-frame.
  Moreover,
  \[
    |\mathcal{L}_t|=M_t\,t\,(h_t-1),
    \qquad
    h_t:=1+\frac12+\cdots+\frac1t.
  \]
\end{proposition}
\begin{proof}
  \uses{def:lubell_frame, def:n_frame, def:M_t}
  Fix $I\subseteq T\subseteq [t]$ with $i:=|I|$ and $z:=|T\setminus I|$.
  A support pattern of size $r+1$ contributes when it chooses one element of $I$ and $r$ elements of $T\setminus I$.
  Using the beta-integral identity
  $1/\binom{t-1}{r} = t\int_0^1 x^r{(1-x)}^{t-1-r}\,dx$,
  one computes
  $\omega_{\mathcal{L}_t}(T,I)=iM_t\cdot z/(t-z)$.
  Since $i\le t-z$, this is at most $zM_t$.
  The size formula follows from
  $|\mathcal{L}_t|=\sum_{j=2}^{t}\binom{t}{j}\frac{M_t}{\binom{t-1}{j-1}}
    =M_t\sum_{j=2}^{t}\frac{t}{j}
    =M_t\,t\,(h_t-1)$.
\end{proof}

The formal statement records the equivalent cardinality formula
\[
  |\mathcal{L}_t|=\sum_{j=2}^{t}\binom{t}{j}\frac{M_t}{\binom{t-1}{j-1}},
\]
which is then simplified in the paper to $M_t\,t\,(h_t-1)$.
The corresponding formal helpers name the multiplicity by \texttt{HypergraphLowerBound.lubellMultiplicity}, the constant-capacity vector by \texttt{HypergraphLowerBound.lubellCap}, and the displayed cardinality expression by \texttt{HypergraphLowerBound.lubellCardSum}.

\begin{proposition}\label{prop:digit_sum}
  \lean{HypergraphLowerBound.digit_sum_formula}
  \leanok%
  \uses{def:k_n}
  Let $s_2(m)$ denote the sum of the binary digits of $m$.
  Then for every $n\ge 1$,
  \[
    k_n=n+\sum_{j=0}^{n-1}s_2(j).
  \]
\end{proposition}
\begin{proof}
  \uses{def:k_n}
  Set $k_0:=0$ and $\Delta_n:=k_n-k_{n-1}$ for $n\ge 1$.
  From the recurrence, $\Delta_{2m}=1+\Delta_m$ and $\Delta_{2m+1}=\Delta_{m+1}$.
  Define $a_n:=1+s_2(n-1)$; the same binary-digit argument gives $a_{2m}=1+a_m$ and $a_{2m+1}=a_{m+1}$, with $a_1=1=\Delta_1$.
  Therefore $\Delta_n=a_n$ for all $n$, and summing yields $k_n=n+\sum_{j=0}^{n-1}s_2(j)$.
\end{proof}

The source file \texttt{frontier.tex} packages the additional asymptotic estimate
\[
  \lim_{n\to\infty}\frac{k_n}{n\log_2 n}=\frac12
\]
with this exact identity. Its proof continues with the doubling identity for
$f(n):=\sum_{j=0}^{n-1}s_2(j)$ and a squeeze argument on dyadic intervals.
In the accompanying formalization the exact formula is isolated as \texttt{HypergraphLowerBound.digit_sum_formula}, with the prefix sum itself named \texttt{HypergraphLowerBound.digitSumPrefix}; these digit-sum estimates are then used directly in the formal asymptotic arguments.

\begin{theorem}\label{thm:fixed_t}
  \lean{HypergraphLowerBound.fixed_t_bound}
  \leanok%
  \uses{prop:lubell, cor:frame_recurrence, def:H_n}
  Fix $t\ge 2$.
  There exists a constant $C_t>0$ such that
  \[
    H(n)\ge \frac{h_t-1}{\log_2 t}\,n\log_2 n - C_t n
    \qquad\text{for all }n\ge 1.
  \]
\end{theorem}
\begin{proof}
  \uses{prop:lubell, cor:frame_recurrence}
  Fix $t$, set $M:=M_t$ and $B:=|\mathcal{L}_t|=Mt(h_t-1)$.
  Define $L^{(t)}_n$ recursively by $L^{(t)}_1:=1$, and for $n\ge 2$,
  using the balanced $t$-way partition and $q:=\lfloor\lfloor n/t\rfloor/M\rfloor$ copies of $\mathcal{L}_t$.
  Since $qM\le p_i$ for every part $p_i$, $q$ copies form a legal frame.
  By Corollary~\ref{cor:frame_recurrence}, $H(n)\ge L^{(t)}_n$.
  An induction using $\sum p_i\log_2 p_i\ge n\log_2(n/t)$ and $qB=(h_t-1)n+O_t(1)$
  yields $L^{(t)}_n\ge a_t n\log_2 n - C_t n$ with $a_t=(h_t-1)/\log_2 t$.
  In the formal proof this argument is carried out first for an auxiliary explicit-witness extremal quantity and then compared to $H(n)$.
  The coefficient $a_t$ is packaged there as \texttt{HypergraphLowerBound.fixedTCoeff}.
\end{proof}

\begin{theorem}\label{thm:asymptotic_proof}
  \lean{HypergraphLowerBound.asymptotic_lower_bound}
  \leanok%
  \uses{thm:fixed_t, prop:digit_sum, def:H_n, def:k_n}
  $\displaystyle\liminf_{n\to\infty}\frac{H(n)}{k_n}\ge 2\ln 2$.
\end{theorem}
\begin{proof}
  \uses{thm:fixed_t, prop:digit_sum}
  By Proposition~\ref{prop:digit_sum}, one obtains the upper bound $k_n\le \frac12 n\log_2 n + O(n)$ used in the formal proof.
  Fix $\varepsilon>0$ and choose $t$ so large that $2(h_t-1)/\log_2 t>2\ln 2 - \varepsilon$.
  Then Theorem~\ref{thm:fixed_t} gives $H(n)\ge ((h_t-1)/\log_2 t)n\log_2 n - O_t(n)$.
  Dividing by the explicit upper bound for $k_n$ and letting $n\to\infty$ yields the result since $\varepsilon$ was arbitrary.
\end{proof}