Part 1: deterministic inequalities (exact integer arithmetic)
  (D1) (a+1)/(2(w(2a)+1)) > w(a)+w(2a)+2 fails for 459 values of a in [1,1e6]; largest failure 527; holds for all a in [528, 1e6]
  (D2) floor(x/2)-2 >= w(ceil(x/2)-1)+1 fails for 6 x in [4,1e6]; holds for all x in [10, 1e6]
  (D3) partial sums up to 2e5: sum_x (3w(x)+2) 2^(-l_x) = 1.0652e+04;  sum_a exp(-(a+1)/(2(w(2a)+1)^2)) = 6.9632e+02
       (both series converge: terms decay like exp(-c x^(1/3)); the Borel-Cantelli argument only needs finiteness)

Part 2 (evidence only): minimum end-separating cut in windows [-R,R]
  seed 1: R=25: weight 0.3795, cols (1, 2), |cut|=3; R=50: weight 0.3795, cols (1, 2), |cut|=3 (same); R=100: weight 0.3795, cols (1, 2), |cut|=3 (same); R=200: weight 0.3795, cols (1, 2), |cut|=3 (same); R=400: weight 0.3795, cols (1, 2), |cut|=3 (same); R=800: weight 0.3795, cols (1, 2), |cut|=3 (same); R=1599: weight 0.3795, cols (1, 2), |cut|=3 (same)
     cheapest straight vertical cut between columns x,x+1 for x in [X,2X): X=10: 1.411, X=100: 1.636, X=400: 2.307, X=1000: 3.447
     Lemma-1 sums: a=100: sum mu_x=13.32 vs w(a)+w(2a)+2=13; a=200: sum mu_x=23.18 vs w(a)+w(2a)+2=16; a=400: sum mu_x=40.70 vs w(a)+w(2a)+2=20; a=700: sum mu_x=63.08 vs w(a)+w(2a)+2=23
  seed 2: R=25: weight 0.5487, cols (-1, 1), |cut|=3; R=50: weight 0.4745, cols (-31, -29), |cut|=6; R=100: weight 0.4745, cols (-31, -29), |cut|=6 (same); R=200: weight 0.4745, cols (-31, -29), |cut|=6 (same); R=400: weight 0.4745, cols (-31, -29), |cut|=6 (same); R=800: weight 0.4745, cols (-31, -29), |cut|=6 (same); R=1599: weight 0.4745, cols (-31, -29), |cut|=6 (same)
     cheapest straight vertical cut between columns x,x+1 for x in [X,2X): X=10: 0.703, X=100: 1.538, X=400: 2.288, X=1000: 3.260
     Lemma-1 sums: a=100: sum mu_x=14.64 vs w(a)+w(2a)+2=13; a=200: sum mu_x=25.09 vs w(a)+w(2a)+2=16; a=400: sum mu_x=39.26 vs w(a)+w(2a)+2=20; a=700: sum mu_x=61.88 vs w(a)+w(2a)+2=23
  seed 3: R=25: weight 0.4016, cols (-2, 0), |cut|=3; R=50: weight 0.4016, cols (-2, 0), |cut|=3 (same); R=100: weight 0.4016, cols (-2, 0), |cut|=3 (same); R=200: weight 0.4016, cols (-2, 0), |cut|=3 (same); R=400: weight 0.4016, cols (-2, 0), |cut|=3 (same); R=800: weight 0.4016, cols (-2, 0), |cut|=3 (same); R=1599: weight 0.4016, cols (-2, 0), |cut|=3 (same)
     cheapest straight vertical cut between columns x,x+1 for x in [X,2X): X=10: 1.309, X=100: 1.270, X=400: 2.434, X=1000: 3.416
     Lemma-1 sums: a=100: sum mu_x=15.52 vs w(a)+w(2a)+2=13; a=200: sum mu_x=24.98 vs w(a)+w(2a)+2=16; a=400: sum mu_x=42.90 vs w(a)+w(2a)+2=20; a=700: sum mu_x=62.16 vs w(a)+w(2a)+2=23
  seed 4: R=25: weight 0.0852, cols (-1, 0), |cut|=2; R=50: weight 0.0852, cols (-1, 0), |cut|=2 (same); R=100: weight 0.0852, cols (-1, 0), |cut|=2 (same); R=200: weight 0.0852, cols (-1, 0), |cut|=2 (same); R=400: weight 0.0852, cols (-1, 0), |cut|=2 (same); R=800: weight 0.0852, cols (-1, 0), |cut|=2 (same); R=1599: weight 0.0852, cols (-1, 0), |cut|=2 (same)
     cheapest straight vertical cut between columns x,x+1 for x in [X,2X): X=10: 1.271, X=100: 1.589, X=400: 2.016, X=1000: 3.223
     Lemma-1 sums: a=100: sum mu_x=16.18 vs w(a)+w(2a)+2=13; a=200: sum mu_x=24.10 vs w(a)+w(2a)+2=16; a=400: sum mu_x=40.14 vs w(a)+w(2a)+2=20; a=700: sum mu_x=59.50 vs w(a)+w(2a)+2=23
  seed 5: R=25: weight 0.3280, cols (-1, 0), |cut|=2; R=50: weight 0.3280, cols (-1, 0), |cut|=2 (same); R=100: weight 0.3280, cols (-1, 0), |cut|=2 (same); R=200: weight 0.3280, cols (-1, 0), |cut|=2 (same); R=400: weight 0.3280, cols (-1, 0), |cut|=2 (same); R=800: weight 0.3280, cols (-1, 0), |cut|=2 (same); R=1599: weight 0.3280, cols (-1, 0), |cut|=2 (same)
     cheapest straight vertical cut between columns x,x+1 for x in [X,2X): X=10: 1.019, X=100: 1.573, X=400: 2.600, X=1000: 2.985
     Lemma-1 sums: a=100: sum mu_x=14.16 vs w(a)+w(2a)+2=13; a=200: sum mu_x=24.71 vs w(a)+w(2a)+2=16; a=400: sum mu_x=40.25 vs w(a)+w(2a)+2=20; a=700: sum mu_x=56.94 vs w(a)+w(2a)+2=23

Part 3: cross-checks of the dual shortest-path min cut
  (a) brute force over all 2^|inner| vertex sets, window [-3,3], 30 seeds: mismatches = 0
  (b) integer max-flow (capacities round(J*1e6), int32) vs dual shortest path, window [-60,60], 10 seeds: mismatches (>1e-3) = 0
