Charging reverse extensions to disjoint configurations

Give each selected boundary vertex of a processed configuration four units of credit, and each selected center one. Reversing a configuration removes its credits. They pay for at most four new vertices, without selecting a center of an earlier configuration. The resulting potential telescopes over the entire normalization sequence.

noncomputable def Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.charge {W : Type} (B P X : Finset W) : ℕ

Size plus the credits attached to selected boundary vertices and centers.

Equations

• Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.charge B P X = X.card + 4 * (X ∩ B).card + (X ∩ P).card

theorem Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.charge_empty {W : Type} (X : Finset W) : charge ∅ ∅ X = X.card

theorem Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.charge_mono {W : Type} {B D P Q X : Finset W} (hBD : B ⊆ D) (hPQ : P ⊆ Q) : charge B P X ≤ charge D Q X

theorem Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.charge_le_five {W : Type} {B P : Finset W} (disjoint : Disjoint B P) (X : Finset W) : charge B P X ≤ 5 * X.card

theorem Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.charge_restore_center {W : Type} {B P T X Y : Finset W} {a b : W} (fresh : a ∉ P) (selected : a ∈ X) (hbB : b ∉ B) (hbP : b ∉ P) (support : Y ⊆ insert b X) : charge B P Y ≤ charge (T ∪ B) (insert a P) X

Selecting the missing boundary endpoint costs one vertex, paid for by the selected center whose configuration is being reversed.

theorem Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.charge_restore_boundary {W : Type} {B P T X Y : Finset W} {a b c : W} (haB : a ∉ B) (haP : a ∉ P) (hcB : c ∉ B) (hcP : c ∉ P) (separate : Disjoint T B) (interior : Disjoint T P) (selected : b ∈ X) (hb : b ∈ T) (size : Y.card ≤ X.card + 4) (support : Y ⊆ insert c (insert a (X ∪ T))) : charge B P Y ≤ charge (T ∪ B) (insert a P) X

A selected boundary endpoint supplies four credits. All added vertices are outside earlier configurations, so they require no further credit.