Complete form of Proposition 3.1

This module gives one declaration containing every finite and asymptotic clause of Proposition 3.1. The finite clauses retain the exact multiplication identity as well as its natural-division consequence. Both limits in equation (9) concern the same concrete prime-power graph and use its actual common degree, not merely the displayed upper bound.

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

structure MooreBound.DegreeDiameter.Proposition31FiniteClaims (q : PrimePowerIndex) (k : ℕ) : Prop

The finite claims of Proposition 3.1 for the concrete graph over the chosen field of cardinality q.

The named fields expose the five claims in the paper: regularity with the actual common degree, the exact order in multiplication and division form (equation (6)), the sharp degree cap (equation (7)), and exact extended diameter (equation (8)).

• regularity (P : Proposition31Vertex (PrimePowerField q) k) : Nat.card ↑((Proposition31Graph (PrimePowerField q) k).neighborSet P) = proposition31PrimePowerDegree k q

  The graph is regular of its actual common degree.

• order_mul : proposition31PrimePowerOrder k q * (↑q + 1) ^ k = qFactorial (↑q) (2 * k + 1)

  Equation (6), before taking natural-number division.

• order_eq : proposition31PrimePowerOrder k q = qFactorial (↑q) (2 * k + 1) / (↑q + 1) ^ k

  Equation (6), in the displayed natural-division form.

• degree_le_cap : proposition31PrimePowerDegree k q ≤ proposition31DegreeCap (↑q) k

  Equation (7), with the actual degree on the left.

• ediam_eq : (Proposition31Graph (PrimePowerField q) k).ediam = ↑k

  Equation (8), as equality of extended diameters.

theorem MooreBound.DegreeDiameter.proposition31_finite_claims (q : PrimePowerIndex) (k : ℕ) (hk : 0 < k) : Proposition31FiniteClaims q k

The finite part of Proposition 3.1, repackaged under a named proposition.

theorem MooreBound.DegreeDiameter.proposition_3_1 (k : ℕ) (hk : 0 < k) : (∀ (q : PrimePowerIndex), Proposition31FiniteClaims q k) ∧ Filter.Tendsto (fun (q : PrimePowerIndex) => ↑(proposition31PrimePowerDegree k q) / ↑(proposition31DegreeCap (↑q) k)) Filter.atTop (nhds 1) ∧ Filter.Tendsto (fun (q : PrimePowerIndex) => ↑(proposition31PrimePowerOrder k q) / ↑(proposition31PrimePowerDegree k q) ^ k) Filter.atTop (nhds 1)

Proposition 3.1 (complete formal statement).

For every prime-power field order, the concrete halved-flag graph satisfies all finite claims in equations (6)--(8). As the field order tends to infinity through all prime powers, its actual degree divided by the cap and its exact order divided by the k-th power of that actual degree both tend to one, as in equation (9).

theorem MooreBound.DegreeDiameter.proposition31_order_div_cap_pow_tendsto_one_from_proposition_3_1 (k : ℕ) (hk : 0 < k) : Filter.Tendsto (fun (q : PrimePowerIndex) => ↑(proposition31PrimePowerOrder k q) / ↑(proposition31DegreeCap (↑q) k) ^ k) Filter.atTop (nhds 1)

Consequence of the two asymptotic clauses of Proposition 3.1.

This is the exact algebraic bridge used in the proof of Theorem 1.1. It is proved from the bundled declaration proposition_3_1, rather than by invoking the independently available cap-normalized limit. Pointwise, after the nonzero denominators have been discharged, the identity is

N / K^k = (N / Δ^k) * (Δ / K)^k.