Sharpness of A_p bounds for dyadic martingale transforms: explicit test functions

To show that the power max(1,1/(p-1)) of [w]_{A_p} is sharp for the martingale transform with signs (-1)^k on the line (generations 0<=k<N), no duality is needed. (1) Weight v=t^{δ-1} and g=Σ_{k<N}(-1)^k h_k, where h_k=2·1_{[0,2^{-k-1})}-1_{[0,2^{-k})}: then |g|<=2 by an induction on partial sums, and Tg=N on [0,2^{-N}). (2) Buckley's weight w=t^{(p-1)(1-δ)} and F=σ·1_{[0,2^{-N})}: its averages are 2^k·c over [0,2^{-k}) and 0 over disjoint cubes, so on [2^{-j-1},2^{-j}) one has exactly TF=c(Σ_{k<j}(-2)^k-(-2)^j), with modulus at least c·2^j. Each scale then contributes c^p/2^p, and N=⌈1/δ⌉ gives the ratio δ^{-p}. In Lean, compute averages as integrals of nested indicators; do not develop Haar orthogonality.