Random graph model for girth

import Mathlib

set_option autoImplicit false

namespace BookSixth

/-- Unordered distinct-vertex pairs as edge slots for random graphs. -/
abbrev edgeSlots (n : Nat) := {p : Prod (Fin n) (Fin n) // p.1 < p.2}

/-- Order two distinct vertices into a slot. -/
def slotOf {n : Nat} (u v : Fin n) (h : Ne u v) : edgeSlots n :=
  if hlt : u < v then Subtype.mk (u, v) hlt
  else Subtype.mk (v, u) ((lt_or_gt_of_ne h).resolve_left hlt)

/-- Cyclic successor on Fin l (wraps around), for cycle indexing. -/
def cycSucc {l : Nat} (hl : 0 < l) (i : Fin l) : Fin l :=
  Fin.mk ((i.val + 1) % l) (by apply Nat.mod_lt; exact hl)

/-- G(n,p) weight: independent per-slot Bernoulli product. -/
noncomputable def graphWeight (n : Nat) (p : Real) (b : edgeSlots n -> Bool) : Real :=
  Finset.prod Finset.univ (fun s => if b s then p else 1 - p)

/-- Cycle edges of a vertex map: consecutive pairs ordered into slots. -/
noncomputable def cycleEdges {n l : Nat} (v : Fin l -> Fin n)
    (hinj : Function.Injective v) (hl3 : Nat.le 3 l)
    (hne : forall i : Fin l, Ne (cycSucc (lt_of_lt_of_le (by norm_num) hl3) i) i) :
    Finset (edgeSlots n) :=
  have hpos : 0 < l := lt_of_lt_of_le (by norm_num) hl3
  Finset.image (fun i : Fin l => slotOf (v i) (v (cycSucc hpos i))
    (fun hcon => absurd (hinj hcon) (Ne.symm (hne i)))) Finset.univ

end BookSixth