RootClauseABoundaryShellEndpoint #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. C₁ hits every sufficiently large target exactly #
theorem
Algsuperdiff.Section4.Provider.Regularity.exists_cedos_stepOneC1_eq
(d : ℕ)
(Citer : ℝ)
(k : ℕ)
{Cfl V : ℝ}
(hCfl : 1 ≤ Cfl)
(hbase : max 2 (2 * ↑d + 2) ≤ V)
(hiter : 4 * Citer * (↑k + 1) / Real.log 3 ≤ V)
(hdelta0 : stepOneC1Delta0 Cfl 1 k ≤ V)
:
The Step-1 constant is onto, above its two C_edos-free floors.
For every V clearing max(2, 2d+2), the C_iter slot 4C_iter(k+1)/log 3
and the floor δ₀(C_fl,1,k)⁻¹, there is a C_edos ≥ C_fl with stepOne d C_edos 1 C_iter k = V. The witness is C_edos = √V/(4·3^{k/4}), at which the
third slot of the max equals V and dominates the other two. This is what
lets two lanes with different pinned (C_iter, k) read one and the same
RootWindowPayload.