A Lean 4 formalization of sharp connectivity windows for friends-and-strangers graphs with an Erdős–Rényi friendship graph. The main result is a complete proof of the sharp threshold for m-vertex hereditary connectivity in G(n, p): for fixed m ≥ 3 and p = 1 − q, the probability that every induced subgraph on m vertices is connected tends to exp(−c^(m−1)/(m−1)!) when q = c·n^(−m/(m−1)), to 1 in the subcritical regime q = o(n^(−m/(m−1))), and to 0 in the supercritical regime q = ω(n^(−m/(m−1))). The proof formalizes the forbidden complete bipartite subgraph characterization in the complement, the first moment method via union bounds over K_{a,m−a} copies, the Poisson convergence of degree-(m−1) vertices through factorial moment computation, and the second moment method for the supercritical case. Applications to lollipop, dandelion, cycle, and K_{2,n−2} base graphs are derived from known deterministic criteria.

The formalization comprises six files totaling ~1,800 lines of Lean 4 with Mathlib. Defs.lean defines the FS graph and proves the path criterion (FS(P_n, Y) connected iff Y = K_n) via a relative-order invariant argument. ForbiddenBipartite.lean gives a complete proof of the equivalence between hereditary connectivity and the absence of complete bipartite subgraphs in the complement, using walk induction and connected component extraction. ErdosRenyi.lean builds a G(n,p) probability framework including total probability, complement symmetry, union bounds, and a first moment bound connecting event probabilities to expected subgraph counts. HereditaryThreshold.lean proves all three regimes of Theorem 3.1, with the critical window following from the star obstruction count converging to c^(m−1)/(m−1)! and non-star obstructions vanishing. CycleBase.lean and K2Base.lean handle the cycle and complete bipartite base graphs, reducing to classical random graph results (forest probability limits and Erdős–Rényi connectivity) that are accepted as explicit hypotheses on the downstream theorems.