Repository navigation
Immerman–Vardi: FO(LFP) = P on ordered finite structures (ROADMAP landmark 10) #1211
Description
Tracking issue for ROADMAP landmark 10 (#1202, section Descriptive complexity and first-order reductions), opened by coordinator-claude-c4b0c164-20261023.
Target. On ordered finite structures, first-order logic with least fixed points defines exactly the polynomial-time properties. The machine side must be proved for actual native algorithms in both directions: an evaluator for FO(LFP) formulas with a polynomial-time certificate, and a definition of every polynomial-time native machine's acceptance in FO(LFP).
Context. Reuse the ordered first-order conventions in ROADMAP: FO(≤, BIT), {0, …, n−1} universes, and numeric predicates computed from the universe size. Also reuse the existing Fagin, Immerman–Szelepcsényi and NL infrastructure. Related characterizations are FO(TC) = NL, FO(DTC) = L, SO-Horn = P and FO = DLOGTIME-uniform AC⁰.
Process. Claim this issue and post an M0 design before any Lean: exact statements, source locators pinned from the source itself (Immerman, Descriptive Complexity; Vardi 1982), the reuse plan with "Existing notions considered", and the milestone split into PRs of about 1.5k lines or less.
Status: available.
Activity
SamuelSchlesinger commentedon Oct 26, 2026
Coordinator-codex-01a16ab8: claiming M0 design with worker audit_prerequisites under Samuel’s current frontier priority, alongside the refreshed-head duty already in flight. No competing claim/PR is present. The design will inspect actual FO/Fagin/ordered-reduction and native-machine APIs, pin primary locators, and give small native milestones before Lean.
A central scope condition is fixed-formula data complexity: polynomial degree may depend on the fixed formula/vocabulary. We will not promise polynomial combined formula/data evaluation, trust arbitrary input BIT tables, or define the machine class by logical definability. Both directions must reach actual native algorithms with explicit finite-structure encodings. The full Immerman–Vardi target and related ROADMAP directions remain intact; M0 is not a capturing-theorem claim.
SamuelSchlesinger commentedon Oct 26, 2026
Worker
audit_prerequisites, M0 only, source pinb0ee011a5e4628ace9585db47e11845f9764c89c. No #1211 Lean or source implementation. No competing LFP module/claim found in the inspected source/open-PR search.Exact target/conventions. For a FIXED finite relational vocabulary
vand ordered query K, proveLFPDefinable K ↔ K.encodedLanguage v ∈ Cslib.Complexity.P encStructure. The right side stays the existing native multi-tape definition of P. ReuseFO.Ordered.Structure(Fin n, n≥2), canonical computed ≤/BIT/0/1/max andQuery.encodedLanguagerejection of malformed tables/small universes.encStructure = encPair encUnary (encList encBits)already charges unary n and every relation-table bit;card_le_length_encStructurerules out a binary-n succinct-domain shortcut. For each fixed formula φ, construct a native evaluator with constants/degree depending on φ AND v. There is no promised polynomial combined formula/data evaluator.Primary locators checked (paraphrases). Immerman 1982, Theorem 1, p.147 states the ordered relational-calculus/LFP polynomial-time characterization. The 1999 book’s Chapter 4, “Inductive Definitions,” pp.57–66 is the relevant published chapter; the author’s 2015 draft has DIFFERENT pagination (Chapter4 starts75), which must not be mixed into citations. In Vardi1982’s author PDF, Theorem5 (PDFp5/proceedings141) gives fixed-point polynomial DATA versus exponential expression complexity; the ordered capture statement is separately in Remark2 (PDFp6/proceedings142). I read those scanned pages, not just a secondary summary. The full published book proof/theorem-number locator remains to be pinned before quoting it in an implementation PR.
Existing notions considered. Reuse Mathlib
FirstOrder.Languageterms/atoms/structures, localFOcombinators,Vocabulary/tuple indexing,FO.Orderedarithmetic/interpretations, the actual ordered fixed-FO checker (queryLanguage_mem_L), native PT/list-table primitives and P’s upstream-machine equivalence. Reuse Fagin’s ordered converse/power bounds and tableau layout facts, not ESO as a substitute machine class. I found no existing LFP syntax. The FO logspace checker does NOT itself give a logspace LFP evaluator: polynomial-size intermediate relations need explicit charged table storage.Small delivery sequence (each PR ≤about1500 lines, split further if needed).
Critical obligations remain real proofs: native encoded-input bit layout, positivity and completeness of transition clauses, finite-stage correctness and native resource bounds. Existing ESO tableau CONSTRAINT formulas may negate guessed tableau relations, so they cannot simply be relabeled as positive LFP. No circular recognition/evaluator hypothesis, clock-budget change or proxy class is proposed. New math/API gets outside review. This M0 neither completes #1211 nor changes the related ordered-NP/NL/FO-reduction ROADMAP scope.
SamuelSchlesinger commentedon Oct 26, 2026
M0 is preserved at6429236121; no #1211 Lean or implementation was started. Paused under Samuel’s #1226-only reallocation (587#6429076407), with the full native Immerman–Vardi objective intact.
SamuelSchlesinger commentedon Oct 27, 2026
Worker
worker-codex-descriptive-fixedpoint-20261027(authoring, delegated bycoordinator-codex-01a16ab8): active M0 design only, resuming and preserving the existing M0 under Samuel’s renewed descriptive-complexity direction. I am verifying current-main APIs and primary locators, adding the coordinated FO(TC)=NL route and bounded milestone contracts, then releasing pending independent review. No Lean, worktree or build in this pass; the user checkout is read/fetch only. Current source pin:fae94eee4dfef9829f1a9599edebf45eb60cfb97(cslib6ff325e870ed89f86be10515f0e7297fa5a32845).SamuelSchlesinger commentedon Oct 27, 2026
Worker
worker-codex-descriptive-fixedpoint-20261027: paused / released at M0 checkpoint under the authoritative priority correction. The relayed descriptive dispatch was stale; Samuel’s later #1226-only direction remains current. No Lean, worktree, build or PR was started. Preserve the earlier M0; the full native FO(LFP)=P objective stays open.Read-only refresh used main
fae94eee4dfef9829f1a9599edebf45eb60cfb97, cslib6ff325e870ed89f86be10515f0e7297fa5a32845, with current repository and matching-pin cslib instructions. Existing interfaces remainFO.Ordered.Structure/Query.encodedLanguage, fixedVocabulary, unary-n/full-tableencStructure, canonical numeric predicates and n≥2. CurrentPuses plainComputableInPolyTime; currentNLis the actual finite-state binary multi-tape NTM definition with every branch halting and every prefix bounded in visited work cells byc*(log₂(encoded length)+1). RecheckedqueryLanguage_mem_L,ConfigurationGraph.accepts_iff_reachable_bad_of_runsInSpace,fits_of_runsInSpace, native counter-program compilation,exists_decidesInSpace_complandcompl_mem_NL. None supplies an LFP/TC syntax or an unproved machine→FO graph interpretation.Primary-source refresh, labeled paraphrases. Immerman’s author reprint
query.pdf, PDFp2, Theorem1 gives relational-calculus-plus-LFP capture assuming total order. This author reprint is not a verified scan of the 1982 proceedings page; do not copy proceedings pagination into its locator.capture.pdf, PDFp14/Theorem4.5 gives P=(FO+LFP); PDFp6/Theorem3.1 gives NL=(FO+positive TC), with reflexive tuple closure defined immediately above it. The unrestricted-TC route must separately reuse native NL complementation. Inspected PDF SHA256s: queryf47e9e244634e413b2e5eb5c0183fa1e06150184ce9f0a6eaae92ef5fd204a6c; captured3790a48e149afafd8b2a25f9deddcb8d98f4c1e02f72f3c4cc8b89488fb0d64.Vardi1982, visually rechecked PDFp5/proceedings141, Theorem5 is fixed-point polynomial data versus exponential expression complexity. PDFp6/proceedings142, Remark2’s ordered capture uses YF⁺, explicitly a slight extension of YF allowing existential quantification over conjunctions of equalities with YF expressions. Preserve that qualification. SHA256
cf01452d82dc760a8363361dca3481493c1d72b02b868b5e9828ee26d78a0a89. Publisher metadata confirms the 1999 LFP chapter at pp.57–66 and TC chapter at pp.139–155; internal published-book theorem locators remain unchecked and must not be inferred from 2015 draft pagination.The TC duplicate search found no dedicated implementation issue/PR, so #1246 was created just before the correction. It preserves the full native FO(TC)=NL objective, exact reflexive semantics, encoding/space conventions and proposed ≤about1500-line milestones; it is now paused too, unreviewed and unimplemented. Shared proposed boundary: the ordered-completeness track owns actual machine→FO graph/input-bit interpretation; TC adds scoped syntax and a charged fixed-formula native evaluator; LFP retains positive syntax/monotonicity, n^r stage bound, charged relation tables and its separate native-P converse. ESO constraint formulas remain unsuitable as positive producer clauses without proof. No abstract/catalogue changes or validation claims. No further work is retained in this slot.
SamuelSchlesinger commentedon Oct 30, 2026
Non-author integration coordinator
/root/mathlib_cache_retry_1730: #1774 needs the two focused lint fixes in its review record before integration. The unchanged mathematical review and rendered-guide evidence are retained there. The native evaluator/converse follow-ups are coordinated separately; this foundational milestone does not close the broader objective.SamuelSchlesinger commentedon Oct 30, 2026
Non-author coordinator/session
codex-descriptive-fix-1774-1651: #1774's operator milestone and bounded lint repair are integrated at746c420f90ffceca479b42b75f65244e3bec3b0a, by normal fast-forward over0f50f86f. See the single validated coordinator-fix record for the two-line diff, independent structural/API classification and passing focused checks plus all six local gates. Fresh canonical CI passed all six gates at its verified synthetic context; #1774 actually landed asce6c4d4bat 2026-10-31 02:12:25 UTC, and the fixed covering main/cache publication is verified complete in the linked record. Authors retain #1780's migration and both child implementations; this does not take them over.746c420f90ffceca479b42b75f65244e3bec3b0a: validated coordinator-fix approval reuses the prior outside mathematical/API review and its book Chapter 9 access limitation. Both reported lint failures are repaired without changing public mathematical meanings. Fresh native CI 41157050905 passed all six gates; actual synthetic checkout/source identity is verified in the coordinator record.2f916390e86cbbd6a084724dfa68f529ebc57020, directly on feat(logic): add FO(LFP), tuple closure, and certified formula synthesis #1774: outside changes requested for the application-level tidy-to-plain cost proof migration. Native CI 41102642507 also fails inherited lint. The migration remains with the author; the evaluator's explicit table-growth bounds and regressions must be retained.3b14fa7c419de7e6e18d8656cb6f7601b8085cc7, directly on feat(logic): certify native polynomial-time FO(LFP) evaluation #1780: outside approval covers its tuple/encoding/Fagin-client layer and explicitly retains feat(logic): certify native polynomial-time FO(LFP) evaluation #1780's blocker. Native CI 41102683482 fails inherited lint.9d5caea2ba3a41e7ecaff51089d4031066cb3206, directly on feat(logic): preserve least fixed points under ordered tuple interpretations #1781: outside approval covers its native capture layer, while retaining the parent blocker. Native CI 41102784658 fails inherited lint.The three unchanged child-head native runs passed build/tests, failed inherited lint, and skipped the final aggregate/style/Init gates; their Guide and Comparator runs passed. They have not inherited the newly published parent fix. The preceding 01:23 UTC triage used strict attribute-disabled text merges of the four then-current cumulative heads against actual main
012a2e027817c3fe8d9516f20500ea2e0918a8e3and accepted #1837 tailfa5a5aa1b66a184fc7d87b17757fc03ac8f86fc4exited 0 with canonical, complete aggregates. No current text conflict was found; that does not replace final Lean validation. #1774 has landed with passing source and merge-group checks. Keep the author-owned #1780 migration separate, review its affected delta, validate exact revisions, and integrate parent-first with actual-main updates after each parent lands. Do not rerun or queue the unchanged failed source.The endpoint remains the agreed #1211 target: one uniform checked sentence and tuple width, actual native P, fixed finite relational vocabulary, canonical order/BIT on
Fin nwithn ≥ 2, and unary-cardinality/full-table inputs. This is readiness triage, not a new mathematics approval. No selected abstract/catalogue changed. The existing exact-head Guide/rendering check remains reusable where repairs preserve its claims and declaration targets. #1211 stays open until the complete agreed endpoint lands; the operator-only parent does not complete it. Preserve #1768's independent roadmap directions.