Levin's Universal One-Way Function

import Mathlib.Probability.Distributions.Uniform
import Mathlib.Data.Fintype.BigOperators
import Onewayf.Adversary
import Onewayf.OneWayFunction
import Onewayf.Bitstrings

-- leandown
-- [meta]
-- title = "Levin's Universal One-Way Function"
-- group = "Cryptography"
-- [content]

-- # Background
--
-- A natural question in cryptography: if one-way functions exist, which ones?
-- Could there be a **single** function that is hard to invert whenever *any*
-- OWF exists?
--
-- **Levin's theorem** (1987) answers yes.  Given an effective enumeration
-- $\varphi_0, \varphi_1, \ldots$ of all poly-time computable functions,
-- define a single function $f_L$ that encodes an index into its input and
-- runs the corresponding $\varphi_i$ on the remainder.  If any component
-- $\varphi_{i^*}$ is a one-way function, then $f_L$ is also a one-way function.
--
-- The key insight is a **coupling argument**: any adversary inverting $f_L$
-- on a random $n$-bit input is, averaged over the $2^k$ possible $k$-bit
-- prefixes (indices), also inverting *some* $\varphi_i$ on the suffix.
-- Since the set of indices is finite, an infinite pigeonhole argument
-- produces a *fixed* index $i^*$ whose component is non-negligibly invertible.

-- # {{definition}}: Effective enumeration
--
-- An **effective enumeration** at prefix length $k$ assigns to each bit string
-- $i$ (interpreted as a $k$-bit index) a poly-time function
-- $\varphi_i : \{0,1\}^* \to \{0,1\}^*$.
--
-- We use raw `BitString` for indices so that `z.take k` serves directly as a
-- lookup key — the same idiom used by `fPrime` in the quadratic-OWF construction.
-- The **completeness** axiom says every poly-time function appears at the image
-- of some `FixedBitString k` element under `.toList`.
--
structure EffectiveEnum (k : ℕ) : Type where
  /-- The enumerated family, indexed by a raw bit string (typically `z.take k`). -/
  fn       : BitString → BitString → BitString
  /-- Every fixed-length index gives a poly-time function. -/
  polytime : ∀ i : FixedBitString k, PolyTimeComputable (fn i.toList)
  /-- The universal computation `z ↦ fn (z.take k) (z.drop k)` is itself poly-time.
      This is the "universal machine" axiom: running the enumeration on an encoded
      (index, input) pair is no harder than running any single component. -/
  universal : PolyTimeComputable (fun z => fn (z.take k) (z.drop k))
  /-- Completeness: every poly-time function appears at some $k$-bit index. -/
  complete : ∀ f : BitString → BitString, PolyTimeComputable f →
               ∃ i : FixedBitString k, ∀ x, fn i.toList x = f x

-- # {{definition}}: Levin's universal OWF
--
-- Split any input $z$ into a $k$-bit **index** prefix $i = z_{[0:k]}$ and
-- a **data** suffix $x = z_{[k:]}$.  Output:
--
-- $$f_L(z) \;=\; z_{[0:k]} \;\|\; \varphi_{z_{[0:k]}}(x)$$
--
-- The output preserves the first $k$ bits verbatim.  Crucially, this means
-- that inverting $f_L(z)$ on a target $y = i \| y'$ forces the inverter to
-- produce a preimage of $y'$ under $\varphi_i$ — the inversion condition
-- $f_L(z') = f_L(z)$ implies $z'_{[0:k]} = z_{[0:k]}$ (since both sides
-- share the same $k$-bit prefix) and then $\varphi_i(z'_{[k:]}) = \varphi_i(x)$.
--
noncomputable def levinOWF (ee : EffectiveEnum k) : BitString → BitString :=
  -- take the first k bits as the index; apply the indexed function to the rest
  fun z => z.take k ++ ee.fn (z.take k) (z.drop k)

-- [hidden: levinOWF unfolding lemma]
-- On a `FixedBitString n` input with `k ≤ n`, `levinOWF` reduces cleanly.
private lemma levinOWF_apply (ee : EffectiveEnum k) (n : ℕ) (_hkn : k ≤ n)
    (z : FixedBitString n) :
    levinOWF ee z.toList = z.toList.take k ++ ee.fn (z.toList.take k) (z.toList.drop k) :=
  rfl

-- Indicator dominance: if `levinOWF ee z'` inverts at `(i, x)` and `z'.length = n`,
-- then the suffix `z'.drop k` inverts `ee.fn i.toList` at `x.toList`.
-- Proof: concat-injectivity forces `z'.take k = i.toList`, giving the suffix condition.
private lemma levinOWF_success_implies_suffix (ee : EffectiveEnum k) (n : ℕ)
    (hkn : k ≤ n) (i : FixedBitString k) (x : FixedBitString (n - k)) (z' : BitString) :
    (if levinOWF ee z' = i.toList ++ ee.fn i.toList x.toList ∧ z'.length = n
     then (1 : ENNReal) else 0) ≤
    (if ee.fn i.toList (z'.drop k) = ee.fn i.toList x.toList ∧
        (z'.drop k).length = n - k
     then (1 : ENNReal) else 0) := by
  -- case split on whether the levinOWF inversion condition holds
  by_cases h : levinOWF ee z' = i.toList ++ ee.fn i.toList x.toList ∧ z'.length = n
  · simp only [if_pos h]
    -- unfold levinOWF so h.1 reads:
    -- z'.take k ++ ee.fn (z'.take k) (z'.drop k) = i.toList ++ ee.fn i.toList x.toList
    simp only [levinOWF] at h
    -- z'.take k has exactly k elements since z'.length = n ≥ k
    have htake_len : (z'.take k).length = k :=
      by simp [List.length_take, Nat.min_eq_left (h.2 ▸ hkn)]
    -- concat-injectivity: z'.take k = i.toList  AND  ee.fn (z'.take k) ... = ee.fn i.toList ...
    have hinj := List.append_inj h.1 (htake_len.trans i.toList_length.symm)
    -- substitute z'.take k = i.toList into hinj.2 to get the suffix condition
    rw [if_pos ⟨hinj.1 ▸ hinj.2, by simp [List.length_drop, h.2]⟩]
  · simp [if_neg h]

-- Bijection splitting a length-n bit string into a k-bit prefix and (n-k)-bit suffix.
private def splitN (k n : ℕ) (hkn : k ≤ n) :
    FixedBitString n ≃ FixedBitString k × FixedBitString (n - k) where
  toFun v :=
    ⟨⟨v.toList.take k, by have h := v.toList_length; simp [List.length_take]; omega⟩,
     ⟨v.toList.drop k, by have h := v.toList_length; simp [List.length_drop, h]⟩⟩
  invFun p :=
    ⟨p.1.toList ++ p.2.toList, by
      have h1 := p.1.toList_length; have h2 := p.2.toList_length
      simp only [List.length_append, h1, h2, Nat.add_sub_cancel' hkn]⟩
  left_inv v := List.Vector.ext (by simp [List.take_append_drop])
  right_inv p := by
    rcases p with ⟨a, b⟩; apply Prod.ext <;> apply List.Vector.ext
    all_goals simp [a.toList_length]

-- The uniform measure on FixedBitString n splits over splitN:
-- uniform(n)(splitN.symm(i,x)) = uniform(k)(i) * uniform(n-k)(x)
private lemma uniform_split (k n : ℕ) (hkn : k ≤ n)
    (i : FixedBitString k) (x : FixedBitString (n - k)) :
    PMF.uniformOfFintype (FixedBitString n) ((splitN k n hkn).symm (i, x)) =
    PMF.uniformOfFintype (FixedBitString k) i *
    PMF.uniformOfFintype (FixedBitString (n - k)) x := by
  simp only [PMF.uniformOfFintype_apply]
  rw [show Fintype.card (FixedBitString n) =
        Fintype.card (FixedBitString k) * Fintype.card (FixedBitString (n - k)) from by
    simp [← pow_add, Nat.add_sub_cancel' hkn]]
  push_cast
  rw [ENNReal.mul_inv (Or.inl (by positivity)) (Or.inr (by positivity))]

-- Scaling: 2^k * uniform(n)(splitN.symm(i,x)) = uniform(n-k)(x)
-- Because 2^k * (1/2^k * 1/2^(n-k)) = 1/2^(n-k).
private lemma two_pow_mul_uniform (k n : ℕ) (hkn : k ≤ n)
    (i : FixedBitString k) (x : FixedBitString (n - k)) :
    (2 : ENNReal) ^ k *
    PMF.uniformOfFintype (FixedBitString n) ((splitN k n hkn).symm (i, x)) =
    PMF.uniformOfFintype (FixedBitString (n - k)) x := by
  rw [uniform_split k n hkn i x, ← mul_assoc]
  -- 2^k * uniform(k)(i) = 1 since uniform(k)(i) = 1/2^k
  have h2k : (2 : ENNReal) ^ k * PMF.uniformOfFintype (FixedBitString k) i = 1 := by
    simp [PMF.uniformOfFintype_apply]
    rw [ENNReal.mul_inv_cancel (by positivity) (by simp)]
  rw [h2k, one_mul]
-- [/hidden]

-- # {{definition}}: The suffix adversary
--
-- Given an adversary $A$ that tries to invert $f_L$, and a fixed index $i^*$,
-- the **suffix adversary** $B_{i^*}$ attacks $\varphi_{i^*}$ directly:
--
-- $$B_{i^*}(y') \;=\; \bigl(A(i^* \| y')\bigr).\mathrm{drop}(k)$$
--
-- On input $y' = \varphi_{i^*}(x)$, $B_{i^*}$ presents the $f_L$-formatted
-- challenge $i^* \| y'$ to $A$, then strips the $k$-bit prefix from $A$'s
-- output to obtain a candidate preimage of $y'$ under $\varphi_{i^*}$.
--
-- If $A$ succeeds — returning $z'$ with $f_L(z') = i^* \| y'$ and $|z'| = n$
-- — then the output prefix is forced to equal $i^*$ (since $f_L$ preserves
-- the first $k$ bits), so the stripped suffix $z'.\mathrm{drop}(k)$ has
-- length $n - k$ and satisfies $\varphi_{i^*}(z'.\mathrm{drop}(k)) = y'$.
--
noncomputable def suffixAdv (A : BitString → PMF BitString) (k : ℕ) (i : FixedBitString k)
    : BitString → PMF BitString :=
  -- prepend the fixed index to the challenge; run A; strip the k-bit prefix
  fun y => (A (i.toList ++ y)).map (·.drop k)

-- Fubini for suffixAdv: ∑' x', suffixAdv A k i y x' * c(x') = ∑' z, A(i++y)(z) * c(z.drop k)
private lemma suffixAdv_indicator_eq (A : BitString → PMF BitString) (k : ℕ) (i : FixedBitString k)
    (g : BitString → BitString) (y fy : BitString) (r : ℕ) :
    (∑' x' : BitString, suffixAdv A k i y x' *
      (if g x' = fy ∧ x'.length = r then (1 : ENNReal) else 0)) =
    ∑' z : BitString, A (i.toList ++ y) z *
      (if g (z.drop k) = fy ∧ (z.drop k).length = r then 1 else 0) := by
  simp only [suffixAdv, PMF.map_apply]
  simp_rw [← ENNReal.tsum_mul_right]
  rw [ENNReal.tsum_comm]
  apply tsum_congr; intro z
  -- the sum ∑' a, (if a = z.drop k then A(i++y)(z) else 0) * c(a) has one nonzero term
  rw [tsum_eq_single (z.drop k) (by intro a ha; simp [ha])]
  simp

-- ENNReal body of invertProb is ≤ 1 (hence ≠ ⊤)
private lemma invertProb_body_le_one (f : BitString → BitString)
    (F : BitString → PMF BitString) (n : ℕ) :
    (∑ x : FixedBitString n,
      PMF.uniformOfFintype (FixedBitString n) x *
      (∑' x' : BitString, F (f x.toList) x' *
        (if f x' = f x.toList ∧ x'.length = n then (1 : ENNReal) else 0))) ≤ 1 := by
  calc _ ≤ ∑ x : FixedBitString n, PMF.uniformOfFintype (FixedBitString n) x := by
        apply Finset.sum_le_sum; intro x _
        -- bound: a * b ≤ a when b ≤ 1
        apply mul_le_of_le_one_right (zero_le _)
        calc ∑' x', F (f x.toList) x' * (if f x' = f x.toList ∧ x'.length = n then 1 else 0)
            ≤ ∑' x', F (f x.toList) x' := by
              apply ENNReal.tsum_le_tsum; intro x'
              exact mul_le_of_le_one_right (zero_le _) (by split_ifs <;> norm_num)
          _ = 1 := PMF.tsum_coe _
     _ = 1 := by
        have h := (PMF.uniformOfFintype (FixedBitString n)).tsum_coe
        rw [tsum_fintype (L := .unconditional _)] at h; exact h

-- # {{lemma}}: Suffix adversary is poly-time
--
-- If $A$ is a poly-time adversary, then $B_{i^*}$ is also poly-time:
-- prepending a fixed string and stripping a fixed prefix are both $O(k)$.
--
lemma suffixAdv_polytime (A : BitString → PMF BitString) (hA : PolyTimeAdversary A)
    (k : ℕ) (i : FixedBitString k) : PolyTimeAdversary (suffixAdv A k i) := by
  -- unfold `suffixAdv` to expose the fixed-prefix map pattern
  unfold suffixAdv
  -- `fixedPad` exactly captures: prepend a fixed prefix, run A, strip k bits
  exact PolyTimeAdversary.fixedPad i.toList k hA

-- # {{lemma}}: The coupling inequality
--
-- The sum of component inversion probabilities dominates the $f_L$ inversion
-- probability, scaled by $2^k$:
--
-- $$\sum_{i \in \{0,1\}^k} \mathrm{invertProb}(\varphi_i,\, B_i,\, n-k)
--   \;\geq\; 2^k \cdot \mathrm{invertProb}(f_L,\, A,\, n)$$
--
-- **Proof sketch.**  Reindex the sum defining $\mathrm{invertProb}(f_L, A, n)$
-- over $\{0,1\}^k \times \{0,1\}^{n-k}$ (prefix $i$, data $x$).  The $f_L$-
-- inversion indicator $[f_L(z') = i \| \varphi_i(x) \wedge |z'| = n]$
-- forces $z'_{[0:k]} = i$, so it collapses to
-- $[\varphi_i(z'_{[k:]}) = \varphi_i(x) \wedge |z'_{[k:]}| = n-k]$.
-- Summing the mass $A(i \| \varphi_i(x))(z')$ over all $z'$ with
-- $z'_{[k:]} = x'$ gives $(A(\ldots).\mathrm{map\;drop}_k)(x')$, which is
-- exactly $B_i(\varphi_i(x))(x')$.  Summing over $i$ and normalizing yields
-- the stated bound.
--
lemma levinOWF_coupling (ee : EffectiveEnum k) (A : BitString → PMF BitString)
    (n : ℕ) (hkn : k ≤ n) :
    (2 : ℝ) ^ k * invertProb (levinOWF ee) A n ≤
    ∑ i : FixedBitString k,
      invertProb (ee.fn i.toList) (suffixAdv A k i) (n - k) := by
  simp only [invertProb]
  -- abbreviate the ENNReal body on each side
  set E_L : ENNReal := ∑ z : FixedBitString n,
    PMF.uniformOfFintype (FixedBitString n) z *
    (∑' z', A (levinOWF ee z.toList) z' *
      (if levinOWF ee z' = levinOWF ee z.toList ∧ z'.length = n then 1 else 0))
  set E_R : FixedBitString k → ENNReal := fun i =>
    ∑ x : FixedBitString (n - k),
      PMF.uniformOfFintype (FixedBitString (n - k)) x *
      (∑' x', suffixAdv A k i (ee.fn i.toList x.toList) x' *
        (if ee.fn i.toList x' = ee.fn i.toList x.toList ∧ x'.length = n - k then 1 else 0))
  -- finiteness: both sides are ≤ 1, hence ≠ ⊤
  have hEL : E_L ≠ ⊤ := ne_top_of_le_ne_top ENNReal.one_ne_top (invertProb_body_le_one _ _ _)
  have hER : ∀ i, E_R i ≠ ⊤ := fun i =>
    ne_top_of_le_ne_top ENNReal.one_ne_top (invertProb_body_le_one _ _ _)
  -- rewrite LHS: (2:ℝ)^k * E_L.toReal = ((2:ENNReal)^k * E_L).toReal
  rw [show (2 : ℝ) ^ k * E_L.toReal = ((2 : ENNReal) ^ k * E_L).toReal by
    rw [ENNReal.toReal_mul, ENNReal.toReal_pow]; norm_cast]
  -- rewrite RHS: ∑ i, (E_R i).toReal = (∑ i, E_R i).toReal
  rw [show ∑ i : FixedBitString k, (E_R i).toReal = (∑ i, E_R i).toReal by
    rw [ENNReal.toReal_sum (fun i _ => hER i)]]
  -- ne_top facts needed for toReal conversion
  have h2k : (2 : ENNReal) ^ k ≠ ⊤ := by norm_cast; exact ENNReal.natCast_ne_top _
  have hL : (2 : ENNReal) ^ k * E_L ≠ ⊤ := ENNReal.mul_ne_top h2k hEL
  have hR : ∑ i : FixedBitString k, E_R i ≠ ⊤ := ENNReal.sum_ne_top.mpr (fun i _ => hER i)
  -- reduce to the ENNReal inequality via monotonicity of toReal
  rw [ENNReal.toReal_le_toReal hL hR]
  -- *** Main ENNReal inequality: (2:ENNReal)^k * E_L ≤ ∑ i, E_R i ***
  -- distribute 2^k into the FixedBitString n sum
  rw [Finset.mul_sum]
  -- reindex FixedBitString n as FixedBitString k × FixedBitString (n-k) via splitN;
  -- outer sum remains over FixedBitString k, so no sum_comm needed
  rw [← Equiv.sum_comp (splitN k n hkn).symm, Fintype.sum_prod_type]
  -- bound each (i, x) term
  apply Finset.sum_le_sum; intro i _
  apply Finset.sum_le_sum; intro x _
  -- simplify: splitN.symm (i, x) has toList = i.toList ++ x.toList
  simp_rw [show ((splitN k n hkn).symm (i, x)).toList = i.toList ++ x.toList from
    by simp [splitN]]
  -- simplify: levinOWF on a concatenated input = i.toList ++ ee.fn i.toList x.toList
  simp_rw [show levinOWF ee (i.toList ++ x.toList) = i.toList ++ ee.fn i.toList x.toList from
    by simp [levinOWF, List.take_left' i.toList_length, List.drop_left' i.toList_length]]
  -- apply 2^k * uniform(n)(splitN.symm(i,x)) = uniform(n-k)(x), absorbing the scaling
  -- ← mul_assoc: reassociate 2^k * (u * inner) to (2^k * u) * inner
  -- two_pow_mul_uniform: (2^k * u) = uniform(n-k)(x), leaving uniform(n-k)(x) * inner
  rw [← mul_assoc, two_pow_mul_uniform k n hkn i x]
  -- rewrite the RHS suffixAdv tsum to the z'-indexed form first, so both sides share the
  -- same index and the same A(...)(z') factor; then a pointwise comparison closes the goal
  -- suffixAdv_indicator_eq: ∑' x', suffixAdv A k i y x' * ind(x') = ∑' z', A(i++y)(z') * ind(z'.drop k)
  -- (no ← : we want to convert the suffixAdv form in the RHS of ≤ to the z-indexed form)
  rw [suffixAdv_indicator_eq A k i (ee.fn i.toList) (ee.fn i.toList x.toList)
        (ee.fn i.toList x.toList) (n - k)]
  -- now goal: uniform(n-k)(x) * (∑' z', A(...) z' * ind_L z') ≤ uniform(n-k)(x) * (∑' z', A(...) z' * ind_R z')
  -- strip the common uniform(n-k)(x) factor (it is the same on both sides)
  apply mul_le_mul_of_nonneg_left _ (zero_le _)
  -- reduce to a termwise bound under the tsum
  apply ENNReal.tsum_le_tsum; intro z'
  -- both sides share the factor A(...)(z'); bound the indicator
  gcongr
  -- the levinOWF inversion indicator implies the suffix indicator (concat-injectivity)
  exact levinOWF_success_implies_suffix ee n hkn i x z'

-- # {{corollary}}: Some prefix achieves the average
--
-- From the coupling and the fact that $\{0,1\}^k$ has exactly $2^k$ elements,
-- at least one prefix $i \in \{0,1\}^k$ satisfies
--
-- $$\mathrm{invertProb}(\varphi_i,\, B_i,\, n-k) \;\geq\;
--   \mathrm{invertProb}(f_L,\, A,\, n)$$
--
-- **Proof.** If every term were strictly less than the average, the sum would
-- be less than $2^k \cdot \mathrm{invertProb}(f_L,\, A,\, n)$, contradicting
-- the coupling inequality.
--
lemma levinOWF_exists_ge (ee : EffectiveEnum k) (A : BitString → PMF BitString)
    (n : ℕ) (hkn : k ≤ n) :
    ∃ i : FixedBitString k,
      invertProb (levinOWF ee) A n ≤
      invertProb (ee.fn i.toList) (suffixAdv A k i) (n - k) := by
  -- derive the averaging bound from the coupling inequality
  have hsum := levinOWF_coupling ee A n hkn
  -- if no single term meets the average, the finite sum would fall below the
  -- coupling lower bound — contradiction
  by_contra hall
  push_neg at hall
  have hlt : ∑ i : FixedBitString k,
      invertProb (ee.fn i.toList) (suffixAdv A k i) (n - k) <
      (2 : ℝ) ^ k * invertProb (levinOWF ee) A n := by
    calc ∑ i : FixedBitString k, invertProb (ee.fn i.toList) (suffixAdv A k i) (n - k)
        -- every term is strictly below the average invertProb (levinOWF ee) A n
        < ∑ _i : FixedBitString k, invertProb (levinOWF ee) A n :=
            Finset.sum_lt_sum_of_nonempty (by simp) (fun i _ => hall i)
        -- sum of the constant is card * value
      _ = (Fintype.card (FixedBitString k) : ℝ) * invertProb (levinOWF ee) A n := by
            simp [Finset.sum_const, nsmul_eq_mul]
        -- |{0,1}^k| = 2^k
      _ = (2 : ℝ) ^ k * invertProb (levinOWF ee) A n := by
            rw [bitStringCardinality]; push_cast; ring
  linarith

-- # {{theorem}}: Levin's OWF is a universal one-way function
--
-- If any component $\varphi_{i^*}$ of the enumeration is a one-way function,
-- then $f_L$ is also a one-way function.
--
-- **Efficiency.** $f_L$ runs one poly-time index lookup and one poly-time
-- function application, so it is poly-time.
--
-- **Hardness** — Levin's argument.  Suppose $A$ inverts $f_L$ with
-- non-negligible probability $\varepsilon(n) \geq n^{-c}$ for infinitely many
-- $n$.  By `levinOWF_exists_ge`, for each such $n$ there is some
-- $i^*(n) \in \{0,1\}^k$ with
--
-- $$\mathrm{invertProb}(\varphi_{i^*(n)},\, B_{i^*(n)},\, n-k) \geq
--   \varepsilon(n) \geq n^{-c}$$
--
-- Since $|\{0,1\}^k| = 2^k$ is **finite**, the infinite sequence
-- $i^*(n)$ must take some fixed value $i^{**}$ infinitely often (infinite
-- pigeonhole principle).  For that $i^{**}$, the poly-time adversary
-- $B_{i^{**}}$ inverts $\varphi_{i^{**}}$ with probability $\geq n^{-c}$
-- for infinitely many $n$, contradicting $\varphi_{i^{**}}$ being a OWF.
--
theorem levinOWF_is_owf (ee : EffectiveEnum k)
    (hf : ∀ i : FixedBitString k, IsOneWayFunction (ee.fn i.toList)) :
    IsOneWayFunction (levinOWF ee) := by
  constructor
  · -- Efficiency: levinOWF ee z = z.take k ++ ee.fn (z.take k) (z.drop k)
    -- = (take k)(z) ++ (ee.universal)(z)
    -- `append` closes this from `take k` and `ee.universal`
    show PolyTimeComputable (fun z => z.take k ++ ee.fn (z.take k) (z.drop k))
    exact PolyTimeComputable.append (PolyTimeComputable.take k) ee.universal
  · -- Hardness: coupling + finite sum of negligibles argument.
    -- If every component φ_i is a OWF, then for any poly-time adversary A:
    -- 2^k * invertProb(f_L, A, n) ≤ ∑_i invertProb(φ_i, B_i, n-k)
    -- Each term on the right is negligible (by hf i), so the sum is negligible
    -- (finite sum), hence so is invertProb(f_L, A, n).
    intro A hA c
    -- each component adversary is poly-time and each component is a OWF
    have h_comp : ∀ i : FixedBitString k,
        Negligible (invertProb (ee.fn i.toList) (suffixAdv A k i)) :=
      fun i => (hf i).hard (suffixAdv A k i) (suffixAdv_polytime A hA k i)
    -- each shifted component is negligible: ε_i(n) := invertProb(φ_i, B_i, n-k)
    have h_shift : ∀ i : FixedBitString k,
        Negligible (fun n => invertProb (ee.fn i.toList) (suffixAdv A k i) (n - k)) :=
      fun i => negligible_shift _ k (h_comp i)
    -- for exponent c+1, get per-index threshold N_i
    have h_shift_c : ∀ i : FixedBitString k, ∃ N,
        ∀ n ≥ N, invertProb (ee.fn i.toList) (suffixAdv A k i) (n - k) ≤
          (n : ℝ) ^ (-(↑(c + 1) : ℤ)) :=
      fun i => h_shift i (c + 1)
    choose Ni hNi using h_shift_c
    -- threshold: large enough for all indices and for coupling to apply
    refine ⟨Finset.univ.sup Ni + k + 1, fun n hn => ?_⟩
    -- n ≥ k (so levinOWF_coupling applies) and n ≥ Ni i for all i
    have hn_k : k ≤ n := by
      have : Finset.univ.sup Ni + k ≤ n := by omega
      omega
    have hn_Ni : ∀ i : FixedBitString k, Ni i ≤ n := fun i =>
      (Finset.le_sup (f := Ni) (Finset.mem_univ i)).trans (by omega)
    have hn_pos : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast (show 1 ≤ n by omega)
    -- coupling: 2^k * invertProb(f_L, A, n) ≤ ∑_i invertProb(φ_i, B_i, n-k)
    have hcoupling := levinOWF_coupling ee A n hn_k
    -- each term in the sum is ≤ n^{-(c+1)}
    have h_each : ∀ i : FixedBitString k,
        invertProb (ee.fn i.toList) (suffixAdv A k i) (n - k) ≤
          (n : ℝ) ^ (-(↑(c + 1) : ℤ)) :=
      fun i => hNi i n (hn_Ni i)
    -- the sum ≤ 2^k * n^{-(c+1)}
    have h_sum : ∑ i : FixedBitString k,
        invertProb (ee.fn i.toList) (suffixAdv A k i) (n - k) ≤
          (2 : ℝ) ^ k * (n : ℝ) ^ (-(↑(c + 1) : ℤ)) :=
      calc ∑ i : FixedBitString k, invertProb (ee.fn i.toList) (suffixAdv A k i) (n - k)
          ≤ ∑ _i : FixedBitString k, (n : ℝ) ^ (-(↑(c + 1) : ℤ)) :=
            Finset.sum_le_sum (fun i _ => h_each i)
        _ = (Fintype.card (FixedBitString k) : ℝ) * (n : ℝ) ^ (-(↑(c + 1) : ℤ)) := by
            simp [Finset.sum_const, nsmul_eq_mul]
        _ = (2 : ℝ) ^ k * (n : ℝ) ^ (-(↑(c + 1) : ℤ)) := by
            rw [bitStringCardinality]; push_cast; ring
    -- combine: 2^k * invertProb(f_L, A, n) ≤ 2^k * n^{-(c+1)}
    have h_scaled : (2 : ℝ) ^ k * invertProb (levinOWF ee) A n ≤
        (2 : ℝ) ^ k * (n : ℝ) ^ (-(↑(c + 1) : ℤ)) :=
      hcoupling.trans h_sum
    -- divide both sides by 2^k > 0
    have h2k_pos : (0 : ℝ) < (2 : ℝ) ^ k := by positivity
    have h_inv : invertProb (levinOWF ee) A n ≤ (n : ℝ) ^ (-(↑(c + 1) : ℤ)) :=
      le_of_mul_le_mul_left h_scaled h2k_pos
    -- n^{-(c+1)} ≤ n^{-c} since -(c+1) ≤ -c and n ≥ 1
    calc invertProb (levinOWF ee) A n
        ≤ (n : ℝ) ^ (-(↑(c + 1) : ℤ)) := h_inv
      _ ≤ (n : ℝ) ^ (-(↑c : ℤ)) := by
          -- -(↑(c+1) : ℤ) ≤ -(↑c : ℤ) and base n ≥ 1 → zpow is monotone in exponent
          apply zpow_le_zpow_right₀ hn_pos
          push_cast; omega