Lax Lean Archive

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

Finite ordered fingerprint budgets

Lax342547.FingerprintCounts · concepts/Lax342547/FingerprintCounts.lean · lax-342547

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

    Padding a fingerprint with absent entries injects all fingerprints of length at most L into words of length L over the raw alphabet with one extra symbol. Thus their number is at most (card U + 1)^L.

    Concept map
    1 concept; 10 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 bounded_list_count proven

    2 pad_injective proven

    3 pad_length proven

    4 pad_recovers proven

    Lean source view on GitHub

    1import Mathlib.Data.Fintype.BigOperators
    2import Mathlib.Data.List.Basic
    3
    4/-!
    5---
    6title: Finite ordered fingerprint budgets
    7type: lemma
    8---
    9Padding a fingerprint with absent entries injects all fingerprints of length at most L into words of length L over the raw alphabet with one extra symbol. Thus their number is at most (card U + 1)^L.
    10-/
    11
    12namespace Lax342547.FingerprintCounts
    13
    14
    15
    16noncomputable def pad {U : Type} (L : ℕ) (l : List U) : List (Option U) :=
    17 l.map some ++ List.replicate (L-l.length) none
    18
    19axiom pad_recovers {U : Type} (L : ℕ) (l : List U) : (pad L l).filterMap id = l
    20
    21axiom pad_injective {U : Type} (L : ℕ) : Function.Injective (pad (U := U) L)
    22
    23axiom pad_length {U : Type} (L : ℕ) (l : List U) (hl : l.length ≤ L) : (pad L l).length = L
    24
    25axiom bounded_list_count {U : Type} [Fintype U] (T : Finset (List U)) (L : ℕ)
    26 (hL : ∀ l ∈ T, l.length ≤ L) : T.card ≤ (Fintype.card U+1)^L
    27
    28end Lax342547.FingerprintCounts
    29
    Show ProofShow ProofShow ProofShow Proof
    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…