Proof of `Inserting a twin preserves crossings`
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.
Description
Duplicating a membership bit beside itself preserves the crossing count.
Proof strategy
Induct on the prefix. The duplicate creates no new change, and the crossing from the preceding bit to the duplicate is the same as the crossing to the original bit.
Attribution
The statement is the adjacent-twin crossing observation used in Lemma 2.1 of Dreier and Kuske, Near-Linear Time Computation of Welzl Orders on Graphs with Linear Neighborhood Complexity.