Lax Lean Archive

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

Crossing counts are stable under membership changes

Lax235315.NearTwinStability · concepts/Lax235315/NearTwinStability.lean · lax-235315

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    If two membership sequences of equal length differ at k positions, the first crossing count is at most the second plus 2k. Interchanging the sequences gives the bound in the other direction. This is the local estimate behind Lemma 2.2 of Dreier–Kuske.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax235315.SequenceCrossings
    2
    3/-!
    4---
    5title: Crossing counts are stable under membership changes
    6type: lemma
    7---
    8If two membership sequences of equal length differ at k positions, the first
    9crossing count is at most the second plus 2k. Interchanging the sequences
    10gives the bound in the other direction. This is the local estimate behind
    11Lemma 2.2 of Dreier--Kuske.
    12
    13# Formalization notes
    14
    15No randomness or shatter-function bound is needed. Each changed position has
    16at most two incident consecutive pairs. For a list containing each vertex
    17once, Hamming distance is the size of the symmetric difference of the sets
    18on the listed vertices; that representation bridge is a separate obligation.
    19-/
    20
    21namespace Lax235315.NearTwinStability
    22open Lax235315.SequenceCrossings
    23
    24/-- Changing k membership positions increases the crossing count by at most 2k. -/
    25axiom crossings_le_add_twice_hamming (xs ys : List Bool)
    26 (h : xs.length = ys.length) :
    27 crossings xs ≤ crossings ys + 2 * hamming xs ys
    28
    29end Lax235315.NearTwinStability
    30
    Show Proof
    Formalization notes

    No randomness or shatter-function bound is needed. Each changed position has at most two incident consecutive pairs. For a list containing each vertex once, Hamming distance is the size of the symmetric difference of the sets on the listed vertices; that representation bridge is a separate obligation.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…