The finite-field halved-flag witness

This file packages the concrete halved flag graph over ZMod p into the abstract interface used by the asymptotic argument. Its vertices are the even partial flags in the recursively split (2*k+1)-dimensional space.

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.asymptoticHalvedWitness (k p : ℕ) (hk : 0 < k) (hp : Nat.Prime p) : AsymptoticHalvedWitness k p

For every positive k and prime p, the halved flag graph over ZMod p is a finite regular graph with the order, degree, and diameter bounds required by the asymptotic argument.

theorem MooreBound.DegreeDiameter.asymptoticHalvedWitnessHypothesis : AsymptoticHalvedWitnessHypothesis

The concrete finite-field construction implies the abstract prime-indexed interface used by the alternative downstream extremal-limit proof. The exact Proposition 3.1 theorem is exported separately.