feat(fagin): prove ordered ESO data queries belong to native NP #1243

Activity

1. SamuelSchlesinger

   self-assigned this

   on Oct 27, 2026
2. SamuelSchlesinger commented on Oct 27, 2026

   

   SamuelSchlesinger

   on Oct 27, 2026 – with ChatGPT Codex Connector

   CollaboratorAuthor

   More actions

   active — worker-codex-descriptive-fagin-20261027 claims this AUTHORING scope under coordinator-codex-01a16ab8. This turn is M0 only, with no implementation branch or worktree. I have read origin/main’s AGENTS/CONTRIBUTING and the pinned cslib instructions. The protected user checkout is read/fetch only; no Lean command or build has run. I am inspecting the existing certificate layout and native ordered model checker, and will post the exact statement/encoding/milestone design here for outside review before implementation.
3. SamuelSchlesinger commented on Oct 27, 2026

   

   SamuelSchlesinger

   on Oct 27, 2026 – with ChatGPT Codex Connector

   CollaboratorAuthor

   More actions

   M0 for outside review — worker-codex-descriptive-fagin-20261027 (AUTHORING). No Lean implementation is authorized by this design post itself. The first requested slice is M1 below; the ordered Fagin endpoint stays open until M2 lands.

   The inspected source is main fae94eee, with cslib 6ff325e870ed89f86be10515f0e7297fa5a32845, Mathlib 625d8914199bc567cca9b91f90e8e5afafa5ae51, and Lean v4.36.0-rc1. Relevant files are unchanged from the initial main snapshot 52519f78. I read main's AGENTS/CONTRIBUTING and the pinned cslib AGENTS/CONTRIBUTING/CODESTYLE. No worktree, build or Lean edit has been made.

   Exact endpoint and scope. Preserve the existing FO.Ordered.Structure, Query, ESODefinable, ESO.Sentence, Complexity.NP and machine definitions. Proposed endpoint types, in Cslib.Logic.FO.Ordered, are:

   theorem ESODefinable.encodedLanguage_mem_NP
       {L : Language} [L.IsRelational] (v : Vocabulary L)
       {K : Query L} (hK : ESODefinable K) :
       K.encodedLanguage v ∈ Complexity.NP encStructure
   
   theorem esoDefinable_iff_encodedLanguage_mem_NP
       {L : Language} [L.IsRelational] (v : Vocabulary L) (K : Query L) :
       ESODefinable K ↔ K.encodedLanguage v ∈ Complexity.NP encStructure

   The reverse implication will use the current ESODefinable.of_queryLanguage_mem_NP, preserving its theorem and proof dependencies. The fixed-sentence precursor takes Φ : ESO.Sentence (Ordered.language L) and the query {M | Φ.Realize M}. Vocabulary and Φ are fixed parameters, never runtime inputs. This is data complexity, not combined model-checking complexity: polynomial degrees/constants may depend on the entire fixed formula, witness arities and vocabulary.

   Input remains EncodedStructure = ℕ × List (List Bool), encoded by encPair encUnary (encList encBits). The universe is Fin n; every original arity-r relation has a complete n^r-bit table in existing tupleIndex order (first coordinate least significant). Missing/extra tables and wrong table lengths are rejected. n = 0 and n = 1 are rejected, including for the true sentence. Numeric ≤, BIT, 0, 1, max retain their current canonical meanings and are computed, never supplied or guessed as tables. The theorem concerns encoded typed inputs; it makes no extra claim about raw bit strings outside the encoding's image. It requires no isomorphism closure of the source relations.

   Primary source mapping, checked at the source. From the author-hosted chapter 7 snapshot, Proposition 7.6, PDF pp. 3–4 / that snapshot's printed pp. 145–146:

   The second-order existentially definable boolean queries are all computable in NP.

   Paraphrase of its proof: guess relation truth tables, regard them as additional input relations, then apply fixed first-order model checking. Theorem 7.8 is on PDF p. 4 / printed p. 146; this work supplies its ESO→NP direction for our explicit conventions. These are the hosted snapshot's own page numbers, not an inferred pagination of the published edition. Chapter 3, Theorem 3.1, printed pp. 57–59, supplies the fixed-formula logspace step. Chapters 0–2, Provisos 1.14–1.15, PDF p. 28 / printed p. 16, supply canonical numeric symbols and n ≥ 2. Our current ordered language is the explicit ≤/BIT/constants specialization of that numeric vocabulary.

   Also checked Fagin's author-linked paper, Section 3, Theorem 6 and its forward proof, printed pp. 53–54 (PDF pp. 12–13). Paraphrase: shape-check the encoding, guess bounded-arity tables, and evaluate the fixed first-order sentence. Its original binary-cardinality encoding and empty-vocabulary distinction are not silently equated with our unary encoding. The implementation adapts the proof at our existing encoding.

   For reproducibility, SHA-256 of the downloaded source snapshots: chapter 7 7cd62b24789fa73893a0e80d22263eaa15b5c8cd3dcde1ff77ede7402cd6a4de; chapters 0–2 f59c173a8b126df3fdae71a1384ddc96a536bf3e1d12f8ccc8a7105a4f1ec4d6; Fagin PDF 495bbae66d0bc9d85ec2497211d1634ffbe5941213af5a17e85bd0d4722182c4. All other source descriptions here are labeled paraphrases, per #1072.

   Existing notions considered. Searches covered current main, the pinned cslib sources and pinned Mathlib ModelTheory/Equiv sources, plus open/all-state issue/PR searches.

   • Fagin/Verifier already has ESO.Sentence.Layout, polynomial, position, certRel, correctness/completeness, and native plain polynomial-time results. Reuse its layout and certificate construction. Its evaluator assumes a relational base language; Ordered.language L contains genuine constant functions, so simply applying its existing NP theorem would be ill-typed and mathematically insufficient.
   • Ordered FO model checking already supplies termExpr, actual numeric handlers, modelChecker and queryLanguage_mem_L. Reuse it on the source vocabulary enlarged by the guessed relations. No second ordered evaluator is planned.
   • Encoding and Ordered/Query already own shape validity, full tables, encoding and malformed/small-input behavior. Reuse them.
   • Mathlib's existing Language.sum, LHom.sumElim, sumMap, IsExpansionOn, sentence transport, Equiv.sigmaFiberEquiv and finite/sum equivalences suffice for symbol enumeration and reassociation. No replacement syntax or structure class. No existing Vocabulary.sum/witness-materialization API was found.
   • cslib's pinned MultiTapeTM.ComputesFunInTimeAndSpace, ComputableInTimeAndSpaceOfLength, and the existing plain list/unary arithmetic/lookup/composition certificates are the runtime layer. Current L_subset_P and mem_NP_iff_decidableInPolyTime give the machine bridges. No new complexity class or assumed polynomial verifier.
   • Fagin/Power, Layout and Tableau already implement NP→ESO, including explicit tape/configuration relations and framing. They are not evidence for ESO→NP and need no new tableau construction here. Closed feat(fagin): recover the ordered existential second-order converse #173/feat(fagin): recover the canonical ordered NP-to-ESO converse #175 concern that opposite direction.

   M1: smallest independently useful slice, target 900–1300 added/changed lines including tests, hard split before ~1500. Add a small sum-vocabulary encoding module and a Fagin witness-input module; keep all existing definitions/statements intact.

   For fixed Φ, reuse ℓ : ESO.Sentence.Layout Φ, put B = ℓ.blocks and d = ℓ.degree, and supply a fixed enumeration e : Fin m ≃ Φ.Var. It is design data, not extra input or a runtime encoding obligation. Write N = (encStructure a).length and retain exactly the existing polynomial p(N) = B·N^d. For each variable i, materialize the full table

   Tᵢ(a,w)[j] = w.getD (ℓ.position N i j) false, for 0 ≤ j < n^(Φ.arity i).

   The constructor A(a,w) is (n, a.2 ++ [T_(e 0), …, T_(e (m−1))]), with vocabulary L.sum (ESO.varLanguage Φ.arity). Numeric symbols do not occur in that vocabulary.

   The public contracts to prove are:

   1. A(a,w).1 = a.1, and v₊.WellFormed (A(a,w)) ↔ v.WellFormed a for every a,w.
   2. On v.WellFormed a, decoding A has exactly the source relations from v.decode a and variable relations ℓ.certRel n N w; prove each relation equation, including arity zero.
   3. Reuse the existing private certificate construction through one public existential lemma: if n ≤ N and 0 < N, every R has some w with w.length = ℓ.polynomial.eval N and ℓ.certRel n N w = R. Do not duplicate its construction/proof.
   4. Exact output length |encStructure A| = N + Σᵢ (2*n^(Φ.arity (e i)) + 1), and hence |encStructure A| ≤ N + m*(2*N^d+1). Unary cardinality already proves n ≤ N and N > 0, even for malformed source tables.
   5. A plain certificate ComputableInPolyTime A (encPair encStructure encBits) encStructure, for all input/certificate pairs. Use fixed enumeration, unary fixed powers, native lookup/map and append. This certifies actual construction cost, not just output size.

   Raw witness words have no table syntax to parse. Missing bits read false and excess bits are ignored in this total constructor; prescribed witness length belongs to the NP verifier contract. M1 tests distinguish those cases. Generic sum-enumeration/decoding facts belong in the neutral encoding module; the layout-dependent construction stays in Fagin. The other descriptive workers have been told no shared structure or input-bit-layout refactor is planned.

   M2: actual ordered endpoint, separate ≤~1500-line PR. Transport the fixed matrix from ((L.sum numericLanguage).sum varLanguage) to ((L.sum varLanguage).sum numericLanguage) by the existing language-map machinery. Prove its realization equivalence with the original matrix using the decoded relations from M1 and the unchanged canonical numeric structure.

   Instantiate queryLanguage_mem_L on v₊ and that transported matrix, use L_subset_P, and compose the resulting native deterministic decider with A. Obtain a verifier V without taking any efficiency hypothesis. Apply the existing strictVerifier to reject certificate lengths other than p(N). Prove IsVerifier encStructure ℓ.polynomial V ({M | Φ.Realize M}.encodedLanguage v) by table completeness/soundness, then prove the two endpoint statements above.

   The native certificate must remain inspectable: produce V,t,s with PolynomiallyBounded t, PolynomiallyBounded s and ComputableInTimeAndSpaceOfLength V (encPair encStructure encBits) encBool t s. Its definition quantifies an actual deterministic multitape TM with binary alphabet and finitely many states, and computation/time/space correctness on every encoded pair. The nondeterministic native corollary uses existing mem_NP_iff_decidableInPolyTime. Polynomial verification is proved by the constructor and current native model checker; it is not an assumption replacing this endpoint.

   Concrete tests. M1 will compute tables and decoded source/variable bits for nonempty unary/binary and nullary witnesses, distinguish tuple coordinate orientation, and exercise empty/truncated/long words, a layout with unused blocks, and empty source vocabulary. M2 will include an actual ESO coloring witness: ∃U, U(0) ∧ ¬U(max) ∧ ∀x y, E(x,y) → (U(x) ↔ ¬U(y)); the two-element edge 0→1 is accepted using U={0}, while adding a self-loop makes it false for every U. Separate quantified BIT/constant tests use ∃U, (∀x, U(x) ↔ BIT(x,1)) ∧ U(max), true at size 3 and false at size 2. Controls cover no second-order variables, nullary true/contradictory witnesses, always-true/false matrices, well-shaped n=0/1, missing/extra/wrong-length source tables, and the strict verifier's short/long rejection. Both semantic and encoded-language outcomes must be checked; signature restatements alone do not count.

   Abstract and completion discipline. The current fagin abstract states the order-free characterization, including empty/singleton structures. M1 does not change that claim. M2 completes the ordered variant and connects it to the existing catalogue entry in scope documentation; it does not overwrite the order-free theorem, impose n≥2 on it, or claim universal-matrix normalization. Any proposed headline/bridge change gets separate explicit outside review and rendered-PDF evidence; if that would exceed the PR cap, split it into M3.

   Before any later Lean work: recheck issue ownership and pins, create an ordinary isolated worktree with independent outputs, verify every manifest pin against the shared read-only dependency store, and run the required cache bootstrap. Implementation uses plain public statements, no sorry/custom axioms/native_decide or raised budgets. Final PRs require meaningful tests, all six gates, hygiene/abstract checks, scripts/check_pr_names.py on the actual PR body, hosted CI linked to the final revision, and outside API/correctness review. This post records design evidence only, not Lean validation.

   Status: awaiting M0 outside review; implementation slot released. coordinator-reviewer-codex-20261023 may review this design under Samuel's review arrangement; neither this author nor the delegating coordinator self-approves its new statements.
4. SamuelSchlesinger commented on Oct 27, 2026

   

   SamuelSchlesinger

   on Oct 27, 2026 – with ChatGPT Codex Connector

   CollaboratorAuthor

   More actions

   paused / slot released — worker-codex-descriptive-fagin-20261027. The M0 checkpoint was posted immediately before the coordinator’s stop arrived. Authoritative correction on #587 confirms that the descriptive/crypto dispatch was stale and Samuel’s later #1226-only direction controls. No Lean implementation, worktree, build or PR was started. The full ordered ESO→native NP objective remains unproved/open here; existing source credit and the proposed M1/M2 split are retained for a future authorized resumption. This is not an active claim or an outside-review request; all capacity returns to #1226.
5. SamuelSchlesinger

   closed this as completedin #1761on Oct 30, 2026
6. SamuelSchlesinger commented on Oct 30, 2026

   

   SamuelSchlesinger

   on Oct 30, 2026 – with ChatGPT Codex Connector

   CollaboratorAuthor

   More actions

   Completed by #1761, now landed on main. This proves fixed-sentence ordered ESO data queries have native NP verifiers at the existing strict source encoding, including malformed-source and witness-length rejection. The integration record owns validation and cache follow-through. The order-free headline is unchanged, and the broader descriptive-complexity work remains open. Non-author coordinator: /root/mathlib_cache_retry_1730.