The exact minimax peak on the sub-disturbance window: the value of scalar adversarial adaptive control from a start below the disturbance level

Theorem A: gamma*(x₀, Delta) = 1 + Delta for every start with |x₀| <= 1 and (2 Delta - 1)|x₀| <= 1, i.e. on the plateau |x₀| <= min(1, 1/(2 Delta - 1)) of the sub-disturbance window; both halves proved, the lower half by an explicit finite adversary (free moves then one identification spike)

For every Delta <= 1 the deferred window is closed outright: gamma*(x₀, Delta) = 1 + Delta on the whole of |x₀| <= 1, endpoints included (at Delta = 1 the plateau's right edge is |x₀| = 1 exactly, and the closed endpoint is proved separately)

Proposition C: from any nonzero start with |x₀| = s <= 1 the source's own midpoint law guarantees peak <= 1 + max(Delta s, (Delta s + 1)²/(8 s), min(1/s, Delta)), hence peak <= 1 + min(Delta, that); this is STRICTLY below the source's guarantee 1 + Delta whenever s > 1/Delta and (Delta s)² - 6 Delta s + 1 < 0 and s < 1 (author fix 2026-09-03: the strict region needs 1/Delta < s < 1; at s = 1 the first branch already equals Delta), so 1 + Delta is not the value throughout the window the source defers

Free move: if |y - u| <= 1 - Delta|x| then w:= y - a x - u satisfies |w| <= 1 for EVERY admissible a in [-Delta, Delta] at once, so below the disturbance level the adversary repositions the state freely, leaks no information about a, and defers its single parameter commitment to the terminal spike

The certified cap of CS3 is attained: over 60 (Delta, s) cells a strong adversary search against the midpoint law never exceeds 1 + max(Delta s, (Delta s + 1)²/(8 s), min(1/s, Delta)) and reaches it exactly in 24 of them, so on those cells that cap is the exact value of the game against the source's own controller

The residual band: between the plateau's right edge 1/(2 Delta - 1) and s₂(Delta) 0.575, 0.45, 0.15 at Delta = 2, 3, 10 the value is still open; the converged two-sided value iteration of the strategy journal drops below 1 + Delta immediately above 1/(2 Delta - 1) at all three, and the optimal implicit selector inside the band is biased away from the midpoint (c* 0.55-0.63 at Delta = 3)

The source's own lower bound reproduced in Lean: the identification spike gives Forced x₀ Delta (1 + Delta |x₀|) against every causal law and from every start (prop:implicit(i) at the midpoint), and the two-move attack from rest gives Forced 0 Delta (1 + Delta) (Proposition prop:lb)

The source's own upper bound reproduced in Lean, in the reusable form of its Remark rem:restart: from any start with |x₀| <= 1 the set-membership certainty-equivalent midpoint deadbeat law of Definition def:controller caps the peak at 1 + Delta, via the window lemma and the invariant gₜ₊₁ <= Lₜ <= 2 Delta

Negative controls: (too small) at every nonzero start strictly inside the plateau the source's own lower bracket endpoint 1 + Delta|x₀| is strictly below the value; (too large) at Delta = 3, |x₀| = 1/2 the value is strictly below 1 + Delta = 4, so the plateau really ends and 1 + Delta is not the answer on the whole window; (non-vacuity) every Delta > 0 admits a nonzero start in the plateau; plus no causal law achieves any cap below 1 + Delta there, and nothing above 1 + Delta is forced anywhere on |x₀| <= 1

Lemma R, certified: the source's own recentring normalisation u ₜ = uₜ + c xₜ is a bijection of the causal class Ctrl, giving ForcedP x₀ m D c <-> Forced x₀ D c and valueP x₀ m D = value x₀ D; with the reflection value(-x₀, Delta) = value(x₀, Delta) the value depends on (x₀, A₀) only through (|x₀|, |A₀|/2); corollary valueP 0 m D = 1 + D, which is the source's Remark 9(c) (asymmetric prior of diameter 2D) certified from rest

The landing lemma: from a nonzero state the adversary forces ANY successor y whose width-2 data window still meets the prior image, and inherits everything forced at the SURVIVING prior, of half-width survD = |[nu-R, nu+R] cap [y-1, y+1]| / (2|x|); with it the sharp spike 1 + Delta|y| + |u|, the echo 1 + muC(R,z) z/(2|x|) at every landing distance z >= 0, and the return to rest 1 + 1/|x| whenever |u| + 1 <= Delta|x|

The source's own three-branch exchange maximum M(R) = 2R(1-R) / (R+1)²/4 / 2(R-1) at a GENERAL half-width R, its constrained maximisation mu|y| <= M(R) under mu <= min(2, 2R) and mu + |y| <= R + 1, and the consequent sharpened guarantee: the midpoint law caps the peak at 1 + max(Delta s, M(Delta s)/(2 s), min(1/s, Delta)) from every nonzero start with s = |x₀| <= 1; strictly below the cap of CS3 wherever Delta s is outside [1/3, 3] (8 against 9 at (Delta, s) = (10, 1/2))

Theorem B: for Delta > 0 and any start with 0 < |x₀| <= 1 satisfying |x₀| + 1 <= 2 Delta |x₀|² (equivalently 2 Delta s >= 1 + 1/s, i.e. s >= (1 + sqrt(1+8 Delta))/(4 Delta)), the exact value is gamma*(x₀, Delta) = 1 + max(Delta s, M(Delta s)/(2 s), min(1/s, Delta)) with s = |x₀|; the lower half is three explicit finite attacks against an arbitrary causal law – the identification spike, the echo at the M-maximiser, and the RETURN TO REST, which lands the state at the origin and cashes the source's Theorem 1 at the reduced, recentred prior

Three exact values strictly inside the deferred window: gamma*(1/2, 3) = 3, gamma*(1/2, 10) = 9, gamma*(9/10, 3) = 37/10. The first two lie STRICTLY BETWEEN both ends of the source's bracket; the third is the lower end 1 + Delta|x₀| exactly. With CS1/CS2 (the upper end, on the plateau) the window is now known to carry all three possibilities

Proposition C's strictness half, in Lean: for Delta > 0 and s > 0, U(s, Delta) < Delta if and only if 1/Delta < s < 1 and (Delta s)² - 6 Delta s + 1 < 0 – equivalently 1/Delta < s < 1 and Delta s < 3 + 2 sqrt 2, only the upper root binding once Delta s > 1; hence gamma* < 1 + Delta throughout that region, the region is nonempty for every Delta > 1 and empty for every Delta <= 1, and the clause s < 1 is not redundant (at Delta = 3, s = 1 the other two clauses hold while U = 3 = Delta)

Negative controls for Theorem B: (too large) gamma* < 1 + Delta throughout its region with |x₀| < 1, plus the three bracket positions at the named cells; (too small) for Delta < 1 the hypothesis fails at every 0 < s <= 1, so nothing is claimed there; (non-vacuity) every Delta > 1 admits a qualifying start strictly inside the window; (disjointness) the hypothesis forces (2 Delta - 1)|x₀| >= 1, so Theorem B never overlaps the interior of CS1's plateau, and at the unique overlap point Delta = |x₀| = 1 the two theorems agree; plus no law achieves a cap below the value and nothing above 1 + U is forced