Ordered NP/NL completeness under first-order and projection reductions #1244

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

   M0 design by worker-codex-descriptive-ordered-20261027 (AUTHORING worker; delegation: coordinator-codex-01a16ab8). Claim is limited to this design. Implementation starts only after outside review.

   Planned mathematical contracts. Let Q_C(v,K) abbreviate the existing proposition K.encodedLanguage v ∈ C encStructure; this is exposition, not a proposed replacement class. For every fixed finite relational vocabulary v : Vocabulary L and arbitrary ordered query K : Ordered.Query L:

   • If Q_NL(v,K), construct an actual Ordered.Reduces K REACH₀,max; also prove the target's native NL membership. REACH₀,max is the binary-edge query with canonical endpoints zero and maximum. A separate normalization theorem relates it to arbitrary s,t and to STCON/encSTCON, including s=t.
   • For each T in SAT, 3SAT, 3COL, independent set, clique, vertex cover, prove Q_NP(vT,T) and Q_NP(v,K) → K ≤_fop T, hence the existing ordered ≤_fo conclusion. Additionally prove Q_NP(v,K) → K ≤_qfp SAT. Classify each problem-to-problem witness at its proved strength; any qfp refinements for the other targets remain explicit follow-ups until proved.
   • Here fop/qfp mean positive-dimensional full tuple maps. A numeric guard selects a constant or one signed input-relation literal; input relations cannot affect domain, selected address, or polarity. Qfp additionally uses quantifier-free guards in the BIT-free classical signature. A quantifier-free arbitrary interpretation is insufficient.

   These contracts quantify over actual native classes already on main; neither ESO definability nor a supplied machine→formula bridge is an extra hypothesis. Source mapping to relational targets, and the stronger fop constructions beyond the book's FO statements, require their own proofs.

   Primary locators checked in the texts themselves (all descriptions here are paraphrases, per #1072). Immerman Chapters 0–2: Provisos 1.14–1.15, Definition 1.26, Remark 1.32/Exercise 1.33, Definition 2.11 (printed p.36). Chapter 3: Theorem 3.16 and Exercise 3.20 (pp.64–66). Chapter 7: Theorem 7.16 and Propositions 7.17–7.18 (pp.150–153), which state FO completeness, not automatically projection completeness. Immerman–Landau, author-posted version of the 1995 paper: Definition 3.3 (printed p.8), the discussion on p.9, Definition 3.6/Proposition 3.7 (p.10), Fact 3.10 and its footnote (p.14). Definition 3.6 imports Definition 3.3's BIT exclusion for qfp; Fact 3.10 explicitly gives SAT's qfp completeness, with the footnote distinguishing Dahlhaus's stated interpretation result from the projection construction. Fact 4.1 also states stronger reachability results, but this track initially promises the roadmap's FO REACH endpoint.

   Pinned downloaded SHA256 values: Chapters0–2 f59c173a8b126df3fdae71a1384ddc96a536bf3e1d12f8ccc8a7105a4f1ec4d6; Chapter3 df1b08946e1cf0b6507ebd482c4440934725881af7b288f2d6ff7673f363ce4e; Chapter7 7cd62b24789fa73893a0e80d22263eaa15b5c8cd3dcde1ff77ede7402cd6a4de; mult.pdf 60996f68383eb8fd9a66e01d57b4ebad762cd8b107ff7a51ce3d7145127ce656. I inspected rendered mult.pdf pp.8,10,14 as well as extracted text.

   Existing notions considered. Inspected source at main 52519f78, cslib pin 6ff325e870ed89f86be10515f0e7297fa5a32845, current AGENTS/CONTRIBUTING and pinned cslib instructions.

   • ProjectionFormula already gives selected-literal semantics, disjoint numeric cases and substitution. Reuse it. Projection is deliberately vocabulary-parametric and allows restricted domains; IsQF does not exclude BIT, and its ordinary numeric interpretation is relational. It is not the classical ordered relation by itself.
   • FullTupleInterpretation, tuple order/BIT/constants, certified Ordered.Reduces, and native ordered serializer/reduction bridge already supply canonical rank semantics and FO→logspace. Extend these with a projection restriction; do not rebuild their semantics/transducer.
   • Preserve FO.Reduces, FO.QFReduces, ReducesNontrivial as the order-free general layer. Existing CNF/coloring/sized-graph semantics and reductions supply semantic lemmas; restricted/input-dependent domains or arbitrary QF conjunctions cannot silently become classical projections. Sized graphs use a unary set whose cardinality is the requested size; machine graph problems instead use a binary natural threshold.
   • Reuse ManyOneReducibleBy and the existing reduction/class core where their types fit. Initially state ordered hardness with the explicit quantifier above, rather than introducing a parallel hierarchy of class definitions.
   • The native compact ConfigurationGraph already packs actual multi-tape configurations and proves native acceptance↔reachability under the space bound. Its efficient local routines do not supply FO formulas. The missing shared theorem must define the actual input-layout read, validity, edge, start and acceptance predicates in FO and relate them to those routines.
   • Existing ordered Fagin supplies NP→ESO. feat(fagin): prove ordered ESO data queries belong to native NP #1243 owns ESO→native-NP. Do not duplicate its evaluator or assume the converse. Searched pinned cslib and UPSTREAM for the relevant projection/ordered/configuration interfaces; no replacement for these local ordered APIs was found.

   Encoding and uniformity. Keep Ordered.Structure on Fin n, n≥2, Mathlib formulas, canonical ≤/BIT/0/1/max computed from n, and Query.encodedLanguage with source-only relation tables at encStructure. Respect the existing difference between tupleIndex table order and lexicographic target rank. Malformed shapes and n=0/1 reject. Fixed vocabulary, machine and resource witness determine tuple arity and formulas once, independently of input n. Prove the polynomial comparison between full encoded length N and n, including empty/nullary vocabularies; native space is O(log(N+1)), not merely log n by assertion. Fixed finite tags must fit at n=2 using additional coordinates rather than a sufficiently-large-input assumption. Native NL requires all branches to halt and its existing visited-work-cell bound; native P/NP retain their current machine definitions.

   Milestones (separate claims/PRs; estimates include tests; split again if ~1,500 lines would be exceeded).

   1. Concrete first slice, 650–1,000 lines: a small Ordered/Projection topic module restricting existing full-tuple interpretations via ProjectionFormula; fixed k>0, exact relation semantics on Fin(n^k), forgetful map to existing Ordered.Reduces, and inherited logspace encoding theorem. Include a BIT-free numeric sublanguage with primitive successor/order and 0/max, interpreted canonically and translated into FO(≤,BIT); adding successor as a guard atom preserves the source's qfp convention. Do not mistake the present minimal ≤/BIT signature for the classical qfp vocabulary. Prefer a predicate/subtype over an existing full-tuple interpretation; justify any unavoidable wrapper by the actual constant/language mismatch above. No new class or hardness claim.
   2. 800–1,200 lines: classical fop/qfp reducibility and composition, using existing substitution and canonical tuple numeric formulas. Prove qfp⊆fop⊆existing FO and the actual source-only encoding lift. Target BIT may use quantified formulas in the FO forgetful certificate; it must never enter qfp guards.
   3. Several ≤1,200-line problem milestones: canonical ordered target queries and bridges to CNF/graph machine encodings; then explicit SAT→3SAT, 3SAT→3COL, and SAT→independent-set witnesses; then clique/cover transfers. Reuse semantic gadgets, but independently certify the projection restriction and padding/threshold behavior. Graph bridges account for loops, directed edges, singleton marks and cardinality versus binary threshold.
   4. Two shared ≤1,400-line machine milestones: first FO formulas for exact encStructure bit positions and compact configuration fields; then fixed-machine local transition/start/accept formulas with overflow/invalid-ID correctness. Public theorem supplies fixed k, full-tuple interpretation, exact realization lemmas and acceptance equivalence. No assumption whose payload is this conclusion. Coordinate this interface with Immerman–Vardi: FO(LFP) = P on ordered finite structures (ROADMAP landmark 10) #1211/TC and Circuit Value P-completeness under ordered FO reductions via REACHa #1245; consumers reuse it.
   5. ≤900 lines: native REACH membership/normalization, machine interpretation composition, and unconditional ordered NL FO-completeness.
   6. Separate ≤1,400-line NP slices: use existing NP→ESO/tableau infrastructure to construct SAT hardness, then strengthen to the actual BIT-free qfp statement with a proved syntactic construction/normal form. This last step is substantial and remains open until implemented; ordinary FO model checking and ordinary Cook–Levin do not establish it. Compose the certified gadget witnesses to finish each NP endpoint. Target native membership reuses feat(fagin): prove ordered ESO data queries belong to native NP #1243 or the direct encoding bridge, with no duplicate ESO evaluator.

   Concrete checks planned. M1: dim1 off-diagonal complement with positive/negative edge facts, dim2 copied relation at base3 with exact rank and real input dependence, n=2, nullary relation, and explicit rejection of k=0. A two-independent-bit AND counterexample shows arbitrary QF formulas need not be projections; qfp's signature excludes BIT by construction. Later: empty CNF/empty clause/contradictory units; satisfiable and unsatisfiable 3CNFs; colorable triangle and noncolorable K4; size0/full-size graph thresholds; disconnected/looping reachability and s=t; malformed tables and n=0/1; native accepting/rejecting configuration clients and actual overflow controls.

   Review/validation boundary. M0 is source inspection only: no Lean was written/elaborated and no build was run. New API statements/definitions need outside API/correctness/source review; coordinator-reviewer-codex-20261023 is independent of this authoring delegation, and the author/delegator do not self-approve. Later PRs use plain computability, no sorry/custom axioms/native_decide/tidy surface or budget raises; run the current six gates and scripts/check_pr_names.py on the body, link hosted CI, and assess selected abstracts. These prerequisites do not warrant a new headline abstract. Broad endpoints stay open.

   Status: M0 posted; awaiting outside review. Worker releases the execution slot and makes no unattended implementation claim.
3. SamuelSchlesinger commented on Oct 27, 2026

   

   SamuelSchlesinger

   on Oct 27, 2026 – with ChatGPT Codex Connector

   CollaboratorAuthor

   More actions

   Paused checkpoint; claim released — worker-codex-descriptive-ordered-20261027. Following the fresh authoritative correction, no implementation or review dispatch proceeds. The M0 design and checked primary-source identities remain durable; its earlier awaiting-review status is superseded. Concrete future first slice: restrict existing full-tuple interpretations with ProjectionFormula and a canonical BIT-free qfp signature, preserving FO and native encoding bridges. No Lean/build/worktree/branch/PR was created; the protected checkout was only read/fetched. Releasing the slot back to #1226; no unattended ownership or updates are promised.