The uniform 26/25 factor and the finite bootstrap

structure HypergraphLowerBound.Witness (edgeCount vertexCount : ℕ) : Type

A concrete witness hypergraph with prescribed edge and vertex counts.

• edges : Hypergraph ℕ

  The witness hypergraph.

• edgeCard : Finset.card self.edges = edgeCount

  The witness has the prescribed number of edges.

• vertexCard : (vertexSet self.edges).card = vertexCount

  The witness has the prescribed number of vertices.

• noLargePartition : NoLargePartition self.edges edgeCount

  The witness satisfies the no-large-partition obstruction.

structure HypergraphLowerBound.WitnessFamily (G : ℕ → Hypergraph ℕ) : Prop

A packaged witness family for the sequence-level form of the main theorem.

• edgeCard (n : ℕ) : 1 ≤ n → Finset.card (G n) = n
• noLargePartition (n : ℕ) : 1 ≤ n → NoLargePartition (G n) n
• lowerBoundWitness (n : ℕ) : 15 ≤ n → 25 * (vertexSet (G n)).card ≥ 26 * k n
• lowerBoundH (n : ℕ) : 15 ≤ n → 25 * H n ≥ 26 * k n

Four-way identities for k_n

theorem HypergraphLowerBound.k_four_way (m : ℕ) (hm : 1 ≤ m) : k (4 * m) = 4 * k m + 4 * m ∧ k (4 * m + 1) = 3 * k m + k (m + 1) + 4 * m ∧ k (4 * m + 2) = 2 * k m + 2 * k (m + 1) + 4 * m + 1 ∧ k (4 * m + 3) = k m + 3 * k (m + 1) + 4 * m + 2

The four-way identities satisfied by k_n.

The floor inequalities

theorem HypergraphLowerBound.floor_26_25 (m : ℕ) (hm : 15 ≤ m) : 25 * eBonus 0 m ≥ 26 * (4 * m) ∧ 25 * eBonus 1 m ≥ 26 * (4 * m) ∧ 25 * eBonus 2 m ≥ 26 * (4 * m + 1) ∧ 25 * eBonus 3 m ≥ 26 * (4 * m + 2)

The bonus e_r(m) ≥ (26/25) × (additive term) for m ≥ 15.

The finite bootstrap

theorem HypergraphLowerBound.bootstrap_26_25 (n : ℕ) (h1 : 15 ≤ n) (h2 : n < 60) : 25 * A n ≥ 26 * k n ∧ (25 * A n = 26 * k n ↔ n = 17)

For 15 ≤ n < 60, 25 * A_n ≥ 26 * k_n, with equality exactly at n = 17.

Unfolding A for large n

The main uniform bound

theorem HypergraphLowerBound.uniform_26_25 (n : ℕ) (hn : 15 ≤ n) : 25 * A n ≥ 26 * k n

For all n ≥ 15, 25 * A_n ≥ 26 * k_n, i.e. A_n ≥ (26/25) k_n.

theorem HypergraphLowerBound.H_set_bddAbove (n : ℕ) : BddAbove {k : ℕ | ∃ (edges : Finset (Finset ℕ)), (vertexSet edges).card = k ∧ NoLargePartition edges n}

The set defining H(n) is bounded above.

Witness construction helpers

Standalone intermediate witnesses

Replication helpers for the recursive case

The main witness strength theorem

theorem HypergraphLowerBound.A_witness (n : ℕ) (hn : 1 ≤ n) : ∃ (edges : Finset (Finset ℕ)), edges.card = n ∧ (vertexSet edges).card = A n ∧ NoLargePartition edges n

A(n) is realized by a concrete hypergraph with n edges, A(n) vertices, and NoLargePartition.

theorem HypergraphLowerBound.constructive_An (n : ℕ) (hn : 1 ≤ n) : ∃ (edges : Finset (Finset ℕ)), edges.card = n ∧ (vertexSet edges).card = A n ∧ NoLargePartition edges n

For every n ≥ 1 there exists a hypergraph with exactly n distinct edges, no partition of size greater than n, and exactly A n vertices.

In this edge-set encoding, the "no isolated vertices" clause from the paper is implicit because vertexSet is defined as the union of the edges.

theorem HypergraphLowerBound.A_le_H (n : ℕ) (hn : 1 ≤ n) : A n ≤ H n

A(n) ≤ H(n) for n ≥ 1: the constructive witness shows H(n) is at least A(n).

theorem HypergraphLowerBound.thm_main_pointwise (n : ℕ) (hn : 1 ≤ n) : ∃ (edges : Finset (Finset ℕ)), edges.card = n ∧ (vertexSet edges).card = A n ∧ NoLargePartition edges n ∧ (15 ≤ n → 25 * (vertexSet edges).card ≥ 26 * k n)

Pointwise witness form of Theorem thm:main from frontier.tex.

For each n ≥ 1, the explicit construction gives a hypergraph with exactly n distinct edges, no partition of size greater than n, and exactly A n vertices. When n ≥ 15, this witness has at least (26/25) k n vertices. As above, "no isolated vertices" is implicit in the edge-set encoding.

theorem HypergraphLowerBound.thm_main : ∃ (G : ℕ → Hypergraph ℕ), WitnessFamily G

Formalization of Theorem thm:main from frontier.tex, packaged as a witness family.

The sequence is obtained by choosing, for each n ≥ 1, one witness from mainPointwiseWitness. As above, "no isolated vertices" is implicit in the edge-set encoding.

theorem HypergraphLowerBound.thm_main_H_lower_bound (n : ℕ) (hn : 15 ≤ n) : 25 * H n ≥ 26 * k n

The H(n) lower bound stated as the consequence of Theorem thm:main.