diff --git a/Complexity.lean b/Complexity.lean
index dba79c39b..c5fa35f23 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1478,6 +1478,7 @@ public import Complexity.Computability.Languages.Slice
 public import Complexity.Computability.MCSP.AntiChecker
 public import Complexity.Computability.MCSP.Basic
 public import Complexity.Computability.MCSP.FormulaMagnification
+public import Complexity.Computability.MCSP.FormulaMagnification.AverageCase
 public import Complexity.Computability.MCSP.FormulaMagnification.StretchedExponential
 public import Complexity.Computability.MCSP.FormulaMagnification.Subexponential
 public import Complexity.Computability.MCSP.HardnessConsequences
diff --git a/Complexity/Computability/MCSP/FormulaMagnification/AverageCase.lean b/Complexity/Computability/MCSP/FormulaMagnification/AverageCase.lean
new file mode 100644
index 000000000..4833a66ab
--- /dev/null
+++ b/Complexity/Computability/MCSP/FormulaMagnification/AverageCase.lean
@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.MCSP.FormulaMagnification.Subexponential
+public import Complexity.Computability.MCSP.SuccinctNP.Words
+
+/-!
+# Subexponential zero-error average-case formula magnification
+
+This module supplies the asymptotic step after the finite one-sided projection in
+`FormulaMagnification`, following [OliveiraSanthanam2018, Section 3.3, Theorem 27, p. 21].
+For subexponential circuit-size and loss schedules, its encoded query length is subexponential.
+Polynomial-size formulas for any binary language agreeing with succinct MCSP therefore give,
+for every positive integer `d` and all sufficiently large `n`, a formula on `N = 2 ^ n` variables
+with at most `2 ^ (n / d)` leaves and the existing one-sided counting guarantee.
+
+These formulas are unknown masks: `true` means unknown, while `false` certifies that the input
+truth table has circuit complexity above the threshold. With loss `r = n`, the unknown fraction
+is at most `2 ^ (-n)`. In particular this is eventually at most the `1 / n` allowance in
+[OliveiraSanthanam2018, Appendix A, Definition 43, p. 34], where `n` is the truth table's arity,
+not its length `N`. The formal statements retain exact natural-number counts.
+
+The quantifier order is `∀ d > 0, ∀ᶠ n, ∃ F`. The lower-bound consequence uses arbitrarily large
+hard lengths at one fixed positive reciprocal exponent. No single simultaneously subexponential
+formula family is inferred from this order. Arbitrary parameter schedules need no computability
+assumption: the single binary NP witness receives the thresholds and samples in its input.
+The concrete rounded `2 ^ (sqrt n)` specialization and a conventional ternary-device formulation
+of Theorem 5 are separate from this asymptotic one-sided result.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.subexponentiallyBounded_avgCaseMCSPQueryEncLength`: closure of the
+  average-case query length under subexponential schedules.
+* `Cslib.Circuits.Boolean.eventually_exists_formula_zero_error_average_case_of_mem_FormulaPoly`:
+  the forward bound with the exact one-sided count.
+* `Cslib.Circuits.Boolean.not_mem_FormulaPoly_of_zero_error_average_case_subexp_hard`: the
+  fixed-exponent lower-bound contrapositive for any agreeing binary language.
+* `Cslib.Circuits.Boolean.exists_NP_not_mem_FormulaPoly_of_zero_error_average_case_subexp_hard`:
+  the corresponding binary NP-language witness.
+
+## References
+
+* [I. C. Oliveira, R. Santhanam, *Hardness Magnification for Natural
+  Problems*][OliveiraSanthanam2018]
+-/
+
+public section
+
+namespace Cslib.Circuits.Boolean
+
+open Filter
+
+/-- The average-case encoded query length is subexponential when both its circuit-size
+threshold and its loss parameter are subexponential. -/
+theorem subexponentiallyBounded_avgCaseMCSPQueryEncLength {s r : ℕ → ℕ}
+    (hs : SubexponentiallyBounded s) (hr : SubexponentiallyBounded r) :
+    SubexponentiallyBounded (fun n => avgCaseMCSPQueryEncLength n (s n) (r n)) := by
+  have hq := (subexponentiallyBounded_computableFunctionsLogBound hs).add hr
+  have h8n : SubexponentiallyBounded (fun n => 8 * n + 10) :=
+    ((SubexponentiallyBounded.const 8).mul SubexponentiallyBounded.id).add (.const 10)
+  have h4n : SubexponentiallyBounded (fun n => 4 * n + 3) :=
+    ((SubexponentiallyBounded.const 4).mul SubexponentiallyBounded.id).add (.const 3)
+  exact (h4n.add (hq.mul h8n)).add hs
+
+open Classical in
+/-- Asymptotic forward form of the finite one-sided projection
+[OliveiraSanthanam2018, Section 3.3, Theorem 27, p. 21]. The formula accepts all small-circuit
+truth tables; its acceptance set is the unknown set of the zero-error device. -/
+theorem eventually_exists_formula_zero_error_average_case_of_mem_FormulaPoly
+    {s r : ℕ → ℕ} (hs : SubexponentiallyBounded s) (hr : SubexponentiallyBounded r)
+    {L : Language Bool} (hag : ∀ x, x ∈ SuccinctMCSP ↔ SuccinctMCSP.enc x ∈ L)
+    (hL : L ∈ FormulaPoly) (d : ℕ) (hd : 0 < d) :
+    ∀ᶠ n in atTop, ∃ F : Formula signature (2 ^ n),
+      F.leafSize ≤ 2 ^ (n / d) ∧
+      (∀ T : BitString (2 ^ n), List.ofFn T ∈ GapMCSP.yesSet s →
+        F.eval interpretation T = true) ∧
+      (Finset.univ.filter fun T : BitString (2 ^ n) =>
+        F.eval interpretation T = true).card ≤ 2 ^ (2 ^ n - r n) := by
+  obtain ⟨c, hc⟩ := mem_FormulaPoly_iff_exists_mem_FormulaSIZE.mp hL
+  have hquery := subexponentiallyBounded_avgCaseMCSPQueryEncLength hs hr
+  have hbound : SubexponentiallyBounded
+      (fun n => c * (avgCaseMCSPQueryEncLength n (s n) (r n) + 1) ^ c) :=
+    (SubexponentiallyBounded.const c).mul ((hquery.add (.const 1)).pow c)
+  have hsample := (subexponentiallyBounded_computableFunctionsLogBound hs).add hr
+  filter_upwards [hsample.eventually_le_two_pow_div 1 (by decide),
+    hbound.eventually_le_two_pow_div d hd] with n hn hsize
+  have ht : computableFunctionsLogBound n (s n) + r n ≤ 2 ^ n := by
+    simpa only [Nat.div_one] using hn
+  obtain ⟨F, hF, hyes, hcard⟩ := exists_formula_zero_error_average_case_of_agrees hag ht
+  exact ⟨F, hF.trans ((hc _).trans hsize), hyes, hcard⟩
+
+open Classical in
+/-- Subexponential-threshold one-sided average-case hardness at arbitrarily large lengths
+rules out polynomial-size formulas for any binary language agreeing with succinct MCSP.
+The loss is `r = n`, so at most a `2 ^ (-n)` fraction of truth tables are unknown. -/
+theorem not_mem_FormulaPoly_of_zero_error_average_case_subexp_hard
+    {s : ℕ → ℕ} (hs : SubexponentiallyBounded s) {d : ℕ} (hd : 0 < d)
+    (hhard : ∀ N : ℕ, ∃ n ≥ N, ∀ F : Formula signature (2 ^ n),
+      (∀ T : BitString (2 ^ n), List.ofFn T ∈ GapMCSP.yesSet s →
+        F.eval interpretation T = true) →
+      (Finset.univ.filter fun T : BitString (2 ^ n) =>
+        F.eval interpretation T = true).card ≤ 2 ^ (2 ^ n - n) →
+      2 ^ (n / d) < F.leafSize)
+    {L : Language Bool} (hag : ∀ x, x ∈ SuccinctMCSP ↔ SuccinctMCSP.enc x ∈ L) :
+    L ∉ FormulaPoly := by
+  intro hL
+  obtain ⟨N, hN⟩ := eventually_atTop.mp
+    (eventually_exists_formula_zero_error_average_case_of_mem_FormulaPoly
+      hs SubexponentiallyBounded.id hag hL d hd)
+  obtain ⟨n, hn, hhardn⟩ := hhard N
+  obtain ⟨F, hF, hyes, hcard⟩ := hN n hn
+  exact (hhardn F hyes hcard).not_ge hF
+
+open Classical in
+/-- A fixed-exponent one-sided average-case formula lower bound for a subexponential MCSP
+threshold yields a binary NP language without polynomial-size De Morgan formulas. The language
+agrees with succinct MCSP on encoded instances; its other words use the existing total verifier.
+This does not require the canonical encoding image itself to be a binary NP language. -/
+theorem exists_NP_not_mem_FormulaPoly_of_zero_error_average_case_subexp_hard
+    {s : ℕ → ℕ} (hs : SubexponentiallyBounded s) {d : ℕ} (hd : 0 < d)
+    (hhard : ∀ N : ℕ, ∃ n ≥ N, ∀ F : Formula signature (2 ^ n),
+      (∀ T : BitString (2 ^ n), List.ofFn T ∈ GapMCSP.yesSet s →
+        F.eval interpretation T = true) →
+      (Finset.univ.filter fun T : BitString (2 ^ n) =>
+        F.eval interpretation T = true).card ≤ 2 ^ (2 ^ n - n) →
+      2 ^ (n / d) < F.leafSize) :
+    ∃ L : Language Bool, (L : Set (List Bool)) ∈ Complexity.NP Turing.MultiTapeTM.encBits ∧
+      L ∉ FormulaPoly := by
+  obtain ⟨L, hL, hag⟩ := SuccinctMCSP.exists_language_mem_NP
+  exact ⟨L, hL, not_mem_FormulaPoly_of_zero_error_average_case_subexp_hard hs hd hhard hag⟩
+
+end Cslib.Circuits.Boolean
diff --git a/ComplexityTests/FormulaMagnificationAverageCase.lean b/ComplexityTests/FormulaMagnificationAverageCase.lean
new file mode 100644
index 000000000..8af9f204c
--- /dev/null
+++ b/ComplexityTests/FormulaMagnificationAverageCase.lean
@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.MCSP.FormulaMagnification.AverageCase
+
+/-!
+# Clients of zero-error average-case formula magnification
+
+The query schedules below are inhabited polynomial examples. The finite client uses an actual
+agreeing NP language, with no unproved formula upper bound, and checks that the formula's false
+output certifies NO and its true output is an unknown mask of the required density.
+-/
+
+namespace ComplexityTests.FormulaMagnificationAverageCase
+
+open Cslib Cslib.Circuits Cslib.Circuits.Boolean Filter
+
+example : SubexponentiallyBounded (fun n => avgCaseMCSPQueryEncLength n (n ^ 2 + 1) n) :=
+  subexponentiallyBounded_avgCaseMCSPQueryEncLength
+    ((SubexponentiallyBounded.id.pow 2).add (.const 1)) SubexponentiallyBounded.id
+
+-- Zero thresholds and zero loss also use the same query encoding and growth API.
+example : SubexponentiallyBounded (fun n => avgCaseMCSPQueryEncLength n 0 0) :=
+  subexponentiallyBounded_avgCaseMCSPQueryEncLength (.const 0) (.const 0)
+
+open Classical in
+example : ∃ F : Formula signature (2 ^ 8),
+    (∀ T : BitString (2 ^ 8), F.eval interpretation T = false →
+      List.ofFn T ∉ GapMCSP.yesSet (fun _ => 1)) ∧
+    8 * (Finset.univ.filter fun T : BitString (2 ^ 8) =>
+      F.eval interpretation T = true).card ≤ 2 ^ (2 ^ 8) := by
+  obtain ⟨L, -, hag⟩ := SuccinctMCSP.exists_language_mem_NP
+  obtain ⟨F, -, hyes, hcard⟩ := exists_formula_zero_error_average_case_of_agrees
+    (s := fun _ => 1) (n := 8) (r := 8) hag (by decide)
+  refine ⟨F, fun T hfalse hsmall => ?_, ?_⟩
+  · have htrue := hyes T hsmall
+    rw [hfalse] at htrue
+    exact Bool.noConfusion htrue
+  · calc
+      8 * (Finset.univ.filter fun T : BitString (2 ^ 8) =>
+          F.eval interpretation T = true).card
+          ≤ 2 ^ 8 * 2 ^ (2 ^ 8 - 8) := Nat.mul_le_mul (by decide) hcard
+      _ = 2 ^ (2 ^ 8) := by norm_num
+
+-- The forward theorem instantiates directly with a fixed reciprocal exponent and loss r=n.
+example {L : Language Bool} (hag : ∀ x, x ∈ SuccinctMCSP ↔ SuccinctMCSP.enc x ∈ L)
+    (hL : L ∈ FormulaPoly) :
+    ∀ᶠ n in atTop, ∃ F : Formula signature (2 ^ n),
+      F.leafSize ≤ 2 ^ (n / 2) ∧
+      (∀ T : BitString (2 ^ n), List.ofFn T ∈ GapMCSP.yesSet (fun n => n ^ 2 + 1) →
+        F.eval interpretation T = true) ∧
+      (Finset.univ.filter fun T : BitString (2 ^ n) =>
+        F.eval interpretation T = true).card ≤ 2 ^ (2 ^ n - n) :=
+  eventually_exists_formula_zero_error_average_case_of_mem_FormulaPoly
+    ((SubexponentiallyBounded.id.pow 2).add (.const 1)) SubexponentiallyBounded.id
+    hag hL 2 (by decide)
+
+end ComplexityTests.FormulaMagnificationAverageCase
diff --git a/ROADMAP.md b/ROADMAP.md
index 9dbf5b5c6..8c3256455 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -450,7 +450,8 @@ each statement against the numbered result. Organize modules by subject, not cha
   multi-tape steps for a constant `c < 1`; prefix-free complexity,
   resource-bounded MCSP variants and connections to learning, cryptography and lower bounds; the
   circuitized anti-checker with an efficient generator; the asymptotic parameter instantiation of
-  Theorem 5 in `MCSP/FormulaMagnification.lean`; and hardness results for `MINKT` and `MINcKT` (whose
+  Theorem 5 (the general subexponential one-sided average-case wrapper is tracked in #1871);
+  and hardness results for `MINKT` and `MINcKT` (whose
   definitions, conditional `K^t` measure, and `NP` memberships are in `Kolmogorov/MINKT.lean`,
   `Kolmogorov/Conditional.lean`, and `Kolmogorov/MINcKT.lean`), as independently scoped
   developments; the reverse