Reduction of the asymptotic theorems to the prime-power graph construction

The weak downstream graph interface is isolated in AsymptoticHalvedWitness. The finite combinatorial lemmas in the first part of this file use no asymptotic or number-theoretic input. The second part supplies the analytic argument from primes in short multiplicative intervals.

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

noncomputable def MooreBound.DegreeDiameter.AsymptoticHalvedWitness (k p : ℕ) : Prop

The exact interface required from the halved flag-graph construction. The intentionally slightly weaker degree estimate (p+1)^(2*k) is the estimate proved directly by the construction and is all that the limiting arguments need.

Equations

• One or more equations did not get rendered due to their size.

def MooreBound.DegreeDiameter.AsymptoticHalvedWitnessHypothesis : Prop

A construction theorem in precisely the form consumed below.

Equations

• MooreBound.DegreeDiameter.AsymptoticHalvedWitnessHypothesis = ∀ (k p : ℕ), 0 < k → Nat.Prime p → MooreBound.DegreeDiameter.AsymptoticHalvedWitness k p

theorem MooreBound.DegreeDiameter.maxDegreeLE_of_regular {V : Type u_1} {G : SimpleGraph V} {Δ : ℕ} (hregular : ∀ (v : V), (G.neighborSet v).ncard = Δ) : MaxDegreeLE G Δ

theorem MooreBound.DegreeDiameter.construction_order_lower {k p d : ℕ} (hw : AsymptoticHalvedWitness k p) (hdegree : (p + 1) ^ (2 * k) ≤ d) : p ^ (2 * k * k) ≤ nKD k d

A single construction witness gives the required vertex-extremum lower bound at every admissible ambient degree.

theorem MooreBound.DegreeDiameter.base_power_le_regular_degree_add_one {k p : ℕ} (hk : 0 < k) {V : Type u_1} [Finite V] {G : SimpleGraph V} {Δ : ℕ} (horder : p ^ (2 * k * k) ≤ Nat.card V) (hregular : ∀ (v : V), (G.neighborSet v).ncard = Δ) (hdiam : G.ediam ≤ ↑k) : p ^ (2 * k) ≤ Δ + 1

theorem MooreBound.DegreeDiameter.construction_edge_lower {k p d : ℕ} (hk : 0 < k) (hw : AsymptoticHalvedWitness k p) (hdegree : (p + 1) ^ (2 * k) + 1 ≤ d) : p ^ (2 * k * (k + 1)) ≤ h (k + 1) d - 1

Applying Lemma 4.1 to a regular construction witness gives an admissible graph for the edge extremum, with the exact edge count needed in Corollary 1.2.