Lax Lean Archive

Binary encoding of finite words

Lax759944.BinaryWordEncoding · concepts/Lax759944/BinaryWordEncoding.lean · lax-759944

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

    A finite list of natural numbers is encoded over a three-symbol alphabet. Each number begins with a separator and is followed by its canonical least-significant-bit-first binary expansion. Thus zero is represented by a separator with no following bits, and the next separator begins the next number. The empty list is represented by the empty string.

    This encoding is self-delimiting at the level of numbers: separators cannot occur as binary digits. Its length is the common input-size measure used by the Turing-machine and word-RAM polynomial-time definitions in this submission.

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

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Bits
    2import Mathlib.Data.Fintype.Basic
    3import Mathlib.Tactic.DeriveFintype
    4
    5/-!
    6---
    7title: Binary encoding of finite words
    8type: definition
    9---
    10A finite list of natural numbers is encoded over a three-symbol alphabet.
    11Each number begins with a separator and is followed by its canonical
    12least-significant-bit-first binary expansion. Thus zero is represented by a
    13separator with no following bits, and the next separator begins the next
    14number. The empty list is represented by the empty string.
    15
    16This encoding is self-delimiting at the level of numbers: separators cannot
    17occur as binary digits. Its length is the common input-size measure used by
    18the Turing-machine and word-RAM polynomial-time definitions in this
    19submission.
    20-/
    21
    22-- Preserve definition unfolding in the generated Fintype instance.
    23set_option backward.isDefEq.respectTransparency false
    24
    25namespace Lax759944.BinaryWordEncoding
    26
    27/-- The finite alphabet used to encode lists of natural numbers. -/
    28inductive Symbol
    29 | separator
    30 | zero
    31 | one
    32 deriving DecidableEq, Fintype, Inhabited
    33
    34/-- Encode one natural number, including the separator which begins it. -/
    35def encodeNat (n : ℕ) : List Symbol :=
    36 .separator :: n.bits.map (fun b => if b then .one else .zero)
    37
    38/-- The canonical binary encoding of a finite list of natural numbers. -/
    39def encode (x : List ℕ) : List Symbol :=
    40 x.flatMap encodeNat
    41
    42/-- The bit-size of a finite list of natural numbers. -/
    43def bitSize (x : List ℕ) : ℕ :=
    44 (encode x).length
    45
    46end Lax759944.BinaryWordEncoding
    47
    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…