Lax Lean Archive

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

Crossings along a finite membership sequence

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

definition

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

    Definition

    For a set and a listed order of vertices, write down whether each vertex belongs to the set. Its crossing count is the number of changes between consecutive entries. For two sequences of the same length, their Hamming distance is the number of positions with different entries.

    Concept map
    1 concept; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Data.List.Basic
    2
    3/-!
    4---
    5title: Crossings along a finite membership sequence
    6type: definition
    7---
    8For a set and a listed order of vertices, write down whether each vertex
    9belongs to the set. Its crossing count is the number of changes between
    10consecutive entries. For two sequences of the same length, their Hamming
    11distance is the number of positions with different entries.
    12
    13# Formalization notes
    14
    15Boolean entries are the actual membership data manipulated by an algorithm.
    16These definitions do not assert that the vertex list is a permutation; that
    17is a separate invariant when this representation is used for an order.
    18The Hamming-distance recursion is used only on equal-length lists.
    19-/
    20
    21namespace Lax235315.SequenceCrossings
    22
    23/-- The number of changes between consecutive membership bits. -/
    24def crossings : List Bool → ℕ
    25 | [] => 0
    26 | [_] => 0
    27 | a :: b :: rest => (if a = b then 0 else 1) + crossings (b :: rest)
    28
    29/-- The number of disagreeing positions of two equal-length membership lists. -/
    30def hamming : List Bool → List Bool → ℕ
    31 | a :: rest, b :: rest' => (if a = b then 0 else 1) + hamming rest rest'
    32 | _, _ => 0
    33
    34end Lax235315.SequenceCrossings
    35
    Formalization notes

    Boolean entries are the actual membership data manipulated by an algorithm. These definitions do not assert that the vertex list is a permutation; that is a separate invariant when this representation is used for an order. The Hamming-distance recursion is used only on equal-length lists.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…