Transport of strong-separator certificates along a Laplacian equivalence

LaplacianEquiv already transports divisors, firing scripts, winnability, rank lower bounds, connectivity and BNExists. What it did not transport is the one remaining ingredient of the rank-one pipeline: the finite StrongSeparator.ExpansionCell data and the StrongSeparatorCertificate predicate assembled from it.

This file adds exactly that. Every field of ExpansionCell is phrased in numEdges and Finset membership, which is precisely the structure a LaplacianEquiv preserves, so the transport is a pure relabeling: no graph theory is redeveloped and no new hypothesis appears.

Why this is the load-bearing piece for the closed length orthant

A degenerate subdivision (Utilities.Certificate.DegenerateSpec.DegSpec) at a face of the length orthant is LaplacianEquiv to the strictly positive subdivision of the contracted core (DegSpec.Contraction.laplacianEquiv). The separator argument of Certificate/SubdivisionSeparator.lean rests on injectivity of Spec.pathVertex, which genuinely fails at a face — coreVertex is not injective there. Rather than redoing that argument in a setting where it is false, we run it on the contracted positive spec, where it applies verbatim, and pull the resulting certificate back along the equivalence.

Finset images along an equivalence

theorem Utilities.Certificate.StrongSeparator.mem_image_equiv_apply {α : Type u} {β : Type v} [DecidableEq β] (f : α ≃ β) (S : Finset α) (x : α) : f x ∈ Finset.image (⇑f) S ↔ x ∈ S

theorem Utilities.Certificate.StrongSeparator.mem_image_equiv {α : Type u} {β : Type v} [DecidableEq β] (f : α ≃ β) (S : Finset α) (y : β) : y ∈ Finset.image (⇑f) S ↔ f.symm y ∈ S

theorem Utilities.Certificate.StrongSeparator.mem_image_equiv_symm {α : Type u} {β : Type v} [DecidableEq α] (f : α ≃ β) (T : Finset β) (x : α) : x ∈ Finset.image (⇑f.symm) T ↔ f x ∈ T

theorem Utilities.Certificate.StrongSeparator.image_equiv_symm_image {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α ≃ β) (T : Finset β) : Finset.image (⇑f) (Finset.image (⇑f.symm) T) = T

theorem Utilities.Certificate.StrongSeparator.image_equiv_univ {α : Type u} {β : Type v} [DecidableEq β] [Fintype α] [Fintype β] (f : α ≃ β) : Finset.image (⇑f) Finset.univ = Finset.univ

theorem Utilities.Certificate.StrongSeparator.image_equiv_symm_ne_univ {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [Fintype β] (f : α ≃ β) {T : Finset β} (h : T ≠ Finset.univ) : Finset.image (⇑f.symm) T ≠ Finset.univ

The elementary quantities transport

theorem Utilities.Certificate.StrongSeparator.num_edges_toEquiv_symm {G : CFGraph} {H : CFGraph} (φ : LaplacianEquiv G H) (x y : H.V) : numEdges G (φ.toEquiv.symm x) (φ.toEquiv.symm y) = numEdges H x y

LaplacianEquiv.symm reading, with the equivalence written on the target side. Stated separately so rw finds it without unfolding symm.

theorem Utilities.Certificate.StrongSeparator.intoMultiplicity_image {G : CFGraph} {H : CFGraph} (φ : LaplacianEquiv G H) (C : Finset G.V) (v : G.V) : intoMultiplicity H (Finset.image (⇑φ.toEquiv) C) (φ.toEquiv v) = intoMultiplicity G C v

theorem Utilities.Certificate.StrongSeparator.isBoundary_image {G : CFGraph} {H : CFGraph} (φ : LaplacianEquiv G H) (C : Finset G.V) (v : G.V) : IsBoundary H (Finset.image (⇑φ.toEquiv) C) (φ.toEquiv v) ↔ IsBoundary G C v

Transport of an expansion cell

def Utilities.Certificate.StrongSeparator.ExpansionCell.map {G : CFGraph} {H : CFGraph} (φ : LaplacianEquiv G H) {R : Finset G.V} (cell : ExpansionCell G R) : ExpansionCell H (Finset.image (⇑φ.toEquiv) R)

Relabel a complementary cell along a Laplacian equivalence. Every field is a numEdges/membership statement, so nothing but the labels changes.

Equations

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

Transport of the certificate

theorem Utilities.Certificate.StrongSeparator.strongSeparatorCertificate_image {G : CFGraph} {H : CFGraph} (φ : LaplacianEquiv G H) {S : Finset G.V} (hSeparator : StrongSeparatorCertificate G S) : StrongSeparatorCertificate H (Finset.image (⇑φ.toEquiv) S)

The missing transport. A strong-separator certificate for S in G is a strong-separator certificate for the relabeled set in H.

theorem Utilities.Certificate.StrongSeparator.strongSeparatorCertificate_of_image {G : CFGraph} {H : CFGraph} (φ : LaplacianEquiv G H) {S : Finset G.V} {T : Finset H.V} (hT : Finset.image (⇑φ.toEquiv) S = T) (hSeparator : StrongSeparatorCertificate G S) : StrongSeparatorCertificate H T

The form used at a call site, where the relabeled separator has already been identified with a set named on the target side.