OAI/Combinatorics/ParityLifts/LeafCounts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Sparsification.weighted_split line 9
2. lemma OAI.Sparsification.state_leaves line 29
3. theorem OAI.Sparsification.sparsification_parameter line 85

   Source documentation

   Width-three sparsification, with the explicit branching base and linear leaf density. No sparsification theorem is imported or presumed.

   theorem sparsification_parameter (F : CNF α) (hw : ∀ C ∈ F, C.card ≤ 3)
       (r : ℕ) (hr : 0 < r) : ∃ L : List (CNF α),
         (∀ H ∈ L, Reduced H ∧ (∀ C ∈ H, C.card ≤ 3) ∧
           H.card ≤ 1 + Fintype.card α * (1 + r ^ 2 + 2 * r ^ 8)) ∧
         (∀ v : α → Prop, Holds F v ↔ ∃ H ∈ L, Holds H v) ∧
         (L.length : ℝ) ≤ branchBase r ^ (3 * Fintype.card α * r ^ 2) := by
   …

   Mentions: OAI.Sparsification.CNF, OAI.Sparsification.Reduced, OAI.Sparsification.Holds, OAI.Sparsification.branchBase

4. lemma OAI.Sparsification.branch_base_exponential line 109
5. lemma OAI.Sparsification.indexed_rate_bound line 121
6. theorem OAI.Sparsification.indexed_sparsification line 139