A union-find connectivity check for ordered cores #

ExplicitPotential.Core.connectedCheck (Utilities/Subdivision/SubdivisionConnectivity.lean) decides ExplicitPotential.Core.Connected by enumerating all 2ⁿ vertex subsets and looking for a crossing slot in each. That is the definition read literally, and it is exact, but it makes every kernel-checked connectivity fact cost exponentially in the number of core vertices.

This file gives the same information for the price of a union--find fold. The partition machinery is already present: compFold core F is the canonical representative map obtained by contracting the slots of F, and compFold_iff says compFold-equality is reachability (Utilities/Subdivision/ContractionForestCensusGeneral.lean). Taking F = Finset.univ, a core is connected exactly when that map is constant.

Measured #

At n = 8, p = 12 (the genus-five atlas), on the sixteen Atanasov--Ranganathan rows, by decide +kernel:

check	per core
`connectedCheck` (`2⁸ = 256` subsets × `8² + 12` tests)	0.54 s
`connectedCheckFast` (one fold, `8²` comparisons)	0.01 s

a factor of about fifty, measured back-to-back in one batch and reproduced. The genus-five library performed twenty-nine such checks, so this is about fifteen seconds of kernel time, ten of it on the critical path (GenusFiveCoreAtlas → GenusFiveCubicAtlas). The saving grows with n: genus six classifies sixty-six cores at n = 10, where the old checker enumerates 1024 subsets.

What is proved #

connectedCheckFast_eq_true_iff is a genuine iff, so this is a drop-in replacement for connectedCheck_eq_true_iff and not merely a sufficient condition. The forward direction is the one every call site uses; the converse is here so that a reader does not have to wonder whether the cheap check is also complete. Neither checker is removed: connectedCheck remains the literal reading of the definition and stays available as an independent cross-check.

source

theorem Utilities.Certificate.ExplicitPotential.Core.mem_iff_of_reachIn {n p : ℕ} {core : Core n p} {F : Finset (Fin p)} {S : Finset (Fin n)} (hNoCrossing : ∀ e ∈ F, core.tail e ∈ S ↔ core.head e ∈ S) {x y : Fin n} (hReach : ContractionForestCensusGeneral.ReachIn core F x y) :

x ∈ S ↔ y ∈ S

Membership in a vertex cut is constant along reachability through F, provided no slot of F crosses the cut. This is the only graph-theoretic content of the checker: a reach path that leaves S must cross it.

source