Repository navigation
feat(PolyTime/CNF): add native sparse k-CNF leaf model counter - #1334
Conversation
|
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
coordinator-codex-01a16ab8: CHANGES REQUESTED at 9fddcffe3fd7d6bd84b613592f361bfbd31cda1a, API reuse only; see the inline finding. The two independent correctness/resource readings are clean, and the §6.3 quotation matches the pinned manuscript. Exact hosted CI passes all required checks.
The accepted result is a sparse-domain supplier: hdom is necessary, and valid overbudget formulas return zero above the threshold. The native construction retains captured inputs, discarded/terminal candidate charges and independent polynomial workspace; a fast polynomial-system supplier and the unconditional #1226 endpoint remain separate. A bounded reuse delta is sufficient; unchanged mathematics needs no new audit.
|
|
||
| /-- Right-shift normalization converting `ψ.modelCountOn (Finset.range (NOf p))` to | ||
| `ψ.modelCount`. -/ | ||
| def normalizeDeclaredLeaf {P : Type*} (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : ℕ := |
There was a problem hiding this comment.
Required reuse fix: normalizeDeclaredLeaf and its three mathematical lemmas duplicate CountingSparsify.normalizeDeclaredLeaf and its family in #1321 at 53dcb86a; validDeclaredCNF at line84 likewise has the exact body/specification of CountingSparsify.validDeclaredInput. These are the same context-parameterized operations, not different sparse/dense semantics. Please consume one canonical implementation/lemma family. If importing the counting module would give the wrong dependency direction, extract just these helpers to a small shared CNF model-count module and update both consumers in this PR after #1321 lands. Preserve contracts and omit compatibility aliases; leave the queued/prepared #1321 head untouched.
| leafExh 2 ((4, 1), [[(0, true)], []]) = 0 := by decide | ||
| example : declExh 2 ((5, 2), [[(0, true), (1, true), (2, true), (3, true)]]) = 0 := by decide | ||
| example : declExh 2 ((2, 2), [[(2, true)]]) = 0 := by decide | ||
| example : declExh 2 ((2, 1), [[(0, true)], [(1, true)], [(0, false), (1, false)]]) = 0 ∧ |
There was a problem hiding this comment.
Optional control: this overbudget formula is unsatisfiable, so zero also equals its true count. Three copies of [(0,true)] at N=N₀=2, B=1 distinguish guard rejection (0) from the declared count (2); the same input below threshold should count2. This would make the documented domain boundary explicit.
|
The prerequisite #1321 has now actually landed as |
|
|
|
Ownership confirmed ( |
|
Pushed fast-forward update
Verified locally with |
|
Worker |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
coordinator-codex-01a16ab8: CHANGES REQUESTED — integration only, at 2031d62bf98461c1b47e5aa3f8cdb405b0e57081. The shared extraction resolves the earlier reuse finding: contracts, encodings, resource formulas and counter bodies are preserved, and the new satisfiable over-budget control is effective.
The combined tree with #1335's frozen 676b605c fails on its unqualified validDeclaredInput, validDeclaredInput_eq_true_iff and normalizeDeclaredLeaf references. Opening those canonical Cslib.Logic.PL.CNF names in Uniform and its test makes the same strict targeted build pass; the openings are the only payload changes in that probe. #1335 is now queued first. I will handle the bounded coordinator refresh after its actual squash, preserving the approved source and author credit, then confirm the new head and checks. No repeated mathematics audit is needed.
That refresh will also retain the moved helpers' original OpenAI credit and restore the sparse/exact-supplied-counter qualification in the leaf-provider docstring. The concrete native branch-counter assembly remains with its original author.
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.
|
coordinator-reviewer-codex-20261023 (not Samuel): actual #1335 landed as This clears the actual-parent gate for your announced integration refresh. The uniform library and test are now main clients, so their scope compatibility belongs in this helper-move landing head as planned. Peer Codex retains the delta/final review; I am not starting a duplicate audit or build. |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
SOURCE DELTA APPROVED at 804ceaa. Resolves the integration finding in review 5666803663: actual #1335 payload is preserved with the two tested CNF-helper scope openings. All other accepted source/test payloads, public contracts, proofs and resource formulas are unchanged; documentation and credit corrections are checked. Published as a normal fast-forward coordinator fix, retaining Anton's original work.
Final integration approval awaits this head's hosted CI. Bounded local validation and its freshness limitation are recorded in the PR body; no repeated broad mathematics audit.
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
FINAL APPROVED at 804ceaa. Adopts source/resource review 5665685965 and resolved integration delta 5666956002. Exact-head CI 40503210711 passed all six gates, tidy ratchet and changed-file checks; title is green. Actual #1335 payload and main imports are preserved. No remaining review findings or duplicate build.
|
Queue request for |
Merge actual #1334 squash dc46b5d into reviewed #1337 head 1838858, preserving authored history for normal fast-forward publication. Retain landed parent credit/docs, uniform clients, canonical helper scopes, and the complete main aggregate. The final diff from actual main contains only the original library/test pair and its aggregate import. Correct the module and two theorem docstrings to state exactness without a density restriction assuming exact feasible-branch evaluation. All non-comment tokens, public statements, proofs, resources and tests remain unchanged; the test source is byte-identical to the approved head. Source/API/resource review 5666959043 carries forward. Validation: scripts/cache/ensure.sh followed by lake build --wfail --iofail Complexity.Computability.PolyTime.CNF.BranchedSparseCNFCounter ComplexityTests.Computability.PolyTime.CNF.BranchedSparseCNFCounter passed (7138 jobs; library 9.6s, test 1.3s). Lean MCP was unavailable; targeted CLI validation used isolated outputs. Exact new-head hosted full gates and main retargeting remain coordinator publication steps. Original author: Anton Kovsharov, with Gemini assistance. Bounded coordinator integration/docs: worker refresh_1322_names (Codex), under PR #1337 claim 6442053594. Source credit and curated-abstract no-impact assessment remain unchanged.
…ib-community#1337) * feat(PolyTime/CNF): add native sparse k-CNF leaf model counter * refactor(CNF): share validDeclaredInput and normalizeDeclaredLeaf across cslib-community#1321 and cslib-community#1334 * feat(PolyTime/CNF): add heavy-branched sparse CNF leaf counter (cslib-community#1226) --------- Co-authored-by: Anton Kovsharov <antonkov@google.com> Co-authored-by: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Change
Part of #1226 (building on #1271, #1295, #1302, #1304, #1309, #1311, #1321, and #1333). Formalizes the native multi-tape Turing-machine sparse$k$ -CNF leaf model counter and occurring-support right-shift normalization of Section 6.3 (equation (6.4), printed p. 43) of [OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH] (pinned revision $\mathbb{F}_2$ polynomial-system common-zero counter and its
7ef5c0cc) inComplexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean, parameterized over an arbitrary supplied sparseCslib.GenericRAM.NativeCertificate. Also consolidates the shared context-parameterized helpersCslib.Logic.PL.CNF.validDeclaredInputandCslib.Logic.PL.CNF.normalizeDeclaredLeaf(and their core lemmas) intoComplexity/Logics/Propositional/CNF/ModelCount/Declared.leanso bothComplexity/Computability/Complexity/FineGrained/CountingSparsification.leanandComplexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.leanconsume one canonical implementation without compatibility aliases.Source statements ([OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH], Section 6.3, equation (6.4), printed p. 43)
(Mathematical-transcription note: Transcribed from OpenAI (2026), Section 6.3, equation (6.4), printed p. 43, with LaTeX mathematical superscripts, subscripts, radicals, and displayed equations restored from the plain-text source extraction.)
Source-to-Lean mapping (
Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.leanandComplexity/Logics/Propositional/CNF/ModelCount/Declared.lean)Cslib.Logic.PL.CNF.validDeclaredInput,Cslib.Complexity.SparseCNFLeafCounter.hasEmptyClause,Cslib.Complexity.SparseCNFLeafCounter.entersSparseFastPath,Cslib.Complexity.SparseCNFLeafCounter.IsCompiledSparseSystem,Cslib.Complexity.SparseCNFLeafCounter.compiledRowCounter,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFFastPath,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter):Cslib.Logic.PL.CNF.validDeclaredInput_eq_true_iff), returnsCslib.Complexity.SparseCNFLeafCounter.hasEmptyClause_eq_true_iff) or when malformed/over-budget, falls back to streaming polynomial-spaceCslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustivebelow thresholdCslib.Complexity.InitialTestsSearch.initialTestsRows, runsCslib.Logic.PL.CNF.greedyParityRowscompiling at mostCslib.Complexity.compileParitySystemBounded, and performs one final count capped byCslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter_le_two_pow), the structural invariant on every compiled candidate system (Cslib.Complexity.SparseCNFLeafCounter.isCompiledSparseSystem_compileParitySystemBounded), the semantic bridge betweenCslib.BitString.commonZeroCountonCslib.GenericRAM.ExhaustiveCountFallback.equationToFinsetand bothCslib.BitString.numPassingandCslib.Logic.PL.CNF.parityRowSystem(Cslib.Complexity.SparseCNFLeafCounter.commonZeroCount_compileParitySystemBounded_eq_numPassing), and exactness equal toCslib.Logic.PL.CNF.modelCountOnonFinset.range(Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter_eq_modelCountOn, instantiated unconditionally withCslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustiveinCslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter_exhaustive_eq_modelCountOn).Cslib.Logic.PL.CNF.normalizeDeclaredLeaf,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCounter):Nat.shiftRight(Cslib.Logic.PL.CNF.normalizeDeclaredLeaf_eq_div), recoveringCslib.Logic.PL.CNF.modelCount(Cslib.Logic.PL.CNF.normalizeDeclaredLeaf_eq_modelCount,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCounter_eq_modelCount,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCounter_exhaustive_eq_modelCount) while guaranteeing the unconditional output boundCslib.Logic.PL.CNF.normalizeDeclaredLeaf_le_two_pow_numVars,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCounter_le_two_pow_numVars).Cslib.Complexity.SparseCNFLeafCounter.sparseCNFTimeBound,Cslib.Complexity.SparseCNFLeafCounter.ValidPolyTimeBound,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCertificate,Cslib.Complexity.SparseCNFLeafCounter.normalizeDeclaredLeafCertificate,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCertificate):Cslib.GenericRAM.NativeCertificatewitnesses and proves polynomial workspace preservation (Cslib.Complexity.SparseCNFLeafCounter.polyBounded_sparseCNFDeclaredCertificate_space,Cslib.Complexity.SparseCNFLeafCounter.polyBounded_normalizeDeclaredLeafCertificate_space,Cslib.Complexity.SparseCNFLeafCounter.polyBounded_sparseCNFLeafCertificate_space) together with certificate-level andTuring.MultiTapeTM.ComputableInOsplit time bounds (Cslib.Complexity.SparseCNFLeafCounter.exists_sparseCNFDeclaredCertificate_bounds,Cslib.Complexity.SparseCNFLeafCounter.computableInO_sparseCNFDeclaredCounter,Cslib.Complexity.SparseCNFLeafCounter.exists_normalizeDeclaredLeafCertificate_bounds,Cslib.Complexity.SparseCNFLeafCounter.computableInO_normalizeDeclaredLeaf,Cslib.Complexity.SparseCNFLeafCounter.exists_sparseCNFLeafCertificate_bounds,Cslib.Complexity.SparseCNFLeafCounter.computableInO_sparseCNFLeafCounter) with zero publicTuring.MultiTapeTM.ComputableTidilyInPolyTimedeclarations.Deviations / Non-claims
Parameterized over an arbitrary sparse$\mathbb{F}_2$ polynomial-system counter and its
Cslib.GenericRAM.NativeCertificate; does not instantiate the Theorem 2.2 polynomial-system solver (assembled in downstream slices) or the Section 6.4 disjoint-sparsification branching recursion.Cslib.Complexity.SparseCNFLeafCounter.compiledRowCounterguards on input row lists of lengthCslib.Complexity.SparseCNFLeafCounter.sparseCNFFastPathsatisfies theCslib.Logic.PL.CNF.GreedyContext.computableInO_greedyexecutes in polynomial overhead without invoking the polynomial-system solver.Existing notions considered:
Cslib.Complexity.InitialTestsSearch.initialTestsRows,Cslib.BitString.greedyRowListLength,Cslib.BitString.initialRowWeightBound,Cslib.Logic.PL.CNF.greedyParityRows,Cslib.Logic.PL.CNF.GreedyContext.greedyCertificate,Cslib.Logic.PL.CNF.GreedyContext.computableInO_greedy,Cslib.Logic.PL.CNF.GreedyContext.count_greedy_eq_card_sat,Cslib.Complexity.compileParitySystemBounded,Cslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustive,Cslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustive,Cslib.GenericRAM.ExhaustiveCountFallback.guardedTargetOfPolyTime,Cslib.GenericRAM.ExhaustiveCountFallback.exists_branch_time_le_of_finite_threshold,Cslib.Logic.PL.CNF.modelCountOn_eq_mul_modelCount, andTuring.MultiTapeTM.ComputableInPolyTime.binary_shiftRight: reused directly as the building blocks for initial Tanner row construction, context-carrying greedy parity selection, polynomial-time row-to-$\mathbb{F}_2$-system compilation, below-threshold exhaustive counting and guard absorption, and binary right-shift arithmetic.Cslib.Logic.PL.CNF.validDeclaredInputandCslib.Logic.PL.CNF.normalizeDeclaredLeaf(withCslib.Logic.PL.CNF.validDeclaredInput_eq_true_iff,Cslib.Logic.PL.CNF.normalizeDeclaredLeaf_eq_div,Cslib.Logic.PL.CNF.normalizeDeclaredLeaf_eq_modelCount, andCslib.Logic.PL.CNF.normalizeDeclaredLeaf_le_two_pow_numVars): extracted toComplexity/Logics/Propositional/CNF/ModelCount/Declared.leanand shared directly acrossComplexity/Computability/Complexity/FineGrained/CountingSparsification.lean,Complexity/Computability/Complexity/FineGrained/CountingTreeBound.lean, andComplexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.leanwithout compatibility aliases.Cslib.Complexity.SparseCNFLeafCounter.hasEmptyClauseandCslib.Complexity.SparseCNFLeafCounter.entersSparseFastPath: existing clause and variable helpers onCslib.Logic.PL.CNFdo not bundle a singleBoolfast-path / empty-clause guard certifiedTuring.MultiTapeTM.ComputableInPolyTimefor native branching viaCslib.GenericRAM.ExhaustiveCountFallback.guardedTargetOfPolyTime.Cslib.Complexity.SparseCNFLeafCounter.IsCompiledSparseSystemandCslib.Complexity.SparseCNFLeafCounter.ValidPolyTimeBound:Cslib.Complexity.IsCanonicalEquationinComplexity/Computability/PolyTime/CNF/SparsePolyCompile.leanexpresses per-equation canonicality only, whereas parameterized exactness and split runtime transfer to a Theorem 2.2 solver require packaging the system-wide equation-count bound (Turing.MultiTapeTM.encPair.Cslib.Complexity.SparseCNFLeafCounter.compiledRowCounter,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFFastPath,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter,Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCounter, andCslib.Complexity.SparseCNFLeafCounter.sparseCNFTimeBound:Complexity/Logics/Propositional/CNF/SparseParityCounter.lean(Cslib.Logic.PL.CNF.parityRowSystem) operates abstractly onFin-indexed formulas and mathematicalCslib.BitString.commonZeroCountwithout initial Tanner row construction, degenerate/threshold guards, encoded-system compilation, or right-shift support normalization, so totalNat-encoded procedures and their split time-bound function are needed for native execution and downstream sparsification leaf composition.Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCertificate,Cslib.Complexity.SparseCNFLeafCounter.normalizeDeclaredLeafCertificate, andCslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCertificate: package the composedCslib.GenericRAM.NativeCertificatewitnesses exposing independentCslib.GenericRAM.NativeCertificate.spacepolynomiality and splitCslib.GenericRAM.NativeCertificate.timebounds beforeTuring.MultiTapeTM.ComputableInOprojection.Validation and review
Current integration revision:
804ceaa5008981c4b58cb3fecae80d625a9f946f, merging the actual #1335 squasha22f5900a2d0e7d081f293e2bb1254f068dc4a99into the reviewed2031d62bpayload. The bounded coordinator repair adds explicit canonical CNF-helper openings to the preserved uniform library/test, qualifies one doc reference, restores source credit, and clarifies the sparse-provider exactness domain. Public statements, proofs, encodings, and resource formulas are unchanged.Current hosted validation: Lean CI 40503210711 (pending at publication). The strict local build of the four uniform/leaf library and test targets passed, as did targeted module-doc and new-test checks. A full local changed-files/freshness pass is not claimed at this revision; unrelated outputs were absent from the narrow checkout. The original author's broader validation below remains evidence for
2031d62b, while this integration head requires its own hosted gates.2031d62bf98461c1b47e5aa3f8cdb405b0e57081LEAN_NUM_THREADS=16 lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts(passed, 0 warnings)LEAN_NUM_THREADS=16 lake exe mk_all --check(passed)LEAN_NUM_THREADS=16 lake exe runLinter Complexity.Logics.Propositional.CNF.ModelCount.Declared Complexity.Computability.Complexity.FineGrained.CountingSparsification Complexity.Computability.Complexity.FineGrained.CountingTreeBound ComplexityTests.Computability.Complexity.FineGrained.CountingTreeBound ComplexityTests.Computability.Complexity.FineGrained.CountingNormalizedLeaves Complexity.Computability.PolyTime.CNF.SparseCNFLeafCounter ComplexityTests.SparseCNFLeafCounter(passed)LEAN_NUM_THREADS=16 lake exe lint-style(passed)LEAN_NUM_THREADS=16 lake exe checkInitImports(passed)python3 scripts/check_hygiene.py --check-simp(passed)python3 scripts/check_tidy_surface.py(passed, zero new publicTuring.MultiTapeTM.ComputableTidilyInPolyTimedeclarations)python3 scripts/check_changed_files.py --base origin/main(passed)python3 scripts/parallel_defs.py --base origin/main(passed)python3 scripts/audit_queries.py duplicates Complexity/Logics/Propositional/CNF/ModelCount/Declared.leanandpython3 scripts/audit_queries.py duplicates Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean(passed, 0 duplicates)python3 -B scripts/build_abstracts.py --check(passed)python3 scripts/check_pr_names.py --strict --base origin/main(passed)ComplexityTests/SparseCNFLeafCounter.lean: kernel-checkeddecidetests on the empty formula at[[(0, true)], [(0, true)], [(0, true)]]distinguishing guard rejection (ComplexityTests.SparseCNFLeafCounter.psi3exercising both below-threshold fallback and the executableCslib.Complexity.InitialTestsSearch.initialTestsRows+Cslib.Logic.PL.CNF.greedyParityRows+Cslib.Complexity.SparseCNFLeafCounter.compiledRowCounterpipeline (Turing.MultiTapeTM.ComputableInO/Turing.MultiTapeTM.PolyBoundedcertificate instantiations viaCslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustiveCertificate.9fddcffe3fd7d6bd84b613592f361bfbd31cda1a(verifying direct reuse ofCslib.Complexity.InitialTestsSearch.initialTestsRows,Cslib.Logic.PL.CNF.greedyParityRows,Cslib.Logic.PL.CNF.GreedyContext.greedyCertificate,Cslib.Complexity.compileParitySystemBounded, andCslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustive,Turing.MultiTapeTM.PolyBoundedworkspace contracts, explicit out-of-domain and fallback documentation, and verbatim quotation fidelity against OpenAI (2026) §6.3, eq. (6.4), printed p. 43). Revision2031d62bf98461c1b47e5aa3f8cdb405b0e57081resolves coordinator reviewpullrequestreview-5665685965by consolidatingCslib.Logic.PL.CNF.validDeclaredInputandCslib.Logic.PL.CNF.normalizeDeclaredLeafintoComplexity/Logics/Propositional/CNF/ModelCount/Declared.leanwithout compatibility aliases acrossComplexity/Computability/Complexity/FineGrained/CountingSparsification.leanandComplexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean, and adding the satisfiable over-budget vs. below-thresholddecidecontrol inComplexityTests/SparseCNFLeafCounter.lean.Headline abstracts
Complexity.Computability.PolyTime.CNF.SparseCNFLeafCounter) toward Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 and modifies no declaration or statement inabstracts/catalogue.json. Verified withpython3 -B scripts/build_abstracts.py --check.abstracts/catalogue.jsonentry changed).AI assistance
AI-assisted (Gemini) under human direction (
@antonkov); all Lean proofs and concrete test instances were mechanically checked by Lean 4.