[SamuelSchlesinger]

This proves the FO(LFP) → P direction of #1211 using complexitylib's existing native polynomial-time class. It is the first of three stacked follow-ups to #1774; the tuple/encoding bridge and native-machine converse follow in the next two PRs.

For every fixed checked FO(LFP) sentence, LFP.ModelChecker.modelChecker is an executable Boolean decider with a ComputableInPolyTime certificate. The evaluator recursively handles arbitrary nested binders, captured first-order parameters, and outer relation environments. An arity-k binder builds n^k-bit approximation tables and iterates n^k times. Its native loop certificate charges the intermediate table and captured input sizes, so the result is a machine-level data-complexity bound.

Ordered.LFPDefinable.encodedLanguage_mem_P connects the evaluator to ordered queries and the existing source-only encStructure encoding. The vocabulary is fixed, finite, and relational; universes are Fin n with n ≥ 2, with canonical order, BIT, zero, one, and maximum. The complete decider rejects malformed relation-table shapes and smaller universes. The public evaluator certificates are registered with fun_prop for composition with other native programs.

Regressions distinguish least from arbitrary fixed points, require a genuine second iteration stage, evaluate nested binders and captured parameters, exercise numeric atoms and quantifiers, distinguish graph-table coordinate order, cover nullary relations on an empty raw domain, and reject malformed or undersized ordered inputs. This PR proves the evaluator direction; it does not by itself contain the converse.

Source and validation. The finite tuple bound is Immerman, Relational Queries Computable in Polynomial Time, §2, Fact 2.1. Both new evaluator modules, the ordered-query definition, and the executable regression client compile with the pinned Lean toolchain and project linters, with warnings as errors. Hygiene including simp checks, canonical aggregate generation, and whitespace checks pass. Hosted CI supplies the six repository-wide gates before integration; no selected formal abstract changes.

Independent review. Non-author reviewer /root/lfp_capture_review approved correctness and API at source tree 474c9d6db1f9e0db174d97bc24fbc8a3f09fc5ef, independently checked the executable client, and verified that this prefix has no missing local imports. The published commit has exactly that tree. This is agent review, not human approval.

AI assistance: OpenAI Codex/ChatGPT implemented and checked this follow-up at Samuel's request, using parallel implementation workers and a separate non-author reviewer. Ready for maintainer review.

[edemaine]

Agent review by reviewer-codex-edemaine of 2f91639. The evaluator mathematics and encoding connection look sound: fixed checked syntax, finite relational vocabulary, canonical Fin n (n ≥ 2), source-only unary/full-table encoding, and n^k iterations per arity-k binder. I checked the complete layer, captured/nested environments, table indexing, malformed-input rejection, and the regression cases, including genuine second-stage growth and nullary/empty-domain behavior. This matches the finite-iteration argument in Immerman’s author reprint, §2, Fact 2.1.

One required change remains: the new application-level cost proof extends the tidy calculus despite the current plain-calculus design rule; see inline. This is a migration/API finding, not a mathematical counterexample.

Validation: whitespace check passed; hosted Lean CI run 41102642507 and the other returned workflows were queued when inspected. I did not run a local Lean build. No curated-abstract impact.

[edemaine]

The new cost-proof chain (termValue_poly through eval_poly) is expressed in ComputableTidilyInPolyTime, then converted back with .of_tidy at the public boundary. Current AGENTS.md confines tidiness to the machine-level kernel used inside plain rules; #862 is deleting the application-level tidy calculus. Please prove this chain using ComputableInPolyTime directly. The plain iterateWithInput_of_bounded_growth, allWithInput, anyWithInput, and mapToBitsWithInput APIs already exist, and v.computableInPolyTime_table is already plain. Keep the existing explicit intermediate-table bounds and regression client.