theorem MathlibNt.SieveTheory.finiteSourceLayer_odd_lowStrip_exact (N : ℕ) (x : ℝ) (hN : 3 ≤ N) (hodd : N % 2 = 1) (hx1 : 1 < x) (hx3 : x ≤ 3) : x * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N x = 3 - x + 3 * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3

For every odd finite depth at least three, the part of the weighted source layer visible below the recursive clamp 3 consists exactly of the first-layer segment 3 - x; every higher odd summand has the same weighted numerator as at x = 3.