Lax Lean Archive

The Constructor Meets the Requested Order

Lax920634.ConstructionSize · concepts/Lax920634/ConstructionSize.lean · lax-920634

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

    For every requested order nn, the selector produces a graph with at least nn vertices and at most 2dD4(n+1)2dD^4(n+1) vertices. Thus the polynomial-time algorithm constructs arbitrarily large graphs with only a fixed-factor overshoot. Here D=1205760000D=120^{5760000} and d=D2d=D^2 are fixed.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax920634.GraphEncoding
    2
    3/-!
    4---
    5title: The Constructor Meets the Requested Order
    6type: lemma
    7---
    8For every requested order nn, the selector produces a graph with at least
    9nn vertices and at most 2dD4(n+1)2dD^4(n+1) vertices. Thus the polynomial-time
    10algorithm constructs arbitrarily large graphs with only a fixed-factor
    11overshoot. Here D=1205760000D=120^{5760000} and d=D2d=D^2 are fixed.
    12
    13# Formalization notes
    14
    15Both bounds concern the exact level used by the binary table constructor.
    16-/
    17
    18namespace Lax920634.ConstructionSize
    19
    20open ZigZagConstruction GraphEncoding SeedSearch
    21
    22/-- The specified size selector meets the request with a fixed linear upper bound. -/
    23axiom size_bounds (n : ℕ) :
    24 n ≤ order (selectedLevel n) ∧
    25 order (selectedLevel n) ≤
    26 (2 * degree * seedDegree ^ 4) * (n + 1)
    27
    28end Lax920634.ConstructionSize
    29
    Show Proof
    Formalization notes

    Both bounds concern the exact level used by the binary table constructor.

    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…