{"id":"8106adea-792b-4166-ba7c-15d31e835b6e","arxiv_id":"2508.05563","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A general axiomatic framework yields restricted weak-type bounds for Carleson operators on doubling metric measure spaces, verified in Lean.","lead":"This paper proves L^p bounds for maximally modulated singular integral operators (Carleson operators) on doubling metric measure spaces, under a set of axiomatic conditions on the modulation functions. It unifies and generalizes prior Carleson-type results that were confined to Euclidean spaces.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The proof's pivotal Hölder van der Corput step rests on an unproved Hölder-to-Lipschitz approximation lemma; combined with unverified examples, the advertised generalization is conditional.","rationale":"The reader's verdict centers on the cancellative axiom; I agree that (1.7) is the load-bearing assumption. A sharper formulation is that the proof does not use (1.7) directly for Hölder kernels; it uses Lemma 7.1. Since that lemma is unproved in the English text and the paper explicitly says so, there is a gap at the point where the main hypotheses are connected to the time-frequency machinery. The Lean formalization claim is real evidence and may already cover this, so the correct stance is to verify rather than reject. Moreover, the paper's claim to generalize classical and modern results requires checking examples; the only example discussed in detail is the classical R setting through the sibling communication, and the Walsh statement is explicitly a 'possible deduction' with no construction of continuous modulations satisfying (1.7). Therefore the verdict remains CONDITIONAL: accept conditional on either a proof/source for Lemma 7.1 or confirmation in the formalization, and on a supplement verifying examples.","tokens_in":40306,"tokens_out":21258,"duration_ms":244250,"concrete_test":"Consult the sibling Lean/mathlib formalization (arXiv:2405.06423) for a proof of Lemma 7.1 as stated (Hölder-to-Lipschitz approximation on doubling metric measure spaces with the stated constants) and for verification that the linear, polynomial, and Malmquist–Takenaka modulation classes satisfy (1.7). If Lemma 7.1 is proved there, the gap is closed; if not, give an independent analytic proof or exhibit a concrete doubling space where the stated bounds fail.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The proof's pivot is the Hölder van der Corput estimate, Proposition 2.5. It is derived in Section 7 from the cancellative axiom (1.7) via Lemma 7.1, a Hölder-to-Lipschitz approximation lemma that is explicitly not proved in the paper ('which we will not prove here'). This is not a cosmetic omission: Lemma 7.1 is the only mechanism that lets the Lipschitz testing condition (1.7) apply to the Hölder products K_{s1}(x1,·)K_{s2}(x2,·) in Lemma 5.3. If the quantitative form of Lemma 7.1 fails on some doubling metric measure space, Proposition 2.5 fails, and with it the tile correlation bound (5.6), the antichain proof in §5, and the separated-tree estimate in §6.5 (Lemma 6.11). A second, application-level fragility is that the named examples are asserted but not checked against (1.7); in particular, Walsh modulations are step functions and do not even form a collection of continuous functions, so the claimed Walsh 'deduction' is not a direct consequence of the stated theorem.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops an axiomatic framework for maximally modulated singular integrals (Carleson operators) on doubling metric measure spaces. The main result, Theorem 1.1, is a restricted weak-type (q,q) estimate for a generalized Carleson operator T under three families of hypotheses: (i) a doubling metric measure space, (ii) a 'cancellative compatible' collection of continuous modulation functions satisfying oscillation and metric axioms (1.2)–(1.7), and (iii) an assumed L2 bound for a non-tangential maximal truncated singular integral T*. Theorem 1.2 is a linearized version with a weaker L2 hypothesis. The proof follows the Euclidean time-frequency analysis of Fefferman and Zorin-Kranich: tiles, trees, forests, antichains, density parameters, and a Hölder van der Corput estimate (Proposition 2.5). The paper claims that the main theorems have been computer-verified in Lean (sibling communication).","tokens_in":40627,"tokens_out":5922,"duration_ms":64137,"significance":"If the proof is completed, the paper makes a significant contribution by placing Carleson operators in a general metric-measure setting and by providing a modular, constant-explicit argument that is amenable to formal verification. The explicit constants and the conditional framing are strengths, and the claimed Lean formalization, if accurate, is a major independent check. However, the significance is currently tempered by two load-bearing gaps: an unproved Hölder-to-Lipschitz approximation lemma used in the pivotal van der Corput step, and the absence of any verified concrete modulation class satisfying the cancellative axiom (1.7). The advertised applications to classical Walsh and polynomial Carleson theorems are not established in this text.","major_comments":[{"comment":"Lemma 7.1 is the only bridge between the Lipschitz testing condition (1.7) and the Hölder-regular kernels used in Lemma 5.3 and Lemma 6.11. The paper states 'we will not prove here' and gives no reference. This lemma is load-bearing: without it, Proposition 2.5 (Hölder van der Corput) is unproved, and the tile correlation bound (5.6), the antichain estimate, and the separated-tree correlation (6.17) all fail. The authors must supply a proof or a precise citation. If the Lean formalization proves this lemma, the paper should say so explicitly and reproduce the argument.","section":"Section 7, Lemma 7.1"},{"comment":"The paper claims to generalize the classical Carleson theorem, Walsh–Carleson, and polynomial Carleson operators, but it does not verify that any of these modulation classes satisfies the 'cancellative compatible' axioms, especially the quantitative oscillatory estimate (1.7). In particular, Walsh modulations are step functions and are not continuous, so they cannot form a collection Θ as required. For polynomial modulations on Euclidean spaces, the cancellative axiom is a nontrivial van der Corput-type statement for Lipschitz test functions; no proof or reference is supplied. The main theorem is conditional, but without a single worked example the framework risks being empty. Please add at least one concrete modulation class satisfying (1.2)–(1.7), or explicitly refer to the sibling communication/blueprint where such verification is done.","section":"Section 1 (axioms (1.2)–(1.7) and examples)"},{"comment":"Lemma 6.6 (boundary overlap) is used in the proof of Lemma 6.5 to bound the operator S_{1,u}, and it is stated without proof ('we do not explicitly prove'). This is a simple finite-overlap counting argument, but for a paper that advertises machine-checked and modular proofs, every auxiliary lemma should be either proved or referenced. This is less severe than the Lemma 7.1 gap, but it is part of the same pattern of leaving auxiliary statements unproved.","section":"Section 6.2, Lemma 6.6"}],"minor_comments":[{"comment":"Several typos and formatting issues should be corrected: 'Carleson opera tors' in the title header, 'singular intgral' in Section 1, 'preceeded' in the introduction, and an inconsistent use of 'S' for both the truncation parameter and the set in Section 6.5. These do not affect the mathematics.","section":"Throughout"},{"comment":"The exponent in (2.6) is 2^{442a^3}, while the theorem states 2^{443a^3}. The iterative argument explains the extra factor, but it may help to state this explicitly to avoid confusion.","section":"Section 2.1, Eq. (2.6)"},{"comment":"In the proof of Lemma 4.12, the claim 'B(u) and B(u') are disjoint, but also B(u) ⊂ B(p) and B(u') ⊂ B(p)' appears to use the definition of B(p) from (4.6) and the relations 100p ≲ 100u. This is correct, but the notation B(p) is overloaded with B(c(p), r) elsewhere; a remark on notation would improve readability.","section":"Section 4.4, Lemma 4.12"}],"recommendation":"major_revision","confidential_remarks":"The manuscript presents a plausible and important framework, and the claimed Lean formalization is a strong signal. However, the paper as submitted is not self-contained at a key point: Lemma 7.1 is unproved and is used in the central van der Corput estimate. The examples section also overclaims without verification. These are fixable within the scope of a revision—supply the missing lemma proof and a concrete verified modulation class—so I recommend major revision rather than rejection. The formalization claim, if accurate, should be leveraged: the authors could point to the specific Lean proof of Lemma 7.1 or include it as an appendix."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This paper is worth engaging with. What is genuinely new is the axiomatic setup: compatible and cancellative modulation classes defined through ball-dependent metrics, which lets the authors transfer the Fefferman–Lie–Zorin-Kranich tile/forest machinery from Euclidean space to doubling metric measure spaces. The main theorem is a clean conditional statement—restricted weak-type bounds for the generalized Carleson operator, assuming an L2 bound for the nontangential maximal operator—and the proof is modular, explicit about constants, and unusually readable for this kind of argument. The claim that the main theorems are computer-verified in Lean is a significant piece of evidence; if the sibling communication really covers these statements, that is about as strong a check as one can get in this area.\n\nThe soft spots are real but not fatal. First, the paper never verifies that any of the named examples—linear, polynomial, Walsh, Malmquist-Takenaka—actually satisfy the compatibility and cancellative axioms. That is a strange omission for a paper whose selling point is generalization. The Walsh case is the sharpest problem: Walsh modulations are step functions, not continuous, so they do not fall under the stated framework at all. The text mentions only a \"possible deduction\" of the Walsh theorem in a modified sense, which is honest but far from the abstract's suggestion that Walsh is covered as a special case. Second, Lemma 7.1, the Hölder-to-Lipschitz approximation lemma, is explicitly not proved and it is load-bearing for the van der Corput step. It looks like a standard quantitative approximation argument and is probably covered by the Lean formalization, but as written the English proof has a hole there. Lemma 6.6 is a minor version of the same issue and is not concerning.\n\nOverall, I think the central argument is very likely correct. The gaps are in presentation and verification of scope, not in the architecture. The paper deserves a serious referee. The referee should be asked to make the examples claim precise, either by proving the axioms for the Euclidean polynomial modulations or by clearly stating which of the named examples are and are not covered. The authors should also either prove Lemma 7.1 or give a precise reference. With those fixes, this would be a strong and durable contribution.","headline":"A serious and substantially new axiomatic framework for Carleson operators on doubling spaces, backed by a Lean-verification claim, but the advertised examples are not actually checked and one load-bearing lemma is left unproved.","tokens_in":41060,"tokens_out":4703,"would_cite":true,"duration_ms":52178,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["42B20","42B25","43A85"],"pacs":[],"model":"deepseek-v4-flash","headline":"Axioms on modulation functions put Carleson operators under Lp control on every doubling metric measure space.","keywords":["Carleson operator","doubling metric measure space","modulation functions","maximally modulated singular integrals","restricted weak type estimates","tile and forest decomposition","one-sided Calderón–Zygmund kernel"],"falsifier":"Take a ball $B$ in hyperbolic space, with $\\Theta=\\{\\xi\\cdot \\rho(\\cdot,x_0):\\xi\\in\\mathbb{R}\\}$ and $d_B$ the oscillation metric, and compute $\\int_B e^{i(\\xi-\\eta)\\rho(x,x_0)}\\varphi(x)d\\mu(x)$ for Lipschitz $\\varphi$. The cancellative axiom requires decay $(1+|\\xi-\\eta|R)^{-1/a}$; if the true decay is slower, this modulation family violates (1.7). A more decisive falsifier would be a family satisfying all hypotheses but for which the restricted weak-type estimate (1.13) fails.","tokens_in":40264,"feed_emoji":"📐","tokens_out":12758,"duration_ms":124231,"temperature":0.7,"pith_summary":"Maximally modulated singular integrals, the Carleson operators, have until now been understood mostly on Euclidean space, where modulation functions are polynomials. This paper replaces that algebraic structure by axioms: a compatible family of continuous modulation functions carrying a ball-dependent metric that controls their oscillation, and a cancellative axiom that supplies quantitative decay of oscillatory integrals. Under these axioms, plus an $L^2$ bound on the non-tangential maximal truncation of the kernel, the generalized Carleson operator satisfies restricted weak-type $(q,q)$ estimates for $1<q<2$ (Theorem 1.1), and a linearized version holds under a weaker per-modulation hypothesis (Theorem 1.2). The results cover the classical Carleson-Hunt theorem, modern polynomial Carleson theorems, and non-polynomial modulation classes in one framework, and the proof has been computer-verified in a formal system.","feed_headline":"Carleson operators get Lp bounds on doubling metric spaces","feed_subtitle":"One L2 condition and a few metric axioms extend Carleson's Fourier convergence theorem far beyond Euclidean space.","key_machinery":"The machinery is a tile structure linking a dyadic grid on $X$ to a covering of the modulation space $\\Theta$ by balls in the family of metrics $d_B$; tiles are then organized into forests (collections of trees where the modulation is effectively constant and separated) and antichains (almost orthogonal individual tiles). The cancellative axiom (1.7) is converted by a Hölder van der Corput estimate into the oscillatory decay needed for tile correlation, and the whole proof reduces to the forest and antichain operator estimates.","core_discovery":"The central claim is a conditional restricted weak-type theorem: on any doubling metric measure space, any cancellative compatible family of modulations, and any one-sided Calderón–Zygmund kernel with an $L^2$ bound on its non-tangential maximal truncation, the generalized Carleson operator satisfies $|\\int_G Tf\\,d\\mu|\\le 2^{443a^3}(q-1)^{-6}\\mu(G)^{1-1/q}\\mu(F)^{1/q}$ for $1<q\\le2$, hence $L^q$ bounds for $1<q<2$. A linearized version weakens the hypothesis by fixing the modulation choice and truncating at the radius where the selected modulation remains close to a tile's modulation.","pith_inferences":["The cancellative axiom is probably not needed at full strength: the Hölder van der Corput step suggests that any polynomial decay rate in (1.7) would drive the same proof with worse constants.","A concrete payoff to test is the family of distance functions or Busemann functions in hyperbolic and CAT(0) spaces; checking the metric axioms (1.3)-(1.6) and the cancellative estimate (1.7) there would yield genuinely non-algebraic Carleson theorems.","The constants such as $2^{443a^3}$ are likely far from optimal; optimizing the dependence on $a$ and $q$, or proving a matching lower bound for a natural modulation family, would clarify how much the cancellative axiom costs."],"forward_implications":["The classical Carleson-Hunt theorem is a special case: Euclidean line, Hilbert kernel, linear modulations, so almost-everywhere convergence of Fourier series in $L^2$ follows from the framework.","Known polynomial Carleson theorems, Stein-Wainger type modulations, and non-polynomial modulation classes are subsumed under one set of axioms with explicit constants.","Any doubling metric measure space admits a Carleson theorem once its modulation family is shown compatible and cancellative, opening the way to Carnot groups, manifolds with doubling measure, and fractal spaces.","The linearized version supplies the missing ingredient for a Walsh-Carleson-type deduction where only a selection-function-adapted $L^2$ bound is available."],"supporting_citations":[{"why":"Supplies the maximal polynomial modulation framework and the forest/antichain decomposition that this proof refines.","marker":"[Zor21]"},{"why":"Provides the pointwise-convergence tile dichotomy that organizes tiles into forests and antichains.","marker":"[Fef73]"},{"why":"Gives the dyadic grid existence theorem for spaces of homogeneous type used to construct the tile structure.","marker":"[Chr90]"},{"why":"Contributes the polynomial Carleson operator method and the tree estimates adapted here.","marker":"[Lie20]"},{"why":"Is the sibling communication that computer-verifies Theorems 1.1 and 1.2, making the proof machine-checked.","marker":"[BdFD+25]"},{"why":"Defines the classical Carleson operator whose convergence theorem motivates the generalized modulation framework.","marker":"[Car66]"},{"why":"Provides the first $L^p$ bounds for the classical operator, a benchmark the axioms must reproduce.","marker":"[Hun68]"}],"fun_headline_variants":["Generalized Carleson theorem extends to doubling metric spaces","Maximal modulations bounded on doubling metric measure spaces","Conditional Lp bounds for Carleson operators on metric spaces","Axiomatic Carleson operators: Lp bounds beyond Euclidean"],"cache_read_input_tokens":2816,"weakest_assumption_plain":"The load-bearing premise is the cancellative axiom (1.7): for every ball and every pair of modulation functions, oscillatory integrals against Lipschitz test functions must decay at the polynomial rate $(1+d_B(\\vartheta,\\theta))^{-1/a}$; if some natural modulation class misses this rate, the conclusions of Theorem 1.1 do not follow.","fun_headline_variants_meta":{"raw":{"variants":["Generalized Carleson theorem extends to doubling metric spaces","Maximal modulations bounded on doubling metric measure spaces","Conditional Lp bounds for Carleson operators on metric spaces","Axiomatic Carleson operators: Lp bounds beyond Euclidean"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000622,"raw_usage":{"total_tokens":2677,"prompt_tokens":658,"completion_tokens":2019,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":402,"completion_tokens_details":{"reasoning_tokens":1949}},"tokens_in":402,"tokens_out":2019,"duration_ms":17225,"temperature":1.0,"reasoning_tokens":1949,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T23:14:10.425504+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a ball $B$ in hyperbolic space, with $\\Theta=\\{\\xi\\cdot \\rho(\\cdot,x_0):\\xi\\in\\mathbb{R}\\}$ and $d_B$ the oscillation metric, and compute $\\int_B e^{i(\\xi-\\eta)\\rho(x,x_0)}\\varphi(x)d\\mu(x)$ for Lipschitz $\\varphi$. The cancellative axiom requires decay $(1+|\\xi-\\eta|R)^{-1/a}$; if the true decay is slower, this modulation family violates (1.7). A more decisive falsifier would be a family satisfying all hypotheses but for which the restricted weak-type estimate (1.13) fails.","supporting_citations":[],"review_version":1}