Proof of `Replacing near twins in a set system`
groundedproofs/Lax235315Proofs/ComponentProofs.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.
Description
Near-twin replacement satisfies the exact registered crossing-number definition.
Proof strategy
For each set, new crossings must have an endpoint in the symmetric difference. The successor map bounds the number charged to second endpoints. Apply the result to a representative of each set and take the finite supremum.
Attribution
Lemma 2.2 of Dreier–Kuske, arXiv:2602.14625v1. The component proof is ported from the existing local Welzl development at commit 44a44623.