# Verification report — OWR-8415343-001 (Chruściel: a composition estimate for Fourier series with the supremum in time inside the sum)

Verification date: 2026-10-09.

**Verdict.** The note gives a **complete answer to the question as posed: yes.** Every statement it makes is
proved, and the scope is as follows.
- **Settled.** For every smooth G with G(0) = 0 and every s > 1 there is a constant C₂ = C₂(G, s), explicit, such
  that Σ_ℓ (1+|ℓ|)^{2s} sup_t |(G∘φ)_ℓ(t)|² ≤ C₂ Σ_ℓ (1+|ℓ|)^{2s} sup_t |φ_ℓ(t)|² whenever the right-hand sum is at most
  1 (inequality (11) of the source, with the index set Z²; Corollary 1.3). The same holds in every dimension d ≥ 1
  for s > d/2, and for every G ∈ C^k with G(0) = 0 and k > M_* + 3/2, where M_* = (s + d/2)·max{1, 1/(s − d/2)}.
- **Sharpness, partly.** The underlying bound for exponentials (Theorem 1.1) has the exponent s + d/2 when
  s > 1 + d/2, and this exponent is attained (Proposition 1.4). Some smoothness of G is necessary: for every
  k < s + d/2 the estimate fails for some G ∈ C^k with G(0) = 0 (Proposition 1.5).
- **Not new mathematics in the method.** The proof follows a known scheme: Leblanc (1969) for weighted Wiener
  algebras, Reich and Sickel (2016) for modulation spaces. The scheme of the necessity result is that of Katznelson
  (1959) and Leblanc. What was not found in the literature is the estimate for this space (supremum over the
  parameter inside the ℓ² sum) and the lower bounds. No priority is claimed.
- **Open.** The exact growth rate of the exponentials for d/2 < s ≤ 1 + d/2 (for d = 2: 1 < s ≤ 2; the exponent is
  not determined for s < 1 + d/2, and for s = 1 + d/2 it is s + d/2 without a bound of exactly this power); the minimal
  smoothness of G (between s + d/2 and M_* + 3/2); the constants are explicit but very large (10^34 to 10^46 in a
  worked example); the paper of Chruściel and Tod for which the estimate is needed was not found, so its use of
  the estimate could not be checked.

The note is unrefereed.

## Statement checked
- **Primary source.** P. T. Chruściel, "Quo Vadis, Mathematical GR?", in: Mathematical Aspects of General
  Relativity (Oberwolfach workshop 2021, organised by C. Cederbaum, M. Dafermos, J. Isenberg, H. Ringström),
  Oberwolfach Reports 18 (2021), no. 3, Report No. 40/2021, pp. 2157–2267, doi:10.4171/OWR/2021/40; the abstract is
  on pp. 2167–2174, the question in its Section 3.3 on pp. 2170–2171, equations (5)–(12).
  - Read in the publisher's file of the report (open access; 1,295,115 bytes, sha256
    `6f260196006d0b22157e91804245d560b5f5e255a1ca1581556376e6682d4742`) and in arXiv:2112.02126v1 (the only
    version; title there "Quo Vadis, Mathematical General Relativity?"; 138,766 bytes, sha256
    `70efa259dbb75a5a568d508101cfccb78cc91f78d91c3e0da9ef2d766083d4bd`). The two texts of Section 3.3 agree up to
    notation (ln P in the report, log P on arXiv). The third verification run fetched both files again and read
    pages 2167 and 2170–2174 of the report and pages 4–5 of the arXiv version, as page images and in the text
    layer of the files.
  - Setting: the flat square torus T² = [0,2π] × [0,2π]; basis f_ℓ(x) = (2π)^{-1} e^{iℓ·x} (5); φ_ℓ and (G∘φ)_ℓ the
    coefficients of φ and of G∘φ (6), (7); G: R → R smooth with G(0) = 0.
  - The classical estimate (8), (9): for s > 1, ‖G∘φ‖_{H^s} ≤ C(‖φ‖_{L^∞}) ‖φ‖_{H^s}; the source says that (8) is
    equivalent to its form (9) with the coefficients "after multiplying the function C by a constant if necesary".
  - The question: for φ = φ(t), t ∈ [t₋, t₊], and N_s(φ) = Σ_ℓ (1+|ℓ|)^{2s} sup_t |φ_ℓ(t)|²: given a smooth G with a
    first-order zero at the origin and s > 1, is there C₂ = C₂(G, s) such that N_s(φ) ≤ 1 (10) implies
    N_s(G∘φ) ≤ C₂ N_s(φ) (11)? The source notes that (8) only gives (12), with the supremum outside the sums.
  - Theorem 1 of the source (existence and uniqueness for the Einstein–Maxwell Robinson–Trautman equations with
    small data given partly at u₋ and partly at u₊) is stated under the assumption (11) and attributed to its
    reference [9], a paper of Chruściel and Tod listed without journal or preprint number.
- **Corpus record.** ulamai/UnsolvedMath, OWR-8415343-001 (dataset version 1.6.0; upstream status `open`). Its
  statement ends with "≤ C_2?": the factor N_s(φ) on the right of (11) is missing, which is a weaker statement. It
  keeps the index set N² of the source.

## Readings
| Reading | Answer | Where |
|---|---|---|
| Inequality (11) as in the source, index set Z², squares read as squared moduli, pointwise supremum over t | holds for every smooth G with G(0) = 0, with explicit C₂ | Corollary 1.3(b) |
| Index set N² literally, as printed | not an orthonormal basis; (11) would fail trivially for G(u) = u + u² (φ = A cos(x₁ − 2x₂) + B cos(2x₁ − x₂)); not the intended reading | Section 1.1 |
| Real orthonormal basis of products of cosines and sines, indexed by pairs of non-negative integers; other equivalent weights | same answer, constant a² C_B² with a = 4 for the real basis | Corollary 6.1(b) |
| Corpus form: right side of (11) replaced by a constant | follows from (11); also holds without G(0) = 0 | Corollary 6.1(a) |
| G of finite smoothness | (11) holds for G ∈ C^k, G(0) = 0, k > M_* + 3/2; for d = 2: k > s + 5/2 if s ≥ 2, k > (s+1)/(s−1) + 3/2 if 1 < s < 2 | Corollary 1.3 |
| G of low smoothness | (11) fails for some G ∈ C^k with G(0) = 0, G′(0) = 1, for every integer 1 ≤ k < s + 1 (d = 2) | Proposition 1.5 |
| Families continuous or smooth in t | the positive results apply; the negative results hold with such families | Remark 7.2 |
| Analytic G (entire, or analytic in a disc of radius > c_s K_s/(2π)) | (11) follows from the algebra property, with small constants (C₂ ≤ 20.9 for G(u) = e^{2u} − 1, s = 2) | Proposition 2.5, Section 9.1 |
| Vector-valued G, complex-valued families; differences | covered | Corollaries 6.2, 6.3 |
| Dimensions d ≠ 2 | every d ≥ 1, s > d/2 | Theorems 1.1, 1.2 |
| The application (Theorem 1 of the source) | not examined; the paper of Chruściel and Tod was not found | Section 1.5 |

## Results in the paper
Notation: ⟨ℓ⟩ = 1 + |ℓ|; c_ℓ(u) Fourier coefficients on T^d; a family is a map t ↦ u(t) on an arbitrary index set;
env(u)_ℓ = sup_t |c_ℓ(u(t))|; ‖u‖_X = (Σ ⟨ℓ⟩^{2s} env(u)_ℓ²)^{1/2}; for d = 2, N_s = 4π² ‖·‖_X². σ = s − d/2;
θ ∈ [0,1], θ < σ; κ = 1 + (1−θ)/σ; M = (s + d/2)κ.
- **Theorem 1.1 (exponentials).** ‖e^{iλψ}‖_X ≤ C_A (1+|λ|)^M for every family ψ of real-valued functions with
  ‖ψ‖_X ≤ 1, with the explicit constant C_A of (1.4). M = s + d/2 if σ > 1 (θ = 1).
- **Theorem 1.2 (composition, measure form).** If G(u) = ∫ (e^{iλu} − 1) dμ(λ) with
  J_μ(r) = ∫ |λ| (1 + r|λ|)^M d|μ| < ∞, then ‖G∘φ‖_X ≤ 2 c_s K_s C_A J_μ(r) ‖φ‖_X for ‖φ‖_X ≤ r.
- **Corollary 1.3.** C^k functions with k > M + 3/2 (constant (1.6)) or k > M + 2 (constant (1.7)); the answer to
  the question for d = 2 with C₂ = C_B², r = 1/(2π).
- **Proposition 1.4 (lower bound).** A family Φ of smooth functions (all slopes a ∈ [−c,c]^d of one profile,
  ψ^a(x) = Σ_j a_j ψ₀(x_j)), ‖Φ‖_X ≤ 1, with ‖e^{iλΦ}‖_X ≥ c_* λ^{s+d/2}, while sup_{u∈Φ} ‖e^{iλu}‖_{H^s} is of order
  λ^s. So Theorem 1.1 is sharp for s > 1 + d/2, and the loss λ^{d/2} against the supremum-outside norm is real.
- **Proposition 1.5, Proposition 8.1, Corollary 8.2 (necessity).** For k < s + d/2 a residual set of G ∈ C^k with
  G(0) = 0 has ‖G∘(rΦ)‖_X = ∞ (Baire category; test functions sin λu, cos λu − 1; the lower bound of Proposition
  1.4). Hölder classes C^{k,α}, k + α < s + d/2, likewise. In the scale A_β(T) of weighted Wiener algebras and for
  s > 1 + d/2: all G ∈ A_β operate if and only if β ≥ s + d/2.
- **Proposition 2.5.** Analytic G by the algebra property: ‖G∘φ‖_X ≤ G̃′(c_s K_s ‖φ‖_X) ‖φ‖_X.
- **Corollaries 6.1–6.3.** Variants (no G(0) = 0; other weights; real basis), several functions and complex-valued
  families, differences.
- **Remark 6.4.** The map λ ↦ e^{iλφ} − 1 is continuous in the norm of the space of families; the proof of Theorem
  1.2 forms no vector-valued integral, and one could be formed.
- **Proposition 9.1.** For d = 1 and 1/2 < s < 1 the norm of exponentials on the unit ball grows at least like
  λ^{3/2} > λ^{s+1/2}.
- **Tables and figure.** Table 1: the case d = 2. Table 2: constants for d = 2 (log₁₀ C_A between 8.66 and 12.37
  in the examples). Figure 1: d = 1, s = 2, upper bound against the computed lower bound and the single-function
  norms.

## Computations (sanity checks; programs and outputs in reproducibility/)
No proof depends on a computation. All computations are floating point.
- **Programs written with the note** (`writing_stage/`). `constants_table.py`: Table 2 with upper bounds for the
  lattice sums K_τ; the worked example (log₁₀ C₂ ≤ 45.6, 34.0, 39.0 for (s, θ) = (2, 0), (2, 0.9), (3, 1) with the
  closed bound for J_μ; 33.2, 27.6, 31.0 with J_μ by quadrature); C₂ ≤ 20.9 for G(u) = e^{2u} − 1, d = 2, s = 2.
  `check_prop_E.py`: the proof of Proposition 9.1 as printed, for s = 0.6, 0.75, 0.9 and λ = 16, …, 1024 (norm of
  the family ≤ 0.71; for each s and λ the smallest modulus of the coefficients lies between 0.082 and 0.094,
  against the required 1/(32π); lower bound divided by λ^{3/2} between 0.072 and 0.084; all tested inequalities
  hold). The program was corrected after the third run: in three cases it had taken K one smaller than the K of
  the proof (see below); its first output is kept. `make_figure.py`: Figure 1 from saved outputs.
- **Programs with which the results were first obtained** (`original/`). `check_lemmas.py`: 36 configurations in
  d = 1, 2, all pass. `check_lemma6_adversarial.py`: 500 optimised cases for Lemma 3.1(ii), no violation.
  `growth_experiment.py`: d = 1, s = 1, six envelopes, λ = 8, …, 1024; polynomial growth, local slopes between 0.82
  and 2.10. `lower_bound_illustration.py`: b(n) decreasing from 0.431 to 0.3306 for n ≤ 20000 (limit 1/π);
  lower bound Q_C(λ) with local slopes 1.49, 2.48–2.49, 3.42–3.49 for s = 1, 2, 3, against 1.00, 2.00, 2.96–3.00
  for the largest single-member H^s norm.
- **Verification run A** (`verification_run_A/`). Tests T1–T8 of the lemmas and of the assembled Steps 0–6 (all
  pass; 11,608,728 comparisons for Lemma 3.1(ii) on optimised members in d = 1, 2; 192 configurations for Step 4);
  Lemmas 2.1 and 3.2 by direct lattice sums in d = 1, 2, 3 (largest ratios left/right 0.65 and 0.25); the two
  moment bounds of Corollary 1.3 on a function with explicit transform (eight parameter sets); the constants with
  two-sided brackets for K_τ; 26 optimisation runs in d = 1 and d = 2 (4.9·10⁶ function evaluations): polynomial
  growth everywhere, every value below 4.5·10⁻⁶ times C_A (1+λ)^M; an explicit λ-dependent family in d = 1 with
  growth λ^{3/2} (the construction behind Proposition 9.1).
- **Verification run B** (`verification_run_B/`). Proposition 1.4 with two profiles (b(n) ≥ 0.3352 for n ≤ 2048 for
  the profile of the note; local slopes of the lower bound tending to s + 1/2; the product formula (7.1) in d = 2
  to 10⁻⁸); the other construction for the bound λ^{3/2}; the inequalities of the second route (2520 tests, no
  violation).
- **Third verification run** (`independent_run_2/`; four programs written from the text of the note before the
  programs of the package were read). `run2_constants.py`: two-sided enclosures of the lattice sums for d = 2
  (K_{1.1} ∈ [5.1570749, 5.1571685], K_{1.5} ∈ [1.9155085, 1.9155088], K₂ = 1.2985901, K₃ = 1.0498762,
  K₄ = 1.0103028); all entries of Table 2 are valid, K_s, B_R and log₁₀C_A being upper bounds (the rows θ = 0.4 and
  θ = 0.9 rest on K_{1.1} ≤ 5.172; with the enclosure B_R ≤ 1984.7 and 364.1, log₁₀C_A ≤ 10.071 and 9.628); worked
  example log₁₀C₂ ≤ 45.588, 33.988, 38.964 (closed bound) and 33.157, 27.557, 30.974 (quadrature); C₂ ≤ 20.8992,
  22.4403, 57.9617 for e^{2u} − 1; C_A = 1.53575·10⁵ for Figure 1. `run2_lemmas.py`: Lemmas 2.1(c), 3.2 in
  d = 1, 2, 3; Lemmas 2.2, 3.1 and the six steps of Section 5 in d = 1, 2 (312 cases, 202 with a non-empty high
  part); Lemma 2.3 and inequality (6.1) in d = 1: 3,633,574 comparisons, 0 violations. `run2_prop91.py`: Proposition 9.1 as printed for
  two profiles, s = 0.6, 0.75, 0.9, λ = 16, …, 1024, all members, each coefficient by direct sampling of the
  function: all inequalities of the proof hold in the 42 cases; moduli of the coefficients ≥ 0.0825; lower bound
  divided by λ^{3/2} between 0.0739 and 0.0972. `run2_lower_bound.py`: (7.1) in d = 2 to 5.8·10⁻¹⁵; b(n) from
  0.43132 to 0.33059 (n ≤ 20000); local slopes of Q_C between 2.478 and 2.495 for 10³ ≤ λ ≤ 10⁵ and of the largest
  H^s norm of a member between 1.995 and 2.000; factor 1.499·10⁷ to the upper bound at λ = 10⁵; in d = 2 the lower
  bound is 40 to 150 times the bound of the proof; Corollary 6.1(b) (quotient between 0.80 and 1.44 on 60 random
  families); the index-set example; the bounds (1.6), (1.7). Three superseded outputs of this run, which document
  errors of its own tests, are kept and described in `independent_run_2/README.md`.
- **Re-runs.** On 2026-10-09 all programs except the 26 optimisation runs of run A were run again, one process at
  a time: twice at the writing, once by the third run from the archive as it was before the revision (0 comparisons
  not identical), and a last time from an extracted copy of the revised archive, now including the four programs of
  the third run (0 comparisons not identical; 24 minutes). The result of the last run is recorded in
  `reproducibility/RERUN_LOG.txt`; `reproducibility/run_quick.sh` repeats it. Of the 26 optimisation runs of run A
  the third run repeated three as a spot check (`single_AP`, `lacdiag_AP`, `flat8_P`): logs identical up to the
  running times, all stored arrays identical. The other 23 were not repeated.

## Independent verification runs
The results were first obtained on 2026-10-09 with complete proofs. A first independent reading of that version
(AI-assisted, without knowledge of the reasoning behind it) found no error in the proofs and led to corrections of
wording (the statement on other bases, now Corollary 6.1(b), is restricted to the basis of products of cosines and
sines) and of one program (a round-off error in a norm). Three independent verification runs, all AI-assisted,
followed on the same day; each wrote its own programs. Runs A and B examined that first version, and neither read
the report of the other. The third run examined the final text of the note (its folder is `independent_run_2/`,
named after the second stage of the verification).

| Item | Run A | Run B | Third run (final text) |
|---|---|---|---|
| Statement against the source (index set, position of the supremum, factor N_s(φ) in (11), corpus text) | CONFIRMED (publisher's file and arXiv v1 read) | source read again; consistent | CONFIRMED (both files fetched anew, pages read as images; every statement of Section 1.1 compared; two precisions of wording required) |
| Lemmas 2.1–2.4, 3.1, 3.2, 4.1 | CONFIRMED (re-derived; tested) | re-derived, correct | CONFIRMED (re-derived from the printed text; tested in d = 1, 2, 3) |
| Theorem 1.1 (exponent M, constant C_A) | CONFIRMED (six steps re-derived) | CONFIRMED by a second route for s ≥ 1 (same exponent, other constant); the six steps re-derived, correct | CONFIRMED (six steps as printed; both regimes of σ; tested in d = 1, 2) |
| Theorem 1.2 | CONFIRMED (Fubini, semicontinuity, Minkowski; no vector-valued integral) | re-derived, correct | CONFIRMED; the question of strong measurability decided (below) |
| Corollary 1.3 (k > M + 2 and k > M + 3/2; the answer) | CONFIRMED | part (a) re-derived, correct | CONFIRMED (both constants re-derived and tested) |
| Corollaries 6.1–6.3 | CONFIRMED | read, not recomputed line by line | CONFIRMED (6.1(b) also tested) |
| Proposition 2.5 (power series) | the case e^{2u} − 1 | not its part | CONFIRMED; the values 20.9, 22.5, 58.0 recomputed |
| Explicit constants | CONFIRMED; two table rows valid but not sharpest | two programs re-run, outputs reproduced | CONFIRMED with two-sided enclosures: all printed values valid |
| Proposition 1.4 | not its part | CONFIRMED (every step; constants c_*, λ_*) | CONFIRMED in the printed form (one family independent of λ) |
| Proposition 1.5 | not its part | CONFIRMED; stronger forms proved (one family, residual set, non-integer smoothness) | CONFIRMED as derived from Proposition 8.1, with the Hölder classes |
| Proposition 8.1, Corollary 8.2 (printed form) | not seen | proved in its report in another form (complex functions e^{iλu} − 1) | CONFIRMED line by line |
| Proposition 9.1 (printed proof) | found the bound, with another proof | found independently by another construction (all s > 1/2) | CONFIRMED line by line and by its own program; thresholds for λ made explicit |
| Literature and novelty | not its part | statement NOT FOUND in the literature; method known; five corrections required | sources read again; statement NOT FOUND; four corrections of wording required |

No run found a wrong theorem, proposition or lemma.

**Corrections required by run B** (literature), all applied in the note:
1. The method is attributed to Bourdaud, Reissig and Sickel (2003) only through Reich and Sickel, who name it as a
   predecessor; that paper was read by nobody here (Section 1.4, "Scope and priority").
2. The hypotheses of Kato, Sugimoto and Tomita (2020), Theorem 1.1, are stated exactly (real f, 1 ≤ p < ∞,
   4/3 ≤ q < ∞, or p = q = ∞; s > n/q′), with the remark of the authors that p = ∞, q < ∞ is excluded; Reich and
   Sickel need 1 < p < ∞ and leave p = ∞ open in their Remark 4.11 (Section 1.4).
3. Leblanc bounds the low coefficients by the Cauchy–Schwarz inequality with Parseval's identity; his Théorème 2
   has the strict inequality β > 1 + 1/(2α). Under the mode-by-mode supremum Parseval is lost, which is why the
   exponent is s + d/2 here (Section 1.4).
4. Katznelson (1959, Théorème 5.7 and Corollaire) and Leblanc (Théorème 1) are credited for the scheme of
   Proposition 1.5; the contribution of the note to it is the lower bound of Proposition 1.4 (Sections 1.4, 8).
5. Bhimani and Solanki (arXiv:2507.16516) are cited as the closest framework (vector-valued weighted Fourier
   algebras); their results concern real-analytic functions and a converse for q < 2 (Section 1.4). An unchecked
   side observation of run B about one of their theorems is not repeated.

**Recommendations of runs A and B, applied:** the condition k > M + 3/2 is stated inside Corollary 1.3 (run A); the
sharper values of the constants are given (run A); the size of the constants is stated plainly, with the
comparison for an entire function (run A); Theorem 1.1 says that the index set is arbitrary (run A); the last
sentence of Proposition 1.4 is quantitative (run B); the statement on the growth exponent is corrected for d = 1,
s < 1 (both runs); the stronger forms of Proposition 1.5 are stated (run B).

**Changes made when the note was written, after runs A and B.**
- Corollary 1.3 states k > M + 3/2 with the constant (1.6); run A had re-derived this (as a remark of the first
  version).
- Proposition 1.4 is stated for one family Φ which does not depend on λ (all slopes in a cube); run B had proved
  this form. The finite families of the first version are the subfamilies used in the proof.
- Proposition 1.5 is derived from Proposition 8.1, and Corollary 8.2 is added; both are taken from the report of
  run B, where they are proved, and were rewritten for real-valued functions (sin λu and cos λu − 1 in place of
  e^{iλu} − 1).
- Proposition 9.1: the printed proof follows the construction of run A (slopes of a smooth sawtooth plus one high
  mode), with the profile of Section 7 and the amplitude 1/(2λ) of the high mode, so that only the elementary
  bounds |a₁| ≥ 1/8 and Σ|a_m| ≤ e^{1/2} are needed.
- Proposition 2.5 is stated for power series (run A proved the case G(u) = e^{2u} − 1).
- A parenthetical remark of run A, that the map λ ↦ e^{iλφ} − 1 into the space X need not be strongly measurable, was
  not repeated.
- Table 2 is recomputed by `writing_stage/constants_table.py` with sharper bounds for K_τ.

**The third run: what it examined, and the result.** It examined the final text, and the parts changed at the
writing first.
- *Mathematics.* It re-derived line by line Proposition 8.1, Corollary 8.2, the proof of Proposition 1.5 with the
  Hölder classes, Proposition 9.1, and the statement and proof of Proposition 1.4; then every lemma and constant of
  Sections 2–6 (cut-off frequency and its uniformity; the bound 1 for the coefficients of the unimodular low part;
  the gradient recursion; the majorant series; the weighted Young inequality with its constant; the exponent M for
  σ > 1 and for σ ≤ 1; d = 1, 2, 3), the proof of Theorem 1.2, the corollaries with the two conditions k > M + 3/2
  and k > M + 2 and their constants, Proposition 2.5, Remark 7.2 and the remarks of Section 9. It found no wrong
  statement and no gap.
- *Strong measurability: the point decided.* Run A had written that λ ↦ e^{iλφ} − 1 need not be strongly measurable,
  because the space of families is not separable. The space is indeed not separable for an infinite index set, but
  the map is continuous: ‖e^{ihφ} − 1‖_X ≤ |h| ‖m‖_s e^{c_s|h|‖m‖₁} by Lemma 4.1, and
  ‖e^{iλφ} − e^{iλ′φ}‖_X ≤ 2c_sK_s ‖e^{iλ′φ}‖_X ‖e^{i(λ−λ′)φ} − 1‖_X by Lemma 2.4. A continuous map of the real line has
  separable range and is strongly measurable. So the remark of run A was not correct, and the decision taken at the
  writing was right. The proof of Theorem 1.2 forms no vector-valued integral in any case; the space of families
  with finite norm is complete, so that the integral can also be read as a Bochner integral, as Reich and Sickel
  do in the proof of their Theorem 4.13 (their Lemma 4.12 is this continuity). The note now contains Remark 6.4.
- *Sources.* Fetched anew and read: Section 3.3 of the source in both versions, with the entry [9] of its list of
  references (p. 2173 of the report);
  Leblanc completely; Katznelson pp. 101–103 and 110–111; Reich–Sickel (introduction, Proposition 2.4, Proposition
  4.10, Remark 4.11, Lemma 4.12, Theorem 4.13 with its proof, final remark); Kato–Sugimoto–Tomita (introduction,
  Theorems 1.1, 1.2, the proof of Theorem 1.1); Bhimani–Solanki (abstract, Section 1 up to Remark 1.5); the
  abstract and introduction of the survey of Bourdaud and Sickel. The attributed statements are exact, with the
  exceptions corrected below.
- *Corrections required by the third run* (twelve; all made):
  1. The Verification paragraph describes the final state.
  2. Section 1.1: "(8) is equivalent to (9)" with another function C, as in the source; "What was read": the two
     versions agree up to the notation ln P / log P.
  3. Abstract and "Scope and priority": the phrase that the two closest composition theorems "exclude exactly the
     corresponding case" is replaced: their hypotheses do not admit the case p = ∞, q = 2, which corresponds to the
     question by analogy only (the two theorems exclude other cases as well, and they are theorems about another
     space).
  4. Section 1.2: Katznelson's Théorème II.1 is a statement for an open interval (closed intervals: its
     Corollaire).
  5. Section 1.4: Bhimani and Solanki remark that their converse fails for q = 2 without weight (Remark 1.3); the
     sentence that they "contain no statement on non-analytic functions for q = 2" is replaced by: they prove no
     composition theorem for functions which are not analytic.
  6. Proposition 9.1: the proof started "for λ > 0", although K is defined only for √2 λ ≥ 1, the envelope bound
     needs K ≥ 1, and K > L is used before it is secured; the proof now starts with λ ≥ 2, introduces λ₁ and
     λ_E = max{λ₁, 2n₀/c′}, and every step names its range. In `check_prop_E.py`, K was one smaller than the K of
     the proof in the three cases s = 0.75, λ = 16, 128, 1024 (exact equality (1+K)^s = √2 λ, rounding in the
     floor): corrected, first output kept, five lines changed, no tested inequality affected. Section 10 now says
     that the range 0.082–0.094 is that of the smallest modulus for each s and λ (the moduli reach 0.105).
  7. Small precisions: Proposition 1.4, last sentence, for λ ≥ λ_* and with a constant c > 0; the Hölder space in
     the proof of Proposition 1.5 with G(0) = 0; Corollary 8.2: the case φ = 0, Λ₀ = {1, 2, 3, …}, and the norm of
     S_n and C_n as an equality.
  8. Remark 6.4 on the continuity of λ ↦ e^{iλφ} − 1.
  9. "Scope and priority": three of the four works citing the source are on arXiv (all three were searched); what
     the third run read; the totals of the searches.
  10. Section 10: five parts, three verification runs, the folder `independent_run_2/`.
  11. Package: this report, `reproducibility/independent_run_2/` with a README, `README.md`, `run_quick.sh`, the
      archive and the Zenodo metadata.
  12. A draft of the notice for the problem collection.
- *Not changed, considered:* Table 2 keeps its values (valid upper bounds from the note's own program; the sharper
  enclosure of K_{1.1} is reported above and in the Verification paragraph). A remark on norms with the supremum
  inside dyadic blocks only was not added: nobody here checked it against a source.

## Relation to the literature, novelty and scope
- **Searches (9 October 2026; first investigation, runs A and B, the writing, and the third run).** 69 queries to
  the arXiv API (modulation, Fourier–Lebesgue and Wiener amalgam spaces and weighted Fourier algebras combined with
  composition, superposition, operating functions, Nemytskij operators; vector-valued and parameter-dependent
  variants; the paper of Chruściel and Tod; later work of its two authors), 29 to zbMATH, 33 to Crossref, further
  queries to OpenAlex, INSPIRE and Semantic Scholar (among them the lists of works citing the source, Reich–Sickel
  and Kato–Sugimoto–Tomita), and six web searches. The counts include the bibliographic checks. Of these the third
  run made 25 queries to the arXiv API (one further query was answered three times with the status 429 and was
  given up), 9 to zbMATH, 16 to Crossref, 5 each to OpenAlex and INSPIRE, and one web search.
  - No statement of the estimate for this space was found.
  - The two closest composition theorems that were found (Reich–Sickel, Theorem 4.13; Kato–Sugimoto–Tomita,
    Theorem 1.1) are for modulation spaces M^s_{p,q}(R^n); their hypotheses do not admit p = ∞ with q < ∞, which
    is the pattern of the question (supremum in the parameter inside, ℓ² in frequency outside). This
    correspondence is an analogy; the note does not claim a theorem about modulation spaces (Remark 9.3).
  - The paper of Chruściel and Tod (reference [9] of the source) was not found on arXiv, in INSPIRE, zbMATH,
    Crossref, OpenAlex or on the publication list of its first author; the third run looked through the 60 latest
    arXiv entries under the surname of the first author (December 2016 to July 2026) and the 25 latest under the
    name of the second (2018 to June 2026). INSPIRE lists four
    works citing the source (Ling 2024; Tahamtan, Flores-Alfonso and Svítek 2023; Wutte 2022; Nozawa 2024); none
    treats (11), by their titles and, for the three which are on arXiv, by a search of their texts. No later work
    was found which proves, uses or avoids (11).
  - One title seen for the first time in the last search: G. Bourdaud, "Composition in Sobolev spaces: a unified
    approach", J. Fourier Anal. Appl. 32 (2026), Paper 53 (doi:10.1007/s00041-026-10248-0). It was not read (no
    abstract in Crossref); by its title and its list of references in Crossref it concerns the classical Sobolev
    spaces of functions, without a parameter. It is not cited in the note.
- **What was read.** The source: Section 3.3 in the publisher's file and in arXiv v1. Leblanc (1969): all five
  pages (journal scan). Katznelson (1959): pages 101–103 and the statement of Théorème II.1 (Numdam scan); the
  rest not read. Reich–Sickel: arXiv v1, introduction, Proposition 2.4 and Section 4.3 from Proposition 4.7 to the
  end; published version not compared. Kato–Sugimoto–Tomita: arXiv v1, Sections 1–4 and the beginning of Section 5;
  published version not compared. Bhimani–Solanki: version 2, abstract and Section 1; proofs not read.
  Bourdaud–Sickel (survey, 2011): introduction, Sections 4.2.2 and 6, in the file on the RIMS site. At the writing
  the cited statements of Leblanc, Katznelson (pages 101–103, Théorème II.1), Reich–Sickel, Kato–Sugimoto–Tomita and
  Bhimani–Solanki were read again in the same files. The third run fetched all these files again (same sha256 as
  recorded by run B for the six files of the literature) and read the parts named in the preceding section.
- **Not read.** Bourdaud–Reissig–Sickel (2003) and the two papers of Kobayashi and Sato (2022): no accessible copy
  was found (the publisher's pages redirect to an identity service, which was not followed; Crossref and OpenAlex
  have no abstracts, zbMATH shows none). Helson–Kahane–Katznelson–Rudin (1959): not consulted. The textbooks of
  Folland and Katznelson are cited for standard facts; no particular statement was looked up.
- **Bibliography.** All entries were checked on 2026-10-09 with Crossref (10 requests), zbMATH (4) and the arXiv
  API (1) at the writing, and again by the third run: the ten DOIs in Crossref (authors, titles, volumes, pages or
  article numbers agree), the two Zbl numbers in zbMATH, the arXiv entry of the source.
- **Caveats.** A search that finds nothing is not a proof of novelty. The published versions of the two arXiv
  papers were not compared with the versions read.
- **Scope.** The note answers the question of the source as posed. It does not determine the exact growth rate for
  d/2 < s ≤ 1 + d/2 or the minimal smoothness of G, its constants are very large, and it says nothing about the
  conditional theorem of the source.

## Public release and license
This paper, its source files, and this verification report are licensed under the Creative Commons Attribution
4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/