Corollary 1.2 directly from Proposition 3.1

This module follows Section 4 of the write-up. For k = ell - 1 it applies the bipartite expansion to the concrete graph in Proposition 3.1. The exact edge count is

|V(H)| * (proposition31PrimePowerDegree k q + 1),

Lemma 4.1 supplies line-graph diameter at most k + 1, and the two limits in equation (9) give the normalized lower bound. The proof records the paper's convention literally: the displayed edge count is first bounded by h ell d - 1, and only then by h ell d.

Lean Pool port of wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022. The port adds a namespace and adapts proofs to the current Mathlib APIs and repository style.

theorem MooreBound.DegreeDiameter.corollary_1_2_from_proposition_3_1 {ell : ℕ} (hell : 2 ≤ ell) : 1 ≤ Filter.liminf (fun (d : ℕ) => ↑(h ell d) / ↑d ^ ell) Filter.atTop

Corollary 1.2, directly from Proposition 3.1 and equation (9).