While this submission is a draft, it cannot be used by other submissions.

Proof of `Crossing counts are stable under membership changes`

groundedproofs/Lax235315Proofs/Crossings.lean · lax-235315

What this proof establishes

no assumptions

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Changing membership at k positions changes the crossing count by at most 2k.

Proof strategy

A strengthened induction charges the first position once and each remaining position at most twice. Each edge changes only when one of its endpoint bits changes, so every changed position is charged at most twice overall.

Attribution

This is the elementary membership-sequence estimate in Lemma 2.2 of Dreier and Kuske, Near-Linear Time Computation of Welzl Orders on Graphs with Linear Neighborhood Complexity.