Repository navigation
feat(FineGrained): compose uniform counting search resources - #1335
Merged
SamuelSchlesinger merged 1 commit intoOct 27, 2026
Merged
Conversation
Replay the preserved native_counter_context supplier onto actual main 2e9725a, consuming the actual #1321 squash 2e9725a and landed #1299/#1320 sources. Library and original tests are byte-identical to prepared 27f682e83dd711ca4757b66617203adc9a2ad44e: eight library and three test proof-name replacements from polyBounded_pow to canonical PolyBounded.pow are the only changes from frozen 68daf67. Add one sorted aggregate import. Preserve every other actual-main blob, source credit and ROADMAP direction. This certifies the complete (context, unary N, CNF) input with independent time and workspace. Fixed threshold/leaf machines precede runtime inputs; all prefix and terminal-state costs and retained context are charged. Larger-context preparation remains charged separately against its original external input. This resource-only theorem does not depend on #1333 semantic strengthening and does not complete the final native counter or #1226. No curated abstract, catalogue or rendering change. Source/test correspondence, actual parent-source identity and diff checks pass. The prepared payload passed targeted strict source/test builds and aggregate validation. Exact actual-parent full validation and outside confirmation are pending at commit creation and will be recorded in the PR before readiness. Original implementation: coordinator-codex-01a16ab8/native_counter_context. AI-assisted mechanical cutover: worker-codex-uniform-cutover-1226 (Codex). Assignment: #1226 (comment) Original outside source review: #1226 (comment) Original six-gate evidence: #1226 (comment)
Collaborator
Author
There was a problem hiding this comment.
coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE FINAL APPROVED at 676b605c8b791482b7854df44071318a07bf055b, carrying the original resource review and actual-parent delta. Complete captured contexts, independent resources, numerical-depth premise, tests and canonical prerequisites are preserved; only the expected eleven proof-name substitutions change the accepted payloads. No findings remain.
Exact-head CI40496264130 passes all six gates, ratchet and changed-file checks; current title checks pass. Scope remains conditional resource composition, with the unconditional native counter separate. Ready for draft release and enqueue.
Collaborator
Author
|
|
This was referenced Oct 27, 2026
Closed
SamuelSchlesinger
marked this pull request as ready for review
October 27, 2026 12:03
SamuelSchlesinger
added a commit
that referenced
this pull request
Oct 27, 2026
Merge actual #1335 squash/main a22f590 into approved #1334 head 2031d62, preserving authored history and the actual-main aggregate union. Open the three canonical CNF helper names in CountingSparsificationUniform and normalizeDeclaredLeaf in its test, matching the completed strict combined-target probe. Fully qualify the normalization theorem doc link. Restore OpenAI source credit alongside Samuel Schlesinger and Anton Kovsharov in ModelCount/Declared, and clarify that the sparse leaf-provider correctness requires its sparse/below-threshold domain and exact supplied polynomial counter. All public definitions, statements, proofs, encodings, resource formulas and test cases retain their approved source. Other #1334 payloads match 2031 byte for byte; unrelated actual-main files and every existing import are preserved. No curated abstract or ROADMAP impact. Validation: scripts/cache/ensure.sh, then one narrow lake build --wfail --iofail on CountingSparsificationUniform and SparseCNFLeafCounter, both library and test targets, passed (7134 jobs). Lean MCP tools were unavailable; CLI fallback used isolated mutable outputs copied from the completed positive probe. Existing source/math review 5666803663 is reused; exact new-head hosted full gates remain required. Original author: Anton Kovsharov, with Gemini assistance. Bounded coordinator repair: worker refresh_1322_names (Codex), under PR #1334 claim 6441311517. Original contributor credit is preserved.
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.
Adds a plain native resource certificate for counting sparsification with a runtime context, unary declared variable count, and CNF. This consumes the landed shared context/declared-count interface and keeps time and workspace independent. Refs #1226.
The threshold and leaf machines are chosen before all inputs. The construction charges the complete encoded context, initialization, every prefix including the terminal state, leaf output, normalization and the final declared-count correction. It retains an explicit polynomial numerical-depth premise; a short binary parameter alone does not establish that bound. Any caller that constructs a larger internal context must also charge that preparation against its original external input.
The two main resource interfaces are
CountingSparsify.exists_computableInO_normalizeDeclaredLeafandCountingSparsify.exists_computableInO_searchDeclaredWith. They compose existing native iteration/context rules with the existing search and exact declared-count semantics. This is an original library resource composition toward the pinned manuscript's §6.4 and Appendix A, not a new claim that the unconditional counter or #1226 is complete. The concrete leaf solver, asymptotic parameter discharge, endpoints and checked abstract remain separate.The original supplier is
68daf676b8678c6b0b9627b2e46374e773ba6d6d, covered by the outside source review. The final integration follows the recorded recipe: consume actual prerequisite squashes, replace eight library and three test uses with canonicalPolyBounded.pow, preserve all other source/test bytes, and retain main's ROADMAP. No selected abstract or rendering changes.The original generic-context, independent-resource and diagnostic-provider regressions are retained. The diagnostic provider demonstrates the resource contract; it is not an exact general model counter.
Current source 676b605c8 is based directly on actual #1321/main 2e9725aec. Byte comparisons confirm the four landed #1321 source/test files match the approved supplier and the new source/tests match the prepared payload, with only the recorded eleven name replacements from the frozen revision. The diff contains exactly the supplier, its original test file, and one aggregate import.
At this exact head, all six default
scripts/check.shgates passed in one campaign with two threads after cache bootstrap. Fresh tidy-surface, changed-file, source-hygiene, abstract-selection and whitespace checks also passed; the strict test gate covered the existing formal-abstract audits. The source stayed unchanged throughout and the final worktree is clean. Lean MCP was unavailable, so validation used the CLI fallback.Outside delta source approval covers this exact head and adopts the original source review: actual-parent helpers, all eleven name replacements, tests, aggregate and ROADMAP correspondence are clean. Hosted CI for this exact head is running. This PR stays draft until the required checks pass.
AI assistance: original implementation by coordinator-codex-01a16ab8 / native_counter_context; mechanical integration and validation by worker-codex-uniform-cutover-1226. Independent review remains with the separate reviewer coordinator.