The far-field exchange: what the δ = 2π route actually is

Record of a measurement-and-proof exchange with the theorem-proving service during submission 9 (eform3), 2026-08-13. It is written down because the mathematical content is not in any artifact yet, the job is still running, and because the shape of the argument changed twice during it, in both directions.

1. The brief's prescribed route is false, and this is why

The submission asked for |Qim(y,s)| ≤ C₂·y/s² by two integrations by parts, and built a 1/s⁴ counting argument on it. No constant C₂ makes that true.

Qim is the imaginary part of the Fourier–Laplace transform of a window with a jump at ±1/2; the jump forces decay of order y/|s| and no better. Squaring gives damage of order y²/s², not y²/s⁴, so the counting the brief proposed is unreachable at any constants.

Established three independent ways:

numerically here: |Qim|·s stays in 0.13–0.30 across s = 20…1600 while |Qim|·s² grows 5 → 220;
by the boundary term: the integrand's value at the support edge is cos(√2/2)·sinh(y/2) = 0.153 ≠ 0;
by the prover, twice independently: jump-formula asymptotics, and directly from the closed forms for Qre and Qim.

The asymptote is (1 + cos√2)/2 · sinh(y/2)/y = 0.2920 at y = 1/2. The coordinator's error was importing a 1/s² rate from a companion result about c₂ = g⋆g, which is continuous because an autocorrelation vanishes at the edge of its support. Ledgered as defect #15.

2. What the route to δ = 2π actually is

Two ingredients, and the second is the one that matters:

Sharp far-field constants. An exact closed form for Qim giving a decreasing majorant with honest constants.
Near-field cancellation. Inside |s| ≤ R₀, Qre(y,s)² > Qim(y,s)², so those offsets contribute no damage at all, rather than contributing the uniform cap, which is what the previous run did.

That distinction is the whole difference between δ = 26 and δ = 2π. It is not a constant-chasing improvement on the brief's route; the brief's route does not exist.

3. The measured facts the argument is designed against

At y = 1/2 unless stated, from closed forms validated against quadrature to 12 digits:

quantity	value
max true damage `max(0, Qim² − Qre²)`	0.00439642 at s = 6.51700 (= 0.0175857 y²)
true no-damage radius (`Qre² ≥ Qim²` for all `\	s\	≤ R`)	R = 6.0653187731 (= 0.9653·2π)
damage support	nonzero on 15.3% of the range: windows of width ≈ 0.962 just above each 2πk
first six peaks	4.396e−3, 9.751e−4, 4.233e−4, 2.361e−4, 1.505e−4, 1.043e−4
sum of ALL peaks (3183 windows to s = 20000)	6.8591e−03; the tail beyond six is 8.4% of the total
both sides vs budget `Shq/2 = 3.3754e−02`	40.6% of budget → margin 2.46×
sharp envelope `sup_{s≥s₀} \	Qim\	·s/y`	0.9463 / 0.9336 / 0.9077 / 0.8040 at s₀ = 5.7 / 6.0 / 2π / 12, essentially y-independent

The 2.46× is the true adversarial value, not an upper estimate. Damage windows recur at spacing 2π and are narrower than the spacing, so a 2π-separated configuration can place a point in every window. There is no configurational saving available; the worst case is exactly the sum of peaks, and it is attained.

This corrected the prover's own working figure of 2.7×, which had summed only the six visible windows and treated the k⁻² tail as negligible.

4. The prover's lemmas, checked here

claim	verdict
`Qre(y,s) ≥ Qre(0,s) − 0.0107` for 0 ≤ y ≤ 1/2	holds, true max drop 0.00649642 at (y,s) = (0.500, 7.8380), 60.7% of the allowance, and the worst point lies beyond R₀
its derivation `(y²/2)cosh(y/2)·(1/12)`	reproduces exactly: 0.01074389; with the sharp `L2 = 0.0712006` it would be 0.00917965 (14% held in reserve)
`Qre(0,·)` monotone decreasing on [0, 2π]	holds, max increase −3.56e−12; endpoints `Qre(0,0) = 0.918725 = A`, `Qre(0,2π) = 0.049027`
far-field majorant `Φ(5.7) = 0.03753`	`\	Qim\	≤ 0.193727 y` against true 0.155601 y → 1.2450× pointwise, 1.5501× squared, as the prover stated

A coordinator caution that the monotonicity had a direction error was withdrawn: the lemma is stated in additive slack form, which absorbs the y-dependence explicitly rather than assuming a monotonicity that does not hold (Qre is not increasing in y: 0.135442 < 0.139436 at s = 5.7).

5. Normalisation note, so it is not re-litigated

Two Shq in play, and they are the same statement:

Shq_prover(y) = ĝ(2y)² − A², Shq_here(y) = ∫ g·sinh²(yu) du, Shq_prover = 2(ĝ(2y) + A) · Shq_here [factor 3.746969 at y = 1/2]

checked to 1.7e−17. A coordinator claim that a floor of 0.23 y² was false was withdrawn, it is false in one normalisation and true in the other. Shq_here/y² → L2 = 0.0712006; Shq_prover/y² → 4A·L2 = 0.261655. Since the final inequality consumes the quotient (damage sum)/(Shq/2), the normalisation cancels.

Corrected constants now in use: A = 0.9187253699, ĝ(1) = 0.9547589817, Shq_prover(1/2) = 0.06750841 = 0.270034 y².

6. Where the recoverable slack is

Margin ≈ 1.19 at the prover's current constants after all three losses multiply. The Φ-tail is near-sharp beyond s ≈ 12, so essentially all recoverable slack sits on the first window. Cheapest order if the margin thins in Lean:

two-piece envelope (flat cap on the first window, then C·y/s with C ≈ 0.80 beyond s = 12);
swap 1/12 → L2 = 0.0712006 in the slack lemma (14%, one constant);
R₀: 5.7 → 5.87 (available at the current cap; the truth is 6.0653).

None disturbs the structure of the argument.