Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax434930.Certificates

Binary encoding of an input and a certificate

concepts/Lax434930/Certificates.lean · lax-434930

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

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

    1st statement pair_injective proven

    2nd statement pair_length proven

    3rd statement unpair_pair proven

    Definition

    To encode a pair (x,y)(x,y) of binary strings, replace each bit bb of xx by 0b0b, then append a single 11 followed by yy. This encoding has length 2∣x∣+∣y∣+12|x|+|y|+1 and has a unique decoding. In particular, a polynomial bound in the encoded length is a polynomial bound in the combined input and certificate lengths.

    Lean source view on GitHub

    1import Lax434930.PolynomialTime
    2
    3/-!
    4---
    5title: Binary encoding of an input and a certificate
    6type: definition
    7---
    8To encode a pair (x,y)(x,y) of binary strings, replace each bit bb of xx by
    90b0b, then append a single 11 followed by yy. This encoding has length
    102∣x∣+∣y∣+12|x|+|y|+1 and has a unique decoding. In particular, a polynomial bound in
    11the encoded length is a polynomial bound in the combined input and
    12certificate lengths.
    13-/
    14
    15namespace Lax434930.Certificates
    16
    17open PolynomialTime
    18
    19/-- A self-delimiting encoding of the first string, followed by the second. -/
    20def pair : Word → Word → Word
    21 | [], y => true :: y
    22 | b :: x, y => false :: b :: pair x y
    23
    24/-- Decode a pair, rejecting a missing delimiter or an incomplete bit block. -/
    25def unpair : Word → Option (Word × Word)
    26 | [] => none
    27 | true :: y => some ([], y)
    28 | false :: [] => none
    29 | false :: b :: rest => (unpair rest).map (fun p => (b :: p.1, p.2))
    30
    31/-- Encoding followed by decoding recovers both strings. -/
    32axiom unpair_pair (x y : Word) : unpair (pair x y) = some (x, y)
    33
    34/-- Distinct pairs of strings have distinct encodings. -/
    35axiom pair_injective : Function.Injective (fun p : Word × Word => pair p.1 p.2)
    36
    37/-- The encoding has linear length in its two arguments. -/
    38axiom pair_length (x y : Word) : (pair x y).length = 2 * x.length + y.length + 1
    39
    40end Lax434930.Certificates
    41
    Show ProofShow ProofShow Proof

    Builds on

    Used by

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…