From 734e8524721bcda3599a69ddded024d8a6433f96 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Tue, 27 Oct 2026 08:20:51 +0000 Subject: [PATCH 1/2] feat(FineGrained): add Section 6.4 Proposition 6.4 tree-wide recovery and candidate-indexed examination bounds (#1226) --- Complexity.lean | 1 + .../GeneralCNFCountingAsymptotics.lean | 1096 +++++++++++++++++ .../GeneralCNFCountingAsymptotics.lean | 327 +++++ 3 files changed, 1424 insertions(+) create mode 100644 Complexity/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean create mode 100644 ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean diff --git a/Complexity.lean b/Complexity.lean index 3399f95a4..6f3dadcd7 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -770,6 +770,7 @@ public import Complexity.Computability.Complexity.FineGrained.CountingTreeBound public import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch public import Complexity.Computability.Complexity.FineGrained.Exponents public import Complexity.Computability.Complexity.FineGrained.GeneralCNFBranchSchedule +public import Complexity.Computability.Complexity.FineGrained.GeneralCNFCountingAsymptotics public import Complexity.Computability.Complexity.FineGrained.GraphProblems public import Complexity.Computability.Complexity.FineGrained.OrthogonalVectors public import Complexity.Computability.Complexity.FineGrained.PPZ diff --git a/Complexity/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean b/Complexity/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean new file mode 100644 index 000000000..4efcb18cc --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean @@ -0,0 +1,1096 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Computability.Complexity.FineGrained.GeneralCNFBranchSchedule +public import Complexity.Computability.Complexity.FineGrained.SparseCountingScale +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingTreeBounds + +/-! +# Section 6.4 Proposition 6.4 tree-wide model-count recovery and total examination bounds + +This module combines the Section 6.4 disjoint sparsification leaf-to-root `ReplacementDesign` +recovery and per-leaf examination bounds +(`Complexity.Computability.Complexity.FineGrained.GeneralCNFBranchSchedule`), the branch-word +representation bridge and `2 ^ (n / B + 1)` leaf-count bounds for normalized clause sets +(`Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingTreeBounds`), and the +asymptotic `interpolationScale` tree-exponent and candidate-query overhead bounds +(`Complexity.Computability.Complexity.FineGrained.SparseCountingScale`) of +[OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] (printed pp. 38–47): + +1. **Normalized Proposition 6.4 leaf decomposition (`CNF.prop64NormalizedLeaves`)**: + Normalizing an arbitrary `k`-CNF `φ : CNF V` via `reduce (nontautological φ.toClauseSet)` before + applying `countingLeaves` at geometric threshold schedule + `θ j = (CNF.prop64ThresholdBase k (Fintype.card V)) ^ j` preserves `CNF.modelCountOn declared` + (`CNF.sum_modelCountOn_prop64NormalizedLeaves`) and the exact `0`/`1` assignment partition + (`CNF.countP_eval_toCNF_prop64NormalizedLeaves`) unconditionally (even when `φ` contains + tautological or duplicate clauses), while ensuring every leaf `L ∈ φ.prop64NormalizedLeaves k` is + sparse, reduced, nontautological, of clause width `≤ k`, and of clause length at most + `CNF.prop64LeafClauseRatio k (Fintype.card V) * Fintype.card V` + (`CNF.length_le_of_mem_prop64NormalizedLeaves`). +2. **Proposition 6.4 tree leaf-count bounds against `numGroups` and `interpolationScale`**: + - `CNF.length_prop64NormalizedLeaves_le_two_pow`: whenever `1 ≤ numGroups (Fintype.card V)` and + `∀ c ∈ φ, c.length ≤ k`, + `(φ.prop64NormalizedLeaves k).length ≤ 2 ^ (Fintype.card V / numGroups (Fintype.card V) + 1)`. + - `CNF.length_prop64NormalizedLeaves_le_interpolationScale_of_clog_ge` and + `CNF.length_prop64NormalizedLeaves_le_interpolationScale`: whenever + `640000 ≤ Nat.clog 2 (Fintype.card V)` (in particular for `2 ^ 640000 ≤ Fintype.card V`), + `1 ≤ interpolationScale (Fintype.card V)` and + `((φ.prop64NormalizedLeaves k).length : ℝ) ≤` + `(2 : ℝ) ^ (17 * interpolationScale (Fintype.card V))`. +3. **Lemma 6.2 candidate-query indexing, overhead, and full Proposition 6.4 tree-wide + `interpolationScale` examination bounds**: + - `CNF.LeafCandidateQueryIndex V B ψ` and `CNF.candidateQueryRows A q`: index all parity-row + systems evaluated during the `3 * n` greedy rounds of Lemma 6.2 (`Sum.inl (i, γ')` for + `i : Fin (3 * Fintype.card V)` and ordered candidate list + `γ' : Fin (CNF.greedyRowListLength B ψ.length) → Fin ψ.length × Bool`, including discarded + candidates counted with list multiplicity, plus `Sum.inr ()` for the final query + `A (3 * Fintype.card V)`), with exact cardinality + `3 * Fintype.card V * (2 * ψ.length) ^ P + 1 ≤ CNF.leafCandidateQueryBound B ψ` + (`CNF.card_leafCandidateQueryIndex_eq`, `CNF.card_leafCandidateQueryIndex_le`). + - `CNF.candidateQueryRows_length_and_weight_le`: every candidate or final query + `q : CNF.LeafCandidateQueryIndex V B ψ` has at most `6 * Fintype.card V` parity rows, each of + Hamming weight at most `CNF.initialRowWeightBound B ψ.length`. + - `CNF.greedyRowListLength_le_mul_pow_clog` and + `CNF.exists_prop64_leafCandidateQueryBound_le_interpolationScale`: prove + `CNF.greedyRowListLength B m ≤ 20000 * B ^ 2 * (Nat.clog 2 (2 * m + 4)) ^ 2` for all `B, m` + and apply `SparseCountingScale.eventually_query_overhead_poly_le` to bound + `(CNF.leafCandidateQueryBound B ψ : ℝ) ≤ (2 : ℝ) ^ interpolationScale (Fintype.card V)` for + every Proposition 6.4 leaf formula `ψ = L.toCNF`. + - `CNF.exists_prop64NormalizedLeaves_greedy_total_recovery_and_examBound` and + `CNF.exists_prop64NormalizedLeaves_total_recovery_and_examBound`: for any `k ≥ 2`, there + exists `N₃ ≥ 2 ^ 640000` such that for any finite variable type `V` with + `N₃ ≤ Fintype.card V` and any width-`≤ k` CNF `φ : CNF V`: + - `φ.modelCountOn Finset.univ` equals the sum of `L.toCNF.modelCountOn Finset.univ` across + `L ∈ φ.prop64NormalizedLeaves k`, + - `(φ.prop64NormalizedLeaves k).length ≤ 2 ^ (Fintype.card V / numGroups (Fintype.card V) + 1)` + and `((φ.prop64NormalizedLeaves k).length : ℝ) ≤` + `(2 : ℝ) ^ (17 * interpolationScale (Fintype.card V))`, + - on every leaf `L ∈ φ.prop64NormalizedLeaves k` (`ψ := L.toCNF`), **every** evaluated query + `q : CNF.LeafCandidateQueryIndex V B ψ` (including every discarded candidate + `A i.1 ++ [testRow γ']` for `i < 3 * Fintype.card V` and `γ'` as well as the final query + `A (3 * Fintype.card V)` at `q = Sum.inr ()`, which recovers `ψ.modelCountOn Finset.univ`) + admits concrete per-branch `ReplacementDesign`s `D b` recovering + `commonZeroCount univ (ψ.parityRowSystem (CNF.candidateQueryRows A q))` with branch-summed + examination count + `≤ (2 : ℝ) ^ ((CNF.prop64BranchExamScaleCoeff k + 32) * interpolationScale n)`, + and summing across all `q : CNF.LeafCandidateQueryIndex V B ψ` bounds the leaf's total + candidate-query examination count by + `(2 : ℝ) ^ (CNF.prop64LeafQueryExamScaleCoeff k * interpolationScale n)`, and + - summing across all leaves in `φ.prop64NormalizedLeaves k` bounds the tree-wide examination + count by `(2 : ℝ) ^ (CNF.prop64TreeExamScaleCoeff k * interpolationScale (Fintype.card V))` + and the total candidate-indexed examination count across the entire sparsification tree by + `(2 : ℝ) ^ (CNF.prop64TotalExamScaleCoeff k * interpolationScale (Fintype.card V))`. + +## Main definitions + +* `Cslib.Logic.PL.CNF.prop64NormalizedLeaves` +* `Cslib.Logic.PL.CNF.leafCandidateQueryBound` +* `Cslib.Logic.PL.CNF.LeafCandidateQueryIndex` +* `Cslib.Logic.PL.CNF.candidateQueryRows` +* `Cslib.Logic.PL.CNF.prop64LeafQueryExamScaleCoeff` +* `Cslib.Logic.PL.CNF.prop64TreeExamScaleCoeff` +* `Cslib.Logic.PL.CNF.prop64TotalExamScaleCoeff` + +## Main results + +* `CNF.card_leafCandidateQueryIndex_eq` +* `CNF.card_leafCandidateQueryIndex_le` +* `CNF.sum_modelCountOn_prop64NormalizedLeaves` +* `CNF.countP_eval_toCNF_prop64NormalizedLeaves` +* `CNF.length_le_of_mem_prop64NormalizedLeaves` +* `CNF.length_prop64NormalizedLeaves_le_two_pow` +* `one_le_interpolationScale_of_clog_ge` +* `CNF.length_prop64NormalizedLeaves_le_interpolationScale_of_clog_ge` +* `CNF.length_prop64NormalizedLeaves_le_interpolationScale` +* `CNF.greedyRowListLength_le_mul_pow_clog` +* `CNF.length_candidateQueryRows_le_of_step` +* `CNF.weight_mem_candidateQueryRows_le_of_step` +* `CNF.candidateQueryRows_length_and_weight_le` +* `CNF.sum_leafCandidateQueryIndex_le` +* `CNF.exists_leafCandidateQueryBound_le_interpolationScale` +* `CNF.exists_prop64_leafCandidateQueryBound_le_interpolationScale` +* `CNF.exists_prop64NormalizedLeaves_greedy_total_recovery_and_examBound` +* `CNF.exists_prop64NormalizedLeaves_total_recovery_and_examBound` + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] + (Sections 6.1–6.4, pp. 39–44; Appendix A, pp. 44–47) +-/ + +public noncomputable section + +namespace Cslib.Logic.PL + +open Filter Finset +open Cslib.BitString +open Cslib.LinearAlgebra +open Cslib.Logic.PL.ClauseSet.Sparsification +open Cslib.Complexity.SubexponentialSAT +open Cslib.Complexity.SubexponentialSAT.ReplacementParams +open Cslib.Complexity.SubexponentialSAT.SparseCountingScale + +variable {V : Type*} {n' : ℕ} + +/-! ### 1. Normalized Proposition 6.4 leaf decomposition (`CNF.prop64NormalizedLeaves`) -/ + +/-- The normalized Proposition 6.4 disjoint counting-sparsification leaf list of `φ : CNF V` +obtained by filtering tautological clauses (`nontautological`) and reducing by subsumption +(`reduce`) before applying `countingLeaves` at geometric threshold schedule +`θ j = (CNF.prop64ThresholdBase k (Fintype.card V)) ^ j` +([OpenAI2026ETH], Lemma 6.3, Proposition 6.4, and Appendix A.1–A.3, pp. 43–47). -/ +@[expose] def CNF.prop64NormalizedLeaves (k : ℕ) [Fintype V] [DecidableEq V] (φ : CNF V) : + List (ClauseSet V) := + countingLeaves (fun j => (CNF.prop64ThresholdBase k (Fintype.card V)) ^ j) + (reduce (nontautological φ.toClauseSet)) + +/-- The Lemma 6.2 / Section 6.3 eq. `(6.4)` candidate-query upper bound +`3 * Fintype.card V * (2 * ψ.length + 2) ^ (CNF.greedyRowListLength B ψ.length) + 1` +bounding the number of candidate parity-row systems evaluated across the `3 * n` greedy rounds on a +sparse formula `ψ : CNF V` at clause-density bound `B` ([OpenAI2026ETH], §6.3, p. 43). -/ +@[expose] def CNF.leafCandidateQueryBound [Fintype V] (B : ℕ) (ψ : CNF V) : ℕ := + 3 * Fintype.card V * (2 * ψ.length + 2) ^ (CNF.greedyRowListLength B ψ.length) + 1 + +/-- Index type of all parity-row systems evaluated during the Section 6.3 Lemma 6.2 greedy +procedure on a leaf formula `ψ : CNF V` at clause-density bound `B` +([OpenAI2026ETH], §6.3, eq. `(6.4)`, p. 43): +- `Sum.inl (i, γ')` indexes the candidate system `A i.1 ++ [testRow γ']` at greedy round + `i : Fin (3 * Fintype.card V)` and ordered candidate list + `γ' : Fin (CNF.greedyRowListLength B ψ.length) → Fin ψ.length × Bool` (including discarded + candidates, counted with list multiplicity), and +- `Sum.inr ()` indexes the final system `A (3 * Fintype.card V)`. -/ +abbrev CNF.LeafCandidateQueryIndex (V : Type*) [Fintype V] (B : ℕ) (ψ : CNF V) : Type _ := + (Fin (3 * Fintype.card V) × + (Fin (CNF.greedyRowListLength B ψ.length) → Fin ψ.length × Bool)) ⊕ Unit + +/-- The parity-row list evaluated at query `q : CNF.LeafCandidateQueryIndex V B ψ` along a +trajectory `A : ℕ → List (Fin ψ.length → Bool)` ([OpenAI2026ETH], §6.3, p. 43): +- at `Sum.inl (i, γ')`, the candidate row list `A i.1 ++ [testRow γ']` at round + `i < 3 * Fintype.card V` and ordered candidate list `γ'`, and +- at `Sum.inr ()`, the final row list `A (3 * Fintype.card V)`. -/ +@[expose] def CNF.candidateQueryRows [Fintype V] {B : ℕ} {ψ : CNF V} + (A : ℕ → List (Fin ψ.length → Bool)) : + CNF.LeafCandidateQueryIndex V B ψ → List (Fin ψ.length → Bool) + | Sum.inl (i, γ') => A i.1 ++ [testRow γ'] + | Sum.inr () => A (3 * Fintype.card V) + +/-- Single-leaf `interpolationScale` exponent multiplier +`CNF.prop64BranchExamScaleCoeff k + 33` combining heavy-variable branching (`+ 32`) with the +Lemma 6.2 candidate-query overhead (`+ 1`) of Section 6.3 eq. `(6.4)`. -/ +@[expose] def CNF.prop64LeafQueryExamScaleCoeff (k : ℕ) : ℕ := + CNF.prop64BranchExamScaleCoeff k + 33 + +/-- Tree-summed `interpolationScale` exponent multiplier +`CNF.prop64BranchExamScaleCoeff k + 49` combining per-leaf branch-summed examination (`+ 32`) with +the Proposition 6.4 sparsification tree leaf-count exponent (`+ 17`). -/ +@[expose] def CNF.prop64TreeExamScaleCoeff (k : ℕ) : ℕ := + CNF.prop64BranchExamScaleCoeff k + 49 + +/-- Total Proposition 6.4 `interpolationScale` exponent multiplier +`CNF.prop64BranchExamScaleCoeff k + 50` combining per-leaf branch-summed examination (`+ 32`), +Lemma 6.2 candidate-query overhead (`+ 1`), and the Proposition 6.4 sparsification tree leaf-count +exponent (`+ 17`). -/ +@[expose] def CNF.prop64TotalExamScaleCoeff (k : ℕ) : ℕ := + CNF.prop64BranchExamScaleCoeff k + 50 + +/-- `CNF.leafCandidateQueryBound B ψ` is at least `1`. -/ +theorem CNF.one_le_leafCandidateQueryBound [Fintype V] (B : ℕ) (ψ : CNF V) : + 1 ≤ CNF.leafCandidateQueryBound B ψ := + Nat.succ_pos _ + +/-- The exact number of candidate and final parity-row queries indexed by +`CNF.LeafCandidateQueryIndex V B ψ` is +`3 * Fintype.card V * (2 * ψ.length) ^ (CNF.greedyRowListLength B ψ.length) + 1`. -/ +theorem CNF.card_leafCandidateQueryIndex_eq [Fintype V] (B : ℕ) (ψ : CNF V) : + Fintype.card (CNF.LeafCandidateQueryIndex V B ψ) = + 3 * Fintype.card V * (2 * ψ.length) ^ (CNF.greedyRowListLength B ψ.length) + 1 := by + simp only [CNF.LeafCandidateQueryIndex, Fintype.card_sum, Fintype.card_prod, + Fintype.card_pi, Fintype.card_fin, Fintype.card_bool, Fintype.card_unit, + Finset.prod_const, Finset.card_univ] + ring + +/-- `Fintype.card (CNF.LeafCandidateQueryIndex V B ψ)` is at most +`CNF.leafCandidateQueryBound B ψ`. -/ +theorem CNF.card_leafCandidateQueryIndex_le [Fintype V] (B : ℕ) (ψ : CNF V) : + Fintype.card (CNF.LeafCandidateQueryIndex V B ψ) ≤ CNF.leafCandidateQueryBound B ψ := by + rw [CNF.card_leafCandidateQueryIndex_eq] + unfold CNF.leafCandidateQueryBound + exact Nat.add_le_add_right + (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (Nat.le_add_right _ 2) _)) 1 + +/-- **Proposition 6.4 normalized additive model-count conservation:** +Summing `L.toCNF.modelCountOn declared` across all leaves `L ∈ φ.prop64NormalizedLeaves k` +recovers `φ.modelCountOn declared` without any nontautology precondition on `φ`. -/ +theorem CNF.sum_modelCountOn_prop64NormalizedLeaves [Fintype V] [DecidableEq V] + (k : ℕ) (φ : CNF V) (declared : Finset V) : + ((φ.prop64NormalizedLeaves k).map fun L => L.toCNF.modelCountOn declared).sum = + φ.modelCountOn declared := + sum_modelCountOn_countingLeaves_nontautological + (fun j => (CNF.prop64ThresholdBase k (Fintype.card V)) ^ j) φ declared + +/-- **Proposition 6.4 normalized exact assignment partition:** +For every assignment `x : V → Bool`, the number of leaf formulas `L.toCNF` +(`L ∈ φ.prop64NormalizedLeaves k`) satisfied by `x` is `1` if `φ.eval x = true` and `0` otherwise. +-/ +theorem CNF.countP_eval_toCNF_prop64NormalizedLeaves [Fintype V] [DecidableEq V] + (k : ℕ) (φ : CNF V) (x : V → Bool) : + ((φ.prop64NormalizedLeaves k).map ClauseSet.toCNF).countP (fun F => F.eval x) = + if φ.eval x then 1 else 0 := + countP_eval_toCNF_countingLeaves_nontautological + (fun j => (CNF.prop64ThresholdBase k (Fintype.card V)) ^ j) φ x + +/-- **Proposition 6.4 normalized leaf structural and clause-density bounds:** +If `∀ c ∈ φ, c.length ≤ k`, then for every leaf `L ∈ φ.prop64NormalizedLeaves k`: +1. `L` is `Sparse` at `θ j = (CNF.prop64ThresholdBase k (Fintype.card V)) ^ j`, `Reduced`, and + nontautological. +2. Every clause `c ∈ L.toCNF` has width `c.length ≤ k`. +3. Every variable `v : V` occurs in at most + `2 * ∑ c ∈ range k, (CNF.prop64ThresholdBase k (Fintype.card V)) ^ c` clauses of `L.toCNF`. +4. Whenever `1 ≤ Fintype.card V`, + `L.toCNF.length ≤ CNF.prop64LeafClauseRatio k (Fintype.card V) * Fintype.card V`. -/ +theorem CNF.length_le_of_mem_prop64NormalizedLeaves [Fintype V] [DecidableEq V] + {φ : CNF V} {k : ℕ} (hk : ∀ c ∈ φ, c.length ≤ k) + {L : ClauseSet V} (hL : L ∈ φ.prop64NormalizedLeaves k) : + Sparse (fun j => (CNF.prop64ThresholdBase k (Fintype.card V)) ^ j) L ∧ + Reduced L ∧ + (∀ C ∈ L, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) ∧ + (∀ c ∈ L.toCNF, c.length ≤ k) ∧ + (∀ v : V, L.toCNF.occurrences v ≤ + 2 * ∑ c ∈ range k, (CNF.prop64ThresholdBase k (Fintype.card V)) ^ c) ∧ + (1 ≤ Fintype.card V → + L.toCNF.length ≤ CNF.prop64LeafClauseRatio k (Fintype.card V) * Fintype.card V) := by + set M := CNF.prop64ThresholdBase k (Fintype.card V) + have hM2 : 2 ≤ M := CNF.two_le_prop64ThresholdBase k (Fintype.card V) + have hθ1 : ∀ j, 1 ≤ M ^ j := fun j => Nat.one_le_pow j M (by omega) + have hsparse : Sparse (M ^ ·) L := sparse_of_mem_countingLeaves_pow hM2 hL + have hred : Reduced L := reduced_of_mem_countingLeaves (reduced_reduce _) hL + have hnt : ∀ C ∈ L, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := + nontautological_of_mem_countingLeaves hθ1 + (fun _ hC => nontautological_of_mem_reduce_nontautological hC) hL + have hroot_k : ∀ C ∈ reduce (nontautological φ.toClauseSet), C.card ≤ k := by + intro C hC + obtain ⟨c, hc, hcard⟩ := + CNF.exists_card_le_of_mem_toClauseSet (nontautological_subset _ (reduce_subset _ hC)) + exact hcard.trans (hk c hc) + have hL_k : ∀ C ∈ L, C.card ≤ k := card_le_of_mem_countingLeaves hroot_k hL + refine ⟨hsparse, hred, hnt, fun c hc => ClauseSet.length_le_of_mem_toCNF hL_k hc, + fun v => ?_, fun hn1 => ?_⟩ + · rw [ClauseSet.occurrences_toCNF] + exact occurrences_le_of_sparse hθ1 hsparse hL_k v + · have hlen_eq : L.toCNF.length = L.card := by + simp only [ClauseSet.toCNF, List.length_map, Finset.length_toList] + have hcard_le : L.card ≤ 2 * (∑ c ∈ range k, M ^ c) * (univ : Finset V).card + 1 := + card_le_of_sparse hθ1 hsparse hL_k univ (fun _ _ _ _ => mem_univ _) + rw [hlen_eq] + rw [card_univ] at hcard_le + unfold CNF.prop64LeafClauseRatio + calc L.card + ≤ 2 * (∑ c ∈ range k, M ^ c) * Fintype.card V + 1 := hcard_le + _ ≤ 2 * (∑ c ∈ range k, M ^ c) * Fintype.card V + Fintype.card V := + Nat.add_le_add_left hn1 _ + _ = (2 * (∑ c ∈ range k, M ^ c) + 1) * Fintype.card V := by ring + +/-! ### 2. Proposition 6.4 tree leaf-count bounds against `numGroups` and `interpolationScale` -/ + +/-- **Proposition 6.4 `2 ^ (n / numGroups n + 1)` leaf-count bound:** +Whenever `1 ≤ numGroups (Fintype.card V)` and `∀ c ∈ φ, c.length ≤ k`, the normalized +counting-sparsification leaf list `φ.prop64NormalizedLeaves k` has length at most +`2 ^ (Fintype.card V / numGroups (Fintype.card V) + 1)`. -/ +theorem CNF.length_prop64NormalizedLeaves_le_two_pow [Fintype V] [DecidableEq V] + {φ : CNF V} {k : ℕ} (hk : ∀ c ∈ φ, c.length ≤ k) + (hs : 1 ≤ numGroups (Fintype.card V)) : + (φ.prop64NormalizedLeaves k).length ≤ + 2 ^ (Fintype.card V / numGroups (Fintype.card V) + 1) := + length_countingLeaves_nontautological_thresholdBase_le hs φ hk Finset.univ + (fun _ _ => mem_univ _) (by rw [card_univ]) + +/-- When `640000 ≤ Nat.clog 2 n`, `1 ≤ interpolationScale n`. -/ +theorem one_le_interpolationScale_of_clog_ge {n : ℕ} (h : 640000 ≤ Nat.clog 2 n) : + 1 ≤ interpolationScale n := by + have hs2 : 2 ≤ numGroups n := two_le_numGroups_of_clog_ge h + have h2pow19 : 2 ^ 19 < Nat.clog 2 n := + lt_of_lt_of_le (by decide : 2 ^ 19 < 640000) h + have hnu20 : 20 ≤ Nat.clog 2 (Nat.clog 2 n) := + (Nat.lt_clog_iff_pow_lt one_lt_two).mpr h2pow19 + have hsq := sq_mul_pow_four_le_clog n + have hclog_le : Nat.clog 2 n ≤ n := + (Nat.clog_le_iff_le_pow one_lt_two).mpr n.lt_two_pow_self.le + have h16_mul : 16 * numGroups n ≤ n := by + have hnu4 : 16 ≤ numGroups n * Nat.clog 2 (Nat.clog 2 n) ^ 4 := by + have : 16 ≤ 2 * 20 ^ 4 := by decide + exact this.trans (Nat.mul_le_mul hs2 (Nat.pow_le_pow_left hnu20 4)) + calc 16 * numGroups n + ≤ (numGroups n * Nat.clog 2 (Nat.clog 2 n) ^ 4) * numGroups n := + Nat.mul_le_mul_right _ hnu4 + _ = numGroups n ^ 2 * Nat.clog 2 (Nat.clog 2 n) ^ 4 := by ring + _ ≤ Nat.clog 2 n := hsq + _ ≤ n := hclog_le + have hs_pos : (0 : ℝ) < numGroups n := Nat.cast_pos.mpr (by omega) + have h16_div : 16 ≤ (n : ℝ) / (numGroups n : ℝ) := by + rw [le_div_iff₀ hs_pos] + exact_mod_cast h16_mul + have hdiv_le := div_numGroups_le_interpolationScale_of_clog_ge h + linarith + +/-- **Proposition 6.4 `(2 : ℝ) ^ (17 * interpolationScale n)` leaf-count bound under +`640000 ≤ Nat.clog 2 (Fintype.card V)`:** +For any width-`≤ k` CNF `φ : CNF V` with `640000 ≤ Nat.clog 2 (Fintype.card V)`, +`((φ.prop64NormalizedLeaves k).length : ℝ) ≤ (2 : ℝ) ^ (17 * interpolationScale (Fintype.card V))`. +-/ +theorem CNF.length_prop64NormalizedLeaves_le_interpolationScale_of_clog_ge + [Fintype V] [DecidableEq V] {φ : CNF V} {k : ℕ} (hk : ∀ c ∈ φ, c.length ≤ k) + (h : 640000 ≤ Nat.clog 2 (Fintype.card V)) : + ((φ.prop64NormalizedLeaves k).length : ℝ) ≤ + (2 : ℝ) ^ (17 * interpolationScale (Fintype.card V)) := by + set n := Fintype.card V + have hs2 : 2 ≤ numGroups n := two_le_numGroups_of_clog_ge h + have hlen_nat : (φ.prop64NormalizedLeaves k).length ≤ 2 ^ (n / numGroups n + 1) := + CNF.length_prop64NormalizedLeaves_le_two_pow hk (le_trans one_le_two hs2) + have hlen_r : ((φ.prop64NormalizedLeaves k).length : ℝ) ≤ + (2 : ℝ) ^ (1 : ℝ) * (2 : ℝ) ^ ((n : ℝ) / (numGroups n : ℝ)) := by + have hcast : ((φ.prop64NormalizedLeaves k).length : ℝ) ≤ + ((2 ^ (n / numGroups n + 1) : ℕ) : ℝ) := Nat.cast_le.mpr hlen_nat + refine hcast.trans ?_ + rw [Nat.cast_pow, Nat.cast_ofNat, pow_succ', Real.rpow_one, ← Real.rpow_natCast] + exact mul_le_mul_of_nonneg_left + (Real.rpow_le_rpow_of_exponent_le one_le_two Nat.cast_div_le) zero_le_two + have h1_scale : (2 : ℝ) ^ (1 : ℝ) ≤ (2 : ℝ) ^ interpolationScale n := + Real.rpow_le_rpow_of_exponent_le one_le_two (one_le_interpolationScale_of_clog_ge h) + have h16_scale : + (2 : ℝ) ^ ((n : ℝ) / (numGroups n : ℝ)) ≤ (2 : ℝ) ^ (16 * interpolationScale n) := + Real.rpow_le_rpow_of_exponent_le one_le_two + (div_numGroups_le_interpolationScale_of_clog_ge h) + calc ((φ.prop64NormalizedLeaves k).length : ℝ) + ≤ (2 : ℝ) ^ (1 : ℝ) * (2 : ℝ) ^ ((n : ℝ) / (numGroups n : ℝ)) := hlen_r + _ ≤ (2 : ℝ) ^ interpolationScale n * (2 : ℝ) ^ (16 * interpolationScale n) := + mul_le_mul h1_scale h16_scale (by positivity) (by positivity) + _ = (2 : ℝ) ^ (17 * interpolationScale n) := by rw [← Real.rpow_add two_pos]; ring_nf + +private theorem le_clog_of_two_pow_le {m n : ℕ} (hn : 2 ^ m ≤ n) : m ≤ Nat.clog 2 n := + (Nat.clog_pow 2 m one_lt_two).symm.le.trans (Nat.clog_mono_right 2 hn) + +/-- **Proposition 6.4 `(2 : ℝ) ^ (17 * interpolationScale n)` leaf-count bound for +`2 ^ 640000 ≤ Fintype.card V`:** +For any width-`≤ k` CNF `φ : CNF V` with `2 ^ 640000 ≤ Fintype.card V`, +`((φ.prop64NormalizedLeaves k).length : ℝ) ≤ (2 : ℝ) ^ (17 * interpolationScale (Fintype.card V))`. +-/ +theorem CNF.length_prop64NormalizedLeaves_le_interpolationScale + [Fintype V] [DecidableEq V] {φ : CNF V} {k : ℕ} (hk : ∀ c ∈ φ, c.length ≤ k) + (hn : 2 ^ 640000 ≤ Fintype.card V) : + ((φ.prop64NormalizedLeaves k).length : ℝ) ≤ + (2 : ℝ) ^ (17 * interpolationScale (Fintype.card V)) := + CNF.length_prop64NormalizedLeaves_le_interpolationScale_of_clog_ge hk (le_clog_of_two_pow_le hn) + +/-! ### 3. Lemma 6.2 candidate-query overhead and Proposition 6.4 tree-wide examination bounds -/ + +/-- For every `B, m : ℕ`, the Lemma 6.1–6.2 greedy candidate list length +`CNF.greedyRowListLength B m = 20000 * B ^ 2 * (Nat.log 2 m + 1) ^ 2` satisfies +`CNF.greedyRowListLength B m ≤ 20000 * B ^ 2 * (Nat.clog 2 (2 * m + 4)) ^ 2`. -/ +theorem CNF.greedyRowListLength_le_mul_pow_clog (B m : ℕ) : + CNF.greedyRowListLength B m ≤ 20000 * B ^ 2 * (Nat.clog 2 (2 * m + 4)) ^ 2 := by + have hlog_lt : Nat.log 2 m < Nat.clog 2 (2 * m + 4) := by + rw [Nat.lt_clog_iff_pow_lt one_lt_two] + rcases Nat.eq_zero_or_pos m with rfl | hm_pos + · decide + · have hpow : 2 ^ Nat.log 2 m ≤ m := Nat.pow_log_le_self 2 (by omega) + omega + unfold CNF.greedyRowListLength + exact Nat.mul_le_mul_left (20000 * B ^ 2) (Nat.pow_le_pow_left hlog_lt 2) + +private theorem greedyRowListLength_le_initialRowWeightBound (B m : ℕ) : + CNF.greedyRowListLength B m ≤ CNF.initialRowWeightBound B m := by + unfold CNF.greedyRowListLength CNF.initialRowWeightBound + exact Nat.mul_le_mul (Nat.mul_le_mul_right _ (by decide)) + (Nat.pow_le_pow_right (Nat.succ_pos _) (by decide)) + +/-- If a trajectory `A : ℕ → List (Fin ψ.length → Bool)` satisfies +`(A i).length ≤ 3 * Fintype.card V + i` for all `i ≤ 3 * Fintype.card V`, then every query +`q : CNF.LeafCandidateQueryIndex V B ψ` (including every discarded candidate +`A i.1 ++ [testRow γ']` for `i < 3 * Fintype.card V` and the final system +`A (3 * Fintype.card V)`) has at most `6 * Fintype.card V` parity rows. -/ +theorem CNF.length_candidateQueryRows_le_of_step [Fintype V] {B : ℕ} {ψ : CNF V} + {A : ℕ → List (Fin ψ.length → Bool)} + (hlen : ∀ i ≤ 3 * Fintype.card V, (A i).length ≤ 3 * Fintype.card V + i) + (q : CNF.LeafCandidateQueryIndex V B ψ) : + (CNF.candidateQueryRows A q).length ≤ 6 * Fintype.card V := by + rcases q with ⟨i, γ'⟩ | ⟨⟩ + · simp only [CNF.candidateQueryRows, List.length_append, List.length_singleton] + have hi : (A i.1).length ≤ 3 * Fintype.card V + i.1 := hlen i.1 i.2.le + omega + · simp only [CNF.candidateQueryRows] + have h3n := hlen (3 * Fintype.card V) le_rfl + omega + +/-- If every row in `A i` (`i ≤ 3 * Fintype.card V`) has Hamming weight at most +`CNF.initialRowWeightBound B ψ.length`, then every row in `CNF.candidateQueryRows A q` +(including every candidate `testRow γ'`) has Hamming weight at most +`CNF.initialRowWeightBound B ψ.length`. -/ +theorem CNF.weight_mem_candidateQueryRows_le_of_step [Fintype V] {B : ℕ} {ψ : CNF V} + {A : ℕ → List (Fin ψ.length → Bool)} + (hw : ∀ i ≤ 3 * Fintype.card V, ∀ r ∈ A i, + weight r ≤ CNF.initialRowWeightBound B ψ.length) + (q : CNF.LeafCandidateQueryIndex V B ψ) : + ∀ r ∈ CNF.candidateQueryRows A q, weight r ≤ CNF.initialRowWeightBound B ψ.length := by + rcases q with ⟨i, γ'⟩ | ⟨⟩ + · intro r hr + simp only [CNF.candidateQueryRows, List.mem_append, List.mem_singleton] at hr + rcases hr with hr | rfl + · exact hw i.1 i.2.le r hr + · exact (weight_testRow_le γ').trans + (greedyRowListLength_le_initialRowWeightBound B ψ.length) + · exact hw (3 * Fintype.card V) le_rfl + +/-- Along any trajectory `A` starting from `A 0 = A₀` with `A₀.length ≤ 3 * Fintype.card V` +and `∀ r ∈ A₀, weight r ≤ CNF.initialRowWeightBound B ψ.length` and appending one +`testRow (γ i)` per step, every query `q : CNF.LeafCandidateQueryIndex V B ψ` has at most +`6 * Fintype.card V` parity rows, each of Hamming weight at most +`CNF.initialRowWeightBound B ψ.length`. -/ +theorem CNF.candidateQueryRows_length_and_weight_le [Fintype V] {B : ℕ} {ψ : CNF V} + {A₀ : List (Fin ψ.length → Bool)} (hlen0 : A₀.length ≤ 3 * Fintype.card V) + (hw0 : ∀ r ∈ A₀, weight r ≤ CNF.initialRowWeightBound B ψ.length) + {A : ℕ → List (Fin ψ.length → Bool)} + {γ : ℕ → Fin (CNF.greedyRowListLength B ψ.length) → Fin ψ.length × Bool} + (h0 : A 0 = A₀) (hA : ∀ i, A (i + 1) = A i ++ [testRow (γ i)]) + (q : CNF.LeafCandidateQueryIndex V B ψ) : + (CNF.candidateQueryRows A q).length ≤ 6 * Fintype.card V ∧ + ∀ r ∈ CNF.candidateQueryRows A q, weight r ≤ CNF.initialRowWeightBound B ψ.length := by + have hstep : ∀ i, (A i).length ≤ 3 * Fintype.card V + i ∧ + ∀ r ∈ A i, weight r ≤ CNF.initialRowWeightBound B ψ.length := by + intro i + induction i with + | zero => + exact ⟨by simpa [h0] using hlen0, fun r hr => hw0 r (h0 ▸ hr)⟩ + | succ i ih => + rw [hA i, List.length_append, List.length_singleton] + refine ⟨by omega, fun r hr => ?_⟩ + rcases List.mem_append.mp hr with hr | hr + · exact ih.2 r hr + · rw [List.mem_singleton.mp hr] + exact (weight_testRow_le (γ i)).trans + (greedyRowListLength_le_initialRowWeightBound B ψ.length) + exact ⟨CNF.length_candidateQueryRows_le_of_step (fun i _ => (hstep i).1) q, + CNF.weight_mem_candidateQueryRows_le_of_step (fun i _ => (hstep i).2) q⟩ + +/-- If `queryExam q ≤ M` (`0 ≤ M`) for every candidate and final query +`q : CNF.LeafCandidateQueryIndex V B ψ`, then the sum of `queryExam q` across all +`q : CNF.LeafCandidateQueryIndex V B ψ` (counting all `3 * Fintype.card V` rounds and all +ordered candidate lists `γ'` with multiplicity plus the final query) is at most +`(CNF.leafCandidateQueryBound B ψ : ℝ) * M`. -/ +theorem CNF.sum_leafCandidateQueryIndex_le [Fintype V] (B : ℕ) (ψ : CNF V) + (queryExam : CNF.LeafCandidateQueryIndex V B ψ → ℝ) {M : ℝ} (hM : 0 ≤ M) + (hq : ∀ q : CNF.LeafCandidateQueryIndex V B ψ, queryExam q ≤ M) : + (∑ q : CNF.LeafCandidateQueryIndex V B ψ, queryExam q) ≤ + (CNF.leafCandidateQueryBound B ψ : ℝ) * M := by + calc (∑ q : CNF.LeafCandidateQueryIndex V B ψ, queryExam q) + ≤ ∑ _q : CNF.LeafCandidateQueryIndex V B ψ, M := + Finset.sum_le_sum fun q _ => hq q + _ = (Fintype.card (CNF.LeafCandidateQueryIndex V B ψ) : ℝ) * M := by + rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] + _ ≤ (CNF.leafCandidateQueryBound B ψ : ℝ) * M := + mul_le_mul_of_nonneg_right + (Nat.cast_le.mpr (CNF.card_leafCandidateQueryIndex_le B ψ)) hM + +/-- **Section 6.3 eq. `(6.4)` candidate-query overhead absorption:** +For any `C_B β_B : ℕ` and any `ε > 0`, there exists `N_q : ℕ` such that for any finite variable +type `V` with `N_q ≤ Fintype.card V`, any CNF `ψ : CNF V`, and any `B : ℕ` satisfying +`ψ.length ≤ B * Fintype.card V` and `B ≤ C_B * (Nat.clog 2 (Fintype.card V)) ^ β_B`, +`(CNF.leafCandidateQueryBound B ψ : ℝ) ≤ (2 : ℝ) ^ (ε * interpolationScale (Fintype.card V))`. -/ +theorem CNF.exists_leafCandidateQueryBound_le_interpolationScale + (C_B β_B : ℕ) {ε : ℝ} (hε : 0 < ε) : + ∃ N_q : ℕ, ∀ {V : Type*} [Fintype V] (ψ : CNF V) {B : ℕ}, + N_q ≤ Fintype.card V → + ψ.length ≤ B * Fintype.card V → + B ≤ C_B * Nat.clog 2 (Fintype.card V) ^ β_B → + (CNF.leafCandidateQueryBound B ψ : ℝ) ≤ + (2 : ℝ) ^ (ε * interpolationScale (Fintype.card V)) := by + obtain ⟨N_q, hN_q⟩ := eventually_atTop.mp + (eventually_query_overhead_poly_le C_B β_B 20000 2 2 hε) + refine ⟨N_q, fun {V _} ψ {B} hcard hm hB => ?_⟩ + have hP := CNF.greedyRowListLength_le_mul_pow_clog B ψ.length + have hbound := hN_q (Fintype.card V) hcard ψ.length B + (CNF.greedyRowListLength B ψ.length) hm hB hP + unfold CNF.leafCandidateQueryBound + exact_mod_cast hbound + +/-- **Proposition 6.4 leaf candidate-query overhead bound (`ε = 1`):** +For any `k ≥ 2`, there exists `N_q ≥ 2` such that for any finite variable type `V` with +`N_q ≤ Fintype.card V` and any `ψ : CNF V` satisfying +`ψ.length ≤ CNF.prop64LeafClauseRatio k (Fintype.card V) * Fintype.card V`, +`(CNF.leafCandidateQueryBound (CNF.prop64LeafClauseRatio k (Fintype.card V)) ψ : ℝ) ≤` +`(2 : ℝ) ^ interpolationScale (Fintype.card V)`. -/ +theorem CNF.exists_prop64_leafCandidateQueryBound_le_interpolationScale {k : ℕ} (hk : 2 ≤ k) : + ∃ N_q : ℕ, 2 ≤ N_q ∧ + ∀ {V : Type*} [Fintype V] (ψ : CNF V), + N_q ≤ Fintype.card V → + ψ.length ≤ CNF.prop64LeafClauseRatio k (Fintype.card V) * Fintype.card V → + (CNF.leafCandidateQueryBound (CNF.prop64LeafClauseRatio k (Fintype.card V)) ψ : ℝ) ≤ + (2 : ℝ) ^ interpolationScale (Fintype.card V) := by + obtain ⟨C_B, _, hCB⟩ := CNF.exists_prop64LeafClauseRatio_le_mul_clog_pow hk + obtain ⟨N_q, hN_q⟩ := + CNF.exists_leafCandidateQueryBound_le_interpolationScale C_B (2 * (k - 1)) one_pos + refine ⟨max N_q 2, le_max_right _ _, fun {V _} ψ hcard hm => ?_⟩ + have hcard_q : N_q ≤ Fintype.card V := (le_max_left _ _).trans hcard + have hn2 : 2 ≤ Fintype.card V := (le_max_right _ _).trans hcard + have hB_le : + CNF.prop64LeafClauseRatio k (Fintype.card V) ≤ + C_B * Nat.clog 2 (Fintype.card V) ^ (2 * (k - 1)) := + hCB (Fintype.card V) hn2 + simpa only [one_mul] using hN_q ψ hcard_q hm hB_le + +private theorem list_sum_map_le_length_mul {α : Type*} (xs : List α) (f : α → ℝ) {M : ℝ} + (hf : ∀ x ∈ xs, f x ≤ M) : + (xs.map f).sum ≤ (xs.length : ℝ) * M := by + simpa only [List.length_map, nsmul_eq_mul] using + List.sum_le_length_nsmul (xs.map f) M (by simpa only [List.forall_mem_map] using hf) + +/-- **Proposition 6.4 end-to-end normalized leaf-to-root greedy recovery, +leaf-count bound, and total candidate-indexed `interpolationScale` examination bounds +([OpenAI2026ETH], §6.4, pp. 43–44 & Appendix A, pp. 44–47):** +For any `k ≥ 2`, there exists `N₃ ≥ 2 ^ 640000` such that for any finite variable type `V` with +`N₃ ≤ Fintype.card V` and any width-`≤ k` CNF `φ : CNF V` (with no clause-count, occurrence, or +nontautology restriction on `φ`): +1. **Exact leaf-summed model-count conservation:** + `((φ.prop64NormalizedLeaves k).map fun L => L.toCNF.modelCountOn Finset.univ).sum =` + `φ.modelCountOn Finset.univ`. +2. **Sparsification tree leaf-count bounds:** + `2 ≤ numGroups (Fintype.card V)`, + `(φ.prop64NormalizedLeaves k).length ≤ 2 ^ (Fintype.card V / numGroups (Fintype.card V) + 1)`, + and `((φ.prop64NormalizedLeaves k).length : ℝ) ≤` + `(2 : ℝ) ^ (17 * interpolationScale (Fintype.card V))`. +3. **Per-leaf greedy parity-design recovery, degree, and candidate-indexed examination bounds:** + For every leaf `L ∈ φ.prop64NormalizedLeaves k` (`ψ := L.toCNF`, + `B := CNF.prop64LeafClauseRatio k (Fintype.card V)`): + - `(CNF.leafCandidateQueryBound B ψ : ℝ) ≤ (2 : ℝ) ^ interpolationScale (Fintype.card V)`, + - `ψ` admits Lemma 6.1 initial parity rows `A₀` such that for any `3 * n`-step greedy trajectory + `(A, γ)`, `CNF.candidateQueryRows A (Sum.inr ()) = A (3 * Fintype.card V)` recovers + `ψ.modelCountOn Finset.univ`, **every** evaluated query `q : CNF.LeafCandidateQueryIndex V B ψ` + (including every discarded candidate `A i.1 ++ [testRow γ']` for `i < 3 * Fintype.card V` and + `γ'` as well as the final query `Sum.inr ()`) has at most `6 * Fintype.card V` rows of weight + `≤ D₀` and admits concrete per-branch `ReplacementDesign`s `D b` recovering + `commonZeroCount univ (ψ.parityRowSystem (CNF.candidateQueryRows A q))` with branch-summed + examination count at most + `(2 : ℝ) ^ ((CNF.prop64BranchExamScaleCoeff k + 32) * interpolationScale (Fintype.card V))`, + and any per-query examination family `queryExam : CNF.LeafCandidateQueryIndex V B ψ → ℝ` + bounded by that single-query bound sums across all `q : CNF.LeafCandidateQueryIndex V B ψ` to + at most + `(2 : ℝ) ^ (CNF.prop64LeafQueryExamScaleCoeff k * interpolationScale (Fintype.card V))`. +4. **Tree-wide and total candidate-indexed examination bounds across `φ.prop64NormalizedLeaves k`:** + - Any per-leaf examination family `leafExam : ClauseSet V → ℝ` bounded on every + `L ∈ φ.prop64NormalizedLeaves k` by + `(2 : ℝ) ^ ((CNF.prop64BranchExamScaleCoeff k + 32) * interpolationScale (Fintype.card V))` + sums across `φ.prop64NormalizedLeaves k` to at most + `(2 : ℝ) ^ (CNF.prop64TreeExamScaleCoeff k * interpolationScale (Fintype.card V))`. + - Any candidate-indexed examination family + `treeQueryExam : (L : ClauseSet V) → CNF.LeafCandidateQueryIndex V B L.toCNF → ℝ` bounded on + every `L ∈ φ.prop64NormalizedLeaves k` and `q : CNF.LeafCandidateQueryIndex V B L.toCNF` by + `(2 : ℝ) ^ ((CNF.prop64BranchExamScaleCoeff k + 32) * interpolationScale (Fintype.card V))` + has total sum + `((φ.prop64NormalizedLeaves k).map fun L =>` + `∑ q : CNF.LeafCandidateQueryIndex V B L.toCNF, treeQueryExam L q).sum` + at most `(2 : ℝ) ^ (CNF.prop64TotalExamScaleCoeff k * interpolationScale (Fintype.card V))`. -/ +theorem CNF.exists_prop64NormalizedLeaves_greedy_total_recovery_and_examBound + {k : ℕ} (hk : 2 ≤ k) : + ∃ N₃ : ℕ, 2 ^ 640000 ≤ N₃ ∧ + ∀ {V : Type*} [Fintype V] [DecidableEq V] + (φ : CNF V), + (∀ c ∈ φ, c.length ≤ k) → + N₃ ≤ Fintype.card V → + let B := CNF.prop64LeafClauseRatio k (Fintype.card V) + ((φ.prop64NormalizedLeaves k).map fun L => L.toCNF.modelCountOn Finset.univ).sum = + φ.modelCountOn Finset.univ ∧ + 2 ≤ numGroups (Fintype.card V) ∧ + (φ.prop64NormalizedLeaves k).length ≤ + 2 ^ (Fintype.card V / numGroups (Fintype.card V) + 1) ∧ + ((φ.prop64NormalizedLeaves k).length : ℝ) ≤ + (2 : ℝ) ^ (17 * interpolationScale (Fintype.card V)) ∧ + (∀ L ∈ φ.prop64NormalizedLeaves k, + let ψ := L.toCNF + let D₀ := CNF.initialRowWeightBound B ψ.length + let P := CNF.greedyRowListLength B ψ.length + let b₀ := CNF.parityBranchThreshold k D₀ (Fintype.card V) + (∀ c ∈ ψ, c.length ≤ k) ∧ + ψ.length ≤ B * Fintype.card V ∧ + (CNF.leafCandidateQueryBound B ψ : ℝ) ≤ + (2 : ℝ) ^ interpolationScale (Fintype.card V) ∧ + ∃ A₀ : List (Fin ψ.length → Bool), A₀.length ≤ 3 * Fintype.card V ∧ + (∀ r ∈ A₀, weight r ≤ D₀) ∧ + ∀ (A : ℕ → List (Fin ψ.length → Bool)) + (γ : ℕ → Fin P → Fin ψ.length × Bool), + A 0 = A₀ → (∀ i, A (i + 1) = A i ++ [testRow (γ i)]) → + (∀ i (γ' : Fin P → Fin ψ.length × Bool), + commonZeroCount univ (ψ.parityRowSystem (A i ++ [testRow (γ i)])) ≤ + commonZeroCount univ (ψ.parityRowSystem (A i ++ [testRow γ']))) → + commonZeroCount univ + (ψ.parityRowSystem (CNF.candidateQueryRows (B := B) A (Sum.inr ()))) = + ψ.modelCountOn Finset.univ ∧ + (∀ q : CNF.LeafCandidateQueryIndex V B ψ, + let rows := CNF.candidateQueryRows A q + rows.length ≤ 6 * Fintype.card V ∧ + (∀ r ∈ rows, weight r ≤ D₀) ∧ + let S := heavyVars univ (univ : Finset (Fin rows.length)) + (fun j => equationScope (ψ.parityRowSystem rows j)) b₀ + ∀ ⦃n' : ℕ⦄ (e : ↥(univ \ S) ≃ Fin n'), + (Fintype.card V ≤ 2 * n' ∧ n' ≤ Fintype.card V) ∧ + (∃ (hF : ∀ b : V → Bool, + Feasible (CNF.prop64ScheduleExponent k) n' (b₀ + 1) + (max (k * (D₀ * 2 ^ k)) 1) + (∑ f : {j : Fin rows.length // + j ∈ (univ : Finset (Fin rows.length))} ⊕ Fin n', + #(branchAugmentedScope S e univ (ψ.parityRowSystem rows) b f))) + (D : ∀ b : V → Bool, + ReplacementDesign + (branchAugmentedScope S e univ (ψ.parityRowSystem rows) b) + (numNodes n') (numGroups n') + (intervalStart (CNF.prop64ScheduleExponent k) n') + (rowBound (CNF.prop64ScheduleExponent k) n') (tauRat n')), + (commonZeroCount (univ : Finset (Fin rows.length)) + (ψ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + ((univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k + (branchPrecision (Fintype.card V)) + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩))).eval 0 / + clearedProductDenom + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k + (branchPrecision (Fintype.card V)) + #(univ : Finset (Fin rows.length))) % + ((2 : ℤ) ^ branchPrecision (Fintype.card V))) ∧ + (∀ b : V → Bool, + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k + (branchPrecision (Fintype.card V)) + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩))).natDegree ≤ + (k * (rowBound (CNF.prop64ScheduleExponent k) n' - 1)) * + (8 * Fintype.card V)) ∧ + ∀ (b : V → Bool) + (s_active : Finset + ({j : Fin rows.length // + j ∈ (univ : Finset (Fin rows.length))} ⊕ Fin n')), + let d := k * (rows.length + 2 * (branchPrecision (Fintype.card V) - 1)) + let q_ord := (d * rowBound (CNF.prop64ScheduleExponent k) n') / numNodes n' + let C := (hF b).toCountingDesign (D b) s_active + (∑ t : Fin (numNodes n'), + (#{p : Finset (Fin n') × Finset (Fin n') | + #p.1 ≤ q_ord ∧ p.2 ⊆ p.1} : ℝ) * + (2 * (#(C.measurementBox t) : ℝ) * + ∑ g : Fin (numGroups n'), + (Fintype.card (C.LocalCube t g) : ℝ))) ≤ + (2 : ℝ) ^ ((CNF.prop64BranchExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V))) ∧ + ∀ (examSum : (V → Bool) → ℝ), + (∀ b ∈ branchAssignments S, + examSum b ≤ + (2 : ℝ) ^ ((CNF.prop64BranchExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V))) → + (∑ b ∈ branchAssignments S, examSum b) ≤ + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V))) ∧ + ∀ (queryExam : CNF.LeafCandidateQueryIndex V B ψ → ℝ), + (∀ q : CNF.LeafCandidateQueryIndex V B ψ, + queryExam q ≤ + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V))) → + (∑ q : CNF.LeafCandidateQueryIndex V B ψ, queryExam q) ≤ + (2 : ℝ) ^ ((CNF.prop64LeafQueryExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V))) ∧ + (∀ (leafExam : ClauseSet V → ℝ), + (∀ L ∈ φ.prop64NormalizedLeaves k, + leafExam L ≤ + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V))) → + ((φ.prop64NormalizedLeaves k).map leafExam).sum ≤ + (2 : ℝ) ^ ((CNF.prop64TreeExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V))) ∧ + ∀ (treeQueryExam : (L : ClauseSet V) → CNF.LeafCandidateQueryIndex V B L.toCNF → ℝ), + (∀ L ∈ φ.prop64NormalizedLeaves k, ∀ q : CNF.LeafCandidateQueryIndex V B L.toCNF, + treeQueryExam L q ≤ + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V))) → + ((φ.prop64NormalizedLeaves k).map fun (L : ClauseSet V) => + ∑ q : CNF.LeafCandidateQueryIndex V B L.toCNF, treeQueryExam L q).sum ≤ + (2 : ℝ) ^ ((CNF.prop64TotalExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V)) := by + obtain ⟨C_B, _, hCB⟩ := CNF.exists_prop64LeafClauseRatio_le_mul_clog_pow hk + obtain ⟨N_row, hN_row16, hrow_rec⟩ := + CNF.exists_branch_schedule_recovery_and_examBound_parityRowSystem_of_le_clog_pow + k C_B (2 * (k - 1)) + obtain ⟨N_gr, hN_gr16, hgreedy_rec⟩ := + CNF.exists_greedy_parityRowSystem_recovery_and_examBound_of_le_clog_pow k C_B (2 * (k - 1)) + obtain ⟨N_q, _, hquery⟩ := CNF.exists_prop64_leafCandidateQueryBound_le_interpolationScale hk + refine ⟨max (2 ^ 640000) (max (max N_row N_gr) N_q), le_max_left _ _, + fun {V _ _} φ hk_φ hcard => ?_⟩ + intro B + have hpow_le : 2 ^ 640000 ≤ Fintype.card V := (le_max_left _ _).trans hcard + have hN_row_le : N_row ≤ Fintype.card V := + (((le_max_left _ _).trans (le_max_left _ _)).trans (le_max_right _ _)).trans hcard + have hN_gr_le : N_gr ≤ Fintype.card V := + (((le_max_right _ _).trans (le_max_left _ _)).trans (le_max_right _ _)).trans hcard + have hNq_le : N_q ≤ Fintype.card V := + ((le_max_right _ _).trans (le_max_right _ _)).trans hcard + have hs2 : 2 ≤ numGroups (Fintype.card V) := two_le_numGroups_of_pow_le hpow_le + have hn1 : 1 ≤ Fintype.card V := le_trans (by decide : 1 ≤ 16384) (hN_row16.trans hN_row_le) + have hn2 : 2 ≤ Fintype.card V := le_trans (by decide : 2 ≤ 16384) (hN_row16.trans hN_row_le) + have hlen_two_pow : + (φ.prop64NormalizedLeaves k).length ≤ + 2 ^ (Fintype.card V / numGroups (Fintype.card V) + 1) := + CNF.length_prop64NormalizedLeaves_le_two_pow hk_φ (by omega) + have hlen_scale : + ((φ.prop64NormalizedLeaves k).length : ℝ) ≤ + (2 : ℝ) ^ (17 * interpolationScale (Fintype.card V)) := + CNF.length_prop64NormalizedLeaves_le_interpolationScale hk_φ hpow_le + have hsum_leaf_queries : ∀ L ∈ φ.prop64NormalizedLeaves k, + ∀ (queryExam : CNF.LeafCandidateQueryIndex V B L.toCNF → ℝ), + (∀ q : CNF.LeafCandidateQueryIndex V B L.toCNF, + queryExam q ≤ + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V))) → + (∑ q : CNF.LeafCandidateQueryIndex V B L.toCNF, queryExam q) ≤ + (2 : ℝ) ^ ((CNF.prop64LeafQueryExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V)) := by + intro L hL queryExam hq_bound + obtain ⟨_, _, _, _, _, hlen_ψ⟩ := CNF.length_le_of_mem_prop64NormalizedLeaves hk_φ hL + have hq_le := hquery L.toCNF hNq_le (hlen_ψ hn1) + have hsum_q := CNF.sum_leafCandidateQueryIndex_le B L.toCNF queryExam (by positivity) hq_bound + calc (∑ q : CNF.LeafCandidateQueryIndex V B L.toCNF, queryExam q) + ≤ (CNF.leafCandidateQueryBound B L.toCNF : ℝ) * + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V)) := hsum_q + _ ≤ (2 : ℝ) ^ interpolationScale (Fintype.card V) * + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V)) := + mul_le_mul_of_nonneg hq_le le_rfl (Nat.cast_nonneg _) (by positivity) + _ = (2 : ℝ) ^ ((CNF.prop64LeafQueryExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V)) := by + rw [← Real.rpow_add two_pos] + unfold CNF.prop64LeafQueryExamScaleCoeff + push_cast + ring_nf + refine ⟨CNF.sum_modelCountOn_prop64NormalizedLeaves k φ Finset.univ, hs2, + hlen_two_pow, hlen_scale, fun L hL => ?_, fun leafExam hleaf => ?_, + fun treeQueryExam htree => ?_⟩ + · intro ψ D₀ P b₀ + obtain ⟨_, _, _, hk_ψ, _, hlen_ψ⟩ := CNF.length_le_of_mem_prop64NormalizedLeaves hk_φ hL + have hm_ψ : ψ.length ≤ B * Fintype.card V := hlen_ψ hn1 + have hB1 : 1 ≤ B := CNF.one_le_prop64LeafClauseRatio k (Fintype.card V) + have hB_le : B ≤ C_B * Nat.clog 2 (Fintype.card V) ^ (2 * (k - 1)) := + hCB (Fintype.card V) hn2 + have hq_le : + (CNF.leafCandidateQueryBound B ψ : ℝ) ≤ (2 : ℝ) ^ interpolationScale (Fintype.card V) := + hquery ψ hNq_le hm_ψ + obtain ⟨A₀, hlen0, hw0, hgreedy⟩ := hgreedy_rec ψ hk_ψ hN_gr_le hB1 hB_le hm_ψ + refine ⟨hk_ψ, hm_ψ, hq_le, A₀, hlen0, hw0, fun A γ h0 hA hγ => ?_⟩ + obtain ⟨hcount, _⟩ := hgreedy A γ h0 hA hγ + refine ⟨hcount, fun q => ?_, hsum_leaf_queries L hL⟩ + obtain ⟨hlen_q, hw_q⟩ := CNF.candidateQueryRows_length_and_weight_le hlen0 hw0 h0 hA q + refine ⟨hlen_q, hw_q, fun {n'} e => ?_⟩ + exact hrow_rec hk_ψ hN_row_le hm_ψ hB_le le_rfl hw_q hlen_q e + · calc ((φ.prop64NormalizedLeaves k).map leafExam).sum + ≤ ((φ.prop64NormalizedLeaves k).length : ℝ) * + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V)) := + list_sum_map_le_length_mul _ _ hleaf + _ ≤ (2 : ℝ) ^ (17 * interpolationScale (Fintype.card V)) * + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V)) := + mul_le_mul_of_nonneg_right hlen_scale (by positivity) + _ = (2 : ℝ) ^ ((CNF.prop64TreeExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V)) := by + rw [← Real.rpow_add two_pos] + unfold CNF.prop64TreeExamScaleCoeff + push_cast + ring_nf + · calc ((φ.prop64NormalizedLeaves k).map fun (L : ClauseSet V) => + ∑ q : CNF.LeafCandidateQueryIndex V B L.toCNF, treeQueryExam L q).sum + ≤ ((φ.prop64NormalizedLeaves k).length : ℝ) * + (2 : ℝ) ^ ((CNF.prop64LeafQueryExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V)) := + list_sum_map_le_length_mul _ _ fun L hL => + hsum_leaf_queries L hL (treeQueryExam L) (htree L hL) + _ ≤ (2 : ℝ) ^ (17 * interpolationScale (Fintype.card V)) * + (2 : ℝ) ^ ((CNF.prop64LeafQueryExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V)) := + mul_le_mul_of_nonneg_right hlen_scale (by positivity) + _ = (2 : ℝ) ^ ((CNF.prop64TotalExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V)) := by + rw [← Real.rpow_add two_pos] + unfold CNF.prop64TotalExamScaleCoeff CNF.prop64LeafQueryExamScaleCoeff + push_cast + ring_nf + +private noncomputable def nextGreedyStep [Fintype V] [DecidableEq V] + (φ : CNF V) (P : ℕ) [Nonempty (Fin φ.length)] + (L : List (Fin φ.length → Bool)) : Fin P → Fin φ.length × Bool := + (exists_min_image (univ : Finset (Fin P → Fin φ.length × Bool)) + (fun γ' => commonZeroCount univ (φ.parityRowSystem (L ++ [testRow γ']))) + univ_nonempty).choose + +private theorem nextGreedyStep_le [Fintype V] [DecidableEq V] + (φ : CNF V) (P : ℕ) [Nonempty (Fin φ.length)] + (L : List (Fin φ.length → Bool)) (γ' : Fin P → Fin φ.length × Bool) : + commonZeroCount univ (φ.parityRowSystem (L ++ [testRow (nextGreedyStep φ P L)])) ≤ + commonZeroCount univ (φ.parityRowSystem (L ++ [testRow γ'])) := + (exists_min_image (univ : Finset (Fin P → Fin φ.length × Bool)) + (fun δ => commonZeroCount univ (φ.parityRowSystem (L ++ [testRow δ]))) + univ_nonempty).choose_spec.2 γ' (mem_univ γ') + +private noncomputable def greedyTrajectory [Fintype V] [DecidableEq V] + (φ : CNF V) (P : ℕ) [Nonempty (Fin φ.length)] + (A₀ : List (Fin φ.length → Bool)) : ℕ → List (Fin φ.length → Bool) + | 0 => A₀ + | i + 1 => + let L := greedyTrajectory φ P A₀ i + L ++ [testRow (nextGreedyStep φ P L)] + +/-- **Proposition 6.4 unconditional normalized leaf-to-root `modelCountOn` recovery +and total candidate-indexed `interpolationScale` examination bounds ([OpenAI2026ETH], §6.4, +pp. 43–44 & Appendix A, pp. 44–47):** +For any `k ≥ 2`, there exists `N₃ ≥ 2 ^ 640000` such that for any finite variable type `V` with +`N₃ ≤ Fintype.card V` and any width-`≤ k` CNF `φ : CNF V`: +1. `((φ.prop64NormalizedLeaves k).map fun L => L.toCNF.modelCountOn Finset.univ).sum =` + `φ.modelCountOn Finset.univ`. +2. `2 ≤ numGroups (Fintype.card V)`, + `(φ.prop64NormalizedLeaves k).length ≤ 2 ^ (Fintype.card V / numGroups (Fintype.card V) + 1)`, + and `((φ.prop64NormalizedLeaves k).length : ℝ) ≤` + `(2 : ℝ) ^ (17 * interpolationScale (Fintype.card V))`. +3. Every leaf `L ∈ φ.prop64NormalizedLeaves k` (`ψ := L.toCNF`) unconditionally admits a greedy + parity-row trajectory `A : ℕ → List (Fin ψ.length → Bool)` such that: + - at the final query `q = Sum.inr ()`, + `commonZeroCount univ (ψ.parityRowSystem (CNF.candidateQueryRows A (Sum.inr ()))) =` + `ψ.modelCountOn Finset.univ`, + - at every greedy round `i : Fin (3 * Fintype.card V)` and every ordered candidate list + `γ' : Fin P → Fin ψ.length × Bool`, + `commonZeroCount univ (ψ.parityRowSystem (A (i.1 + 1))) ≤` + `commonZeroCount univ (ψ.parityRowSystem (CNF.candidateQueryRows A (Sum.inl (i, γ'))))`, + - for **every** evaluated query `q : CNF.LeafCandidateQueryIndex V B ψ` (including every + discarded candidate `Sum.inl (i, γ')` as well as `Sum.inr ()`), + `rows := CNF.candidateQueryRows A q` satisfies `rows.length ≤ 6 * Fintype.card V` and + `∀ r ∈ rows, weight r ≤ D₀`, and for any free-variable equivalence `e : ↥(univ \ S) ≃ Fin n'`, + there exist per-branch `hF b` and concrete `ReplacementDesign`s `D b` recovering + `(commonZeroCount univ (ψ.parityRowSystem rows) : ℤ)` (and hence + `(ψ.modelCountOn Finset.univ : ℤ)` at `q = Sum.inr ()`) via + `univariateClearedParityTruncatedSum` with numerator degree + `≤ (k * (rowBound (CNF.prop64ScheduleExponent k) n' - 1)) * (8 * Fintype.card V)` and + single-branch / branch-summed `interpolationScale` examination bounds, and + - any per-query examination family `queryExam : CNF.LeafCandidateQueryIndex V B ψ → ℝ` bounded + by `(2 : ℝ) ^ ((CNF.prop64BranchExamScaleCoeff k + 32) * interpolationScale n)` sums across all + `q : CNF.LeafCandidateQueryIndex V B ψ` to at most + `(2 : ℝ) ^ (CNF.prop64LeafQueryExamScaleCoeff k * interpolationScale n)`. +4. Summing across all leaves in `φ.prop64NormalizedLeaves k` bounds the tree-wide examination count + by `(2 : ℝ) ^ (CNF.prop64TreeExamScaleCoeff k * interpolationScale (Fintype.card V))` and the + total candidate-indexed examination count by + `(2 : ℝ) ^ (CNF.prop64TotalExamScaleCoeff k * interpolationScale (Fintype.card V))`. -/ +theorem CNF.exists_prop64NormalizedLeaves_total_recovery_and_examBound + {k : ℕ} (hk : 2 ≤ k) : + ∃ N₃ : ℕ, 2 ^ 640000 ≤ N₃ ∧ + ∀ {V : Type*} [Fintype V] [DecidableEq V] + (φ : CNF V), + (∀ c ∈ φ, c.length ≤ k) → + N₃ ≤ Fintype.card V → + let B := CNF.prop64LeafClauseRatio k (Fintype.card V) + ((φ.prop64NormalizedLeaves k).map fun L => L.toCNF.modelCountOn Finset.univ).sum = + φ.modelCountOn Finset.univ ∧ + 2 ≤ numGroups (Fintype.card V) ∧ + (φ.prop64NormalizedLeaves k).length ≤ + 2 ^ (Fintype.card V / numGroups (Fintype.card V) + 1) ∧ + ((φ.prop64NormalizedLeaves k).length : ℝ) ≤ + (2 : ℝ) ^ (17 * interpolationScale (Fintype.card V)) ∧ + (∀ L ∈ φ.prop64NormalizedLeaves k, + let ψ := L.toCNF + let D₀ := CNF.initialRowWeightBound B ψ.length + let P := CNF.greedyRowListLength B ψ.length + let b₀ := CNF.parityBranchThreshold k D₀ (Fintype.card V) + (∀ c ∈ ψ, c.length ≤ k) ∧ + ψ.length ≤ B * Fintype.card V ∧ + (CNF.leafCandidateQueryBound B ψ : ℝ) ≤ + (2 : ℝ) ^ interpolationScale (Fintype.card V) ∧ + ∃ A : ℕ → List (Fin ψ.length → Bool), + commonZeroCount univ + (ψ.parityRowSystem (CNF.candidateQueryRows (B := B) A (Sum.inr ()))) = + ψ.modelCountOn Finset.univ ∧ + (∀ (i : Fin (3 * Fintype.card V)) (γ' : Fin P → Fin ψ.length × Bool), + commonZeroCount univ (ψ.parityRowSystem (A (i.1 + 1))) ≤ + commonZeroCount univ + (ψ.parityRowSystem (CNF.candidateQueryRows A (Sum.inl (i, γ'))))) ∧ + (∀ q : CNF.LeafCandidateQueryIndex V B ψ, + let rows := CNF.candidateQueryRows A q + rows.length ≤ 6 * Fintype.card V ∧ + (∀ r ∈ rows, weight r ≤ D₀) ∧ + let S := heavyVars univ (univ : Finset (Fin rows.length)) + (fun j => equationScope (ψ.parityRowSystem rows j)) b₀ + ∀ ⦃n' : ℕ⦄ (e : ↥(univ \ S) ≃ Fin n'), + (Fintype.card V ≤ 2 * n' ∧ n' ≤ Fintype.card V) ∧ + (∃ (hF : ∀ b : V → Bool, + Feasible (CNF.prop64ScheduleExponent k) n' (b₀ + 1) + (max (k * (D₀ * 2 ^ k)) 1) + (∑ f : {j : Fin rows.length // + j ∈ (univ : Finset (Fin rows.length))} ⊕ Fin n', + #(branchAugmentedScope S e univ (ψ.parityRowSystem rows) b f))) + (D : ∀ b : V → Bool, + ReplacementDesign + (branchAugmentedScope S e univ (ψ.parityRowSystem rows) b) + (numNodes n') (numGroups n') + (intervalStart (CNF.prop64ScheduleExponent k) n') + (rowBound (CNF.prop64ScheduleExponent k) n') (tauRat n')), + (commonZeroCount (univ : Finset (Fin rows.length)) + (ψ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + ((univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k + (branchPrecision (Fintype.card V)) + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩))).eval 0 / + clearedProductDenom + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k + (branchPrecision (Fintype.card V)) + #(univ : Finset (Fin rows.length))) % + ((2 : ℤ) ^ branchPrecision (Fintype.card V))) ∧ + (∀ b : V → Bool, + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k + (branchPrecision (Fintype.card V)) + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩))).natDegree ≤ + (k * (rowBound (CNF.prop64ScheduleExponent k) n' - 1)) * + (8 * Fintype.card V)) ∧ + ∀ (b : V → Bool) + (s_active : Finset + ({j : Fin rows.length // + j ∈ (univ : Finset (Fin rows.length))} ⊕ Fin n')), + let d := k * (rows.length + 2 * (branchPrecision (Fintype.card V) - 1)) + let q_ord := (d * rowBound (CNF.prop64ScheduleExponent k) n') / numNodes n' + let C := (hF b).toCountingDesign (D b) s_active + (∑ t : Fin (numNodes n'), + (#{p : Finset (Fin n') × Finset (Fin n') | + #p.1 ≤ q_ord ∧ p.2 ⊆ p.1} : ℝ) * + (2 * (#(C.measurementBox t) : ℝ) * + ∑ g : Fin (numGroups n'), + (Fintype.card (C.LocalCube t g) : ℝ))) ≤ + (2 : ℝ) ^ ((CNF.prop64BranchExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V))) ∧ + ∀ (examSum : (V → Bool) → ℝ), + (∀ b ∈ branchAssignments S, + examSum b ≤ + (2 : ℝ) ^ ((CNF.prop64BranchExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V))) → + (∑ b ∈ branchAssignments S, examSum b) ≤ + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V))) ∧ + ∀ (queryExam : CNF.LeafCandidateQueryIndex V B ψ → ℝ), + (∀ q : CNF.LeafCandidateQueryIndex V B ψ, + queryExam q ≤ + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V))) → + (∑ q : CNF.LeafCandidateQueryIndex V B ψ, queryExam q) ≤ + (2 : ℝ) ^ ((CNF.prop64LeafQueryExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V))) ∧ + (∀ (leafExam : ClauseSet V → ℝ), + (∀ L ∈ φ.prop64NormalizedLeaves k, + leafExam L ≤ + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V))) → + ((φ.prop64NormalizedLeaves k).map leafExam).sum ≤ + (2 : ℝ) ^ ((CNF.prop64TreeExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V))) ∧ + ∀ (treeQueryExam : (L : ClauseSet V) → CNF.LeafCandidateQueryIndex V B L.toCNF → ℝ), + (∀ L ∈ φ.prop64NormalizedLeaves k, ∀ q : CNF.LeafCandidateQueryIndex V B L.toCNF, + treeQueryExam L q ≤ + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V))) → + ((φ.prop64NormalizedLeaves k).map fun (L : ClauseSet V) => + ∑ q : CNF.LeafCandidateQueryIndex V B L.toCNF, treeQueryExam L q).sum ≤ + (2 : ℝ) ^ ((CNF.prop64TotalExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V)) := by + obtain ⟨C_B, _, hCB⟩ := CNF.exists_prop64LeafClauseRatio_le_mul_clog_pow hk + obtain ⟨N_row, hN_row16, hrow_rec⟩ := + CNF.exists_branch_schedule_recovery_and_examBound_parityRowSystem_of_le_clog_pow + k C_B (2 * (k - 1)) + obtain ⟨N₃, hN₃, hgreedy_total⟩ := + CNF.exists_prop64NormalizedLeaves_greedy_total_recovery_and_examBound hk + refine ⟨max N₃ N_row, le_trans hN₃ (le_max_left _ _), + fun {V _ _} φ hk_φ hcard => ?_⟩ + intro B + have hN₃_le : N₃ ≤ Fintype.card V := (le_max_left _ _).trans hcard + have hN_row_le : N_row ≤ Fintype.card V := (le_max_right _ _).trans hcard + have hn2 : 2 ≤ Fintype.card V := le_trans (by decide : 2 ≤ 16384) (hN_row16.trans hN_row_le) + obtain ⟨hsum, hs2, hlen_pow, hlen_scale, hleaf, htree, htotal⟩ := hgreedy_total φ hk_φ hN₃_le + refine ⟨hsum, hs2, hlen_pow, hlen_scale, fun L hL => ?_, htree, htotal⟩ + intro ψ D₀ P b₀ + obtain ⟨hk_ψ, hm_ψ, hq_le, A₀, hlen0, hw0, hgreedy⟩ := hleaf L hL + refine ⟨hk_ψ, hm_ψ, hq_le, ?_⟩ + rcases Nat.eq_zero_or_pos ψ.length with hlen_zero | hlen_pos + · have hnil : ψ = [] := List.eq_nil_of_length_eq_zero hlen_zero + let A : ℕ → List (Fin ψ.length → Bool) := fun _ => [] + have hcount_nil : + commonZeroCount univ (ψ.parityRowSystem (CNF.candidateQueryRows (B := B) A (Sum.inr ()))) = + ψ.modelCountOn Finset.univ := by + change commonZeroCount univ (ψ.parityRowSystem []) = ψ.modelCountOn Finset.univ + rw [CNF.commonZeroCount_parityRowSystem_eq_modelCountOn_add] + suffices #{σ : V → Bool | ψ.eval σ = false ∧ PassesTests ψ.violations [] σ} = 0 by omega + rw [card_eq_zero, filter_eq_empty_iff] + intro σ _ ⟨hev, _⟩ + rw [hnil] at hev + exact Bool.noConfusion hev + have hB1 : 1 ≤ B := CNF.one_le_prop64LeafClauseRatio k (Fintype.card V) + have hP_pos : 0 < P := by + change 0 < 20000 * B ^ 2 * (Nat.log 2 ψ.length + 1) ^ 2 + positivity + have hmin_vac : ∀ (i : Fin (3 * Fintype.card V)) (γ' : Fin P → Fin ψ.length × Bool), + commonZeroCount univ (ψ.parityRowSystem (A (i.1 + 1))) ≤ + commonZeroCount univ + (ψ.parityRowSystem (CNF.candidateQueryRows A (Sum.inl (i, γ')))) := by + intro _ γ' + exact Fin.elim0 (hlen_zero ▸ (γ' ⟨0, hP_pos⟩).1) + have hB_le : B ≤ C_B * Nat.clog 2 (Fintype.card V) ^ (2 * (k - 1)) := + hCB (Fintype.card V) hn2 + refine ⟨A, hcount_nil, hmin_vac, fun q => ?_, fun queryExam hq_bound => ?_⟩ + · have hlen_q : (CNF.candidateQueryRows A q).length ≤ 6 * Fintype.card V := + CNF.length_candidateQueryRows_le_of_step (fun _ _ => Nat.zero_le _) q + have hw_q : ∀ r ∈ CNF.candidateQueryRows A q, weight r ≤ D₀ := + CNF.weight_mem_candidateQueryRows_le_of_step (by intro _ _ _ hr; cases hr) q + exact ⟨hlen_q, hw_q, fun {n'} e => + hrow_rec hk_ψ hN_row_le hm_ψ hB_le le_rfl hw_q hlen_q e⟩ + · have hsum_q := CNF.sum_leafCandidateQueryIndex_le B ψ queryExam (by positivity) hq_bound + calc (∑ q : CNF.LeafCandidateQueryIndex V B ψ, queryExam q) + ≤ (CNF.leafCandidateQueryBound B ψ : ℝ) * + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V)) := hsum_q + _ ≤ (2 : ℝ) ^ interpolationScale (Fintype.card V) * + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V)) := + mul_le_mul_of_nonneg hq_le le_rfl (Nat.cast_nonneg _) (by positivity) + _ = (2 : ℝ) ^ ((CNF.prop64LeafQueryExamScaleCoeff k : ℝ) * + interpolationScale (Fintype.card V)) := by + rw [← Real.rpow_add two_pos] + unfold CNF.prop64LeafQueryExamScaleCoeff + push_cast + ring_nf + · have : Nonempty (Fin ψ.length) := ⟨⟨0, hlen_pos⟩⟩ + let A := greedyTrajectory ψ P A₀ + let γ : ℕ → Fin P → Fin ψ.length × Bool := fun i => nextGreedyStep ψ P (A i) + have hmin : ∀ i (γ' : Fin P → Fin ψ.length × Bool), + commonZeroCount univ (ψ.parityRowSystem (A i ++ [testRow (γ i)])) ≤ + commonZeroCount univ (ψ.parityRowSystem (A i ++ [testRow γ'])) := + fun i γ' => nextGreedyStep_le ψ P (A i) γ' + obtain ⟨hcount, hq_all, hq_sum⟩ := hgreedy A γ rfl (fun _ => rfl) hmin + exact ⟨A, hcount, fun i γ' => hmin i.1 γ', hq_all, hq_sum⟩ + +end Cslib.Logic.PL diff --git a/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean b/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean new file mode 100644 index 000000000..ded9c92dc --- /dev/null +++ b/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean @@ -0,0 +1,327 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Complexity.Init +public import Complexity.Computability.Complexity.FineGrained.GeneralCNFCountingAsymptotics + +/-! +# Tests for `Complexity.Computability.Complexity.FineGrained.GeneralCNFCountingAsymptotics` + +Exercises the normalized Proposition 6.4 leaf decomposition (`CNF.prop64NormalizedLeaves`), +leaf-count bounds against `numGroups` and `interpolationScale`, Lemma 6.2 candidate-query indexing +and bounds (`CNF.LeafCandidateQueryIndex`, `CNF.candidateQueryRows`, +`CNF.card_leafCandidateQueryIndex_eq`, `CNF.card_leafCandidateQueryIndex_le`, +`CNF.candidateQueryRows_length_and_weight_le`, `CNF.greedyRowListLength_le_mul_pow_clog`), and the +end-to-end candidate-indexed and tree-wide `ReplacementDesign` recovery and actual +`toCountingDesign` examination bounds on concrete 3-CNF formulas containing tautological clauses. +-/ + +public noncomputable section + +namespace CslibTests + +open Finset +open Cslib.BitString +open Cslib.LinearAlgebra +open Cslib.Logic.PL +open Cslib.Logic.PL.ClauseSet.Sparsification +open Cslib.Complexity.SubexponentialSAT +open Cslib.Complexity.SubexponentialSAT.ReplacementParams + +/-- Concrete 3-CNF on `Fin 4` containing a width-3 tautological clause +`[(0, true), (0, false), (1, true)]` together with two non-tautological clauses +`(x₀ ∨ ¬x₁ ∨ x₂) ∧ (¬x₁ ∨ ¬x₃)`. -/ +def sampleTaut3CNF : CNF (Fin 4) := + [[(0, true), (0, false), (1, true)], + [(0, true), (1, false), (2, true)], + [(1, false), (3, false)]] + +theorem sampleTaut3CNF_width_le_three : + ∀ c ∈ sampleTaut3CNF, c.length ≤ 3 := by + decide + +theorem sampleTaut3CNF_modelCountOn_eq_eleven : + sampleTaut3CNF.modelCountOn Finset.univ = 11 := by + decide + +/-- Summing `L.toCNF.modelCountOn Finset.univ` across `sampleTaut3CNF.prop64NormalizedLeaves 3` +recovers the exact model count `11` despite the tautological clause in `sampleTaut3CNF`. -/ +theorem sampleTaut3CNF_sum_modelCountOn_prop64NormalizedLeaves : + ((sampleTaut3CNF.prop64NormalizedLeaves 3).map + fun L => L.toCNF.modelCountOn Finset.univ).sum = 11 := by + rw [CNF.sum_modelCountOn_prop64NormalizedLeaves, sampleTaut3CNF_modelCountOn_eq_eleven] + +/-- On the satisfying assignment `fun _ => false`, exactly `1` normalized leaf formula of +`sampleTaut3CNF` evaluates to `true`. -/ +theorem sampleTaut3CNF_countP_eval_prop64NormalizedLeaves_true : + ((sampleTaut3CNF.prop64NormalizedLeaves 3).map ClauseSet.toCNF).countP + (fun F => F.eval (fun _ : Fin 4 => false)) = 1 := by + rw [CNF.countP_eval_toCNF_prop64NormalizedLeaves] + decide + +/-- On the falsifying assignment `fun _ => true`, `0` normalized leaf formulas of +`sampleTaut3CNF` evaluate to `true`. -/ +theorem sampleTaut3CNF_countP_eval_prop64NormalizedLeaves_false : + ((sampleTaut3CNF.prop64NormalizedLeaves 3).map ClauseSet.toCNF).countP + (fun F => F.eval (fun _ : Fin 4 => true)) = 0 := by + rw [CNF.countP_eval_toCNF_prop64NormalizedLeaves] + decide + +/-- Every leaf `L ∈ sampleTaut3CNF.prop64NormalizedLeaves 3` is reduced, free of complementary +literals within each clause (the tautological clause has been filtered out), has clause width at +most `3`, and satisfies `L.toCNF.length ≤ CNF.prop64LeafClauseRatio 3 4 * 4`. -/ +theorem sampleTaut3CNF_leaf_nontautological_and_length_le + {L : ClauseSet (Fin 4)} (hL : L ∈ sampleTaut3CNF.prop64NormalizedLeaves 3) : + Reduced L ∧ + (∀ C ∈ L, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) ∧ + (∀ c ∈ L.toCNF, c.length ≤ 3) ∧ + L.toCNF.length ≤ CNF.prop64LeafClauseRatio 3 4 * 4 := by + obtain ⟨_, hred, hnt, hk_L, _, hlen_L⟩ := + CNF.length_le_of_mem_prop64NormalizedLeaves sampleTaut3CNF_width_le_three hL + exact ⟨hred, hnt, hk_L, hlen_L (by decide : 1 ≤ Fintype.card (Fin 4))⟩ + +/-- Concrete check of `CNF.card_leafCandidateQueryIndex_eq`, `CNF.card_leafCandidateQueryIndex_le`, +`CNF.greedyRowListLength_le_mul_pow_clog`, and `CNF.candidateQueryRows_length_and_weight_le` on +both a round-`0` candidate query `Sum.inl (0, γ₀)` and the final query `Sum.inr ()` for +`sampleTaut3CNF`. -/ +theorem sampleTaut3CNF_candidateQueryIndex_and_rows_bounds : + Fintype.card (CNF.LeafCandidateQueryIndex (Fin 4) 2 sampleTaut3CNF) = + 12 * 6 ^ (CNF.greedyRowListLength 2 3) + 1 ∧ + Fintype.card (CNF.LeafCandidateQueryIndex (Fin 4) 2 sampleTaut3CNF) ≤ + CNF.leafCandidateQueryBound 2 sampleTaut3CNF ∧ + CNF.greedyRowListLength 2 sampleTaut3CNF.length ≤ + 20000 * 2 ^ 2 * (Nat.clog 2 (2 * sampleTaut3CNF.length + 4)) ^ 2 ∧ + let γ₀ : Fin (CNF.greedyRowListLength 2 sampleTaut3CNF.length) → + Fin sampleTaut3CNF.length × Bool := + fun _ => (⟨0, by decide⟩, true) + let A : ℕ → List (Fin sampleTaut3CNF.length → Bool) := + fun i => List.replicate i (testRow γ₀) + let q_cand : CNF.LeafCandidateQueryIndex (Fin 4) 2 sampleTaut3CNF := + Sum.inl (⟨0, by decide⟩, γ₀) + let q_final : CNF.LeafCandidateQueryIndex (Fin 4) 2 sampleTaut3CNF := Sum.inr () + (CNF.candidateQueryRows A q_cand).length ≤ 24 ∧ + (∀ r ∈ CNF.candidateQueryRows A q_cand, + weight r ≤ CNF.initialRowWeightBound 2 sampleTaut3CNF.length) ∧ + (CNF.candidateQueryRows A q_final).length ≤ 24 ∧ + (∀ r ∈ CNF.candidateQueryRows A q_final, + weight r ≤ CNF.initialRowWeightBound 2 sampleTaut3CNF.length) := by + refine ⟨?_, CNF.card_leafCandidateQueryIndex_le 2 sampleTaut3CNF, + CNF.greedyRowListLength_le_mul_pow_clog 2 sampleTaut3CNF.length, ?_⟩ + · rw [CNF.card_leafCandidateQueryIndex_eq, Fintype.card_fin, + show sampleTaut3CNF.length = 3 by rfl, show 3 * 4 = 12 by rfl, show 2 * 3 = 6 by rfl] + · intro γ₀ A q_cand q_final + have hA : ∀ i, A (i + 1) = A i ++ [testRow γ₀] := fun i => List.replicate_succ' + have hcand := CNF.candidateQueryRows_length_and_weight_le (B := 2) (ψ := sampleTaut3CNF) + (A₀ := []) (Nat.zero_le _) (fun _ hr => nomatch hr) (A := A) (γ := fun _ => γ₀) rfl hA q_cand + have hfinal := CNF.candidateQueryRows_length_and_weight_le (B := 2) (ψ := sampleTaut3CNF) + (A₀ := []) (Nat.zero_le _) (fun _ hr => nomatch hr) (A := A) (γ := fun _ => γ₀) rfl hA q_final + simpa only [Fintype.card_fin] using ⟨hcand.1, hcand.2, hfinal.1, hfinal.2⟩ + +/-- At `k = 3`, the Proposition 6.4 `interpolationScale` exponent multipliers form a strictly +increasing chain. -/ +theorem prop64_scale_coeffs_strict_mono_k3 : + CNF.prop64BranchExamScaleCoeff 3 < CNF.prop64LeafQueryExamScaleCoeff 3 ∧ + CNF.prop64LeafQueryExamScaleCoeff 3 < CNF.prop64TreeExamScaleCoeff 3 ∧ + CNF.prop64TreeExamScaleCoeff 3 < CNF.prop64TotalExamScaleCoeff 3 := by + unfold CNF.prop64LeafQueryExamScaleCoeff CNF.prop64TreeExamScaleCoeff + CNF.prop64TotalExamScaleCoeff + omega + +/-- Concrete 3-CNF on `Fin N` (`1 ≤ N`) with one tautological clause and one width-3 clause. -/ +def sampleLargeTaut3CNF (N : ℕ) [NeZero N] : CNF (Fin N) := + [[(0, true), (0, false), (0, true)], + [(0, true), (0, true), (0, true)]] + +theorem sampleLargeTaut3CNF_width_le_three (N : ℕ) [NeZero N] : + ∀ c ∈ sampleLargeTaut3CNF N, c.length ≤ 3 := by + intro c hc + simp only [sampleLargeTaut3CNF, List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with rfl | rfl <;> simp + +private theorem pos_of_two_pow_le {m n : ℕ} (h : 2 ^ m ≤ n) : 0 < n := + lt_of_lt_of_le (Nat.pow_pos two_pos) h + +/-- Nonvacuous instantiation of +`CNF.exists_prop64NormalizedLeaves_total_recovery_and_examBound` at `k = 3` on a concrete 3-CNF +with a tautological clause over `V = Fin N₃`, exercising: +1. exact normalized leaf-summed model-count conservation, +2. the per-leaf greedy trajectory `A` and per-query `ReplacementDesign` recovery and actual + branch-summed `toCountingDesign` examination bound for **every** evaluated query + `q : CNF.LeafCandidateQueryIndex (Fin N₃) B L.toCNF` (including discarded candidates + `Sum.inl (i, γ')` and the final query `Sum.inr ()`), and +3. the candidate-indexed leaf examination sum (`CNF.prop64LeafQueryExamScaleCoeff 3`), + tree-wide final-query examination sum (`CNF.prop64TreeExamScaleCoeff 3`), and + total candidate-indexed tree-wide examination sum (`CNF.prop64TotalExamScaleCoeff 3`) + evaluated on the **actual** `toCountingDesign` examination costs of each query `q`. -/ +theorem nonvacuous_prop64NormalizedLeaves_total_recovery_and_actual_candidate_examBound_k3 : + ∃ (N₃ : ℕ) (_ : NeZero N₃), 2 ^ 640000 ≤ N₃ ∧ + let φ := sampleLargeTaut3CNF N₃ + let B := CNF.prop64LeafClauseRatio 3 (Fintype.card (Fin N₃)) + ((φ.prop64NormalizedLeaves 3).map fun L => L.toCNF.modelCountOn Finset.univ).sum = + φ.modelCountOn Finset.univ ∧ + 2 ≤ numGroups (Fintype.card (Fin N₃)) ∧ + (φ.prop64NormalizedLeaves 3).length ≤ + 2 ^ (Fintype.card (Fin N₃) / numGroups (Fintype.card (Fin N₃)) + 1) ∧ + ((φ.prop64NormalizedLeaves 3).length : ℝ) ≤ + (2 : ℝ) ^ (17 * interpolationScale (Fintype.card (Fin N₃))) ∧ + ∃ (actualQueryExam : (L : ClauseSet (Fin N₃)) → + CNF.LeafCandidateQueryIndex (Fin N₃) B L.toCNF → ℝ), + (∀ L ∈ φ.prop64NormalizedLeaves 3, + let ψ := L.toCNF + let D₀ := CNF.initialRowWeightBound B ψ.length + let P := CNF.greedyRowListLength B ψ.length + let b₀ := CNF.parityBranchThreshold 3 D₀ (Fintype.card (Fin N₃)) + (∀ c ∈ ψ, c.length ≤ 3) ∧ + ψ.length ≤ B * Fintype.card (Fin N₃) ∧ + ∃ A : ℕ → List (Fin ψ.length → Bool), + commonZeroCount univ + (ψ.parityRowSystem (CNF.candidateQueryRows (B := B) A (Sum.inr ()))) = + ψ.modelCountOn Finset.univ ∧ + (∀ (i : Fin (3 * Fintype.card (Fin N₃))) (γ' : Fin P → Fin ψ.length × Bool), + commonZeroCount univ (ψ.parityRowSystem (A (i.1 + 1))) ≤ + commonZeroCount univ + (ψ.parityRowSystem (CNF.candidateQueryRows A (Sum.inl (i, γ'))))) ∧ + (∀ q : CNF.LeafCandidateQueryIndex (Fin N₃) B ψ, + let rows := CNF.candidateQueryRows A q + rows.length ≤ 6 * Fintype.card (Fin N₃) ∧ + (∀ r ∈ rows, weight r ≤ D₀) ∧ + let S := heavyVars univ (univ : Finset (Fin rows.length)) + (fun j => equationScope (ψ.parityRowSystem rows j)) b₀ + let n' := Fintype.card ↥(univ \ S) + let e : ↥(univ \ S) ≃ Fin n' := Fintype.equivFin ↥(univ \ S) + ∃ (hF : ∀ b : Fin N₃ → Bool, + Feasible (CNF.prop64ScheduleExponent 3) n' (b₀ + 1) + (max (3 * (D₀ * 2 ^ 3)) 1) + (∑ f : {j : Fin rows.length // + j ∈ (univ : Finset (Fin rows.length))} ⊕ Fin n', + #(branchAugmentedScope S e univ (ψ.parityRowSystem rows) b f))) + (D : ∀ b : Fin N₃ → Bool, + ReplacementDesign + (branchAugmentedScope S e univ (ψ.parityRowSystem rows) b) + (numNodes n') (numGroups n') + (intervalStart (CNF.prop64ScheduleExponent 3) n') + (rowBound (CNF.prop64ScheduleExponent 3) n') (tauRat n')), + (commonZeroCount (univ : Finset (Fin rows.length)) + (ψ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + ((univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent 3) n') : ℤ) 3 + (branchPrecision (Fintype.card (Fin N₃))) + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩))).eval 0 / + clearedProductDenom + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent 3) n') : ℤ) 3 + (branchPrecision (Fintype.card (Fin N₃))) + #(univ : Finset (Fin rows.length))) % + ((2 : ℤ) ^ branchPrecision (Fintype.card (Fin N₃)))) ∧ + actualQueryExam L q = + ∑ b ∈ branchAssignments S, + let d := 3 * (rows.length + 2 * (branchPrecision (Fintype.card (Fin N₃)) - 1)) + let q_ord := (d * rowBound (CNF.prop64ScheduleExponent 3) n') / numNodes n' + let C := (hF b).toCountingDesign (D b) univ + ∑ t : Fin (numNodes n'), + (#{p : Finset (Fin n') × Finset (Fin n') | + #p.1 ≤ q_ord ∧ p.2 ⊆ p.1} : ℝ) * + (2 * (#(C.measurementBox t) : ℝ) * + ∑ g : Fin (numGroups n'), + (Fintype.card (C.LocalCube t g) : ℝ))) ∧ + (∑ q : CNF.LeafCandidateQueryIndex (Fin N₃) B ψ, actualQueryExam L q) ≤ + (2 : ℝ) ^ ((CNF.prop64LeafQueryExamScaleCoeff 3 : ℝ) * + interpolationScale (Fintype.card (Fin N₃)))) ∧ + ((φ.prop64NormalizedLeaves 3).map fun (L : ClauseSet (Fin N₃)) => + actualQueryExam L (Sum.inr ())).sum ≤ + (2 : ℝ) ^ ((CNF.prop64TreeExamScaleCoeff 3 : ℝ) * + interpolationScale (Fintype.card (Fin N₃))) ∧ + ((φ.prop64NormalizedLeaves 3).map fun (L : ClauseSet (Fin N₃)) => + ∑ q : CNF.LeafCandidateQueryIndex (Fin N₃) B L.toCNF, actualQueryExam L q).sum ≤ + (2 : ℝ) ^ ((CNF.prop64TotalExamScaleCoeff 3 : ℝ) * + interpolationScale (Fintype.card (Fin N₃))) := by + obtain ⟨N₃, hN₃, hprop64⟩ := + CNF.exists_prop64NormalizedLeaves_total_recovery_and_examBound (by decide : 2 ≤ 3) + have hpos : 0 < N₃ := pos_of_two_pow_le hN₃ + have : NeZero N₃ := ⟨Nat.ne_of_gt hpos⟩ + have hcard : N₃ ≤ Fintype.card (Fin N₃) := by rw [Fintype.card_fin] + set φ := sampleLargeTaut3CNF N₃ + set B := CNF.prop64LeafClauseRatio 3 (Fintype.card (Fin N₃)) + obtain ⟨hsum, hs2, hlen_pow, hlen_scale, hleaf, htree, htotal⟩ := + hprop64 φ (sampleLargeTaut3CNF_width_le_three N₃) hcard + classical + let actualQueryExam : (L : ClauseSet (Fin N₃)) → + CNF.LeafCandidateQueryIndex (Fin N₃) B L.toCNF → ℝ := + fun L q => + if hL : L ∈ φ.prop64NormalizedLeaves 3 then + let ψ := L.toCNF + let D₀ := CNF.initialRowWeightBound B ψ.length + let b₀ := CNF.parityBranchThreshold 3 D₀ (Fintype.card (Fin N₃)) + let A := (hleaf L hL).2.2.2.choose + let hA_spec := (hleaf L hL).2.2.2.choose_spec + let rows := CNF.candidateQueryRows A q + let S := heavyVars univ (univ : Finset (Fin rows.length)) + (fun j => equationScope (ψ.parityRowSystem rows j)) b₀ + let n' := Fintype.card ↥(univ \ S) + let e : ↥(univ \ S) ≃ Fin n' := Fintype.equivFin ↥(univ \ S) + let hpack := ((hA_spec.2.2.1 q).2.2 e).2.1 + let hF := hpack.choose + let D := hpack.choose_spec.choose + ∑ b ∈ branchAssignments S, + let d := 3 * (rows.length + 2 * (branchPrecision (Fintype.card (Fin N₃)) - 1)) + let q_ord := (d * rowBound (CNF.prop64ScheduleExponent 3) n') / numNodes n' + let C := (hF b).toCountingDesign (D b) univ + ∑ t : Fin (numNodes n'), + (#{p : Finset (Fin n') × Finset (Fin n') | + #p.1 ≤ q_ord ∧ p.2 ⊆ p.1} : ℝ) * + (2 * (#(C.measurementBox t) : ℝ) * + ∑ g : Fin (numGroups n'), + (Fintype.card (C.LocalCube t g) : ℝ)) + else 0 + have hactual_bound : ∀ L ∈ φ.prop64NormalizedLeaves 3, + ∀ q : CNF.LeafCandidateQueryIndex (Fin N₃) B L.toCNF, + actualQueryExam L q ≤ + (2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff 3 + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card (Fin N₃))) := by + intro L hL q + dsimp only [actualQueryExam] + rw [dite_eq_left_of_eq_true (eq_true hL)] + let ψ := L.toCNF + let D₀ := CNF.initialRowWeightBound B ψ.length + let b₀ := CNF.parityBranchThreshold 3 D₀ (Fintype.card (Fin N₃)) + let A := (hleaf L hL).2.2.2.choose + let hA_spec := (hleaf L hL).2.2.2.choose_spec + let rows := CNF.candidateQueryRows A q + let S := heavyVars univ (univ : Finset (Fin rows.length)) + (fun j => equationScope (ψ.parityRowSystem rows j)) b₀ + let n' := Fintype.card ↥(univ \ S) + let e : ↥(univ \ S) ≃ Fin n' := Fintype.equivFin ↥(univ \ S) + have hq_e := (hA_spec.2.2.1 q).2.2 e + have hexam := hq_e.2.1.choose_spec.choose_spec.2.2 + exact hq_e.2.2 _ fun b _ => hexam b univ + refine ⟨N₃, inferInstance, hN₃, hsum, hs2, hlen_pow, hlen_scale, actualQueryExam, + fun L hL => ?_, + htree (fun L => actualQueryExam L (Sum.inr ())) (fun L hL => hactual_bound L hL (Sum.inr ())), + htotal actualQueryExam hactual_bound⟩ + have hk_ψ := (hleaf L hL).1 + have hm_ψ := (hleaf L hL).2.1 + let A := (hleaf L hL).2.2.2.choose + have hA_spec := (hleaf L hL).2.2.2.choose_spec + refine ⟨hk_ψ, hm_ψ, A, hA_spec.1, hA_spec.2.1, fun q => ?_, + hA_spec.2.2.2 (actualQueryExam L) (hactual_bound L hL)⟩ + obtain ⟨hlen_q, hw_q, hq_all_e⟩ := hA_spec.2.2.1 q + refine ⟨hlen_q, hw_q, ?_⟩ + intro S n' e + have hpack := (hq_all_e e).2.1 + let hF := hpack.choose + let D := hpack.choose_spec.choose + have hrec := hpack.choose_spec.choose_spec.1 + refine ⟨hF, D, hrec, ?_⟩ + dsimp only [actualQueryExam] + rw [dite_eq_left_of_eq_true (eq_true hL)] + +end CslibTests From 098bb30ee8164fc9d20587bf9e59276852750fae Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 06:23:06 -0400 Subject: [PATCH 2/2] fix(FineGrained): qualify counting test names and wrap docs Keep the bounded shared-definition migration introduced in 7a14a043f. Fully qualify the nine test references as Cslib.BitString names because CslibTests does not open Cslib. Wrap the two expanded library doc lines without changing their words. No imports, opens, aliases, tactic changes, resource overrides, or changes to the mathematical statements or tests. Relative to reviewed 734e8524721bcda3599a69ddded024d8a6433f96, the owned payloads have exactly 41 definition-name substitutions (32 library, 9 test), plus whitespace-only wrapping in the leading library docstring. Reversing the names gives exact test byte identity and exact library identity after normalizing only that docstring whitespace. All unrelated actual-main 30bd34c7 files and every aggregate import are preserved. Validation: after scripts/cache/ensure.sh in the isolated worktree, lake build --wfail --iofail Complexity.Computability.Complexity.FineGrained.GeneralCNFCountingAsymptotics ComplexityTests.Computability.Complexity.FineGrained.GeneralCNFCountingAsymptotics passed (6382 jobs). Lean MCP tools were unavailable; targeted CLI fallback. Exact-head hosted full gates remain the coordinator's publication step. Original mathematical author: worker-jetski-4aebfa9b (Gemini). Bounded coordinator repair: worker-codex-general-counting-refresh-1322 (Codex), under PR #1322 issuecomment-6439245804. Existing source credit and curated-abstract no-impact assessment are unchanged. --- .../GeneralCNFCountingAsymptotics.lean | 8 ++++---- .../GeneralCNFCountingAsymptotics.lean | 18 +++++++++--------- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Complexity/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean b/Complexity/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean index 33e313975..7fa9620a6 100644 --- a/Complexity/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean +++ b/Complexity/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean @@ -49,8 +49,8 @@ asymptotic `interpolationScale` tree-exponent and candidate-query overhead bound - `CNF.LeafCandidateQueryIndex V B ψ` and `CNF.candidateQueryRows A q`: index all parity-row systems evaluated during the `3 * n` greedy rounds of Lemma 6.2 (`Sum.inl (i, γ')` for `i : Fin (3 * Fintype.card V)` and ordered candidate list - `γ' : Fin (BitString.greedyRowListLength B ψ.length) → Fin ψ.length × Bool`, including discarded - candidates counted with list multiplicity, plus `Sum.inr ()` for the final query + `γ' : Fin (BitString.greedyRowListLength B ψ.length) → Fin ψ.length × Bool`, including + discarded candidates counted with list multiplicity, plus `Sum.inr ()` for the final query `A (3 * Fintype.card V)`), with exact cardinality `3 * Fintype.card V * (2 * ψ.length) ^ P + 1 ≤ CNF.leafCandidateQueryBound B ψ` (`CNF.card_leafCandidateQueryIndex_eq`, `CNF.card_leafCandidateQueryIndex_le`). @@ -59,8 +59,8 @@ asymptotic `interpolationScale` tree-exponent and candidate-query overhead bound Hamming weight at most `BitString.initialRowWeightBound B ψ.length`. - `CNF.greedyRowListLength_le_mul_pow_clog` and `CNF.exists_prop64_leafCandidateQueryBound_le_interpolationScale`: prove - `BitString.greedyRowListLength B m ≤ 20000 * B ^ 2 * (Nat.clog 2 (2 * m + 4)) ^ 2` for all `B, m` - and apply `SparseCountingScale.eventually_query_overhead_poly_le` to bound + `BitString.greedyRowListLength B m ≤ 20000 * B ^ 2 * (Nat.clog 2 (2 * m + 4)) ^ 2` + for all `B, m` and apply `SparseCountingScale.eventually_query_overhead_poly_le` to bound `(CNF.leafCandidateQueryBound B ψ : ℝ) ≤ (2 : ℝ) ^ interpolationScale (Fintype.card V)` for every Proposition 6.4 leaf formula `ψ = L.toCNF`. - `CNF.exists_prop64NormalizedLeaves_greedy_total_recovery_and_examBound` and diff --git a/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean b/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean index adb3a6199..9f115bbd5 100644 --- a/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean +++ b/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFCountingAsymptotics.lean @@ -91,12 +91,12 @@ both a round-`0` candidate query `Sum.inl (0, γ₀)` and the final query `Sum.i `sampleTaut3CNF`. -/ theorem sampleTaut3CNF_candidateQueryIndex_and_rows_bounds : Fintype.card (CNF.LeafCandidateQueryIndex (Fin 4) 2 sampleTaut3CNF) = - 12 * 6 ^ (BitString.greedyRowListLength 2 3) + 1 ∧ + 12 * 6 ^ (Cslib.BitString.greedyRowListLength 2 3) + 1 ∧ Fintype.card (CNF.LeafCandidateQueryIndex (Fin 4) 2 sampleTaut3CNF) ≤ CNF.leafCandidateQueryBound 2 sampleTaut3CNF ∧ - BitString.greedyRowListLength 2 sampleTaut3CNF.length ≤ + Cslib.BitString.greedyRowListLength 2 sampleTaut3CNF.length ≤ 20000 * 2 ^ 2 * (Nat.clog 2 (2 * sampleTaut3CNF.length + 4)) ^ 2 ∧ - let γ₀ : Fin (BitString.greedyRowListLength 2 sampleTaut3CNF.length) → + let γ₀ : Fin (Cslib.BitString.greedyRowListLength 2 sampleTaut3CNF.length) → Fin sampleTaut3CNF.length × Bool := fun _ => (⟨0, by decide⟩, true) let A : ℕ → List (Fin sampleTaut3CNF.length → Bool) := @@ -106,10 +106,10 @@ theorem sampleTaut3CNF_candidateQueryIndex_and_rows_bounds : let q_final : CNF.LeafCandidateQueryIndex (Fin 4) 2 sampleTaut3CNF := Sum.inr () (CNF.candidateQueryRows A q_cand).length ≤ 24 ∧ (∀ r ∈ CNF.candidateQueryRows A q_cand, - weight r ≤ BitString.initialRowWeightBound 2 sampleTaut3CNF.length) ∧ + weight r ≤ Cslib.BitString.initialRowWeightBound 2 sampleTaut3CNF.length) ∧ (CNF.candidateQueryRows A q_final).length ≤ 24 ∧ (∀ r ∈ CNF.candidateQueryRows A q_final, - weight r ≤ BitString.initialRowWeightBound 2 sampleTaut3CNF.length) := by + weight r ≤ Cslib.BitString.initialRowWeightBound 2 sampleTaut3CNF.length) := by refine ⟨?_, CNF.card_leafCandidateQueryIndex_le 2 sampleTaut3CNF, CNF.greedyRowListLength_le_mul_pow_clog 2 sampleTaut3CNF.length, ?_⟩ · rw [CNF.card_leafCandidateQueryIndex_eq, Fintype.card_fin, @@ -173,8 +173,8 @@ theorem nonvacuous_prop64NormalizedLeaves_total_recovery_and_actual_candidate_ex CNF.LeafCandidateQueryIndex (Fin N₃) B L.toCNF → ℝ), (∀ L ∈ φ.prop64NormalizedLeaves 3, let ψ := L.toCNF - let D₀ := BitString.initialRowWeightBound B ψ.length - let P := BitString.greedyRowListLength B ψ.length + let D₀ := Cslib.BitString.initialRowWeightBound B ψ.length + let P := Cslib.BitString.greedyRowListLength B ψ.length let b₀ := CNF.parityBranchThreshold 3 D₀ (Fintype.card (Fin N₃)) (∀ c ∈ ψ, c.length ≤ 3) ∧ ψ.length ≤ B * Fintype.card (Fin N₃) ∧ @@ -259,7 +259,7 @@ theorem nonvacuous_prop64NormalizedLeaves_total_recovery_and_actual_candidate_ex fun L q => if hL : L ∈ φ.prop64NormalizedLeaves 3 then let ψ := L.toCNF - let D₀ := BitString.initialRowWeightBound B ψ.length + let D₀ := Cslib.BitString.initialRowWeightBound B ψ.length let b₀ := CNF.parityBranchThreshold 3 D₀ (Fintype.card (Fin N₃)) let A := (hleaf L hL).2.2.2.choose let hA_spec := (hleaf L hL).2.2.2.choose_spec @@ -291,7 +291,7 @@ theorem nonvacuous_prop64NormalizedLeaves_total_recovery_and_actual_candidate_ex dsimp only [actualQueryExam] rw [dite_eq_left_of_eq_true (eq_true hL)] let ψ := L.toCNF - let D₀ := BitString.initialRowWeightBound B ψ.length + let D₀ := Cslib.BitString.initialRowWeightBound B ψ.length let b₀ := CNF.parityBranchThreshold 3 D₀ (Fintype.card (Fin N₃)) let A := (hleaf L hL).2.2.2.choose let hA_spec := (hleaf L hL).2.2.2.choose_spec