diff --git a/Complexity.lean b/Complexity.lean index 15aed906a..4116b611b 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -772,6 +772,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 @@ -1830,6 +1831,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 new file mode 100644 index 000000000..9e80c930a --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean @@ -0,0 +1,1062 @@ +/- +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.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.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 +(`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. **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):** + - `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.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 + +/-! ### 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 ≤ BitString.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 ≤ BitString.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₀ := BitString.initialRowWeightBound B φ.length + let P := BitString.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₀ := BitString.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₀ := BitString.initialRowWeightBound B ψ.length + let P := BitString.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₀ := BitString.initialRowWeightBound B ψ.length + let P := BitString.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/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 diff --git a/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean b/ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFHermiteRecovery.lean new file mode 100644 index 000000000..41f80ff89 --- /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₀ := Cslib.BitString.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₀ := Cslib.BitString.initialRowWeightBound B ψ.length + let P := Cslib.BitString.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₀ := Cslib.BitString.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₀ := Cslib.BitString.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