Weak-type two-weight bound from cube testing: absorb on principal cubes

To get a weak-type mixed bound ‖A_S‖_{Lp(w)→L^{p,∞}(w)} ≲ [w]^{1/p}[w]_{A∞}^{1/p'} for sparse operators, dualize with 1_E (E = {A_S h > t}): you need ∫(A_S(1_E w))^s σ ≲ T' w(E), with only the cube-testing constant T'. Take principal cubes P for γ_Q = w(E∩Q)/w(Q), so γ_Q ≤ 2γ_{π(Q)} and A_S(1_E w) ≤ 2∑_P γ_P Φ_P (Φ_P is the testing function of P). Apply the chain inequality, then Hölder, to G(P)=∫(∑_{P'⊆P} γΦ)^s σ. With the ansatz G(P') ≤ K·w(E∩P') = Kγ_{P'}w(P') the sum becomes ∑γ^{r}w(P'), r = 1+(s-1)/s > 1, which the principal-cube Carleson lemma bounds by K_r w(E∩P). Absorb: K ≤ (sK_r)^s T'. The key choice is to normalize by w(E∩P), not by |P| or w(P). Lean gotcha: inside open Filter, 𝓟 is the principal-filter notation, so it cannot be a variable name. It parsed in a scratch file without that open and failed in the module.