[SamuelSchlesinger]

This adds the logical transport and actual input-layout formulas needed by the native-machine → FO(LFP) direction of #1211. It is the second stacked follow-up to #1774, based on #1780.

The reusable tuple compiler translates checked FO(LFP) syntax through a first-order interpretation. It replaces variables by coordinate blocks, scales relation arities, translates term applications through witness graphs, and preserves captured parameters and arbitrary nested binders. Syntactic positivity and well-formedness are preserved. Its semantic proof transports all candidate fixed-point relations through the tuple equivalence; the raw prefixed-point semantics is preserved even before a positivity assumption is supplied.

FullTupleInterpretation.onLFPSentence specializes this to canonical ordered tuple universes. Vocabulary.orderedPowerInterpretation connects that interpretation to the library's existing power structure, reversing coordinate blocks to reconcile lexicographic ranking with the encoding's little-endian tuple index. The exact structure equality supports later sentence pullback without additional input relations.

Vocabulary.inputLength and Vocabulary.inputBit are ordinary first-order formulas for the actual unary-cardinality/full-truth-table encStructure word, including framing. Their correctness is proved for every well-formed input whose word fits inside the power domain. No guessed bit relation or assumed encoding compiler is introduced. The reusable strict-order interpretation is extracted from Fagin.Ordered; its existing client is migrated and checked.

Tests cover nullary and unary payloads, framing markers, false data bits, terminators and padding, and distinguish the tuple ranks of (0,1) and (1,0). The new encoding semantic laws are registered with fo_realize.

Sources and validation. The polynomial tuple-domain construction follows Immerman, Relational Queries Computable in Polynomial Time, §3; the detailed transport and encoding proofs instantiate it for the library's canonical ordered vocabulary. Every new module, the existing Fagin.Ordered client, and FOInputEncoding compile with the pinned Lean compiler, project linters, and warnings as errors. Hygiene including simp checks, canonical aggregate generation, and whitespace checks pass. The repository-wide gates remain with hosted CI before integration; no selected formal abstract changes.

Independent review. Non-author reviewer /root/lfp_capture_review approved correctness and API at source tree 65538659960c8a957181edd64ed32649428b062d, independently compiled the encoding regressions, and verified this prefix's import closure. 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, with parallel workers and a separate non-author reviewer. Ready for maintainer review.

[edemaine]

Agent approval by reviewer-codex-edemaine of 3b14fa7, covering this layer over #1780. No blocking findings in the complete tuple/encoding delta or migrated Fagin client. The separate #1780 cost-calculus finding remains with that layer.

The compiler transports all candidate relations bijectively, preserving raw prefixed-intersection semantics, nested binders, captured parameters, and syntactic positivity. Term graphs also cover constants and nullary arguments. The power bridge correctly reverses coordinate blocks between colex table indexing and lexicographic ranks. Input-length/bit formulas describe the actual framed unary/full-table encoding; their domain must contain its endpoint. These are concrete encoding/transport details of the tuple construction in Immerman’s author reprint, §3, pp. 6–7.

I checked the actual prerequisite definitions and regressions distinguishing ranks (0,1)/(1,0), nullary/unary payloads, markers, false bits, terminators, and padding. Aggregate coverage and whitespace checks passed. Hosted Lean CI run 41102683482 and the other returned workflows were queued when inspected; no local Lean build performed. No curated-abstract impact. This is agent review.