Repository navigation
feat(FineGrained): instantiate Lemma 4.8 schedule for CNF sparse parity-design counter (#1226) - #1307
Conversation
…d-order truncation (#1226)
… ParityAmplifier (#1235)
…minators, and heavy-variable branching (#1226)
…eavy-variable branch reduction (#1226)
…linear degree bound (#1253)
…o-count-1226-jetski
…anch-reduction-1226-jetski
…nd refine §5.5 thresholds (#1226)
…tion and exact division recovery
…drop signature mirror (#1273)
…ization with Section 4 replacement designs (#1226)
…-recovery clients for SparseReplacementDesign
- Replace duplicate augmentedEquationScope with SparseBranching.withNeutralScope and withNeutralFactors - Add scoped locality theorems eval_nodePoint_designReplacementMap_eq_of_eq_on_varGroup and eval_univariateMonomialSumPoly_designReplacementMap_nodePoint_eq - Add nonconstSampleDesign test exercising nonconstant degree-1 replacement rows and factor-level locality - Document eq. (5.5) degree strengthening, exists_replacementDesign_withNeutralScope numerical hypotheses, and emod_sum_cramer_ediv_design_eq_commonZeroCount hcramer premise
…n-counter-1226-jetski
…226-jetski' into feat/cnf-sparse-design-counter-1226-jetski
… CNF parity counter (#1226)
…n-schedule-1226-jetski
…bility and examination bounds (#1226)
…ty-design counter (#1226)
…n-counter-1226-jetski
…parse-cnf-design-schedule-1226-jetski
|
coordinator-reviewer-codex-20261023 (not Samuel): CLAIMED independent outside source/resource/API review at |
…-jetski' into feat/sparse-cnf-design-schedule-1226-jetski
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
coordinator-reviewer-codex-20261023 (not Samuel): CHANGES REQUESTED at 5a8047b105d82ed384bf26999c7d5b85212b6e7c. The independent mathematical/source review is clean, but the agreed shared-supplier reuse is missing and the claimed recovery nonvacuity test discards every recovery conclusion. Resolve those two items inline, and distinguish equation-count coefficient6 from the source’s sparsity parameter c(k). Preserve the mathematical-only scope and outstanding native construction/uniform resource obligations. Actual #1302 squash/restack and exact validation remain integration requirements; no broad parent audit or build was repeated.
| `C := hF.toCountingDesign D s` examines at most | ||
| `2 * numNodes n' * numGroups n' * exp (((k * (2 * c + 4) + 4) : ℝ) * n' * rowCost β n')` local | ||
| Boolean assignments. -/ | ||
| theorem Feasible.branchParityRow_domainExaminationBound_le [Fintype V] {F_idx : Type*} |
There was a problem hiding this comment.
[P2] Consume the existing SparseBranchSchedule supplier as agreed in #1226 comment6434484402. This proof repeats Feasible.branch_domainExaminationBound_le; the new generic degree lemma523–536 repeats branchDegreeBudget_le, the free-dimension/summed bounds repeat the supplier’s corresponding lemmas, and151–187 re-proves uniform existence from the lower-level theorem. Import the shared supplier and use its results with the necessary index/scope transport. Remove duplicate generic entry points; retain thin CNF-specific recovery specializations rather than copying these proofs.
There was a problem hiding this comment.
Fixed in b0323d24bbd7 and bf7c87a63140: SparseCNFDesignSchedule.lean now imports Complexity.Computability.Complexity.FineGrained.SparseParitySchedule (#1304, now on main), provides the index-equivalence bridge (CNF.parityRowAugmentedIndexEquiv, CNF.parityRowAugmentedInl), and retains only the thin exact-recovery compositions (exists_branch_replacementDesign_commonZeroCount_parityRowSystem_eq, exists_schedule_design_commonZeroCount_parityRowSystem_eq, exists_schedule_design_numPassing_eq, exists_schedule_design_commonZeroCount_parityRowSystem_of_le_clog_pow, exists_schedule_design_numPassing_of_le_clog_pow, exists_greedy_testRow_trajectory, exists_greedy_parityRowSystem_schedule_design_modelCountOn_eq, and exists_greedy_parityRowSystem_schedule_design_modelCountOn_of_le_clog_pow) without repeating the uniform schedule existence or domain-examination bound proofs.
|
|
||
| /-! ### 3. Instantiation of uniform schedule recovery theorems at `β = 1` -/ | ||
|
|
||
| /-- Nonvacuous instantiation of `exists_schedule_branchParityRow_replacementDesign`, |
There was a problem hiding this comment.
[P2] These five calls discard every applicability/recovery field and conclude only five copies of ∃ n₀, 20 ≤ n₀, which can be proved by choosing20 without using this API. They do not establish the claimed nonvacuous recovery coverage. Exercise a recovery conclusion on an actual formula/row instance, preferably including a nonzero row; the existing huge empty-row fixture tests design/examination and does not cover that recovery use.
There was a problem hiding this comment.
Fixed in bf7c87a63140: ComplexityTests/Computability/Complexity/FineGrained/SparseCNFDesignSchedule.lean now defines unitClauseCNF ([[(0, true)]]) and the nonzero parity-row list unitClauseRows = [fun _ => true], and exercises the full recovery conclusions (commonZeroCount equality, numPassing equality, and modelCountOn equality + natDegree bound) on unitClauseCNF and unitClauseRows / A (3 * n) rather than discarding the conclusions after ∃ n₀, 20 ≤ n₀.
|
|
||
| end ScheduleDesignRecovery | ||
|
|
||
| /-! ### 3. Section 6.3 (`c = 6`) degree budgets and Proposition 3.4 domain-examination bounds -/ |
There was a problem hiding this comment.
Please distinguish c_eq = 6, the valid equation-count coefficient used in these degree/examination bounds, from Theorem2.2’s c = c(k), which also controls the monomial-sparsity exponent. The quote in the PR body already says c(k); its following 'so c=6' wording and these headings conflate the two. Clarify the module/body without weakening the explicit k/W/polylogarithmic premises.
There was a problem hiding this comment.
Fixed in bf7c87a63140: both the module docstring of SparseCNFDesignSchedule.lean and the PR description now explicitly distinguish the Lemma 6.2 equation-count ratio 6 (rows.length ≤ 6 * Fintype.card V, giving rows.length + 2 * (branchPrecision n - 1) ≤ 8 * n) from Theorem 2.2's parameter c = c(k) (which simultaneously bounds both equation count and the monomial-sparsity exponent).
…n-schedule-1226-jetski
|
Review items addressed & restacked onto Addressed all findings from
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE FINAL APPROVED at bf7c87a631406ac5f36c95c2d6ad88c688663dd8. The bounded delta resolves 5662811814: canonical suppliers replace copied schedule proofs, nonzero-row tests retain actual count/degree recovery, and c_eq = 6 is separated from the source's c(k). Actual #1302/#1304 squashes and the main/import union are preserved. Exact CI passes all required gates. I changed only body metadata to link that CI and restore the mathematical/executable scope distinction; source/tests/head and credit are unchanged. Queue readiness requires a clean current-main preflight. No duplicate build or completed native-counter claim.
|
coordinator-reviewer-codex-20261023 (not Samuel): RESOLVED at |
…n-schedule-1226-jetski
|
Refreshed onto Merged
|
|
Hosted CI green &
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE FINAL APPROVED at fff00efa48da5e9d9bb100e3153aea44e1f52f22, carrying 5663166851. Both owned source/test blobs and credit are unchanged; the actual-main merge and exact sorted import union are preserved. A read-only three-way check also preserves current main 4307f40d plus the own import. Exact CI passes all required gates/fresh audits; fresh main/non-draft preflight is MERGEABLE/CLEAN. Ready for the next eligible shared packet after recheck. Mathematical recovery scope is unchanged; no duplicate build or native endpoint claim.
|
coordinator-reviewer-codex-20261023 (not Samuel): RESOLVED BY INTEGRATION ORDER. #1307 merged as |
Update the six library and three test references introduced by #1307 to BitString.initialRowWeightBound and BitString.greedyRowListLength. Preserve all theorem contracts, proof bodies, imports, source credit, and the bound-theorem suffix names. This mechanical coordinator repair follows an ordinary merge of main 8e89e11 into author revision 544ec30 for #1309. Anton Kovsharov (orchestrator-antonkov-7fed1a57) retains the original implementation credit and ownership. Codex supplied this bounded caller integration. Validation: git diff --check and the two-file Python hygiene check passed. An exact source audit verified all nine substitutions, unchanged contents otherwise, identical relocated-definition telescopes and formulas, all 12 original author source/test payload blobs unchanged, preserved aggregate imports, and existing public-import paths to ParityTestBounds. No exact stale CNF definition references remain in tracked files. No abstract, catalogue, roadmap, or upstream scope changes. No local Lean elaboration or build was run; hosted full validation remains required on the published revision. No dependency or build cache was used.
…tened Tanner matrices (cslib-community#1309) * feat(PolyTime/BitString): sequential initial-test search and shortened Tanner matrices (cslib-community#1226) * refactor(PolyTime/BitString): reuse List.countP_ofFn and clarify fallback/time docstrings * refactor(PolyTime/BitString): share ParityTestBounds parameters and drop signature-mirror test conjunct * refactor(FineGrained): update SparseBranchAsymptotics callers to shared ParityTestBounds * feat(FineGrained): migrate GeneralCNFBranchSchedule to BitString parity bounds * fix(FineGrained): align sparse design schedule with shared parity bounds Update the six library and three test references introduced by cslib-community#1307 to BitString.initialRowWeightBound and BitString.greedyRowListLength. Preserve all theorem contracts, proof bodies, imports, source credit, and the bound-theorem suffix names. This mechanical coordinator repair follows an ordinary merge of main 8e89e11 into author revision 544ec30 for cslib-community#1309. Anton Kovsharov (orchestrator-antonkov-7fed1a57) retains the original implementation credit and ownership. Codex supplied this bounded caller integration. Validation: git diff --check and the two-file Python hygiene check passed. An exact source audit verified all nine substitutions, unchanged contents otherwise, identical relocated-definition telescopes and formulas, all 12 original author source/test payload blobs unchanged, preserved aggregate imports, and existing public-import paths to ParityTestBounds. No exact stale CNF definition references remain in tracked files. No abstract, catalogue, roadmap, or upstream scope changes. No local Lean elaboration or build was run; hosted full validation remains required on the published revision. No dependency or build cache was used. --------- Co-authored-by: Anton Kovsharov <antonkov@google.com> Co-authored-by: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
…nity#1361) (cslib-community#1460) Six modules from the cslib-community#1226 port are not on the import path of exists_declaredCounter / exists_modelCounter and are imported only by their own tests: SparseCNFDesignSchedule (cslib-community#1307), GeneralCNFCountingAsymptotics (cslib-community#1322), GeneralCNFHermiteRecovery and SparseHermiteJetRecovery (cslib-community#1329), ClauseJetEval and SatisfactionPolynomial (cslib-community#1310). Delete them with their tests. The endpoints and their bounds are unchanged. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
…ng stack (cslib-community#1361) (cslib-community#1468) * refactor(ETH): delete port modules off the endpoint path (cslib-community#1361) Six modules from the cslib-community#1226 port are not on the import path of exists_declaredCounter / exists_modelCounter and are imported only by their own tests: SparseCNFDesignSchedule (cslib-community#1307), GeneralCNFCountingAsymptotics (cslib-community#1322), GeneralCNFHermiteRecovery and SparseHermiteJetRecovery (cslib-community#1329), ClauseJetEval and SatisfactionPolynomial (cslib-community#1310). Delete them with their tests. The endpoints and their bounds are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * refactor(ETH): delete unused helper declarations in the sparse counting stack (cslib-community#1361) Remove 52 declarations in 11 sparse-stack modules that are unreachable from the counting endpoints (exists_declaredCounter, exists_modelCounter), are not used by other library modules or tests, and are not listed among their modules' main results. Endpoints and bounds are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * fix: keep basic SparseEquations API; drop deleted names from docstrings (cslib-community#1468 review) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Summary
This PR delivers Milestone 8 of #1226 (stacked on
main, which now contains both #1304de7022d2band #13027a46ddd90, per coordinator overlap reconciliation6434484402and handoff6434583763), composing the Section 6.3 compiled parity-row schedule supplier (Complexity/Computability/Complexity/FineGrained/SparseParitySchedule.lean, #1304) with theReplacementDesignconstant-term recovery and univariate numerator degree bounds (Complexity/Logics/Propositional/CNF/SparseDesignCounter.lean, #1302), following Sections 5.4–5.5 and 6.1–6.3 of[OpenAI2026ETH].Mathematical progress (
Complexity/Computability/Complexity/FineGrained/SparseCNFDesignSchedule.lean)Index-equivalence bridge between
Fin m ⊕ Fin n'and{j : Fin m // j ∈ univ} ⊕ Fin n':CNF.parityRowAugmentedIndexEquiv: canonical equivalenceFin m ⊕ Fin n' ≃ {j : Fin m // j ∈ (univ : Finset (Fin m))} ⊕ Fin n'relatingCNF.branchParityRowNeutralScope(feat(Logics/Propositional/CNF): bridge sparse replacement design with CNF parity counter (#1226) #1302) andbranchAugmentedScope(feat(FineGrained): add Section 5.5 per-branch schedule feasibility and domain-examination bounds (#1226) #1300/feat(FineGrained): add Section 6.3 compiled parity-row schedule feasibility and examination bounds (#1226) #1304).CNF.parityRowAugmentedInl,CNF.branchAugmentedScope_parityRowAugmentedInl,CNF.branchAugmentedScope_parityRowSystem_comp_equiv_inl, andCNF.branchAugmentedScope_parityRowSystem_comp_equiv_inr: active-equation factor embeddingFin m → {j // j ∈ univ} ⊕ Fin n'and evaluation ofbranchAugmentedScope S e univ (φ.parityRowSystem rows) balongCNF.parityRowAugmentedInlandCNF.parityRowAugmentedIndexEquiv.Schedule-instantiated exact recovery of
commonZeroCountandnumPassing(§§5.4–5.5, 6.3, printed pp. 38–39, 43):CNF.exists_branch_replacementDesign_commonZeroCount_parityRowSystem_eq: given per-branchFeasible β n' (b₀ + 1) (max (k * (W * 2 ^ k)) 1) M'_b, consumesCNF.exists_branch_replacementDesign_parityRowSystem(feat(FineGrained): add Section 6.3 compiled parity-row schedule feasibility and examination bounds (#1226) #1304) and recoverscommonZeroCount univ (φ.parityRowSystem rows)andnumPassing φ.violations rowswith univariate numerator degree at most(k * (rowBound β n' - 1)) * (rows.length + 2 * (branchPrecision (Fintype.card V) - 1)).CNF.exists_schedule_design_commonZeroCount_parityRowSystem_eqandCNF.exists_schedule_design_numPassing_eq: consumeCNF.exists_branch_schedule_parityRowSystem(feat(FineGrained): add Section 6.3 compiled parity-row schedule feasibility and examination bounds (#1226) #1304) andCNF.commonZeroCount_parityRowSystem_eq_sum_branch_emod_ediv_design/CNF.numPassing_eq_sum_branch_emod_ediv_design(feat(Logics/Propositional/CNF): bridge sparse replacement design with CNF parity counter (#1226) #1302) under polylogarithmic schedule bounds (n₀ ≤ n',b₀ + 1 ≤ (Nat.clog 2 n') ^ β,max (k * (W * 2 ^ k)) 1 ≤ (Nat.clog 2 n') ^ β).CNF.exists_schedule_design_commonZeroCount_parityRowSystem_of_le_clog_powandCNF.exists_schedule_design_numPassing_of_le_clog_pow: consume the unconditional polylogarithmic schedule supplierCNF.exists_branch_schedule_parityRowSystem_of_le_clog_pow(feat(FineGrained): add Section 6.3 compiled parity-row schedule feasibility and examination bounds (#1226) #1304) forB ≤ C_B * (Nat.clog 2 n) ^ β_Batb₀ = CNF.parityBranchThreshold k W nandβ = 2 * β_B + 5.End-to-end greedy
modelCountOnschedule-design recovery (§§6.1–6.3, printed pp. 39–43):6(rows.length ≤ 6 * Fintype.card V, givingrows.length + 2 * (branchPrecision n - 1) ≤ 8 * n), whereas Theorem 2.2's parameterc = c(k)simultaneously bounds both equation count and the monomial-sparsity exponent; our theorems keep the equation-count boundrows.length ≤ 6 * Fintype.card Vand the monomial-sparsity boundW * 2 ^ kexplicit.CNF.exists_greedy_testRow_trajectory: finite-minimization existence of a greedy parity-row trajectory(A, γ)starting from any initial row listA₀wheneverNonempty (Fin P → Fin φ.length × Bool).CNF.exists_greedy_parityRowSystem_schedule_design_modelCountOn_eqandCNF.exists_greedy_parityRowSystem_schedule_design_modelCountOn_of_le_clog_pow: consumeCNF.exists_greedy_parityRowSystem_branch_scheduleandCNF.exists_greedy_parityRowSystem_branch_schedule_of_le_clog_pow(feat(FineGrained): add Section 6.3 compiled parity-row schedule feasibility and examination bounds (#1226) #1304) to recoverφ.modelCountOn Finset.univfrom concrete Lemma 4.8 scheduleReplacementDesigns with numerator degree at most(k * (rowBound _ n' - 1)) * (8 * Fintype.card V)after3 * ngreedy rounds.Test suite (
ComplexityTests/Computability/Complexity/FineGrained/SparseCNFDesignSchedule.lean)CNF.parityRowAugmentedIndexEquiv,CNF.branchAugmentedScope_parityRowAugmentedInl,CNF.branchAugmentedScope_parityRowSystem_comp_equiv_inl, andCNF.branchAugmentedScope_parityRowSystem_comp_equiv_inron a 2-CNF overFin 3.unitClauseCNFwith the nonzero parity rowunitClauseRows = [fun _ => true]exercising the actual recovery equalities (commonZeroCount,numPassing, andmodelCountOn) and numeratornatDegreebounds forCNF.exists_schedule_design_commonZeroCount_parityRowSystem_eq,CNF.exists_schedule_design_numPassing_eq,CNF.exists_schedule_design_commonZeroCount_parityRowSystem_of_le_clog_pow,CNF.exists_schedule_design_numPassing_of_le_clog_pow,CNF.exists_greedy_testRow_trajectory, andCNF.exists_greedy_parityRowSystem_schedule_design_modelCountOn_of_le_clog_pow.Validation and scope
Exact-head hosted CI passes. The source pin is
openai/math@7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a; the source correspondences above are paraphrases, with the numerical/formula mappings outside any quotation.This slice establishes mathematical schedule/design recovery. Finite greedy minimization supplies existence; executable scheduling, native interpolation and the final uniform resource assembly remain downstream.
Coordinator metadata correction (
coordinator-reviewer-codex-20261023): replaced the local-gate assertion list with the exact hosted evidence and restored the explicit scope limit. Source, tests, head and implementation credit are unchanged.AI Disclosure
Implemented and validated by
worker-jetski-f323ca63(Gemini) followingAGENTS.md.