From 9fddcffe3fd7d6bd84b613592f361bfbd31cda1a Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Tue, 27 Oct 2026 10:09:13 +0000 Subject: [PATCH 1/3] feat(PolyTime/CNF): add native sparse k-CNF leaf model counter --- Complexity.lean | 1 + .../PolyTime/CNF/SparseCNFLeafCounter.lean | 1363 +++++++++++++++++ ComplexityTests/SparseCNFLeafCounter.lean | 116 ++ 3 files changed, 1480 insertions(+) create mode 100644 Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean create mode 100644 ComplexityTests/SparseCNFLeafCounter.lean diff --git a/Complexity.lean b/Complexity.lean index 25bad897b..0e4d8517c 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1387,6 +1387,7 @@ public import Complexity.Computability.PolyTime.BooleanAnalysis.SparsePolyCounte public import Complexity.Computability.PolyTime.CNF.ClauseJetEval public import Complexity.Computability.PolyTime.CNF.GreedyParityContext public import Complexity.Computability.PolyTime.CNF.GreedyParitySearch +public import Complexity.Computability.PolyTime.CNF.SparseCNFLeafCounter public import Complexity.Computability.PolyTime.CNF.SparsePolyCompile public import Complexity.Computability.PolyTime.CommonCountingAccum public import Complexity.Computability.PolyTime.FineGrained.ParameterCheck diff --git a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean new file mode 100644 index 000000000..8ab1a7846 --- /dev/null +++ b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean @@ -0,0 +1,1363 @@ +/- +Copyright (c) 2026 Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anton Kovsharov +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Computability.Complexity.Problems.SAT +public import Complexity.Computability.GenericRAM.Native.ExhaustiveCountFallback +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List.Size +public import Complexity.Computability.PolyTime.BitString.InitialTestsSearch +public import Complexity.Computability.PolyTime.CNF.GreedyParityContext +public import Complexity.Computability.PolyTime.CNF.SparsePolyCompile +public import Complexity.Logics.Propositional.CNF.ModelCount.DenseRelabel +public import Complexity.Logics.Propositional.CNF.SparseParityCounter +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Mathlib.Data.List.GetD +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Native sparse `k`-CNF leaf model counter and occurring-support normalization + +Implements the deterministic sparse `k`-CNF model-counting algorithm of Section 6.3 (equation +(6.4), printed p. 43) of [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] on +native multi-tape Turing machines, parameterized over a sparse `𝔽₂` polynomial-system counter: +- **Encoded / machine-certified procedures**: `validDeclaredCNF`, `hasEmptyClause`, and + `entersSparseFastPath` are `ComputableInPolyTime` Boolean guards; `compiledRowCounter`, + `sparseCNFFastPath`, `sparseCNFDeclaredCounter`, `normalizeDeclaredLeaf`, and + `sparseCNFLeafCounter` are certified by `sparseCNFDeclaredCertificate`, + `normalizeDeclaredLeafCertificate`, and `sparseCNFLeafCertificate`. +- **Unencoded mathematical specifications**: `IsCompiledSparseSystem`, `sparseCNFTimeBound`, and + `ValidPolyTimeBound` state structural equation invariants and split runtime hypotheses. +- **Total fallback conventions**: `sparseCNFDeclaredCounter` returns `0` when + `validDeclaredCNF k N ψ = false`, when `[] ∈ ψ`, or when `N ≥ N₀` and `ψ.length > B * N`; returns + `2 ^ N` on `ψ = []`; and falls back to `countCNFExhaustive (N, ψ)` (which defaults variable + indices `≥ N` to `false`) when `N < N₀`. `normalizeDeclaredLeaf` shifts right by + `N - ψ.distinctVars.length` to recover `ψ.modelCount` within `≤ 2 ^ ψ.numVars`. + +## Main definitions + +* `validDeclaredCNF`, `hasEmptyClause`, `entersSparseFastPath`, `IsCompiledSparseSystem` +* `compiledRowCounter`, `sparseCNFFastPath`, `sparseCNFDeclaredCounter` +* `normalizeDeclaredLeaf`, `sparseCNFLeafCounter`, `sparseCNFTimeBound`, `ValidPolyTimeBound` +* `sparseCNFDeclaredCertificate`, `normalizeDeclaredLeafCertificate`, `sparseCNFLeafCertificate` + +## Main results + +* `isCompiledSparseSystem_compileParitySystemBounded`, + `commonZeroCount_compileParitySystemBounded_eq_numPassing` +* `sparseCNFDeclaredCounter_le_two_pow`, `sparseCNFDeclaredCounter_eq_modelCountOn`, + `sparseCNFDeclaredCounter_exhaustive_eq_modelCountOn` +* `normalizeDeclaredLeaf_eq_modelCount`, `sparseCNFLeafCounter_le_two_pow_numVars`, + `sparseCNFLeafCounter_eq_modelCount`, `sparseCNFLeafCounter_exhaustive_eq_modelCount` +* `polyBounded_sparseCNFDeclaredCertificate_space`, `exists_sparseCNFDeclaredCertificate_bounds`, + `computableInO_sparseCNFDeclaredCounter`, `computableInO_normalizeDeclaredLeaf`, + `polyBounded_sparseCNFLeafCertificate_space`, `exists_sparseCNFLeafCertificate_bounds`, + `computableInO_sparseCNFLeafCounter` + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Section 6.3, equation (6.4), + printed p. 43. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SparseCNFLeafCounter + +open Finset Cslib.BitString Cslib.GenericRAM Cslib.GenericRAM.ExhaustiveCountFallback +open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.CNF.GreedyContext +open Cslib.Complexity.InitialTestsSearch Turing.MultiTapeTM + +/-! ### 1. Guards, Compiled-System Invariant, and Core Definitions -/ + +/-- Guard checking clause widths `≤ k` and occurring variables `< N`. -/ +def validDeclaredCNF (k N : ℕ) (ψ : CNF ℕ) : Bool := + (ψ.all fun c => decide (c.length ≤ k)) && (ψ.vars.all fun v => decide (v < N)) + +/-- Boolean check for whether `ψ` contains an empty clause `[]`. -/ +def hasEmptyClause (ψ : CNF ℕ) : Bool := ψ.any List.isEmpty + +/-- Guard characterizing inputs `(N, B, ψ)` entering the Section 6.3 parity-test fast path. -/ +def entersSparseFastPath (k N₀ N B : ℕ) (ψ : CNF ℕ) : Bool := + validDeclaredCNF k N ψ && !ψ.isEmpty && !hasEmptyClause ψ && + !decide (N < N₀) && decide (ψ.length ≤ B * N) + +/-- Sparsity, canonicality, degree, and variable-range invariant satisfied by every sparse `𝔽₂` +polynomial system compiled along the Section 6.3 parity-test search. -/ +def IsCompiledSparseSystem (k N maxEqs maxTerms : ℕ) (sys : List (List (List ℕ))) : Prop := + sys.length ≤ maxEqs ∧ ∀ eq ∈ sys, IsCanonicalEquation eq ∧ eq.length ≤ maxTerms ∧ + ∀ mon ∈ eq, mon.length ≤ k ∧ ∀ v ∈ mon, v < N + +/-- Candidate parity-row counter compiling `(ψ, rows)` via `compileParitySystemBounded k` and +evaluating `polyCounter` at ambient variable count `N` whenever `rows.length ≤ 6 * N`. -/ +def compiledRowCounter (k : ℕ) (polyCounter : ℕ × List (List (List ℕ)) → ℕ) + (q : (ℕ × CNF ℕ) × List (List Bool)) : ℕ := + if decide (q.2.length ≤ 6 * q.1.1) then + polyCounter (q.1.1, compileParitySystemBounded k q.1.2 q.2) + else 0 + +/-- Deterministic Section 6.3 fast path: initial Tanner rows via `initialTestsRows`, `3 * N` rounds +of `greedyParityRows`, and one final `compiledRowCounter` call capped at `2 ^ N`. -/ +def sparseCNFFastPath (k N B : ℕ) (polyCounter : ℕ × List (List (List ℕ)) → ℕ) (ψ : CNF ℕ) : ℕ := + let m := ψ.length + let finalRows := greedyParityRows (fun rows => compiledRowCounter k polyCounter ((N, ψ), rows)) + N m (greedyRowListLength B m) (initialTestsRows m B) + min (2 ^ N) (compiledRowCounter k polyCounter ((N, ψ), finalRows)) + +/-- **Section 6.3 declared-range sparse `k`-CNF model counter.** +Returns `0` if invalid, `2 ^ N` on `[]`, `0` if `[] ∈ ψ`, `countCNFExhaustive (N, ψ)` if `N < N₀`, +`sparseCNFFastPath k N B polyCounter ψ` if `ψ.length ≤ B * N`, and `0` otherwise. -/ +def sparseCNFDeclaredCounter {P : Type*} (NOf BOf : P → ℕ) (k N₀ : ℕ) + (polyCounter : ℕ × List (List (List ℕ)) → ℕ) (x : P × CNF ℕ) : ℕ := + let N := NOf x.1; let B := BOf x.1; let ψ := x.2 + if validDeclaredCNF k N ψ then + if ψ.isEmpty then 2 ^ N + else if hasEmptyClause ψ then 0 + else if decide (N < N₀) then countCNFExhaustive (N, ψ) + else if decide (ψ.length ≤ B * N) then sparseCNFFastPath k N B polyCounter ψ + else 0 + else 0 + +/-- Right-shift normalization converting `ψ.modelCountOn (Finset.range (NOf p))` to +`ψ.modelCount`. -/ +def normalizeDeclaredLeaf {P : Type*} (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : ℕ := + h x >>> (NOf x.1 - x.2.distinctVars.length) + +/-- Normalized Section 6.3 sparse `k`-CNF leaf provider returning `ψ.modelCount` on valid sparse +width-`≤ k` formulas with variables in `Finset.range (NOf p)`. -/ +def sparseCNFLeafCounter {P : Type*} (NOf BOf : P → ℕ) (k N₀ : ℕ) + (polyCounter : ℕ × List (List (List ℕ)) → ℕ) (x : P × CNF ℕ) : ℕ := + normalizeDeclaredLeaf NOf (sparseCNFDeclaredCounter NOf BOf k N₀ polyCounter) x + +/-! ### 2. Structural & Semantic Proofs for Guards, Compilation, and Greedy Search -/ + +theorem validDeclaredCNF_eq_true_iff {k N : ℕ} {ψ : CNF ℕ} : + validDeclaredCNF k N ψ = true ↔ + (∀ c ∈ ψ, c.length ≤ k) ∧ ψ.vars.toFinset ⊆ Finset.range N := by + simp only [validDeclaredCNF, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq] + exact and_congr_right' ⟨fun h _ hv => Finset.mem_range.mpr (h _ (List.mem_toFinset.mp hv)), + fun h _ hv => Finset.mem_range.mp (h (List.mem_toFinset.mpr hv))⟩ + +theorem hasEmptyClause_eq_true_iff {ψ : CNF ℕ} : hasEmptyClause ψ = true ↔ [] ∈ ψ := by + simp only [hasEmptyClause, List.any_eq_true, List.isEmpty_iff] + exact ⟨fun ⟨_, hc, hnil⟩ => hnil ▸ hc, fun h => ⟨[], h, rfl⟩⟩ + +theorem entersSparseFastPath_eq_true_iff {k N₀ N B : ℕ} {ψ : CNF ℕ} : + entersSparseFastPath k N₀ N B ψ = true ↔ + validDeclaredCNF k N ψ = true ∧ ψ.isEmpty = false ∧ hasEmptyClause ψ = false ∧ + N₀ ≤ N ∧ ψ.length ≤ B * N := by + simp only [entersSparseFastPath, Bool.and_eq_true, Bool.not_eq_true', decide_eq_false_iff_not, + decide_eq_true_eq, not_lt, and_assoc] + +private theorem pos_of_nonempty_nonnil_valid {k N : ℕ} {ψ : CNF ℕ} + (hvalid : validDeclaredCNF k N ψ = true) (hne : ψ.isEmpty = false) + (hnil : hasEmptyClause ψ = false) : 1 ≤ N ∧ 1 ≤ ψ.length := by + obtain ⟨_, hsub⟩ := validDeclaredCNF_eq_true_iff.mp hvalid + rcases ψ with _ | ⟨_ | ⟨l, ls⟩, cs⟩ + · simp at hne + · exact False.elim (Bool.false_ne_true (hnil ▸ hasEmptyClause_eq_true_iff.mpr List.mem_cons_self)) + · have hlt := Finset.mem_range.mp (hsub (List.mem_toFinset.mpr + (CNF.mem_vars.mpr ⟨l :: ls, List.mem_cons_self, l.2, List.mem_cons_self⟩))) + exact ⟨by omega, by simp⟩ + +private theorem greedyRowListLength_pos {B m : ℕ} (hB : 1 ≤ B) : 1 ≤ greedyRowListLength B m := by + unfold greedyRowListLength + have := Nat.one_le_pow 2 B hB; have := Nat.one_le_pow 2 (Nat.log 2 m + 1) (Nat.succ_pos _) + nlinarith + +private theorem greedyRowListLength_le_initialRowWeightBound (B m : ℕ) : + greedyRowListLength B m ≤ initialRowWeightBound B m := by + unfold greedyRowListLength initialRowWeightBound + have := Nat.pow_le_pow_right (Nat.succ_pos (Nat.log 2 m)) (by decide : 2 ≤ 3); nlinarith + +/-- Every `compileParitySystemBounded k ψ rows` on a width-`≤ k` formula with variables `< N`, +`rows.length ≤ maxEqs`, and row Hamming weights `≤ W` satisfies `IsCompiledSparseSystem`. -/ +theorem isCompiledSparseSystem_compileParitySystemBounded {k N maxEqs W : ℕ} {ψ : CNF ℕ} + (hw : ∀ c ∈ ψ, c.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) + {rows : List (List Bool)} (hlen : rows.length ≤ maxEqs) (hwt : ∀ r ∈ rows, r.count true ≤ W) : + IsCompiledSparseSystem k N maxEqs (W * 2 ^ k) (compileParitySystemBounded k ψ rows) := by + rw [compileParitySystemBounded_eq_compileParitySystem hw] + refine ⟨by simpa only [compileParitySystem, List.length_map] using hlen, fun eq heq => ?_⟩ + obtain ⟨r, hr, rfl⟩ := List.mem_map.mp heq + refine ⟨isCanonicalEquation_compileParityRow ψ r, + (length_compileParityRow_le hw r).trans (Nat.mul_le_mul_right _ (hwt r hr)), + fun mon hmon => ⟨length_mem_compileParityRow_le hw r hmon, fun v hv => ?_⟩⟩ + exact Finset.mem_range.mp + (hsub (List.mem_toFinset.mpr (mem_vars_of_mem_compileParityRow hmon hv))) + +private def toFinCNF (N : ℕ) (hN : 1 ≤ N) (ψ : CNF ℕ) : CNF (Fin N) := + ψ.relabel fun v => ⟨v % N, Nat.mod_lt v hN⟩ + +private def extendFinAssign {N : ℕ} (σ : Fin N → Bool) (v : ℕ) : Bool := + (List.ofFn σ).getD v false + +private theorem extendFinAssign_lt {N : ℕ} (σ : Fin N → Bool) {v : ℕ} (hlt : v < N) : + extendFinAssign σ v = σ ⟨v, hlt⟩ := by + rw [extendFinAssign, List.getD_eq_getElem _ _ (by simp [hlt]), List.getElem_ofFn] + +private theorem eval_toFinCNF_eq {N : ℕ} (hN : 1 ≤ N) {ψ : CNF ℕ} + (hsub : ψ.vars.toFinset ⊆ Finset.range N) (σ : Fin N → Bool) : + (toFinCNF N hN ψ).eval σ = ψ.eval (extendFinAssign σ) := by + rw [toFinCNF, CNF.eval_relabel]; refine CNF.eval_congr fun v hv => ?_ + have hlt := Finset.mem_range.mp (hsub (List.mem_toFinset.mpr hv)) + simp only [Function.comp_apply, Nat.mod_eq_of_lt hlt, extendFinAssign_lt σ hlt] + +private theorem get_eval_toFinCNF_eq {N : ℕ} (hN : 1 ≤ N) {ψ : CNF ℕ} + (hsub : ψ.vars.toFinset ⊆ Finset.range N) (σ : Fin N → Bool) + (e : Fin (toFinCNF N hN ψ).length) : + ((toFinCNF N hN ψ).get e).eval σ = + (ψ.get ⟨e.1, by simpa only [toFinCNF, CNF.relabel, List.length_map] using e.2⟩).eval + (extendFinAssign σ) := by + have he_lt : e.1 < ψ.length := by simpa only [toFinCNF, CNF.relabel, List.length_map] using e.2 + change ((ψ.map (Clause.relabel fun v => ⟨v % N, Nat.mod_lt v hN⟩))[e.1]).eval σ = + ψ[e.1].eval (extendFinAssign σ) + rw [List.getElem_map, Clause.eval_relabel]; apply Bool.eq_iff_iff.mpr + simp only [Clause.eval_eq_true_iff] + refine exists_congr fun b => and_congr_right fun hb1 => ?_ + have hlt := Finset.mem_range.mp (hsub (List.mem_toFinset.mpr + (CNF.mem_vars.mpr ⟨ψ[e.1], List.getElem_mem he_lt, b.2, hb1⟩))) + simp only [Function.comp_apply, Nat.mod_eq_of_lt hlt, extendFinAssign_lt σ hlt] + +private theorem passesTests_toFinCNF_iff {N : ℕ} (hN : 1 ≤ N) {ψ : CNF ℕ} + (hsub : ψ.vars.toFinset ⊆ Finset.range N) (rows : List (List Bool)) (σ : Fin N → Bool) : + PassesTests (toFinCNF N hN ψ).violations + (rows.map (ofList (toFinCNF N hN ψ).length)) σ ↔ + PassesTests ψ.violations (rows.map fun r (e : Fin ψ.length) => r.getD e.1 false) + (extendFinAssign σ) := by + have hlen : (toFinCNF N hN ψ).length = ψ.length := by + simp only [toFinCNF, CNF.relabel, List.length_map] + simp only [PassesTests, List.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] + refine forall₂_congr fun r _ => ?_ + rw [show ofList (toFinCNF N hN ψ).length r ⬝ᵥ (toFinCNF N hN ψ).violations σ = + (fun e : Fin ψ.length => r.getD e.1 false) ⬝ᵥ ψ.violations (extendFinAssign σ) from + Fintype.sum_equiv (finCongr hlen) _ _ fun i => by + simp only [finCongr_apply, Fin.val_cast, ofList, CNF.violations, + get_eval_toFinCNF_eq hN hsub]; rfl] + +private theorem card_sat_toFinCNF_eq_modelCountOn {N : ℕ} (hN : 1 ≤ N) {ψ : CNF ℕ} + (hsub : ψ.vars.toFinset ⊆ Finset.range N) : + #{σ : Fin N → Bool | (toFinCNF N hN ψ).eval σ = true} = ψ.modelCountOn (Finset.range N) := by + let eqv : (Fin N → Bool) ≃ (↥(Finset.range N) → Bool) := + ⟨fun σ v => σ ⟨v.1, Finset.mem_range.mp v.2⟩, + fun τ i => τ ⟨i.1, Finset.mem_range.mpr i.2⟩, fun _ => rfl, fun _ => rfl⟩ + have heval (σ : Fin N → Bool) : (toFinCNF N hN ψ).eval σ = + ψ.eval (fun v => if hv : v ∈ Finset.range N then eqv σ ⟨v, hv⟩ else false) := by + rw [eval_toFinCNF_eq hN hsub σ]; refine CNF.eval_congr fun v hv => ?_ + have hlt := Finset.mem_range.mp (hsub (List.mem_toFinset.mpr hv)) + simp only [Finset.mem_range.mpr hlt, ↓reduceDIte, extendFinAssign_lt σ hlt]; rfl + rw [CNF.modelCountOn] + exact Finset.card_bij (fun σ _ => eqv σ) + (fun σ hσ => by + simp only [Finset.mem_filter, Finset.mem_univ, true_and, heval] at hσ ⊢; exact hσ) + (fun _ _ _ _ h => eqv.injective h) + (fun τ hτ => ⟨eqv.symm τ, by + simp only [Finset.mem_filter, Finset.mem_univ, true_and, heval, eqv.apply_symm_apply] at hτ ⊢ + exact hτ, eqv.apply_symm_apply τ⟩) + +/-- **Semantic bridge to `equationToFinset` and `CNF.parityRowSystem`**: on a width-`≤ k` formula +`ψ` with variables `< N` (`1 ≤ N`), `commonZeroCount` on `compileParitySystemBounded k ψ rows` +equals both `numPassing` and `commonZeroCount` on `(relabel ... ψ).parityRowSystem`. -/ +theorem commonZeroCount_compileParitySystemBounded_eq_numPassing {k N : ℕ} (hN : 1 ≤ N) + {ψ : CNF ℕ} (hw : ∀ c ∈ ψ, c.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) + (rows : List (List Bool)) : + let sys := compileParitySystemBounded k ψ rows + let ψFin : CNF (Fin N) := ψ.relabel fun v => ⟨v % N, Nat.mod_lt v hN⟩ + commonZeroCount (Finset.univ : Finset (Fin sys.length)) + (fun i : Fin sys.length => equationToFinset N sys[i]) = + numPassing ψFin.violations (rows.map (ofList ψFin.length)) ∧ + commonZeroCount (Finset.univ : Finset (Fin sys.length)) + (fun i : Fin sys.length => equationToFinset N sys[i]) = + commonZeroCount Finset.univ (ψFin.parityRowSystem (rows.map (ofList ψFin.length))) := by + dsimp only; set sys := compileParitySystemBounded k ψ rows + have hsys_eq : sys = compileParitySystem ψ rows := + compileParitySystemBounded_eq_compileParitySystem hw rows + have hcanon : ∀ eq ∈ sys, IsCanonicalEquation eq ∧ ∀ m ∈ eq, ∀ v ∈ m, v < N := by + rw [hsys_eq]; intro eq heq; obtain ⟨r, _, rfl⟩ := List.mem_map.mp heq + exact ⟨isCanonicalEquation_compileParityRow ψ r, fun m hm v hv => + Finset.mem_range.mp (hsub (List.mem_toFinset.mpr (mem_vars_of_mem_compileParityRow hm hv)))⟩ + have hnum : commonZeroCount (Finset.univ : Finset (Fin sys.length)) + (fun i : Fin sys.length => equationToFinset N sys[i]) = + numPassing (toFinCNF N hN ψ).violations (rows.map (ofList (toFinCNF N hN ψ).length)) := by + rw [← countSystemExhaustive_eq_commonZeroCount hcanon, countSystemExhaustive_eq_card_filter, + hsys_eq, numPassing] + congr 1; ext σ + simp only [Finset.mem_filter, Finset.mem_univ, true_and, + evalSystem_compileParitySystem_iff_passesTests, passesTests_toFinCNF_iff hN hsub]; rfl + exact ⟨hnum, hnum.trans (CNF.commonZeroCount_parityRowSystem (toFinCNF N hN ψ) _).symm⟩ + +private theorem modelCountOn_le_two_pow_card {V : Type*} [DecidableEq V] (ψ : CNF V) + (declared : Finset V) : ψ.modelCountOn declared ≤ 2 ^ declared.card := by + rw [CNF.modelCountOn]; refine (Finset.card_filter_le _ _).trans ?_ + simp only [Finset.card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_coe, le_rfl] + +/-- Unconditional upper bound: `sparseCNFDeclaredCounter` never exceeds `2 ^ NOf x.1`. -/ +theorem sparseCNFDeclaredCounter_le_two_pow {P : Type*} (NOf BOf : P → ℕ) (k N₀ : ℕ) + (polyCounter : ℕ × List (List (List ℕ)) → ℕ) (x : P × CNF ℕ) : + sparseCNFDeclaredCounter NOf BOf k N₀ polyCounter x ≤ 2 ^ NOf x.1 := by + unfold sparseCNFDeclaredCounter sparseCNFFastPath; dsimp only + split_ifs + · exact le_rfl + · exact Nat.zero_le _ + · rw [countCNFExhaustive_eq_modelCountOn_range (NOf x.1) x.2] + simpa only [Finset.card_range] using modelCountOn_le_two_pow_card x.2 (Finset.range (NOf x.1)) + · exact Nat.min_le_left _ _ + · exact Nat.zero_le _ + · exact Nat.zero_le _ + +/-- **Exactness of `sparseCNFDeclaredCounter` (§6.3, Lemmas 6.1–6.2).** -/ +theorem sparseCNFDeclaredCounter_eq_modelCountOn {P : Type*} {NOf BOf : P → ℕ} {k N₀ : ℕ} + {polyCounter : ℕ × List (List (List ℕ)) → ℕ} {p : P} {ψ : CNF ℕ} + (hw : ∀ c ∈ ψ, c.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) + (hdom : ψ.length ≤ BOf p * NOf p ∨ ψ = [] ∨ [] ∈ ψ ∨ NOf p < N₀) + (hpoly : N₀ ≤ NOf p → ∀ sys : List (List (List ℕ)), + IsCompiledSparseSystem k (NOf p) (6 * NOf p) + (initialRowWeightBound (BOf p) ψ.length * 2 ^ k) sys → + polyCounter (NOf p, sys) = + commonZeroCount (Finset.univ : Finset (Fin sys.length)) + (fun i : Fin sys.length => equationToFinset (NOf p) sys[i])) : + sparseCNFDeclaredCounter NOf BOf k N₀ polyCounter (p, ψ) = + ψ.modelCountOn (Finset.range (NOf p)) := by + have hvalid : validDeclaredCNF k (NOf p) ψ = true := validDeclaredCNF_eq_true_iff.mpr ⟨hw, hsub⟩ + unfold sparseCNFDeclaredCounter; simp only [hvalid, ↓reduceIte] + by_cases he : ψ.isEmpty = true + · simp only [he, ↓reduceIte]; rw [List.isEmpty_iff.mp he, CNF.modelCountOn_nil, Finset.card_range] + · simp only [Bool.not_eq_true] at he; simp only [he, Bool.false_eq_true, ↓reduceIte] + by_cases hnil : hasEmptyClause ψ = true + · simp only [hnil, ↓reduceIte] + exact (CNF.modelCountOn_eq_zero_of_nil_mem (hasEmptyClause_eq_true_iff.mp hnil) _).symm + · simp only [Bool.not_eq_true] at hnil; simp only [hnil, Bool.false_eq_true, ↓reduceIte] + by_cases hlt : NOf p < N₀ + · simp only [decide_eq_true hlt, ↓reduceIte] + exact countCNFExhaustive_eq_modelCountOn_range (NOf p) ψ + · have hge := Nat.le_of_not_lt hlt + simp only [decide_eq_false hlt, Bool.false_eq_true, ↓reduceIte] + have hmB : ψ.length ≤ BOf p * NOf p := by + rcases hdom with hm | rfl | hmem | hlt' + · exact hm + · simp at he + · exact False.elim (Bool.false_ne_true (hnil ▸ hasEmptyClause_eq_true_iff.mpr hmem)) + · exact False.elim (hlt hlt') + simp only [decide_eq_true hmB, ↓reduceIte] + obtain ⟨hN1, _⟩ := pos_of_nonempty_nonnil_valid hvalid he hnil + have hB1 : 1 ≤ BOf p := by + rcases Nat.eq_zero_or_pos (BOf p) with hB0 | hBp + · rw [hB0, Nat.zero_mul] at hmB; omega + · exact hBp + obtain ⟨_, hinit_rows, hinit_dist⟩ := initialTestsRows_spec hN1 hB1 hmB + let ψFin := toFinCNF (NOf p) hN1 ψ + have hcard : Fintype.card (Fin (NOf p)) = NOf p := Fintype.card_fin (NOf p) + have hlen_fin : ψFin.length = ψ.length := by + simp only [ψFin, toFinCNF, CNF.relabel, List.length_map] + have hgreedy := count_greedy_eq_card_sat (compiledRowCounter k polyCounter) + (NOf p, ψ) ψFin (P := greedyRowListLength (BOf p) ψ.length) + (by rw [hcard]; exact hN1) (greedyRowListLength_pos hB1) + (initRows := initialTestsRows ψ.length (BOf p)) + (fun r hr => (hinit_rows r hr).1.trans hlen_fin.symm) + (fun rows _ hrows_len hrows_wt => by + have h6 : rows.length ≤ 6 * NOf p := by rw [hcard] at hrows_len; omega + have hwt : ∀ r ∈ rows, r.count true ≤ initialRowWeightBound (BOf p) ψ.length := + fun r hr => (hrows_wt r hr).elim (fun h => (hinit_rows r h).2) fun hP => + hP.trans (greedyRowListLength_le_initialRowWeightBound (BOf p) ψ.length) + have his := isCompiledSparseSystem_compileParitySystemBounded hw hsub h6 hwt + simp only [compiledRowCounter, decide_eq_true h6, ↓reduceIte]; rw [hpoly hge _ his] + exact (commonZeroCount_compileParitySystemBounded_eq_numPassing hN1 hw hsub rows).1) + (fun σ hpass hfalse => by + have hz_ne : ψFin.violations σ ≠ 0 := fun h0 => + Bool.false_ne_true (hfalse.symm.trans ((CNF.violations_eq_zero_iff ψFin σ).mp h0)) + have hdot : ∀ row ∈ initialTestsRows ψ.length (BOf p), + ofList ψ.length row ⬝ᵥ + (fun e : Fin ψ.length => ψFin.violations σ ⟨e.1, by omega⟩) = false := + fun row hrow => (Fintype.sum_equiv (finCongr hlen_fin) _ _ fun _ => rfl).symm.trans + (hpass (ofList ψFin.length row) (List.mem_map_of_mem hrow)) + let eqv : Fin ψ.length ≃ Fin ψFin.length := finCongr hlen_fin.symm + have hwt_eq : weight (fun e : Fin ψ.length => ψFin.violations σ ⟨e.1, by omega⟩) = + weight (ψFin.violations σ) := + Finset.card_bij (fun i _ => eqv i) + (fun _ hi => by + simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi ⊢; exact hi) + (fun _ _ _ _ h => eqv.injective h) + (fun j hj => ⟨eqv.symm j, + by simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hj ⊢; exact hj, + eqv.apply_symm_apply j⟩) + have hz_ne' : (fun e : Fin ψ.length => ψFin.violations σ ⟨e.1, by omega⟩) ≠ 0 := + fun h0 => hz_ne (funext fun e => congrFun h0 ⟨e.1, by omega⟩) + have hdist := hinit_dist _ hz_ne' hdot + rw [hwt_eq] at hdist; exact hlen_fin.le.trans hdist) + rw [hcard, hlen_fin, card_sat_toFinCNF_eq_modelCountOn hN1 hsub] at hgreedy + unfold sparseCNFFastPath; dsimp only; rw [hgreedy] + exact Nat.min_eq_right (by + simpa only [Finset.card_range] using + modelCountOn_le_two_pow_card ψ (Finset.range (NOf p))) + +/-- Instantiation of `sparseCNFDeclaredCounter` with `countSystemExhaustive` computes +`ψ.modelCountOn (Finset.range (NOf p))` unconditionally on every valid sparse formula. -/ +theorem sparseCNFDeclaredCounter_exhaustive_eq_modelCountOn {P : Type*} {NOf BOf : P → ℕ} + {k N₀ : ℕ} {p : P} {ψ : CNF ℕ} + (hw : ∀ c ∈ ψ, c.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) + (hdom : ψ.length ≤ BOf p * NOf p ∨ ψ = [] ∨ [] ∈ ψ ∨ NOf p < N₀) : + sparseCNFDeclaredCounter NOf BOf k N₀ countSystemExhaustive (p, ψ) = + ψ.modelCountOn (Finset.range (NOf p)) := + sparseCNFDeclaredCounter_eq_modelCountOn hw hsub hdom fun _ _ hsys => + countSystemExhaustive_eq_commonZeroCount fun eq heq => + ⟨(hsys.2 eq heq).1, fun m hm v hv => ((hsys.2 eq heq).2.2 m hm).2 v hv⟩ + +/-! ### 3. Exact Occurring-Support Normalization (`normalizeDeclaredLeaf`) -/ + +theorem normalizeDeclaredLeaf_eq_div {P : Type*} (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : + normalizeDeclaredLeaf NOf h x = h x / 2 ^ (NOf x.1 - x.2.numVars) := by + rw [normalizeDeclaredLeaf, Nat.shiftRight_eq_div_pow, CNF.length_distinctVars] + +/-- `normalizeDeclaredLeaf` recovers `ψ.modelCount` from `ψ.modelCountOn (Finset.range (NOf p))`. -/ +theorem normalizeDeclaredLeaf_eq_modelCount {P : Type*} {NOf : P → ℕ} {h : P × CNF ℕ → ℕ} + {p : P} {ψ : CNF ℕ} (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) + (hh : h (p, ψ) = ψ.modelCountOn (Finset.range (NOf p))) : + normalizeDeclaredLeaf NOf h (p, ψ) = ψ.modelCount := by + rw [normalizeDeclaredLeaf_eq_div, hh, + CNF.modelCountOn_eq_mul_modelCount ψ (Finset.range (NOf p)) hsub, Finset.card_range, + Nat.mul_div_right _ (by positivity)] + +/-- `normalizeDeclaredLeaf` is bounded by `2 ^ ψ.numVars` whenever `h (p, ψ) ≤ 2 ^ NOf p`. -/ +theorem normalizeDeclaredLeaf_le_two_pow_numVars {P : Type*} {NOf : P → ℕ} {h : P × CNF ℕ → ℕ} + {p : P} {ψ : CNF ℕ} (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) + (hh : h (p, ψ) ≤ 2 ^ NOf p) : + normalizeDeclaredLeaf NOf h (p, ψ) ≤ 2 ^ ψ.numVars := by + rw [normalizeDeclaredLeaf_eq_div] + have hle : ψ.numVars ≤ NOf p := by + simpa only [CNF.numVars, Finset.card_range] using Finset.card_le_card hsub + exact Nat.div_le_of_le_mul (hh.trans (by rw [← pow_add, Nat.sub_add_cancel hle])) + +/-- **Unconditional leaf-accumulator bound**: `sparseCNFLeafCounter` never exceeds `2 ^ ψ.numVars` +on any input `(p, ψ)`, regardless of `polyCounter`. -/ +theorem sparseCNFLeafCounter_le_two_pow_numVars {P : Type*} (NOf BOf : P → ℕ) (k N₀ : ℕ) + (polyCounter : ℕ × List (List (List ℕ)) → ℕ) (x : P × CNF ℕ) : + sparseCNFLeafCounter NOf BOf k N₀ polyCounter x ≤ 2 ^ x.2.numVars := by + rcases x with ⟨p, ψ⟩ + by_cases hv : validDeclaredCNF k (NOf p) ψ = true + · exact normalizeDeclaredLeaf_le_two_pow_numVars (validDeclaredCNF_eq_true_iff.mp hv).2 + (sparseCNFDeclaredCounter_le_two_pow NOf BOf k N₀ polyCounter (p, ψ)) + · simp only [Bool.not_eq_true] at hv + simp only [sparseCNFLeafCounter, normalizeDeclaredLeaf, sparseCNFDeclaredCounter, hv, + Bool.false_eq_true, ↓reduceIte, Nat.zero_shiftRight, Nat.zero_le] + +/-- **Exactness of `sparseCNFLeafCounter`**: returns `ψ.modelCount` on every valid width-`≤ k` +sparse leaf `ψ` with variables in `Finset.range (NOf p)`. -/ +theorem sparseCNFLeafCounter_eq_modelCount {P : Type*} {NOf BOf : P → ℕ} {k N₀ : ℕ} + {polyCounter : ℕ × List (List (List ℕ)) → ℕ} {p : P} {ψ : CNF ℕ} + (hw : ∀ c ∈ ψ, c.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) + (hdom : ψ.length ≤ BOf p * NOf p ∨ ψ = [] ∨ [] ∈ ψ ∨ NOf p < N₀) + (hpoly : N₀ ≤ NOf p → ∀ sys : List (List (List ℕ)), + IsCompiledSparseSystem k (NOf p) (6 * NOf p) + (initialRowWeightBound (BOf p) ψ.length * 2 ^ k) sys → + polyCounter (NOf p, sys) = + commonZeroCount (Finset.univ : Finset (Fin sys.length)) + (fun i : Fin sys.length => equationToFinset (NOf p) sys[i])) : + sparseCNFLeafCounter NOf BOf k N₀ polyCounter (p, ψ) = ψ.modelCount := + normalizeDeclaredLeaf_eq_modelCount hsub + (sparseCNFDeclaredCounter_eq_modelCountOn hw hsub hdom hpoly) + +/-- Instantiation of `sparseCNFLeafCounter` with `countSystemExhaustive` computes `ψ.modelCount`. -/ +theorem sparseCNFLeafCounter_exhaustive_eq_modelCount {P : Type*} {NOf BOf : P → ℕ} {k N₀ : ℕ} + {p : P} {ψ : CNF ℕ} + (hw : ∀ c ∈ ψ, c.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) + (hdom : ψ.length ≤ BOf p * NOf p ∨ ψ = [] ∨ [] ∈ ψ ∨ NOf p < N₀) : + sparseCNFLeafCounter NOf BOf k N₀ countSystemExhaustive (p, ψ) = ψ.modelCount := + normalizeDeclaredLeaf_eq_modelCount hsub + (sparseCNFDeclaredCounter_exhaustive_eq_modelCountOn hw hsub hdom) + +end Cslib.Complexity.SparseCNFLeafCounter + +end + +/-! ### 4. Native Machine Certificates and Split Time / Polynomial-Space Bounds -/ + +public section + +namespace Cslib.Complexity.SparseCNFLeafCounter + +open Finset Cslib.BitString Cslib.GenericRAM Cslib.GenericRAM.ExhaustiveCountFallback +open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.CNF.GreedyContext +open Cslib.Complexity.InitialTestsSearch Turing.MultiTapeTM + +local notation "encSys" => encList (encList (encList encNat)) +local notation "PolySys" => ℕ × List (List (List ℕ)) + +private abbrev encCandCtx := encPair encUnary encCNF +private abbrev encCandIn := encPair encCandCtx (encList encBits) + +variable {P : Type} {encP : P ↪ List Bool} {NOf BOf : P → ℕ} {polyCounter : PolySys → ℕ} + +/-- Split Section 6.3 runtime upper bound: `poly L` outside `entersSparseFastPath`, and initial +Tanner search plus `(3 * N + 1) * ((2 * m) ^ P + 1)` candidate system evaluations inside. -/ +def sparseCNFTimeBound (encP : P ↪ List Bool) (NOf BOf : P → ℕ) (k N₀ : ℕ) + (poly qInit : ℕ → ℕ) (R : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : ℕ := + let L := (encPair encP encCNF x).length; let N := NOf x.1; let B := BOf x.1; let m := x.2.length + if entersSparseFastPath k N₀ N B x.2 then + poly L + 2 ^ qInit (B + Nat.log 2 (m + 2)) + + (3 * N + 1) * (candidateTupleCount m (greedyRowListLength B m) + 1) * (poly L + R x) + else poly L + +/-- Hypothesis bounding `cPoly.time (NOf x.1, sys) ≤ R x` on every compiled sparse system of at +most `6 * NOf x.1` equations and polynomial encoded length produced on the Section 6.3 fast path. -/ +def ValidPolyTimeBound (encP : P ↪ List Bool) (NOf BOf : P → ℕ) (k N₀ : ℕ) + {polyCounter : PolySys → ℕ} + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (polySys : ℕ → ℕ) (R : P × CNF ℕ → ℕ) : Prop := + ∀ x : P × CNF ℕ, entersSparseFastPath k N₀ (NOf x.1) (BOf x.1) x.2 = true → + ∀ sys : List (List (List ℕ)), + IsCompiledSparseSystem k (NOf x.1) (6 * NOf x.1) + (initialRowWeightBound (BOf x.1) x.2.length * 2 ^ k) sys → + (encPair encUnary encSys (NOf x.1, sys)).length ≤ polySys (encPair encP encCNF x).length → + cPoly.time (NOf x.1, sys) ≤ R x + +private theorem exists_mono_poly {α : Type} {size u : α → ℕ} (hu : PolyBounded size u) : + ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ Monotone p ∧ ∀ a, u a ≤ p (size a) := by + obtain ⟨c, d, h⟩ := hu.exists_le + exact ⟨fun n => c * (n + 1) ^ d, by fun_prop, + fun _ _ hxy => Nat.mul_le_mul_left c (Nat.pow_le_pow_left (Nat.add_le_add_right hxy 1) d), h⟩ + +private theorem polyBounded_output_of_space {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool} + {f : α → β} (c : NativeCertificate f ei eo) + (hs : PolyBounded (fun a => (ei a).length) c.space) : + PolyBounded (fun a => (ei a).length) (fun a => (eo (f a)).length) := + let ⟨k, _, hl⟩ := c.computes; ((PolyBounded.const k).mul (hs.add (.const 1))).mono hl + +private theorem polyBounded_comp_space {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} + {eo : γ ↪ List Bool} {f : α → β} {g : β → γ} (d : NativeCertificate g em eo) + (c : NativeCertificate f ei em) (hd : PolyBounded (fun b => (em b).length) d.space) + (hc : PolyBounded (fun a => (ei a).length) c.space) : + PolyBounded (fun a => (ei a).length) (d.comp c).space := + hc.add (hd.comp (polyBounded_output_of_space c hc)) + +private theorem polyBounded_prod_space {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} + {eo : γ ↪ List Bool} {f : α → β} {g : α → γ} (c : NativeCertificate f ei em) + (d : NativeCertificate g ei eo) (hc : PolyBounded (fun a => (ei a).length) c.space) + (hd : PolyBounded (fun a => (ei a).length) d.space) : + PolyBounded (fun a => (ei a).length) (c.prod d).space := hc.add hd + +private theorem polyBounded_pair_len {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool} + {f : α → β} (hf : PolyBounded (fun a => (ei a).length) (fun a => (eo (f a)).length)) : + PolyBounded (fun a => (ei a).length) (fun a => (encPair ei eo (a, f a)).length) := + ((((PolyBounded.const 2).mul PolyBounded.self).add hf).add (.const 2)).mono fun a => by + simp only [length_encPair]; omega + +private abbrev toSysInput (k : ℕ) (q : (ℕ × CNF ℕ) × List (List Bool)) : PolySys := + (q.1.1, compileParitySystemBounded k q.1.2 q.2) + +private theorem computableInPolyTime_toSysInput (k : ℕ) : + ComputableInPolyTime (toSysInput k) encCandIn (encPair encUnary encSys) := by + unfold toSysInput encCandIn encCandCtx; fun_prop + +private theorem computableInPolyTime_rowLenGuard : + ComputableInPolyTime (fun q : (ℕ × CNF ℕ) × List (List Bool) => decide (q.2.length ≤ 6 * q.1.1)) + encCandIn encBool := .of_tidy (by unfold encCandIn encCandCtx; fun_prop) + +private noncomputable def compiledRowCertificate (k : ℕ) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) : + NativeCertificate (compiledRowCounter k polyCounter) encCandIn encNat := + guardedTargetOfPolyTime computableInPolyTime_rowLenGuard + (cPoly.comp (NativeCertificate.ofPolyTime (computableInPolyTime_toSysInput k))) + (NativeCertificate.const 0) + (fun _ h => by simp only [Function.comp_apply, toSysInput, compiledRowCounter, h, ↓reduceIte]) + (fun _ h => by simp only [compiledRowCounter, h, Bool.false_eq_true, ↓reduceIte]) + +private theorem polyBounded_compiledRowCertificate_space (k : ℕ) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (hSpace : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space) : + PolyBounded (fun q => (encCandIn q).length) (compiledRowCertificate k cPoly).space := + polyBounded_branch_space _ _ _ + (NativeCertificate.ofPolyTime_isPolynomial computableInPolyTime_rowLenGuard).2 + (polyBounded_comp_space cPoly (NativeCertificate.ofPolyTime (computableInPolyTime_toSysInput k)) + hSpace (NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_toSysInput k)).2) + PolyBounded.self + +private noncomputable def greedyCellTime (k : ℕ) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (a : (ℕ × CNF ℕ) × ℕ × ℕ × ℕ × List (List Bool)) (i j : ℕ) : ℕ := + (compiledRowCertificate k cPoly).time (a.1, + greedyParityRowsAt (fun r => compiledRowCounter k polyCounter (a.1, r)) + a.2.2.1 a.2.2.2.1 a.2.2.2.2 i ++ + [materializeTestRow a.2.2.1 (decodeTestTuple a.2.2.1 a.2.2.2.1 j)]) + +private noncomputable def greedyMaxCellTime (k : ℕ) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (a : (ℕ × CNF ℕ) × ℕ × ℕ × ℕ × List (List Bool)) : ℕ := + listMax (fun i => listMax (greedyCellTime k cPoly a i) + (List.range (candidateTupleCount a.2.2.1 a.2.2.2.1 + 1))) (List.range (3 * a.2.1 + 1)) + +private theorem le_greedyMaxCellTime (k : ℕ) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (a : (ℕ × CNF ℕ) × ℕ × ℕ × ℕ × List (List Bool)) {i j : ℕ} + (hi : i ≤ 3 * a.2.1) (hj : j ≤ candidateTupleCount a.2.2.1 a.2.2.2.1) : + greedyCellTime k cPoly a i j ≤ greedyMaxCellTime k cPoly a := + (le_listMax (f := greedyCellTime k cPoly a i) (List.mem_range.mpr (by omega))).trans + (le_listMax (f := fun i' => listMax (greedyCellTime k cPoly a i') + (List.range (candidateTupleCount a.2.2.1 a.2.2.2.1 + 1))) (List.mem_range.mpr (by omega))) + +open Classical in +private noncomputable def greedyBoundedCertificate (k : ℕ) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) : + NativeCertificate + (fun a : (ℕ × CNF ℕ) × ℕ × ℕ × ℕ × List (List Bool) => + greedyParityRows (fun r => compiledRowCounter k polyCounter (a.1, r)) + a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) + (encGreedyInput encCandCtx) (encList encBits) := + let cCand := compiledRowCertificate k cPoly + if h : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space then + let hG := computableInO_greedy cCand (polyBounded_compiledRowCertificate_space k cPoly h) + (greedyMaxCellTime k cPoly) (fun a _ hi _ hj => le_greedyMaxCellTime k cPoly a hi hj) + ⟨fun a => (3 * a.2.1 + 1) * (candidateTupleCount a.2.2.1 a.2.2.2.1 + 1) * + (hG.choose (encGreedyInput encCandCtx a).length + greedyMaxCellTime k cPoly a), + fun a => hG.choose (encGreedyInput encCandCtx a).length, hG.choose_spec.2⟩ + else greedyCertificate cCand + +private theorem polyBounded_greedyBoundedCertificate_space (k : ℕ) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (hSpace : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space) : + PolyBounded (fun a => (encGreedyInput encCandCtx a).length) + (greedyBoundedCertificate k cPoly).space := by + let hG := computableInO_greedy (compiledRowCertificate k cPoly) + (polyBounded_compiledRowCertificate_space k cPoly hSpace) (greedyMaxCellTime k cPoly) + (fun a _ hi _ hj => le_greedyMaxCellTime k cPoly a hi hj) + have heq : (greedyBoundedCertificate k cPoly).space = + fun a => hG.choose (encGreedyInput encCandCtx a).length := by + unfold greedyBoundedCertificate; simp only [hSpace, ↓reduceDIte] + rw [heq]; exact PolyBounded.of_polynomiallyBounded _ hG.choose_spec.1 + +private theorem computableInPolyTime_validDeclaredCNF (k : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) : + ComputableInPolyTime (fun x : P × CNF ℕ => validDeclaredCNF k (NOf x.1) x.2) + (encPair encP encCNF) encBool := by + refine .of_tidy ?_ + have hN_nat := ComputableTidilyInPolyTime.unary_to_binary.comp + (hNOf.tidy.comp (ComputableTidilyInPolyTime.fst encP encCNF)) + have h1 : ComputableTidilyInPolyTime (fun x : P × CNF ℕ => x.2.all fun c => decide (c.length ≤ k)) + (encPair encP encCNF) encBool := by + apply ComputableTidilyInPolyTime.allWithInput (by fun_prop) + have := (SAT.computableInPolyTime_clause_length (by fun_prop : ComputableInPolyTime Prod.snd + (encPair (encPair encP encCNF) (encList (encPair encNat encBool))) _)).tidy + fun_prop + have h2 : ComputableTidilyInPolyTime + (fun x : P × CNF ℕ => x.2.vars.all fun v => decide (v < NOf x.1)) + (encPair encP encCNF) encBool := by + apply ComputableTidilyInPolyTime.allWithInput + (SAT.computableInPolyTime_vars.tidy.comp (ComputableTidilyInPolyTime.snd encP encCNF)) + exact ComputableTidilyInPolyTime.binary_lt' + (ComputableTidilyInPolyTime.snd (encPair encP encCNF) encNat) + (hN_nat.comp (ComputableTidilyInPolyTime.fst (encPair encP encCNF) encNat)) + unfold validDeclaredCNF; exact ComputableTidilyInPolyTime.bool_and' h1 h2 + +private theorem computableInPolyTime_isEmptyCNF : + ComputableInPolyTime (fun x : P × CNF ℕ => x.2.isEmpty) (encPair encP encCNF) encBool := + .of_tidy ((ComputableTidilyInPolyTime.listIsEmpty' _).comp + (ComputableTidilyInPolyTime.snd encP encCNF)) + +private theorem computableInPolyTime_hasEmptyClause : + ComputableInPolyTime (fun x : P × CNF ℕ => hasEmptyClause x.2) (encPair encP encCNF) encBool := + .of_tidy (by + unfold hasEmptyClause + apply ComputableTidilyInPolyTime.anyWithInput (ComputableTidilyInPolyTime.snd encP encCNF) + exact (ComputableTidilyInPolyTime.listIsEmpty' _).comp + (ComputableTidilyInPolyTime.snd (encPair encP encCNF) _)) + +private theorem computableInPolyTime_twoPowN (hNOf : ComputableInPolyTime NOf encP encUnary) : + ComputableInPolyTime (fun x : P × CNF ℕ => 2 ^ NOf x.1) (encPair encP encCNF) encNat := + ComputableInPolyTime.binary_two_pow.comp (hNOf.comp (by fun_prop)) + +private theorem computableInPolyTime_baseGuard (k : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) : + ComputableInPolyTime (fun x : P × CNF ℕ => + validDeclaredCNF k (NOf x.1) x.2 && !x.2.isEmpty && !hasEmptyClause x.2) + (encPair encP encCNF) encBool := by + have := (computableInPolyTime_validDeclaredCNF k hNOf).tidy + have := (computableInPolyTime_isEmptyCNF (encP := encP)).tidy + have := (computableInPolyTime_hasEmptyClause (encP := encP)).tidy + exact .of_tidy (by fun_prop) + +private theorem computableInPolyTime_entersSparseFastPath (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) + (hBOf : ComputableInPolyTime BOf encP encUnary) : + ComputableInPolyTime + (fun x : P × CNF ℕ => entersSparseFastPath k N₀ (NOf x.1) (BOf x.1) x.2) + (encPair encP encCNF) encBool := by + have := (computableInPolyTime_baseGuard k hNOf).tidy + have hN := hNOf.comp (by fun_prop : ComputableInPolyTime Prod.fst (encPair encP encCNF) encP) + have hB := hBOf.comp (by fun_prop : ComputableInPolyTime Prod.fst (encPair encP encCNF) encP) + have hm := SAT.computableInPolyTime_length + (by fun_prop : ComputableInPolyTime Prod.snd (encPair encP encCNF) encCNF) + have := (by fun_prop : ComputableInPolyTime (fun x : P × CNF ℕ => decide (NOf x.1 < N₀)) + (encPair encP encCNF) encBool).tidy + have := (by fun_prop : ComputableInPolyTime + (fun x : P × CNF ℕ => decide (x.2.length ≤ BOf x.1 * NOf x.1)) + (encPair encP encCNF) encBool).tidy + refine .of_tidy ?_; unfold entersSparseFastPath; fun_prop + +private def nonExhGuard {P : Type*} (NOf : P → ℕ) (k N₀ : ℕ) (x : P × CNF ℕ) : Bool := + !(validDeclaredCNF k (NOf x.1) x.2 && !x.2.isEmpty && !hasEmptyClause x.2 && + decide (NOf x.1 < N₀)) + +private def nonExhDirect {P : Type*} (NOf : P → ℕ) (k : ℕ) (x : P × CNF ℕ) : ℕ := + if validDeclaredCNF k (NOf x.1) x.2 && x.2.isEmpty then 2 ^ NOf x.1 else 0 + +private def sparseCNFNonFastFallback {P : Type*} (NOf : P → ℕ) (k N₀ : ℕ) (x : P × CNF ℕ) : ℕ := + if nonExhGuard NOf k N₀ x then nonExhDirect NOf k x else countCNFExhaustive (NOf x.1, x.2) + +private theorem computableInPolyTime_nonExhGuard (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) : + ComputableInPolyTime (nonExhGuard NOf k N₀) (encPair encP encCNF) encBool := by + have := (computableInPolyTime_baseGuard k hNOf).tidy + have hN := hNOf.comp (by fun_prop : ComputableInPolyTime Prod.fst (encPair encP encCNF) encP) + have := (by fun_prop : ComputableInPolyTime (fun x : P × CNF ℕ => decide (NOf x.1 < N₀)) + (encPair encP encCNF) encBool).tidy + refine .of_tidy ?_; unfold nonExhGuard; fun_prop + +private theorem computableInPolyTime_nonExhDirect (k : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) : + ComputableInPolyTime (nonExhDirect NOf k) (encPair encP encCNF) encNat := + .of_tidy ((ComputableTidilyInPolyTime.bool_and' + (computableInPolyTime_validDeclaredCNF k hNOf).tidy + (computableInPolyTime_isEmptyCNF (encP := encP)).tidy).ite' + (computableInPolyTime_twoPowN hNOf).tidy (ComputableTidilyInPolyTime.const 0)) + +private theorem computableInPolyTime_exhInput (hNOf : ComputableInPolyTime NOf encP encUnary) : + ComputableInPolyTime (fun x : P × CNF ℕ => (NOf x.1, x.2)) + (encPair encP encCNF) (encPair encUnary encCNF) := + (hNOf.comp (by fun_prop)).prod (by fun_prop) + +private noncomputable def nonFastFallbackCertificate (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) : + NativeCertificate (sparseCNFNonFastFallback NOf k N₀) (encPair encP encCNF) encNat := + NativeCertificate.branch + (NativeCertificate.ofPolyTime (computableInPolyTime_nonExhGuard k N₀ hNOf)) + (NativeCertificate.ofPolyTime (computableInPolyTime_nonExhDirect k hNOf)) + (countCNFExhaustiveCertificate.comp + (NativeCertificate.ofPolyTime (computableInPolyTime_exhInput hNOf))) + +private theorem isPolynomial_nonFastFallbackCertificate (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) : + (nonFastFallbackCertificate k N₀ hNOf).IsPolynomial := by + have hDir := NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_nonExhDirect k hNOf) + have hExhIn := NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_exhInput hNOf) + have hExhLen := (computableInPolyTime_exhInput hNOf).polyBounded_length + have hExhSpace := polyBounded_comp_space countCNFExhaustiveCertificate + (NativeCertificate.ofPolyTime (computableInPolyTime_exhInput hNOf)) + polyBounded_countCNFExhaustive_space hExhIn.2 + obtain ⟨P_ex, Q_ex, hP_ex, hQ_ex, hExhT⟩ := exists_countCNFExhaustive_time_le + obtain ⟨hSpace, C, d, hTime⟩ := exists_branch_time_le_of_finite_threshold + (μ := fun x : P × CNF ℕ => NOf x.1) (N₀ := N₀) (P_ex := fun x => P_ex (NOf x.1, x.2)) + (Q_ex := fun x => (NativeCertificate.ofPolyTime (computableInPolyTime_exhInput hNOf)).time x + + Q_ex (NOf x.1, x.2)) + (NativeCertificate.ofPolyTime (computableInPolyTime_nonExhGuard k N₀ hNOf)) + (NativeCertificate.ofPolyTime (computableInPolyTime_nonExhDirect k hNOf)) + (countCNFExhaustiveCertificate.comp + (NativeCertificate.ofPolyTime (computableInPolyTime_exhInput hNOf))) + (NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_nonExhGuard k N₀ hNOf)) + hDir.2 hExhSpace + (fun _ h => by + simp only [nonExhGuard, Bool.not_eq_false', Bool.and_eq_true, decide_eq_true_eq] at h + exact h.2) + (hP_ex.comp hExhLen) (hExhIn.1.add (hQ_ex.comp hExhLen)) + (fun x _ => by + have ht := hExhT (NOf x.1, x.2) + simp only [NativeCertificate.comp_time]; dsimp only at ht ⊢; omega) + refine ⟨(hDir.1.add (PolyBounded.of_forall_le C d fun _ => le_rfl)).mono fun x => ?_, hSpace⟩ + have hx := hTime x; dsimp only [nonFastFallbackCertificate] at hx ⊢; split_ifs at hx <;> omega + +private theorem computableInPolyTime_mbPair (hBOf : ComputableInPolyTime BOf encP encUnary) : + ComputableInPolyTime (fun x : P × CNF ℕ => (x.2.length, BOf x.1)) + (encPair encP encCNF) (encPair encUnary encUnary) := + (SAT.computableInPolyTime_length (by fun_prop)).prod (hBOf.comp (by fun_prop)) + +private def assembleGreedyInput (NOf BOf : P → ℕ) (y : (P × CNF ℕ) × List (List Bool)) : + (ℕ × CNF ℕ) × ℕ × ℕ × ℕ × List (List Bool) := + ((NOf y.1.1, y.1.2), NOf y.1.1, y.1.2.length, greedyRowListLength (BOf y.1.1) y.1.2.length, y.2) + +private theorem computableInPolyTime_assembleGreedyInput + (hNOf : ComputableInPolyTime NOf encP encUnary) + (hBOf : ComputableInPolyTime BOf encP encUnary) : + ComputableInPolyTime (assembleGreedyInput NOf BOf) + (encPair (encPair encP encCNF) (encList encBits)) (encGreedyInput encCandCtx) := by + have hp : ComputableInPolyTime (fun y : (P × CNF ℕ) × List (List Bool) => y.1.1) + (encPair (encPair encP encCNF) (encList encBits)) encP := by fun_prop + have hψ : ComputableInPolyTime (fun y : (P × CNF ℕ) × List (List Bool) => y.1.2) + (encPair (encPair encP encCNF) (encList encBits)) encCNF := by fun_prop + have hN := hNOf.comp hp; have hm := SAT.computableInPolyTime_length hψ + unfold assembleGreedyInput encGreedyInput encGreedyIn encCandCtx + exact (hN.prod hψ).prod (hN.prod (hm.prod + ((greedyRowListLength_polyTime hm (hBOf.comp hp)).prod (by fun_prop)))) + +private def assembleFinalCand (NOf : P → ℕ) (y : (P × CNF ℕ) × List (List Bool)) : + (ℕ × CNF ℕ) × List (List Bool) := ((NOf y.1.1, y.1.2), y.2) + +private theorem computableInPolyTime_assembleFinalCand + (hNOf : ComputableInPolyTime NOf encP encUnary) : + ComputableInPolyTime (assembleFinalCand NOf) + (encPair (encPair encP encCNF) (encList encBits)) encCandIn := by + unfold assembleFinalCand encCandIn encCandCtx + exact ((hNOf.comp (by fun_prop)).prod (by fun_prop)).prod (by fun_prop) + +private def capByTwoPow (NOf : P → ℕ) (y : (P × CNF ℕ) × ℕ) : ℕ := min (2 ^ NOf y.1.1) y.2 + +private theorem computableInPolyTime_capByTwoPow + (hNOf : ComputableInPolyTime NOf encP encUnary) : + ComputableInPolyTime (capByTwoPow NOf) (encPair (encPair encP encCNF) encNat) encNat := by + have h2pow := (computableInPolyTime_twoPowN hNOf).tidy.comp + (ComputableTidilyInPolyTime.fst (encPair encP encCNF) encNat) + have hres := ComputableTidilyInPolyTime.snd (encPair encP encCNF) encNat + refine .of_tidy (((ComputableTidilyInPolyTime.binary_le' h2pow hres).ite' h2pow hres).of_enc_eq + fun y => congrArg encNat ?_) + by_cases h : 2 ^ NOf y.1.1 ≤ y.2 <;> simp [capByTwoPow, h, Nat.le_of_not_le] + +private noncomputable def initRowsCertificate (hBOf : ComputableInPolyTime BOf encP encUnary) : + NativeCertificate (fun x : P × CNF ℕ => initialTestsRows x.2.length (BOf x.1)) + (encPair encP encCNF) (encList encBits) := + let cMB : NativeCertificate (fun p : ℕ × ℕ => initialTestsRows p.1 p.2) + (encPair encUnary encUnary) (encList encBits) := + ⟨fun p => 2 ^ initialTestsRows_computableInO.choose (p.2 + Nat.log 2 (p.1 + 2)), + fun p => initialTestsRows_computableInO.choose_spec.choose (p.1 + p.2), + initialTestsRows_computableInO.choose_spec.choose_spec.2.2⟩ + (cMB.comp (NativeCertificate.ofPolyTime (computableInPolyTime_mbPair hBOf))).congr fun _ => rfl + +private theorem polyBounded_initRowsCertificate_space + (hBOf : ComputableInPolyTime BOf encP encUnary) : + PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) + (initRowsCertificate hBOf).space := by + have hc := NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_mbPair hBOf) + have hsum : PolyBounded (fun p : ℕ × ℕ => (encPair encUnary encUnary p).length) + (fun p => p.1 + p.2) := PolyBounded.self.mono fun p => by + simp only [length_encPair, encUnary_apply, List.length_replicate]; omega + exact hc.2.add (((PolyBounded.of_polynomiallyBounded id + initialTestsRows_computableInO.choose_spec.choose_spec.2.1).comp hsum).comp + (computableInPolyTime_mbPair hBOf).polyBounded_length) + +private noncomputable def cIdPair (encP : P ↪ List Bool) : + NativeCertificate (fun x : P × CNF ℕ => x) (encPair encP encCNF) (encPair encP encCNF) := + NativeCertificate.linear (ComputableInO.of_linear (.of_eq fun _ => rfl)) + +private noncomputable def withInputPost {β γ : Type} {em : β ↪ List Bool} {eo : γ ↪ List Bool} + {f : P × CNF ℕ → β} {g : (P × CNF ℕ) × β → γ} + (c : NativeCertificate f (encPair encP encCNF) em) + (hg : ComputableInPolyTime g (encPair (encPair encP encCNF) em) eo) : + NativeCertificate (fun x => g (x, f x)) (encPair encP encCNF) eo := + ((NativeCertificate.ofPolyTime hg).comp ((cIdPair encP).prod c)).congr fun _ => rfl + +private theorem polyBounded_withInputPost_space {β γ : Type} {em : β ↪ List Bool} + {eo : γ ↪ List Bool} {f : P × CNF ℕ → β} {g : (P × CNF ℕ) × β → γ} + (c : NativeCertificate f (encPair encP encCNF) em) + (hg : ComputableInPolyTime g (encPair (encPair encP encCNF) em) eo) + (hs : PolyBounded (fun x => (encPair encP encCNF x).length) c.space) : + PolyBounded (fun x => (encPair encP encCNF x).length) + (withInputPost (encP := encP) c hg).space := + polyBounded_comp_space _ _ (NativeCertificate.ofPolyTime_isPolynomial hg).2 + (polyBounded_prod_space _ _ PolyBounded.self hs) + +private theorem exists_withInputPost_time {β γ : Type} {em : β ↪ List Bool} + {eo : γ ↪ List Bool} {f : P × CNF ℕ → β} {g : (P × CNF ℕ) × β → γ} + (c : NativeCertificate f (encPair encP encCNF) em) + (hg : ComputableInPolyTime g (encPair (encPair encP encCNF) em) eo) + (hs : PolyBounded (fun x => (encPair encP encCNF x).length) c.space) : + ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ + ∀ x, (withInputPost (encP := encP) c hg).time x ≤ + c.time x + p (encPair encP encCNF x).length := by + have hplen := polyBounded_pair_len (polyBounded_output_of_space c hs) + obtain ⟨pG, hpG, _, hG⟩ := exists_mono_poly + ((NativeCertificate.ofPolyTime_isPolynomial hg).1.comp hplen) + refine ⟨fun L => L + pG L, (by fun_prop : Cslib.PolynomiallyBounded id).add hpG, fun x => ?_⟩ + have hx : (NativeCertificate.ofPolyTime hg).time (x, f x) ≤ pG (encPair encP encCNF x).length := + hG x + change (encPair encP encCNF x).length + c.time x + + (NativeCertificate.ofPolyTime hg).time (x, f x) ≤ + c.time x + ((encPair encP encCNF x).length + pG (encPair encP encCNF x).length); omega + +private noncomputable def fastPathGreedyInCert + (hNOf : ComputableInPolyTime NOf encP encUnary) + (hBOf : ComputableInPolyTime BOf encP encUnary) := + withInputPost (initRowsCertificate (encP := encP) hBOf) + (computableInPolyTime_assembleGreedyInput hNOf hBOf) + +private noncomputable def fastPathFinalCandCert (k : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) := + withInputPost ((greedyBoundedCertificate k cPoly).comp (fastPathGreedyInCert hNOf hBOf)) + (computableInPolyTime_assembleFinalCand hNOf) + +private noncomputable def fastPathCertificate (k : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) : + NativeCertificate (fun x : P × CNF ℕ => sparseCNFFastPath k (NOf x.1) (BOf x.1) polyCounter x.2) + (encPair encP encCNF) encNat := + (withInputPost ((compiledRowCertificate k cPoly).comp (fastPathFinalCandCert k hNOf hBOf cPoly)) + (computableInPolyTime_capByTwoPow hNOf)).congr fun x => by + dsimp only [Function.comp_apply, capByTwoPow, assembleFinalCand, assembleGreedyInput, + sparseCNFFastPath] + +private theorem polyBounded_fastPathGreedyInCert_space + (hNOf : ComputableInPolyTime NOf encP encUnary) + (hBOf : ComputableInPolyTime BOf encP encUnary) : + PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) + (fastPathGreedyInCert hNOf hBOf).space := + polyBounded_withInputPost_space _ _ (polyBounded_initRowsCertificate_space (encP := encP) hBOf) + +private theorem polyBounded_fastPathFinalCandCert_space (k : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (hSpace : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space) : + PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) + (fastPathFinalCandCert k hNOf hBOf cPoly).space := + polyBounded_withInputPost_space _ _ (polyBounded_comp_space _ _ + (polyBounded_greedyBoundedCertificate_space k cPoly hSpace) + (polyBounded_fastPathGreedyInCert_space hNOf hBOf)) + +private theorem polyBounded_fastPathCertificate_space (k : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (hSpace : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space) : + PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) + (fastPathCertificate k hNOf hBOf cPoly).space := + polyBounded_withInputPost_space _ _ (polyBounded_comp_space _ _ + (polyBounded_compiledRowCertificate_space k cPoly hSpace) + (polyBounded_fastPathFinalCandCert_space k hNOf hBOf cPoly hSpace)) + +private theorem fastPath_agrees {k N₀ : ℕ} (x : P × CNF ℕ) + (h : entersSparseFastPath k N₀ (NOf x.1) (BOf x.1) x.2 = true) : + sparseCNFFastPath k (NOf x.1) (BOf x.1) polyCounter x.2 = + sparseCNFDeclaredCounter NOf BOf k N₀ polyCounter x := by + obtain ⟨hv, he, hnil, hge, hmB⟩ := entersSparseFastPath_eq_true_iff.mp h + simp only [sparseCNFDeclaredCounter, hv, he, hnil, decide_eq_false (not_lt.mpr hge), + decide_eq_true hmB, Bool.false_eq_true, ↓reduceIte] + +private theorem nonFastFallback_agrees {k N₀ : ℕ} (x : P × CNF ℕ) + (h : entersSparseFastPath k N₀ (NOf x.1) (BOf x.1) x.2 = false) : + sparseCNFNonFastFallback NOf k N₀ x = sparseCNFDeclaredCounter NOf BOf k N₀ polyCounter x := by + unfold entersSparseFastPath sparseCNFNonFastFallback nonExhGuard nonExhDirect + sparseCNFDeclaredCounter at * + dsimp only at * + cases hv : validDeclaredCNF k (NOf x.1) x.2 <;> cases he : x.2.isEmpty <;> + cases hnil : hasEmptyClause x.2 <;> by_cases hlt : NOf x.1 < N₀ <;> + by_cases hmB : x.2.length ≤ BOf x.1 * NOf x.1 <;> + simp only [hv, he, hnil, hlt, hmB, decide_true, decide_false, Bool.and_true, Bool.and_false, + Bool.not_true, Bool.not_false, Bool.false_eq_true, Bool.true_eq_false, ↓reduceIte] at h ⊢ + +/-- **Native resource certificate for `sparseCNFDeclaredCounter`.** -/ +noncomputable def sparseCNFDeclaredCertificate (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + {polyCounter : PolySys → ℕ} + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) : + NativeCertificate (sparseCNFDeclaredCounter NOf BOf k N₀ polyCounter) + (encPair encP encCNF) encNat := + guardedTargetOfPolyTime (computableInPolyTime_entersSparseFastPath k N₀ hNOf hBOf) + (fastPathCertificate k hNOf hBOf cPoly) (nonFastFallbackCertificate k N₀ hNOf) + fastPath_agrees nonFastFallback_agrees + +/-- **Polynomial workspace of `sparseCNFDeclaredCertificate`.** -/ +theorem polyBounded_sparseCNFDeclaredCertificate_space (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + {polyCounter : PolySys → ℕ} + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (hSpace : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space) : + PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) + (sparseCNFDeclaredCertificate k N₀ hNOf hBOf cPoly).space := by + unfold sparseCNFDeclaredCertificate + exact polyBounded_branch_space _ _ _ + (NativeCertificate.ofPolyTime_isPolynomial + (computableInPolyTime_entersSparseFastPath k N₀ hNOf hBOf)).2 + (polyBounded_fastPathCertificate_space k hNOf hBOf cPoly hSpace) + (isPolynomial_nonFastFallbackCertificate k N₀ hNOf).2 + +private theorem mem_greedyParityRowsAt_or {countSys : List (List Bool) → ℕ} + {m P : ℕ} {initRows : List (List Bool)} {i : ℕ} {r : List Bool} + (hr : r ∈ greedyParityRowsAt countSys m P initRows i) : + r ∈ initRows ∨ (r.length = m ∧ r.count true ≤ P) := by + induction i with + | zero => exact Or.inl hr + | succ i ih => + rw [greedyParityRowsAt_succ, List.mem_append, List.mem_singleton] at hr + exact hr.elim ih fun h => h ▸ Or.inr ⟨length_selectBestTestRow _ _ _ _, + count_true_selectBestTestRow_le _ _ _ _⟩ + +private theorem exists_compiledRowCertificate_bounds (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) : + ∃ pCandOver polySys : ℕ → ℕ, + Cslib.PolynomiallyBounded pCandOver ∧ Cslib.PolynomiallyBounded polySys ∧ + ∀ R, ValidPolyTimeBound encP NOf BOf k N₀ cPoly polySys R → ∀ x : P × CNF ℕ, + entersSparseFastPath k N₀ (NOf x.1) (BOf x.1) x.2 = true → + ∀ rows : List (List Bool), rows.length ≤ 7 * NOf x.1 → + (∀ r ∈ rows, r.length = x.2.length ∧ + r.count true ≤ initialRowWeightBound (BOf x.1) x.2.length) → + (compiledRowCertificate k cPoly).time ((NOf x.1, x.2), rows) ≤ + pCandOver (encPair encP encCNF x).length + R x := by + obtain ⟨pRowG, hpRowG, hmRowG, hRowG⟩ := exists_mono_poly + (NativeCertificate.ofPolyTime_isPolynomial computableInPolyTime_rowLenGuard).1 + obtain ⟨pToSys, hpToSys, hmToSys, hToSys⟩ := exists_mono_poly + (NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_toSysInput k)).1 + obtain ⟨pSysLen, hpSysLen, hmSysLen, hSysLen⟩ := exists_mono_poly + (computableInPolyTime_toSysInput k).polyBounded_length + obtain ⟨pNLen, hpNLen, _, hNLen⟩ := exists_mono_poly + ((hNOf.comp (by fun_prop : ComputableInPolyTime Prod.fst (encPair encP encCNF) encP) + ).polyBounded_length) + let candInBound (L : ℕ) : ℕ := 2 * (2 * pNLen L + L + 2) + (7 * pNLen L) * (2 * L + 1) + 2 + have hcandInBound_poly : Cslib.PolynomiallyBounded candInBound := by + dsimp only [candInBound]; fun_prop + let polySys (L : ℕ) : ℕ := pSysLen (candInBound L) + let pCandOver (L : ℕ) : ℕ := pRowG (candInBound L) + pToSys (candInBound L) + candInBound L + refine ⟨pCandOver, polySys, + ((hpRowG.comp hcandInBound_poly).add (hpToSys.comp hcandInBound_poly)).add hcandInBound_poly, + hpSysLen.comp hcandInBound_poly, fun R hR x hfast rows hrlen hrprops => ?_⟩ + set L := (encPair encP encCNF x).length + obtain ⟨hv, _, _, _, _⟩ := entersSparseFastPath_eq_true_iff.mp hfast + obtain ⟨hw, hsub⟩ := validDeclaredCNF_eq_true_iff.mp hv + have hN_le : NOf x.1 ≤ pNLen L := by + simpa only [Function.comp_apply, encUnary_apply, List.length_replicate, L] using hNLen x + have hψ_le : (encCNF x.2).length ≤ L := by simp only [L, length_encPair]; omega + have hm_le : x.2.length ≤ L := + (show x.2.length ≤ (encCNF x.2).length from by + unfold encCNF + exact SizedListEncoding.length_le (encList (encPair encNat encBool)) x.2).trans hψ_le + have hr_enc : (encList encBits rows).length ≤ (7 * pNLen L) * (2 * L + 1) := + (length_encList_le encBits rows (b := L) fun r hr => by + simpa only [encBits_apply, (hrprops r hr).1] using hm_le).trans + (Nat.mul_le_mul_right (2 * L + 1) (hrlen.trans (Nat.mul_le_mul_left 7 hN_le))) + have hcin : (encCandIn ((NOf x.1, x.2), rows)).length ≤ candInBound L := by + simp only [encCandIn, encCandCtx, length_encPair, encUnary_apply, List.length_replicate, + candInBound]; omega + have hrg := (hRowG ((NOf x.1, x.2), rows)).trans (hmRowG hcin) + unfold compiledRowCertificate guardedTargetOfPolyTime; rw [guardedTargetCertificate_time] + by_cases h6 : rows.length ≤ 6 * NOf x.1 + · simp only [decide_eq_true h6, ↓reduceIte, NativeCertificate.comp_time] + have hts := (hToSys ((NOf x.1, x.2), rows)).trans (hmToSys hcin) + have hsys_len := (hSysLen ((NOf x.1, x.2), rows)).trans (hmSysLen hcin) + have his := isCompiledSparseSystem_compileParitySystemBounded hw hsub h6 + fun r hr => (hrprops r hr).2 + have hpoly_t : cPoly.time (toSysInput k ((NOf x.1, x.2), rows)) ≤ R x := + hR x hfast _ his hsys_len + exact (Nat.add_le_add hrg (Nat.add_le_add hts hpoly_t)).trans (by dsimp only [pCandOver]; omega) + · simp only [decide_eq_false h6, Bool.false_eq_true, ↓reduceIte, NativeCertificate.const_time] + dsimp only [pCandOver]; omega + +/-- **Explicit certificate-level workspace and split-time bounds for +`sparseCNFDeclaredCertificate`.** -/ +theorem exists_sparseCNFDeclaredCertificate_bounds (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + {polyCounter : PolySys → ℕ} + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (hSpace : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space) : + ∃ poly qInit polySys : ℕ → ℕ, + Cslib.PolynomiallyBounded poly ∧ Cslib.PolynomiallyBounded qInit ∧ + Cslib.PolynomiallyBounded polySys ∧ + (∀ x, (sparseCNFDeclaredCertificate k N₀ hNOf hBOf cPoly).space x ≤ + poly (encPair encP encCNF x).length) ∧ + ∀ R, ValidPolyTimeBound encP NOf BOf k N₀ cPoly polySys R → ∀ x, + (sparseCNFDeclaredCertificate k N₀ hNOf hBOf cPoly).time x ≤ + 2 * (sparseCNFTimeBound encP NOf BOf k N₀ poly qInit R x + 1) := by + obtain ⟨pCandOver, polySys, hpCandOver, hpolySys, hCandT⟩ := + exists_compiledRowCertificate_bounds (BOf := BOf) k N₀ hNOf cPoly + obtain ⟨pSp, hpSp, _, hSp⟩ := exists_mono_poly + (polyBounded_sparseCNFDeclaredCertificate_space k N₀ hNOf hBOf cPoly hSpace) + obtain ⟨pGuard, hpGuard, _, hGuard⟩ := exists_mono_poly (NativeCertificate.ofPolyTime_isPolynomial + (computableInPolyTime_entersSparseFastPath k N₀ hNOf hBOf)).1 + obtain ⟨pFall, hpFall, _, hFall⟩ := exists_mono_poly + (isPolynomial_nonFastFallbackCertificate k N₀ hNOf).1 + obtain ⟨pMB, hpMB, _, hMB⟩ := exists_mono_poly + (NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_mbPair hBOf)).1 + let qInit := initialTestsRows_computableInO.choose + have hqInit := initialTestsRows_computableInO.choose_spec.choose_spec.1 + obtain ⟨pAsmG, hpAsmG, hAsmG⟩ := exists_withInputPost_time + (initRowsCertificate (encP := encP) hBOf) (computableInPolyTime_assembleGreedyInput hNOf hBOf) + (polyBounded_initRowsCertificate_space (encP := encP) hBOf) + have hGreedyInSpace := polyBounded_fastPathGreedyInCert_space hNOf hBOf + have hGreedyInLen := polyBounded_output_of_space (fastPathGreedyInCert hNOf hBOf) hGreedyInSpace + have hCandSpace := polyBounded_compiledRowCertificate_space k cPoly hSpace + let hG := computableInO_greedy (compiledRowCertificate k cPoly) hCandSpace + (greedyMaxCellTime k cPoly) (fun a _ hi _ hj => le_greedyMaxCellTime k cPoly a hi hj) + obtain ⟨pGC, hpGC, _, hGC⟩ := exists_mono_poly + ((PolyBounded.of_polynomiallyBounded id hG.choose_spec.1).comp hGreedyInLen) + obtain ⟨pAsmF, hpAsmF, hAsmF⟩ := exists_withInputPost_time + ((greedyBoundedCertificate k cPoly).comp (fastPathGreedyInCert hNOf hBOf)) + (computableInPolyTime_assembleFinalCand hNOf) + (polyBounded_comp_space _ _ (polyBounded_greedyBoundedCertificate_space k cPoly hSpace) + hGreedyInSpace) + obtain ⟨pCap, hpCap, hCap⟩ := exists_withInputPost_time + ((compiledRowCertificate k cPoly).comp (fastPathFinalCandCert k hNOf hBOf cPoly)) + (computableInPolyTime_capByTwoPow hNOf) + (polyBounded_comp_space _ _ hCandSpace + (polyBounded_fastPathFinalCandCert_space k hNOf hBOf cPoly hSpace)) + let poly (L : ℕ) : ℕ := + pSp L + pGuard L + pFall L + pMB L + pAsmG L + pGC L + pAsmF L + pCap L + pCandOver L + have hpoly : Cslib.PolynomiallyBounded poly := + (((((((hpSp.add hpGuard).add hpFall).add hpMB).add hpAsmG).add hpGC).add hpAsmF).add + hpCap).add hpCandOver + refine ⟨poly, qInit, polySys, hpoly, hqInit, hpolySys, + fun x => (hSp x).trans (by dsimp only [poly]; omega), fun R hR x => ?_⟩ + have hg := hGuard x + unfold sparseCNFDeclaredCertificate guardedTargetOfPolyTime sparseCNFTimeBound + rw [guardedTargetCertificate_time] + cases hfast : entersSparseFastPath k N₀ (NOf x.1) (BOf x.1) x.2 + · simp only [hfast, Bool.false_eq_true, ↓reduceIte] + exact (Nat.add_le_add hg (hFall x)).trans (by dsimp only [poly]; omega) + · simp only [hfast, ↓reduceIte] + obtain ⟨hv, he, hnil, _, hmB⟩ := entersSparseFastPath_eq_true_iff.mp hfast + obtain ⟨hN1, _⟩ := pos_of_nonempty_nonnil_valid hv he hnil + have hB1 : 1 ≤ BOf x.1 := by + rcases Nat.eq_zero_or_pos (BOf x.1) with hB0 | hBp + · rw [hB0, Nat.zero_mul] at hmB; omega + · exact hBp + obtain ⟨hinit_len, hinit_rows, _⟩ := initialTestsRows_spec hN1 hB1 hmB + let gIn := assembleGreedyInput NOf BOf (x, initialTestsRows x.2.length (BOf x.1)) + let finalRows := greedyParityRows + (fun r => compiledRowCounter k polyCounter ((NOf x.1, x.2), r)) + (NOf x.1) x.2.length (greedyRowListLength (BOf x.1) x.2.length) + (initialTestsRows x.2.length (BOf x.1)) + have hmax_cell : greedyMaxCellTime k cPoly gIn ≤ + pCandOver (encPair encP encCNF x).length + R x := by + refine listMax_le fun i hi => listMax_le fun _ _ => ?_ + have hi' : i ≤ 3 * NOf x.1 := by + have := List.mem_range.mp hi; dsimp only [gIn, assembleGreedyInput] at this; omega + dsimp only [greedyCellTime, gIn, assembleGreedyInput] + refine hCandT R hR x hfast _ (by + rw [List.length_append, List.length_singleton, length_greedyParityRowsAt] + exact (Nat.add_le_add (Nat.add_le_add hinit_len hi') (le_refl 1)).trans (by omega)) ?_ + intro r hr; rcases List.mem_append.mp hr with hprev | hcand + · exact (mem_greedyParityRowsAt_or hprev).elim (fun h0 => hinit_rows r h0) fun ⟨hrl, hrw⟩ => + ⟨hrl, hrw.trans (greedyRowListLength_le_initialRowWeightBound (BOf x.1) x.2.length)⟩ + · rw [List.mem_singleton.mp hcand] + exact ⟨length_materializeTestRow _ _, + (count_true_materializeTestRow_decodeTestTuple_le _ _ _).trans + (greedyRowListLength_le_initialRowWeightBound (BOf x.1) x.2.length)⟩ + have hfinal_cand_t : (compiledRowCertificate k cPoly).time ((NOf x.1, x.2), finalRows) ≤ + pCandOver (encPair encP encCNF x).length + R x := + hCandT R hR x hfast finalRows + (by + dsimp only [finalRows]; rw [length_greedyParityRows] + exact (Nat.add_le_add_right hinit_len _).trans (by omega)) + fun r hr => (mem_greedyParityRowsAt_or hr).elim (fun h0 => hinit_rows r h0) + fun ⟨hrl, hrw⟩ => + ⟨hrl, hrw.trans (greedyRowListLength_le_initialRowWeightBound (BOf x.1) x.2.length)⟩ + let K := (3 * NOf x.1 + 1) * + (candidateTupleCount x.2.length (greedyRowListLength (BOf x.1) x.2.length) + 1) + have hgreedy_t : (greedyBoundedCertificate k cPoly).time gIn ≤ + K * (poly (encPair encP encCNF x).length + R x) := by + have heq : (greedyBoundedCertificate k cPoly).time gIn = + K * (hG.choose (encGreedyInput encCandCtx gIn).length + + greedyMaxCellTime k cPoly gIn) := by + unfold greedyBoundedCertificate; simp only [hSpace, ↓reduceDIte]; rfl + rw [heq]; refine Nat.mul_le_mul_left K ((Nat.add_le_add (hGC x) hmax_cell).trans ?_) + dsimp only [poly]; omega + have hfinal_absorb : (compiledRowCertificate k cPoly).time ((NOf x.1, x.2), finalRows) ≤ + K * (poly (encPair encP encCNF x).length + R x) := + (hfinal_cand_t.trans (by dsimp only [poly]; omega)).trans + (Nat.le_mul_of_pos_left _ (Nat.mul_pos (Nat.succ_pos _) (Nat.succ_pos _))) + have ht1 : (initRowsCertificate (encP := encP) hBOf).time x ≤ + pMB (encPair encP encCNF x).length + + 2 ^ qInit (BOf x.1 + Nat.log 2 (x.2.length + 2)) := Nat.add_le_add_right (hMB x) _ + have ht2 := (hAsmG x).trans (Nat.add_le_add_right ht1 _) + have ht3 : ((greedyBoundedCertificate k cPoly).comp (fastPathGreedyInCert hNOf hBOf)).time x ≤ + (pMB (encPair encP encCNF x).length + 2 ^ qInit (BOf x.1 + Nat.log 2 (x.2.length + 2)) + + pAsmG (encPair encP encCNF x).length) + + K * (poly (encPair encP encCNF x).length + R x) := by + rw [NativeCertificate.comp_time]; exact Nat.add_le_add ht2 hgreedy_t + have ht4 := (hAsmF x).trans (Nat.add_le_add_right ht3 _) + have ht5 : ((compiledRowCertificate k cPoly).comp + (fastPathFinalCandCert k hNOf hBOf cPoly)).time x ≤ + ((pMB (encPair encP encCNF x).length + 2 ^ qInit (BOf x.1 + Nat.log 2 (x.2.length + 2)) + + pAsmG (encPair encP encCNF x).length + + K * (poly (encPair encP encCNF x).length + R x)) + + pAsmF (encPair encP encCNF x).length) + + K * (poly (encPair encP encCNF x).length + R x) := by + rw [NativeCertificate.comp_time] + dsimp only [Function.comp_apply, assembleFinalCand, assembleGreedyInput] + exact Nat.add_le_add ht4 hfinal_absorb + have ht6 : (fastPathCertificate k hNOf hBOf cPoly).time x ≤ _ := + (hCap x).trans (Nat.add_le_add_right ht5 _) + refine (Nat.add_le_add hg ht6).trans ?_ + dsimp only [K] + generalize 2 ^ qInit (BOf x.1 + Nat.log 2 (x.2.length + 2)) = E_init + generalize (3 * NOf x.1 + 1) * + (candidateTupleCount x.2.length (greedyRowListLength (BOf x.1) x.2.length) + 1) * + (poly (encPair encP encCNF x).length + R x) = T_prod + dsimp only [poly]; omega + +/-- **Split `ComputableInO` time and polynomial-workspace bound for `sparseCNFDeclaredCounter`.** -/ +theorem computableInO_sparseCNFDeclaredCounter (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + {polyCounter : PolySys → ℕ} + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (hSpace : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space) : + ∃ poly qInit polySys : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ + Cslib.PolynomiallyBounded qInit ∧ Cslib.PolynomiallyBounded polySys ∧ + ∀ R, ValidPolyTimeBound encP NOf BOf k N₀ cPoly polySys R → + ComputableInO (sparseCNFDeclaredCounter NOf BOf k N₀ polyCounter) + (encPair encP encCNF) encNat (sparseCNFTimeBound encP NOf BOf k N₀ poly qInit R) + (fun x => poly (encPair encP encCNF x).length) := by + obtain ⟨poly, qInit, polySys, hpoly, hqInit, hpolySys, hS, hT⟩ := + exists_sparseCNFDeclaredCertificate_bounds k N₀ hNOf hBOf cPoly hSpace + exact ⟨poly, qInit, polySys, hpoly, hqInit, hpolySys, fun R hR => + (sparseCNFDeclaredCertificate k N₀ hNOf hBOf cPoly).computes.mono 2 (hT R hR) fun x => + (hS x).trans (by omega)⟩ + +/-! #### Right-Shift Normalization Certificate -/ + +private def shiftAmount (NOf : P → ℕ) (x : P × CNF ℕ) : ℕ := NOf x.1 - x.2.distinctVars.length + +private theorem computableInPolyTime_shiftAmount + (hNOf : ComputableInPolyTime NOf encP encUnary) : + ComputableInPolyTime (shiftAmount NOf) (encPair encP encCNF) encNat := by + refine .of_tidy ?_ + have hN := ComputableTidilyInPolyTime.unary_to_binary.comp + (hNOf.tidy.comp (ComputableTidilyInPolyTime.fst encP encCNF)) + have hnv := ComputableTidilyInPolyTime.unary_to_binary.comp + (SAT.computableInPolyTime_numVars.tidy.comp (ComputableTidilyInPolyTime.snd encP encCNF)) + refine (ComputableTidilyInPolyTime.binary_sub' hN hnv).of_enc_eq fun x => congrArg encNat ?_ + rw [shiftAmount, CNF.length_distinctVars]; rfl + +/-- **Native resource certificate for `normalizeDeclaredLeaf NOf h`**, composing `cLeaf` with +`ComputableInPolyTime.binary_shiftRight` on `NOf x.1 - x.2.distinctVars.length`. -/ +noncomputable def normalizeDeclaredLeafCertificate + (hNOf : ComputableInPolyTime NOf encP encUnary) {h : P × CNF ℕ → ℕ} + (cLeaf : NativeCertificate h (encPair encP encCNF) encNat) : + NativeCertificate (normalizeDeclaredLeaf NOf h) (encPair encP encCNF) encNat := + ((NativeCertificate.ofPolyTime ComputableInPolyTime.binary_shiftRight).comp + (cLeaf.prod (NativeCertificate.ofPolyTime (computableInPolyTime_shiftAmount hNOf)))).congr + fun _ => rfl + +/-- Polynomial workspace preservation for `normalizeDeclaredLeafCertificate`. -/ +theorem polyBounded_normalizeDeclaredLeafCertificate_space + (hNOf : ComputableInPolyTime NOf encP encUnary) {h : P × CNF ℕ → ℕ} + (cLeaf : NativeCertificate h (encPair encP encCNF) encNat) + (hSpace : PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) cLeaf.space) : + PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) + (normalizeDeclaredLeafCertificate hNOf cLeaf).space := by + unfold normalizeDeclaredLeafCertificate + have hSh := NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_shiftAmount hNOf) + have hSr := NativeCertificate.ofPolyTime_isPolynomial ComputableInPolyTime.binary_shiftRight + exact polyBounded_comp_space _ _ hSr.2 (polyBounded_prod_space _ _ hSpace hSh.2) + +/-- Explicit certificate-level workspace and additive polynomial-time overhead bounds for +`normalizeDeclaredLeafCertificate`. -/ +theorem exists_normalizeDeclaredLeafCertificate_bounds + (hNOf : ComputableInPolyTime NOf encP encUnary) {h : P × CNF ℕ → ℕ} + (cLeaf : NativeCertificate h (encPair encP encCNF) encNat) + (hSpace : PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) cLeaf.space) : + ∃ poly : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ + (∀ x, (normalizeDeclaredLeafCertificate hNOf cLeaf).space x ≤ + poly (encPair encP encCNF x).length) ∧ + (∀ x, (normalizeDeclaredLeafCertificate hNOf cLeaf).time x ≤ + cLeaf.time x + poly (encPair encP encCNF x).length) := by + have hNormSpace := polyBounded_normalizeDeclaredLeafCertificate_space hNOf cLeaf hSpace + have hPairLen : PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) + (fun x => (encPair encNat encNat (h x, shiftAmount NOf x)).length) := + ((((PolyBounded.const 2).mul (polyBounded_output_of_space cLeaf hSpace)).add + (computableInPolyTime_shiftAmount hNOf).polyBounded_length).add (.const 2)).mono fun x => by + simp only [length_encPair]; omega + have hShT := (NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_shiftAmount hNOf)).1 + have hSrT := (NativeCertificate.ofPolyTime_isPolynomial + ComputableInPolyTime.binary_shiftRight).1.comp hPairLen + obtain ⟨poly, hpoly, _, hB⟩ := exists_mono_poly ((hNormSpace.add hShT).add hSrT) + refine ⟨poly, hpoly, fun x => by have hx := hB x; omega, fun x => ?_⟩ + have hx := hB x + change cLeaf.time x + + (NativeCertificate.ofPolyTime (computableInPolyTime_shiftAmount hNOf)).time x + + (NativeCertificate.ofPolyTime ComputableInPolyTime.binary_shiftRight).time + (h x, shiftAmount NOf x) ≤ _; omega + +/-- Split `ComputableInO` time and polynomial-workspace bound for `normalizeDeclaredLeaf`. -/ +theorem computableInO_normalizeDeclaredLeaf + (hNOf : ComputableInPolyTime NOf encP encUnary) {h : P × CNF ℕ → ℕ} + (cLeaf : NativeCertificate h (encPair encP encCNF) encNat) + (hSpace : PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) cLeaf.space) : + ∃ poly : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ + ComputableInO (normalizeDeclaredLeaf NOf h) (encPair encP encCNF) encNat + (fun x => cLeaf.time x + poly (encPair encP encCNF x).length) + (fun x => poly (encPair encP encCNF x).length) := by + obtain ⟨poly, hpoly, hS, hT⟩ := exists_normalizeDeclaredLeafCertificate_bounds hNOf cLeaf hSpace + exact ⟨poly, hpoly, (normalizeDeclaredLeafCertificate hNOf cLeaf).computes.mono_le hT hS⟩ + +/-- **Native resource certificate for `sparseCNFLeafCounter`.** -/ +noncomputable def sparseCNFLeafCertificate (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + {polyCounter : PolySys → ℕ} + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) : + NativeCertificate (sparseCNFLeafCounter NOf BOf k N₀ polyCounter) + (encPair encP encCNF) encNat := + (normalizeDeclaredLeafCertificate hNOf + (sparseCNFDeclaredCertificate k N₀ hNOf hBOf cPoly)).congr fun _ => rfl + +/-- **Polynomial workspace of `sparseCNFLeafCertificate`.** -/ +theorem polyBounded_sparseCNFLeafCertificate_space (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + {polyCounter : PolySys → ℕ} + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (hSpace : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space) : + PolyBounded (fun x : P × CNF ℕ => (encPair encP encCNF x).length) + (sparseCNFLeafCertificate k N₀ hNOf hBOf cPoly).space := by + unfold sparseCNFLeafCertificate + exact polyBounded_normalizeDeclaredLeafCertificate_space hNOf _ + (polyBounded_sparseCNFDeclaredCertificate_space k N₀ hNOf hBOf cPoly hSpace) + +/-- **Certificate-level workspace and split-time bounds for `sparseCNFLeafCertificate`.** -/ +theorem exists_sparseCNFLeafCertificate_bounds (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + {polyCounter : PolySys → ℕ} + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (hSpace : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space) : + ∃ poly qInit polySys : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ + Cslib.PolynomiallyBounded qInit ∧ Cslib.PolynomiallyBounded polySys ∧ + (∀ x, (sparseCNFLeafCertificate k N₀ hNOf hBOf cPoly).space x ≤ + poly (encPair encP encCNF x).length) ∧ + ∀ R, ValidPolyTimeBound encP NOf BOf k N₀ cPoly polySys R → ∀ x, + (sparseCNFLeafCertificate k N₀ hNOf hBOf cPoly).time x ≤ + 2 * (sparseCNFTimeBound encP NOf BOf k N₀ poly qInit R x + 1) := by + obtain ⟨pDecl, qInit, polySys, hpDecl, hqInit, hpolySys, _, hDeclT⟩ := + exists_sparseCNFDeclaredCertificate_bounds k N₀ hNOf hBOf cPoly hSpace + obtain ⟨pNorm, hpNorm, hNormS, hNormT⟩ := exists_normalizeDeclaredLeafCertificate_bounds hNOf + (sparseCNFDeclaredCertificate k N₀ hNOf hBOf cPoly) + (polyBounded_sparseCNFDeclaredCertificate_space k N₀ hNOf hBOf cPoly hSpace) + let poly (L : ℕ) : ℕ := pDecl L + pNorm L + refine ⟨poly, qInit, polySys, hpDecl.add hpNorm, hqInit, hpolySys, + fun x => by unfold sparseCNFLeafCertificate; exact (hNormS x).trans (Nat.le_add_left _ _), + fun R hR x => ?_⟩ + have h1 : (sparseCNFLeafCertificate k N₀ hNOf hBOf cPoly).time x ≤ + (sparseCNFDeclaredCertificate k N₀ hNOf hBOf cPoly).time x + + pNorm (encPair encP encCNF x).length := by + unfold sparseCNFLeafCertificate; exact hNormT x + have h2 := hDeclT R hR x + unfold sparseCNFTimeBound at h2 ⊢; dsimp only at h2 ⊢ + cases hfast : entersSparseFastPath k N₀ (NOf x.1) (BOf x.1) x.2 + · simp only [hfast, Bool.false_eq_true, ↓reduceIte] at h2 ⊢; dsimp only [poly]; omega + · simp only [hfast, ↓reduceIte] at h2 ⊢ + have hmul := Nat.mul_le_mul_left ((3 * NOf x.1 + 1) * + (candidateTupleCount x.2.length (greedyRowListLength (BOf x.1) x.2.length) + 1)) + (show pDecl (encPair encP encCNF x).length + R x ≤ + poly (encPair encP encCNF x).length + R x by dsimp only [poly]; omega) + dsimp only [poly] at hmul ⊢; omega + +/-- **Split `ComputableInO` time and polynomial-workspace bound for `sparseCNFLeafCounter`.** -/ +theorem computableInO_sparseCNFLeafCounter (k N₀ : ℕ) + (hNOf : ComputableInPolyTime NOf encP encUnary) (hBOf : ComputableInPolyTime BOf encP encUnary) + {polyCounter : PolySys → ℕ} + (cPoly : NativeCertificate polyCounter (encPair encUnary encSys) encNat) + (hSpace : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space) : + ∃ poly qInit polySys : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ + Cslib.PolynomiallyBounded qInit ∧ Cslib.PolynomiallyBounded polySys ∧ + ∀ R, ValidPolyTimeBound encP NOf BOf k N₀ cPoly polySys R → + ComputableInO (sparseCNFLeafCounter NOf BOf k N₀ polyCounter) + (encPair encP encCNF) encNat (sparseCNFTimeBound encP NOf BOf k N₀ poly qInit R) + (fun x => poly (encPair encP encCNF x).length) := by + obtain ⟨poly, qInit, polySys, hpoly, hqInit, hpolySys, hS, hT⟩ := + exists_sparseCNFLeafCertificate_bounds k N₀ hNOf hBOf cPoly hSpace + exact ⟨poly, qInit, polySys, hpoly, hqInit, hpolySys, fun R hR => + (sparseCNFLeafCertificate k N₀ hNOf hBOf cPoly).computes.mono 2 (hT R hR) fun x => + (hS x).trans (by omega)⟩ + +end Cslib.Complexity.SparseCNFLeafCounter + +end diff --git a/ComplexityTests/SparseCNFLeafCounter.lean b/ComplexityTests/SparseCNFLeafCounter.lean new file mode 100644 index 000000000..805561809 --- /dev/null +++ b/ComplexityTests/SparseCNFLeafCounter.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2026 Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anton Kovsharov +-/ + +module + +public import Complexity.Init +public import Complexity.Computability.PolyTime.CNF.SparseCNFLeafCounter +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain + +/-! +# Kernel-checked tests for `Cslib.Complexity.SparseCNFLeafCounter` + +Concrete `decide` and end-to-end semantic/resource tests for `sparseCNFDeclaredCounter`, +`normalizeDeclaredLeaf`, `sparseCNFLeafCounter`, and their native machine certificates. +-/ + +@[expose] public section + +namespace ComplexityTests.SparseCNFLeafCounter + +open Cslib.BitString Cslib.Complexity Cslib.Complexity.InitialTestsSearch +open Cslib.Complexity.SparseCNFLeafCounter Cslib.GenericRAM +open Cslib.GenericRAM.ExhaustiveCountFallback Cslib.Logic.PL Cslib.Logic.PL.CNF +open Turing.MultiTapeTM + +/-- Runtime parameter pair `(N, B)` encoded in unary. -/ +abbrev encNB : ℕ × ℕ ↪ List Bool := encPair encUnary encUnary + +private abbrev declExh (N₀ : ℕ) (x : (ℕ × ℕ) × CNF ℕ) : ℕ := + sparseCNFDeclaredCounter Prod.fst Prod.snd 3 N₀ countSystemExhaustive x + +private abbrev leafExh (N₀ : ℕ) (x : (ℕ × ℕ) × CNF ℕ) : ℕ := + sparseCNFLeafCounter Prod.fst Prod.snd 3 N₀ countSystemExhaustive x + +/-! ### 1. Degenerate, Unit-Clause, Unused-Variable, and Guard Boundary Cases -/ + +example : declExh 2 ((0, 1), []) = 1 ∧ leafExh 2 ((0, 1), []) = 1 := by decide +example : declExh 2 ((3, 1), []) = 8 ∧ leafExh 2 ((3, 1), []) = 1 := by decide +example : declExh 4 ((1, 1), [[(0, true)]]) = 1 ∧ leafExh 4 ((1, 1), [[(0, true)]]) = 1 := by decide +example : declExh 4 ((3, 1), [[(0, true)]]) = 4 ∧ leafExh 4 ((3, 1), [[(0, true)]]) = 1 := by decide +example : declExh 2 ((0, 1), [[]]) = 0 ∧ leafExh 2 ((0, 1), [[]]) = 0 := by decide +example : declExh 2 ((4, 1), [[(0, true)], []]) = 0 ∧ + leafExh 2 ((4, 1), [[(0, true)], []]) = 0 := by decide +example : declExh 2 ((5, 2), [[(0, true), (1, true), (2, true), (3, true)]]) = 0 := by decide +example : declExh 2 ((2, 2), [[(2, true)]]) = 0 := by decide +example : declExh 2 ((2, 1), [[(0, true)], [(1, true)], [(0, false), (1, false)]]) = 0 ∧ + leafExh 2 ((2, 1), [[(0, true)], [(1, true)], [(0, false), (1, false)]]) = 0 := by decide + +/-! ### 2. Multi-Clause Sparse `3`-CNF Across Fallback, Pipeline Primitives, and Fast Path -/ + +/-- Three-clause `3`-CNF `(x₀ ∨ ¬x₁ ∨ x₂) ∧ (¬x₀ ∨ x₂) ∧ (x₁ ∨ ¬x₂)` (`modelCount = 3`, +`modelCountOn (Finset.range 4) = 6`). -/ +def psi3 : CNF ℕ := + [[(0, true), (1, false), (2, true)], [(0, false), (2, true)], [(1, true), (2, false)]] + +example : psi3.modelCount = 3 := by decide +example : psi3.modelCountOn (Finset.range 4) = 6 := by decide +example : declExh 5 ((4, 1), psi3) = 6 := by decide +example : leafExh 5 ((4, 1), psi3) = 3 := by decide +example : entersSparseFastPath 3 2 4 1 psi3 = true := by decide +example : (initialTestsRows 3 1).length ≤ 12 ∧ ∀ r ∈ initialTestsRows 3 1, r.length = 3 := by decide +example : + let initRows := initialTestsRows 3 1 + let rows := greedyParityRows + (fun r => compiledRowCounter 3 countSystemExhaustive ((4, psi3), r)) 1 3 1 initRows + compiledRowCounter 3 countSystemExhaustive ((4, psi3), rows) = 6 := by decide + +example : declExh 2 ((4, 1), psi3) = 6 := by + have hw : ∀ c ∈ psi3, c.length ≤ 3 := by decide + have hsub : psi3.vars.toFinset ⊆ Finset.range 4 := by decide + rw [declExh, sparseCNFDeclaredCounter_exhaustive_eq_modelCountOn (NOf := Prod.fst) + (BOf := Prod.snd) (p := (4, 1)) hw hsub (Or.inl (by decide))] + decide + +example : leafExh 2 ((4, 1), psi3) = 3 := by + have hw : ∀ c ∈ psi3, c.length ≤ 3 := by decide + have hsub : psi3.vars.toFinset ⊆ Finset.range 4 := by decide + rw [leafExh, sparseCNFLeafCounter_exhaustive_eq_modelCount (NOf := Prod.fst) + (BOf := Prod.snd) (p := (4, 1)) hw hsub (Or.inl (by decide))] + decide + +example (x : (ℕ × ℕ) × CNF ℕ) : + sparseCNFDeclaredCounter Prod.fst Prod.snd 3 2 (fun _ => 999) x ≤ 2 ^ x.1.1 ∧ + sparseCNFLeafCounter Prod.fst Prod.snd 3 2 (fun _ => 999) x ≤ 2 ^ x.2.numVars := + ⟨sparseCNFDeclaredCounter_le_two_pow _ _ _ _ _ x, + sparseCNFLeafCounter_le_two_pow_numVars _ _ _ _ _ x⟩ + +/-! ### 3. Concrete Native Certificate & Split `ComputableInO` Instantiations -/ + +private def CheckSplitComputableInO (f : (ℕ × ℕ) × CNF ℕ → ℕ) : Prop := + ∃ poly qInit polySys : ℕ → ℕ, Cslib.PolynomiallyBounded poly ∧ + Cslib.PolynomiallyBounded qInit ∧ Cslib.PolynomiallyBounded polySys ∧ + ∀ R, ValidPolyTimeBound encNB Prod.fst Prod.snd 3 16 countSystemExhaustiveCertificate + polySys R → + ComputableInO f (encPair encNB encCNF) encNat + (sparseCNFTimeBound encNB Prod.fst Prod.snd 3 16 poly qInit R) + (fun x => poly (encPair encNB encCNF x).length) + +example : CheckSplitComputableInO (declExh 16) ∧ CheckSplitComputableInO (leafExh 16) := + ⟨computableInO_sparseCNFDeclaredCounter 3 16 (by fun_prop) (by fun_prop) + countSystemExhaustiveCertificate polyBounded_countSystemExhaustive_space, + computableInO_sparseCNFLeafCounter 3 16 (by fun_prop) (by fun_prop) + countSystemExhaustiveCertificate polyBounded_countSystemExhaustive_space⟩ + +example : + PolyBounded (fun x : (ℕ × ℕ) × CNF ℕ => (encPair encNB encCNF x).length) + (sparseCNFLeafCertificate (encP := encNB) (NOf := Prod.fst) (BOf := Prod.snd) 3 16 + (by fun_prop) (by fun_prop) countSystemExhaustiveCertificate).space := + polyBounded_sparseCNFLeafCertificate_space 3 16 (by fun_prop) (by fun_prop) + countSystemExhaustiveCertificate polyBounded_countSystemExhaustive_space + +end ComplexityTests.SparseCNFLeafCounter From 49d0c18bfcf273aad3c5151df9ccd526b006c7d0 Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Tue, 27 Oct 2026 11:46:53 +0000 Subject: [PATCH 2/3] refactor(CNF): share validDeclaredInput and normalizeDeclaredLeaf across #1321 and #1334 --- .../FineGrained/CountingSparsification.lean | 51 +------- .../FineGrained/CountingTreeBound.lean | 1 + .../PolyTime/CNF/SparseCNFLeafCounter.lean | 116 ++++++------------ .../CNF/ModelCount/Declared.lean | 47 ++++++- .../FineGrained/CountingTreeBound.lean | 1 + ComplexityTests/SparseCNFLeafCounter.lean | 4 + 6 files changed, 93 insertions(+), 127 deletions(-) diff --git a/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean b/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean index 279d353c2..246d9ab44 100644 --- a/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean +++ b/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Complexity.FineGrained.Exponents +public import Complexity.Logics.Propositional.CNF.ModelCount.Declared public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingSearch public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingPolyTime import Complexity.Computability.Complexity.Problems.SAT.PolyTime @@ -1134,6 +1135,10 @@ theorem exists_computableInO_search_polySpace (hM2 : 2 ≤ M) {k B L_coeff : ℕ section ContextWrapper +open Cslib.Logic.PL.CNF (normalizeDeclaredLeaf normalizeDeclaredLeaf_eq_div + normalizeDeclaredLeaf_eq_modelCount normalizeDeclaredLeaf_le_two_pow_numVars + validDeclaredInput validDeclaredInput_eq_true_iff) + variable {P : Type*} /-- One step of the depth-first search of the counting-sparsification tree carrying an unchanged @@ -1175,52 +1180,6 @@ theorem iterate_stepWith_countingThreshold (MOf : P → ℕ) (K : ℕ) (g : P × | succ r ih => rw [Function.iterate_succ_apply, stepWith_countingThreshold, ih, Function.iterate_succ_apply] -/-- Exact right-shift normalization converting a declared-range leaf count -`ψ.modelCountOn (Finset.range (NOf p))` into the occurring-variable count `ψ.modelCount` -(`= h (p, ψ) >>> (NOf p - ψ.distinctVars.length)`). -/ -def normalizeDeclaredLeaf (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : ℕ := - h x >>> (NOf x.1 - x.2.distinctVars.length) - -theorem normalizeDeclaredLeaf_eq_div (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : - normalizeDeclaredLeaf NOf h x = h x / 2 ^ (NOf x.1 - x.2.numVars) := by - rw [normalizeDeclaredLeaf, Nat.shiftRight_eq_div_pow, CNF.length_distinctVars] - -/-- When `ψ`'s occurring variables lie in `Finset.range (NOf p)` and `h (p, ψ)` equals the -declared-range model count `ψ.modelCountOn (Finset.range (NOf p))`, `normalizeDeclaredLeaf` -recovers the exact occurring-variable count `ψ.modelCount`. -/ -theorem normalizeDeclaredLeaf_eq_modelCount {NOf : P → ℕ} {h : P × CNF ℕ → ℕ} - {p : P} {ψ : CNF ℕ} (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) - (hh : h (p, ψ) = ψ.modelCountOn (Finset.range (NOf p))) : - normalizeDeclaredLeaf NOf h (p, ψ) = ψ.modelCount := by - rw [normalizeDeclaredLeaf_eq_div, hh, - CNF.modelCountOn_eq_mul_modelCount ψ (Finset.range (NOf p)) hsub, Finset.card_range, - Nat.mul_div_right _ (by positivity)] - -/-- When `ψ`'s occurring variables lie in `Finset.range (NOf p)` and `h (p, ψ) ≤ 2 ^ NOf p`, -`normalizeDeclaredLeaf NOf h (p, ψ)` is at most `2 ^ ψ.numVars`. -/ -theorem normalizeDeclaredLeaf_le_two_pow_numVars {NOf : P → ℕ} {h : P × CNF ℕ → ℕ} - {p : P} {ψ : CNF ℕ} (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) - (hh : h (p, ψ) ≤ 2 ^ NOf p) : - normalizeDeclaredLeaf NOf h (p, ψ) ≤ 2 ^ ψ.numVars := by - rw [normalizeDeclaredLeaf_eq_div] - have hle : ψ.numVars ≤ NOf p := by - simpa only [CNF.numVars, Finset.card_range] using Finset.card_le_card hsub - refine Nat.div_le_of_le_mul (hh.trans ?_) - rw [← pow_add, Nat.sub_add_cancel hle] - -/-- Guard checking that every clause of `φ` has width at most `k` and every occurring variable of -`φ` lies in `0, ..., N - 1`. -/ -def validDeclaredInput (k N : ℕ) (φ : CNF ℕ) : Bool := - (φ.all fun c => decide (c.length ≤ k)) && (φ.vars.all fun v => decide (v < N)) - -theorem validDeclaredInput_eq_true_iff {k N : ℕ} {φ : CNF ℕ} : - validDeclaredInput k N φ = true ↔ - (∀ c ∈ φ, c.length ≤ k) ∧ φ.vars.toFinset ⊆ Finset.range N := by - simp only [validDeclaredInput, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq] - refine and_congr_right' ⟨fun h v hv => ?_, fun h v hv => ?_⟩ - · exact Finset.mem_range.mpr (h v (List.mem_toFinset.mp hv)) - · exact Finset.mem_range.mp (h (List.mem_toFinset.mpr hv)) - /-- **Runtime-context counting-sparsification search** (occurring-variable count): run `stepWith (fun q => countingThreshold (MOf q)) K g` for `rounds (BOf p) φ` steps from `(p, init k φ)` and return the accumulated occurring-variable count. -/ diff --git a/Complexity/Computability/Complexity/FineGrained/CountingTreeBound.lean b/Complexity/Computability/Complexity/FineGrained/CountingTreeBound.lean index 3e2e80916..611f2488f 100644 --- a/Complexity/Computability/Complexity/FineGrained/CountingTreeBound.lean +++ b/Complexity/Computability/Complexity/FineGrained/CountingTreeBound.lean @@ -63,6 +63,7 @@ unconditionally at `M = countingThresholdBase K B`. namespace Cslib.Complexity open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification Cslib.Logic.PL.ClauseSet.Sparsification +open Cslib.Logic.PL.CNF (normalizeDeclaredLeaf validDeclaredInput) open Turing.MultiTapeTM namespace CountingSparsify diff --git a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean index 8ab1a7846..2abf69fc3 100644 --- a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean +++ b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean @@ -22,7 +22,6 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain import Mathlib.Data.List.GetD import Mathlib.Tactic.Linarith -import Mathlib.Tactic.Positivity import Mathlib.Tactic.Ring /-! @@ -31,24 +30,23 @@ import Mathlib.Tactic.Ring Implements the deterministic sparse `k`-CNF model-counting algorithm of Section 6.3 (equation (6.4), printed p. 43) of [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] on native multi-tape Turing machines, parameterized over a sparse `𝔽₂` polynomial-system counter: -- **Encoded / machine-certified procedures**: `validDeclaredCNF`, `hasEmptyClause`, and - `entersSparseFastPath` are `ComputableInPolyTime` Boolean guards; `compiledRowCounter`, - `sparseCNFFastPath`, `sparseCNFDeclaredCounter`, `normalizeDeclaredLeaf`, and +- **Encoded procedures**: `Cslib.Logic.PL.CNF.validDeclaredInput`, `hasEmptyClause`, and + `entersSparseFastPath` are `ComputableInPolyTime` guards; `compiledRowCounter`, + `sparseCNFFastPath`, `sparseCNFDeclaredCounter`, `Cslib.Logic.PL.CNF.normalizeDeclaredLeaf`, and `sparseCNFLeafCounter` are certified by `sparseCNFDeclaredCertificate`, `normalizeDeclaredLeafCertificate`, and `sparseCNFLeafCertificate`. -- **Unencoded mathematical specifications**: `IsCompiledSparseSystem`, `sparseCNFTimeBound`, and +- **Unencoded specifications**: `IsCompiledSparseSystem`, `sparseCNFTimeBound`, and `ValidPolyTimeBound` state structural equation invariants and split runtime hypotheses. -- **Total fallback conventions**: `sparseCNFDeclaredCounter` returns `0` when - `validDeclaredCNF k N ψ = false`, when `[] ∈ ψ`, or when `N ≥ N₀` and `ψ.length > B * N`; returns - `2 ^ N` on `ψ = []`; and falls back to `countCNFExhaustive (N, ψ)` (which defaults variable - indices `≥ N` to `false`) when `N < N₀`. `normalizeDeclaredLeaf` shifts right by +- **Total fallbacks**: `sparseCNFDeclaredCounter` returns `0` when `validDeclaredInput = false`, + `[] ∈ ψ`, or `N ≥ N₀ ∧ ψ.length > B * N`; `2 ^ N` on `ψ = []`; and `countCNFExhaustive (N, ψ)` + (defaulting variables `≥ N` to `false`) when `N < N₀`. `normalizeDeclaredLeaf` shifts right by `N - ψ.distinctVars.length` to recover `ψ.modelCount` within `≤ 2 ^ ψ.numVars`. ## Main definitions -* `validDeclaredCNF`, `hasEmptyClause`, `entersSparseFastPath`, `IsCompiledSparseSystem` -* `compiledRowCounter`, `sparseCNFFastPath`, `sparseCNFDeclaredCounter` -* `normalizeDeclaredLeaf`, `sparseCNFLeafCounter`, `sparseCNFTimeBound`, `ValidPolyTimeBound` +* `hasEmptyClause`, `entersSparseFastPath`, `IsCompiledSparseSystem`, `compiledRowCounter` +* `sparseCNFFastPath`, `sparseCNFDeclaredCounter`, `sparseCNFLeafCounter` +* `sparseCNFTimeBound`, `ValidPolyTimeBound` * `sparseCNFDeclaredCertificate`, `normalizeDeclaredLeafCertificate`, `sparseCNFLeafCertificate` ## Main results @@ -57,8 +55,8 @@ native multi-tape Turing machines, parameterized over a sparse `𝔽₂` polynom `commonZeroCount_compileParitySystemBounded_eq_numPassing` * `sparseCNFDeclaredCounter_le_two_pow`, `sparseCNFDeclaredCounter_eq_modelCountOn`, `sparseCNFDeclaredCounter_exhaustive_eq_modelCountOn` -* `normalizeDeclaredLeaf_eq_modelCount`, `sparseCNFLeafCounter_le_two_pow_numVars`, - `sparseCNFLeafCounter_eq_modelCount`, `sparseCNFLeafCounter_exhaustive_eq_modelCount` +* `sparseCNFLeafCounter_le_two_pow_numVars`, `sparseCNFLeafCounter_eq_modelCount`, + `sparseCNFLeafCounter_exhaustive_eq_modelCount` * `polyBounded_sparseCNFDeclaredCertificate_space`, `exists_sparseCNFDeclaredCertificate_bounds`, `computableInO_sparseCNFDeclaredCounter`, `computableInO_normalizeDeclaredLeaf`, `polyBounded_sparseCNFLeafCertificate_space`, `exists_sparseCNFLeafCertificate_bounds`, @@ -66,8 +64,7 @@ native multi-tape Turing machines, parameterized over a sparse `𝔽₂` polynom ## References -* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Section 6.3, equation (6.4), - printed p. 43. +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §6.3, eq. (6.4), p. 43. -/ @[expose] public section @@ -80,26 +77,20 @@ open Cslib.Complexity.InitialTestsSearch Turing.MultiTapeTM /-! ### 1. Guards, Compiled-System Invariant, and Core Definitions -/ -/-- Guard checking clause widths `≤ k` and occurring variables `< N`. -/ -def validDeclaredCNF (k N : ℕ) (ψ : CNF ℕ) : Bool := - (ψ.all fun c => decide (c.length ≤ k)) && (ψ.vars.all fun v => decide (v < N)) - /-- Boolean check for whether `ψ` contains an empty clause `[]`. -/ def hasEmptyClause (ψ : CNF ℕ) : Bool := ψ.any List.isEmpty /-- Guard characterizing inputs `(N, B, ψ)` entering the Section 6.3 parity-test fast path. -/ def entersSparseFastPath (k N₀ N B : ℕ) (ψ : CNF ℕ) : Bool := - validDeclaredCNF k N ψ && !ψ.isEmpty && !hasEmptyClause ψ && + validDeclaredInput k N ψ && !ψ.isEmpty && !hasEmptyClause ψ && !decide (N < N₀) && decide (ψ.length ≤ B * N) -/-- Sparsity, canonicality, degree, and variable-range invariant satisfied by every sparse `𝔽₂` -polynomial system compiled along the Section 6.3 parity-test search. -/ +/-- Sparsity, canonicality, degree, and variable-range invariant for compiled `𝔽₂` systems. -/ def IsCompiledSparseSystem (k N maxEqs maxTerms : ℕ) (sys : List (List (List ℕ))) : Prop := sys.length ≤ maxEqs ∧ ∀ eq ∈ sys, IsCanonicalEquation eq ∧ eq.length ≤ maxTerms ∧ ∀ mon ∈ eq, mon.length ≤ k ∧ ∀ v ∈ mon, v < N -/-- Candidate parity-row counter compiling `(ψ, rows)` via `compileParitySystemBounded k` and -evaluating `polyCounter` at ambient variable count `N` whenever `rows.length ≤ 6 * N`. -/ +/-- Evaluates `polyCounter (N, compileParitySystemBounded k ψ rows)` when `rows.length ≤ 6 * N`. -/ def compiledRowCounter (k : ℕ) (polyCounter : ℕ × List (List (List ℕ)) → ℕ) (q : (ℕ × CNF ℕ) × List (List Bool)) : ℕ := if decide (q.2.length ≤ 6 * q.1.1) then @@ -120,7 +111,7 @@ Returns `0` if invalid, `2 ^ N` on `[]`, `0` if `[] ∈ ψ`, `countCNFExhaustive def sparseCNFDeclaredCounter {P : Type*} (NOf BOf : P → ℕ) (k N₀ : ℕ) (polyCounter : ℕ × List (List (List ℕ)) → ℕ) (x : P × CNF ℕ) : ℕ := let N := NOf x.1; let B := BOf x.1; let ψ := x.2 - if validDeclaredCNF k N ψ then + if validDeclaredInput k N ψ then if ψ.isEmpty then 2 ^ N else if hasEmptyClause ψ then 0 else if decide (N < N₀) then countCNFExhaustive (N, ψ) @@ -128,41 +119,28 @@ def sparseCNFDeclaredCounter {P : Type*} (NOf BOf : P → ℕ) (k N₀ : ℕ) else 0 else 0 -/-- Right-shift normalization converting `ψ.modelCountOn (Finset.range (NOf p))` to -`ψ.modelCount`. -/ -def normalizeDeclaredLeaf {P : Type*} (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : ℕ := - h x >>> (NOf x.1 - x.2.distinctVars.length) - -/-- Normalized Section 6.3 sparse `k`-CNF leaf provider returning `ψ.modelCount` on valid sparse -width-`≤ k` formulas with variables in `Finset.range (NOf p)`. -/ +/-- Normalized Section 6.3 sparse `k`-CNF leaf provider returning `ψ.modelCount` on valid inputs. -/ def sparseCNFLeafCounter {P : Type*} (NOf BOf : P → ℕ) (k N₀ : ℕ) (polyCounter : ℕ × List (List (List ℕ)) → ℕ) (x : P × CNF ℕ) : ℕ := normalizeDeclaredLeaf NOf (sparseCNFDeclaredCounter NOf BOf k N₀ polyCounter) x /-! ### 2. Structural & Semantic Proofs for Guards, Compilation, and Greedy Search -/ -theorem validDeclaredCNF_eq_true_iff {k N : ℕ} {ψ : CNF ℕ} : - validDeclaredCNF k N ψ = true ↔ - (∀ c ∈ ψ, c.length ≤ k) ∧ ψ.vars.toFinset ⊆ Finset.range N := by - simp only [validDeclaredCNF, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq] - exact and_congr_right' ⟨fun h _ hv => Finset.mem_range.mpr (h _ (List.mem_toFinset.mp hv)), - fun h _ hv => Finset.mem_range.mp (h (List.mem_toFinset.mpr hv))⟩ - theorem hasEmptyClause_eq_true_iff {ψ : CNF ℕ} : hasEmptyClause ψ = true ↔ [] ∈ ψ := by simp only [hasEmptyClause, List.any_eq_true, List.isEmpty_iff] exact ⟨fun ⟨_, hc, hnil⟩ => hnil ▸ hc, fun h => ⟨[], h, rfl⟩⟩ theorem entersSparseFastPath_eq_true_iff {k N₀ N B : ℕ} {ψ : CNF ℕ} : entersSparseFastPath k N₀ N B ψ = true ↔ - validDeclaredCNF k N ψ = true ∧ ψ.isEmpty = false ∧ hasEmptyClause ψ = false ∧ + validDeclaredInput k N ψ = true ∧ ψ.isEmpty = false ∧ hasEmptyClause ψ = false ∧ N₀ ≤ N ∧ ψ.length ≤ B * N := by simp only [entersSparseFastPath, Bool.and_eq_true, Bool.not_eq_true', decide_eq_false_iff_not, decide_eq_true_eq, not_lt, and_assoc] private theorem pos_of_nonempty_nonnil_valid {k N : ℕ} {ψ : CNF ℕ} - (hvalid : validDeclaredCNF k N ψ = true) (hne : ψ.isEmpty = false) + (hvalid : validDeclaredInput k N ψ = true) (hne : ψ.isEmpty = false) (hnil : hasEmptyClause ψ = false) : 1 ≤ N ∧ 1 ≤ ψ.length := by - obtain ⟨_, hsub⟩ := validDeclaredCNF_eq_true_iff.mp hvalid + obtain ⟨_, hsub⟩ := validDeclaredInput_eq_true_iff.mp hvalid rcases ψ with _ | ⟨_ | ⟨l, ls⟩, cs⟩ · simp at hne · exact False.elim (Bool.false_ne_true (hnil ▸ hasEmptyClause_eq_true_iff.mpr List.mem_cons_self)) @@ -327,7 +305,8 @@ theorem sparseCNFDeclaredCounter_eq_modelCountOn {P : Type*} {NOf BOf : P → (fun i : Fin sys.length => equationToFinset (NOf p) sys[i])) : sparseCNFDeclaredCounter NOf BOf k N₀ polyCounter (p, ψ) = ψ.modelCountOn (Finset.range (NOf p)) := by - have hvalid : validDeclaredCNF k (NOf p) ψ = true := validDeclaredCNF_eq_true_iff.mpr ⟨hw, hsub⟩ + have hvalid : validDeclaredInput k (NOf p) ψ = true := + validDeclaredInput_eq_true_iff.mpr ⟨hw, hsub⟩ unfold sparseCNFDeclaredCounter; simp only [hvalid, ↓reduceIte] by_cases he : ψ.isEmpty = true · simp only [he, ↓reduceIte]; rw [List.isEmpty_iff.mp he, CNF.modelCountOn_nil, Finset.card_range] @@ -411,30 +390,7 @@ theorem sparseCNFDeclaredCounter_exhaustive_eq_modelCountOn {P : Type*} {NOf BOf countSystemExhaustive_eq_commonZeroCount fun eq heq => ⟨(hsys.2 eq heq).1, fun m hm v hv => ((hsys.2 eq heq).2.2 m hm).2 v hv⟩ -/-! ### 3. Exact Occurring-Support Normalization (`normalizeDeclaredLeaf`) -/ - -theorem normalizeDeclaredLeaf_eq_div {P : Type*} (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : - normalizeDeclaredLeaf NOf h x = h x / 2 ^ (NOf x.1 - x.2.numVars) := by - rw [normalizeDeclaredLeaf, Nat.shiftRight_eq_div_pow, CNF.length_distinctVars] - -/-- `normalizeDeclaredLeaf` recovers `ψ.modelCount` from `ψ.modelCountOn (Finset.range (NOf p))`. -/ -theorem normalizeDeclaredLeaf_eq_modelCount {P : Type*} {NOf : P → ℕ} {h : P × CNF ℕ → ℕ} - {p : P} {ψ : CNF ℕ} (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) - (hh : h (p, ψ) = ψ.modelCountOn (Finset.range (NOf p))) : - normalizeDeclaredLeaf NOf h (p, ψ) = ψ.modelCount := by - rw [normalizeDeclaredLeaf_eq_div, hh, - CNF.modelCountOn_eq_mul_modelCount ψ (Finset.range (NOf p)) hsub, Finset.card_range, - Nat.mul_div_right _ (by positivity)] - -/-- `normalizeDeclaredLeaf` is bounded by `2 ^ ψ.numVars` whenever `h (p, ψ) ≤ 2 ^ NOf p`. -/ -theorem normalizeDeclaredLeaf_le_two_pow_numVars {P : Type*} {NOf : P → ℕ} {h : P × CNF ℕ → ℕ} - {p : P} {ψ : CNF ℕ} (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) - (hh : h (p, ψ) ≤ 2 ^ NOf p) : - normalizeDeclaredLeaf NOf h (p, ψ) ≤ 2 ^ ψ.numVars := by - rw [normalizeDeclaredLeaf_eq_div] - have hle : ψ.numVars ≤ NOf p := by - simpa only [CNF.numVars, Finset.card_range] using Finset.card_le_card hsub - exact Nat.div_le_of_le_mul (hh.trans (by rw [← pow_add, Nat.sub_add_cancel hle])) +/-! ### 3. Normalized Leaf Provider (`sparseCNFLeafCounter`) -/ /-- **Unconditional leaf-accumulator bound**: `sparseCNFLeafCounter` never exceeds `2 ^ ψ.numVars` on any input `(p, ψ)`, regardless of `polyCounter`. -/ @@ -442,8 +398,8 @@ theorem sparseCNFLeafCounter_le_two_pow_numVars {P : Type*} (NOf BOf : P → ℕ (polyCounter : ℕ × List (List (List ℕ)) → ℕ) (x : P × CNF ℕ) : sparseCNFLeafCounter NOf BOf k N₀ polyCounter x ≤ 2 ^ x.2.numVars := by rcases x with ⟨p, ψ⟩ - by_cases hv : validDeclaredCNF k (NOf p) ψ = true - · exact normalizeDeclaredLeaf_le_two_pow_numVars (validDeclaredCNF_eq_true_iff.mp hv).2 + by_cases hv : validDeclaredInput k (NOf p) ψ = true + · exact normalizeDeclaredLeaf_le_two_pow_numVars (validDeclaredInput_eq_true_iff.mp hv).2 (sparseCNFDeclaredCounter_le_two_pow NOf BOf k N₀ polyCounter (p, ψ)) · simp only [Bool.not_eq_true] at hv simp only [sparseCNFLeafCounter, normalizeDeclaredLeaf, sparseCNFDeclaredCounter, hv, @@ -633,9 +589,9 @@ private theorem polyBounded_greedyBoundedCertificate_space (k : ℕ) unfold greedyBoundedCertificate; simp only [hSpace, ↓reduceDIte] rw [heq]; exact PolyBounded.of_polynomiallyBounded _ hG.choose_spec.1 -private theorem computableInPolyTime_validDeclaredCNF (k : ℕ) +private theorem computableInPolyTime_validDeclaredInput (k : ℕ) (hNOf : ComputableInPolyTime NOf encP encUnary) : - ComputableInPolyTime (fun x : P × CNF ℕ => validDeclaredCNF k (NOf x.1) x.2) + ComputableInPolyTime (fun x : P × CNF ℕ => validDeclaredInput k (NOf x.1) x.2) (encPair encP encCNF) encBool := by refine .of_tidy ?_ have hN_nat := ComputableTidilyInPolyTime.unary_to_binary.comp @@ -654,7 +610,7 @@ private theorem computableInPolyTime_validDeclaredCNF (k : ℕ) exact ComputableTidilyInPolyTime.binary_lt' (ComputableTidilyInPolyTime.snd (encPair encP encCNF) encNat) (hN_nat.comp (ComputableTidilyInPolyTime.fst (encPair encP encCNF) encNat)) - unfold validDeclaredCNF; exact ComputableTidilyInPolyTime.bool_and' h1 h2 + unfold validDeclaredInput; exact ComputableTidilyInPolyTime.bool_and' h1 h2 private theorem computableInPolyTime_isEmptyCNF : ComputableInPolyTime (fun x : P × CNF ℕ => x.2.isEmpty) (encPair encP encCNF) encBool := @@ -676,9 +632,9 @@ private theorem computableInPolyTime_twoPowN (hNOf : ComputableInPolyTime NOf en private theorem computableInPolyTime_baseGuard (k : ℕ) (hNOf : ComputableInPolyTime NOf encP encUnary) : ComputableInPolyTime (fun x : P × CNF ℕ => - validDeclaredCNF k (NOf x.1) x.2 && !x.2.isEmpty && !hasEmptyClause x.2) + validDeclaredInput k (NOf x.1) x.2 && !x.2.isEmpty && !hasEmptyClause x.2) (encPair encP encCNF) encBool := by - have := (computableInPolyTime_validDeclaredCNF k hNOf).tidy + have := (computableInPolyTime_validDeclaredInput k hNOf).tidy have := (computableInPolyTime_isEmptyCNF (encP := encP)).tidy have := (computableInPolyTime_hasEmptyClause (encP := encP)).tidy exact .of_tidy (by fun_prop) @@ -702,11 +658,11 @@ private theorem computableInPolyTime_entersSparseFastPath (k N₀ : ℕ) refine .of_tidy ?_; unfold entersSparseFastPath; fun_prop private def nonExhGuard {P : Type*} (NOf : P → ℕ) (k N₀ : ℕ) (x : P × CNF ℕ) : Bool := - !(validDeclaredCNF k (NOf x.1) x.2 && !x.2.isEmpty && !hasEmptyClause x.2 && + !(validDeclaredInput k (NOf x.1) x.2 && !x.2.isEmpty && !hasEmptyClause x.2 && decide (NOf x.1 < N₀)) private def nonExhDirect {P : Type*} (NOf : P → ℕ) (k : ℕ) (x : P × CNF ℕ) : ℕ := - if validDeclaredCNF k (NOf x.1) x.2 && x.2.isEmpty then 2 ^ NOf x.1 else 0 + if validDeclaredInput k (NOf x.1) x.2 && x.2.isEmpty then 2 ^ NOf x.1 else 0 private def sparseCNFNonFastFallback {P : Type*} (NOf : P → ℕ) (k N₀ : ℕ) (x : P × CNF ℕ) : ℕ := if nonExhGuard NOf k N₀ x then nonExhDirect NOf k x else countCNFExhaustive (NOf x.1, x.2) @@ -724,7 +680,7 @@ private theorem computableInPolyTime_nonExhDirect (k : ℕ) (hNOf : ComputableInPolyTime NOf encP encUnary) : ComputableInPolyTime (nonExhDirect NOf k) (encPair encP encCNF) encNat := .of_tidy ((ComputableTidilyInPolyTime.bool_and' - (computableInPolyTime_validDeclaredCNF k hNOf).tidy + (computableInPolyTime_validDeclaredInput k hNOf).tidy (computableInPolyTime_isEmptyCNF (encP := encP)).tidy).ite' (computableInPolyTime_twoPowN hNOf).tidy (ComputableTidilyInPolyTime.const 0)) @@ -941,7 +897,7 @@ private theorem nonFastFallback_agrees {k N₀ : ℕ} (x : P × CNF ℕ) unfold entersSparseFastPath sparseCNFNonFastFallback nonExhGuard nonExhDirect sparseCNFDeclaredCounter at * dsimp only at * - cases hv : validDeclaredCNF k (NOf x.1) x.2 <;> cases he : x.2.isEmpty <;> + cases hv : validDeclaredInput k (NOf x.1) x.2 <;> cases he : x.2.isEmpty <;> cases hnil : hasEmptyClause x.2 <;> by_cases hlt : NOf x.1 < N₀ <;> by_cases hmB : x.2.length ≤ BOf x.1 * NOf x.1 <;> simp only [hv, he, hnil, hlt, hmB, decide_true, decide_false, Bool.and_true, Bool.and_false, @@ -1015,7 +971,7 @@ private theorem exists_compiledRowCertificate_bounds (k N₀ : ℕ) hpSysLen.comp hcandInBound_poly, fun R hR x hfast rows hrlen hrprops => ?_⟩ set L := (encPair encP encCNF x).length obtain ⟨hv, _, _, _, _⟩ := entersSparseFastPath_eq_true_iff.mp hfast - obtain ⟨hw, hsub⟩ := validDeclaredCNF_eq_true_iff.mp hv + obtain ⟨hw, hsub⟩ := validDeclaredInput_eq_true_iff.mp hv have hN_le : NOf x.1 ≤ pNLen L := by simpa only [Function.comp_apply, encUnary_apply, List.length_replicate, L] using hNLen x have hψ_le : (encCNF x.2).length ≤ L := by simp only [L, length_encPair]; omega diff --git a/Complexity/Logics/Propositional/CNF/ModelCount/Declared.lean b/Complexity/Logics/Propositional/CNF/ModelCount/Declared.lean index ef6ad8a2c..70da55527 100644 --- a/Complexity/Logics/Propositional/CNF/ModelCount/Declared.lean +++ b/Complexity/Logics/Propositional/CNF/ModelCount/Declared.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026 Samuel Schlesinger. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Samuel Schlesinger +Authors: Samuel Schlesinger, Anton Kovsharov -/ module @@ -31,6 +31,8 @@ counting development in #1226. They do not implement a counting algorithm or ass ## Main definitions * `Cslib.Logic.PL.CNF.modelCountOn`: count assignments on a declared finite set. +* `Cslib.Logic.PL.CNF.validDeclaredInput`: guard for clause widths `≤ k` and variables `< N`. +* `Cslib.Logic.PL.CNF.normalizeDeclaredLeaf`: right-shift a declared count by unused variables. ## Main results @@ -38,6 +40,9 @@ counting development in #1226. They do not implement a counting algorithm or ass * `Cslib.Logic.PL.CNF.modelCountOn_eq_mul_modelCount`: unused variables give independent choices. * `Cslib.Logic.PL.CNF.vars_dense_relabel`: dense renaming has exactly the expected variable range. * `Cslib.Logic.PL.CNF.modelCountOn_dense_relabel`: dense renaming preserves the declared count. +* `Cslib.Logic.PL.CNF.validDeclaredInput_eq_true_iff`: width and `Finset.range N` equivalence. +* `Cslib.Logic.PL.CNF.normalizeDeclaredLeaf_eq_div`, `normalizeDeclaredLeaf_eq_modelCount`, + `normalizeDeclaredLeaf_le_two_pow_numVars`: division form, `modelCount`, and `2 ^ numVars` bound. -/ @[expose] public section @@ -157,4 +162,44 @@ theorem modelCountOn_dense_relabel (φ : CNF V) : (φ.relabel φ.distinctVars.idxOf).modelCountOn (Finset.range φ.numVars) = φ.modelCount := by rw [← vars_dense_relabel φ, modelCountOn_vars, modelCount_dense_relabel] +/-- Guard checking that every clause of `φ` has width `≤ k` and every variable lies in `< N`. -/ +def validDeclaredInput (k N : ℕ) (φ : CNF ℕ) : Bool := + (φ.all fun c => decide (c.length ≤ k)) && (φ.vars.all fun v => decide (v < N)) + +theorem validDeclaredInput_eq_true_iff {k N : ℕ} {φ : CNF ℕ} : + validDeclaredInput k N φ = true ↔ + (∀ c ∈ φ, c.length ≤ k) ∧ φ.vars.toFinset ⊆ Finset.range N := by + simp only [validDeclaredInput, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq] + exact and_congr_right' ⟨fun h _ hv => Finset.mem_range.mpr (h _ (List.mem_toFinset.mp hv)), + fun h _ hv => Finset.mem_range.mp (h (List.mem_toFinset.mpr hv))⟩ + +/-- Right-shift normalization converting a declared-range count `ψ.modelCountOn (Finset.range N)` +into `ψ.modelCount` (`= h (p, ψ) >>> (NOf p - ψ.distinctVars.length)`). -/ +def normalizeDeclaredLeaf {P : Type*} (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : ℕ := + h x >>> (NOf x.1 - x.2.distinctVars.length) + +theorem normalizeDeclaredLeaf_eq_div {P : Type*} (NOf : P → ℕ) (h : P × CNF ℕ → ℕ) (x : P × CNF ℕ) : + normalizeDeclaredLeaf NOf h x = h x / 2 ^ (NOf x.1 - x.2.numVars) := by + rw [normalizeDeclaredLeaf, Nat.shiftRight_eq_div_pow, length_distinctVars] + +/-- When `ψ`'s variables lie in `Finset.range (NOf p)` and `h (p, ψ)` equals the declared-range +count `ψ.modelCountOn (Finset.range (NOf p))`, `normalizeDeclaredLeaf` recovers `ψ.modelCount`. -/ +theorem normalizeDeclaredLeaf_eq_modelCount {P : Type*} {NOf : P → ℕ} {h : P × CNF ℕ → ℕ} {p : P} + {ψ : CNF ℕ} (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) + (hh : h (p, ψ) = ψ.modelCountOn (Finset.range (NOf p))) : + normalizeDeclaredLeaf NOf h (p, ψ) = ψ.modelCount := by + rw [normalizeDeclaredLeaf_eq_div, hh, modelCountOn_eq_mul_modelCount ψ _ hsub, Finset.card_range, + Nat.mul_div_right _ (Nat.two_pow_pos _)] + +/-- When `ψ`'s variables lie in `Finset.range (NOf p)` and `h (p, ψ) ≤ 2 ^ NOf p`, +`normalizeDeclaredLeaf NOf h (p, ψ)` is at most `2 ^ ψ.numVars`. -/ +theorem normalizeDeclaredLeaf_le_two_pow_numVars {P : Type*} {NOf : P → ℕ} {h : P × CNF ℕ → ℕ} + {p : P} {ψ : CNF ℕ} (hsub : ψ.vars.toFinset ⊆ Finset.range (NOf p)) + (hh : h (p, ψ) ≤ 2 ^ NOf p) : + normalizeDeclaredLeaf NOf h (p, ψ) ≤ 2 ^ ψ.numVars := by + rw [normalizeDeclaredLeaf_eq_div] + have hle : ψ.numVars ≤ NOf p := by + simpa only [numVars, Finset.card_range] using Finset.card_le_card hsub + exact Nat.div_le_of_le_mul (hh.trans (by rw [← pow_add, Nat.sub_add_cancel hle])) + end Cslib.Logic.PL.CNF diff --git a/ComplexityTests/Computability/Complexity/FineGrained/CountingTreeBound.lean b/ComplexityTests/Computability/Complexity/FineGrained/CountingTreeBound.lean index b557337e0..999f6ac9d 100644 --- a/ComplexityTests/Computability/Complexity/FineGrained/CountingTreeBound.lean +++ b/ComplexityTests/Computability/Complexity/FineGrained/CountingTreeBound.lean @@ -19,6 +19,7 @@ public import Complexity.Computability.Complexity.FineGrained.CountingTreeBound namespace Cslib.Complexity.CountingTreeBoundTests open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification Cslib.Logic.PL.ClauseSet.Sparsification +open Cslib.Logic.PL.CNF (normalizeDeclaredLeaf) open Cslib.Complexity.CountingSparsify Turing.MultiTapeTM example : countingDepthCoeff 1 2 = 0 := by decide diff --git a/ComplexityTests/SparseCNFLeafCounter.lean b/ComplexityTests/SparseCNFLeafCounter.lean index 805561809..f38b24e39 100644 --- a/ComplexityTests/SparseCNFLeafCounter.lean +++ b/ComplexityTests/SparseCNFLeafCounter.lean @@ -49,6 +49,10 @@ example : declExh 2 ((5, 2), [[(0, true), (1, true), (2, true), (3, true)]]) = 0 example : declExh 2 ((2, 2), [[(2, true)]]) = 0 := by decide example : declExh 2 ((2, 1), [[(0, true)], [(1, true)], [(0, false), (1, false)]]) = 0 ∧ leafExh 2 ((2, 1), [[(0, true)], [(1, true)], [(0, false), (1, false)]]) = 0 := by decide +example : declExh 2 ((2, 1), [[(0, true)], [(0, true)], [(0, true)]]) = 0 ∧ + leafExh 2 ((2, 1), [[(0, true)], [(0, true)], [(0, true)]]) = 0 := by decide +example : declExh 3 ((2, 1), [[(0, true)], [(0, true)], [(0, true)]]) = 2 ∧ + leafExh 3 ((2, 1), [[(0, true)], [(0, true)], [(0, true)]]) = 1 := by decide /-! ### 2. Multi-Clause Sparse `3`-CNF Across Fallback, Pipeline Primitives, and Fast Path -/ From 18388586880035d095e0c405c2640b22f73f37a5 Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Tue, 27 Oct 2026 12:07:13 +0000 Subject: [PATCH 3/3] feat(PolyTime/CNF): add heavy-branched sparse CNF leaf counter (#1226) --- Complexity.lean | 1 + .../CNF/BranchedSparseCNFCounter.lean | 1182 +++++++++++++++++ .../CNF/BranchedSparseCNFCounter.lean | 147 ++ 3 files changed, 1330 insertions(+) create mode 100644 Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean create mode 100644 ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean diff --git a/Complexity.lean b/Complexity.lean index e67637244..1cddaf7a5 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1386,6 +1386,7 @@ public import Complexity.Computability.PCP.ThreeSAT public import Complexity.Computability.PCP.TwoProverGame public import Complexity.Computability.PolyTime.BitString.InitialTestsSearch public import Complexity.Computability.PolyTime.BooleanAnalysis.SparsePolyCounter +public import Complexity.Computability.PolyTime.CNF.BranchedSparseCNFCounter public import Complexity.Computability.PolyTime.CNF.ClauseJetEval public import Complexity.Computability.PolyTime.CNF.GreedyParityContext public import Complexity.Computability.PolyTime.CNF.GreedyParitySearch diff --git a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean new file mode 100644 index 000000000..483caa0c3 --- /dev/null +++ b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean @@ -0,0 +1,1182 @@ +/- +Copyright (c) 2026 Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anton Kovsharov +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Computability.Complexity.FineGrained.CountingSparsification +public import Complexity.Computability.Complexity.FineGrained.GeneralCNFBranchSchedule +public import Complexity.Computability.Complexity.FineGrained.SparseBranchAsymptotics +public import Complexity.Computability.Complexity.FineGrained.SparseCountingScale +public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Complexity +public import Complexity.Computability.PolyTime.BooleanAnalysis.SparsePolyCounter +public import Complexity.Computability.PolyTime.CNF.SparseCNFLeafCounter +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParametersPolyTime +import all Complexity.Computability.PolyTime.CNF.SparseCNFLeafCounter +import Complexity.Computability.Complexity.Problems.SAT.PolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Complexity.Foundations.Data.List.Counting +import Mathlib.Analysis.Complex.ExponentialBounds +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Heavy-branched sparse `k`-CNF leaf model counter (`BranchedSparseCNFCounter`) + +Connects the heavy-branched sparse `𝔽₂` polynomial-system zero counter `countSparsePolySystem` +(§5.5, Theorem 2.2, pp. 38–39) to `sparseCNFDeclaredCounter` / `normalizeDeclaredLeaf` (§6.3, p. 43) +at the Proposition 6.4 leaf schedule (§6.4, pp. 43–44) of [OpenAI, *The Exponential Time Hypothesis +is False*][OpenAI2026ETH], parameterized solely over `branchEval : BranchEvalInput → ℕ`: + +- **Encoded procedures vs. specification**: `leafDensityRatio` (`encPair encUnit encUnary → + encUnary`) and `branchedPolyCounter`, `branchedSparseCNFDeclaredCounter`, and + `branchedSparseCNFLeafCounter` carry uniform `NativeCertificate` witnesses with global + `PolyBounded` workspace; `BranchPolylogTimeBound` states the unencoded Proposition 5.3 runtime + hypothesis on `cBranch`. +- **Total fallback & exactness**: valid dense formulas (`leafDensityRatio k N * N < ψ.length`, + including `[[]]` at `N = 0`) dispatch to `countCNFExhaustive`, sparse formulas dispatch to + `sparseCNFDeclaredCounter` backed by `branchedPolyCounter`, invalid inputs (`validDeclaredInput = + false`) return `0`, and exactness holds unconditionally on all width-`≤ k` supported CNFs. + +## Main definitions + +* `leafSearchDivisor`, `leafThresholdBase`, `leafOccBound`, `leafDensityRatio` +* `branchedPolyCounter`, `branchedSparseCNFDeclaredCounter`, `branchedSparseCNFLeafCounter` +* `branchedPolyCertificate`, `branchedSparseCNFDeclaredCertificate`, + `branchedSparseCNFLeafCertificate`, `BranchPolylogTimeBound` + +## Main results + +* `leafOccBound_eq_sum`, `leafOccBound_eq_occBound`, `leafDensityRatio_eq_prop64LeafClauseRatio`, + `exists_leafDensityRatio_le_mul_clog_pow`, `computableInPolyTime_leafDensityRatio` +* `branchedSparseCNFDeclaredCounter_le_two_pow`, `branchedSparseCNFLeafCounter_le_two_pow_numVars` +* `branchedPolyCounter_eq_commonZeroCount`, `branchedSparseCNFDeclaredCounter_eq_modelCountOn`, + `branchedSparseCNFLeafCounter_eq_modelCount` +* `polyBounded_branchedSparseCNFDeclaredCertificate_space`, + `polyBounded_branchedSparseCNFLeafCertificate_space` +* `exists_threshold_branchedSparseCNF_time_bound`, `exists_branchedSparseCNF_time_bound` + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §5.4 (Proposition 5.3, + pp. 37–38), §5.5 (Theorem 2.2, pp. 38–39), §6.3 (eq. (6.4), p. 43), §6.4 (Proposition 6.4, + pp. 43–44). +-/ + +namespace Cslib.Complexity.BranchedSparseCNFCounter + +open Finset Cslib.BitString Cslib.Complexity.SparseCNFLeafCounter +open Cslib.Complexity.SubexponentialSAT Cslib.Complexity.SubexponentialSAT.SparsePolyCounter +open Cslib.GenericRAM Cslib.GenericRAM.ExhaustiveCountFallback +open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.ClauseSet.Sparsification +open Turing.MultiTapeTM +open Turing.MultiTapeTM.Universal (encUnit) + +local notation "encSys" => encList (encList (encList encNat)) +local notation "encLeafCtx" => encPair encUnit encUnary +local notation "encLeafIn" => encPair encLeafCtx encCNF + +@[expose] public section + +/-! ### 1. Proposition 6.4 / Section 6.3 Leaf Parameters and Total Counters -/ + +/-- Sparsification search divisor `max 1 ⌊√⌈log₂ N⌉ / ⌈log₂ ⌈log₂ N⌉⌉²⌋` (§6.4, Proposition 6.4). -/ +def leafSearchDivisor (N : ℕ) : ℕ := max 1 (ReplacementParams.numGroups N) + +/-- Appendix A.3 dyadic threshold base `countingThresholdBase (max 2 k) (leafSearchDivisor N)`. -/ +def leafThresholdBase (k N : ℕ) : ℕ := countingThresholdBase (max 2 k) (leafSearchDivisor N) + +/-- Sparse leaf clause-density sum `2 * ∑_{j < max 2 k} (leafThresholdBase k N) ^ j` (§6.4). -/ +def leafOccBound (k N : ℕ) : ℕ := + 2 * ((List.range (max 2 k)).map (leafThresholdBase k N ^ ·)).sum + +/-- Promised sparse leaf clause-to-variable ratio `leafOccBound k N + 1` (§6.3–6.4). -/ +def leafDensityRatio (k N : ℕ) : ℕ := leafOccBound k N + 1 + +/-- Heavy-branched sparse `𝔽₂` polynomial-system zero counter at `mkPaperSparseInput y.1 k y.2`. -/ +def branchedPolyCounter (k N₀_top N₀_branch : ℕ) (branchEval : BranchEvalInput → ℕ) + (y : ℕ × List (List (List ℕ))) : ℕ := + countSparsePolySystem N₀_top N₀_branch branchEval (mkPaperSparseInput y.1 k y.2) + +/-- **Total declared-range sparse `k`-CNF leaf model counter** (§6.3–6.4): dispatches valid dense +formulas (`leafDensityRatio k N * N < ψ.length`, including `[[]]` at `N = 0`) to +`countCNFExhaustive` and sparse formulas (`ψ.length ≤ leafDensityRatio k N * N`) to +`sparseCNFDeclaredCounter` backed by `branchedPolyCounter`. -/ +def branchedSparseCNFDeclaredCounter (k N₀_leaf N₀_top N₀_branch : ℕ) + (branchEval : BranchEvalInput → ℕ) (x : (Unit × ℕ) × CNF ℕ) : ℕ := + let N := x.1.2; let B := leafDensityRatio k N; let ψ := x.2 + if validDeclaredInput k N ψ && decide (B * N < ψ.length) then countCNFExhaustive (N, ψ) + else sparseCNFDeclaredCounter Prod.snd (fun p : Unit × ℕ => leafDensityRatio k p.2) + k (max 1 N₀_leaf) (branchedPolyCounter k N₀_top N₀_branch branchEval) x + +/-- **Total normalized occurring-support sparse `k`-CNF leaf model counter** (§6.3–6.4). -/ +def branchedSparseCNFLeafCounter (k N₀_leaf N₀_top N₀_branch : ℕ) + (branchEval : BranchEvalInput → ℕ) (x : (Unit × ℕ) × CNF ℕ) : ℕ := + normalizeDeclaredLeaf Prod.snd + (branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval) x + +end + +public section + +/-! ### 2. Leaf Parameter Bounds & Unary `ComputableInPolyTime` Certificate -/ + +/-- `leafOccBound k N` equals `2 * ∑ j ∈ Finset.range (max 2 k), leafThresholdBase k N ^ j`. -/ +theorem leafOccBound_eq_sum (k N : ℕ) : + leafOccBound k N = 2 * ∑ j ∈ Finset.range (max 2 k), leafThresholdBase k N ^ j := by + unfold leafOccBound; congr 1 + +/-- `leafOccBound k N` agrees with `CountingSparsify.occBound (max 2 k) (leafThresholdBase k N)`. -/ +theorem leafOccBound_eq_occBound (k N : ℕ) : + leafOccBound k N = CountingSparsify.occBound (max 2 k) (leafThresholdBase k N) := by + rw [leafOccBound_eq_sum]; rfl + +/-- When `1 ≤ ReplacementParams.numGroups N`, `leafDensityRatio` equals `prop64LeafClauseRatio`. -/ +theorem leafDensityRatio_eq_prop64LeafClauseRatio {k N : ℕ} + (hs : 1 ≤ ReplacementParams.numGroups N) : + leafDensityRatio k N = CNF.prop64LeafClauseRatio (max 2 k) N := by + simp only [leafDensityRatio, leafOccBound_eq_sum, leafThresholdBase, leafSearchDivisor, + max_eq_right hs, CNF.prop64LeafClauseRatio, CNF.prop64ThresholdBase] + +/-- `1 ≤ leafDensityRatio k N` for all `k, N : ℕ`. -/ +theorem one_le_leafDensityRatio (k N : ℕ) : 1 ≤ leafDensityRatio k N := Nat.succ_pos _ + +/-- For `1 ≤ N`, `leafOccBound k N * N + 1 ≤ leafDensityRatio k N * N`. -/ +theorem leafOccBound_mul_succ_le_leafDensityRatio_mul {k N : ℕ} (hN : 1 ≤ N) : + leafOccBound k N * N + 1 ≤ leafDensityRatio k N * N := + (Nat.add_le_add_left hN _).trans_eq (by unfold leafDensityRatio; ring) + +/-- **Polylogarithmic leaf clause-density bound (§6.4, Proposition 6.4, p. 44)**: +`∃ C_B, ∀ N ≥ 2, leafDensityRatio k N ≤ C_B * (Nat.clog 2 N) ^ (2 * (max 2 k - 1))`. -/ +theorem exists_leafDensityRatio_le_mul_clog_pow (k : ℕ) : + ∃ C_B : ℕ, ∀ N : ℕ, 2 ≤ N → + leafDensityRatio k N ≤ C_B * (Nat.clog 2 N) ^ (2 * (max 2 k - 1)) := by + obtain ⟨C₀, _, hC₀⟩ := CNF.exists_prop64LeafClauseRatio_le_mul_clog_pow (le_max_left 2 k) + let B₁ := 2 * (∑ j ∈ Finset.range (max 2 k), countingThresholdBase (max 2 k) 1 ^ j) + 1 + refine ⟨max C₀ B₁, fun N hN => ?_⟩ + rcases Nat.eq_zero_or_pos (ReplacementParams.numGroups N) with hs0 | hs_pos + · have h0 : leafDensityRatio k N = B₁ := by + simp only [leafDensityRatio, leafOccBound_eq_sum, leafThresholdBase, leafSearchDivisor, + hs0, max_eq_left (Nat.zero_le 1), B₁] + have hlam1 : 1 ≤ Nat.clog 2 N := + (Nat.lt_clog_iff_pow_lt Nat.one_lt_two).mpr (by omega : 2 ^ 0 < N) + rw [h0]; exact (le_max_right C₀ B₁).trans (Nat.le_mul_of_pos_right _ (Nat.one_le_pow _ _ hlam1)) + · rw [leafDensityRatio_eq_prop64LeafClauseRatio hs_pos] + exact (hC₀ N hN).trans (Nat.mul_le_mul_right _ (le_max_left C₀ B₁)) + +private theorem computableInPolyTime_leafDensityRatio_binary (k : ℕ) : + ComputableInPolyTime (leafDensityRatio k) encNat encNat := by + open ComputableInPolyTime in + have hmax1 : ComputableInPolyTime (fun x : ℕ => max 1 x) encNat encNat := + .of_tidy (((ComputableTidilyInPolyTime.binary_le' (ComputableTidilyInPolyTime.const 1) + ComputableTidilyInPolyTime.id').ite' ComputableTidilyInPolyTime.id' + (ComputableTidilyInPolyTime.const 1)).of_enc_eq fun x => + congrArg encNat (by + split_ifs with hx <;> simp only [decide_eq_true_eq] at hx <;> omega)) + have hM : ComputableInPolyTime (leafThresholdBase k) encNat encNat := + (computableInPolyTime_countingThresholdBase (max 2 k)).comp + (hmax1.comp ParameterCheck.computableInPolyTime_numGroups) + have hgeom (n : ℕ) : + ComputableInPolyTime (fun M : ℕ => ∑ j ∈ Finset.range n, M ^ j) encNat encNat := by + induction n with + | zero => simpa only [Finset.range_zero, Finset.sum_empty] using (const (encIn := encNat) 0) + | succ n ih => + exact (binary_add.comp ((binary_mul' id' ih).prod (const 1))).of_enc_eq fun M => + congrArg encNat (by + dsimp only [Function.comp_apply] + rw [Finset.sum_range_succ', pow_zero, Finset.mul_sum]; simp only [pow_succ']) + have hocc : ComputableInPolyTime (leafOccBound k) encNat encNat := + (binary_mul' (const 2) ((hgeom (max 2 k)).comp hM)).of_enc_eq fun N => + congrArg encNat (leafOccBound_eq_sum k N).symm + exact binary_add.comp (hocc.prod (const 1)) + +private theorem exists_leafDensityRatio_le_poly (k : ℕ) : + ∃ C_u d_u : ℕ, ∀ N : ℕ, leafDensityRatio k N ≤ C_u * (N + 1) ^ d_u := by + obtain ⟨C_B, hCB⟩ := exists_leafDensityRatio_le_mul_clog_pow k + set d_u := 2 * (max 2 k - 1) + set C_u := max C_B (max (leafDensityRatio k 0) (leafDensityRatio k 1)) + refine ⟨C_u, d_u, fun N => ?_⟩ + rcases N with _ | _ | N' + · have h0 : leafDensityRatio k 0 ≤ C_u := + (le_max_left _ (leafDensityRatio k 1)).trans (le_max_right C_B _) + simpa only [Nat.zero_add, one_pow, mul_one] using h0 + · have h1 : leafDensityRatio k 1 ≤ C_u := + (le_max_right (leafDensityRatio k 0) _).trans (le_max_right C_B _) + exact (h1.trans_eq (mul_one C_u).symm).trans + (Nat.mul_le_mul_left C_u (Nat.one_le_pow d_u 2 Nat.zero_lt_two)) + · have hclog_le : Nat.clog 2 (N' + 2) ≤ N' + 2 + 1 := + ((Nat.clog_le_iff_le_pow Nat.one_lt_two).mpr (N' + 2).lt_two_pow_self.le).trans (by omega) + exact (hCB (N' + 2) (by omega)).trans + (Nat.mul_le_mul (le_max_left _ _) (Nat.pow_le_pow_left hclog_le d_u)) + +/-- **Unary `ComputableInPolyTime` certificate for `leafDensityRatio`** on `(Unit × ℕ)` +(`encPair encUnit encUnary → encUnary`), clamping the binary `countingThresholdBase` schedule by its +polynomial unary upper bound via `ComputableInPolyTime.binary_min_unary'`. -/ +theorem computableInPolyTime_leafDensityRatio (k : ℕ) : + ComputableInPolyTime (fun p : Unit × ℕ => leafDensityRatio k p.2) + (encPair encUnit encUnary) encUnary := by + open ComputableInPolyTime in + obtain ⟨C_u, d_u, hCu⟩ := exists_leafDensityRatio_le_poly k + have hN_u : ComputableInPolyTime (fun p : Unit × ℕ => p.2) encLeafCtx encUnary := + snd encUnit encUnary + have hcap_u : ComputableInPolyTime (fun p : Unit × ℕ => C_u * (p.2 + 1) ^ d_u) + encLeafCtx encUnary := + unary_mul' (const C_u) ((unary_pow d_u).comp (unary_add' hN_u (const 1))) + have hval_b : ComputableInPolyTime (fun p : Unit × ℕ => leafDensityRatio k p.2) + encLeafCtx encNat := + (computableInPolyTime_leafDensityRatio_binary k).comp (unary_to_binary.comp hN_u) + exact (binary_min_unary' hcap_u hval_b).of_enc_eq fun p => + congrArg encUnary (Nat.min_eq_right (hCu p.2)).symm + +/-! ### 3. Unconditional Output Caps & Semantic Exactness Across All Width-`≤ k` CNFs -/ + +/-- **Unconditional declared-range output cap**: `branchedSparseCNFDeclaredCounter ≤ 2 ^ x.1.2`. -/ +theorem branchedSparseCNFDeclaredCounter_le_two_pow (k N₀_leaf N₀_top N₀_branch : ℕ) + (branchEval : BranchEvalInput → ℕ) (x : (Unit × ℕ) × CNF ℕ) : + branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval x ≤ 2 ^ x.1.2 := by + unfold branchedSparseCNFDeclaredCounter; dsimp only; split_ifs + · rw [countCNFExhaustive_eq_modelCountOn_range, CNF.modelCountOn] + refine (Finset.card_filter_le _ _).trans ?_ + simp only [Finset.card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_coe, + Finset.card_range, le_rfl] + · exact sparseCNFDeclaredCounter_le_two_pow Prod.snd _ k (max 1 N₀_leaf) _ x + +/-- **Unconditional occurring-support output cap**: +`branchedSparseCNFLeafCounter ≤ 2 ^ x.2.numVars`. -/ +theorem branchedSparseCNFLeafCounter_le_two_pow_numVars (k N₀_leaf N₀_top N₀_branch : ℕ) + (branchEval : BranchEvalInput → ℕ) (x : (Unit × ℕ) × CNF ℕ) : + branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch branchEval x ≤ 2 ^ x.2.numVars := by + rcases x with ⟨p, ψ⟩ + by_cases hv : validDeclaredInput k p.2 ψ = true + · exact normalizeDeclaredLeaf_le_two_pow_numVars (validDeclaredInput_eq_true_iff.mp hv).2 + (branchedSparseCNFDeclaredCounter_le_two_pow k N₀_leaf N₀_top N₀_branch branchEval (p, ψ)) + · simp only [Bool.not_eq_true] at hv + simp only [branchedSparseCNFLeafCounter, normalizeDeclaredLeaf, + branchedSparseCNFDeclaredCounter, sparseCNFDeclaredCounter, hv, Bool.false_and, + Bool.false_eq_true, ↓reduceIte, Nat.zero_shiftRight, Nat.zero_le] + +/-- **Semantic bridge for `branchedPolyCounter` (§5.5 & §6.3)**: under exact feasible branch +evaluation, `branchedPolyCounter` equals `commonZeroCount` on `IsCompiledSparseSystem`. -/ +theorem branchedPolyCounter_eq_commonZeroCount {k N₀_top N₀_branch N maxEqs maxTerms : ℕ} + {branchEval : BranchEvalInput → ℕ} + (hbranch : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) = HeavyBranchFold.rootCount n' eqs') + {sys : List (List (List ℕ))} (hsys : IsCompiledSparseSystem k N maxEqs maxTerms sys) : + branchedPolyCounter k N₀_top N₀_branch branchEval (N, sys) = + commonZeroCount (Finset.univ : Finset (Fin sys.length)) + (fun i : Fin sys.length => equationToFinset N sys[i]) := + countSparsePolySystem_eq_commonZeroCount hbranch (mkPaperSparseInput N k sys) + (fun eq heq => (hsys.2 eq heq).1) (fun eq heq m hm v hv => ((hsys.2 eq heq).2.2 m hm).2 v hv) + +/-- **Unconditional exactness of `branchedSparseCNFDeclaredCounter` (§5.5, §6.3, §6.4)** on all +width-`≤ k` formulas `ψ` with `ψ.vars.toFinset ⊆ Finset.range N`. -/ +theorem branchedSparseCNFDeclaredCounter_eq_modelCountOn {k N₀_leaf N₀_top N₀_branch : ℕ} + {branchEval : BranchEvalInput → ℕ} + (hbranch : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) = HeavyBranchFold.rootCount n' eqs') + (c : Unit) (N : ℕ) (ψ : CNF ℕ) (hw : ∀ cl ∈ ψ, cl.length ≤ k) + (hsub : ψ.vars.toFinset ⊆ Finset.range N) : + branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval ((c, N), ψ) = + ψ.modelCountOn (Finset.range N) := by + have hv : validDeclaredInput k N ψ = true := validDeclaredInput_eq_true_iff.mpr ⟨hw, hsub⟩ + unfold branchedSparseCNFDeclaredCounter; dsimp only + by_cases hgt : leafDensityRatio k N * N < ψ.length + · simp only [hv, decide_eq_true hgt, Bool.and_true, ↓reduceIte] + exact countCNFExhaustive_eq_modelCountOn_range N ψ + · simp only [hv, decide_eq_false hgt, Bool.and_false, Bool.false_eq_true, ↓reduceIte] + exact sparseCNFDeclaredCounter_eq_modelCountOn hw hsub (Or.inl (Nat.le_of_not_lt hgt)) + fun _ _ hsys => branchedPolyCounter_eq_commonZeroCount hbranch hsys + +/-- **Unconditional exactness of `branchedSparseCNFLeafCounter` (§5.5, §6.3, §6.4)** on all +width-`≤ k` formulas `ψ` with `ψ.vars.toFinset ⊆ Finset.range N`. -/ +theorem branchedSparseCNFLeafCounter_eq_modelCount {k N₀_leaf N₀_top N₀_branch : ℕ} + {branchEval : BranchEvalInput → ℕ} + (hbranch : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) = HeavyBranchFold.rootCount n' eqs') + (c : Unit) (N : ℕ) (ψ : CNF ℕ) (hw : ∀ cl ∈ ψ, cl.length ≤ k) + (hsub : ψ.vars.toFinset ⊆ Finset.range N) : + branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch branchEval ((c, N), ψ) = + ψ.modelCount := + normalizeDeclaredLeaf_eq_modelCount hsub + (branchedSparseCNFDeclaredCounter_eq_modelCountOn hbranch c N ψ hw hsub) + +/-- Concrete instantiation of `branchedSparseCNFDeclaredCounter_eq_modelCountOn` with +`countSystemExhaustive`. -/ +theorem branchedSparseCNFDeclaredCounter_exhaustive_eq_modelCountOn + (k N₀_leaf N₀_top N₀_branch : ℕ) (c : Unit) (N : ℕ) (ψ : CNF ℕ) + (hw : ∀ cl ∈ ψ, cl.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) : + branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch + (fun inp => countSystemExhaustive (inp.1.1, inp.2.2.2)) ((c, N), ψ) = + ψ.modelCountOn (Finset.range N) := + branchedSparseCNFDeclaredCounter_eq_modelCountOn + (fun n' eqs' _ => countSystemExhaustive_eq_rootCount n' eqs') c N ψ hw hsub + +/-- Concrete instantiation of `branchedSparseCNFLeafCounter_eq_modelCount` with +`countSystemExhaustive`. -/ +theorem branchedSparseCNFLeafCounter_exhaustive_eq_modelCount + (k N₀_leaf N₀_top N₀_branch : ℕ) (c : Unit) (N : ℕ) (ψ : CNF ℕ) + (hw : ∀ cl ∈ ψ, cl.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) : + branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch + (fun inp => countSystemExhaustive (inp.1.1, inp.2.2.2)) ((c, N), ψ) = + ψ.modelCount := + branchedSparseCNFLeafCounter_eq_modelCount + (fun n' eqs' _ => countSystemExhaustive_eq_rootCount n' eqs') c N ψ hw hsub + +/-! ### 4. Uniform Native Certificates & Global `PolyBounded` Workspace -/ + +private theorem computableInPolyTime_mkPaperInputConst (k : ℕ) : + ComputableInPolyTime (fun y : ℕ × List (List (List ℕ)) => mkPaperSparseInput y.1 k y.2) + (encPair encUnary encSys) encSparseSystemInput := by + have hk : ComputableInPolyTime (fun _ : ℕ × List (List (List ℕ)) => k) + (encPair encUnary encSys) encUnary := .of_tidy (ComputableTidilyInPolyTime.const k) + exact computableInPolyTime_mkPaperSparseInput.comp + (((ComputableInPolyTime.fst encUnary encSys).prod hk).prod + (ComputableInPolyTime.snd encUnary encSys)) + +/-- **Native resource certificate for `branchedPolyCounter` (§5.5).** -/ +noncomputable def branchedPolyCertificate (k N₀_top N₀_branch : ℕ) + {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') : + NativeCertificate (branchedPolyCounter k N₀_top N₀_branch branchEval) + (encPair encUnary encSys) encNat := + ((sparsePolyCounterCertificate N₀_top N₀_branch cBranch hbound).comp + (NativeCertificate.ofPolyTime (computableInPolyTime_mkPaperInputConst k))).congr fun _ => rfl + +/-- Polynomial workspace preservation for `branchedPolyCertificate`. -/ +theorem polyBounded_branchedPolyCertificate_space (k N₀_top N₀_branch : ℕ) + {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') + (hs_br : PolyBounded (fun x => (encBranchEvalInput x).length) cBranch.space) : + PolyBounded (fun y => (encPair encUnary encSys y).length) + (branchedPolyCertificate k N₀_top N₀_branch cBranch hbound).space := by + unfold branchedPolyCertificate + have hmk := computableInPolyTime_mkPaperInputConst k + exact (NativeCertificate.ofPolyTime_isPolynomial hmk).2.add + ((polyBounded_sparsePolyCounterCertificate_space N₀_top N₀_branch cBranch hbound hs_br).comp + hmk.polyBounded_length) + +private def denseFallbackGuard (k : ℕ) (x : (Unit × ℕ) × CNF ℕ) : Bool := + validDeclaredInput k x.1.2 x.2 && decide (leafDensityRatio k x.1.2 * x.1.2 < x.2.length) + +private theorem computableInPolyTime_denseFallbackGuard (k : ℕ) : + ComputableInPolyTime (denseFallbackGuard k) encLeafIn encBool := by + have hN_u : ComputableInPolyTime (fun x : (Unit × ℕ) × CNF ℕ => x.1.2) encLeafIn encUnary := + (ComputableInPolyTime.snd encUnit encUnary).comp (ComputableInPolyTime.fst encLeafCtx encCNF) + have hB_u : ComputableInPolyTime (fun x : (Unit × ℕ) × CNF ℕ => leafDensityRatio k x.1.2) + encLeafIn encUnary := + (computableInPolyTime_leafDensityRatio k).comp (ComputableInPolyTime.fst encLeafCtx encCNF) + have hm_u : ComputableInPolyTime (fun x : (Unit × ℕ) × CNF ℕ => x.2.length) + encLeafIn encUnary := + SAT.computableInPolyTime_length (ComputableInPolyTime.snd encLeafCtx encCNF) + have h1 := + (computableInPolyTime_validDeclaredInput k (ComputableInPolyTime.snd encUnit encUnary)).tidy + have h2 : ComputableTidilyInPolyTime + (fun x : (Unit × ℕ) × CNF ℕ => decide (leafDensityRatio k x.1.2 * x.1.2 < x.2.length)) + encLeafIn encBool := + ComputableTidilyInPolyTime.binary_lt' + (ComputableTidilyInPolyTime.binary_mul' + (ComputableTidilyInPolyTime.unary_to_binary.comp hB_u.tidy) + (ComputableTidilyInPolyTime.unary_to_binary.comp hN_u.tidy)) + (ComputableTidilyInPolyTime.unary_to_binary.comp hm_u.tidy) + exact .of_tidy (ComputableTidilyInPolyTime.bool_and' h1 h2) + +private theorem computableInPolyTime_leafExhProj : + ComputableInPolyTime (fun x : (Unit × ℕ) × CNF ℕ => (x.1.2, x.2)) + encLeafIn (encPair encUnary encCNF) := + ((ComputableInPolyTime.snd encUnit encUnary).comp + (ComputableInPolyTime.fst encLeafCtx encCNF)).prod (ComputableInPolyTime.snd encLeafCtx encCNF) + +/-- **Uniform `NativeCertificate` for `branchedSparseCNFDeclaredCounter`** (§6.3–6.4). -/ +noncomputable def branchedSparseCNFDeclaredCertificate (k N₀_leaf N₀_top N₀_branch : ℕ) + {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') : + NativeCertificate (branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval) + (encPair (encPair encUnit encUnary) encCNF) encNat := + guardedTargetOfPolyTime (computableInPolyTime_denseFallbackGuard k) + (countCNFExhaustiveCertificate.comp + (NativeCertificate.ofPolyTime computableInPolyTime_leafExhProj)) + (sparseCNFDeclaredCertificate k (max 1 N₀_leaf) (ComputableInPolyTime.snd encUnit encUnary) + (computableInPolyTime_leafDensityRatio k) + (branchedPolyCertificate k N₀_top N₀_branch cBranch hbound)) + (fun x h => by + simp only [Function.comp_apply, branchedSparseCNFDeclaredCounter, denseFallbackGuard] at h ⊢ + simp only [h, ↓reduceIte]) + (fun x h => by + simp only [branchedSparseCNFDeclaredCounter, denseFallbackGuard] at h ⊢ + simp only [h, Bool.false_eq_true, ↓reduceIte]) + +/-- **Uniform `NativeCertificate` for `branchedSparseCNFLeafCounter`** (§6.3–6.4). -/ +noncomputable def branchedSparseCNFLeafCertificate (k N₀_leaf N₀_top N₀_branch : ℕ) + {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') : + NativeCertificate (branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch branchEval) + (encPair (encPair encUnit encUnary) encCNF) encNat := + (normalizeDeclaredLeafCertificate (ComputableInPolyTime.snd encUnit encUnary) + (branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound)).congr + fun _ => rfl + +/-- **Global `PolyBounded` workspace for `branchedSparseCNFDeclaredCertificate`.** -/ +theorem polyBounded_branchedSparseCNFDeclaredCertificate_space (k N₀_leaf N₀_top N₀_branch : ℕ) + {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') + (hs_br : PolyBounded (fun x => (encBranchEvalInput x).length) cBranch.space) : + PolyBounded (fun x : (Unit × ℕ) × CNF ℕ => + (encPair (encPair encUnit encUnary) encCNF x).length) + (branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).space := by + unfold branchedSparseCNFDeclaredCertificate + have hpr := NativeCertificate.ofPolyTime_isPolynomial computableInPolyTime_leafExhProj + exact polyBounded_branch_space _ _ _ + (NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_denseFallbackGuard k)).2 + (hpr.2.add (polyBounded_countCNFExhaustive_space.comp + computableInPolyTime_leafExhProj.polyBounded_length)) + (polyBounded_sparseCNFDeclaredCertificate_space k (max 1 N₀_leaf) + (ComputableInPolyTime.snd encUnit encUnary) (computableInPolyTime_leafDensityRatio k) + (branchedPolyCertificate k N₀_top N₀_branch cBranch hbound) + (polyBounded_branchedPolyCertificate_space k N₀_top N₀_branch cBranch hbound hs_br)) + +/-- **Global `PolyBounded` workspace for `branchedSparseCNFLeafCertificate`.** -/ +theorem polyBounded_branchedSparseCNFLeafCertificate_space (k N₀_leaf N₀_top N₀_branch : ℕ) + {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') + (hs_br : PolyBounded (fun x => (encBranchEvalInput x).length) cBranch.space) : + PolyBounded (fun x : (Unit × ℕ) × CNF ℕ => + (encPair (encPair encUnit encUnary) encCNF x).length) + (branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).space := + polyBounded_normalizeDeclaredLeafCertificate_space + (ComputableInPolyTime.snd encUnit encUnary) _ + (polyBounded_branchedSparseCNFDeclaredCertificate_space k N₀_leaf N₀_top N₀_branch + cBranch hbound hs_br) + +/-! ### 5. Fast-Regime `2 ^ {O_k(interpolationScale N)}` Runtime Envelope (§5.5, §6.3, §6.4) -/ + +/-- **Proposition 5.3 per-branch subexponential runtime hypothesis (`BranchPolylogTimeBound`)**: +for every degree cap `k_deg`, polylogarithmic exponent `β`, and prefactor `C_inc`, above a constant +threshold `N₀_br`, every feasible reduced branch `(n', sys')` with `sysMaxDegree sys' ≤ k_deg`, +`sys'.length ≤ C_inc * n'`, and neutral-augmented incidence and scope width +`≤ C_inc * ⌈log₂ n'⌉ ^ β` runs in at most +`C_br * (|enc (n', sys')| + 1) ^ d_br * 2 ^ (A_br * interpolationScale n')` steps. -/ +def BranchPolylogTimeBound (N₀_branch : ℕ) {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) : Prop := + ∀ k_deg β C_inc : ℕ, ∃ N₀_br C_br d_br A_br : ℕ, + ∀ n' : ℕ, ∀ sys' : List (List (List ℕ)), + checkBranchFeasible N₀_branch (n', sys') = true → N₀_br ≤ n' → + sysMaxDegree sys' ≤ k_deg → + sys'.length ≤ C_inc * n' → + branchMaxFactorIncidence n' sys' ≤ C_inc * Nat.clog 2 n' ^ β → + branchMaxFactorWidth n' sys' ≤ C_inc * Nat.clog 2 n' ^ β → + (cBranch.time (prepareBranchEvalInput (n', sys')) : ℝ) ≤ + (C_br : ℝ) * ((encPair encUnary encSys (n', sys')).length + 1 : ℝ) ^ d_br * + (2 : ℝ) ^ ((A_br : ℝ) * interpolationScale n') + +private theorem interpolationScale_le_two_mul_of_le_two_mul {n' N : ℕ} + (hn'_le : n' ≤ N) (hN_le : N ≤ 2 * n') : + interpolationScale n' ≤ 2 * interpolationScale N := by + rcases Nat.eq_zero_or_pos n' with rfl | hn'_pos + · simp only [interpolationScale_zero]; linarith [interpolationScale_nonneg N] + have h1_lt : 1 < Real.log ((n' : ℝ) + 16) := by + rw [← Real.log_exp 1] + exact Real.log_lt_log (Real.exp_pos 1) + (by linarith [Real.exp_one_lt_d9, (Nat.cast_nonneg n' : (0 : ℝ) ≤ n')]) + have hX'_pos : 0 < Real.log ((n' : ℝ) + 16) := zero_lt_one.trans h1_lt + have hX'_le_X : Real.log ((n' : ℝ) + 16) ≤ Real.log ((N : ℝ) + 16) := + Real.log_le_log (by positivity) (by linarith [show (n' : ℝ) ≤ N from Nat.cast_le.mpr hn'_le]) + have hX_pos : 0 < Real.log ((N : ℝ) + 16) := hX'_pos.trans_le hX'_le_X + have hL_sq : Real.log (Real.log ((n' : ℝ) + 16)) ^ 2 ≤ + Real.log (Real.log ((N : ℝ) + 16)) ^ 2 := + pow_le_pow_left₀ (Real.log_pos h1_lt).le (Real.log_le_log hX'_pos hX'_le_X) 2 + have hX_le_4 : Real.log ((N : ℝ) + 16) ≤ (2 : ℝ) ^ 2 * Real.log ((n' : ℝ) + 16) := by + have hN_sq : (N : ℝ) + 16 ≤ ((n' : ℝ) + 16) ^ 2 := by + have : (N : ℝ) ≤ 2 * (n' : ℝ) := by exact_mod_cast hN_le + nlinarith [sq_nonneg (n' : ℝ)] + have hlog := Real.log_le_log (by positivity) hN_sq + rw [Real.log_pow, Nat.cast_ofNat] at hlog; linarith + have hsqrt_le : Real.sqrt (Real.log ((N : ℝ) + 16)) ≤ + 2 * Real.sqrt (Real.log ((n' : ℝ) + 16)) := + (Real.sqrt_le_sqrt hX_le_4).trans_eq + (by rw [Real.sqrt_mul (sq_nonneg (2 : ℝ)), Real.sqrt_sq zero_le_two]) + have hsX' : 0 < Real.sqrt (Real.log ((n' : ℝ) + 16)) := Real.sqrt_pos.mpr hX'_pos + have hsX : 0 < Real.sqrt (Real.log ((N : ℝ) + 16)) := Real.sqrt_pos.mpr hX_pos + unfold interpolationScale + rw [mul_div_assoc', div_le_div_iff₀ hsX' hsX] + have hmul := mul_le_mul + (mul_le_mul (Nat.cast_le.mpr hn'_le) hL_sq (by positivity) (Nat.cast_nonneg N)) + hsqrt_le hsX.le (by positivity) + linarith + +private theorem scopeWidthOn_le_mul (N k maxTerms : ℕ) (eq : List (List ℕ)) + (hlen : eq.length ≤ maxTerms) (hdeg : ∀ m ∈ eq, m.length ≤ k) : + scopeWidthOn N eq ≤ maxTerms * k := by + have hsub : ((List.range N).filter fun u => eq.any fun m => decide (u ∈ m)).toFinset ⊆ + (eq.flatMap id).toFinset := fun u hu => by + simp only [List.mem_toFinset, List.mem_filter, List.any_eq_true, decide_eq_true_eq, + List.mem_flatMap, id_eq] at hu ⊢ + exact hu.2 + calc scopeWidthOn N eq + = (((List.range N).filter fun u => eq.any fun m => decide (u ∈ m)).toFinset).card := by + rw [scopeWidthOn, List.countP_eq_length_filter, + List.toFinset_card_of_nodup (List.nodup_range.filter _)] + _ ≤ (eq.flatMap id).toFinset.card := Finset.card_le_card hsub + _ ≤ (eq.flatMap id).length := List.toFinset_card_le _ + _ ≤ eq.length * k := List.length_flatMap_le hdeg + _ ≤ maxTerms * k := Nat.mul_le_mul_right k hlen + +private theorem foldl_max_le_of_forall {l : List ℕ} {init B : ℕ} (hi : init ≤ B) + (hl : ∀ x ∈ l, x ≤ B) : l.foldl max init ≤ B := by + induction l generalizing init with + | nil => exact hi + | cons a as ih => + exact ih (max_le hi (hl a List.mem_cons_self)) fun x hx => hl x (List.mem_cons_of_mem a hx) + +private theorem compiled_system_incidence_bounds (k C_B β_B : ℕ) : + ∃ C_inc : ℕ, 12 ≤ C_inc ∧ ∀ {N m B : ℕ} {sys : List (List (List ℕ))}, + 2 ≤ N → B ≤ C_B * Nat.clog 2 N ^ β_B → m ≤ B * N → + IsCompiledSparseSystem k N (6 * N) (initialRowWeightBound B m * 2 ^ k) sys → + let inp := mkPaperSparseInput N k sys + inp.2.1.2.2 + 1 ≤ C_inc * Nat.clog 2 N ^ (2 * β_B + 4) ∧ + branchMaxFactorWidth N sys ≤ C_inc * Nat.clog 2 N ^ (2 * β_B + 4) := by + set K_W := CNF.initialRowWeightCoeff C_B β_B + set C_inc := 6 * k * 2 ^ k * K_W + 12 + refine ⟨C_inc, by dsimp only [C_inc]; omega, fun {N m B sys} hN2 hB hm hsys => ?_⟩ + set lam := Nat.clog 2 N + have hlam1 : 1 ≤ lam := (Nat.lt_clog_iff_pow_lt Nat.one_lt_two).mpr (by omega : 2 ^ 0 < N) + have hcz : ¬ Nat.clog 2 N = 0 := by omega + have hW_le : initialRowWeightBound B m ≤ K_W * lam ^ (2 * β_B + 3) := + CNF.initialRowWeightBound_le_mul_pow_clog hN2 hm hB + set T := initialRowWeightBound B m * 2 ^ k * k + have hsc_all : ∀ eq ∈ sys, scopeWidthOn N eq ≤ T := fun eq heq => + scopeWidthOn_le_mul N k (initialRowWeightBound B m * 2 ^ k) eq (hsys.2 eq heq).2.1 + fun mon hmon => ((hsys.2 eq heq).2.2 mon hmon).1 + have hT_le : T ≤ (k * 2 ^ k * K_W) * lam ^ (2 * β_B + 3) := by + calc T = k * 2 ^ k * initialRowWeightBound B m := by dsimp only [T]; ring + _ ≤ k * 2 ^ k * (K_W * lam ^ (2 * β_B + 3)) := Nat.mul_le_mul_left _ hW_le + _ = (k * 2 ^ k * K_W) * lam ^ (2 * β_B + 3) := by ring + have hpow1 : 1 ≤ lam ^ (2 * β_B + 4) := Nat.one_le_pow _ lam hlam1 + have hpow_step : lam ^ (2 * β_B + 3) ≤ lam ^ (2 * β_B + 4) := + Nat.pow_le_pow_right hlam1 (by omega) + have hw_le : branchMaxFactorWidth N sys ≤ C_inc * lam ^ (2 * β_B + 4) := by + unfold branchMaxFactorWidth + refine foldl_max_le_of_forall (Nat.mul_pos (by dsimp only [C_inc]; omega) hpow1) fun w hw => ?_ + obtain ⟨eq, heq, rfl⟩ := List.mem_map.mp hw + have h1 := (hsc_all eq heq).trans (hT_le.trans (Nat.mul_le_mul_left _ hpow_step)) + dsimp only [C_inc]; nlinarith + have hsum_le : (sys.map (scopeWidthOn N)).sum ≤ (6 * T) * N := by + calc (sys.map (scopeWidthOn N)).sum + ≤ (sys.map fun _ => T).sum := List.sum_le_sum fun eq heq => hsc_all eq heq + _ = sys.length * T := by rw [List.map_const', List.sum_replicate_nat] + _ ≤ (6 * T) * N := (Nat.mul_le_mul_right T hsys.1).trans_eq (by ring) + set M := branchAugmentedIncidence N sys + have hdiv_M : (M + N - 1) / N ≤ 6 * T + 2 := + Nat.div_le_of_le_mul ((Nat.sub_le (M + N) 1).trans + (by change (sys.map (scopeWidthOn N)).sum + N + N ≤ N * (6 * T + 2); nlinarith)) + have hcut_le : ParameterCheck.heavyIncidenceCutoff M N ≤ (6 * T + 2) * lam := by + unfold ParameterCheck.heavyIncidenceCutoff; simp only [hcz, ↓reduceIte] + have hsq : (Nat.clog 2 N - 1).sqrt + 1 ≤ lam := by + change (lam - 1).sqrt + 1 ≤ lam; have := Nat.sqrt_le_self (lam - 1); omega + exact Nat.mul_le_mul hdiv_M hsq + have hb0_le : max 1 (ParameterCheck.heavyIncidenceCutoff M N) + 1 ≤ + C_inc * lam ^ (2 * β_B + 4) := by + have hp3 : 1 ≤ lam ^ (2 * β_B + 3) := Nat.one_le_pow _ lam hlam1 + have h6T : (6 * T + 2) * lam ≤ (6 * k * 2 ^ k * K_W + 2) * lam ^ (2 * β_B + 4) := + (Nat.mul_le_mul_right lam + (show 6 * T + 2 ≤ (6 * (k * 2 ^ k * K_W) + 2) * lam ^ (2 * β_B + 3) by nlinarith)).trans_eq + (by rw [pow_succ]; ring) + have h1 : max 1 (ParameterCheck.heavyIncidenceCutoff M N) + 1 ≤ (6 * T + 2) * lam + 1 := + Nat.add_le_add_right (max_le (show 1 ≤ (6 * T + 2) * lam by nlinarith) hcut_le) 1 + dsimp only [C_inc]; nlinarith + exact ⟨hb0_le, hw_le⟩ + +private theorem nat_poly_le_subexp {t C L d d_max : ℕ} {A X : ℝ} + (ht : t ≤ C * (L + 1) ^ d) (hd : d ≤ d_max) (hA : 0 ≤ A) (hX : 0 ≤ X) : + (t : ℝ) ≤ (C : ℝ) * (L + 1 : ℝ) ^ d_max * (2 : ℝ) ^ (A * X) := by + have hc : (t : ℝ) ≤ (C : ℝ) * (L + 1 : ℝ) ^ d_max := by + exact_mod_cast ht.trans (Nat.mul_le_mul_left C (Nat.pow_le_pow_right (Nat.succ_pos L) hd)) + exact (hc.trans_eq (mul_one _).symm).trans + (mul_le_mul_of_nonneg_left (Real.one_le_rpow one_le_two (mul_nonneg hA hX)) (by positivity)) + +private theorem ceil_subexp_le {C L d d_max : ℕ} {A X : ℝ} + (hd : d ≤ d_max) (hA : 0 ≤ A) (hX : 0 ≤ X) : + (⌈((C : ℕ) : ℝ) * (L + 1 : ℝ) ^ d * (2 : ℝ) ^ (A * X)⌉₊ : ℝ) ≤ + ((C + 1 : ℕ) : ℝ) * (L + 1 : ℝ) ^ d_max * (2 : ℝ) ^ (A * X) := by + have hbase : (1 : ℝ) ≤ (L + 1 : ℝ) := by exact_mod_cast Nat.succ_pos L + have hd_le : (L + 1 : ℝ) ^ d ≤ (L + 1 : ℝ) ^ d_max := pow_le_pow_right₀ hbase hd + have htwo : (1 : ℝ) ≤ (2 : ℝ) ^ (A * X) := Real.one_le_rpow one_le_two (mul_nonneg hA hX) + have hceil := (Nat.ceil_lt_add_one + (by positivity : 0 ≤ ((C : ℕ) : ℝ) * (L + 1 : ℝ) ^ d * (2 : ℝ) ^ (A * X))).le + have hw := mul_le_mul_of_nonneg_right + (mul_le_mul_of_nonneg_left hd_le (Nat.cast_nonneg C)) (zero_le_one.trans htwo) + have h1 := one_le_mul_of_one_le_of_one_le (one_le_pow₀ hbase (n := d_max)) htwo + push_cast; linarith + +private theorem comp_poly_pow_le {len C_l L d_l d d_all : ℕ} + (hM : len + 1 ≤ (C_l + 1) * (L + 1) ^ d_l) (hd : d ≤ d_all) : + (len + 1 : ℝ) ^ d ≤ (((C_l + 1) ^ d_all : ℕ) : ℝ) * (L + 1 : ℝ) ^ (d_l * d_all) := by + have hnat : (len + 1) ^ d ≤ (C_l + 1) ^ d_all * (L + 1) ^ (d_l * d_all) := + (Nat.pow_le_pow_right (Nat.succ_pos len) hd).trans + ((Nat.pow_le_pow_left hM d_all).trans_eq (by rw [mul_pow, ← pow_mul])) + exact_mod_cast hnat + +private theorem polySys_time_bound_of_branchPolylog (k N₀_top N₀_branch : ℕ) + {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') + (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) : + ∃ N_sys C_sys d_sys A_sys : ℕ, 16384 ≤ N_sys ∧ + ∀ {N m : ℕ} {sys : List (List (List ℕ))}, + N_sys ≤ N → m ≤ leafDensityRatio k N * N → + IsCompiledSparseSystem k N (6 * N) + (initialRowWeightBound (leafDensityRatio k N) m * 2 ^ k) sys → + ((branchedPolyCertificate k N₀_top N₀_branch cBranch hbound).time (N, sys) : ℝ) ≤ + (C_sys : ℝ) * ((encPair encUnary encSys (N, sys)).length + 1 : ℝ) ^ d_sys * + (2 : ℝ) ^ ((A_sys : ℝ) * interpolationScale N) := by + obtain ⟨C_B, hCB⟩ := exists_leafDensityRatio_le_mul_clog_pow k + set β_B := 2 * (max 2 k - 1) + obtain ⟨C_inc, hCinc12, hInc⟩ := compiled_system_incidence_bounds k C_B β_B + set α_inc := 2 * β_B + 4; set β₀ := 2 * α_inc + 1 + obtain ⟨N₁, _, hBranchOk⟩ := + exists_threshold_checkBranchFeasible_eq_true N₀_branch (β₀ := β₀) (by dsimp only [β₀]; omega) + obtain ⟨N₀_br, C_br, d_br, A_br, hBrT⟩ := hbr_time k (2 * α_inc) C_inc + obtain ⟨C_g, d_g, hGuardT⟩ := exists_guardedBranchCertificate_time_le N₀_branch 0 cBranch + obtain ⟨C_ov, d_ov, hFeasT⟩ := + sparsePolyCounterCertificate_time_le_of_feasible N₀_top N₀_branch cBranch hbound + have hmk := computableInPolyTime_mkPaperInputConst k + obtain ⟨C_mk, d_mk, hMkT⟩ := (NativeCertificate.ofPolyTime_isPolynomial hmk).1.exists_le + obtain ⟨C_ml, d_ml, hMkLen⟩ := hmk.polyBounded_length.exists_le + obtain ⟨C_bl, d_bl, hBrLen⟩ := + (computableInPolyTime_toBranchInput.polyBounded_length.comp hmk.polyBounded_length).exists_le + set N_sys := max (max 16384 N₀_top) (max (2 * max N₁ N₀_br) (2 * 2 ^ C_inc)) + set d_br_all := max d_br d_g + set d_in := max (d_ml * d_ov) (max (d_bl * d_br_all) d_mk) + set C_p1 := C_ov * (C_ml + 1) ^ d_ov; set C_p2 := (C_br + C_g) * (C_bl + 1) ^ d_br_all + set C_sys := C_mk + 2 * (C_p1 + C_p2 + 1); set A_sys := 2 * A_br + 32 + refine ⟨N_sys, C_sys, d_in, A_sys, le_trans (le_max_left 16384 N₀_top) (le_max_left _ _), + fun {N m sys} hN hm hsys => ?_⟩ + have hN16 : 16384 ≤ N := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hN + have hN_top : max N₀_top 2 ≤ N := + max_le (le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hN) (by omega) + set inp := mkPaperSparseInput N k sys + have hinp1 : inp.1 = N := rfl; have hinp_sys : inp.2.2 = sys := rfl + have htop : checkTopFeasible N₀_top inp = true := + checkTopFeasible_mkPaperSparseInput_of_le hN_top (fun eq heq => (hsys.2 eq heq).1) + (fun eq heq mon hmon v hv => ((hsys.2 eq heq).2.2 mon hmon).2 v hv) + (fun eq heq mon hmon => ((hsys.2 eq heq).2.2 mon hmon).1) + obtain ⟨hb0_inc, hw_inc⟩ := hInc (by omega : 2 ≤ N) (hCB N (by omega)) hm hsys + set lam := Nat.clog 2 N + have hlam14 : 14 ≤ lam := by + have := (Nat.lt_clog_iff_pow_lt Nat.one_lt_two).mpr (show 2 ^ 13 < N by omega); omega + have hs_eq : inp.2.1.2.1 = (lam - 1).sqrt + 1 := by + have hcz : ¬ Nat.clog 2 N = 0 := by omega + have hc : ParameterCheck.heavyIncidenceCutoff 1 N = (lam - 1).sqrt + 1 := by + unfold ParameterCheck.heavyIncidenceCutoff; simp only [hcz, ↓reduceIte] + rw [show 1 + N - 1 = N by omega, Nat.div_self (by omega : 0 < N), one_mul] + change max 1 (ParameterCheck.heavyIncidenceCutoff 1 N) = _; rw [hc]; omega + have hs2 : 2 ≤ inp.2.1.2.1 := by + rw [hs_eq]; have := Nat.le_sqrt.mpr (show 1 * 1 ≤ lam - 1 by omega); omega + have hsqrt_le_s : lam.sqrt ≤ inp.2.1.2.1 := by + rw [hs_eq]; by_contra hgt + have h1 : ((lam - 1).sqrt + 2) * ((lam - 1).sqrt + 2) ≤ lam := Nat.le_sqrt.mp (by omega) + have h2 := Nat.lt_succ_sqrt (lam - 1); simp only [Nat.succ_eq_add_one] at h2 + nlinarith [show lam = (lam - 1) + 1 by omega] + have hS_le_sqrt : (HeavyBranchFold.heavyVarList N inp.2.1.2.2 sys).length ≤ N / lam.sqrt := + (checkTopFeasible_eq_true_iff.mp htop).2.2.2.2.2.trans + (Nat.div_le_div_left hsqrt_le_s (Nat.sqrt_pos.mpr (by omega))) + set Ly := (encPair encUnary encSys (N, sys)).length + have hinp_len : (encSparseSystemInput inp).length + 1 ≤ (C_ml + 1) * (Ly + 1) ^ d_ml := by + have h := hMkLen (N, sys); have hp := Nat.one_le_pow d_ml (Ly + 1) (Nat.succ_pos Ly) + dsimp only [inp]; nlinarith + have hbr_in_len : (HeavyBranchFold.encBranchInput (toBranchInput inp)).length + 1 ≤ + (C_bl + 1) * (Ly + 1) ^ d_bl := by + have h := hBrLen (N, sys); have hp := Nat.one_le_pow d_bl (Ly + 1) (Nat.succ_pos Ly) + dsimp only [inp]; nlinarith + have hrho_nn : 0 ≤ interpolationScale N := interpolationScale_nonneg N + set R_branch : ℕ := ⌈((C_p2 : ℕ) : ℝ) * (Ly + 1 : ℝ) ^ (d_bl * d_br_all) * + (2 : ℝ) ^ ((2 * (A_br : ℝ)) * interpolationScale N)⌉₊ + have hper_branch : ∀ idx < 2 ^ (HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2).length, + ∀ n' sys', HeavyBranchFold.prepareBranch inp.1 + (HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2) + (lowBits (HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2).length idx) + inp.2.2 = .reduced n' sys' → + (guardedBranchCertificate N₀_branch cBranch).time (n', sys') ≤ R_branch := by + intro idx _ n' sys' hred + obtain ⟨hn'_eq, hN_2n', hcan', hvars', hdeg', hb', hw'⟩ := + reduced_branch_invariants htop hs2 hred + rw [hinp1] at hn'_eq hN_2n' + have hn'_le_N : n' ≤ N := hn'_eq.symm ▸ Nat.sub_le N _ + have hn'_N1_br : max N₁ N₀_br ≤ n' := by + have : 2 * max N₁ N₀_br ≤ N := le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hN + omega + have hCinc_le_clog : C_inc ≤ Nat.clog 2 n' := by + have : 2 * 2 ^ C_inc ≤ N := le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) hN + exact (Nat.clog_pow 2 C_inc Nat.one_lt_two).symm.le.trans (Nat.clog_mono_right 2 (by omega)) + have hclog_tr := clog_pow_le_clog_pow_two_mul (by omega : 4 ≤ n') hN_2n' α_inc + have hb_2a := hb'.trans (hb0_inc.trans (Nat.mul_le_mul_left C_inc hclog_tr)) + have hw_2a := hw'.trans (hw_inc.trans (Nat.mul_le_mul_left C_inc hclog_tr)) + have hb_b0 : branchMaxFactorIncidence n' sys' ≤ Nat.clog 2 n' ^ β₀ := + (hb_2a.trans (Nat.mul_le_mul_right _ hCinc_le_clog)).trans_eq + (by dsimp only [β₀]; rw [pow_succ']) + have hw_b0 : branchMaxFactorWidth n' sys' ≤ Nat.clog 2 n' ^ β₀ := + (hw_2a.trans (Nat.mul_le_mul_right _ hCinc_le_clog)).trans_eq + (by dsimp only [β₀]; rw [pow_succ']) + have hlen_sys' : sys'.length ≤ C_inc * n' := by + obtain ⟨_, _, _, hsys'_eq⟩ := HeavyBranchFold.prepareBranch_eq_reduced_iff.mp hred + have hle6 : sys'.length ≤ 6 * N := by + rw [hsys'_eq, List.length_map] + exact (List.length_filter_le _ _).trans (by rw [List.length_map, hinp_sys]; exact hsys.1) + exact (hle6.trans (by omega : 6 * N ≤ 12 * n')).trans (Nat.mul_le_mul_right n' hCinc12) + have hchk : checkBranchFeasible N₀_branch (n', sys') = true := + (hBranchOk ((le_max_left N₁ N₀_br).trans hn'_N1_br) hcan' hvars' hb_b0 hw_b0).2.2 + have hgt := hGuardT (n', sys') (by simp only [hchk, Bool.true_eq_false, IsEmpty.forall_iff]) + simp only [hchk, ↓reduceIte] at hgt + have hc_br := hBrT n' sys' hchk ((le_max_right N₁ N₀_br).trans hn'_N1_br) + (sysMaxDegree_le_iff.mpr hdeg') hlen_sys' hb_2a hw_2a + have hlen_red := (Nat.add_le_add_right (HeavyBranchFold.length_enc_reduced_le hred) 1).trans + hbr_in_len + have hp_br := comp_poly_pow_le hlen_red (le_max_left d_br d_g) + have hexp_tr : (2 : ℝ) ^ ((A_br : ℝ) * interpolationScale n') ≤ + (2 : ℝ) ^ ((2 * (A_br : ℝ)) * interpolationScale N) := + Real.rpow_le_rpow_of_exponent_le one_le_two (by + have hsc := interpolationScale_le_two_mul_of_le_two_mul hn'_le_N hN_2n' + nlinarith [(Nat.cast_nonneg A_br : (0 : ℝ) ≤ A_br)]) + have ht2_nat : C_g * ((encPair encUnary encSys (n', sys')).length + 1) ^ d_g ≤ + (C_g * (C_bl + 1) ^ d_br_all) * (Ly + 1) ^ (d_bl * d_br_all) := + (Nat.mul_le_mul_left C_g ((Nat.pow_le_pow_right (Nat.succ_pos _) + (le_max_right d_br d_g)).trans + ((Nat.pow_le_pow_left hlen_red d_br_all).trans_eq (by rw [mul_pow, ← pow_mul])))).trans_eq + (mul_assoc _ _ _).symm + have ht2 := nat_poly_le_subexp ht2_nat le_rfl (by positivity : (0 : ℝ) ≤ 2 * (A_br : ℝ)) hrho_nn + have ht1 : (cBranch.time (prepareBranchEvalInput (n', sys')) : ℝ) ≤ + (C_br : ℝ) * (((C_bl + 1) ^ d_br_all : ℕ) : ℝ) * (Ly + 1 : ℝ) ^ (d_bl * d_br_all) * + (2 : ℝ) ^ ((2 * (A_br : ℝ)) * interpolationScale N) := + (hc_br.trans (mul_le_mul (mul_le_mul_of_nonneg_left hp_br (Nat.cast_nonneg C_br)) + hexp_tr (by positivity) (by positivity))).trans_eq (by dsimp only [d_br_all]; ring) + have htot_br : ((guardedBranchCertificate N₀_branch cBranch).time (n', sys') : ℝ) ≤ + (C_p2 : ℝ) * (Ly + 1 : ℝ) ^ (d_bl * d_br_all) * + (2 : ℝ) ^ ((2 * (A_br : ℝ)) * interpolationScale N) := by + have hgt_cast : ((guardedBranchCertificate N₀_branch cBranch).time (n', sys') : ℝ) ≤ + (cBranch.time (prepareBranchEvalInput (n', sys')) : ℝ) + + ((C_g * ((encPair encUnary encSys (n', sys')).length + 1) ^ d_g : ℕ) : ℝ) := by + exact_mod_cast hgt + exact hgt_cast.trans ((add_le_add ht1 ht2).trans_eq (by dsimp only [C_p2]; push_cast; ring)) + exact Nat.cast_le.mp (htot_br.trans (Nat.le_ceil _)) + have hsp_t := hFeasT inp R_branch htop hper_branch + have hcov_nat : C_ov * ((encSparseSystemInput inp).length + 1) ^ d_ov ≤ + C_p1 * (Ly + 1) ^ (d_ml * d_ov) := + (Nat.mul_le_mul_left C_ov (Nat.pow_le_pow_left hinp_len d_ov)).trans_eq + (by dsimp only [C_p1]; rw [mul_pow, ← pow_mul, mul_assoc]) + have hcov_r := nat_poly_le_subexp hcov_nat (le_max_left _ _ : d_ml * d_ov ≤ d_in) + (by positivity : (0 : ℝ) ≤ 2 * (A_br : ℝ)) hrho_nn + have hRbr_r : (R_branch : ℝ) ≤ ((C_p2 + 1 : ℕ) : ℝ) * (Ly + 1 : ℝ) ^ d_in * + (2 : ℝ) ^ ((2 * (A_br : ℝ)) * interpolationScale N) := + ceil_subexp_le ((le_max_left _ _).trans (le_max_right _ _)) (by positivity) hrho_nn + have hinner_r : + (((C_ov * ((encSparseSystemInput inp).length + 1) ^ d_ov + R_branch : ℕ)) : ℝ) ≤ + ((C_p1 + C_p2 + 1 : ℕ) : ℝ) * (Ly + 1 : ℝ) ^ d_in * + (2 : ℝ) ^ ((2 * (A_br : ℝ)) * interpolationScale N) := by + rw [Nat.cast_add, show ((C_p1 + C_p2 + 1 : ℕ) : ℝ) = (C_p1 : ℝ) + ((C_p2 + 1 : ℕ) : ℝ) by + push_cast; ring, add_mul, add_mul] + exact add_le_add hcov_r hRbr_r + have hS_pow_r : + ((2 ^ (HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2).length + 1 : ℕ) : ℝ) ≤ + 2 * (2 : ℝ) ^ (32 * interpolationScale N) := by + have hpow_le : (2 ^ (HeavyBranchFold.heavyVarList N inp.2.1.2.2 sys).length : ℝ) ≤ + (2 : ℝ) ^ (32 * interpolationScale N) := + (pow_le_pow_right₀ one_le_two hS_le_sqrt).trans + (ReplacementParams.two_pow_div_sqrt_clog_le_interpolationScale hN16) + have h1_32 : (1 : ℝ) ≤ (2 : ℝ) ^ (32 * interpolationScale N) := + Real.one_le_rpow one_le_two (mul_nonneg (by positivity) hrho_nn) + rw [hinp1, hinp_sys]; push_cast; linarith only [hpow_le, h1_32] + have hsp_r : ((sparsePolyCounterCertificate N₀_top N₀_branch cBranch hbound).time inp : ℝ) ≤ + ((2 * (C_p1 + C_p2 + 1) : ℕ) : ℝ) * (Ly + 1 : ℝ) ^ d_in * + (2 : ℝ) ^ ((A_sys : ℝ) * interpolationScale N) := by + have hcast : ((sparsePolyCounterCertificate N₀_top N₀_branch cBranch hbound).time inp : ℝ) ≤ + ((2 ^ (HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2).length + 1 : ℕ) : ℝ) * + (((C_ov * ((encSparseSystemInput inp).length + 1) ^ d_ov + R_branch : ℕ)) : ℝ) := by + exact_mod_cast hsp_t + calc ((sparsePolyCounterCertificate N₀_top N₀_branch cBranch hbound).time inp : ℝ) + ≤ (2 * (2 : ℝ) ^ (32 * interpolationScale N)) * + (((C_p1 + C_p2 + 1 : ℕ) : ℝ) * (Ly + 1 : ℝ) ^ d_in * + (2 : ℝ) ^ ((2 * (A_br : ℝ)) * interpolationScale N)) := + hcast.trans (mul_le_mul hS_pow_r hinner_r (by positivity) (by positivity)) + _ = ((2 * (C_p1 + C_p2 + 1) : ℕ) : ℝ) * (Ly + 1 : ℝ) ^ d_in * + ((2 : ℝ) ^ (32 * interpolationScale N) * + (2 : ℝ) ^ ((2 * (A_br : ℝ)) * interpolationScale N)) := by push_cast; ring + _ = ((2 * (C_p1 + C_p2 + 1) : ℕ) : ℝ) * (Ly + 1 : ℝ) ^ d_in * + (2 : ℝ) ^ ((A_sys : ℝ) * interpolationScale N) := by + rw [← Real.rpow_add two_pos]; dsimp only [A_sys]; push_cast; ring_nf + have hmk_r := nat_poly_le_subexp (hMkT (N, sys)) + ((le_max_right _ _).trans (le_max_right _ _) : d_mk ≤ d_in) (Nat.cast_nonneg A_sys) hrho_nn + have htot : (branchedPolyCertificate k N₀_top N₀_branch cBranch hbound).time (N, sys) = + (NativeCertificate.ofPolyTime hmk).time (N, sys) + + (sparsePolyCounterCertificate N₀_top N₀_branch cBranch hbound).time inp := rfl + rw [htot, Nat.cast_add, + show (C_sys : ℝ) = (C_mk : ℝ) + ((2 * (C_p1 + C_p2 + 1) : ℕ) : ℝ) from Nat.cast_add _ _, + add_mul, add_mul] + exact add_le_add hmk_r hsp_r + +private theorem exists_branchedSparseCNFLeafCertificate_time_le + (k N₀_leaf N₀_top N₀_branch : ℕ) {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') + (hs_br : PolyBounded (fun x => (encBranchEvalInput x).length) cBranch.space) : + ∃ C_nm d_nm : ℕ, ∀ x : (Unit × ℕ) × CNF ℕ, + (branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).time x ≤ + (branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).time x + + C_nm * ((encLeafIn x).length + 1) ^ d_nm := by + obtain ⟨pNorm, hpNorm, _, hNormT⟩ := exists_normalizeDeclaredLeafCertificate_bounds + (ComputableInPolyTime.snd encUnit encUnary) + (branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound) + (polyBounded_branchedSparseCNFDeclaredCertificate_space k N₀_leaf N₀_top N₀_branch + cBranch hbound hs_br) + obtain ⟨C_nm, d_nm, hNm⟩ := + (PolyBounded.of_polynomiallyBounded (fun n : ℕ => n) hpNorm).exists_le + refine ⟨C_nm, d_nm, fun x => ?_⟩ + have h1 : (branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).time x ≤ + (branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).time x + + pNorm (encLeafIn x).length := by + unfold branchedSparseCNFLeafCertificate; exact hNormT x + exact h1.trans (Nat.add_le_add_left (hNm (encLeafIn x).length) _) + +private theorem fast_path_arith_bound + {C_B β_B C_qi d_qi C_i d_i N_init PowE C_pol d_pol C_R0 d_R0 A_sys d_t C_dg C_ex0 C_decl : ℕ} + {N m B L poly_L q_val t_dg t_in : ℕ} + (hCi : C_i = C_qi * (C_B + CNF.initialRowWeightCoeff (C_B + 1) β_B) ^ d_qi) + (hdi : d_i = (2 * β_B + 3) * d_qi) + (hPowE : PowE = 2 ^ (C_i * Nat.clog 2 N_init ^ d_i)) + (hNinit : ∀ n, N_init ≤ n → + (2 : ℝ) ^ ((C_i : ℝ) * (Nat.clog 2 n : ℝ) ^ d_i) ≤ (2 : ℝ) ^ (1 * interpolationScale n)) + (hNq : ∀ m' B' P' : ℕ, m' ≤ B' * N → B' ≤ C_B * Nat.clog 2 N ^ β_B → + P' ≤ 20000 * B' ^ 2 * Nat.clog 2 (2 * m' + 4) ^ 2 → + 3 * (N : ℝ) * (2 * (m' : ℝ) + 2) ^ P' + 1 ≤ (2 : ℝ) ^ (1 * interpolationScale N)) + (hN2 : 2 ≤ N) (hm1 : 1 ≤ m) (hmB : m ≤ B * N) (hB : B ≤ C_B * Nat.clog 2 N ^ β_B) + (hQi : q_val ≤ C_qi * (B + Nat.log 2 (m + 2) + 1) ^ d_qi) + (hPol : poly_L ≤ C_pol * (L + 1) ^ d_pol) (hd_pol : d_pol ≤ d_t) (hd_R0 : d_R0 ≤ d_t) + (hdg_r : (t_dg : ℝ) ≤ + (C_dg : ℝ) * (L + 1 : ℝ) ^ d_t * (2 : ℝ) ^ (((A_sys + 1 : ℕ) : ℝ) * interpolationScale N)) + (hin_le : t_in ≤ 2 * (poly_L + 2 ^ q_val + + (3 * N + 1) * (candidateTupleCount m (greedyRowListLength B m) + 1) * + (poly_L + ⌈((C_R0 : ℕ) : ℝ) * (L + 1 : ℝ) ^ d_R0 * + (2 : ℝ) ^ ((A_sys : ℝ) * interpolationScale N)⌉₊) + 1)) + (hC_decl : C_decl = C_dg + C_ex0 + 2 * (C_pol + PowE + 3 * (C_pol + C_R0 + 1) + 1)) : + (t_dg : ℝ) + (t_in : ℝ) ≤ + (C_decl : ℝ) * (L + 1 : ℝ) ^ d_t * + (2 : ℝ) ^ (((A_sys + 1 : ℕ) : ℝ) * interpolationScale N) := by + set lam := Nat.clog 2 N; set A_t := A_sys + 1 + set R_x := ⌈((C_R0 : ℕ) : ℝ) * (L + 1 : ℝ) ^ d_R0 * + (2 : ℝ) ^ ((A_sys : ℝ) * interpolationScale N)⌉₊ + have hrho_nn : 0 ≤ interpolationScale N := interpolationScale_nonneg N + have h1_dt : (1 : ℝ) ≤ (L + 1 : ℝ) ^ d_t := one_le_pow₀ (by exact_mod_cast Nat.succ_pos L) + have htwo_At : (1 : ℝ) ≤ (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) := + Real.one_le_rpow one_le_two (mul_nonneg (Nat.cast_nonneg A_t) hrho_nn) + have h1_to_At : (2 : ℝ) ^ (1 * interpolationScale N) ≤ + (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) := + Real.rpow_le_rpow_of_exponent_le one_le_two + (mul_le_mul_of_nonneg_right (by exact_mod_cast (Nat.succ_pos A_sys : 1 ≤ A_t)) hrho_nn) + have hlam1 : 1 ≤ lam := (Nat.lt_clog_iff_pow_lt Nat.one_lt_two).mpr (by omega : 2 ^ 0 < N) + have hinit_exp : q_val ≤ C_i * lam ^ d_i := by + have hm2_le : m + 2 ≤ (B + 1) * N := by nlinarith only [hmB, hN2] + have hB1_le : B + 1 ≤ (C_B + 1) * lam ^ β_B := by + have hp := Nat.one_le_pow β_B lam hlam1; nlinarith only [hB, hp] + have hW2 := CNF.initialRowWeightBound_le_mul_pow_clog hN2 hm2_le hB1_le + have hlog_m2 : Nat.log 2 (m + 2) + 1 ≤ + CNF.initialRowWeightCoeff (C_B + 1) β_B * lam ^ (2 * β_B + 3) := by + refine le_trans ?_ hW2; unfold initialRowWeightBound + exact (Nat.le_self_pow (by decide : 3 ≠ 0) _).trans + (Nat.le_mul_of_pos_left _ (by positivity)) + have hu_le : B + Nat.log 2 (m + 2) + 1 ≤ + (C_B + CNF.initialRowWeightCoeff (C_B + 1) β_B) * lam ^ (2 * β_B + 3) := by + have hB' : B ≤ C_B * lam ^ (2 * β_B + 3) := + hB.trans (Nat.mul_le_mul_left C_B (Nat.pow_le_pow_right hlam1 (by omega))) + rw [Nat.add_assoc]; exact (Nat.add_le_add hB' hlog_m2).trans_eq (Nat.add_mul _ _ _).symm + exact hQi.trans ((Nat.mul_le_mul_left C_qi (Nat.pow_le_pow_left hu_le d_qi)).trans_eq + (by rw [hCi, hdi, mul_pow, ← pow_mul, mul_assoc])) + have hqinit_r : ((2 ^ q_val : ℕ) : ℝ) ≤ + (PowE : ℝ) * (L + 1 : ℝ) ^ d_t * (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) := by + have hbase_init : ((2 ^ q_val : ℕ) : ℝ) ≤ + (PowE : ℝ) * (2 : ℝ) ^ (1 * interpolationScale N) := by + by_cases hNi : N_init ≤ N + · have h1 : ((2 ^ q_val : ℕ) : ℝ) ≤ (2 : ℝ) ^ ((C_i : ℝ) * (lam : ℝ) ^ d_i) := by + rw [Nat.cast_pow, Nat.cast_ofNat, ← Real.rpow_natCast] + exact Real.rpow_le_rpow_of_exponent_le one_le_two (by exact_mod_cast hinit_exp) + have h2 : (1 : ℝ) ≤ (PowE : ℝ) := by rw [hPowE]; exact_mod_cast Nat.one_le_two_pow + exact (h1.trans (hNinit N hNi)).trans (le_mul_of_one_le_left (by positivity) h2) + · have he_le : q_val ≤ C_i * Nat.clog 2 N_init ^ d_i := + hinit_exp.trans (Nat.mul_le_mul_left C_i + (Nat.pow_le_pow_left (Nat.clog_mono_right 2 (by omega)) d_i)) + have h1 : ((2 ^ q_val : ℕ) : ℝ) ≤ (PowE : ℝ) := by + rw [hPowE]; exact Nat.cast_le.mpr (Nat.pow_le_pow_right Nat.zero_lt_two he_le) + exact h1.trans (le_mul_of_one_le_right (by positivity) + (Real.one_le_rpow one_le_two (mul_nonneg zero_le_one hrho_nn))) + exact ((hbase_init.trans (mul_le_mul_of_nonneg_left h1_to_At (by positivity))).trans + (mul_le_mul_of_nonneg_left ((one_mul _).symm.le.trans + (mul_le_mul_of_nonneg_right h1_dt (by positivity))) (by positivity))).trans_eq (by ring) + set P := greedyRowListLength B m + have hP_le : P ≤ 20000 * B ^ 2 * Nat.clog 2 (2 * m + 4) ^ 2 := by + have hlt_clog : Nat.log 2 m < Nat.clog 2 (2 * m + 4) := by + rw [Nat.lt_clog_iff_pow_lt Nat.one_lt_two] + have := Nat.pow_log_le_self 2 (by omega : m ≠ 0); omega + exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) 2) + have hcand_r : (((3 * N + 1) * (candidateTupleCount m P + 1) : ℕ) : ℝ) ≤ + 3 * (2 : ℝ) ^ (1 * interpolationScale N) := by + have hq_ev := hNq m B P hmB hB hP_le + have hcand_le : candidateTupleCount m P ≤ (2 * m + 2) ^ P := Nat.pow_le_pow_left (by omega) P + have hp_pos : 1 ≤ (2 * m + 2) ^ P := Nat.one_le_pow P _ (by omega) + have hnat_ineq : (3 * N + 1) * (candidateTupleCount m P + 1) ≤ + 3 * (3 * N * (2 * m + 2) ^ P + 1) := + (Nat.mul_le_mul (by omega : 3 * N + 1 ≤ 4 * N) + (by omega : candidateTupleCount m P + 1 ≤ 2 * (2 * m + 2) ^ P)).trans + (calc (4 * N) * (2 * (2 * m + 2) ^ P) = 8 * (N * (2 * m + 2) ^ P) := by ring + _ ≤ 3 * (3 * N * (2 * m + 2) ^ P + 1) := by rw [mul_assoc 3 N]; omega) + have hcast : (((3 * N + 1) * (candidateTupleCount m P + 1) : ℕ) : ℝ) ≤ + 3 * (3 * (N : ℝ) * (2 * (m : ℝ) + 2) ^ P + 1) := by exact_mod_cast hnat_ineq + exact hcast.trans (mul_le_mul_of_nonneg_left hq_ev zero_le_three) + have hpolR_r : ((poly_L + R_x : ℕ) : ℝ) ≤ ((C_pol + C_R0 + 1 : ℕ) : ℝ) * (L + 1 : ℝ) ^ d_t * + (2 : ℝ) ^ ((A_sys : ℝ) * interpolationScale N) := by + rw [Nat.cast_add, show ((C_pol + C_R0 + 1 : ℕ) : ℝ) = (C_pol : ℝ) + ((C_R0 + 1 : ℕ) : ℝ) by + push_cast; ring, add_mul, add_mul] + exact add_le_add (nat_poly_le_subexp hPol hd_pol (Nat.cast_nonneg A_sys) hrho_nn) + (ceil_subexp_le hd_R0 (Nat.cast_nonneg A_sys) hrho_nn) + have hprod_r : (((3 * N + 1) * (candidateTupleCount m P + 1) * (poly_L + R_x) : ℕ) : ℝ) ≤ + ((3 * (C_pol + C_R0 + 1) : ℕ) : ℝ) * (L + 1 : ℝ) ^ d_t * + (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) := by + calc (((3 * N + 1) * (candidateTupleCount m P + 1) * (poly_L + R_x) : ℕ) : ℝ) + ≤ (3 * (2 : ℝ) ^ (1 * interpolationScale N)) * + (((C_pol + C_R0 + 1 : ℕ) : ℝ) * (L + 1 : ℝ) ^ d_t * + (2 : ℝ) ^ ((A_sys : ℝ) * interpolationScale N)) := by + rw [Nat.cast_mul]; exact mul_le_mul hcand_r hpolR_r (by positivity) (by positivity) + _ = ((3 * (C_pol + C_R0 + 1) : ℕ) : ℝ) * (L + 1 : ℝ) ^ d_t * + ((2 : ℝ) ^ (1 * interpolationScale N) * + (2 : ℝ) ^ ((A_sys : ℝ) * interpolationScale N)) := by push_cast; ring + _ = ((3 * (C_pol + C_R0 + 1) : ℕ) : ℝ) * (L + 1 : ℝ) ^ d_t * + (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) := by + rw [← Real.rpow_add two_pos]; dsimp only [A_t]; push_cast; ring_nf + have hpol_At := nat_poly_le_subexp hPol hd_pol (Nat.cast_nonneg A_t) hrho_nn + have h1_At := one_le_mul_of_one_le_of_one_le h1_dt htwo_At + have hin_cast : (t_in : ℝ) ≤ 2 * ((poly_L : ℝ) + ((2 ^ q_val : ℕ) : ℝ) + + (((3 * N + 1) * (candidateTupleCount m P + 1) * (poly_L + R_x) : ℕ) : ℝ) + 1) := by + exact_mod_cast hin_le + have hC_eq : (C_decl : ℝ) = (C_dg : ℝ) + (C_ex0 : ℝ) + + 2 * ((C_pol : ℝ) + (PowE : ℝ) + ((3 * (C_pol + C_R0 + 1) : ℕ) : ℝ) + 1) := by + rw [hC_decl]; push_cast; ring + have h0_ex : (0 : ℝ) ≤ + (C_ex0 : ℝ) * (L + 1 : ℝ) ^ d_t * (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) := by + positivity + rw [hC_eq]; linarith only [hdg_r, hin_cast, hpol_At, hqinit_r, hprod_r, h1_At, h0_ex] + +/-- **Threshold-parametric fast-regime `2 ^ {O_k(interpolationScale N)}` runtime bound +(§5.5, §6.3 eq. (6.4), §6.4 Proposition 6.4)**: above `N_min ≥ 16384`, both leaf certificates run +in `C_t * (|enc x| + 1) ^ d_t * 2 ^ (A_t * interpolationScale x.1.2)` steps on +`x.2.length ≤ leafOccBound k x.1.2 * x.1.2 + 1` (for all `N : ℕ`, including `N = 0`). -/ +theorem exists_threshold_branchedSparseCNF_time_bound (k N₀_top N₀_branch : ℕ) + {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') + (hs_br : PolyBounded (fun x => (encBranchEvalInput x).length) cBranch.space) + (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) : + ∃ N_min : ℕ, 16384 ≤ N_min ∧ ∀ N₀_leaf : ℕ, N_min ≤ N₀_leaf → + ∃ C_t d_t A_t : ℕ, 1 ≤ A_t ∧ + ∀ x : (Unit × ℕ) × CNF ℕ, x.2.length ≤ leafOccBound k x.1.2 * x.1.2 + 1 → + ((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch + cBranch hbound).time x : ℝ) ≤ + (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t * + (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) ∧ + ((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch + cBranch hbound).time x : ℝ) ≤ + (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t * + (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) := by + obtain ⟨N_sys, C_sys, d_sys, A_sys, hNsys16, hSysT⟩ := + polySys_time_bound_of_branchPolylog k N₀_top N₀_branch cBranch hbound hbr_time + obtain ⟨C_B, hCB⟩ := exists_leafDensityRatio_le_mul_clog_pow k; set β_B := 2 * (max 2 k - 1) + obtain ⟨N_q, hNq⟩ := Filter.eventually_atTop.mp + (SparseCountingScale.eventually_query_overhead_poly_le C_B β_B 20000 2 2 one_pos) + set N_min := max N_sys N_q + refine ⟨N_min, hNsys16.trans (le_max_left _ _), fun N₀_leaf hN₀ => ?_⟩ + have hNOf := ComputableInPolyTime.snd encUnit encUnary + have hBOf := computableInPolyTime_leafDensityRatio k + obtain ⟨cPoly, hcPoly⟩ : + ∃ c, c = branchedPolyCertificate k N₀_top N₀_branch cBranch hbound := ⟨_, rfl⟩ + have hcPoly_sp : PolyBounded (fun y => (encPair encUnary encSys y).length) cPoly.space := + hcPoly ▸ polyBounded_branchedPolyCertificate_space k N₀_top N₀_branch cBranch hbound hs_br + obtain ⟨poly, qInit, polySys, hpoly, hqInit, hpolySys, _, hInnerDeclT⟩ := + exists_sparseCNFDeclaredCertificate_bounds k (max 1 N₀_leaf) hNOf hBOf cPoly hcPoly_sp + obtain ⟨cInner, hcInner⟩ : + ∃ c, c = sparseCNFDeclaredCertificate k (max 1 N₀_leaf) hNOf hBOf cPoly := ⟨_, rfl⟩ + rw [← hcInner] at hInnerDeclT + obtain ⟨C_nm, d_nm, hLeafT⟩ := exists_branchedSparseCNFLeafCertificate_time_le + k N₀_leaf N₀_top N₀_branch cBranch hbound hs_br + obtain ⟨cDecl, hcDecl⟩ : + ∃ c, c = branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound := + ⟨_, rfl⟩ + obtain ⟨cLeaf, hcLeaf⟩ : + ∃ c, c = branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound := + ⟨_, rfl⟩ + have hcDecl_time : ∀ x, cDecl.time x = + (NativeCertificate.ofPolyTime (computableInPolyTime_denseFallbackGuard k)).time x + + if denseFallbackGuard k x then (countCNFExhaustiveCertificate.comp + (NativeCertificate.ofPolyTime computableInPolyTime_leafExhProj)).time x + else cInner.time x := fun x => by + rw [hcDecl]; unfold branchedSparseCNFDeclaredCertificate guardedTargetOfPolyTime + rw [guardedTargetCertificate_time _ _ _ _ _ x, ← hcPoly, ← hcInner] + rw [← hcLeaf, ← hcDecl] at hLeafT ⊢ + obtain ⟨C_pol, d_pol, hPol⟩ := (PolyBounded.of_polynomiallyBounded (·) hpoly).exists_le + obtain ⟨C_qi, d_qi, hQi⟩ := (PolyBounded.of_polynomiallyBounded (·) hqInit).exists_le + obtain ⟨C_ps, d_ps, hPs⟩ := (PolyBounded.of_polynomiallyBounded (·) hpolySys).exists_le + obtain ⟨C_dg, d_dg, hDg⟩ := (NativeCertificate.ofPolyTime_isPolynomial + (computableInPolyTime_denseFallbackGuard k)).1.exists_le + obtain ⟨P_ex, Q_ex, hP_ex, hQ_ex, hExhT⟩ := exists_countCNFExhaustive_time_le + obtain ⟨C_ex0, d_ex0, hEx0⟩ := + ((NativeCertificate.ofPolyTime_isPolynomial computableInPolyTime_leafExhProj).1.add + ((((PolyBounded.const 2).mul hP_ex).add hQ_ex).comp + computableInPolyTime_leafExhProj.polyBounded_length)).exists_le + set C_i := C_qi * (C_B + CNF.initialRowWeightCoeff (C_B + 1) β_B) ^ d_qi + set d_i := (2 * β_B + 3) * d_qi + obtain ⟨N_init, hNinit⟩ := Filter.eventually_atTop.mp + (SparseCountingScale.eventually_two_pow_clog_pow_le (C_i : ℝ) d_i one_pos) + obtain ⟨PowE, hPowE⟩ : ∃ n, n = 2 ^ (C_i * Nat.clog 2 N_init ^ d_i) := ⟨_, rfl⟩ + obtain ⟨C_R0, hC_R0⟩ : ∃ n, n = C_sys * (C_ps + 1) ^ d_sys := ⟨_, rfl⟩ + set d_R0 := d_ps * d_sys + let R (x : (Unit × ℕ) × CNF ℕ) : ℕ := ⌈((C_R0 : ℕ) : ℝ) * ((encLeafIn x).length + 1 : ℝ) ^ d_R0 * + (2 : ℝ) ^ ((A_sys : ℝ) * interpolationScale x.1.2)⌉₊ + have hValidR : ValidPolyTimeBound encLeafCtx Prod.snd + (fun p : Unit × ℕ => leafDensityRatio k p.2) k (max 1 N₀_leaf) cPoly polySys R := by + intro x hfast sys hsys hlen + obtain ⟨_, _, _, hge, hmB⟩ := entersSparseFastPath_eq_true_iff.mp hfast + have ht := hSysT + (le_trans (le_max_left _ _) (hN₀.trans ((le_max_right 1 N₀_leaf).trans hge))) hmB hsys + rw [← hcPoly] at ht; set L := (encLeafIn x).length + have hps_bound : (encPair encUnary encSys (x.1.2, sys)).length + 1 ≤ + (C_ps + 1) * (L + 1) ^ d_ps := by + have hp1 := Nat.one_le_pow d_ps (L + 1) (Nat.succ_pos L) + have h1 := hlen.trans (hPs L); nlinarith only [hp1, h1] + have ht' : (cPoly.time (x.1.2, sys) : ℝ) ≤ + (C_R0 : ℝ) * (L + 1 : ℝ) ^ d_R0 * (2 : ℝ) ^ ((A_sys : ℝ) * interpolationScale x.1.2) := + (ht.trans (mul_le_mul_of_nonneg_right + (mul_le_mul_of_nonneg_left (comp_poly_pow_le hps_bound (le_rfl : d_sys ≤ d_sys)) + (Nat.cast_nonneg C_sys)) (by positivity))).trans_eq + (by rw [hC_R0]; dsimp only [d_R0]; push_cast; ring) + exact Nat.cast_le.mp (ht'.trans (Nat.le_ceil _)) + set A_t := A_sys + 1; set d_t := max (max d_dg d_ex0) (max d_pol (max d_R0 d_nm)) + obtain ⟨C_decl, hC_decl⟩ : + ∃ n, n = C_dg + C_ex0 + 2 * (C_pol + PowE + 3 * (C_pol + C_R0 + 1) + 1) := ⟨_, rfl⟩ + set C_t := C_decl + C_nm; refine ⟨C_t, d_t, A_t, Nat.succ_pos _, fun x hlen_x => ?_⟩ + set L := (encLeafIn x).length + have hrho_nn : 0 ≤ interpolationScale x.1.2 := interpolationScale_nonneg x.1.2 + have hd_dg : d_dg ≤ d_t := (le_max_left _ _).trans (le_max_left _ _) + have hd_ex0 : d_ex0 ≤ d_t := (le_max_right _ _).trans (le_max_left _ _) + have hd_pol : d_pol ≤ d_t := (le_max_left _ _).trans (le_max_right _ _) + have hd_R0 : d_R0 ≤ d_t := (le_max_left _ _).trans ((le_max_right _ _).trans (le_max_right _ _)) + have hd_nm : d_nm ≤ d_t := (le_max_right _ _).trans ((le_max_right _ _).trans (le_max_right _ _)) + have hdg_r := nat_poly_le_subexp (hDg x) hd_dg (Nat.cast_nonneg A_t) hrho_nn + have hdecl_bound : (cDecl.time x : ℝ) ≤ + (C_decl : ℝ) * (L + 1 : ℝ) ^ d_t * (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) := by + rw [hcDecl_time x]; cases hd : denseFallbackGuard k x + · simp only [Bool.false_eq_true, ↓reduceIte, Nat.cast_add] + have hinner_t := hInnerDeclT R hValidR x + unfold sparseCNFTimeBound at hinner_t; dsimp only at hinner_t + cases hfast : entersSparseFastPath k (max 1 N₀_leaf) x.1.2 (leafDensityRatio k x.1.2) x.2 + · simp only [hfast, Bool.false_eq_true, ↓reduceIte] at hinner_t + have hpol_nat : 2 * (poly L + 1) ≤ (2 * (C_pol + 1)) * (L + 1) ^ d_pol := by + have hp1 := Nat.one_le_pow d_pol (L + 1) (Nat.succ_pos L) + have h1 := hPol L; nlinarith only [hp1, h1] + have hpol_r := nat_poly_le_subexp (hinner_t.trans hpol_nat) hd_pol + (Nat.cast_nonneg A_t) hrho_nn + have hle_C : (C_dg : ℝ) + ((2 * (C_pol + 1) : ℕ) : ℝ) ≤ (C_decl : ℝ) := by + exact_mod_cast (show C_dg + 2 * (C_pol + 1) ≤ C_decl by rw [hC_decl]; omega) + exact (add_le_add hdg_r hpol_r).trans (by + rw [← add_mul, ← add_mul] + exact mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_right hle_C (by positivity)) + (by positivity)) + · simp only [hfast, ↓reduceIte] at hinner_t + obtain ⟨_, he, _, hge, hmB⟩ := entersSparseFastPath_eq_true_iff.mp hfast + have hN_min : N_min ≤ x.1.2 := hN₀.trans ((le_max_right 1 N₀_leaf).trans hge) + have hN2 : 2 ≤ x.1.2 := + (by omega : 2 ≤ 16384).trans ((hNsys16.trans (le_max_left _ _)).trans hN_min) + have hm1 : 1 ≤ x.2.length := by + rcases eq : x.2 with _ | ⟨_, _⟩ + · rw [eq] at he; cases he + · exact Nat.succ_pos _ + exact fast_path_arith_bound rfl rfl hPowE hNinit + (hNq x.1.2 ((le_max_right _ _).trans hN_min)) hN2 hm1 hmB (hCB x.1.2 hN2) + (hQi _) (hPol L) hd_pol hd_R0 hdg_r hinner_t hC_decl + · simp only [↓reduceIte, Nat.cast_add] + have hgt_dense : leafDensityRatio k x.1.2 * x.1.2 < x.2.length := by + simp only [denseFallbackGuard, Bool.and_eq_true, decide_eq_true_eq] at hd; exact hd.2 + have hN0 : x.1.2 = 0 := by + rcases Nat.eq_zero_or_pos x.1.2 with h0 | hpos + · exact h0 + · exact False.elim ((leafOccBound_mul_succ_le_leafDensityRatio_mul hpos).not_gt + (lt_of_lt_of_le hgt_dense hlen_x)) + have hex_nat : (countCNFExhaustiveCertificate.comp + (NativeCertificate.ofPolyTime computableInPolyTime_leafExhProj)).time x ≤ + C_ex0 * (L + 1) ^ d_ex0 := by + rw [NativeCertificate.comp_time]; have hex := hExhT (x.1.2, x.2) + have hpow0 : 2 ^ x.1.2 + 1 = 2 := by rw [hN0]; rfl + dsimp only [computableInPolyTime_leafExhProj] at *; rw [hpow0] at hex + exact (Nat.add_le_add_left hex _).trans (hEx0 x) + have hex_r := nat_poly_le_subexp hex_nat hd_ex0 (Nat.cast_nonneg A_t) hrho_nn + have hle_C : (C_dg : ℝ) + (C_ex0 : ℝ) ≤ (C_decl : ℝ) := by + exact_mod_cast (show C_dg + C_ex0 ≤ C_decl by rw [hC_decl]; omega) + exact (add_le_add hdg_r hex_r).trans (by + rw [← add_mul, ← add_mul] + exact mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_right hle_C (by positivity)) + (by positivity)) + refine ⟨hdecl_bound.trans (mul_le_mul_of_nonneg_right + (mul_le_mul_of_nonneg_right (Nat.cast_le.mpr (Nat.le_add_right _ _)) (by positivity)) + (by positivity)), ?_⟩ + have hnt_r : (cLeaf.time x : ℝ) ≤ + (cDecl.time x : ℝ) + ((C_nm * (L + 1) ^ d_nm : ℕ) : ℝ) := by exact_mod_cast hLeafT x + have hnm_r := nat_poly_le_subexp (le_rfl : C_nm * (L + 1) ^ d_nm ≤ C_nm * (L + 1) ^ d_nm) + hd_nm (Nat.cast_nonneg A_t) hrho_nn + rw [show (C_t : ℝ) = (C_decl : ℝ) + (C_nm : ℝ) from Nat.cast_add _ _, add_mul, add_mul] + exact hnt_r.trans (add_le_add hdecl_bound hnm_r) + +/-- **Existential fast-regime `2 ^ {O_k(interpolationScale N)}` runtime bound +(§5.5, §6.3 eq. (6.4), §6.4 Proposition 6.4)**: +under `BranchPolylogTimeBound N₀_branch cBranch` and polynomial branch workspace `hs_br`, there +exist `N₀_leaf N₀_top C_t d_t A_t : ℕ` (`1 ≤ A_t`) bounding both leaf certificates across all +`x = ((c, N), ψ)` satisfying `ψ.length ≤ leafOccBound k N * N + 1` (including `N = 0`). -/ +theorem exists_branchedSparseCNF_time_bound (k N₀_branch : ℕ) + {branchEval : BranchEvalInput → ℕ} + (cBranch : NativeCertificate branchEval encBranchEvalInput encNat) + (hbound : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true → + branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') + (hs_br : PolyBounded (fun x => (encBranchEvalInput x).length) cBranch.space) + (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) : + ∃ N₀_leaf N₀_top C_t d_t A_t : ℕ, 1 ≤ A_t ∧ + ∀ x : (Unit × ℕ) × CNF ℕ, x.2.length ≤ leafOccBound k x.1.2 * x.1.2 + 1 → + ((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch + cBranch hbound).time x : ℝ) ≤ + (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t * + (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) ∧ + ((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch + cBranch hbound).time x : ℝ) ≤ + (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t * + (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) := by + obtain ⟨N_min, _, hBound⟩ := + exists_threshold_branchedSparseCNF_time_bound k 0 N₀_branch cBranch hbound hs_br hbr_time + obtain ⟨C_t, d_t, A_t, hA, hT⟩ := hBound N_min le_rfl + exact ⟨N_min, 0, C_t, d_t, A_t, hA, hT⟩ + +end +end Cslib.Complexity.BranchedSparseCNFCounter diff --git a/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean new file mode 100644 index 000000000..c8e3427fc --- /dev/null +++ b/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean @@ -0,0 +1,147 @@ +/- +Copyright (c) 2026 Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anton Kovsharov +-/ + +module + +public import Complexity.Init +public import Complexity.Computability.PolyTime.CNF.BranchedSparseCNFCounter +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain + +/-! # Kernel-checked tests for `Cslib.Complexity.BranchedSparseCNFCounter` -/ + +@[expose] public section + +namespace ComplexityTests.Computability.PolyTime.CNF.BranchedSparseCNFCounter + +open Cslib.Complexity Cslib.Complexity.BranchedSparseCNFCounter Cslib.GenericRAM +open Cslib.Complexity.SparseCNFLeafCounter Cslib.Complexity.SubexponentialSAT +open Cslib.Complexity.SubexponentialSAT.SparsePolyCounter Cslib.GenericRAM.ExhaustiveCountFallback +open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.ClauseSet.Sparsification Turing.MultiTapeTM +open Turing.MultiTapeTM.Universal (encUnit) + +local notation "encLeafIn" => encPair (encPair encUnit encUnary) encCNF + +/-- Concrete branch evaluator executing streaming `countSystemExhaustive` on `(n', eqs')`. -/ +abbrev exhBranchEval (inp : BranchEvalInput) : ℕ := countSystemExhaustive (inp.1.1, inp.2.2.2) +private abbrev declExh (k a b c : ℕ) := branchedSparseCNFDeclaredCounter k a b c exhBranchEval +private abbrev leafExh (k a b c : ℕ) := branchedSparseCNFLeafCounter k a b c exhBranchEval + +-- 1. `N = 0` boundary (`[]` and `[[]]`, exercising the dense `B * N < ψ.length` outer guard). +example : declExh 3 0 0 0 (((), 0), []) = 1 ∧ leafExh 3 0 0 0 (((), 0), []) = 1 ∧ + declExh 3 0 0 0 (((), 0), [[]]) = 0 ∧ leafExh 3 0 0 0 (((), 0), [[]]) = 0 ∧ + ([[]] : CNF ℕ).length = leafOccBound 3 0 * 0 + 1 ∧ + leafDensityRatio 3 0 * 0 < ([[]] : CNF ℕ).length := by decide + +-- 2. Repeated unit clauses exceeding `leafDensityRatio 3 2 * 2` on `N = 2`. +private theorem ratio_three_of_div {N : ℕ} (h : leafSearchDivisor N = 1) : + leafDensityRatio 3 N = 525315 := by + have hM : leafThresholdBase 3 N = 2 ^ 9 := by + unfold leafThresholdBase; rw [h] + exact countingThresholdBase_eq_two_pow (k := 3) (B := 1) (m := 9) + (by decide) (by decide) (by decide) (by decide) + unfold leafDensityRatio leafOccBound; rw [hM]; decide +theorem leafDensityRatio_three_two : leafDensityRatio 3 2 = 525315 := + ratio_three_of_div (by unfold leafSearchDivisor; rw [SparseCountingScale.numGroups_of_lt_three + (by decide : 2 < 3)]; decide) +private def unit0 : CNF ℕ := [[(0, true)]] +private def denseUnits2 : CNF ℕ := List.replicate 1050631 [(0, true)] + +example : leafDensityRatio 3 2 * 2 < denseUnits2.length ∧ + declExh 3 0 0 0 (((), 2), denseUnits2) = 2 ∧ leafExh 3 0 0 0 (((), 2), denseUnits2) = 1 := by + have hw : ∀ c ∈ denseUnits2, c.length ≤ 3 := fun c hc => by + rw [(List.mem_replicate.mp hc).2]; decide + have hvset : denseUnits2.vars.toFinset = unit0.vars.toFinset := by + ext v; simp only [denseUnits2, unit0, List.mem_toFinset, CNF.mem_vars, List.mem_replicate, + ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, true_and, exists_eq_left, List.mem_singleton] + have hsub : denseUnits2.vars.toFinset ⊆ Finset.range 2 := by rw [hvset]; decide + have heval : ∀ σ, denseUnits2.eval σ = unit0.eval σ := fun σ => by + simp only [denseUnits2, unit0, CNF.eval, List.all_replicate, OfNat.ofNat_ne_zero, + ↓reduceIte, List.all_cons, List.all_nil, Bool.and_true] + have hon : denseUnits2.modelCountOn (Finset.range 2) = 2 := + (show _ = unit0.modelCountOn (Finset.range 2) by simp only [CNF.modelCountOn, heval]).trans + (by decide) + have hmul := CNF.modelCountOn_eq_mul_modelCount denseUnits2 (Finset.range 2) hsub + rw [hon, CNF.numVars, hvset, show (Finset.range 2).card - unit0.vars.toFinset.card = 1 by decide] + at hmul + refine ⟨by rw [leafDensityRatio_three_two, denseUnits2, List.length_replicate]; decide, ?_⟩ + unfold declExh leafExh exhBranchEval + rw [branchedSparseCNFDeclaredCounter_exhaustive_eq_modelCountOn 3 0 0 0 () 2 _ hw hsub, + branchedSparseCNFLeafCounter_exhaustive_eq_modelCount 3 0 0 0 () 2 _ hw hsub, hon]; omega + +-- 3. Non-dense variable support (`N = 4`, variables `{0, 2}`) across fallback and fast paths. +theorem leafDensityRatio_three_four : leafDensityRatio 3 4 = 525315 := + ratio_three_of_div (by unfold leafSearchDivisor; rw [(SparseCountingScale.numGroups_eq_iff + (s := 1) (by decide)).mpr (by decide)]; decide) +private def nonDense1 : CNF ℕ := [[(0, true), (2, false)]] +private def nonDense2 : CNF ℕ := [[(0, true), (2, false)], [(0, false), (2, false)]] + +example : (declExh 3 5 0 0 (((), 4), nonDense1) = 12 ∧ leafExh 3 5 0 0 (((), 4), nonDense1) = 3 ∧ + declExh 3 5 0 0 (((), 4), nonDense2) = 8 ∧ leafExh 3 5 0 0 (((), 4), nonDense2) = 2) ∧ + entersSparseFastPath 3 1 4 (leafDensityRatio 3 4) nonDense2 = true ∧ + declExh 3 0 0 0 (((), 4), nonDense1) = 12 ∧ leafExh 3 0 0 0 (((), 4), nonDense1) = 3 ∧ + declExh 3 0 0 0 (((), 4), nonDense2) = 8 ∧ leafExh 3 0 0 0 (((), 4), nonDense2) = 2 := by + refine ⟨?_, by rw [leafDensityRatio_three_four]; decide, ?_⟩ + · unfold declExh leafExh branchedSparseCNFLeafCounter normalizeDeclaredLeaf + branchedSparseCNFDeclaredCounter sparseCNFDeclaredCounter + dsimp only; rw [leafDensityRatio_three_four]; decide + · have hd := branchedSparseCNFDeclaredCounter_exhaustive_eq_modelCountOn 3 0 0 0 () 4 + have hl := branchedSparseCNFLeafCounter_exhaustive_eq_modelCount 3 0 0 0 () 4 + unfold declExh leafExh exhBranchEval + rw [hd nonDense1 (by decide) (by decide), hl nonDense1 (by decide) (by decide), + hd nonDense2 (by decide) (by decide), hl nonDense2 (by decide) (by decide)]; decide + +-- 4. Invalid width / out-of-range variables and unconditional global output caps. +example : declExh 3 0 0 0 (((), 5), [[(0, true), (1, true), (2, true), (3, true)]]) = 0 ∧ + leafExh 3 0 0 0 (((), 5), [[(0, true), (1, true), (2, true), (3, true)]]) = 0 ∧ + declExh 3 0 0 0 (((), 2), [[(2, true)]]) = 0 ∧ + leafExh 3 0 0 0 (((), 2), [[(2, true)]]) = 0 := by decide +example (x : (Unit × ℕ) × CNF ℕ) : + branchedSparseCNFDeclaredCounter 3 2 2 2 (fun _ => 999999) x ≤ 2 ^ x.1.2 ∧ + branchedSparseCNFLeafCounter 3 2 2 2 (fun _ => 999999) x ≤ 2 ^ x.2.numVars := + ⟨branchedSparseCNFDeclaredCounter_le_two_pow 3 2 2 2 _ x, + branchedSparseCNFLeafCounter_le_two_pow_numVars 3 2 2 2 _ x⟩ + +-- 5. Concrete `NativeCertificate`, `.isComputable`, and `PolyBounded` workspace checks. +private theorem computableInPolyTime_exhBranchProj : + ComputableInPolyTime (fun inp : BranchEvalInput => (inp.1.1, inp.2.2.2)) + encBranchEvalInput (encPair encUnary (encList (encList (encList encNat)))) := by + unfold encBranchEvalInput + exact ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.fst _ _)).prod + ((ComputableInPolyTime.snd _ _).comp + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _))) +private noncomputable def exhBranchCert : + NativeCertificate exhBranchEval encBranchEvalInput encNat := + countSystemExhaustiveCertificate.comp (.ofPolyTime computableInPolyTime_exhBranchProj) +private theorem exhBranchEval_le (n' : ℕ) (eqs' : List (List (List ℕ))) + (_ : checkBranchFeasible 2 (n', eqs') = true) : + exhBranchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n' := + (countSystemExhaustive_eq_rootCount n' eqs').trans_le + (HeavyBranchFold.rootCount_le_two_pow n' eqs') +private theorem polyBounded_exhBranchCert_space : + PolyBounded (fun x => (encBranchEvalInput x).length) exhBranchCert.space := + (NativeCertificate.ofPolyTime_isPolynomial computableInPolyTime_exhBranchProj).2.add + (polyBounded_countSystemExhaustive_space.comp + computableInPolyTime_exhBranchProj.polyBounded_length) +private noncomputable abbrev cDeclTest := + branchedSparseCNFDeclaredCertificate 3 2 2 2 exhBranchCert exhBranchEval_le +private noncomputable abbrev cLeafTest := + branchedSparseCNFLeafCertificate 3 2 2 2 exhBranchCert exhBranchEval_le +example : ComputableInPolyTime (fun p : Unit × ℕ => leafDensityRatio 3 p.2) + (encPair encUnit encUnary) encUnary ∧ + IsComputable (declExh 3 2 2 2) encLeafIn encNat ∧ + IsComputable (leafExh 3 2 2 2) encLeafIn encNat ∧ + PolyBounded (fun x => (encLeafIn x).length) cDeclTest.space ∧ + PolyBounded (fun x => (encLeafIn x).length) cLeafTest.space ∧ + ComputableInO (declExh 3 2 2 2) encLeafIn encNat cDeclTest.time cDeclTest.space ∧ + ComputableInO (leafExh 3 2 2 2) encLeafIn encNat cLeafTest.time cLeafTest.space := + ⟨computableInPolyTime_leafDensityRatio 3, cDeclTest.isComputable, cLeafTest.isComputable, + polyBounded_branchedSparseCNFDeclaredCertificate_space 3 2 2 2 _ _ + polyBounded_exhBranchCert_space, + polyBounded_branchedSparseCNFLeafCertificate_space 3 2 2 2 _ _ polyBounded_exhBranchCert_space, + cDeclTest.computes, cLeafTest.computes⟩ + +end ComplexityTests.Computability.PolyTime.CNF.BranchedSparseCNFCounter +end