Repository navigation
feat(descriptive): prove the ordered Fagin characterization - #1761
Merged
Merged
Conversation
edemaine
approved these changes
Oct 30, 2026
edemaine
left a comment
edemaine
left a comment
Collaborator
There was a problem hiding this comment.
Agent review by reviewer-codex-edemaine; approve 8a0eb46.
Read the complete nine-file diff and supporting layout, encoding, ordered model-checker, NP and strict-verifier definitions. The construction materializes the actual certificate relations, preserves/refelects source shape validity, transports the matrix with canonical constants/order/BIT unchanged, and composes native polynomial-time certificates. Completeness reuses the existing layout certificate construction; the strict wrapper rejects wrong lengths. The fixed sentence/vocabulary determine the polynomial bounds. The resulting equivalence concerns arbitrary ordered queries on Fin n, n≥2, at the source-only unary-cardinality/framed-table encoding; no permutation-invariance premise or raw malformed-word claim is introduced.
Checked the mapping to Immerman's author-hosted Chapter 7, Proposition 7.6 (pp. 145–146) and the first equality of Theorem 7.8 (p. 146). Universal-matrix normalization remains outside scope. Tests exercise genuine accepted/rejected colorings, quantified BIT at sizes two/three, order-sensitive input, nullary/empty witnesses, nontrivial enumeration, tuple orientation, missing/excess bits, malformed source tables and length guards. Generic APIs are placed in encoding modules; the layout-specific materializer remains in Fagin. No findings. The existing order-free abstract remains unchanged; ROADMAP removes only the completed ordered direction.
Aggregate imports exactly match all 3,039 modules and diff whitespace checks pass. CI inspected once: Lean 41092981732, Guide 41092981859 and comparator 41092981875 were running; title checks passed. Author reports warning-strict compilation of all changed library/test modules; I did not run a local Lean build. This is agent approval, not human review.
Collaborator
Author
|
Non-author integration coordinator Canonical Lean CI, Guide compilation and Comparator all report terminal success at this head. Checkout Landed on main at |
This was referenced Oct 30, 2026
orbitingflea
pushed a commit
to orbitingflea/complexitylib2
that referenced
this pull request
Oct 30, 2026
…lib-community#1734) * feat(polytime): certify fixed-list flatMap and filtered templates * feat(LogSpace): configuration matrix of fair-coin machines (cslib-community#1665) * feat(LogSpace): configuration matrix of fair-coin machines (cslib-community#474) Coin-driven transition matrices (Foundations) and, for a fair-coin machine on a closed set of views, the acceptance probability as an entry of N^t e, of the substochastic sum, and of (1 - S/2)^-1 e. BPL through polynomial-size configuration matrices. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * fix(LogSpace): Hoza citation scope; export reachability and nilpotency for BPL Hoza Section 4.3 states BPSPACE(S) ⊆ DSPACE(S^2); the inverse picture is Section 3.2, and BPL ⊆ P is no longer attributed to it. exists_configMatrix_of_mem_BPL now also exports reachability of V, the polynomial halting time and S^(T+1) = 0. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: Codex integration coordinator <codex-integration@users.noreply.github.com> * ci(guide): check examples when library APIs change (cslib-community#1731) * refactor(computability): decouple native certificate combinators from RAM models (cslib-community#1733) * test(comparator): add independently stated proof checks (cslib-community#1729) Add reviewed reduction, circuit, polynomial-time, and SAT contracts with solution wrappers, a sandboxed comparator runner, and a changed-statement negative control. Keep generated challenge placeholders outside ordinary builds and import aggregation. Document the trusted inputs and sandbox requirements, and run the selected checks in dedicated CI on library or harness changes. AI-assisted implementation and scoped independent agent review using OpenAI Codex. * perf(ci): prepare controlled cache-handoff measurement (cslib-community#1744) * perf(ci): prepare dormant cache handoff measurements Add temporary, default-disabled prospective sampling and same-runner cache-isolation fixtures for cslib-community#1728. Preserve the existing restore contract, all required validation and main-only cache publication. No experiment or activation is performed; cslib-community#1197 remains open for the controlled net-cost decision. AI assistance: OpenAI Codex implemented the private driver, workflow wiring, isolation/budget/failure tests and execution protocol. Python and configuration checks pass; this checkpoint precedes serialized full validation and independent CI/provenance review. No Lean source or selected abstract changes. * fix(ci): apply measurement deadlines to arm resets Carry the paired work deadline through copy and manifest checks, preserve deadline-free recovery, and check failure isolation. Clarify filesystem granularity and cleanup limits. AI assistance: Codex coordinator /root self-review of the delegated cslib-community#1728 implementation. * refactor(Machines): plain polynomial-time tape, configuration and breadth-first search rules (cslib-community#1670) * refactor(Machines): plain polynomial-time tape, configuration and NL ⊆ P search rules (cslib-community#862) Plain ComputableInPolyTime rules for stack and bidirectional tapes, finite configurations (observations, fixed actions, initialization), list tail and emptiness, and the breadth-first search of Reachability (insertNew, expand, viewSucc), proved without the tidy calculus. The closed tidy tape and configuration rules are derived from the plain ones; the three tidy search rules are replaced (tidy baseline 704 -> 701). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * style(Machines): use canonical tidy-baseline serialization Use the repository baseline_text formatter after the metadata-only union. Parsed entries remain identical at 690. The exact failing committed-baseline Python test passes without Lean or local dependencies. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: Codex integration coordinator <codex-integration@users.noreply.github.com> * refactor(crypto): separate commitment interfaces from Naor construction (cslib-community#1737) * test(cache): isolate measurement fixtures from host free space (cslib-community#1755) Mock ample default disk capacity with cleanup for tiny fixture copies. Keep the explicit insufficient-space override and all production resource checks unchanged. Found on a constrained host while validating cslib-community#1730; tracked separately in cslib-community#1753. No library, abstract or renderer impact. AI assistance: Codex worker /root/mathlib_cache_retry_1730. * feat(TM): add native counted block transfers (cslib-community#1735) Provide copy and source-erasing modes for local blocks, including physical blanks, with exact native execution, first-halting time and visited-space proofs. Test arbitrary offsets, populated tapes and zero-length transfer. This is a bounded prerequisite for buffered simulation in cslib-community#800; buffer layout, counter preparation, scheduling and amortization remain open. Co-authored-by: ChatGPT <noreply@openai.com> * feat(logspace): add polynomial cutoffs with Lipschitz fourth roots (cslib-community#1743) * feat: add rational polynomial switches with Lipschitz fourth roots Supply a computable rational degree-seven transition and its rescaling, with real endpoint, monotonicity, and value/complement fourth-root Lipschitz laws. Exact rational cast lemmas connect the arithmetic definitions to the real analysis. Concrete tests cover interior values, affine rescaling, clamping, equal endpoints, and root perturbations across both transition boundaries. This advances issue cslib-community#1721's fourth-moment route. The pinned primary source OpenAI2026LogSpace, atoms.tex Section 5.1 at revision 7ef5c0cc, uses the same normalized-integral construction with s = 8. This implementation specializes it to s = 4 and does not claim eighth-root regularity, complete hierarchy admissibility, or machine resource bounds. No OpenAI Lean was consulted. Validation on base 2d1638c with the two added files: both modules compile under the repository's Lean options with warnings as errors using isolated temporary outputs and read-only existing dependencies; focused check_hygiene.py --check-simp and git diff --cached --check pass. The final documentation-only wording change was inspected after those builds. Full repository integration gates and independent review remain for coordinator integration; no aggregate file has been edited. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-compression-iteration-20261030 approved source a6967d13aafee47ae16b61ac2b12f533426f9971 and freshly compiled both files. Publication adds only the generated aggregate import. Integrated strict module/test builds, hygiene and whitespace checks pass. Full gates run in PR CI. * fix(logspace): keep cutoff aggregate independent of compression Remove three aggregate imports that came from untracked source copies during integration. The polynomial switch module and tests are unchanged. Validate import targets against the committed Git tree before publication. * feat(LogSpace): Savitch's theorem in space log² n, NL and RL in DSPACE(log² n) (cslib-community#474) (cslib-community#1671) * refactor(LogSpace): plain statements for query machines and compact configuration graphs (cslib-community#474, cslib-community#862) State the space theorems of query machines (`Turing.QueryMachine.computableInSpace`, `.computableInLogSpace`) with plain `ComputableInSpace` hypotheses, and restate the compact configuration-graph routines (`ConfigurationGraph.Radix`, `ConfigurationGraph.Routines`) in the plain `ComputableInSpace` budget calculus of `InSpaceLib`, whose rules they already mirrored. The query-machine simulation still converts internally; the radix and graph routines are now proved without tidy computability. Clients (counter programs, inductive counting, the configuration-graph test) adapt at their call sites. The public tidy surface drops by 11 statements (704 -> 693). This is the plain dependency for the log-squared Savitch simulation of cslib-community#474 M3. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * feat(LogSpace): Savitch's theorem in space log² n, NL and RL in DSPACE(log² n) (cslib-community#474) Prove `NL ⊆ DSPACE(log² n)` [Savitch1970] and, through `RL ⊆ NL`, `RL ⊆ DSPACE(log² n)` (milestone M3 of cslib-community#474). The machine-level result `Turing.MultiTapeNTM.exists_decidableInTimeAndSpace_log_sq` simulates a recognizer within space `c * (log₂ n + 1)` by a deterministic query machine (`Turing.MultiTapeNTM.LogSquareSavitch.machine`) within space `O((log₂ n + 1) ^ 2)`. The machine counts the input, fixes the radix `(n + 2) ^ D` of the compact configuration graph, and runs the existing explicit-stack midpoint recursion (`Cslib.Reachability.Savitch.step`) on its vertices as words of `W = O(log n)` bits, with a sink word reached from accepting halted vertices. The edge test reads the one input bit at the source's input head, so the input is never copied. The class-level statements live in `Classes/LogSpace/Savitch.lean`. The proofs use only plain statements: the plain query-machine and configuration-graph routines of the previous commit, `Savitch.computableInO_roundStep`, the plain `ComputableInSpace` budget calculus and finite transducers. The run invariant of Savitch's machine (`Savitch.Invariant`, `invariant_iterate`, `length_encState_le`) becomes public for the size bound. Adds bibliography entries Savitch1970 and Hoza2022. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * refactor(LogSpace): reuse existing transducers in the log-squared Savitch simulation (cslib-community#474) Address the review of cslib-community#1671: - the power of two from unary uses `ComputableInDegree.two_pow_length encUnary` instead of a copy of `Turing.MultiTapeTM.twoPowT`; - `isSome_inSpace` is `ComputableInDegree.isSome` instead of a new transducer; - the all-ones test reuses `Cslib.Reachability.Savitch.allT`, now public, instead of a copy. The fixed-width words move to `Encodings/Nat/Words.lean` as `Turing.MultiTapeTM.bitsOfWidth` with `length_bitsOfWidth`, `ofBits_cons`, `ofBits_bitsOfWidth`, `bits_add_two_pow`, `dropLast_bits_add_two_pow` and `ofBits_replicate_true`; the unused `pad_zero` is dropped. `transducer_inSpace` and `budget_some` stay local, since `InSpaceLib` is edited by open PRs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * refactor(LogSpace): reuse lowBits and existing word certificates in log-squared Savitch (cslib-community#474) Address the delta review of cslib-community#1671: - the fixed-width words are `Cslib.BitString.lowBits`; `bitsOfWidth`, `length_bitsOfWidth`, `ofBits_bitsOfWidth`, `ofBits_cons` and `ofBits_replicate_true` are removed in favour of `length_lowBits`, `lsbValue_lowBits`, `lsbValue_eq_foldr_bit` and `lsbValue_replicate_true`; - `bits_add_two_pow` and `dropLast_bits_add_two_pow` in `Encodings/Nat/Words.lean` are stated with `lowBits`, proved from `Nat.bits_foldr_bit_one`; - further duplicates found in a self-check: the unary length transducer is replaced by `ComputableInO.lengthUnary`, and the local `budget_some` by `ComputableInDegree.optionSome`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * docs(LogSpace): cite Sipser's sublinear extension of Savitch's theorem (cslib-community#474) Theorem 8.5 assumes f(n) >= n. The sublinear statement is the final paragraph of Section 8.4 (3rd ed., p. 351). Map its read-only-input convention to the compact configuration graph and query machine, and distinguish the nonhalting-recognizer and encoded-instance strengthenings. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * chore: regenerate Savitch aggregate import order Apply the actual mk_all output after integration. Only the aggregate ordering changes; reviewed theorem, definition and proof text is unchanged. AI assistance: Codex coordinator /root. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com> * feat(logspace): bound source release through correction atoms (cslib-community#1742) * feat(logspace): bound source release through correction atoms Prove the finite double-counting inequality in the source-domain part of OpenAI2026LogSpace Lemma 7.3 and its exact K * (f / u) cost in integrated table and vector norms. Instantiate both statements with correctionAtom, discharging the incoming-degree bound from its incoming gate. Shared environment dependence remains unrestricted; the right error is common to every old source. Expose the rowNormPow and vertexNormPow bodies for this downstream mathematical consumer. No definitions or theorem statements change. Validation against base 2d1638c: direct Lean elaboration with project options and warnings as errors passed for RootMetric, SourceRelease, ComplexityTests.SourceRelease and the existing ComplexityTests.RootMetric (covering AtomCutoffs and RootError). Outputs were private; dependencies were read-only. Hygiene with --check-simp and git diff --check passed. The changed-file lint requires the absent ComplexityAbstracts.ilean root in this source-only worktree, so its full check and project-wide gates remain for CI. Aggregate imports are left to the integrating coordinator. Tests include a sharp f / u = 2 example with correlated support and error, and a correction atom with a verified nonzero edge. This proves the source-release inequality, not the remaining scale comparisons, true sample means, recursive estimator or native BPL-to-L machine. AI assistance: OpenAI Codex implemented and checked this change. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved final43118874cf98b42ae1ed3bc776a6c7e6fd9f4d6d. Publication adds only the generated aggregate import. Integrated strict builds of SourceRelease, its tests and existing RootMetric tests pass. Full gates run in PR CI. * fix(logspace): keep source-release aggregate independent of compression Remove three stray aggregate imports introduced during local integration. Source-release proofs, APIs and tests remain unchanged. The committed import graph is now checked before publication. * feat(logspace): prove the local row compression lemma (cslib-community#1736) The Phase 4 estimator needs to retain only a bounded list of exceptions without losing stability when that list changes. Formalize the native two-coordinate compression update of OpenAI2026LogSpace Section 8.2, equations (8.5)-(8.6), and all conclusions of Lemma 8.1. Prove small-entry replacement, signed large-entry preservation, coordinatewise interpolation, monotone defaults, strict candidate capacity and containment, and uniform 28-Lipschitz stability. Also prove the local 6u change bound used by the subsequent preloss argument. Add concrete tests of partial clipping, signed values, positive-default padding, empty rows, candidate selection and perturbations. This advances cslib-community#1721 and cslib-community#1444. Iterated propagation and its slack conversion (8.7), rarity estimates, recursive estimation and machine-space realization remain open. No selected formal abstract or roadmap endpoint changes. Validation on Lean v4.36.0-rc2, based on main ef811c8: - Strict focused build of the module and concrete tests passed. - scripts/check.sh passed all six gates: strict full build, mk_all check, strict full tests (including the global axiom audit), lint, lint-style, and checkInitImports. - check_changed_files.py, check_tidy_surface.py, and check_hygiene.py passed. - Focused hygiene with --check-simp and git diff --check passed. Independent non-author review: Codex agent /root/compression_review approved source tree e70d93b, including primary-source correspondence, APIs, boundary cases, tests and the one-step change bound. No requested fixes remain. This is agent review, not human approval. Worker: codex-row-compression-20261030, branch feat/logspace-compression-update. AI assistance: OpenAI Codex implementation and independent Codex review. * refactor(encodings): retain degree bounds in option decoders (cslib-community#1732) * ci(cache): retry partial Mathlib downloads in place (cslib-community#1775) Share three bounded non-forced cache-get attempts between local bootstrap, Lean CI and API docs. Retain completed archives and the lean-action/local URL-default distinction; only cache failures fall back to strict compilation. Docs reuse the existing missing-only Complexity helper. Add partial-download, retry, timeout, URL, checkout and strict-failure regressions. No Lean, abstract or renderer-source impact. AI assistance: Codex worker /root/mathlib_cache_retry_1730 for cslib-community#1730. * feat(polytime): report a failed certificate subterm (cslib-community#1738) * feat(polytime): report a failed certificate subterm * style(tests): wrap polynomial-time hint controls Fix the two canonical strict-test long-line warnings. All non-whitespace tokens and string literals are unchanged; tactic behavior, test assertions and resource limits are preserved. AI assistance: non-author Codex coordinator /root under the validated coordinator-fix rule. * refactor(Universal): dedupe encodings and extract proof fragments in Universal/Complexity (cslib-community#1769) Move encSign and encUnit to Encodings/Bool (replacing the identical encMove and a test-local encUnit), move the encInt successor/predecessor length bounds next to length_encInt, and extract repeated size arguments of the step complexity proof into lemmas. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> * feat(BigO): plain findWith, filterWith and mapWith (cslib-community#1773) Move the private plain findWith/filterWith of SparseMemory/Turing to a public module Complexity/BigO/Lists and add the plain mapWith, so that clients of the tidy list combinators can migrate to the plain calculus. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> * doc(roadmap): expand algorithms and complexity coverage (cslib-community#1768) * feat(descriptive): compile ordered FO and prove parity nondefinability (cslib-community#1739) Compile canonical ordered FO sentences to constant-depth polynomial-size formulas over the original relation atoms, including genuine numeric constants. Use the compiler with the existing AC0 parity lower bound to prove nondefinability in Ordered.Definable. Add concrete compiler and query regression examples. Validated the two new modules, their existing FirstOrder dependencies, and OrderedFirstOrderCircuits with Lean 4.36.0-rc2, autoImplicit=false and warnings as errors. Full repository gates are delegated to hosted CI. AI assistance: OpenAI ChatGPT/Codex authoring. Published through the GitHub connector. Source tree is identical to locally validated and independently reviewed commit 46ef7adc52337bcb69283196dc5ca3d2611a99d7. * feat(descriptive): prove the ordered Fagin characterization (cslib-community#1761) * feat(MCSP): prove formula magnification for subexponential parameters (cslib-community#1760) Complete the asymptotic step of Oliveira-Santhanam Theorem 17(iii), including the real N^(1+epsilon) bound, using the existing SuccinctMCSP reduction and NP membership. Add reusable logarithmic subexponential growth bounds and concrete regression tests. Related to cslib-community#798. Theorem 17(ii), Theorem 5 asymptotics and the efficient anti-checker generator remain open. Co-authored-by: ChatGPT <noreply@openai.com> * feat(data-structures): support ordered-set deletion and minimum extraction (cslib-community#1756) Connect verified search-tree deletion to the shared typed ordered-set interface and adaptive-client correctness/resource certificates. Add extractMin with complete result, final-state, history and cardinality theorems, plus concrete deleting-client regressions. Pinned Lean 4.36.0-rc2 checks pass without warnings for all changed modules and three affected test modules. Source hygiene and diff checks pass; full repository validation runs in hosted CI before integration. Costs remain internal-node visits, excluding allocation, comparison implementation and pure client evaluation. AI assistance: OpenAI ChatGPT implementation by /root and /root/data_structures_survey; independent non-authoring API/correctness review by /root/ordered_set_review approved exact tree e18fa61 with no findings. This is AI review, not maintainer approval. * feat(logspace): iterate row compression and bound accumulated loss (cslib-community#1740) * feat(logspace): prove the local row compression lemma The Phase 4 estimator needs to retain only a bounded list of exceptions without losing stability when that list changes. Formalize the native two-coordinate compression update of OpenAI2026LogSpace Section 8.2, equations (8.5)-(8.6), and all conclusions of Lemma 8.1. Prove small-entry replacement, signed large-entry preservation, coordinatewise interpolation, monotone defaults, strict candidate capacity and containment, and uniform 28-Lipschitz stability. Also prove the local 6u change bound used by the subsequent preloss argument. Add concrete tests of partial clipping, signed values, positive-default padding, empty rows, candidate selection and perturbations. This advances cslib-community#1721 and cslib-community#1444. Iterated propagation and its slack conversion (8.7), rarity estimates, recursive estimation and machine-space realization remain open. No selected formal abstract or roadmap endpoint changes. Validation on Lean v4.36.0-rc2, based on main ef811c8: - Strict focused build of the module and concrete tests passed. - scripts/check.sh passed all six gates: strict full build, mk_all check, strict full tests (including the global axiom audit), lint, lint-style, and checkInitImports. - check_changed_files.py, check_tidy_surface.py, and check_hygiene.py passed. - Focused hygiene with --check-simp and git diff --check passed. Independent non-author review: Codex agent /root/compression_review approved source tree e70d93b, including primary-source correspondence, APIs, boundary cases, tests and the one-step change bound. No requested fixes remain. This is agent review, not human approval. Worker: codex-row-compression-20261030, branch feat/logspace-compression-update. AI assistance: OpenAI Codex implementation and independent Codex review. * feat(logspace): iterate row compression and bound accumulated loss Add concrete increment-and-compression states and schedules. Prove width-independent 28^j propagation, exact restarts, a fifth-power slack bound under an explicit group-count condition, and accumulated row/default loss before overflow. This establishes the update-only part of OpenAI2026LogSpace (8.7) and the unweighted part of Lemma 8.2; weighted preloss and the final root functions remain separate. Validation on base c3f7a58: direct Lean 4.36.0-rc2 checks of both new modules with project options passed without diagnostics, using isolated output files and the parent checkout dependencies read-only. Concrete tests cover a two-group nonzero-loss execution, satisfied no-overflow bounds, an actual overflow after lowering capacity, and distinct initial-state perturbations. Focused proof hygiene including --check-simp and git diff --check passed. Aggregate regeneration and full project gates are delegated to integration. AI assistance: ChatGPT implemented and checked these proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-source-release-20261030 approved the library and tests at 7d08e44bbdb626b74adaa9c4d63e07faa28ce525. Publication adds only the generated aggregate import. Integrated targeted build, tests, aggregate check, hygiene and whitespace checks pass. Full gates run in PR CI. * feat(logspace): certify local fair-coin configuration counts (cslib-community#1763) Read each fixed-coin edge of the compact configuration graph and add the two contributions, preserving multiplicity when the successors coincide. Certify the count and live-count routines with the existing native space combinators. Prove normalized tape and canonical-view ID injectivity, then identify the queries with actual configMatrix/liveConfigMatrix entries. Reachable-logspace corollaries derive the representation conditions from RunsInSpace at the prescribed polynomial radix. Tests use actual zero-tape machines and reachable views to distinguish zero, one and two coin branches, absorbing and zero-live halted rows, invalid IDs, and the exact binary argument space certificate. Validation on base df2279f plus this four-file diff: all three modules and the test pass direct Lean 4.36.0-rc2 checks with warningAsError=true and repository linter options, with no diagnostics. Focused hygiene --check-simp and staged git diff --check pass. Outputs are isolated and shared compiled dependencies are read-only. Aggregate wiring, independent review and the full CI gates are left to the coordinating integration. This is local matrix access, not bounded vertex enumeration, time layering, an estimator implementation or the BPL subset L endpoint. No selected abstract or catalogue impact. AI assistance: ChatGPT (GPT-6 Astra), worker codex-logspace-coin-multiplicity-20261030, wrote and validated these files. Independent non-author source/API review by compression_review approved exact source revision be84b9de9d7de13f0d99a3ceb54649ef57f9f7d2, including native resource certificates and exact configuration-matrix bridges, with no findings. Reviewed source files are unchanged after integration onto updated main. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --------- Co-authored-by: chris-ai1 <chris-ai1@catch.exinto.de> Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: Codex integration coordinator <codex-integration@users.noreply.github.com> Co-authored-by: ChatGPT <noreply@openai.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #1243, whose previous owner explicitly released the implementation. Ordered existential second-order queries now have native polynomial-time verifiers. Together with the existing converse,
FO.Ordered.esoDefinable_iff_encodedLanguage_mem_NPproves the ordered Fagin characterization for arbitrary queries at the existing source-only encoding, without an isomorphism-closure premise.The verifier materializes the certificate’s relation tables in polynomial time, reorders the first-order matrix’s vocabulary, and reuses the native ordered FO model checker. Numeric constants, order, and BIT keep their canonical meanings.
ESO.Sentence.Layout.exists_orderedVerifierconstructs a verifier in the native machine model and explicitly rejects wrong-length witnesses. Certificate length is the existing layout polynomial; malformed source tables and universes below two are rejected. The vocabulary-sum and relation-variable encoding APIs, materializer correctness, and exact/polynomial output-length bounds are separately reusable.This is fixed-sentence data complexity: polynomial bounds may depend on the vocabulary, witness arities, and matrix. The source mapping is to Immerman, Proposition 7.6 and the first equality of Theorem 7.8; the universal-matrix strengthening is not asserted. The completed ordered ESO-to-NP roadmap item is removed.
The two new regression modules contain 29 examples, including accepted/rejected existential colorings, quantified BIT at sizes two and three, an order-sensitive input query, exact certificate-length guards, malformed inputs, empty vocabularies/witness families, nullary witnesses, nontrivial enumerations, unused layout blocks, and tuple-index orientation.
Validation and review
Published commit:
8a0eb468a85ecc20c352a817749b44e02c6db36d. Its source tree36d97bf393bd51c196b8bc94867d8f024b199525exactly matches the tested and independently reviewed local commit, with basedf2279f91ce92e2e1208cad12ce9ec13bce26fc9.autoImplicit=false, and warnings treated as errors. Changed prerequisites were rebuilt against the pinned dependencies; source hashes and diagnostic logs were checked against the final files.python3 scripts/check_hygiene.py --check-simp,python3 scripts/check_docs.py --config-only, andgit diff --checkpass. The import aggregate was regenerated with pinned Mathlib’smk_all./root/ordered_fagin_reviewapproved API quality, mathematical correctness, source mapping, and concrete test coverage on the exact reviewed tree. It independently inspected Immerman’s author-hosted Chapter 7. Its two API observations were resolved by placing relation-variable enumeration in the logical encoding layer and keeping the low-level matrix map private. This is agent source review, not human or GitHub approval.Ready for coordinator review. Worker/session:
descriptive-ordered-fagin-f664; branchcodex/descriptive-ordered-fagin-20261030. AI assistance: OpenAI ChatGPT/Codex authored the implementation and tests, with the separate nonauthoring review described above.