Lax Lean Archive

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

Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.

Polynomial-time evaluation of fixed-point queries

Lax979537.FixedPointEvaluation · concepts/Lax979537/FixedPointEvaluation.lean · lax-979537

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

    Every fixed FO(LFP) formula can be evaluated in polynomial time on finite ordered structures, including the assignment to its free variables. This is data complexity: the machine and polynomial may depend on the formula. The formula is not part of the machine's input.

    The proof must implement first-order evaluation and relation-table iteration on the concrete Turing-machine model. Finite convergence alone does not discharge this computational obligation.

    Concept map
    7 concepts; 1 descendant hidden
    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 Lax979537.FixedPointSemantics
    2import Lax979537.PolynomialTime
    3
    4/-!
    5---
    6title: Polynomial-time evaluation of fixed-point queries
    7type: theorem
    8---
    9Every fixed FO(LFP) formula can be evaluated in polynomial time on finite
    10ordered structures, including the assignment to its free variables.
    11This is data complexity: the machine and polynomial may depend on the
    12formula. The formula is not part of the machine's input.
    13
    14The proof must implement first-order evaluation and relation-table iteration
    15on the concrete Turing-machine model. Finite convergence alone does not
    16discharge this computational obligation.
    17-/
    18
    19namespace Lax979537.FixedPointEvaluation
    20
    21open Lax979537.OrderedStructures Lax979537.FixedPointSyntax
    22open Lax979537.FixedPointSemantics Lax979537.PolynomialTime
    23
    24axiom evaluationInP {σ : Vocabulary} {k : Nat} (φ : Formula σ k) :
    25 InP (fun A => Satisfies A φ)
    26
    27end Lax979537.FixedPointEvaluation
    28
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…