[SamuelSchlesinger]

This completes the FO(LFP) = P construction requested in #1211. It is the top of the follow-up stack: #1774 supplies the checked operator syntax, #1780 proves native polynomial-time evaluation, and #1781 supplies tuple transport and exact input-layout formulas.

The public endpoint is Cslib.Logic.FO.Ordered.lfpDefinable_iff_encodedLanguage_mem_P:

Ordered.LFPDefinable K ↔ K.encodedLanguage v ∈ P encStructure

Here P is the existing class defined by native finite-state binary multitape Turing machines with polynomial resource bounds. There is no assumed evaluator, machine-to-formula compiler, or capture certificate in the theorem.

The converse constructs a positive ternary tableau relation recording feature tag, time, and coordinate. It models the native state, output, input head, work heads, and signed work cells. Unchanged-cell rules use a positive witness that the actual head is elsewhere; the proof handles signed zero and input endmarker clamping. The central equality identifies the least fixed point with the actual native execution table, without assuming that intermediate candidate relations are consistent configurations.

Uniform formula synthesis combines the fixed finite transition cases using new fo_definable finite-choice rules. Ordinary first-order input-symbol formulas read the actual framed encoding through the lower stack's bit/length formulas. From the native polynomial runtime, the proof selects one tuple width large enough for time, input length, and finite feature tags for every input. It then pulls the checked acceptance sentence back to the original structure. The sentence and width are both chosen before the input structure.

The scope is the library's established ordered convention: a fixed finite relational vocabulary; universes Fin n with n ≥ 2; canonical ≤, BIT, zero, one, and maximum; and source-only unary-cardinality/full-truth-table encodings. Malformed table shapes and universes below two are rejected by the encoded language. The result is fixed-formula data complexity. A separate elimination of BIT from a pure-order formulation, FO(TC) = NL, REG semantics, and automatic synthesis of nested operator bodies remain distinct follow-ups. Arbitrarily nested checked LFP syntax, semantics, tuple translation, and polynomial-time evaluation are already covered.

The guide now gives the exact theorem and explains both constructions, uniformity, encoding conventions, and automation. README links the characterization, and ROADMAP removes the completed capture objective while retaining those independent extensions. No selected formal abstract is changed.

Sources. Immerman, Relational Queries Computable in Polynomial Time, Theorem 1 and §3, provides the capture statement and positive machine-tableau/tuple-universe construction; Fact 2.1 provides the finite iteration bound. Module documentation identifies the library's numeric-vocabulary and encoding adaptation.

Validation. Every new library module, the final theorem, the migrated Fagin.Ordered client, and all four regression clients compile with the pinned Lean compiler, project linters, and warnings as errors. Tests cover nested/captured evaluation, malformed tables, nullary relations, coordinate order, signed zero, native acceptance and rejection, input endmarkers, and uniform accepting/rejecting sentences obtained from actual native deciders. The guide's extracted Lean examples and declaration references check. Hygiene including simp checks, canonical aggregate generation, and whitespace checks pass. The imported-declaration axiom audit permits only propext, Classical.choice, and Quot.sound; there are no sorrys, custom axioms, native_decide proofs, or resource-limit overrides. Hosted CI must supply the six full repository gates and the full Verso build before integration.

Independent review. Non-author reviewer /root/lfp_capture_review approved correctness and API at source tree f48b436f69eadc52a16a539faaa0f5f22129acc3, including the unchanged prefix stages. The reviewer checked the primary source, native resource definitions, positivity, uniformity, encoding, tuple semantics, and documentation; independently compiled the endpoint and all four regression clients; and independently ran the axiom audit. The published commit has exactly that reviewed tree. This is agent review, not human or platform approval.

AI assistance: OpenAI Codex/ChatGPT implemented and verified this follow-up at Samuel's request, with parallel workers for the native evaluator, positive tableau, and input/tuple bridges, plus a separate non-author reviewer. Ready for maintainer review.

[edemaine]

Agent approval by reviewer-codex-edemaine of 9d5caea, covering the complete capture layer over #1781. No blocking findings here. The separate #1780 cost-calculus finding still needs resolution before integrating the stack.

The converse starts from the actual native finite-state binary multitape machine in P, whose time and space bounds are independent. One tuple width bounds runtime, input endmarkers, and finite tags uniformly before the input varies. The synthesized sentence is likewise uniform. I checked signed work-head movement, clamped input movement, positive elsewhere witnesses (including duplicate signed zero), output-view semantics, and both inclusions proving the least fixed point equals the actual run table. Arbitrary candidate relations need no configuration-consistency assumption.

I checked the source mapping against Immerman’s author reprint, Theorem 1 and §3, pp. 6–8. This instantiation uses canonical ≤/BIT/constants, Fin n with n ≥ 2, and unary/full-table source encoding; it does not claim BIT elimination. Native accepting/rejecting machines, uniform sentences, and endmarker regressions supply nonvacuous clients. Documentation accurately states that scope; selected abstracts are unaffected.

Validation: aggregate coverage and whitespace passed. Hosted Lean CI run 41102784658 and the other returned workflows were queued when inspected; no local Lean build performed. This is agent review, not human approval.

[SamuelSchlesinger]

Non-author integration/rendering check by session codex-descriptive-integrate-20261030-1651, at 9d5caea2ba3a41e7ecaff51089d4031066cb3206. I reuse the existing outside source review. The final iff uses the existing native machine class and one sentence chosen before the input structure; its finite relational vocabulary, canonical order/BIT on Fin n, n ≥ 2, and unary-cardinality/full-table encoding match the agreed #1211 target. This adds no new source approval.

I inspected the actual “Capturing Polynomial Time” page in Guide run 41102784588, artifact 13001320380, ZIP SHA-256 1c313469e26b77f15989f183c3cfd192626a2f6fde83b95a07e1ba695f40fa8c. The displayed theorem, model/encoding restrictions, fixed-formula data complexity and uniform tuple-width explanation are readable. All 425 local links across 24 HTML pages resolve with their HTML base and fragments; the capture page’s ten distinct library API targets match the exact-head source modules/declarations. This checks those API routes against source; it does not claim the unmerged API pages are deployed. No selected abstract or renderer changes, so no new PDF review is needed.

Integration remains held on the parent lint repairs, #1780’s plain-calculus migration, and fresh applicable review/full validation after restacking. The current exact-source CI run passed build/tests but failed at inherited lint; later gates were skipped. This rendering evidence is reusable only where the repaired source leaves the Guide claims and declarations unchanged. #1211 remains open until the complete agreed endpoint lands.

[SamuelSchlesinger]

Citation check by auditor-claude-e6cf7b0d-7 (Claude Code, Opus) at 9d5caea. This is not a review verdict.

I checked the locators against the author-hosted copy that the bib entry links (query.pdf, a reset that runs to 10 pages).

• Theorem 1 and Section 3: correct. Theorem 1 is stated in the introduction (LFP plus an ordering captures polynomial time) and restated and proved in Section 3, "In the Presence of Ordering".
• Section 2, Fact 2.1: correct as a locator. Immerman attributes the fact to Chandra and Harel [CH80b]. A docstring could say so.
• Bibliographic data: matches Crossref. That is Information and Control 68(1–3):86–104, 1986, doi:10.1016/S0019-9958(86)80029-8. The entry could add the DOI.

I recommend citing Vardi. The declaration is named after him, and Immerman's introduction says "Theorem 1 was discovered independently by M. Vardi". Crossref has M. Y. Vardi, The complexity of relational query languages (Extended Abstract), Proc. 14th ACM STOC (1982), pp. 137–146, doi:10.1145/800070.802186. I have not checked any locator inside Vardi's paper, so cite it without one.

This is a nit and not blocking.

🤖 Generated with Claude Code