SETH ⇒ OVC sparsification bundle 16: concrete word-RAM formalization

import Definitions.Def_WordRAMEquivalence_Foundation1
import Definitions.Def_WordRAM_Conjectures
import Definitions.Def_WordRAM_SETHOV_Reduction
import Definitions.Def_SETHOV_Sparsification_15

set_option autoImplicit true

/-! Injecting all leaf occurrences into bounded-weight fixed-length bit strings. -/
namespace WordRAM.Conjectures.Sparsification.CodeCount

def pad (length : Nat) (word : List Bool) : List Bool := word ++ List.replicate (length - word.length) false

theorem pad_length (word : List Bool) (bounded : word.length ≤ length) : (pad length word).length = length := by
  simp [pad]
  omega

theorem pad_ones (word : List Bool) (length : Nat) : Codes.ones (pad length word) = Codes.ones word := by
  simp [pad, Codes.ones, List.filter_append]

/-- Padding cannot identify distinct members of a prefix-free family. -/
theorem pad_nodup (words : List (List Bool)) (free : Codes.PrefixFree words) (length : Nat) :
    (words.map (pad length)).Nodup := by
  apply List.pairwise_map.mpr
  apply free.imp
  intro a b apart same
  have aPrefix : List.IsPrefix a (pad length b) := by rw [← same]; exact List.prefix_append _ _
  have bPrefix : List.IsPrefix b (pad length b) := List.prefix_append _ _
  rcases List.prefix_or_prefix_of_prefix aPrefix bPrefix with ab | ba
  · exact apart.1 ab
  · exact apart.2 ba

/-- Enumeration of all bit strings of exactly the requested length. -/
def words : Nat → List (List Bool)
  | 0 => [[]]
  | length + 1 => (words length).map (false :: ·) ++ (words length).map (true :: ·)

theorem mem_words (word : List Bool) (length : Nat) : word ∈ words length ↔ word.length = length := by
  induction length generalizing word with
  | zero => simp [words]
  | succ length ih =>
    cases word with
    | nil => simp [words]
    | cons bit rest => cases bit <;> simp [words, List.mem_map, ih]

def boundedWords (length limit : Nat) : List (List Bool) :=
  (words length).filter (fun word => decide (Codes.ones word ≤ limit))

theorem mem_boundedWords (word : List Bool) (length limit : Nat) :
    word ∈ boundedWords length limit ↔ word.length = length ∧ Codes.ones word ≤ limit := by
  simp only [boundedWords, List.mem_filter, mem_words, decide_eq_true_eq]

/-- Any bounded prefix-free family injects into the fixed-length enumeration. -/
theorem family_count (codes : List (List Bool)) (free : Codes.PrefixFree codes) (length limit : Nat)
    (bounds : ∀ code ∈ codes, code.length ≤ length ∧ Codes.ones code ≤ limit) :
    codes.length ≤ (boundedWords length limit).length := by
  have distinct := pad_nodup codes free length
  have included : codes.map (pad length) ⊆ boundedWords length limit := by
    intro padded member
    obtain ⟨code, present, rfl⟩ := List.mem_map.mp member
    have bound := bounds code present
    exact (mem_boundedWords _ _ _).mpr ⟨pad_length code bound.1, by rw [pad_ones]; exact bound.2⟩
  simpa only [List.length_map] using distinct.length_le_of_subset included

end WordRAM.Conjectures.Sparsification.CodeCount

/-! A natural-number generating-function bound for bounded-weight bit strings. -/
namespace WordRAM.Conjectures.Sparsification.WeightedCount

def zeros (word : List Bool) : Nat := (word.filter (fun bit => !bit)).length

def weight (base : Nat) (word : List Bool) : Nat := base ^ zeros word

theorem zeros_ones (word : List Bool) : zeros word + Codes.ones word = word.length := by
  have partition := Branch.filter_lengths word id
  change Codes.ones word + zeros word = word.length at partition
  omega

theorem sum_mul (items : List α) (f : α → Nat) (base : Nat) :
    (items.map (fun item => base * f item)).sum = base * (items.map f).sum := by
  induction items with
  | nil => simp
  | cons item rest ih => simp [ih, Nat.mul_add]

/-- Sum of B^(number of zeros) over all length-L strings is (B+1)^L. -/
theorem total_weight (base length : Nat) :
    ((CodeCount.words length).map (weight base)).sum = (base + 1) ^ length := by
  induction length with
  | zero => simp [CodeCount.words, weight, zeros]
  | succ length ih =>
    have falseWeight : (fun word => weight base (false :: word)) = fun word => base * weight base word := by
      funext word
      simp [weight, zeros, Nat.pow_succ, Nat.mul_comm]
    have trueWeight : (fun word => weight base (true :: word)) = weight base := by
      funext word
      simp [weight, zeros]
    simp only [CodeCount.words, List.map_append, List.map_map, Function.comp_def, List.sum_append,
      falseWeight, trueWeight, sum_mul, ih]
    simp [Nat.pow_succ, Nat.add_mul, Nat.mul_comm]

theorem filter_sum_le (items : List α) (predicate : α → Bool) (value : α → Nat) :
    ((items.filter predicate).map value).sum ≤ (items.map value).sum := by
  induction items with
  | nil => simp
  | cons item rest ih =>
    cases eq : predicate item <;> simp [eq] <;> omega

theorem length_mul_le_sum (items : List α) (value : α → Nat) (lower : Nat)
    (bounded : ∀ item ∈ items, lower ≤ value item) : items.length * lower ≤ (items.map value).sum := by
  induction items with
  | nil => simp
  | cons item rest ih =>
    have first := bounded item (by simp)
    have later := ih (fun a ha => bounded a (by simp [ha]))
    simp only [List.length_cons, Nat.add_mul, Nat.one_mul, List.map_cons, List.sum_cons]
    omega

/-- A weighted counting bound expressed entirely in natural-number arithmetic.
It can later be combined with an upper bound on (B+1)^L. -/
theorem count_bound (base length limit : Nat) (positive : 1 ≤ base) :
    (CodeCount.boundedWords length limit).length * base ^ (length - limit) ≤ (base + 1) ^ length := by
  have lower := length_mul_le_sum (CodeCount.boundedWords length limit) (weight base) (base ^ (length - limit))
    (by
      intro word member
      have properties := (CodeCount.mem_boundedWords word length limit).mp member
      have counts := zeros_ones word
      apply Nat.pow_le_pow_right (by omega : 0 < base)
      omega)
  have upper := filter_sum_le (CodeCount.words length) (fun word => decide (Codes.ones word ≤ limit)) (weight base)
  rw [total_weight] at upper
  exact Nat.le_trans lower upper

/-- A finite geometric estimate, avoiding rational numbers and limits. -/
theorem power_ratio (base exponent : Nat) (bounded : exponent ≤ base) :
    (base - exponent) * (base + 1) ^ exponent ≤ base ^ (exponent + 1) := by
  induction exponent with
  | zero => simp
  | succ exponent ih =>
    have previous := ih (by omega)
    have step : (base - (exponent + 1)) * (base + 1) ≤ base * (base - exponent) := by
      have difference : base - exponent = (base - (exponent + 1)) + 1 := by omega
      rw [difference, Nat.mul_add, Nat.mul_add, Nat.mul_one, Nat.mul_one]
      rw [Nat.mul_comm (base - (exponent + 1)) base]
      omega
    calc
      (base - (exponent + 1)) * (base + 1) ^ (exponent + 1)
          = ((base - (exponent + 1)) * (base + 1)) * (base + 1) ^ exponent := by
            simp [Nat.pow_succ, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm]
      _ ≤ (base * (base - exponent)) * (base + 1) ^ exponent := Nat.mul_le_mul_right _ step
      _ = base * ((base - exponent) * (base + 1) ^ exponent) := Nat.mul_assoc _ _ _
      _ ≤ base * base ^ (exponent + 1) := Nat.mul_le_mul_left _ previous
      _ = base ^ (exponent + 1 + 1) := by simp [Nat.pow_succ, Nat.mul_comm]

/-- A block of at most B/2 bits has generating weight at most twice B^length. -/
theorem block_bound (base length : Nat) (positive : 0 < base) (bounded : 2 * length ≤ base) :
    (base + 1) ^ length ≤ 2 * base ^ length := by
  have ratio := power_ratio base length (by omega)
  have denominator : base ≤ 2 * (base - length) := by omega
  have first := Nat.mul_le_mul_right ((base + 1) ^ length) denominator
  have second := Nat.mul_le_mul_left 2 ratio
  have combined : base * (base + 1) ^ length ≤ base * (2 * base ^ length) := by
    calc
      base * (base + 1) ^ length ≤ (2 * (base - length)) * (base + 1) ^ length := first
      _ = 2 * ((base - length) * (base + 1) ^ length) := Nat.mul_assoc _ _ _
      _ ≤ 2 * base ^ (length + 1) := second
      _ = base * (2 * base ^ length) := by simp [Nat.pow_succ, Nat.mul_assoc, Nat.mul_comm]
  exact Nat.le_of_mul_le_mul_left combined positive

end WordRAM.Conjectures.Sparsification.WeightedCount

/-! Block bounds on leaf counts, with no real arithmetic. -/
namespace WordRAM.Conjectures.Sparsification.Blocks

theorem cancel_weight (count base length limit factor : Nat) (positive : 0 < base)
    (weighted : count * base ^ (length - limit) ≤ factor * base ^ length) :
    count ≤ factor * base ^ limit := by
  have exponent : length ≤ length - limit + limit := by omega
  have lower := Nat.mul_le_mul_left count (Nat.pow_le_pow_right positive exponent)
  have upper := Nat.mul_le_mul_right (base ^ limit) weighted
  rw [Nat.pow_add] at lower
  have combined : count * base ^ length ≤ (factor * base ^ limit) * base ^ length := by
    apply Nat.le_trans lower
    simpa only [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using upper
  exact Nat.le_of_mul_le_mul_right combined (Nat.pow_pos positive)

theorem block_count (base block blocks limit : Nat) (positive : 0 < base) (sizeBound : 2 * block ≤ base) :
    (CodeCount.boundedWords (block * blocks) limit).length ≤ 2 ^ blocks * base ^ limit := by
  have weighted := WeightedCount.count_bound base (block * blocks) limit positive
  have blockBound := WeightedCount.block_bound base block positive sizeBound
  have raised := Nat.pow_le_pow_left blockBound blocks
  have total : (base + 1) ^ (block * blocks) ≤ 2 ^ blocks * base ^ (block * blocks) := by
    simpa only [Nat.pow_mul, Nat.mul_pow] using raised
  exact cancel_weight _ base _ limit _ positive (Nat.le_trans weighted total)

theorem cover_variables (a n : Nat) (positive : 0 < a) : n ≤ a * (n / a + 1) := by
  have remainder := Nat.mod_lt n positive
  have division := Nat.mod_add_div n a
  rw [Nat.mul_add, Nat.mul_one]
  omega

/-- An explicit block estimate for the actual leaf count. -/
theorem leaf_count (a : Nat) (positive : 1 ≤ a) (formula : CNF n) (k : Nat) :
    (Tree.leaves formula (Thresholds.threshold a) k (Thresholds.threshold_large a positive)).length ≤
      2 ^ (n / a + 1) * (2 * (Thresholds.cumulative a k * a) + 1) ^ (k * (n / a + 1)) := by
  let codes := (Codes.leaves formula (Thresholds.threshold a) k (Thresholds.threshold_large a positive)).map Prod.fst
  let block := Thresholds.cumulative a k * a
  let blocks := n / a + 1
  have cover := cover_variables a n positive
  have lengthBound : Thresholds.cumulative a k * n ≤ block * blocks := by
    exact Nat.le_trans (Nat.mul_le_mul_left _ cover) (Nat.le_of_eq (Nat.mul_assoc _ _ _).symm)
  have bounded := CodeCount.family_count codes
    (Codes.prefix_free formula (Thresholds.threshold a) k (Thresholds.threshold_large a positive))
    (block * blocks) (k * blocks) (by
      intro code member
      obtain ⟨entry, present, rfl⟩ := List.mem_map.mp member
      have bound := Codes.bounds a positive formula k present
      exact ⟨Nat.le_trans bound.1 lengthBound, Nat.le_trans bound.2 (Nat.mul_le_mul_left _ (by omega))⟩)
  have count := Codes.code_count formula (Thresholds.threshold a) k (Thresholds.threshold_large a positive)
  rw [← count]
  exact Nat.le_trans bounded (block_count (2 * block + 1) block blocks (k * blocks) (by omega) (by omega))

end WordRAM.Conjectures.Sparsification.Blocks

/-! Polynomial growth in the tuning parameter, with fixed clause width. -/
namespace WordRAM.Conjectures.Sparsification.Growth

def measure (a i : Nat) : Nat := Thresholds.cumulative a i + Thresholds.coefficient a i + Thresholds.threshold a i + 2

theorem measure_positive (a i : Nat) : 1 ≤ measure a i := by unfold measure; omega

theorem measure_step (a : Nat) (positive : 1 ≤ a) (i : Nat) :
    measure a (i + 1) ≤ (8 * a) * (measure a i * measure a i) := by
  let s := measure a i
  have cum : Thresholds.cumulative a (i + 1) + 2 ≤ s := by
    rw [Thresholds.prefix_succ]
    dsimp [s, measure]
    omega
  have cap : 2 * Thresholds.threshold a i - 1 ≤ 2 * s := by
    dsimp [s, measure]
    omega
  have coeff : Thresholds.coefficient a (i + 1) ≤ 2 * s * s := by
    rw [Thresholds.coefficient_succ]
    exact Nat.mul_le_mul cap (by omega)
  have thresh : Thresholds.threshold a (i + 1) ≤ a * (2 * s * s) := by
    rw [Thresholds.threshold_succ]
    exact Nat.mul_le_mul_left a coeff
  have small : Thresholds.cumulative a (i + 1) + 2 ≤ s * s :=
    Nat.le_trans cum (Nat.le_mul_of_pos_right _ (measure_positive a i))
  calc
    measure a (i + 1) = (Thresholds.cumulative a (i + 1) + 2) +
        Thresholds.coefficient a (i + 1) + Thresholds.threshold a (i + 1) := by
      simp [measure, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
    _ ≤ s * s + 2 * s * s + a * (2 * s * s) := Nat.add_le_add (Nat.add_le_add small coeff) thresh
    _ = (3 + 2 * a) * (s * s) := by
      simp [Nat.add_mul, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm]
      omega
    _ ≤ (8 * a) * (s * s) := Nat.mul_le_mul_right _ (by omega)

theorem measure_bound (a : Nat) (positive : 1 ≤ a) (i : Nat) :
    measure a i ≤ (8 * a) ^ (3 ^ i) := by
  induction i with
  | zero =>
    change 0 + 0 + 2 + 2 ≤ (8 * a) ^ (3 ^ 0)
    simp only [Nat.pow_zero, Nat.pow_one]
    omega
  | succ i ih =>
    have step := measure_step a positive i
    have square := Nat.mul_le_mul ih ih
    have powerPositive : 1 ≤ 3 ^ i := Nat.pow_pos (by decide)
    calc
      measure a (i + 1) ≤ (8 * a) * (measure a i * measure a i) := step
      _ ≤ (8 * a) * ((8 * a) ^ (3 ^ i) * (8 * a) ^ (3 ^ i)) := Nat.mul_le_mul_left _ square
      _ = (8 * a) ^ (1 + (3 ^ i + 3 ^ i)) := by rw [Nat.pow_add, Nat.pow_one, Nat.pow_add]
      _ ≤ (8 * a) ^ (3 ^ (i + 1)) := by
        apply Nat.pow_le_pow_right (by omega : 0 < 8 * a)
        rw [Nat.pow_succ]
        omega

theorem base_bound (a : Nat) (positive : 1 ≤ a) (k : Nat) :
    2 * (Thresholds.cumulative a k * a) + 1 ≤ (8 * a) ^ (3 ^ k + 2) := by
  have cum : Thresholds.cumulative a k ≤ (8 * a) ^ (3 ^ k) :=
    Nat.le_trans (by unfold measure; omega) (measure_bound a positive k)
  have product : Thresholds.cumulative a k * a ≤ (8 * a) ^ (3 ^ k + 1) := by
    rw [Nat.pow_succ]
    exact Nat.mul_le_mul cum (by omega)
  have powerPositive : 1 ≤ (8 * a) ^ (3 ^ k + 1) := Nat.pow_pos (by omega)
  have triple : 2 * (Thresholds.cumulative a k * a) + 1 ≤ 3 * (8 * a) ^ (3 ^ k + 1) := by omega
  calc
    2 * (Thresholds.cumulative a k * a) + 1 ≤ 3 * (8 * a) ^ (3 ^ k + 1) := triple
    _ ≤ (8 * a) * (8 * a) ^ (3 ^ k + 1) := Nat.mul_le_mul_right _ (by omega)
    _ = (8 * a) ^ (3 ^ k + 2) := by rw [Nat.pow_succ]; exact Nat.mul_comm _ _

/-- Choosing a power of two turns the polynomial base bound into an explicit exponent. -/
theorem power_two_base (t k : Nat) :
    2 * (Thresholds.cumulative (2 ^ t) k * 2 ^ t) + 1 ≤ 2 ^ ((t + 3) * (3 ^ k + 2)) := by
  have bound := base_bound (2 ^ t) (Nat.pow_pos (by decide)) k
  have eq : 8 * 2 ^ t = 2 ^ (t + 3) := by rw [Nat.pow_add]; exact Nat.mul_comm _ _
  rw [eq, ← Nat.pow_mul] at bound
  exact bound

end WordRAM.Conjectures.Sparsification.Growth

/-! Explicit choice of tuning parameter yielding arbitrarily small leaf exponents. -/
namespace WordRAM.Conjectures.Sparsification.Exponent

def rate (t k : Nat) : Nat := 1 + k * ((t + 3) * (3 ^ k + 2))

theorem leaf_exponent (t k : Nat) (formula : CNF n) :
    (Tree.leaves formula (Thresholds.threshold (2 ^ t)) k
      (Thresholds.threshold_large (2 ^ t) (Nat.pow_pos (by decide)))).length ≤
      2 ^ ((n / 2 ^ t + 1) * rate t k) := by
  have bound := Blocks.leaf_count (2 ^ t) (Nat.pow_pos (by decide)) formula k
  have baseBound := Growth.power_two_base t k
  have raised := Nat.pow_le_pow_left baseBound (k * (n / 2 ^ t + 1))
  apply Nat.le_trans bound
  apply Nat.le_trans (Nat.mul_le_mul_left _ raised)
  apply Nat.le_of_eq
  rw [← Nat.pow_mul, ← Nat.pow_add]
  congr 1
  simp [rate, Nat.mul_add, Nat.add_mul, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm]

theorem square_le_power (m : Nat) (large : 4 ≤ m) : m * m ≤ 2 ^ m := by
  induction m with
  | zero => omega
  | succ m ih =>
    by_cases previous : 4 ≤ m
    · have old := ih previous
      have quadratic := Nat.mul_le_mul_right m (by omega : 3 ≤ m)
      have growth : (m + 1) * (m + 1) ≤ 2 * (m * m) := by
        simp only [Nat.add_mul, Nat.mul_add, Nat.one_mul, Nat.mul_one]
        omega
      exact Nat.le_trans growth (by simpa only [Nat.pow_succ, Nat.mul_comm] using Nat.mul_le_mul_left 2 old)
    · have hm : m = 3 := by omega
      subst hm
      decide

def tuningExponent (r k : Nat) : Nat := 2 * r * (1 + k * (3 ^ k + 2)) + 4

def tuning (r k : Nat) : Nat := 2 ^ tuningExponent r k

theorem tuning_positive (r k : Nat) : 1 ≤ tuning r k := Nat.pow_pos (by decide)

theorem tuning_rate (r k : Nat) : 2 * r * rate (tuningExponent r k) k ≤ tuning r k := by
  let c := 2 * r * (1 + k * (3 ^ k + 2))
  let t := c + 4
  have rateBound : rate t k ≤ (1 + k * (3 ^ k + 2)) * (t + 3) := by
    calc
      rate t k = 1 + (k * (3 ^ k + 2)) * (t + 3) := by simp [rate, Nat.mul_assoc, Nat.mul_comm]
      _ ≤ (t + 3) + (k * (3 ^ k + 2)) * (t + 3) := Nat.add_le_add_right (by omega) _
      _ = (1 + k * (3 ^ k + 2)) * (t + 3) := by rw [Nat.add_mul, Nat.one_mul]
  have first : 2 * r * rate t k ≤ c * (t + 3) := by
    simpa only [c, Nat.mul_assoc] using Nat.mul_le_mul_left (2 * r) rateBound
  have second : c * (t + 3) ≤ t * t := by
    dsimp only [t]
    simp only [Nat.mul_add, Nat.add_mul]
    omega
  exact Nat.le_trans first (Nat.le_trans second (square_le_power t (by dsimp [t]; omega)))

theorem exponent_small (a rate r n : Nat) (positive : 0 < a) (large : a ≤ n)
    (scaled : 2 * r * rate ≤ a) : (n / a + 1) * rate * r ≤ n := by
  have quotientPositive : 1 ≤ n / a := (Nat.le_div_iff_mul_le positive).mpr (by simpa using large)
  have doubled : n / a + 1 ≤ 2 * (n / a) := by omega
  calc
    (n / a + 1) * rate * r ≤ (2 * (n / a)) * rate * r := Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ doubled)
    _ = (n / a) * (2 * r * rate) := by simp [Nat.mul_comm, Nat.mul_left_comm]
    _ ≤ (n / a) * a := Nat.mul_le_mul_left _ scaled
    _ ≤ n := Nat.div_mul_le_self _ _

/-- For every requested reciprocal exponent r, the chosen algorithm eventually
has at most 2^(n/r) leaves, expressed without fractional exponentiation. -/
theorem leaf_count_power (r k : Nat) (formula : CNF n) (large : tuning r k ≤ n) :
    (Tree.leaves formula (Thresholds.threshold (tuning r k)) k
      (Thresholds.threshold_large (tuning r k) (tuning_positive r k))).length ^ r ≤ 2 ^ n := by
  have count := leaf_exponent (tuningExponent r k) k formula
  have powered := Nat.pow_le_pow_left count r
  rw [← Nat.pow_mul] at powered
  exact Nat.le_trans powered (Nat.pow_le_pow_right (by decide)
    (exponent_small (tuning r k) (rate (tuningExponent r k) k) r n (tuning_positive r k) large (tuning_rate r k)))

end WordRAM.Conjectures.Sparsification.Exponent

/-! Complete combinatorial sparsification: a computable family of sparse formulas,
assignment preservation, and an arbitrarily small exponential leaf bound.
This module does not claim a wordRAM implementation or a machine time bound. -/
namespace WordRAM.Conjectures.Sparsification.Combinatorial

def output (r k : Nat) (formula : CNF n) : List (CNF n) :=
  Tree.leaves formula (Thresholds.threshold (Exponent.tuning r k)) k
    (Thresholds.threshold_large (Exponent.tuning r k) (Exponent.tuning_positive r k))

def occurrenceBound (r k : Nat) : Nat := (8 * Exponent.tuning r k) ^ (3 ^ k)

def density (r k : Nat) : Nat := 2 * (k * occurrenceBound r k)

theorem occurrence_positive (r k : Nat) : 1 ≤ occurrenceBound r k := by
  have positive := Exponent.tuning_positive r k
  exact Nat.pow_pos (by omega)

theorem threshold_bound (r k i : Nat) (bounded : i ≤ k) :
    Thresholds.threshold (Exponent.tuning r k) i ≤ occurrenceBound r k := by
  have first : Thresholds.threshold (Exponent.tuning r k) i ≤ Growth.measure (Exponent.tuning r k) i := by
    unfold Growth.measure
    omega
  have second := Growth.measure_bound (Exponent.tuning r k) (Exponent.tuning_positive r k) i
  have exponent := Nat.pow_le_pow_right (by decide : 0 < 3) bounded
  have third := Nat.pow_le_pow_right (by have := Exponent.tuning_positive r k; omega : 0 < 8 * Exponent.tuning r k) exponent
  exact Nat.le_trans first (Nat.le_trans second third)

theorem density_positive (r k : Nat) (positive : 1 ≤ k) : 1 ≤ density r k :=
  Nat.mul_pos (by decide) (Nat.mul_pos positive (occurrence_positive r k))

theorem sparse_outputs (r k : Nat) (formula : CNF n) (width : ∀ clause ∈ formula, clause.length ≤ k) :
    ∀ leaf ∈ output r k formula,
      (∀ clause ∈ leaf, clause.length ≤ k) ∧ leaf.length ≤ density r k * n := by
  exact Tree.leaves_bounds formula _ k (occurrenceBound r k)
    (Thresholds.threshold_large _ (Exponent.tuning_positive r k)) (occurrence_positive r k)
    (fun i _ smaller => threshold_bound r k i (Nat.le_of_lt smaller)) width

theorem leaf_bound (r k : Nat) (formula : CNF n) (large : Exponent.tuning r k ≤ n) :
    (output r k formula).length ^ r ≤ 2 ^ n := Exponent.leaf_count_power r k formula large

end WordRAM.Conjectures.Sparsification.Combinatorial