From 734e8524721bcda3599a69ddded024d8a6433f96 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Tue, 27 Oct 2026 08:20:51 +0000 Subject: [PATCH 1/3] 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 f6e5b348ca6a290e933a2cd63eb948abdd077a17 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Tue, 27 Oct 2026 09:04:39 +0000 Subject: [PATCH 2/3] feat(Computability/Complexity/FineGrained): Stage-1/2 JetTable and Hermite-Cramer recovery across Sec 6.3/6.4 --- Complexity.lean | 1 + .../GeneralCNFHermiteRecovery.lean | 1274 +++++++++++++++++ .../GeneralCNFHermiteRecovery.lean | 409 ++++++ 3 files changed, 1684 insertions(+) create mode 100644 Complexity/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean create mode 100644 ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean diff --git a/Complexity.lean b/Complexity.lean index 6f3dadcd7..950c6b133 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -771,6 +771,7 @@ 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.GeneralCNFHermiteRecovery 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/GeneralCNFHermiteRecovery.lean b/Complexity/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean new file mode 100644 index 000000000..8b63129f2 --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean @@ -0,0 +1,1274 @@ +/- +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.GeneralCNFCountingAsymptotics +public import Complexity.Foundations.BooleanAnalysis.SparseHermiteRecovery + +/-! +# Stage-1/Stage-2 `clearedParityJetTable` and Hermite–Cramer recovery across Section 6.3/6.4 + +This module connects the Stage-1/Stage-2 `JetTable` bridge and unconditional Hermite–Cramer +determinant recovery (`Complexity.Foundations.BooleanAnalysis.SparseHermiteRecovery`) with the +Section 6.3 compiled CNF parity-row schedule +(`Complexity.Computability.Complexity.FineGrained.GeneralCNFBranchSchedule`) and the Section 6.4 +Proposition 6.4 tree-wide candidate-indexed recovery and examination bounds +(`Complexity.Computability.Complexity.FineGrained.GeneralCNFCountingAsymptotics`) of +[OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] (Sections 5.4–5.5, 6.1–6.4, +and Appendices A–B, printed pp. 37–50): + +1. **Appendix B.2–B.3 Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer coordinate recovery + and arbitrary-`ι` branch-summed recovery (`Cslib.BitString`, printed pp. 48–50):** + - `hermiteCramerNumerator_clearedParityJetTable_eq_mul`: at distinct integer nodes + `nodes : Fin Q → ℤ` with `(k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J`, the Cramer determinant + `hermiteCramerNumerator nodes hQ hJ` of + `fun t j => clearedParityJetTable I P d_den k ℓ J θ (nodes t) j s` + for each `V`-degree coordinate `s : Fin ℓ` equals + `(Polynomial.hermiteMatrix nodes J).det *` + `(univariateClearedParityCoord I P d_den k ℓ θ s.1).eval 0`. + - `emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount` and + `emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount`: summing the + exact integer Cramer quotients of the Stage-1/Stage-2 `JetTable` entries + `clearedParityJetTable I P (commonDenom Q R : ℤ) k ℓ J` + `(designReplacementScaledIntMap D emb) (nodeInt t) j s` + over `s : Fin ℓ` and reducing modulo `2 ^ ℓ` recovers `commonZeroCount I P` without auxiliary + `D_H` or `hcramer` premises (Appendix B.3, eq. `(B.1)`). + - `commonZeroCount_eq_sum_branch_hermiteCramerNumerator_design_of_fintype` and + `commonZeroCount_eq_sum_branch_clearedParityJetTable_design`: generalize branch-summed + Hermite–Cramer determinant recovery from `Fin n` to arbitrary finite variable types + `[Fintype ι] [DecidableEq ι]` (`S : Finset ι`, `e : ↥(univ \ S) ≃ Fin n'`) at shared precision + `ℓ = branchPrecision (Fintype.card ι)` and canonical jet order + `J = sparseParityJetOrder k R Q #I ℓ`, both for the single truncated-sum Cramer determinant and + for the Stage-1/Stage-2 `clearedParityJetTable` coordinate sum over `s : Fin ℓ`. + +2. **Section 6.3 compiled CNF parity-row schedule Hermite–Cramer and `clearedParityJetTable` + recovery with `interpolationScale` examination bounds (`Cslib.Logic.PL.CNF`, pp. 38–43, 48–50):** + - `CNF.commonZeroCount_parityRowSystem_eq_sum_branch_hermiteCramerNumerator_design`, + `CNF.numPassing_eq_sum_branch_hermiteCramerNumerator_design`, + `CNF.commonZeroCount_parityRowSystem_eq_sum_branch_clearedParityJetTable_design`, and + `CNF.numPassing_eq_sum_branch_clearedParityJetTable_design`: specialize both Hermite–Cramer + recovery forms to `φ.branchParityRowSystem rows S e b` across `b ∈ branchAssignments S`. + - `CNF.exists_branch_schedule_hermiteCramer_and_examBound_parityRowSystem_of_le_clog_pow`, + `CNF.exists_greedy_parityRowSystem_hermiteCramer_recovery_and_examBound_of_le_clog_pow`, and + `CNF.exists_parityRowSystem_modelCountOn_hermiteCramer_recovery_and_examBound_of_le_clog_pow`: + certify that the Lemma 4.8 per-branch `ReplacementDesign` family `D b` at + `b₀ = CNF.parityBranchThreshold k W (Fintype.card V)` and `β = 2 * β_B + 5` has positive node + count `0 < numNodes n'` and simultaneously recovers + `commonZeroCount univ (φ.parityRowSystem rows)` (and `φ.modelCountOn Finset.univ` after + `3 * n` greedy rounds) via **both** explicit Hermite–Cramer truncated-sum determinants and + Stage-1/Stage-2 `clearedParityJetTable` coordinate sums at `nodeInt` and canonical jet order + `J = sparseParityJetOrder k (rowBound (2 * β_B + 5) n') (numNodes n') rows.length ℓ`, while + satisfying the univariate degree bound and the per-branch / branch-summed + `2 ^ (A * interpolationScale (Fintype.card V))` domain-examination bounds. + +3. **Proposition 6.4 tree-wide candidate-indexed Hermite–Cramer & `clearedParityJetTable` recovery + and total examination bounds (`Cslib.Logic.PL.CNF`, §6.4 & Appendices A–B, pp. 43–50):** + - `CNF.exists_prop64NormalizedLeaves_greedy_total_hermiteCramer_recovery_and_examBound` and + `CNF.exists_prop64NormalizedLeaves_total_hermiteCramer_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`, on every normalized leaf + `L ∈ φ.prop64NormalizedLeaves k` (`ψ := L.toCNF`) and every candidate query + `q : CNF.LeafCandidateQueryIndex V B ψ` (covering all `3 * n` greedy stages and all ordered + candidate lists `γ'` with list multiplicity, including discarded candidates, plus the final + query `Sum.inr ()`), the certified per-branch `ReplacementDesign` family `D q b` recovers + `commonZeroCount univ (ψ.parityRowSystem (CNF.candidateQueryRows A q))` via **both** explicit + Hermite–Cramer truncated-sum determinants and Stage-1/Stage-2 `clearedParityJetTable` + coordinate sums at `nodeInt` and canonical jet order `sparseParityJetOrder`, while satisfying + the per-query (`≤ 2 ^ ((CNF.prop64BranchExamScaleCoeff k + 32) * interpolationScale n)`), + per-leaf candidate-summed + (`≤ 2 ^ (CNF.prop64LeafQueryExamScaleCoeff k * interpolationScale n)`), + and tree-wide candidate-summed + (`≤ 2 ^ (CNF.prop64TotalExamScaleCoeff k * interpolationScale n)`) + domain-examination bounds. + +## Main results + +* `Cslib.BitString.hermiteCramerNumerator_clearedParityJetTable_eq_mul`, + `Cslib.BitString.emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount`, + `Cslib.BitString.emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount`, + `Cslib.BitString.commonZeroCount_eq_sum_branch_hermiteCramerNumerator_design_of_fintype`, + `Cslib.BitString.commonZeroCount_eq_sum_branch_clearedParityJetTable_design` +* `Cslib.Logic.PL.CNF.commonZeroCount_parityRowSystem_eq_sum_branch_hermiteCramerNumerator_design`, + `Cslib.Logic.PL.CNF.numPassing_eq_sum_branch_hermiteCramerNumerator_design`, + `Cslib.Logic.PL.CNF.commonZeroCount_parityRowSystem_eq_sum_branch_clearedParityJetTable_design`, + `Cslib.Logic.PL.CNF.numPassing_eq_sum_branch_clearedParityJetTable_design` +* `CNF.exists_branch_schedule_hermiteCramer_and_examBound_parityRowSystem_of_le_clog_pow`, + `CNF.exists_greedy_parityRowSystem_hermiteCramer_recovery_and_examBound_of_le_clog_pow`, + `CNF.exists_parityRowSystem_modelCountOn_hermiteCramer_recovery_and_examBound_of_le_clog_pow` +* `CNF.exists_prop64NormalizedLeaves_greedy_total_hermiteCramer_recovery_and_examBound`, + `CNF.exists_prop64NormalizedLeaves_total_hermiteCramer_recovery_and_examBound` + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] + (Sections 5.4–5.5, pp. 38–39; Sections 6.1–6.4, pp. 39–44; Appendices A–B, pp. 44–50) +-/ + +@[expose] public noncomputable section + +open Finset Polynomial +open scoped BigOperators + +/-! ### 1. Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer recovery -/ + +namespace Cslib.BitString + +open Cslib.LinearAlgebra + +variable {ι κ : Type*} + +/-- **Cramer numerator factorization for `clearedParityJetTable` (Appendix B.2–B.3, eq. `(B.1)`, +pp. 48–50)**: when `(k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J`, the Cramer determinant of the +`s`-th `V`-degree coordinate (`s : Fin ℓ`) of the Stage-1/Stage-2 integer Taylor-jet table +`clearedParityJetTable I P d_den k ℓ J θ` at `nodes` equals +`(Polynomial.hermiteMatrix nodes J).det *` +`(univariateClearedParityCoord I P d_den k ℓ θ s.1).eval 0`. -/ +theorem hermiteCramerNumerator_clearedParityJetTable_eq_mul [Fintype ι] [DecidableEq ι] + (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) {k ℓ R_deg Q J : ℕ} + (nodes : Fin Q → ℤ) (hQ : 0 < Q) (hJ : 0 < J) + (θ : (ι → Bool) → κ → ι → Polynomial ℤ) + (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) + (hθ : ∀ x : ι → Bool, ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (θ x i v).natDegree ≤ R_deg) + (hQJ : (k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J) (s : Fin ℓ) : + hermiteCramerNumerator nodes hQ hJ + (fun t j => clearedParityJetTable I P d_den k ℓ J θ (nodes t) j s) = + (Polynomial.hermiteMatrix nodes J).det * + (univariateClearedParityCoord I P d_den k ℓ θ s.1).eval 0 := by + simp only [clearedParityJetTable_apply] + exact hermiteCramerNumerator_univariateClearedParityCoord_eq_mul I P d_den nodes hQ hJ θ hk hθ + hQJ s.2 + +/-- **Unconditional Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer coordinate recovery of +`commonZeroCount` (Appendix B.2–B.3, eq. `(B.1)`, pp. 48–50)**: at distinct integer nodes +`nodes : Fin Q → ℤ` with `(k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J`, `d_den ≠ 0`, and +`Fintype.card ι < ℓ`, summing the exact integer Cramer quotients of `clearedParityJetTable` over +`s : Fin ℓ` and reducing modulo `2 ^ ℓ` recovers `commonZeroCount I P`. -/ +theorem emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount + [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {d_den : ℤ} + (hd : d_den ≠ 0) {k ℓ R_deg Q J : ℕ} {nodes : Fin Q → ℤ} (hnodes : Function.Injective nodes) + (hQ : 0 < Q) (hJ : 0 < J) (hℓ : Fintype.card ι < ℓ) + (θ : (ι → Bool) → κ → ι → Polynomial ℤ) + (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) + (hdeg : ∀ x : ι → Bool, ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (θ x i v).natDegree ≤ R_deg) + (hθ : ∀ x : ι → Bool, ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, + (θ x i v).eval 0 = d_den * bitVal ℤ (x v)) + (hQJ : (k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J) : + (∑ s : Fin ℓ, + hermiteCramerNumerator nodes hQ hJ + (fun t j => clearedParityJetTable I P d_den k ℓ J θ (nodes t) j s) / + (clearedProductDenom d_den k ℓ #I * (Polynomial.hermiteMatrix nodes J).det)) % + ((2 : ℤ) ^ ℓ) = + commonZeroCount I P := by + simp only [clearedParityJetTable_apply] + rw [Fin.sum_univ_eq_sum_range (fun s => + hermiteCramerNumerator nodes hQ hJ + (fun t j => + (Polynomial.taylor (nodes t) + (univariateClearedParityCoord I P d_den k ℓ θ s)).coeff j.1) / + (clearedProductDenom d_den k ℓ #I * (Polynomial.hermiteMatrix nodes J).det))] + exact emod_sum_hermiteCramerNumerator_ediv_eq_commonZeroCount I P hd hnodes hQ hJ hℓ θ hk hdeg + hθ hQJ + +/-- **Concrete `ReplacementDesign` Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer +coordinate recovery of `commonZeroCount` (§5.4 & Appendix B.2–B.3, eq. `(B.1)`, pp. 48–50)**: +for any `D : ReplacementDesign scope Q r A₀ R τ` with `0 < Q`, `0 < J`, `n < ℓ`, +`∀ i ∈ I, ∀ M ∈ P i, #M ≤ k`, and `(k * (R - 1)) * (#I + 2 * (ℓ - 1)) < Q * J`, summing the +Cramer quotients of `clearedParityJetTable` at `nodeInt` over `s : Fin ℓ` and reducing modulo +`2 ^ ℓ` recovers `commonZeroCount I P`. -/ +theorem emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount + {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type*} [Fintype F] + {scope : F → Finset (Fin n)} (D : ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) + (I : Finset κ) (P : κ → Finset (Finset (Fin n))) {k ℓ J : ℕ} + (hQ : 0 < Q) (hJ : 0 < J) (hℓ : n < ℓ) + (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) + (hQJ : (k * (R - 1)) * (#I + 2 * (ℓ - 1)) < Q * J) : + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := Q)) hQ hJ + (fun t j => + clearedParityJetTable I P (commonDenom Q R : ℤ) k ℓ J + (designReplacementScaledIntMap D emb) (nodeInt t) j s) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) = + commonZeroCount I P := by + simp only [clearedParityJetTable_apply] + rw [Fin.sum_univ_eq_sum_range (fun s => + hermiteCramerNumerator (nodeInt (Q := Q)) hQ hJ + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityCoord I P (commonDenom Q R : ℤ) k ℓ + (designReplacementScaledIntMap D emb) s)).coeff j.1) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det))] + exact emod_sum_hermiteCramerNumerator_design_eq_commonZeroCount D emb I P hQ hJ hℓ hk hQJ + +/-- **§5.5 & Appendix B.3 branch-summed Hermite–Cramer truncated-sum recovery of `commonZeroCount` +over arbitrary finite variable types `[Fintype ι] [DecidableEq ι]`**: given a heavy-variable subset +`S : Finset ι`, a free-variable relabeling `e : ↥(univ \ S) ≃ Fin n'`, and a per-branch +`ReplacementDesign` family `D b` (`0 < Q`), summing the branch modular residues of the concrete +`hermiteCramerNumerator` quotients at `nodeInt` and canonical jet order +`J = sparseParityJetOrder k R Q #I (branchPrecision (Fintype.card ι))` across +`b ∈ branchAssignments S` recovers `commonZeroCount I P`. -/ +theorem commonZeroCount_eq_sum_branch_hermiteCramerNumerator_design_of_fintype + [Fintype ι] [DecidableEq ι] {n' Q r A₀ R : ℕ} {τ : ℚ} + {F : (ι → Bool) → Type*} [∀ b, Fintype (F b)] + (S : Finset ι) (e : ↥(univ \ S) ≃ Fin n') + (I : Finset κ) (P : κ → Finset (Finset ι)) {k : ℕ} + (scope : (b : ι → Bool) → F b → Finset (Fin n')) + (D : (b : ι → Bool) → ReplacementDesign (scope b) Q r A₀ R τ) + (emb : (b : ι → Bool) → κ → F b) + (hQ : 0 < Q) (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) : + let ℓ := branchPrecision (Fintype.card ι) + let J := sparseParityJetOrder k R Q #I ℓ + (commonZeroCount I P : ℤ) = + ∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := Q)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum I + (fun i => relabelRestrictedMonomials S e b (P i)) + (commonDenom Q R : ℤ) k ℓ + (designReplacementScaledIntMap (D b) (emb b)))).coeff j) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) := by + intro ℓ J + rw [commonZeroCount_eq_sum_branch_emod_ediv_cleared S e I P (commonDenom_intCast_ne_zero Q R) + (fun b => designReplacementScaledIntMap (D b) (emb b)) hk + (fun b _ x j _ _ _ v _ => eval_zero_designReplacementScaledIntMap (D b) (emb b) x j v)] + refine sum_congr rfl fun b _ => ?_ + have hlt : n' < ℓ := by + have hle : n' ≤ Fintype.card ι := by + simpa only [Fintype.card_fin] using + (Fintype.card_congr e).symm.trans_le (Fintype.card_subtype_le _) + change n' < Fintype.card ι + 1 + omega + have hk_branch : ∀ i ∈ I, ∀ M ∈ relabelRestrictedMonomials S e b (P i), #M ≤ k := + fun i hi M hM => card_mem_relabelRestrictedMonomials_le (hk i hi) M hM + rw [emod_hermiteCramerNumerator_truncatedSum_design_eq_commonZeroCount (D b) (emb b) I + (fun i => relabelRestrictedMonomials S e b (P i)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) + hlt hk_branch (lt_mul_sparseParityJetOrder k R #I ℓ hQ)] + exact emod_ediv_eval_zero_clearedParityTruncatedSum_design_eq_commonZeroCount (D b) (emb b) I + (fun i => relabelRestrictedMonomials S e b (P i)) hlt hk_branch + +/-- **§5.5 & Appendix B.2–B.3 branch-summed Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer +coordinate recovery of `commonZeroCount` over arbitrary finite variable types**: under the same +hypotheses, summing the coordinate Cramer quotients of `clearedParityJetTable` over `s : Fin ℓ` +modulo `2 ^ ℓ` on each branch and summing across `b ∈ branchAssignments S` recovers +`commonZeroCount I P`. -/ +theorem commonZeroCount_eq_sum_branch_clearedParityJetTable_design + [Fintype ι] [DecidableEq ι] {n' Q r A₀ R : ℕ} {τ : ℚ} + {F : (ι → Bool) → Type*} [∀ b, Fintype (F b)] + (S : Finset ι) (e : ↥(univ \ S) ≃ Fin n') + (I : Finset κ) (P : κ → Finset (Finset ι)) {k : ℕ} + (scope : (b : ι → Bool) → F b → Finset (Fin n')) + (D : (b : ι → Bool) → ReplacementDesign (scope b) Q r A₀ R τ) + (emb : (b : ι → Bool) → κ → F b) + (hQ : 0 < Q) (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) : + let ℓ := branchPrecision (Fintype.card ι) + let J := sparseParityJetOrder k R Q #I ℓ + (commonZeroCount I P : ℤ) = + ∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := Q)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) + (fun t j => + clearedParityJetTable I + (fun i => relabelRestrictedMonomials S e b (P i)) + (commonDenom Q R : ℤ) k ℓ J + (designReplacementScaledIntMap (D b) (emb b)) (nodeInt t) j s) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) := by + intro ℓ J + rw [commonZeroCount_eq_sum_branch_emod_ediv_cleared S e I P (commonDenom_intCast_ne_zero Q R) + (fun b => designReplacementScaledIntMap (D b) (emb b)) hk + (fun b _ x j _ _ _ v _ => eval_zero_designReplacementScaledIntMap (D b) (emb b) x j v)] + refine sum_congr rfl fun b _ => ?_ + have hlt : n' < ℓ := by + have hle : n' ≤ Fintype.card ι := by + simpa only [Fintype.card_fin] using + (Fintype.card_congr e).symm.trans_le (Fintype.card_subtype_le _) + change n' < Fintype.card ι + 1 + omega + have hk_branch : ∀ i ∈ I, ∀ M ∈ relabelRestrictedMonomials S e b (P i), #M ≤ k := + fun i hi M hM => card_mem_relabelRestrictedMonomials_le (hk i hi) M hM + rw [emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount (D b) (emb b) + I (fun i => relabelRestrictedMonomials S e b (P i)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) + hlt hk_branch (lt_mul_sparseParityJetOrder k R #I ℓ hQ)] + exact emod_ediv_eval_zero_clearedParityTruncatedSum_design_eq_commonZeroCount (D b) (emb b) I + (fun i => relabelRestrictedMonomials S e b (P i)) hlt hk_branch + +end Cslib.BitString + +/-! ### 2. Section 6.3 CNF parity-row schedule Hermite–Cramer & `clearedParityJetTable` recovery -/ + +namespace Cslib.Logic.PL + +open Cslib.BitString +open Cslib.LinearAlgebra +open Cslib.Logic.PL.ClauseSet.Sparsification +open Cslib.Complexity.SubexponentialSAT +open Cslib.Complexity.SubexponentialSAT.ReplacementParams + +variable {V : Type*} + +section CNFDeterminantRecovery + +variable [Fintype V] [DecidableEq V] {n' Q r A₀ R : ℕ} {τ : ℚ} + +/-- **§5.4–5.5 & §6.3 branch-summed Hermite–Cramer truncated-sum recovery of `commonZeroCount` on +`φ.parityRowSystem rows`**: when every clause of `φ` has width at most `k` and `0 < Q`, summing the +per-branch `hermiteCramerNumerator` quotients of `univariateClearedParityTruncatedSum` at `nodeInt` +and canonical jet order `J = sparseParityJetOrder k R Q #(univ : Finset (Fin rows.length)) ℓ` +across `b ∈ branchAssignments S` recovers `commonZeroCount univ (φ.parityRowSystem rows)`. -/ +theorem CNF.commonZeroCount_parityRowSystem_eq_sum_branch_hermiteCramerNumerator_design + {F : (V → Bool) → Type*} [∀ b, Fintype (F b)] {φ : CNF V} {k : ℕ} + (hk : ∀ c ∈ φ, c.length ≤ k) (rows : List (Fin φ.length → Bool)) + (S : Finset V) (e : ↥(univ \ S) ≃ Fin n') + (scope : (b : V → Bool) → F b → Finset (Fin n')) + (D : (b : V → Bool) → ReplacementDesign (scope b) Q r A₀ R τ) + (emb : (b : V → Bool) → Fin rows.length → F b) (hQ : 0 < Q) : + let ℓ := branchPrecision (Fintype.card V) + let J := sparseParityJetOrder k R Q #(univ : Finset (Fin rows.length)) ℓ + (commonZeroCount (univ : Finset (Fin rows.length)) (φ.parityRowSystem rows) : ℤ) = + ∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := Q)) hQ + (sparseParityJetOrder_pos k R Q #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) (commonDenom Q R : ℤ) k ℓ + (designReplacementScaledIntMap (D b) (emb b)))).coeff j) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) := + commonZeroCount_eq_sum_branch_hermiteCramerNumerator_design_of_fintype S e + (univ : Finset (Fin rows.length)) (φ.parityRowSystem rows) scope D emb hQ + (fun j _ _M hM => CNF.card_mem_parityRowSystem_le hk rows j hM) + +/-- **§5.4–5.5 & §6.3 branch-summed Hermite–Cramer truncated-sum recovery of `numPassing`**: +under the same hypotheses, the branch-summed `hermiteCramerNumerator` quotients recover +`numPassing φ.violations rows`. -/ +theorem CNF.numPassing_eq_sum_branch_hermiteCramerNumerator_design + {F : (V → Bool) → Type*} [∀ b, Fintype (F b)] {φ : CNF V} {k : ℕ} + (hk : ∀ c ∈ φ, c.length ≤ k) (rows : List (Fin φ.length → Bool)) + (S : Finset V) (e : ↥(univ \ S) ≃ Fin n') + (scope : (b : V → Bool) → F b → Finset (Fin n')) + (D : (b : V → Bool) → ReplacementDesign (scope b) Q r A₀ R τ) + (emb : (b : V → Bool) → Fin rows.length → F b) (hQ : 0 < Q) : + let ℓ := branchPrecision (Fintype.card V) + let J := sparseParityJetOrder k R Q #(univ : Finset (Fin rows.length)) ℓ + (numPassing φ.violations rows : ℤ) = + ∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := Q)) hQ + (sparseParityJetOrder_pos k R Q #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) (commonDenom Q R : ℤ) k ℓ + (designReplacementScaledIntMap (D b) (emb b)))).coeff j) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) := by + rw [← CNF.commonZeroCount_parityRowSystem] + exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_hermiteCramerNumerator_design hk rows S e + scope D emb hQ + +/-- **§5.4–5.5, §6.3 & Appendix B.2–B.3 branch-summed Stage-1/Stage-2 `clearedParityJetTable` +Hermite–Cramer coordinate recovery of `commonZeroCount` on `φ.parityRowSystem rows`**: under the +same hypotheses, summing the coordinate Cramer quotients of `clearedParityJetTable` over +`s : Fin ℓ` modulo `2 ^ ℓ` on each branch and summing across `b ∈ branchAssignments S` recovers +`commonZeroCount univ (φ.parityRowSystem rows)`. -/ +theorem CNF.commonZeroCount_parityRowSystem_eq_sum_branch_clearedParityJetTable_design + {F : (V → Bool) → Type*} [∀ b, Fintype (F b)] {φ : CNF V} {k : ℕ} + (hk : ∀ c ∈ φ, c.length ≤ k) (rows : List (Fin φ.length → Bool)) + (S : Finset V) (e : ↥(univ \ S) ≃ Fin n') + (scope : (b : V → Bool) → F b → Finset (Fin n')) + (D : (b : V → Bool) → ReplacementDesign (scope b) Q r A₀ R τ) + (emb : (b : V → Bool) → Fin rows.length → F b) (hQ : 0 < Q) : + let ℓ := branchPrecision (Fintype.card V) + let J := sparseParityJetOrder k R Q #(univ : Finset (Fin rows.length)) ℓ + (commonZeroCount (univ : Finset (Fin rows.length)) (φ.parityRowSystem rows) : ℤ) = + ∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := Q)) hQ + (sparseParityJetOrder_pos k R Q #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + clearedParityJetTable (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) (commonDenom Q R : ℤ) k ℓ J + (designReplacementScaledIntMap (D b) (emb b)) (nodeInt t) j s) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) := + commonZeroCount_eq_sum_branch_clearedParityJetTable_design S e + (univ : Finset (Fin rows.length)) (φ.parityRowSystem rows) scope D emb hQ + (fun j _ _M hM => CNF.card_mem_parityRowSystem_le hk rows j hM) + +/-- **§5.4–5.5, §6.3 & Appendix B.2–B.3 branch-summed Stage-1/Stage-2 `clearedParityJetTable` +Hermite–Cramer coordinate recovery of `numPassing`**: under the same hypotheses, the branch-summed +coordinate Cramer quotients of `clearedParityJetTable` recover `numPassing φ.violations rows`. -/ +theorem CNF.numPassing_eq_sum_branch_clearedParityJetTable_design + {F : (V → Bool) → Type*} [∀ b, Fintype (F b)] {φ : CNF V} {k : ℕ} + (hk : ∀ c ∈ φ, c.length ≤ k) (rows : List (Fin φ.length → Bool)) + (S : Finset V) (e : ↥(univ \ S) ≃ Fin n') + (scope : (b : V → Bool) → F b → Finset (Fin n')) + (D : (b : V → Bool) → ReplacementDesign (scope b) Q r A₀ R τ) + (emb : (b : V → Bool) → Fin rows.length → F b) (hQ : 0 < Q) : + let ℓ := branchPrecision (Fintype.card V) + let J := sparseParityJetOrder k R Q #(univ : Finset (Fin rows.length)) ℓ + (numPassing φ.violations rows : ℤ) = + ∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := Q)) hQ + (sparseParityJetOrder_pos k R Q #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + clearedParityJetTable (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) (commonDenom Q R : ℤ) k ℓ J + (designReplacementScaledIntMap (D b) (emb b)) (nodeInt t) j s) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) := by + rw [← CNF.commonZeroCount_parityRowSystem] + exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_clearedParityJetTable_design hk rows S e + scope D emb hQ + +end CNFDeterminantRecovery + +/-- Helper: any `Feasible β n b w M` instance implies `0 < numNodes n`. -/ +theorem _root_.Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.numNodes_pos + {β n b w M : ℕ} (hF : Feasible β n b w M) : + 0 < numNodes n := by + have hR := hF.thirtyTwo_le_rowBound + have hQ := hF.six_mul_rowBound_le_numNodes + omega + +/-- **Unified Section 6.3 schedule feasibility, Hermite–Cramer & `clearedParityJetTable` recovery, +degree bound, and `2 ^ (A * interpolationScale n)` examination bound for `CNF.parityRowSystem` +([OpenAI2026ETH], §§5.4–5.5, 6.3, and Appendix B.2–B.3, printed pp. 38–43, 48–50):** +For any `k C_B β_B : ℕ`, at the threshold `N₁ ≥ 16384` of +`CNF.exists_branch_schedule_recovery_and_examBound_parityRowSystem_of_le_clog_pow k C_B β_B`, +whenever `∀ c ∈ φ, c.length ≤ k`, `N₁ ≤ Fintype.card V`, `φ.length ≤ B * Fintype.card V`, +`B ≤ C_B * Nat.clog 2 (Fintype.card V) ^ β_B`, `W ≤ CNF.initialRowWeightBound B φ.length`, +`∀ r ∈ rows, weight r ≤ W`, and `rows.length ≤ 6 * Fintype.card V`, at +`b₀ = CNF.parityBranchThreshold k W (Fintype.card V)` and `β = 2 * β_B + 5`, for any +free-variable equivalence `e : ↥(univ \ S) ≃ Fin n'`, there exist `hQ : 0 < numNodes n'`, +per-branch feasibility proofs `hF b`, and concrete `ReplacementDesign`s `D b` such that at shared +precision `ℓ = branchPrecision (Fintype.card V)` and canonical jet order +`J = sparseParityJetOrder k (rowBound (2 * β_B + 5) n') (numNodes n')` +`#(univ : Finset (Fin rows.length)) ℓ`: +1. `(commonZeroCount univ (φ.parityRowSystem rows) : ℤ)` equals the branch-summed Hermite–Cramer + truncated-sum determinant residue at `nodeInt` and jet order `J`. +2. `(commonZeroCount univ (φ.parityRowSystem rows) : ℤ)` ALSO equals the branch-summed + Stage-1/Stage-2 `clearedParityJetTable` coordinate Hermite–Cramer residue over `s : Fin ℓ` at + `nodeInt` and jet order `J` (Appendix B.2–B.3, eq. `(B.1)`). +3. Every branch polynomial has + `natDegree ≤ (k * (rowBound (2 * β_B + 5) n' - 1)) * (8 * Fintype.card V)`. +4. Every branch `b : V → Bool` has domain-examination count at most + `(2 : ℝ) ^ ((CNF.parityBranchExamScaleCoeff k β_B : ℝ) * interpolationScale (Fintype.card V))`, + and any per-branch examination family bounded by that quantity sums across `branchAssignments S` + to at most `(2 : ℝ) ^ (((CNF.parityBranchExamScaleCoeff k β_B + 32 : ℕ) : ℝ) *` + `interpolationScale (Fintype.card V))`. -/ +theorem CNF.exists_branch_schedule_hermiteCramer_and_examBound_parityRowSystem_of_le_clog_pow + (k C_B β_B : ℕ) : + ∃ N₁ : ℕ, 16384 ≤ N₁ ∧ + ∀ {V : Type*} [Fintype V] [DecidableEq V] + {φ : CNF V} ⦃n' B W : ℕ⦄, + (∀ c ∈ φ, c.length ≤ k) → + N₁ ≤ Fintype.card V → + φ.length ≤ B * Fintype.card V → + B ≤ C_B * Nat.clog 2 (Fintype.card V) ^ β_B → + W ≤ CNF.initialRowWeightBound B φ.length → + ∀ {rows : List (Fin φ.length → Bool)}, + (∀ r ∈ rows, weight r ≤ W) → + rows.length ≤ 6 * Fintype.card V → + let b₀ := CNF.parityBranchThreshold k W (Fintype.card V) + let S := heavyVars univ (univ : Finset (Fin rows.length)) + (fun j => equationScope (φ.parityRowSystem rows j)) b₀ + ∀ (e : ↥(univ \ S) ≃ Fin n'), + (Fintype.card V ≤ 2 * n' ∧ n' ≤ Fintype.card V) ∧ + (∃ (hQ : 0 < numNodes n') + (hF : ∀ b : V → Bool, + Feasible (2 * β_B + 5) n' (b₀ + 1) (max (k * (W * 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 (2 * β_B + 5) n') + (rowBound (2 * β_B + 5) n') (tauRat n')), + let ℓ := branchPrecision (Fintype.card V) + let J := sparseParityJetOrder k (rowBound (2 * β_B + 5) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ + (commonZeroCount (univ : Finset (Fin rows.length)) (φ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos k (rowBound (2 * β_B + 5) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)))).coeff j) / + (clearedProductDenom + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (commonZeroCount (univ : Finset (Fin rows.length)) (φ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos k (rowBound (2 * β_B + 5) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + clearedParityJetTable (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ J + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)) (nodeInt t) j s) / + (clearedProductDenom + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (∀ b : V → Bool, + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩))).natDegree ≤ + (k * (rowBound (2 * β_B + 5) 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 := (d * rowBound (2 * β_B + 5) 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 ∧ p.2 ⊆ p.1} : ℝ) * + (2 * (#(C.measurementBox t) : ℝ) * + ∑ g : Fin (numGroups n'), (Fintype.card (C.LocalCube t g) : ℝ))) ≤ + (2 : ℝ) ^ ((CNF.parityBranchExamScaleCoeff k β_B : ℝ) * + interpolationScale (Fintype.card V))) ∧ + ∀ (examSum : (V → Bool) → ℝ), + (∀ b ∈ branchAssignments S, + examSum b ≤ + (2 : ℝ) ^ ((CNF.parityBranchExamScaleCoeff k β_B : ℝ) * + interpolationScale (Fintype.card V))) → + (∑ b ∈ branchAssignments S, examSum b) ≤ + (2 : ℝ) ^ (((CNF.parityBranchExamScaleCoeff k β_B + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V)) := by + obtain ⟨N₁, hN₁, hrec⟩ := + CNF.exists_branch_schedule_recovery_and_examBound_parityRowSystem_of_le_clog_pow k C_B β_B + refine ⟨N₁, hN₁, fun {V _ _ φ n' B W} hk hcard hm hB hW_bound {rows} hW hlen => ?_⟩ + intro b₀ S e + obtain ⟨hn_bounds, ⟨hF, D, _, hdeg, hexam⟩, hsum⟩ := + hrec hk hcard hm hB hW_bound hW hlen e + have hQ : 0 < numNodes n' := (hF (fun _ => false)).numNodes_pos + refine ⟨hn_bounds, ⟨hQ, hF, D, ?_, ?_, hdeg, hexam⟩, hsum⟩ + · exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_hermiteCramerNumerator_design hk rows + S e (fun b => branchAugmentedScope S e univ (φ.parityRowSystem rows) b) D + (fun _ j => Sum.inl ⟨j, mem_univ j⟩) hQ + · exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_clearedParityJetTable_design hk rows + S e (fun b => branchAugmentedScope S e univ (φ.parityRowSystem rows) b) D + (fun _ j => Sum.inl ⟨j, mem_univ j⟩) hQ + +/-- **Unified Lemma 6.1 + Lemma 6.2 + Section 6.3 greedy parity-test schedule with +Hermite–Cramer & `clearedParityJetTable` recovery and `2 ^ (A * interpolationScale n)` bounds:** +At every stage `i ≤ 3 * Fintype.card V`, the greedy trajectory `A i` admits per-branch `hF b` and +`D b` recovering `commonZeroCount univ (φ.parityRowSystem (A i))` (and `φ.modelCountOn Finset.univ` +at stage `3 * Fintype.card V`) via **both** explicit Hermite–Cramer truncated-sum determinants and +Stage-1/Stage-2 `clearedParityJetTable` coordinate sums at `nodeInt` and canonical jet order +`sparseParityJetOrder`, with single-branch and branch-summed `interpolationScale` examination +bounds. -/ +theorem CNF.exists_greedy_parityRowSystem_hermiteCramer_recovery_and_examBound_of_le_clog_pow + (k C_B β_B : ℕ) : + ∃ N₁ : ℕ, 16384 ≤ N₁ ∧ + ∀ {V : Type*} [Fintype V] [DecidableEq V] + (φ : CNF V) {B : ℕ}, + (∀ c ∈ φ, c.length ≤ k) → + N₁ ≤ Fintype.card V → + 1 ≤ B → + B ≤ C_B * Nat.clog 2 (Fintype.card V) ^ β_B → + φ.length ≤ B * Fintype.card V → + let D₀ := CNF.initialRowWeightBound B φ.length + let P := CNF.greedyRowListLength B φ.length + let b₀ := CNF.parityBranchThreshold k D₀ (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 (A (3 * Fintype.card V))) = + φ.modelCountOn Finset.univ ∧ + ∀ i ≤ 3 * Fintype.card V, + (A i).length ≤ 6 * Fintype.card V ∧ + let S := heavyVars univ (univ : Finset (Fin (A i).length)) + (fun j => equationScope (φ.parityRowSystem (A i) j)) b₀ + ∀ ⦃n' : ℕ⦄ (e : ↥(univ \ S) ≃ Fin n'), + (Fintype.card V ≤ 2 * n' ∧ n' ≤ Fintype.card V) ∧ + (∃ (hQ : 0 < numNodes n') + (hF : ∀ b : V → Bool, + Feasible (2 * β_B + 5) n' (b₀ + 1) (max (k * (D₀ * 2 ^ k)) 1) + (∑ f : {j : Fin (A i).length // + j ∈ (univ : Finset (Fin (A i).length))} ⊕ Fin n', + #(branchAugmentedScope S e univ (φ.parityRowSystem (A i)) b f))) + (D : ∀ b : V → Bool, + ReplacementDesign + (branchAugmentedScope S e univ (φ.parityRowSystem (A i)) b) + (numNodes n') (numGroups n') (intervalStart (2 * β_B + 5) n') + (rowBound (2 * β_B + 5) n') (tauRat n')), + let ℓ := branchPrecision (Fintype.card V) + let J := sparseParityJetOrder k (rowBound (2 * β_B + 5) n') (numNodes n') + #(univ : Finset (Fin (A i).length)) ℓ + (commonZeroCount (univ : Finset (Fin (A i).length)) + (φ.parityRowSystem (A i)) : ℤ) = + (∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos k (rowBound (2 * β_B + 5) n') (numNodes n') + #(univ : Finset (Fin (A i).length)) ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum + (univ : Finset (Fin (A i).length)) + (φ.branchParityRowSystem (A i) S e b) + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)))).coeff j) / + (clearedProductDenom + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + #(univ : Finset (Fin (A i).length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (commonZeroCount (univ : Finset (Fin (A i).length)) + (φ.parityRowSystem (A i)) : ℤ) = + (∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos k (rowBound (2 * β_B + 5) n') (numNodes n') + #(univ : Finset (Fin (A i).length)) ℓ) + (fun t j => + clearedParityJetTable (univ : Finset (Fin (A i).length)) + (φ.branchParityRowSystem (A i) S e b) + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ J + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)) (nodeInt t) j s) / + (clearedProductDenom + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + #(univ : Finset (Fin (A i).length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (∀ b : V → Bool, + (univariateClearedParityTruncatedSum (univ : Finset (Fin (A i).length)) + (φ.branchParityRowSystem (A i) S e b) + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩))).natDegree ≤ + (k * (rowBound (2 * β_B + 5) n' - 1)) * (8 * Fintype.card V)) ∧ + ∀ (b : V → Bool) + (s_active : Finset + ({j : Fin (A i).length // + j ∈ (univ : Finset (Fin (A i).length))} ⊕ Fin n')), + let d := k * ((A i).length + 2 * (branchPrecision (Fintype.card V) - 1)) + let q := (d * rowBound (2 * β_B + 5) 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 ∧ p.2 ⊆ p.1} : ℝ) * + (2 * (#(C.measurementBox t) : ℝ) * + ∑ g : Fin (numGroups n'), (Fintype.card (C.LocalCube t g) : ℝ))) ≤ + (2 : ℝ) ^ ((CNF.parityBranchExamScaleCoeff k β_B : ℝ) * + interpolationScale (Fintype.card V))) ∧ + ∀ (examSum : (V → Bool) → ℝ), + (∀ b ∈ branchAssignments S, + examSum b ≤ + (2 : ℝ) ^ ((CNF.parityBranchExamScaleCoeff k β_B : ℝ) * + interpolationScale (Fintype.card V))) → + (∑ b ∈ branchAssignments S, examSum b) ≤ + (2 : ℝ) ^ (((CNF.parityBranchExamScaleCoeff k β_B + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V)) := by + obtain ⟨N₁, hN₁, hgreedy⟩ := + CNF.exists_greedy_parityRowSystem_recovery_and_examBound_of_le_clog_pow k C_B β_B + refine ⟨N₁, hN₁, fun {V _ _} φ {B} hk hcard hB1 hB_le hm => ?_⟩ + intro D₀ P b₀ + obtain ⟨A₀, hlen0, hw0, htraj⟩ := hgreedy φ hk hcard hB1 hB_le hm + refine ⟨A₀, hlen0, hw0, fun A γ h0 hA hγ => ?_⟩ + obtain ⟨hcount, hstage⟩ := htraj A γ h0 hA hγ + refine ⟨hcount, fun i hi => ?_⟩ + obtain ⟨hlen_i, hstage_e⟩ := hstage i hi + refine ⟨hlen_i, fun ⦃n'⦄ e => ?_⟩ + obtain ⟨hn_bounds, ⟨hF, D, _, hdeg, hexam⟩, hsum⟩ := hstage_e e + have hQ : 0 < numNodes n' := (hF (fun _ => false)).numNodes_pos + refine ⟨hn_bounds, ⟨hQ, hF, D, ?_, ?_, hdeg, hexam⟩, hsum⟩ + · exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_hermiteCramerNumerator_design hk (A i) + _ e (fun b => branchAugmentedScope _ e univ (φ.parityRowSystem (A i)) b) D + (fun _ j => Sum.inl ⟨j, mem_univ j⟩) hQ + · exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_clearedParityJetTable_design hk (A i) + _ e (fun b => branchAugmentedScope _ e univ (φ.parityRowSystem (A i)) b) D + (fun _ j => Sum.inl ⟨j, mem_univ j⟩) hQ + +/-- **Unconditional Section 6.3 parity-row system existence, Hermite–Cramer & +`clearedParityJetTable` recovery of `φ.modelCountOn Finset.univ`, degree bound, and +`2 ^ (A * interpolationScale n)` examination bound:** +For any `k C_B β_B : ℕ`, at `N₁ ≥ 16384`, for any width-`≤ k` CNF `φ : CNF V` with +`N₁ ≤ Fintype.card V`, `1 ≤ B`, `B ≤ C_B * Nat.clog 2 (Fintype.card V) ^ β_B`, and +`φ.length ≤ B * Fintype.card V` (including `φ = []`), there exists a parity-row list +`rows : List (Fin φ.length → Bool)` (`rows.length ≤ 6 * Fintype.card V`) such that +`commonZeroCount univ (φ.parityRowSystem rows) = φ.modelCountOn Finset.univ`, and for any +free-variable equivalence `e : ↥(univ \ S) ≃ Fin n'`, there exist `hQ : 0 < numNodes n'`, +per-branch `hF b`, and concrete `ReplacementDesign`s `D b` recovering +`(φ.modelCountOn Finset.univ : ℤ)` via **both** explicit Hermite–Cramer truncated-sum determinants +and Stage-1/Stage-2 `clearedParityJetTable` coordinate sums at `nodeInt` and canonical jet order +`sparseParityJetOrder`, with single-branch and branch-summed `interpolationScale` examination +bounds. -/ +theorem CNF.exists_parityRowSystem_modelCountOn_hermiteCramer_recovery_and_examBound_of_le_clog_pow + (k C_B β_B : ℕ) : + ∃ N₁ : ℕ, 16384 ≤ N₁ ∧ + ∀ {V : Type*} [Fintype V] [DecidableEq V] + (φ : CNF V) {B : ℕ}, + (∀ c ∈ φ, c.length ≤ k) → + N₁ ≤ Fintype.card V → + 1 ≤ B → + B ≤ C_B * Nat.clog 2 (Fintype.card V) ^ β_B → + φ.length ≤ B * Fintype.card V → + let D₀ := CNF.initialRowWeightBound B φ.length + let b₀ := CNF.parityBranchThreshold k D₀ (Fintype.card V) + ∃ rows : List (Fin φ.length → Bool), + rows.length ≤ 6 * Fintype.card V ∧ + commonZeroCount univ (φ.parityRowSystem rows) = φ.modelCountOn Finset.univ ∧ + 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) ∧ + (∃ (hQ : 0 < numNodes n') + (hF : ∀ b : V → Bool, + Feasible (2 * β_B + 5) 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 (2 * β_B + 5) n') + (rowBound (2 * β_B + 5) n') (tauRat n')), + let ℓ := branchPrecision (Fintype.card V) + let J := sparseParityJetOrder k (rowBound (2 * β_B + 5) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ + (φ.modelCountOn Finset.univ : ℤ) = + (∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos k (rowBound (2 * β_B + 5) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)))).coeff j) / + (clearedProductDenom + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (φ.modelCountOn Finset.univ : ℤ) = + (∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos k (rowBound (2 * β_B + 5) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + clearedParityJetTable (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ J + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)) (nodeInt t) j s) / + (clearedProductDenom + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (∀ b : V → Bool, + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') (rowBound (2 * β_B + 5) n') : ℤ) k ℓ + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩))).natDegree ≤ + (k * (rowBound (2 * β_B + 5) 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 := (d * rowBound (2 * β_B + 5) 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 ∧ p.2 ⊆ p.1} : ℝ) * + (2 * (#(C.measurementBox t) : ℝ) * + ∑ g : Fin (numGroups n'), (Fintype.card (C.LocalCube t g) : ℝ))) ≤ + (2 : ℝ) ^ ((CNF.parityBranchExamScaleCoeff k β_B : ℝ) * + interpolationScale (Fintype.card V))) ∧ + ∀ (examSum : (V → Bool) → ℝ), + (∀ b ∈ branchAssignments S, + examSum b ≤ + (2 : ℝ) ^ ((CNF.parityBranchExamScaleCoeff k β_B : ℝ) * + interpolationScale (Fintype.card V))) → + (∑ b ∈ branchAssignments S, examSum b) ≤ + (2 : ℝ) ^ (((CNF.parityBranchExamScaleCoeff k β_B + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card V)) := by + obtain ⟨N₁, hN₁, hmodel⟩ := + CNF.exists_parityRowSystem_modelCountOn_recovery_and_examBound_of_le_clog_pow k C_B β_B + refine ⟨N₁, hN₁, fun {V _ _} φ {B} hk hcard hB1 hB_le hm => ?_⟩ + intro D₀ b₀ + obtain ⟨rows, hlen, hcount, hstage⟩ := hmodel φ hk hcard hB1 hB_le hm + refine ⟨rows, hlen, hcount, fun ⦃n'⦄ e => ?_⟩ + obtain ⟨hn_bounds, ⟨hF, D, _, hdeg, hexam⟩, hsum⟩ := hstage e + have hQ : 0 < numNodes n' := (hF (fun _ => false)).numNodes_pos + refine ⟨hn_bounds, ⟨hQ, hF, D, ?_, ?_, hdeg, hexam⟩, hsum⟩ + · rw [← hcount] + exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_hermiteCramerNumerator_design hk rows + _ e (fun b => branchAugmentedScope _ e univ (φ.parityRowSystem rows) b) D + (fun _ j => Sum.inl ⟨j, mem_univ j⟩) hQ + · rw [← hcount] + exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_clearedParityJetTable_design hk rows + _ e (fun b => branchAugmentedScope _ e univ (φ.parityRowSystem rows) b) D + (fun _ j => Sum.inl ⟨j, mem_univ j⟩) hQ + +/-! ### 3. Proposition 6.4 tree-wide Hermite–Cramer & `clearedParityJetTable` recovery -/ + +/-- **Proposition 6.4 tree-wide candidate-indexed Hermite–Cramer & `clearedParityJetTable` +recovery and total `2 ^ (O_k(interpolationScale n))` examination bounds ([OpenAI2026ETH], +§§5.4–5.5, 6.1–6.4, and Appendices A–B, printed pp. 38–50):** +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. **Exact leaf-summed model-count conservation and `2 ^ (17 * interpolationScale n)` leaf-count + bound:** + `((φ.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)`, + and `((φ.prop64NormalizedLeaves k).length : ℝ) ≤` + `(2 : ℝ) ^ (17 * interpolationScale (Fintype.card V))`. +2. **Per-leaf candidate-query cardinality and overhead bound:** + For every leaf `L ∈ φ.prop64NormalizedLeaves k` (`ψ := L.toCNF`), + `Fintype.card (CNF.LeafCandidateQueryIndex V B ψ) = 3 * Fintype.card V * (2 * ψ.length) ^ P + 1` + `≤ CNF.leafCandidateQueryBound B ψ`, and + `(CNF.leafCandidateQueryBound B ψ : ℝ) ≤ (2 : ℝ) ^ interpolationScale (Fintype.card V)`. +3. **Every candidate query and final query certified via explicit Hermite–Cramer determinants, + Stage-1/Stage-2 `clearedParityJetTable` coordinate sums, and `interpolationScale` examination + bounds:** + There exist Lemma 6.1 initial rows `A₀` such that for any Lemma 6.2 greedy trajectory `A`: + - `commonZeroCount univ (ψ.parityRowSystem (A (3 * Fintype.card V))) = ψ.modelCountOn univ`, + - for **every** query `q : CNF.LeafCandidateQueryIndex V B ψ` (every candidate `(i, γ')` across + `i < 3 * n` and ordered candidate list `γ'` with list multiplicity, including discarded + candidates, plus the final query `Sum.inr ()`), and any free-variable equivalence + `e : ↥(univ \ S_q) ≃ Fin n'`, there exist `hQ : 0 < numNodes n'`, per-branch `hF b`, and + concrete `ReplacementDesign`s `D b` at schedule exponent `β = CNF.prop64ScheduleExponent k` + recovering `commonZeroCount univ (ψ.parityRowSystem (CNF.candidateQueryRows A q))` via **both** + explicit Hermite–Cramer truncated-sum determinants and Stage-1/Stage-2 `clearedParityJetTable` + coordinate sums at `nodeInt` and canonical jet order `sparseParityJetOrder`, with single-query + branch-summed examination count at most + `(2 : ℝ) ^ (((CNF.prop64BranchExamScaleCoeff k + 32 : ℕ) : ℝ) * interpolationScale n)` and + candidate-summed leaf examination count `∑ q, queryExam q` at most + `(2 : ℝ) ^ ((CNF.prop64LeafQueryExamScaleCoeff k : ℝ) * interpolationScale n)`. +4. **Tree-wide single-query and total candidate-indexed examination bounds:** + Summing across `φ.prop64NormalizedLeaves k` bounds the tree-wide single-query 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))`. -/ +theorem CNF.exists_prop64NormalizedLeaves_greedy_total_hermiteCramer_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 ∧ + Fintype.card (CNF.LeafCandidateQueryIndex V B ψ) = + 3 * Fintype.card V * (2 * ψ.length) ^ P + 1 ∧ + Fintype.card (CNF.LeafCandidateQueryIndex V B ψ) ≤ + CNF.leafCandidateQueryBound B ψ ∧ + (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 (A (3 * Fintype.card V))) = + ψ.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) ∧ + (∃ (hQ : 0 < numNodes n') + (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')), + let ℓ := branchPrecision (Fintype.card V) + let J := sparseParityJetOrder k (rowBound (CNF.prop64ScheduleExponent k) n') + (numNodes n') #(univ : Finset (Fin rows.length)) ℓ + (commonZeroCount (univ : Finset (Fin rows.length)) + (ψ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos k + (rowBound (CNF.prop64ScheduleExponent k) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum + (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k ℓ + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)))).coeff j) / + (clearedProductDenom + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (commonZeroCount (univ : Finset (Fin rows.length)) + (ψ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos k + (rowBound (CNF.prop64ScheduleExponent k) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + clearedParityJetTable (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k ℓ J + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)) (nodeInt t) j s) / + (clearedProductDenom + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (∀ b : V → Bool, + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k ℓ + (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_jet := (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_jet ∧ 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 ⟨N₃, hN₃, hprop64⟩ := + CNF.exists_prop64NormalizedLeaves_greedy_total_recovery_and_examBound hk + refine ⟨N₃, hN₃, fun {V _ _} φ hk_φ hcard => ?_⟩ + intro B + obtain ⟨hsum_mc, hs2, hlen_pow, hlen_scale, hleaf, htree_branch, htree_total⟩ := + hprop64 φ hk_φ hcard + refine ⟨hsum_mc, hs2, hlen_pow, hlen_scale, fun L hL => ?_, htree_branch, htree_total⟩ + intro ψ D₀ P b₀ + obtain ⟨hk_ψ, hm_ψ, hcand_scale, A₀, hlen0, hw0, htraj⟩ := hleaf L hL + refine ⟨hk_ψ, hm_ψ, CNF.card_leafCandidateQueryIndex_eq B ψ, + CNF.card_leafCandidateQueryIndex_le B ψ, hcand_scale, A₀, hlen0, hw0, + fun A γ h0 hA hmin => ?_⟩ + obtain ⟨hcount, hquery, hleaf_sum⟩ := htraj A γ h0 hA hmin + refine ⟨hcount, fun q => ?_, hleaf_sum⟩ + obtain ⟨hlen_q, hw_q, hstage_q⟩ := hquery q + refine ⟨hlen_q, hw_q, fun ⦃n'⦄ e => ?_⟩ + obtain ⟨hn_bounds, ⟨hF, D, _, hdeg, hexam⟩, hsum⟩ := hstage_q e + have hQ : 0 < numNodes n' := (hF (fun _ => false)).numNodes_pos + refine ⟨hn_bounds, ⟨hQ, hF, D, ?_, ?_, hdeg, hexam⟩, hsum⟩ + · exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_hermiteCramerNumerator_design hk_ψ + (CNF.candidateQueryRows A q) _ e + (fun b => branchAugmentedScope _ e univ (ψ.parityRowSystem (CNF.candidateQueryRows A q)) b) D + (fun _ j => Sum.inl ⟨j, mem_univ j⟩) hQ + · exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_clearedParityJetTable_design hk_ψ + (CNF.candidateQueryRows A q) _ e + (fun b => branchAugmentedScope _ e univ (ψ.parityRowSystem (CNF.candidateQueryRows A q)) b) D + (fun _ j => Sum.inl ⟨j, mem_univ j⟩) hQ + +/-- **Proposition 6.4 unconditional trajectory-instantiated tree-wide Hermite–Cramer & +`clearedParityJetTable` recovery and total candidate-indexed `2 ^ (O_k(interpolationScale n))` +examination bounds ([OpenAI2026ETH], §6.4 & Appendices A–B, printed pp. 43–50):** +For any `k ≥ 2`, at `N₃ ≥ 2 ^ 640000`, for any finite variable type `V` with `N₃ ≤ Fintype.card V` +and any width-`≤ k` CNF `φ : CNF V`, every leaf `L ∈ φ.prop64NormalizedLeaves k` (`ψ := L.toCNF`) +unconditionally admits a concrete Lemma 6.2 greedy trajectory `A : ℕ → List (Fin ψ.length → Bool)` +such that +`commonZeroCount univ (ψ.parityRowSystem (CNF.candidateQueryRows (B := B) A (Sum.inr ()))) =` +`ψ.modelCountOn Finset.univ`, every round satisfies the Lemma 6.2 minimality inequality, and +every candidate query `q : CNF.LeafCandidateQueryIndex V B ψ` (including discarded candidates with +list multiplicity and the final query `Sum.inr ()`) is recovered via **both** explicit +Hermite–Cramer truncated-sum determinants and Stage-1/Stage-2 `clearedParityJetTable` coordinate +sums at `nodeInt` and canonical jet order `sparseParityJetOrder`, with per-query, per-leaf +candidate-summed, and tree-wide candidate-summed `interpolationScale` examination bounds. -/ +theorem CNF.exists_prop64NormalizedLeaves_total_hermiteCramer_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 ∧ + Fintype.card (CNF.LeafCandidateQueryIndex V B ψ) = + 3 * Fintype.card V * (2 * ψ.length) ^ P + 1 ∧ + Fintype.card (CNF.LeafCandidateQueryIndex V B ψ) ≤ + CNF.leafCandidateQueryBound B ψ ∧ + (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) ∧ + (∃ (hQ : 0 < numNodes n') + (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')), + let ℓ := branchPrecision (Fintype.card V) + let J := sparseParityJetOrder k (rowBound (CNF.prop64ScheduleExponent k) n') + (numNodes n') #(univ : Finset (Fin rows.length)) ℓ + (commonZeroCount (univ : Finset (Fin rows.length)) + (ψ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos k + (rowBound (CNF.prop64ScheduleExponent k) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum + (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k ℓ + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)))).coeff j) / + (clearedProductDenom + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (commonZeroCount (univ : Finset (Fin rows.length)) + (ψ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos k + (rowBound (CNF.prop64ScheduleExponent k) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + clearedParityJetTable (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k ℓ J + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)) (nodeInt t) j s) / + (clearedProductDenom + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (∀ b : V → Bool, + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent k) n') : ℤ) k ℓ + (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_jet := (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_jet ∧ 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 ⟨N₃, hN₃, htotal⟩ := + CNF.exists_prop64NormalizedLeaves_total_recovery_and_examBound hk + refine ⟨N₃, hN₃, fun {V _ _} φ hk_φ hcard => ?_⟩ + intro B + obtain ⟨hsum_mc, hs2, hlen_pow, hlen_scale, hleaf, htree_branch, htree_total⟩ := + htotal φ hk_φ hcard + refine ⟨hsum_mc, hs2, hlen_pow, hlen_scale, fun L hL => ?_, htree_branch, htree_total⟩ + intro ψ D₀ P b₀ + obtain ⟨hk_ψ, hm_ψ, hcand_scale, A, hcount, hmin, hquery, hleaf_sum⟩ := hleaf L hL + refine ⟨hk_ψ, hm_ψ, CNF.card_leafCandidateQueryIndex_eq B ψ, + CNF.card_leafCandidateQueryIndex_le B ψ, hcand_scale, A, hcount, hmin, + fun q => ?_, hleaf_sum⟩ + obtain ⟨hlen_q, hw_q, hstage_q⟩ := hquery q + refine ⟨hlen_q, hw_q, fun ⦃n'⦄ e => ?_⟩ + obtain ⟨hn_bounds, ⟨hF, D, _, hdeg, hexam⟩, hsum⟩ := hstage_q e + have hQ : 0 < numNodes n' := (hF (fun _ => false)).numNodes_pos + refine ⟨hn_bounds, ⟨hQ, hF, D, ?_, ?_, hdeg, hexam⟩, hsum⟩ + · exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_hermiteCramerNumerator_design hk_ψ + (CNF.candidateQueryRows A q) _ e + (fun b => branchAugmentedScope _ e univ (ψ.parityRowSystem (CNF.candidateQueryRows A q)) b) D + (fun _ j => Sum.inl ⟨j, mem_univ j⟩) hQ + · exact CNF.commonZeroCount_parityRowSystem_eq_sum_branch_clearedParityJetTable_design hk_ψ + (CNF.candidateQueryRows A q) _ e + (fun b => branchAugmentedScope _ e univ (ψ.parityRowSystem (CNF.candidateQueryRows A q)) b) D + (fun _ j => Sum.inl ⟨j, mem_univ j⟩) hQ + +end Cslib.Logic.PL diff --git a/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean b/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean new file mode 100644 index 000000000..c591c2a67 --- /dev/null +++ b/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean @@ -0,0 +1,409 @@ +/- +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.GeneralCNFHermiteRecovery + +/-! +# Tests for `Complexity.Computability.Complexity.FineGrained.GeneralCNFHermiteRecovery` + +Exercises the Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer coordinate recovery +(`hermiteCramerNumerator_clearedParityJetTable_eq_mul`, +`emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount`), +`Feasible.numNodes_pos`, the Section 6.3 compiled CNF parity-row schedule Hermite–Cramer and +`clearedParityJetTable` recovery +(`CNF.exists_parityRowSystem_modelCountOn_hermiteCramer_recovery_and_examBound_of_le_clog_pow`), +and the Proposition 6.4 tree-wide candidate-indexed Hermite–Cramer and `clearedParityJetTable` +recovery and actual `toCountingDesign` examination bounds +(`CNF.exists_prop64NormalizedLeaves_total_hermiteCramer_recovery_and_examBound`) on concrete +systems and 3-CNF formulas. +-/ + +public noncomputable section + +namespace CslibTests + +open Finset Polynomial +open Cslib +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 +open scoped BigOperators + +/-- Concrete linear parity system `x₀ + x₁ = 0` on `Fin 2` (`1` equation with monomials `{0}` and +`{1}`), which has `commonZeroCount univ sampleParitySystem2 = 2`. -/ +def sampleParitySystem2 : Fin 1 → Finset (Finset (Fin 2)) := + fun _ => {{0}, {1}} + +theorem commonZeroCount_sampleParitySystem2 : + commonZeroCount (univ : Finset (Fin 1)) sampleParitySystem2 = 2 := by + decide + +/-- Concrete check of `hermiteCramerNumerator_clearedParityJetTable_eq_mul` and +`emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount` on +`sampleParitySystem2` (`commonZeroCount = 2`) with constant replacement map +`θ x i v = Polynomial.C (bitVal ℤ (x v))` (`d_den = 1`, `R_deg = 0`), single interpolation node +`nodes 0 = 0` (`Q = 1`), jet order `J = 1`, and precision `ℓ = 3`: the Stage-1/Stage-2 +`clearedParityJetTable` coordinate Cramer quotients sum modulo `2 ^ 3 = 8` to the exact common-zero +count `2`. -/ +theorem clearedParityJetTable_hermiteCramer_recovers_sampleParitySystem2 : + let I : Finset (Fin 1) := univ + let θ : (Fin 2 → Bool) → Fin 1 → Fin 2 → Polynomial ℤ := + fun x _ v => Polynomial.C (bitVal ℤ (x v)) + let nodes : Fin 1 → ℤ := fun _ => 0 + (∀ s : Fin 3, + hermiteCramerNumerator nodes Nat.one_pos Nat.one_pos + (fun t j => + clearedParityJetTable I sampleParitySystem2 1 1 3 1 θ (nodes t) j s) = + (Polynomial.hermiteMatrix nodes 1).det * + (univariateClearedParityCoord I sampleParitySystem2 1 1 3 θ s.1).eval 0) ∧ + (∑ s : Fin 3, + hermiteCramerNumerator nodes Nat.one_pos Nat.one_pos + (fun t j => + clearedParityJetTable I sampleParitySystem2 1 1 3 1 θ (nodes t) j s) / + (clearedProductDenom 1 1 3 #I * + (Polynomial.hermiteMatrix nodes 1).det)) % ((2 : ℤ) ^ 3) = 2 := by + intro I θ nodes + have hk : ∀ i ∈ I, ∀ M ∈ sampleParitySystem2 i, #M ≤ 1 := by decide + have hdeg : ∀ x : Fin 2 → Bool, ∀ i ∈ I, ∀ M ∈ sampleParitySystem2 i, ∀ v ∈ M, + (θ x i v).natDegree ≤ 0 := by + intro x _ _ _ _ v _ + exact (Polynomial.natDegree_C (bitVal ℤ (x v))).le + have hθ : ∀ x : Fin 2 → Bool, ∀ i ∈ I, ∀ M ∈ sampleParitySystem2 i, ∀ v ∈ M, + (θ x i v).eval 0 = 1 * bitVal ℤ (x v) := by + intro x _ _ _ _ v _ + simp [θ] + have hQJ : (1 * 0) * (#I + 2 * (3 - 1)) < 1 * 1 := by decide + have hnodes : Function.Injective nodes := fun a b _ => Subsingleton.elim a b + have hℓ : Fintype.card (Fin 2) < 3 := by decide + refine ⟨fun s => + hermiteCramerNumerator_clearedParityJetTable_eq_mul I sampleParitySystem2 1 nodes + Nat.one_pos Nat.one_pos θ hk hdeg hQJ s, ?_⟩ + rw [emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount + I sampleParitySystem2 one_ne_zero hnodes Nat.one_pos Nat.one_pos hℓ θ hk hdeg hθ hQJ, + commonZeroCount_sampleParitySystem2] + rfl + +/-- Concrete 3-CNF on `Fin N` (`1 ≤ N`) with one tautological clause and one width-3 clause. -/ +def sampleHermiteTaut3CNF (N : ℕ) [NeZero N] : CNF (Fin N) := + [[(0, true), (0, false), (0, true)], + [(0, true), (0, true), (0, true)]] + +theorem sampleHermiteTaut3CNF_width_le_three (N : ℕ) [NeZero N] : + ∀ c ∈ sampleHermiteTaut3CNF N, c.length ≤ 3 := by + intro c hc + simp only [sampleHermiteTaut3CNF, List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with rfl | rfl <;> simp + +private theorem pos_of_le {m n : ℕ} (hm : 0 < m) (h : m ≤ n) : 0 < n := + lt_of_lt_of_le hm h + +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 Section 6.3 instantiation of +`CNF.exists_parityRowSystem_modelCountOn_hermiteCramer_recovery_and_examBound_of_le_clog_pow` +at `k = 3`, `C_B = 1`, `β_B = 2` on `sampleHermiteTaut3CNF N₁`, verifying `0 < numNodes n'`, +both the Hermite–Cramer truncated-sum determinant recovery and the Stage-1/Stage-2 +`clearedParityJetTable` coordinate recovery of `(φ.modelCountOn Finset.univ : ℤ)`, and the +branch-summed `interpolationScale` examination bound on the actual `toCountingDesign` sum. -/ +theorem nonvacuous_sec63_modelCountOn_hermiteCramer_and_clearedParityJetTable_recovery_k3 : + ∃ (N₁ : ℕ) (_ : NeZero N₁), 16384 ≤ N₁ ∧ + let φ := sampleHermiteTaut3CNF N₁ + let D₀ := CNF.initialRowWeightBound 1 φ.length + let b₀ := CNF.parityBranchThreshold 3 D₀ (Fintype.card (Fin N₁)) + ∃ rows : List (Fin φ.length → Bool), + rows.length ≤ 6 * Fintype.card (Fin N₁) ∧ + commonZeroCount univ (φ.parityRowSystem rows) = φ.modelCountOn Finset.univ ∧ + 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) + ∃ (hQ : 0 < numNodes n') + (hF : ∀ b : Fin N₁ → Bool, + Feasible 9 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 9 n') + (rowBound 9 n') (tauRat n')), + let ℓ := branchPrecision (Fintype.card (Fin N₁)) + let J := sparseParityJetOrder 3 (rowBound 9 n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ + (φ.modelCountOn Finset.univ : ℤ) = + (∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos 3 (rowBound 9 n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') (rowBound 9 n') : ℤ) 3 ℓ + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)))).coeff j) / + (clearedProductDenom + (commonDenom (numNodes n') (rowBound 9 n') : ℤ) 3 ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (φ.modelCountOn Finset.univ : ℤ) = + (∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos 3 (rowBound 9 n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + clearedParityJetTable (univ : Finset (Fin rows.length)) + (φ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') (rowBound 9 n') : ℤ) 3 ℓ J + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)) (nodeInt t) j s) / + (clearedProductDenom + (commonDenom (numNodes n') (rowBound 9 n') : ℤ) 3 ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (∑ b ∈ branchAssignments S, + let d := 3 * (rows.length + 2 * (branchPrecision (Fintype.card (Fin N₁)) - 1)) + let q_ord := (d * rowBound 9 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) : ℝ))) ≤ + (2 : ℝ) ^ (((CNF.parityBranchExamScaleCoeff 3 2 + 32 : ℕ) : ℝ) * + interpolationScale (Fintype.card (Fin N₁))) := by + obtain ⟨N₁, hN₁, hsec63⟩ := + CNF.exists_parityRowSystem_modelCountOn_hermiteCramer_recovery_and_examBound_of_le_clog_pow + 3 1 2 + have hpos : 0 < N₁ := pos_of_le (by decide : 0 < 16384) hN₁ + have : NeZero N₁ := ⟨Nat.ne_of_gt hpos⟩ + set φ := sampleHermiteTaut3CNF N₁ + have hcard : N₁ ≤ Fintype.card (Fin N₁) := by rw [Fintype.card_fin] + have hB_le : 1 ≤ 1 * Nat.clog 2 (Fintype.card (Fin N₁)) ^ 2 := by + rw [Fintype.card_fin, one_mul] + have hclog : 1 ≤ Nat.clog 2 N₁ := + (Nat.lt_clog_iff_pow_lt one_lt_two).mpr (by omega : 2 ^ 0 < N₁) + exact Nat.one_le_pow 2 _ hclog + have hm : φ.length ≤ 1 * Fintype.card (Fin N₁) := by + rw [Fintype.card_fin, one_mul] + change 2 ≤ N₁ + omega + obtain ⟨rows, hlen, hcount, hstage⟩ := + hsec63 φ (sampleHermiteTaut3CNF_width_le_three N₁) hcard le_rfl hB_le hm + refine ⟨N₁, inferInstance, hN₁, rows, hlen, hcount, ?_⟩ + intro S n' e + obtain ⟨_, ⟨hQ, hF, D, hrec_trunc, hrec_jet, _, hexam⟩, hsum⟩ := hstage e + exact ⟨hQ, hF, D, hrec_trunc, hrec_jet, hsum _ fun b _ => hexam b univ⟩ + +/-- Nonvacuous Proposition 6.4 instantiation of +`CNF.exists_prop64NormalizedLeaves_total_hermiteCramer_recovery_and_examBound` at `k = 3` on +`sampleHermiteTaut3CNF N₃`, certifying for every normalized leaf `L ∈ φ.prop64NormalizedLeaves 3` +and every candidate query `q : CNF.LeafCandidateQueryIndex (Fin N₃) B L.toCNF` (including +discarded candidates with list multiplicity and the final query `Sum.inr ()`) both the +Hermite–Cramer truncated-sum determinant recovery and the Stage-1/Stage-2 `clearedParityJetTable` +coordinate recovery at `nodeInt` and canonical jet order `sparseParityJetOrder`, together with the +per-leaf candidate-summed, tree-wide final-query, and tree-wide total candidate-indexed +`interpolationScale` bounds evaluated on the **actual** `toCountingDesign` examination costs. -/ +theorem nonvacuous_prop64NormalizedLeaves_total_hermiteCramer_and_jetTable_recovery_k3 : + ∃ (N₃ : ℕ) (_ : NeZero N₃), 2 ^ 640000 ≤ N₃ ∧ + let φ := sampleHermiteTaut3CNF N₃ + let B := CNF.prop64LeafClauseRatio 3 (Fintype.card (Fin N₃)) + ((φ.prop64NormalizedLeaves 3).map fun L => L.toCNF.modelCountOn Finset.univ).sum = + φ.modelCountOn Finset.univ ∧ + ((φ.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₃)) + Fintype.card (CNF.LeafCandidateQueryIndex (Fin N₃) B ψ) = + 3 * Fintype.card (Fin N₃) * (2 * ψ.length) ^ P + 1 ∧ + ∃ A : ℕ → List (Fin ψ.length → Bool), + commonZeroCount univ + (ψ.parityRowSystem (CNF.candidateQueryRows (B := B) A (Sum.inr ()))) = + ψ.modelCountOn Finset.univ ∧ + (∀ q : CNF.LeafCandidateQueryIndex (Fin N₃) B ψ, + 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) + ∃ (hQ : 0 < numNodes n') + (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')), + let ℓ := branchPrecision (Fintype.card (Fin N₃)) + let J := sparseParityJetOrder 3 (rowBound (CNF.prop64ScheduleExponent 3) n') + (numNodes n') #(univ : Finset (Fin rows.length)) ℓ + (commonZeroCount (univ : Finset (Fin rows.length)) + (ψ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos 3 + (rowBound (CNF.prop64ScheduleExponent 3) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum + (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent 3) n') : ℤ) 3 ℓ + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)))).coeff j) / + (clearedProductDenom + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent 3) n') : ℤ) 3 ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + (commonZeroCount (univ : Finset (Fin rows.length)) + (ψ.parityRowSystem rows) : ℤ) = + (∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := numNodes n')) hQ + (sparseParityJetOrder_pos 3 + (rowBound (CNF.prop64ScheduleExponent 3) n') (numNodes n') + #(univ : Finset (Fin rows.length)) ℓ) + (fun t j => + clearedParityJetTable (univ : Finset (Fin rows.length)) + (ψ.branchParityRowSystem rows S e b) + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent 3) n') : ℤ) 3 ℓ J + (designReplacementScaledIntMap (D b) + (fun j => Sum.inl ⟨j, mem_univ j⟩)) (nodeInt t) j s) / + (clearedProductDenom + (commonDenom (numNodes n') + (rowBound (CNF.prop64ScheduleExponent 3) n') : ℤ) 3 ℓ + #(univ : Finset (Fin rows.length)) * + (Polynomial.hermiteMatrix (nodeInt (Q := numNodes n')) J).det)) % + ((2 : ℤ) ^ ℓ)) ∧ + actualQueryExam L q = + ∑ b ∈ branchAssignments S, + let d := 3 * (rows.length + 2 * (branchPrecision (Fintype.card (Fin N₃)) - 1)) + let q_jet := (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_jet ∧ 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_hermiteCramer_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 φ := sampleHermiteTaut3CNF N₃ + set B := CNF.prop64LeafClauseRatio 3 (Fintype.card (Fin N₃)) + obtain ⟨hsum, _, _, hlen_scale, hleaf, htree, htotal⟩ := + hprop64 φ (sampleHermiteTaut3CNF_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.2.2.choose + let hA_spec := (hleaf L hL).2.2.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_spec.choose + let D := hpack.choose_spec.choose_spec.choose + ∑ b ∈ branchAssignments S, + let d := 3 * (rows.length + 2 * (branchPrecision (Fintype.card (Fin N₃)) - 1)) + let q_jet := (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_jet ∧ 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.2.2.choose + let hA_spec := (hleaf L hL).2.2.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.choose_spec.2.2.2 + exact hq_e.2.2 _ fun b _ => hexam b univ + refine ⟨N₃, inferInstance, hN₃, hsum, 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 hcard_eq := (hleaf L hL).2.2.1 + let A := (hleaf L hL).2.2.2.2.2.choose + have hA_spec := (hleaf L hL).2.2.2.2.2.choose_spec + refine ⟨hcard_eq, A, hA_spec.1, fun q => ?_, + hA_spec.2.2.2 (actualQueryExam L) (hactual_bound L hL)⟩ + obtain ⟨_, _, hq_all_e⟩ := hA_spec.2.2.1 q + intro rows S n' e + have hpack := (hq_all_e e).2.1 + let hQ := hpack.choose + let hF := hpack.choose_spec.choose + let D := hpack.choose_spec.choose_spec.choose + have hrec_trunc := hpack.choose_spec.choose_spec.choose_spec.1 + have hrec_jet := hpack.choose_spec.choose_spec.choose_spec.2.1 + refine ⟨hQ, hF, D, hrec_trunc, hrec_jet, ?_⟩ + dsimp only [actualQueryExam] + rw [dite_eq_left_of_eq_true (eq_true hL)] + +end CslibTests From 7df4cf1d97d40f2354cb735c70e5aed78aa5e4f1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 05:50:43 -0400 Subject: [PATCH 3/3] refactor(BooleanAnalysis): extract shared Hermite jet recovery Move the five generic Cslib.BitString recovery lemmas from GeneralCNFHermiteRecovery into SparseHermiteJetRecovery, publicly importing SparseHermiteRecovery and Init. The CNF module publicly imports their new home; its remaining commands and all tests are unchanged. Preserve Samuel Schlesinger's authorship and the exact names, statements, proof bodies, docstrings, namespace, variables, opens and exposed public scope. This bounded placement fix is based on independently reviewed PR #1329 head f6e5b348ca6a290e933a2cd63eb948abdd077a17 and addresses review 5664751087. No restack, parent #1322 change or #1309 rename is included. Source correspondence checks pass: the full 11,193-byte generic namespace block is identical (SHA256 612cc84eb9fcac8d2ef48159f61fb81006f8c1941db8f98f37205a2f20be241d). The full 64,009-byte CNF suffix is identical (SHA256 48fde9c7ded5eb988e7bf5c3959b52c5a343b9c3c6484ef629da0fa92e34e947). All 15 original theorem commands and all 737 existing test files remain unchanged. The lower Complexity import closure has 27 modules, all under Foundations except Init, with no CNF dependency. Complexity.lean changes only by the sorted public import of the new shared module. Validation after scripts/cache/ensure.sh: - lake build --wfail --iofail Complexity.Foundations.BooleanAnalysis.SparseHermiteJetRecovery Complexity.Computability.Complexity.FineGrained.GeneralCNFHermiteRecovery ComplexityTests.Computability.Complexity.FineGrained.GeneralCNFHermiteRecovery passed. - lake exe mk_all generated the one new import; --check passed. - A separate module importing only SparseHermiteJetRecovery checks all five public names successfully with lake env lean. - git diff --check and the source-correspondence script passed. Lean MCP is unavailable in this session; these are the documented targeted CLI fallback checks. Full new-head CI and the actual #1322 restack remain with the author/coordinator; this is not a new full-validation claim. Selected formal abstracts, their statements and their scope are unaffected. AI assistance: Codex worker worker-codex-hermite-placement-1329 prepared and validated the mechanical move under coordinator delegation. --- Complexity.lean | 1 + .../GeneralCNFHermiteRecovery.lean | 224 +---------------- .../SparseHermiteJetRecovery.lean | 225 ++++++++++++++++++ 3 files changed, 232 insertions(+), 218 deletions(-) create mode 100644 Complexity/Foundations/BooleanAnalysis/SparseHermiteJetRecovery.lean diff --git a/Complexity.lean b/Complexity.lean index 950c6b133..093de7151 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1822,6 +1822,7 @@ public import Complexity.Foundations.BooleanAnalysis.SignApproximation public import Complexity.Foundations.BooleanAnalysis.SparseBranching public import Complexity.Foundations.BooleanAnalysis.SparseClearedSpecialization public import Complexity.Foundations.BooleanAnalysis.SparseEquations +public import Complexity.Foundations.BooleanAnalysis.SparseHermiteJetRecovery public import Complexity.Foundations.BooleanAnalysis.SparseHermiteRecovery public import Complexity.Foundations.BooleanAnalysis.SparseReplacementDesign public import Complexity.Foundations.BooleanAnalysis.Symmetrization diff --git a/Complexity/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean b/Complexity/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean index 8b63129f2..52c28d39a 100644 --- a/Complexity/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean +++ b/Complexity/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean @@ -9,13 +9,13 @@ module public import Complexity.Init public import Complexity.Computability.Complexity.FineGrained.GeneralCNFCountingAsymptotics -public import Complexity.Foundations.BooleanAnalysis.SparseHermiteRecovery +public import Complexity.Foundations.BooleanAnalysis.SparseHermiteJetRecovery /-! # Stage-1/Stage-2 `clearedParityJetTable` and Hermite–Cramer recovery across Section 6.3/6.4 This module connects the Stage-1/Stage-2 `JetTable` bridge and unconditional Hermite–Cramer -determinant recovery (`Complexity.Foundations.BooleanAnalysis.SparseHermiteRecovery`) with the +determinant recovery (`Complexity.Foundations.BooleanAnalysis.SparseHermiteJetRecovery`) with the Section 6.3 compiled CNF parity-row schedule (`Complexity.Computability.Complexity.FineGrained.GeneralCNFBranchSchedule`) and the Section 6.4 Proposition 6.4 tree-wide candidate-indexed recovery and examination bounds @@ -23,29 +23,10 @@ Proposition 6.4 tree-wide candidate-indexed recovery and examination bounds [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] (Sections 5.4–5.5, 6.1–6.4, and Appendices A–B, printed pp. 37–50): -1. **Appendix B.2–B.3 Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer coordinate recovery - and arbitrary-`ι` branch-summed recovery (`Cslib.BitString`, printed pp. 48–50):** - - `hermiteCramerNumerator_clearedParityJetTable_eq_mul`: at distinct integer nodes - `nodes : Fin Q → ℤ` with `(k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J`, the Cramer determinant - `hermiteCramerNumerator nodes hQ hJ` of - `fun t j => clearedParityJetTable I P d_den k ℓ J θ (nodes t) j s` - for each `V`-degree coordinate `s : Fin ℓ` equals - `(Polynomial.hermiteMatrix nodes J).det *` - `(univariateClearedParityCoord I P d_den k ℓ θ s.1).eval 0`. - - `emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount` and - `emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount`: summing the - exact integer Cramer quotients of the Stage-1/Stage-2 `JetTable` entries - `clearedParityJetTable I P (commonDenom Q R : ℤ) k ℓ J` - `(designReplacementScaledIntMap D emb) (nodeInt t) j s` - over `s : Fin ℓ` and reducing modulo `2 ^ ℓ` recovers `commonZeroCount I P` without auxiliary - `D_H` or `hcramer` premises (Appendix B.3, eq. `(B.1)`). - - `commonZeroCount_eq_sum_branch_hermiteCramerNumerator_design_of_fintype` and - `commonZeroCount_eq_sum_branch_clearedParityJetTable_design`: generalize branch-summed - Hermite–Cramer determinant recovery from `Fin n` to arbitrary finite variable types - `[Fintype ι] [DecidableEq ι]` (`S : Finset ι`, `e : ↥(univ \ S) ≃ Fin n'`) at shared precision - `ℓ = branchPrecision (Fintype.card ι)` and canonical jet order - `J = sparseParityJetOrder k R Q #I ℓ`, both for the single truncated-sum Cramer determinant and - for the Stage-1/Stage-2 `clearedParityJetTable` coordinate sum over `s : Fin ℓ`. +1. **Shared parity-system recovery (Appendix B.2–B.3, printed pp. 48–50):** + `Complexity.Foundations.BooleanAnalysis.SparseHermiteJetRecovery` supplies the generic + `Cslib.BitString` coordinate and arbitrary-finite-type branch recovery lemmas. This module + publicly imports that API and specializes it to CNF parity-row systems below. 2. **Section 6.3 compiled CNF parity-row schedule Hermite–Cramer and `clearedParityJetTable` recovery with `interpolationScale` examination bounds (`Cslib.Logic.PL.CNF`, pp. 38–43, 48–50):** @@ -89,11 +70,6 @@ and Appendices A–B, printed pp. 37–50): ## Main results -* `Cslib.BitString.hermiteCramerNumerator_clearedParityJetTable_eq_mul`, - `Cslib.BitString.emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount`, - `Cslib.BitString.emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount`, - `Cslib.BitString.commonZeroCount_eq_sum_branch_hermiteCramerNumerator_design_of_fintype`, - `Cslib.BitString.commonZeroCount_eq_sum_branch_clearedParityJetTable_design` * `Cslib.Logic.PL.CNF.commonZeroCount_parityRowSystem_eq_sum_branch_hermiteCramerNumerator_design`, `Cslib.Logic.PL.CNF.numPassing_eq_sum_branch_hermiteCramerNumerator_design`, `Cslib.Logic.PL.CNF.commonZeroCount_parityRowSystem_eq_sum_branch_clearedParityJetTable_design`, @@ -115,194 +91,6 @@ and Appendices A–B, printed pp. 37–50): open Finset Polynomial open scoped BigOperators -/-! ### 1. Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer recovery -/ - -namespace Cslib.BitString - -open Cslib.LinearAlgebra - -variable {ι κ : Type*} - -/-- **Cramer numerator factorization for `clearedParityJetTable` (Appendix B.2–B.3, eq. `(B.1)`, -pp. 48–50)**: when `(k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J`, the Cramer determinant of the -`s`-th `V`-degree coordinate (`s : Fin ℓ`) of the Stage-1/Stage-2 integer Taylor-jet table -`clearedParityJetTable I P d_den k ℓ J θ` at `nodes` equals -`(Polynomial.hermiteMatrix nodes J).det *` -`(univariateClearedParityCoord I P d_den k ℓ θ s.1).eval 0`. -/ -theorem hermiteCramerNumerator_clearedParityJetTable_eq_mul [Fintype ι] [DecidableEq ι] - (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) {k ℓ R_deg Q J : ℕ} - (nodes : Fin Q → ℤ) (hQ : 0 < Q) (hJ : 0 < J) - (θ : (ι → Bool) → κ → ι → Polynomial ℤ) - (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) - (hθ : ∀ x : ι → Bool, ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (θ x i v).natDegree ≤ R_deg) - (hQJ : (k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J) (s : Fin ℓ) : - hermiteCramerNumerator nodes hQ hJ - (fun t j => clearedParityJetTable I P d_den k ℓ J θ (nodes t) j s) = - (Polynomial.hermiteMatrix nodes J).det * - (univariateClearedParityCoord I P d_den k ℓ θ s.1).eval 0 := by - simp only [clearedParityJetTable_apply] - exact hermiteCramerNumerator_univariateClearedParityCoord_eq_mul I P d_den nodes hQ hJ θ hk hθ - hQJ s.2 - -/-- **Unconditional Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer coordinate recovery of -`commonZeroCount` (Appendix B.2–B.3, eq. `(B.1)`, pp. 48–50)**: at distinct integer nodes -`nodes : Fin Q → ℤ` with `(k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J`, `d_den ≠ 0`, and -`Fintype.card ι < ℓ`, summing the exact integer Cramer quotients of `clearedParityJetTable` over -`s : Fin ℓ` and reducing modulo `2 ^ ℓ` recovers `commonZeroCount I P`. -/ -theorem emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount - [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {d_den : ℤ} - (hd : d_den ≠ 0) {k ℓ R_deg Q J : ℕ} {nodes : Fin Q → ℤ} (hnodes : Function.Injective nodes) - (hQ : 0 < Q) (hJ : 0 < J) (hℓ : Fintype.card ι < ℓ) - (θ : (ι → Bool) → κ → ι → Polynomial ℤ) - (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) - (hdeg : ∀ x : ι → Bool, ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (θ x i v).natDegree ≤ R_deg) - (hθ : ∀ x : ι → Bool, ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, - (θ x i v).eval 0 = d_den * bitVal ℤ (x v)) - (hQJ : (k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J) : - (∑ s : Fin ℓ, - hermiteCramerNumerator nodes hQ hJ - (fun t j => clearedParityJetTable I P d_den k ℓ J θ (nodes t) j s) / - (clearedProductDenom d_den k ℓ #I * (Polynomial.hermiteMatrix nodes J).det)) % - ((2 : ℤ) ^ ℓ) = - commonZeroCount I P := by - simp only [clearedParityJetTable_apply] - rw [Fin.sum_univ_eq_sum_range (fun s => - hermiteCramerNumerator nodes hQ hJ - (fun t j => - (Polynomial.taylor (nodes t) - (univariateClearedParityCoord I P d_den k ℓ θ s)).coeff j.1) / - (clearedProductDenom d_den k ℓ #I * (Polynomial.hermiteMatrix nodes J).det))] - exact emod_sum_hermiteCramerNumerator_ediv_eq_commonZeroCount I P hd hnodes hQ hJ hℓ θ hk hdeg - hθ hQJ - -/-- **Concrete `ReplacementDesign` Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer -coordinate recovery of `commonZeroCount` (§5.4 & Appendix B.2–B.3, eq. `(B.1)`, pp. 48–50)**: -for any `D : ReplacementDesign scope Q r A₀ R τ` with `0 < Q`, `0 < J`, `n < ℓ`, -`∀ i ∈ I, ∀ M ∈ P i, #M ≤ k`, and `(k * (R - 1)) * (#I + 2 * (ℓ - 1)) < Q * J`, summing the -Cramer quotients of `clearedParityJetTable` at `nodeInt` over `s : Fin ℓ` and reducing modulo -`2 ^ ℓ` recovers `commonZeroCount I P`. -/ -theorem emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount - {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type*} [Fintype F] - {scope : F → Finset (Fin n)} (D : ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) - (I : Finset κ) (P : κ → Finset (Finset (Fin n))) {k ℓ J : ℕ} - (hQ : 0 < Q) (hJ : 0 < J) (hℓ : n < ℓ) - (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) - (hQJ : (k * (R - 1)) * (#I + 2 * (ℓ - 1)) < Q * J) : - (∑ s : Fin ℓ, - hermiteCramerNumerator (nodeInt (Q := Q)) hQ hJ - (fun t j => - clearedParityJetTable I P (commonDenom Q R : ℤ) k ℓ J - (designReplacementScaledIntMap D emb) (nodeInt t) j s) / - (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * - (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) = - commonZeroCount I P := by - simp only [clearedParityJetTable_apply] - rw [Fin.sum_univ_eq_sum_range (fun s => - hermiteCramerNumerator (nodeInt (Q := Q)) hQ hJ - (fun t j => - (Polynomial.taylor (nodeInt t) - (univariateClearedParityCoord I P (commonDenom Q R : ℤ) k ℓ - (designReplacementScaledIntMap D emb) s)).coeff j.1) / - (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * - (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det))] - exact emod_sum_hermiteCramerNumerator_design_eq_commonZeroCount D emb I P hQ hJ hℓ hk hQJ - -/-- **§5.5 & Appendix B.3 branch-summed Hermite–Cramer truncated-sum recovery of `commonZeroCount` -over arbitrary finite variable types `[Fintype ι] [DecidableEq ι]`**: given a heavy-variable subset -`S : Finset ι`, a free-variable relabeling `e : ↥(univ \ S) ≃ Fin n'`, and a per-branch -`ReplacementDesign` family `D b` (`0 < Q`), summing the branch modular residues of the concrete -`hermiteCramerNumerator` quotients at `nodeInt` and canonical jet order -`J = sparseParityJetOrder k R Q #I (branchPrecision (Fintype.card ι))` across -`b ∈ branchAssignments S` recovers `commonZeroCount I P`. -/ -theorem commonZeroCount_eq_sum_branch_hermiteCramerNumerator_design_of_fintype - [Fintype ι] [DecidableEq ι] {n' Q r A₀ R : ℕ} {τ : ℚ} - {F : (ι → Bool) → Type*} [∀ b, Fintype (F b)] - (S : Finset ι) (e : ↥(univ \ S) ≃ Fin n') - (I : Finset κ) (P : κ → Finset (Finset ι)) {k : ℕ} - (scope : (b : ι → Bool) → F b → Finset (Fin n')) - (D : (b : ι → Bool) → ReplacementDesign (scope b) Q r A₀ R τ) - (emb : (b : ι → Bool) → κ → F b) - (hQ : 0 < Q) (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) : - let ℓ := branchPrecision (Fintype.card ι) - let J := sparseParityJetOrder k R Q #I ℓ - (commonZeroCount I P : ℤ) = - ∑ b ∈ branchAssignments S, - (hermiteCramerNumerator (nodeInt (Q := Q)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) - (fun t j => - (Polynomial.taylor (nodeInt t) - (univariateClearedParityTruncatedSum I - (fun i => relabelRestrictedMonomials S e b (P i)) - (commonDenom Q R : ℤ) k ℓ - (designReplacementScaledIntMap (D b) (emb b)))).coeff j) / - (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * - (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) := by - intro ℓ J - rw [commonZeroCount_eq_sum_branch_emod_ediv_cleared S e I P (commonDenom_intCast_ne_zero Q R) - (fun b => designReplacementScaledIntMap (D b) (emb b)) hk - (fun b _ x j _ _ _ v _ => eval_zero_designReplacementScaledIntMap (D b) (emb b) x j v)] - refine sum_congr rfl fun b _ => ?_ - have hlt : n' < ℓ := by - have hle : n' ≤ Fintype.card ι := by - simpa only [Fintype.card_fin] using - (Fintype.card_congr e).symm.trans_le (Fintype.card_subtype_le _) - change n' < Fintype.card ι + 1 - omega - have hk_branch : ∀ i ∈ I, ∀ M ∈ relabelRestrictedMonomials S e b (P i), #M ≤ k := - fun i hi M hM => card_mem_relabelRestrictedMonomials_le (hk i hi) M hM - rw [emod_hermiteCramerNumerator_truncatedSum_design_eq_commonZeroCount (D b) (emb b) I - (fun i => relabelRestrictedMonomials S e b (P i)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) - hlt hk_branch (lt_mul_sparseParityJetOrder k R #I ℓ hQ)] - exact emod_ediv_eval_zero_clearedParityTruncatedSum_design_eq_commonZeroCount (D b) (emb b) I - (fun i => relabelRestrictedMonomials S e b (P i)) hlt hk_branch - -/-- **§5.5 & Appendix B.2–B.3 branch-summed Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer -coordinate recovery of `commonZeroCount` over arbitrary finite variable types**: under the same -hypotheses, summing the coordinate Cramer quotients of `clearedParityJetTable` over `s : Fin ℓ` -modulo `2 ^ ℓ` on each branch and summing across `b ∈ branchAssignments S` recovers -`commonZeroCount I P`. -/ -theorem commonZeroCount_eq_sum_branch_clearedParityJetTable_design - [Fintype ι] [DecidableEq ι] {n' Q r A₀ R : ℕ} {τ : ℚ} - {F : (ι → Bool) → Type*} [∀ b, Fintype (F b)] - (S : Finset ι) (e : ↥(univ \ S) ≃ Fin n') - (I : Finset κ) (P : κ → Finset (Finset ι)) {k : ℕ} - (scope : (b : ι → Bool) → F b → Finset (Fin n')) - (D : (b : ι → Bool) → ReplacementDesign (scope b) Q r A₀ R τ) - (emb : (b : ι → Bool) → κ → F b) - (hQ : 0 < Q) (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) : - let ℓ := branchPrecision (Fintype.card ι) - let J := sparseParityJetOrder k R Q #I ℓ - (commonZeroCount I P : ℤ) = - ∑ b ∈ branchAssignments S, - (∑ s : Fin ℓ, - hermiteCramerNumerator (nodeInt (Q := Q)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) - (fun t j => - clearedParityJetTable I - (fun i => relabelRestrictedMonomials S e b (P i)) - (commonDenom Q R : ℤ) k ℓ J - (designReplacementScaledIntMap (D b) (emb b)) (nodeInt t) j s) / - (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * - (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) := by - intro ℓ J - rw [commonZeroCount_eq_sum_branch_emod_ediv_cleared S e I P (commonDenom_intCast_ne_zero Q R) - (fun b => designReplacementScaledIntMap (D b) (emb b)) hk - (fun b _ x j _ _ _ v _ => eval_zero_designReplacementScaledIntMap (D b) (emb b) x j v)] - refine sum_congr rfl fun b _ => ?_ - have hlt : n' < ℓ := by - have hle : n' ≤ Fintype.card ι := by - simpa only [Fintype.card_fin] using - (Fintype.card_congr e).symm.trans_le (Fintype.card_subtype_le _) - change n' < Fintype.card ι + 1 - omega - have hk_branch : ∀ i ∈ I, ∀ M ∈ relabelRestrictedMonomials S e b (P i), #M ≤ k := - fun i hi M hM => card_mem_relabelRestrictedMonomials_le (hk i hi) M hM - rw [emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount (D b) (emb b) - I (fun i => relabelRestrictedMonomials S e b (P i)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) - hlt hk_branch (lt_mul_sparseParityJetOrder k R #I ℓ hQ)] - exact emod_ediv_eval_zero_clearedParityTruncatedSum_design_eq_commonZeroCount (D b) (emb b) I - (fun i => relabelRestrictedMonomials S e b (P i)) hlt hk_branch - -end Cslib.BitString - /-! ### 2. Section 6.3 CNF parity-row schedule Hermite–Cramer & `clearedParityJetTable` recovery -/ namespace Cslib.Logic.PL diff --git a/Complexity/Foundations/BooleanAnalysis/SparseHermiteJetRecovery.lean b/Complexity/Foundations/BooleanAnalysis/SparseHermiteJetRecovery.lean new file mode 100644 index 000000000..923e8a477 --- /dev/null +++ b/Complexity/Foundations/BooleanAnalysis/SparseHermiteJetRecovery.lean @@ -0,0 +1,225 @@ +/- +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.Foundations.BooleanAnalysis.SparseHermiteRecovery + +/-! +# Stage-1/Stage-2 jet-table Hermite–Cramer recovery + +This module connects `clearedParityJetTable` to the Hermite–Cramer recovery API in +`Complexity.Foundations.BooleanAnalysis.SparseHermiteRecovery`. It proves coordinate recovery +for finite parity systems and branch-summed recovery over arbitrary finite variable types, +independently of CNF formulas. The CNF specializations and examination bounds are in +`Complexity.Computability.Complexity.FineGrained.GeneralCNFHermiteRecovery`. + +## Main results + +* `Cslib.BitString.hermiteCramerNumerator_clearedParityJetTable_eq_mul`, + `Cslib.BitString.emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount`, + `Cslib.BitString.emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount`, + `Cslib.BitString.commonZeroCount_eq_sum_branch_hermiteCramerNumerator_design_of_fintype`, + `Cslib.BitString.commonZeroCount_eq_sum_branch_clearedParityJetTable_design` + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] + (Sections 5.4–5.5 and Appendix B.2–B.3, printed pp. 37–39, 48–50) +-/ + +@[expose] public noncomputable section + +open Finset Polynomial +open scoped BigOperators + +namespace Cslib.BitString + +open Cslib.LinearAlgebra + +variable {ι κ : Type*} + +/-- **Cramer numerator factorization for `clearedParityJetTable` (Appendix B.2–B.3, eq. `(B.1)`, +pp. 48–50)**: when `(k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J`, the Cramer determinant of the +`s`-th `V`-degree coordinate (`s : Fin ℓ`) of the Stage-1/Stage-2 integer Taylor-jet table +`clearedParityJetTable I P d_den k ℓ J θ` at `nodes` equals +`(Polynomial.hermiteMatrix nodes J).det *` +`(univariateClearedParityCoord I P d_den k ℓ θ s.1).eval 0`. -/ +theorem hermiteCramerNumerator_clearedParityJetTable_eq_mul [Fintype ι] [DecidableEq ι] + (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) {k ℓ R_deg Q J : ℕ} + (nodes : Fin Q → ℤ) (hQ : 0 < Q) (hJ : 0 < J) + (θ : (ι → Bool) → κ → ι → Polynomial ℤ) + (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) + (hθ : ∀ x : ι → Bool, ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (θ x i v).natDegree ≤ R_deg) + (hQJ : (k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J) (s : Fin ℓ) : + hermiteCramerNumerator nodes hQ hJ + (fun t j => clearedParityJetTable I P d_den k ℓ J θ (nodes t) j s) = + (Polynomial.hermiteMatrix nodes J).det * + (univariateClearedParityCoord I P d_den k ℓ θ s.1).eval 0 := by + simp only [clearedParityJetTable_apply] + exact hermiteCramerNumerator_univariateClearedParityCoord_eq_mul I P d_den nodes hQ hJ θ hk hθ + hQJ s.2 + +/-- **Unconditional Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer coordinate recovery of +`commonZeroCount` (Appendix B.2–B.3, eq. `(B.1)`, pp. 48–50)**: at distinct integer nodes +`nodes : Fin Q → ℤ` with `(k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J`, `d_den ≠ 0`, and +`Fintype.card ι < ℓ`, summing the exact integer Cramer quotients of `clearedParityJetTable` over +`s : Fin ℓ` and reducing modulo `2 ^ ℓ` recovers `commonZeroCount I P`. -/ +theorem emod_sum_hermiteCramerNumerator_clearedParityJetTable_ediv_eq_commonZeroCount + [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {d_den : ℤ} + (hd : d_den ≠ 0) {k ℓ R_deg Q J : ℕ} {nodes : Fin Q → ℤ} (hnodes : Function.Injective nodes) + (hQ : 0 < Q) (hJ : 0 < J) (hℓ : Fintype.card ι < ℓ) + (θ : (ι → Bool) → κ → ι → Polynomial ℤ) + (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) + (hdeg : ∀ x : ι → Bool, ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (θ x i v).natDegree ≤ R_deg) + (hθ : ∀ x : ι → Bool, ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, + (θ x i v).eval 0 = d_den * bitVal ℤ (x v)) + (hQJ : (k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J) : + (∑ s : Fin ℓ, + hermiteCramerNumerator nodes hQ hJ + (fun t j => clearedParityJetTable I P d_den k ℓ J θ (nodes t) j s) / + (clearedProductDenom d_den k ℓ #I * (Polynomial.hermiteMatrix nodes J).det)) % + ((2 : ℤ) ^ ℓ) = + commonZeroCount I P := by + simp only [clearedParityJetTable_apply] + rw [Fin.sum_univ_eq_sum_range (fun s => + hermiteCramerNumerator nodes hQ hJ + (fun t j => + (Polynomial.taylor (nodes t) + (univariateClearedParityCoord I P d_den k ℓ θ s)).coeff j.1) / + (clearedProductDenom d_den k ℓ #I * (Polynomial.hermiteMatrix nodes J).det))] + exact emod_sum_hermiteCramerNumerator_ediv_eq_commonZeroCount I P hd hnodes hQ hJ hℓ θ hk hdeg + hθ hQJ + +/-- **Concrete `ReplacementDesign` Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer +coordinate recovery of `commonZeroCount` (§5.4 & Appendix B.2–B.3, eq. `(B.1)`, pp. 48–50)**: +for any `D : ReplacementDesign scope Q r A₀ R τ` with `0 < Q`, `0 < J`, `n < ℓ`, +`∀ i ∈ I, ∀ M ∈ P i, #M ≤ k`, and `(k * (R - 1)) * (#I + 2 * (ℓ - 1)) < Q * J`, summing the +Cramer quotients of `clearedParityJetTable` at `nodeInt` over `s : Fin ℓ` and reducing modulo +`2 ^ ℓ` recovers `commonZeroCount I P`. -/ +theorem emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount + {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type*} [Fintype F] + {scope : F → Finset (Fin n)} (D : ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) + (I : Finset κ) (P : κ → Finset (Finset (Fin n))) {k ℓ J : ℕ} + (hQ : 0 < Q) (hJ : 0 < J) (hℓ : n < ℓ) + (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) + (hQJ : (k * (R - 1)) * (#I + 2 * (ℓ - 1)) < Q * J) : + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := Q)) hQ hJ + (fun t j => + clearedParityJetTable I P (commonDenom Q R : ℤ) k ℓ J + (designReplacementScaledIntMap D emb) (nodeInt t) j s) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) = + commonZeroCount I P := by + simp only [clearedParityJetTable_apply] + rw [Fin.sum_univ_eq_sum_range (fun s => + hermiteCramerNumerator (nodeInt (Q := Q)) hQ hJ + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityCoord I P (commonDenom Q R : ℤ) k ℓ + (designReplacementScaledIntMap D emb) s)).coeff j.1) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det))] + exact emod_sum_hermiteCramerNumerator_design_eq_commonZeroCount D emb I P hQ hJ hℓ hk hQJ + +/-- **§5.5 & Appendix B.3 branch-summed Hermite–Cramer truncated-sum recovery of `commonZeroCount` +over arbitrary finite variable types `[Fintype ι] [DecidableEq ι]`**: given a heavy-variable subset +`S : Finset ι`, a free-variable relabeling `e : ↥(univ \ S) ≃ Fin n'`, and a per-branch +`ReplacementDesign` family `D b` (`0 < Q`), summing the branch modular residues of the concrete +`hermiteCramerNumerator` quotients at `nodeInt` and canonical jet order +`J = sparseParityJetOrder k R Q #I (branchPrecision (Fintype.card ι))` across +`b ∈ branchAssignments S` recovers `commonZeroCount I P`. -/ +theorem commonZeroCount_eq_sum_branch_hermiteCramerNumerator_design_of_fintype + [Fintype ι] [DecidableEq ι] {n' Q r A₀ R : ℕ} {τ : ℚ} + {F : (ι → Bool) → Type*} [∀ b, Fintype (F b)] + (S : Finset ι) (e : ↥(univ \ S) ≃ Fin n') + (I : Finset κ) (P : κ → Finset (Finset ι)) {k : ℕ} + (scope : (b : ι → Bool) → F b → Finset (Fin n')) + (D : (b : ι → Bool) → ReplacementDesign (scope b) Q r A₀ R τ) + (emb : (b : ι → Bool) → κ → F b) + (hQ : 0 < Q) (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) : + let ℓ := branchPrecision (Fintype.card ι) + let J := sparseParityJetOrder k R Q #I ℓ + (commonZeroCount I P : ℤ) = + ∑ b ∈ branchAssignments S, + (hermiteCramerNumerator (nodeInt (Q := Q)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) + (fun t j => + (Polynomial.taylor (nodeInt t) + (univariateClearedParityTruncatedSum I + (fun i => relabelRestrictedMonomials S e b (P i)) + (commonDenom Q R : ℤ) k ℓ + (designReplacementScaledIntMap (D b) (emb b)))).coeff j) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) := by + intro ℓ J + rw [commonZeroCount_eq_sum_branch_emod_ediv_cleared S e I P (commonDenom_intCast_ne_zero Q R) + (fun b => designReplacementScaledIntMap (D b) (emb b)) hk + (fun b _ x j _ _ _ v _ => eval_zero_designReplacementScaledIntMap (D b) (emb b) x j v)] + refine sum_congr rfl fun b _ => ?_ + have hlt : n' < ℓ := by + have hle : n' ≤ Fintype.card ι := by + simpa only [Fintype.card_fin] using + (Fintype.card_congr e).symm.trans_le (Fintype.card_subtype_le _) + change n' < Fintype.card ι + 1 + omega + have hk_branch : ∀ i ∈ I, ∀ M ∈ relabelRestrictedMonomials S e b (P i), #M ≤ k := + fun i hi M hM => card_mem_relabelRestrictedMonomials_le (hk i hi) M hM + rw [emod_hermiteCramerNumerator_truncatedSum_design_eq_commonZeroCount (D b) (emb b) I + (fun i => relabelRestrictedMonomials S e b (P i)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) + hlt hk_branch (lt_mul_sparseParityJetOrder k R #I ℓ hQ)] + exact emod_ediv_eval_zero_clearedParityTruncatedSum_design_eq_commonZeroCount (D b) (emb b) I + (fun i => relabelRestrictedMonomials S e b (P i)) hlt hk_branch + +/-- **§5.5 & Appendix B.2–B.3 branch-summed Stage-1/Stage-2 `clearedParityJetTable` Hermite–Cramer +coordinate recovery of `commonZeroCount` over arbitrary finite variable types**: under the same +hypotheses, summing the coordinate Cramer quotients of `clearedParityJetTable` over `s : Fin ℓ` +modulo `2 ^ ℓ` on each branch and summing across `b ∈ branchAssignments S` recovers +`commonZeroCount I P`. -/ +theorem commonZeroCount_eq_sum_branch_clearedParityJetTable_design + [Fintype ι] [DecidableEq ι] {n' Q r A₀ R : ℕ} {τ : ℚ} + {F : (ι → Bool) → Type*} [∀ b, Fintype (F b)] + (S : Finset ι) (e : ↥(univ \ S) ≃ Fin n') + (I : Finset κ) (P : κ → Finset (Finset ι)) {k : ℕ} + (scope : (b : ι → Bool) → F b → Finset (Fin n')) + (D : (b : ι → Bool) → ReplacementDesign (scope b) Q r A₀ R τ) + (emb : (b : ι → Bool) → κ → F b) + (hQ : 0 < Q) (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) : + let ℓ := branchPrecision (Fintype.card ι) + let J := sparseParityJetOrder k R Q #I ℓ + (commonZeroCount I P : ℤ) = + ∑ b ∈ branchAssignments S, + (∑ s : Fin ℓ, + hermiteCramerNumerator (nodeInt (Q := Q)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) + (fun t j => + clearedParityJetTable I + (fun i => relabelRestrictedMonomials S e b (P i)) + (commonDenom Q R : ℤ) k ℓ J + (designReplacementScaledIntMap (D b) (emb b)) (nodeInt t) j s) / + (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * + (Polynomial.hermiteMatrix (nodeInt (Q := Q)) J).det)) % ((2 : ℤ) ^ ℓ) := by + intro ℓ J + rw [commonZeroCount_eq_sum_branch_emod_ediv_cleared S e I P (commonDenom_intCast_ne_zero Q R) + (fun b => designReplacementScaledIntMap (D b) (emb b)) hk + (fun b _ x j _ _ _ v _ => eval_zero_designReplacementScaledIntMap (D b) (emb b) x j v)] + refine sum_congr rfl fun b _ => ?_ + have hlt : n' < ℓ := by + have hle : n' ≤ Fintype.card ι := by + simpa only [Fintype.card_fin] using + (Fintype.card_congr e).symm.trans_le (Fintype.card_subtype_le _) + change n' < Fintype.card ι + 1 + omega + have hk_branch : ∀ i ∈ I, ∀ M ∈ relabelRestrictedMonomials S e b (P i), #M ≤ k := + fun i hi M hM => card_mem_relabelRestrictedMonomials_le (hk i hi) M hM + rw [emod_sum_hermiteCramerNumerator_clearedParityJetTable_design_eq_commonZeroCount (D b) (emb b) + I (fun i => relabelRestrictedMonomials S e b (P i)) hQ (sparseParityJetOrder_pos k R Q #I ℓ) + hlt hk_branch (lt_mul_sparseParityJetOrder k R #I ℓ hQ)] + exact emod_ediv_eval_zero_clearedParityTruncatedSum_design_eq_commonZeroCount (D b) (emb b) I + (fun i => relabelRestrictedMonomials S e b (P i)) hlt hk_branch + +end Cslib.BitString