Lax Lean Archive

Polynomial-time evaluation of fixed-point queries

Lax751879.FixedPointEvaluation · concepts/Lax751879/FixedPointEvaluation.lean · lax-751879

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 Lax751879.FixedPointSemantics
    2import Lax751879.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 Lax751879.FixedPointEvaluation
    20
    21open Lax751879.OrderedStructures Lax751879.FixedPointSyntax
    22open Lax751879.FixedPointSemantics Lax751879.PolynomialTime
    23
    24axiom evaluationInP {σ : Vocabulary} {k : Nat} (φ : Formula σ k) :
    25 InP (fun A => Satisfies A φ)
    26
    27end Lax751879.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…