Lax Lean Archive

The Explicit Construction Runs in Polynomial Time

Lax920634.PolynomialConstruction · concepts/Lax920634/PolynomialConstruction.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

    The specified graph-table constructor is computed by one deterministic Turing machine in polynomial time in the unary requested order. Its output is exactly the graph encoding defined by the seed scan, tower recurrence, level selector, and path replacement.

    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
    2import Mathlib.Computability.TuringMachine.Computable
    3
    4/-!
    5---
    6title: The Explicit Construction Runs in Polynomial Time
    7type: lemma
    8---
    9The specified graph-table constructor is computed by one deterministic
    10Turing machine in polynomial time in the unary requested order. Its output
    11is exactly the graph encoding defined by the seed scan, tower recurrence,
    12level selector, and path replacement.
    13
    14# Formalization notes
    15
    16The model is mathlib's deterministic finite stack-machine model, with the
    17identity encoding on binary input and output words. Its polynomial bound
    18counts machine transitions. The theorem concerns the actual specified
    19function, rather than an arbitrary constructor of graphs with similar
    20properties. Fixed seed precomputation contributes a constant independent
    21of the requested order.
    22-/
    23
    24namespace Lax920634.PolynomialConstruction
    25
    26open GraphEncoding Turing
    27
    28/-- One deterministic polynomial-time machine computes the specified graph constructor. -/
    29axiom polynomial_time :
    30 Nonempty (TM2ComputableInPolyTime id id construct)
    31
    32end Lax920634.PolynomialConstruction
    33
    Show Proof
    Formalization notes

    The model is mathlib's deterministic finite stack-machine model, with the identity encoding on binary input and output words. Its polynomial bound counts machine transitions. The theorem concerns the actual specified function, rather than an arbitrary constructor of graphs with similar properties. Fixed seed precomputation contributes a constant independent of the requested order.

    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…