Lax Lean Archive

Sizes of encodings and the reduction graph

Lax689614.Sizes · concepts/Lax689614/Sizes.lean · lax-689614

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

    Theorem

    The graph encoding has n2+n+1n^2+n+1 bits. The formula encoding has mn+n+m+2mn+n+m+2 bits, where nn and mm are its variable and clause counts. The reduction graph has exactly 13n+4m+1813n+4m+18 vertices. These bounds account explicitly for the unary size prefixes and incidence matrices; they are separate from the running-time proof of the reduction.

    Concept map
    6 concepts
    100%
    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.

    1 construction_size proven

    2 formula_length proven

    3 graph_length proven

    Lean source view on GitHub

    1import Lax689614.Construction
    2
    3/-!
    4---
    5title: Sizes of encodings and the reduction graph
    6type: theorem
    7---
    8The graph encoding has n2+n+1n^2+n+1 bits. The formula encoding has
    9mn+n+m+2mn+n+m+2 bits, where nn and mm are its variable and clause counts.
    10The reduction graph has exactly 13n+4m+1813n+4m+18 vertices.
    11These bounds account explicitly for the unary size prefixes and incidence
    12matrices; they are separate from the running-time proof of the reduction.
    13-/
    14
    15namespace Lax689614.Sizes
    16
    17axiom graph_length (G : Encoding.Graph) :
    18 (Encoding.graphWord G).length = G.vertices ^ 2 + G.vertices + 1
    19
    20axiom formula_length (φ : PositiveCNF.Formula) :
    21 (Encoding.formulaWord φ).length =
    22 φ.clauses.length * φ.nvars + φ.nvars + φ.clauses.length + 2
    23
    24axiom construction_size (φ : PositiveCNF.Formula) :
    25 Construction.size φ = 13 * φ.nvars + 4 * φ.clauses.length + 18
    26
    27end Lax689614.Sizes
    28
    Show ProofShow ProofShow Proof
    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…