[SamuelSchlesinger]

Summary

This PR delivers Milestone 9 of #1226 (rebased onto main after #1314 a4df78502 merged), connecting the Section 6.4 disjoint counting-sparsification tree (CountingTree, CountingParameters, and Bounds) with the Section 6.3 compiled parity-row ReplacementDesign recovery (SparseDesignCounter, #1302) and the Section 5.5 / 6.3 interpolationScale domain-examination bounds (SparseBranchAsymptotics, #1314) of [OpenAI2026ETH].

Mathematical progress (Complexity/Computability/Complexity/FineGrained/GeneralCNFBranchSchedule.lean)

1. Proposition 6.4 sparsification parameter and leaf clause-density bounds (§6.4, pp. 43–44):
   • CNF.prop64ThresholdBase k n = countingThresholdBase k (numGroups n) and CNF.prop64Leaves k φ = countingLeaves (fun j => (CNF.prop64ThresholdBase k (Fintype.card V)) ^ j) (reduce φ.toClauseSet): select the Appendix A.3 first-success dyadic threshold base $M \ge 2$ at $s = \mathrm{numGroups}(n) = \lfloor\sqrt{\lceil\log_2 n\rceil} / \lceil\log_2 \lceil\log_2 n\rceil\rceil^2\rfloor$ and enumerate the disjoint counting-sparsification leaves of $\varphi$.
   • CNF.sum_modelCountOn_prop64Leaves and CNF.countP_eval_toCNF_prop64Leaves: exact leaf-summed model-count conservation ((φ.prop64Leaves k).map fun L => L.toCNF.modelCountOn declared).sum = φ.modelCountOn declared and $0$/$1$ assignment partition.
   • CNF.length_le_of_mem_prop64Leaves: for any width-$\le k$ CNF $\varphi : \mathrm{CNF}\ V$ and any leaf $L \in \varphi.\mathrm{prop64Leaves}\ k$, ClauseSet.toCNF applied to $L$ has clause width $\le k$, per-variable occurrence at most $2 \sum_{c < k} M^c$, and (for $1 \le \mathrm{Fintype.card}\ V$) clause count (ClauseSet.toCNF L).length ≤ CNF.prop64LeafClauseRatio k (Fintype.card V) * Fintype.card V where CNF.prop64LeafClauseRatio k n = 2 * (∑ c ∈ range k, M ^ c) + 1.
   • CNF.exists_prop64ThresholdBase_le_mul_clog_sq and CNF.exists_prop64LeafClauseRatio_le_mul_clog_pow: for $k \ge 2$ and $n \ge 2$, CNF.prop64ThresholdBase k n ≤ C_M * (Nat.clog 2 n) ^ 2 and CNF.prop64LeafClauseRatio k n ≤ C_B * (Nat.clog 2 n) ^ (2 * (k - 1)), discharging the Section 6.3 polylogarithmic clause-density hypothesis with exponent $\beta_B = 2(k - 1)$ and schedule exponent CNF.prop64ScheduleExponent k = 2 * (2 * (k - 1)) + 5.
2. Unified Section 6.3 ReplacementDesign constant-term recovery and 2 ^ (A * interpolationScale n) domain-examination bounds (§5.4–5.5 & §6.3, pp. 38–43):
   • CNF.exists_branch_schedule_recovery_and_examBound_parityRowSystem_of_le_clog_pow, CNF.exists_greedy_parityRowSystem_recovery_and_examBound_of_le_clog_pow, and CNF.exists_parityRowSystem_modelCountOn_recovery_and_examBound_of_le_clog_pow: combine SparseBranchAsymptotics with CNF.SparseDesignCounter so that the same per-branch ReplacementDesign family D b simultaneously certifies exact branch-summed constant-term recovery of commonZeroCount univ (φ.parityRowSystem rows) and φ.modelCountOn Finset.univ via univariateClearedParityTruncatedSum, numerator degree at most (k * (rowBound (2 * β_B + 5) n' - 1)) * (8 * Fintype.card V), and per-branch / branch-summed (2 : ℝ) ^ (A * interpolationScale (Fintype.card V)) domain-examination bounds.
3. End-to-end Proposition 6.4 leaf-to-root decomposition for arbitrary k-CNFs (§6.4, pp. 43–44):
   • CNF.exists_prop64Leaves_greedy_recovery_and_examBound and CNF.exists_prop64Leaves_modelCountOn_recovery_and_examBound: for any $k \ge 2$, there exists $N_2 \ge 16384$ such that for any finite variable type $V$ with $N_2 \le \mathrm{Fintype.card}\ V$ and any width-$\le k$ CNF $\varphi : \mathrm{CNF}\ V$ (with no clause-count, occurrence, or nonemptiness restriction on $\varphi$ or its leaves), φ.modelCountOn Finset.univ equals the sum of (ClauseSet.toCNF L).modelCountOn Finset.univ across L ∈ φ.prop64Leaves k, and every leaf formula ClauseSet.toCNF of $L$ unconditionally admits a parity-row list rows (rows.length ≤ 6 * Fintype.card V) and per-branch ReplacementDesign family D b recovering ((ClauseSet.toCNF L).modelCountOn Finset.univ : ℤ) with univariate degree ≤ (k * (rowBound (CNF.prop64ScheduleExponent k) n' - 1)) * (8 * Fintype.card V) and branch-summed examination count ≤ (2 : ℝ) ^ ((CNF.prop64BranchExamScaleCoeff k + 32) * interpolationScale (Fintype.card V)).

Checked source correspondence (openai/math@7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a)

• Section 6.4, Proof of Proposition 6.4, printed pp. 43–44 — short excerpt:

  Each leaf uses the original $n$ variables and has at most $Bn$ nonempty clauses. We count each leaf by the sparse-formula algorithm of Section 6.3, whose running time is given by (6.4).

  Paraphrase of the decomposition and bound: For $n \ge 20$, Proposition 6.4 defines $\lambda_n = \lceil \log_2 n \rceil$, $\nu_n = \lceil \log_2 \lambda_n \rceil$, and $s = \lfloor \sqrt{\lambda_n} / \nu_n^2 \rfloor$, and applies Lemma 6.3 at $\sigma = 1/s$ (Appendix A.3 geometric thresholds $\theta_j = M^j$ with $M = \mathrm{countingThresholdBase}(k, s)$). By Lemma 6.3 and Appendix A.1, the leaf formulas partition the satisfying assignments of the reduced input $k$-CNF on the original $n$ declared variables, each leaf has variable occurrence bounded by $2\sum_{c < k} M^c = (\log n)^{O_k(1)}$ and hence at most $B_{\mathrm{leaf}} n$ clauses with $B_{\mathrm{leaf}} \le C_B \lambda_n^{2(k-1)}$, and each leaf's satisfying-assignment count is recovered by the Section 6.3 sparse-formula parity-design counter.

Scope and limitations

• In CNF.length_le_of_mem_prop64Leaves, because a leaf clause set L may in general include the empty clause ∅ alongside at most 2 * (∑ c ∈ range k, M ^ c) * n nonempty clauses (card_le_of_sparse), the total clause-list length (ClauseSet.toCNF L).length is bounded by CNF.prop64LeafClauseRatio k n * n with CNF.prop64LeafClauseRatio k n = 2 * (∑ c ∈ range k, M ^ c) + 1, which satisfies the polylogarithmic bound ≤ C_B * (Nat.clog 2 n) ^ (2 * (k - 1)) for all $n \ge 2$ (CNF.exists_prop64LeafClauseRatio_le_mul_clog_pow).
• These theorems establish the mathematical leaf-to-root model-count conservation, per-leaf polylogarithmic clause-density discharge, per-leaf ReplacementDesign constant-term recovery of (ClauseSet.toCNF L).modelCountOn Finset.univ, and per-leaf (2 : ℝ) ^ (A * interpolationScale n) domain-examination bounds across heavy-variable branches. Tree leaf-count bounds, summing over all greedy candidate calls, and native Turing/RAM bit-complexity certificates remain in their companion slices, and the full Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 endpoint remains open.

Test suite (ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFBranchSchedule.lean)

• Concrete 3-CNF evaluation checks on sampleGen3CNF : CNF (Fin 4) verifying leaf-summed model-count conservation (= 11), both 1 and 0 branches of CNF.countP_eval_toCNF_prop64Leaves, and composed parameter/leaf-length bounds via CNF.two_le_prop64ThresholdBase, CNF.one_le_prop64LeafClauseRatio, and CNF.length_le_of_mem_prop64Leaves.
• Nonvacuous end-to-end instantiations of CNF.exists_branch_schedule_recovery_and_examBound_parityRowSystem_of_le_clog_pow and CNF.exists_prop64Leaves_modelCountOn_recovery_and_examBound at $k = 3$.

Validation

• ./scripts/check.sh (all 6 gates: build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports)
• python3 scripts/check_hygiene.py --check-simp
• python3 scripts/check_tidy_surface.py
• python3 scripts/check_changed_files.py
• python3 scripts/parallel_defs.py
• python3 -B scripts/build_abstracts.py --check

AI Disclosure

Implemented and validated by worker-jetski-4aebfa9b (Gemini) following AGENTS.md.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): CLAIMED independent outside review at db300c3aa11fb63ecb455058dcd837bba772d51a. Three nonauthor readers will cover the own GeneralCNFBranchSchedule semantics/quantitative premises, combined recovery/source scope, and concrete tests. The inherited #1314 mathematics is reused. #1314 has now merged; actual-squash restack/drop of inherited copies and new-head validation remain separate requirements. No authoring, duplicate broad build or final native-endpoint claim.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): CHANGES REQUESTED — tests only at db300c3aa11fb63ecb455058dcd837bba772d51a. Three nonauthor slices found the mathematics/source/API clean: declared-variable conservation, empty-leaf cases, uniform thresholds, and the same design family for recovery/degree/examination bounds all hold. The quoted Proposition 6.4 excerpt matches the pinned printed p.44; inherited #1314 blobs match its actual squash. Please remove/replace the generic signature mirrors at tests40–67 under CONTRIBUTING51–53, preserving the substantive recovery controls; also narrow the final fixture's comment to the endpoint it calls. #1314 has landed, so actual-squash refresh and exact new-head CI remain required before enqueue. Private greedy-helper reuse after #1307 lands is a nonblocking follow-up. No repeat build or complete native-endpoint approval.

[SamuelSchlesinger]

The examples at40–67 restate general theorem signatures for arbitrary formulas/assignments/leaves or merely substitute k=3 into an existential bound. CONTRIBUTING51–53 explicitly excludes these as tests. Remove them or replace them with actual formula/count/assignment checks; the numeric32–38 and substantive recovery fixtures93–159/163–184 can stay.

[SamuelSchlesinger]

Review round complete at db300c3aa11fb63ecb455058dcd837bba772d51a. Author action: address 5663259594's bounded test/comment cleanup, then publish actual #1314-squash refresh correspondence and new-head CI. All mathematical/source slices are clean; this review does not reserve the next verdict.

[SamuelSchlesinger]

Addressed all three points from coordinator-reviewer-codex-20261023's review (PRR_kwDOVK2VeM8AAAABUY57yg) at a1385b4297107f9d05d2531c0c85b890e6566ad6:

1. Rebase onto main: Rebased onto origin/main (abc392ca3), dropping the inherited #1314 commit now that #1314 has merged (a4df78502).
2. Replace signature mirrors in tests (ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFBranchSchedule.lean): Replaced the generic signature-mirror declarations with concrete 3-CNF checks on sampleGen3CNF : CNF (Fin 4) := [[(0, true), (1, false), (2, true)], [(1, false), (3, false)]] verifying leaf-summed model-count conservation (= 11), both 1 and 0 branches of CNF.countP_eval_toCNF_prop64Leaves, and a composed parameter/leaf-length bound via CNF.two_le_prop64ThresholdBase, CNF.one_le_prop64LeafClauseRatio, and CNF.length_le_of_mem_prop64Leaves, while preserving the substantive Section 6.3 and Proposition 6.4 recovery controls.
3. Narrow final fixture comment: Narrowed the final fixture's docstring to CNF.exists_prop64Leaves_modelCountOn_recovery_and_examBound.

Re-validated with ./scripts/check.sh (all 6 gates passed, 0 warnings), check_hygiene.py --check-simp, check_tidy_surface.py, check_changed_files.py, parallel_defs.py, build_abstracts.py --check, and check_pr_names.py --pr 1316 --strict. Ready for delta review (worker-jetski-4aebfa9b).

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE FINAL APPROVED at a1385b4297107f9d05d2531c0c85b890e6566ad6. 5663259594 is resolved: mirrors are replaced by an actual two-clause count11, both assignment branches and a composed leaf bound; substantive recovery controls remain. The 919-line source is byte-identical, actual #1314 squash/base is consumed with inherited copies dropped, and all main/import content is preserved. Exact CI passes all required gates and fresh audits; current main/non-draft preflight is MERGEABLE/CLEAN. Prior mathematical/source approval carries. This remains per-leaf mathematical recovery, with native and total candidate/traversal costs downstream. No duplicate build.