A union-find two-edge-connectivity check for ordered cores

ExplicitPotential.Core.twoEdgeConnectedCheck (Utilities/Subdivision/SubdivisionTwoEdgeCut.lean:190) decides ExplicitPotential.Core.TwoEdgeConnected by enumerating all 2ⁿ vertex subsets and counting the slots that cross each one. That is the definition read literally, and it is exact, but it makes every kernel-checked two-edge-connectivity fact cost exponentially in the number of core vertices. It is the same shape Utilities/Subdivision/ConnectedCheckFast.lean was written to replace for plain connectedness, and it was left behind there.

This file gives the same information for the price of p + 1 union--find folds. The reading is the standard one: a core is two-edge connected exactly when it is connected and deleting any single slot leaves it connected. Deleting a slot needs no new datum, because compFold core F already takes an arbitrary slot set: compFold core (Finset.univ.erase e) is the component map of the core with slot e removed.

Why the connectivity conjunct is not redundant

Dropping connectedCheckFast makes the checker wrong at p = 0: the two-vertex edgeless core Core 2 0 has Finset.univ.erase e vacuously constant (there is no e), so the fold condition holds, while the core is not even connected. For p ≥ 1 the fold condition alone does imply connectedness, but the conjunction is the honest statement and costs one extra fold.

Measured

At n = 8, p = 12 (the genus-five atlas), on the sixteen Atanasov--Ranganathan rows, by decide +kernel, measured back-to-back in one batch and reproduced:

check	sixteen cores
twoEdgeConnectedCheck (2⁸ = 256 subsets × a Fin 12 filter each)	12.6 s
twoEdgeConnectedCheckFast (13 folds of 8² comparisons)	1.95 s

The saving grows with n: the old checker doubles per core vertex, the new one grows linearly in n · p.

What is proved

twoEdgeConnectedCheckFast_eq_true_iff is a genuine iff, so this is a drop-in replacement for twoEdgeConnectedCheck_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: twoEdgeConnectedCheck remains the literal reading of the definition and stays available as an independent cross-check.

@[reducible, inline]

abbrev Utilities.Certificate.ExplicitPotential.Core.without {p : ℕ} (e : Fin p) : Finset (Fin p)

The slot set that survives deleting e.

Equations

• Utilities.Certificate.ExplicitPotential.Core.without e = Finset.univ.erase e

def Utilities.Certificate.ExplicitPotential.Core.twoEdgeConnectedCheckFast {n p : ℕ} (core : Core n p) : Bool

The union--find two-edge-connectivity checker. A core is two-edge connected exactly when it is connected and every single-slot deletion still leaves one class.

Equations

• One or more equations did not get rendered due to their size.

theorem Utilities.Certificate.ExplicitPotential.Core.twoEdgeConnected_of_twoEdgeConnectedCheckFast {n p : ℕ} {core : Core n p} (hCheck : core.twoEdgeConnectedCheckFast = true) : core.TwoEdgeConnected

The direction every call site uses.

@[simp]

theorem Utilities.Certificate.ExplicitPotential.Core.twoEdgeConnectedCheckFast_eq_true_iff {n p : ℕ} (core : Core n p) : core.twoEdgeConnectedCheckFast = true ↔ core.TwoEdgeConnected

The cheap checker is exact, not merely sufficient.