FO(TC) = native NL on canonically ordered finite structures #1246

Paused / released, 2026-10-27: the authoritative correction says the descriptive dispatch was stale and Samuel’s later #1226-only direction remains current. This issue was created immediately before that correction. Its M0 is unreviewed; no implementation is authorized under the current allocation.

Tracking the full FO(TC)=NL objective in ROADMAP’s descriptive-complexity section, coordinated with #1211 and Samuel’s dispatch (superseded allocation). M0 author: worker-codex-descriptive-fixedpoint-20261027, delegated by coordinator-codex-01a16ab8. Design only; no Lean has been written. The capture theorem remains open. Separate scoped milestones below do not complete it.

For every fixed relational language L, finite enumeration v : Vocabulary L, and ordered query K : FO.Ordered.Query L, the intended endpoint is
TCDefinable K ↔ K.encodedLanguage v ∈ Cslib.Complexity.NL encStructure.
Here TCDefinable will mean existence of one finite FO(TC) sentence, with arbitrary Boolean connectives, first-order quantifiers, nested TC and parameters, interpreted on all existing FO.Ordered.Structure L. It will not define a replacement machine class. The forward theorem first constructs a native machine for each fixed formula/vocabulary; the converse constructs a single finite formula from each existing native NL witness. Neither formula nor machine varies with universe size.

Exact conventions. Retain Fin n, 2 ≤ n, canonical computed ≤/BIT/0/1/max, and the existing source-only Query.encodedLanguage. Numeric tables are not input. EncodedStructure = ℕ × List (List Bool) and encStructure = encPair encUnary (encList encBits) charge unary n and complete relation tables. For well-formed input, its length is exactly 2*n+1 + Σ i, (2*n^(v.arity i)+1); derive/use this from Encoding/Layout.length_encStructure and shape, including an empty vocabulary and nullary tables of length one. Malformed shapes and n=0/1 are rejected. Thus encoded length is polynomial in n for fixed v and n ≤ encoded length. Coefficients, tuple dimensions and all resource constants may depend on the fixed formula/vocabulary or fixed source machine; no formula-independent data-complexity exponent is promised.

TC is reflexive transitive closure on tuples: for a body ψ whose two bound k-tuples are x,y and whose remaining environment is η,
Realize (TC ψ s t) η ↔ Relation.ReflTransGen (fun a b => Realize ψ (η,x:=a,y:=b)) (eval s) (eval t).
Zero-length paths count. Allow k=0 explicitly: the empty tuple has one value, so its reflexive TC test is true even for a false edge body. Distinguish the positive-TC fragment from unrestricted negated TC.

Native forward route. Reuse the actual fixed-FO checker, tuple/radix arithmetic and nondeterministic counter-program compiler, with fixed finite code, binary alphabet and finitely many native states. A TC call retains current/target tuples, environment and a binary bounded-path counter; guess in-range successor tuples and check each edge by the recursively compiled body. A simple accepting path needs at most n^k-1 edges (test equality before decrementing); all other branches reject when their bound expires. Nested evaluation retains only a fixed number of O(log n)-bit fields per fixed formula, recomputes edges and never stores a graph/path/closure table. Prove every branch halts and every prefix uses O(log N) work cells for encoded length N. Boolean conjunction and universal quantification need actual sequential native constructions; existential search and disjunction use bounded choices. Negation uses the existing native MultiTapeNTM.exists_decidesInSpace_compl / Complexity.compl_mem_NL construction, rather than flipping nondeterministic accept states. Syntax-directed compilation must select and compose these finite-state witnesses, with callbacks and saved environments charged; no assumed evaluation oracle. The public endpoint uses plain native resource predicates. The current compiler’s tidy callbacks remain internal.

Converse/shared interface. The ordered-completeness worker owns the machine→FO compact-configuration interpretation needed also for REACH hardness. Its proposed contract is: for each fixed native NL machine/witness and v, produce fixed positive tuple dimension and FO formulas for valid configurations, actual native step, start and accepting halt; prove realization matches ConfigurationGraph / native view facts, including encStructure framing, input boundaries, work-tape symbols, summarized output [true], and malformed IDs. Existing accepts_iff_reachable_bad_of_runsInSpace and fits_of_runsInSpace supply semantic/size lemmas, not FO definability. Absorb the polynomial-in-N bound into n^d using the fixed-v length bound. Encode finite control with fixed Boolean tuple tags so n=2 works for arbitrarily many fixed states. TC then applies to this actual FO edge relation, existentially choosing an accepting endpoint. No hypothesis that a configuration formula/evaluator already exists may appear in the final capture theorem. Generic encoded-input bit/layout facts belong below Fagin/TC/LFP; coordinate extraction with the ordered worker.

Existing notions considered (main fae94eee4dfef9829f1a9599edebf45eb60cfb97, cslib 6ff325e870ed89f86be10515f0e7297fa5a32845). Reuse Mathlib terms/atomic syntax and Relation.ReflTransGen; local Vocabulary, encoding/layout, FO.Ordered arithmetic/full-tuple interpretation; queryLanguage_mem_L; CounterProgram.exists_decidesInLogSpace, NondeterministicQueryMachine.exists_decidesInSpace; compact native configuration graph and native NL complementation. Mathlib’s closed BoundedFormula inductive cannot acquire TC constructors: a scoped extension AST is necessary, retaining its terms/atoms and proving the FO embedding. Do not duplicate structures, encodings or reachability. Source searches in local/pinned cslib and current main found no logical TC/LFP AST. Open+closed issue/PR searches for FO(TC), LFP, and transitive closure found #1211/#587/#1202, but no dedicated TC implementation/claim; #465 supplies NL complementation rather than logical capture.

Primary sources checked; all following descriptions are paraphrases. Immerman’s author reprint, Languages That Capture Complexity Classes, §3, PDF p.6, Theorem3.1 proves NL=(FO+positive TC); PDF p.7, Theorem3.3 gives the positive-TC normal form. §2/PDFp5 assumes ordered successor and at least two elements. This is not itself the later unrestricted-negation statement: that step here explicitly uses the existing native NL complementation theorem. SHA256 of the inspected author PDF: d3790a48e149afafd8b2a25f9deddcb8d98f4c1e02f72f3c4cc8b89488fb0d64; reprint page numbers are not claimed to be published SIAM pagination. Vardi1982, PDFp5/proceedings141, Theorem4 separately distinguishes nondeterministic-logspace data complexity from PSPACE expression complexity. The published 1999 book places Complementation and Transitive Closure at pp.139–155; exact internal theorem locators must be checked from that edition before a PR quotes them. Do not transplant 2015 draft pagination.

Milestone order, each PR about ≤1500 changed lines; split before exceeding it.

1. Scoped TC syntax, Mathlib-FO embedding, substitution/renaming and exact reflexive tuple semantics; concrete controls for no edges, one edge, cycle, unreachable target, k=0 and parameter capture. This is syntax/semantics only.
2. Native bounded tuple-path controller with explicit all-prefix space and all-branches termination; checked reachable and unreachable graphs. No general capture claim yet.
3. Positive-TC recursive compiler, including saved environments/quantifiers; then a separate unrestricted-negation compiler using the existing complement machine. Prove actual encoded query membership in native NL.
4. Consume independently reviewed machine→FO graph milestones from the ordered track; prove TC pullback/parameter semantics and native NL→TC definability.
5. Combine both directions, review the full quantifiers/encoding statement, retain n=2/nullary/malformed/empty-vocabulary controls and explicit actual native machine examples.

#1211 owns LFP syntax/monotonicity/tables/native-P capture, and the ordered track owns ordered reductions/completeness. This issue does not start competing extensions. M0 has no abstract/catalogue impact; bounded syntax helpers will not be promoted to a headline. Each implementation PR requires source-faithful quotation/mapping or labeled specialization, concrete true/false clients, plain public statements, no sorry/custom axiom/native_decide or budget increases, scripts/check_pr_names.py on its body, all required checks with hosted CI, and independent nonauthor review of the exact revision.

Status: Paused / released under the priority correction. The M0 is unreviewed and unimplemented. The full objective remains open; no implementation ownership is retained.