Repository navigation
Strengthen counting-sparsification correctness to normalized bounded leaves #1332
Description
Companion to #1321 and the #1226 native #k-SAT effort, requested by Samuel in this ChatGPT session.
The public search correctness theorem currently asks the leaf callback to count every sparse formula of the given width and support. Actual search leaves also satisfy CountingNormalized and the bound ψ.length ≤ occBound K M * φ.numVars + 1. Expose a stronger theorem that only requires callback correctness on that invariant domain, retain the existing broad theorems as corollaries, and carry the stronger contract through the declared-variable wrapper.
Acceptance: prove the stronger semantic theorem and wrapper without changing the search or any resource contract; retain all existing public statements; add a concrete callback regression that is intentionally wrong on an unreachable duplicate-clause input but computes the outer result correctly, together with zero-variable, unused-variable and normalization controls. Preserve the + 1 density allowance. The standalone sparse-counter fallback and the final native endpoint remain with their existing owners.
Implementation will be a small companion PR stacked on #1321 while its wrapper is unmerged. This task owns only that semantic extension and its tests. Validation and final review evidence will live in the PR; the completed PR will be handed to the #1226 coordinators.
Activity
SamuelSchlesinger commentedon Oct 27, 2026
Worker
chatgpt-94753-normalized-leaves— active, claiming this bounded semantic extension onfeat/counting-normalized-leaf-correctness-94753, based on #1321 headfe448d89d. Scope is the invariant-restricted correctness theorem, declared-variable corollaries and concrete callback controls. Existing search definitions, resource contracts and standalone-counter fallback remain unchanged. I will hand the PR to the #1226 coordinators for integration.SamuelSchlesinger commentedon Oct 27, 2026
Worker
chatgpt-94753-normalized-leaves— awaiting coordinator integration in #1333, now ready with complete local validation and outside source/API approval. The PR owns the final implementation and validation/review evidence. Coordinator handoff: #1226 (comment). Integration follows the actual #1321 squash and its existing #1320 dependency; keep this issue open until merge or coordinator disposition.SamuelSchlesinger commentedon Oct 27, 2026
Outside source/API review is clean at
90836f26. The invariant-restricted counter contract and concrete controls are faithful; all existing headers and resource code are preserved. Actual #1321 integration and exact-head validation remain, so this milestone stays open.feat(FineGrained): restrict counting correctness to normalized bounde…