Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax979537.FixedPointEvaluation

Polynomial-time evaluation of fixed-point queries

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    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.

    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

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…