feat(MagicFunction): Schwartzness of the eight-dimensional integrals Iⱼ and Jⱼ via smooth cutoff

[thefundamentaltheor3m]

(This is an experimental PR: I wanted to see if Claude could do this in a good way by launching and interacting with independent review agents along the way. This will be done in a much better way in #444.)

Schwartzness of the eight-dimensional integrals Iⱼ and Jⱼ

The one-dimensional integrals RealIntegrals.Iⱼ', Jⱼ' : ℝ → ℂ are not Schwartz functions as currently stated: they grow exponentially as x → -∞, and the sixth integrals are not even given by convergent integrals far to the left of the origin. The previous smooth'/decay' obligations in a/Schwartz.lean and b/Schwartz.lean were therefore unprovable. Since the eight-dimensional integrals are obtained by composing with ‖·‖² ≥ 0, only the behaviour on [0, ∞) matters — so we multiply by a smooth transition function (STF) that is 1 on [0, ∞) and vanishes far to the left, and compose that with ‖·‖².

What this PR does

1. New: ForMathlib/RadialSchwartz/SmoothCutoff.lean — fully proved, no sorries

• exists_smooth_cutoff : ∃ f : ℝ → ℝ, ContDiff ℝ ∞ f ∧ (∀ x ≤ -1, f x = 0) ∧ ∀ x ≥ 0, f x = 1 — this is precisely the statement of Existence of smooth cutoff function #316 (@mattcushman), obtained here in one term from mathlib's Real.smoothTransition. I could not make this PR depend on Existence of smooth cutoff function #316 in the git sense: its base branch schwartzness-dimensions shares no merge base with current main (the history was rewritten; 143 files / 12k+ lines and an older toolchain apart), so the statement is included and credited instead. If Existence of smooth cutoff function #316 is rebased and merged first, this lemma can be dropped in favour of it.
• SchwartzMap.ofNonnegDecay (f : ℝ → E) (a : ℝ) (ha : a < 0) (hf : ContDiffOn ℝ ∞ f (Ioi a)) (hdecay : …) : 𝓢(ℝ, E) — the Schwartz function x ↦ Real.smoothTransition (1 - 2x/a) • f x, given smoothness of f on (a, ∞) and Schwartz-type decay on [0, ∞) only. The transition vanishes on (-∞, a/2] and is 1 on [0, ∞). For a = -2 the cutoff is exactly smoothTransition (x + 1), i.e. the STF of Existence of smooth cutoff function #316 transitioning on [-1, 0].
• ofNonnegDecay_apply_of_nonneg / ofNonnegDecay_apply_of_le_half: it agrees with f on [0, ∞) and vanishes below a/2.

#print axioms: all three check with [propext, Classical.choice, Quot.sound] — no sorryAx.

2. a/Schwartz.lean: SchwartzIntegrals.Iⱼ' := ofNonnegDecay RealIntegrals.Iⱼ' (-2) …

• The false global decay obligations are replaced by provable ones, Iⱼ'_decay_nonneg (decay of all derivatives on [0, ∞)); the zeroth-order cases are supplied (up to integrating the bound) by the existing IntegralEstimates.Iⱼ'_bounding. The I₃' transfer trick of feat(Schwartz): prove I₃'_decay' #339 also ports verbatim to these restated bounds.
• I₆'_smooth' (false: the integral only converges for x > -2, by norm_φ₀_le) is replaced by I₆'_smoothOn : ContDiffOn ℝ ∞ I₆' (Ioi (-2)). I₁'…I₅'_smooth' are kept unchanged (compact contours; the existing conditional proof of I₃'_smooth' survives untouched).
• New main results: Iⱼ_coe : ⇑Iⱼ = RadialFunctions.Iⱼ and a_coe : ⇑a = RadialFunctions.a — the eight-dimensional Schwartz functions are equal to the radial functions, because the cutoff is invisible after composing with ‖·‖² ≥ 0 (via the existing schwartzMap_multidimensional_of_schwartzMap_real, i.e. SchwartzMap.compCLM with ‖·‖²).
• a'_eq_sum_RealIntegrals (false as a global function equality under any correct definition) is replaced by a'_apply_of_nonneg; a_eq_sum_integrals_SchwartzIntegrals remains rfl, and a_eq_sum_integrals_RadialFunctions keeps its statement with a two-line proof.

3. b/Schwartz.lean: same treatment for Jⱼ/b, with a = -1

The blueprint's bound ‖ψS z‖ ≤ C e^{-π Im z} (lemma:psi-bound) only guarantees convergence of J₆' on (-1, ∞), so a transition on [-1, 0] cannot work on the b-side; instead the cutoff transitions on [-1/2, 0]. This is the only asymmetry with the a-side, and is why ofNonnegDecay is parametrised by the threshold a.

Status of the remaining hypotheses

The 23 remaining sorries (11 on the a-side, 12 on the b-side) are exactly the corrected one-dimensional smoothness/decay statements — all now believed provable (Leibniz rule + the IntegralEstimates bounds, blueprint Prop. 7.8 / prop:b-schwartz). Everything built on top of them — the Schwartz structures, the equalities with RadialFunctions.Iⱼ/Jⱼ/a/b, and all downstream files (Eigenfunction, SpecialValues, g/Basic) — is fully verified: the sorry count is unchanged, but the statements are now true and the architecture sound.

Verification

• Full project build from source: lake build succeeds (3453 jobs), including all downstream consumers, with no new warnings from the touched files (style linters clean).
• #print axioms a_coe / b_coe: sorryAx enters only through the restated hypotheses above.

🤖 Generated with Claude Code

https://claude.ai/code/session_017PgeJjuvzNGKAeHZy9gxUn

---

Generated by Claude Code

[thefundamentaltheor3m]

🔍 Independent Review — Round 1

Overall. The structural core of this PR is genuinely good. SchwartzMap.ofNonnegDecay correctly diagnoses and solves the real problem — the 1-D integrals are not Schwartz on all of ℝ — it builds with no sorry and only standard axioms (verified below), and the a parameter is a well-justified generalisation of the requested STF. The 8-dimensional Schwartzness is reduced to the 1-D smoothness/decay exactly as the task framed ("based on the 1-D counterparts"), and — crucially — the restated 1-D statements are now true and provable, whereas the pre-PR ones were false. The remaining items are polish: a couple of unused declarations, helper lemmas that should be private, and a prose-only (unwired) link to the bounding lemmas.

Verification I ran. lake build of all three files: clean (3359 jobs, exit 0); the only warnings are sorry in the 1-D *_smooth' / *_decay_nonneg lemmas. #print axioms on ofNonnegDecay, ofNonnegDecay_apply_of_nonneg, ofNonnegDecay_apply_of_le_half, exists_smooth_cutoff, contDiff_transition_smul, decay_transition_smul → all [propext, Classical.choice, Quot.sound], i.e. no sorryAx. So the "no sorry / standard axioms" claim for SmoothCutoff.lean is true.

---

1. Faithfulness to the ask

✅ The essential fix is correct and is the heart of the task. Pre-PR, I₆'_smooth' asserted ContDiff ℝ ∞ I₆' on all of ℝ and Iⱼ'_decay' asserted decay for all x — both false (I₆' isn't even integrable below -2; every Iⱼ' grows like e^{-πxt} as x → -∞), so the old sorrys were unprovable. Restricting to ContDiffOn … (Ioi (-2)) and ∀ x ≥ 0 makes them true, and multiplying by the cutoff repairs Schwartzness. This is exactly right, and worth calling out as the main value of the PR.

✅ The a-parameter generalisation is justified, not gratuitous. The transition smoothTransition (1 - 2*x/a) must vanish inside the smoothness domain Ioi a; since I₆'/J₆' are only smooth on (-2,∞)/(-1,∞), a fixed STF wouldn't fit both. For a = -2 the transition is exactly smoothTransition (x + 1) — precisely the STF the task described (0 on (-∞,-1], 1 on [0,∞), transitioning on [-1,0]). Nice.

🟡 should-fix (defensible) — the analytic content is entirely deferred, and Iⱼ'_bounding is referenced only in prose. All Iⱼ'_decay_nonneg / Jⱼ'_decay_nonneg (and the *_smooth' / *_smoothOn) are sorry. The section docstring (a/Schwartz.lean:98-102) says the k=n=0 bounds "are provided … by Iⱼ'_bounding", but no code realises this — and I₁'_bounding (which is fully proven, IntegralEstimates/I1.lean:212) is unused by the decay lemma. This is a reasonable scope decision (the full ∀ k n decay needs differentiation-under-the-integral, and the *_smooth' lemmas were already sorry on main), and it's honest sorry-ing of the hypotheses the title says the result is "based on". But reviewers should understand the PR delivers the bridge, not the analytic inputs. Concretely, the k=n=0 case is wirable — for x ≥ 0, rexp(-πx/s) ≤ 1, so ‖I₁' x‖ ≤ ∫_{Ici 1} C₀·rexp(-2πs) =: C uniformly — so consider either discharging that base case from I₁'_bounding as a demonstration, or softening the docstring to mark the connection as intended/future.

🟡 should-fix — exists_smooth_cutoff (SmoothCutoff.lean:46) is dead code. It restates PR #316's statement but is never used anywhere (the construction inlines smoothTransition (1 - 2*x/a); grep confirms only the declaration + its own docstring reference it). Reproving it in 2 lines from Real.smoothTransition instead of depending on the unmerged #316 is a fine call — but then the theorem serves no purpose. Suggestion: delete it, or if you want to record that #316's statement is discharged, keep it with a one-line comment saying it is not used by the construction.

2. Idiomaticity & Mathlib quality

✅ ofNonnegDecay is well-designed at the right generality. Stating it over a general E : NormedAddCommGroup/NormedSpace ℝ is correct and free (iterated derivatives + decay make sense for any target), while fixing the source to ℝ is right because the half-line is ℝ-specific. It reuses Real.smoothTransition, the SchwartzMap structure, and schwartzMap_multidimensional_of_schwartzMap_real; only one new def is introduced. Modulo the domain-specific content, the shape would be acceptable in mathlib.

🟡 should-fix — make the two glue lemmas private. contDiff_transition_smul (:84) and decay_transition_smul (:96) are public in the SchwartzMap namespace, but their statements hardcode smoothTransition (1 - 2*x/a) and they're used only inside ofNonnegDecay (grep confirms no uses outside SmoothCutoff.lean). The four preceding transition lemmas are already private; these two should be too (naming-conventions "Helper Lemma Naming"; style "When to Use Private"). As-is they pollute SchwartzMap.* with implementation details.

🟢 nice-to-have — add the basic _apply unfolding lemma. There's ofNonnegDecay_apply_of_nonneg and ofNonnegDecay_apply_of_le_half (the latter is currently unused, :148 — fine as API), but not the most basic one:

@[simp] theorem ofNonnegDecay_apply (…) :
    ofNonnegDecay f a ha hf hdecay x = smoothTransition (1 - 2 * x / a) • f x := rfl

With it, the two conditional lemmas become by simp [transition_eq_one …] / [transition_eq_zero …] instead of change …; rw …, and downstream rewriting gets easier.

🟢 nice-to-have — the name ofNonnegDecay advertises only the decay hypothesis. The construction also requires smoothness on a right half-line and picks a specific cutoff. Terseness is a virtue, so this is not blocking, but a name hinting at the half-line/smoothness (or a short docstring line to that effect) would aid discoverability.

Naming is otherwise on-convention: _smoothOn for ContDiffOn, _decay_nonneg, _coe, _apply_of_nonneg. Header ordering (@[expose] public section after the module docstring) was actually fixed here relative to main — good.

3. Efficiency

✅ The two proofs are near-minimal for what they are. contDiff_transition_smul uses fun_prop and contDiffAt_const.congr_of_eventuallyEq cleanly; decay_transition_smul is a standard three-region bound (vanishing / compact / decay). This is exactly the "analysis boilerplate that doesn't golf well" category — no positivity/gcongr/fun_prop opportunities are being missed, and there's no nested-have bloat. by norm_num for (-2 : ℝ) < 0 is the right choice (positivity can't prove < 0).

🟢 nice-to-have — the middle split point is 1, not 0 (decay_transition_smul:113). Since the transition is already ≡ 1 on all of [0,∞), using the compact interval [a/2, 0] and the decay region x > 0 would be marginally more natural (and slightly shrink the constant). Purely cosmetic; the current split is correct.

4. Clarity, conciseness, cleanliness, modularity

✅ Excellent module docstrings and separation of concerns. The top-of-file docs explain why the 1-D functions fail to be Schwartz and how the cutoff repairs it (module docstrings may carry strategy — this is the right place for it). Putting the reusable bridge in ForMathlib/RadialSchwartz/SmoothCutoff.lean and the domain wiring in the MagicFunction files is good modularity. The Iⱼ_coe : ⇑Iⱼ = RadialFunctions.Iⱼ theorems are the cleanest possible statement of "Iⱼ is Schwartz", and I checked them against the Basic.lean definitions (RadialFunctions.Iⱼ x = Iⱼ' (‖x‖^2), and sq_nonneg supplies 0 ≤ ‖x‖^2) — mathematically sound.

🟢 nice-to-have — one docstring wraps mid-phrase (a/Schwartz.lean:24-25: "agreeing with / the Iⱼ'"). Trivial reflow.

---

What's done well (summary)

• Correctly identifies that the pre-PR 1-D sorrys were false statements, and fixes them by restricting to [0,∞) / Ioi a + cutoff. This is the crux and it's right.
• ofNonnegDecay: clean, general over E, sorry-free, standard axioms only (verified), minimal new definitions.
• a-parameter elegantly accommodates the I₆'/J₆' smoothness domains; recovers the requested STF at a = -2.
• Good reuse of existing infrastructure; good docstrings and file organisation; even fixed a pre-existing header-ordering lint.

Severity ranking

• Blocking: none — builds clean, axioms clean, structural goal met. (The sorrys are the 1-D inputs the result is explicitly "based on.")
• Should-fix: (a) make contDiff_transition_smul / decay_transition_smul private; (b) remove or comment-mark the unused exists_smooth_cutoff; (c) wire Iⱼ'_bounding into the k=n=0 decay case or soften the docstring claim that it's already used.
• Nice-to-have: add @[simp] ofNonnegDecay_apply (rfl); reconsider the ofNonnegDecay name; split at 0 rather than 1 in decay_transition_smul; reflow the a/Schwartz.lean:24-25 docstring.

Nice work on the hard part — the bridge is the right abstraction and it's solid.

---

Generated by Claude Code

[thefundamentaltheor3m]

Response to Round 1 review

Thanks for the careful, verified review. Addressed in 993a2f8. Point-by-point:

Should-fix

1. Private helpers — partially done, with a constraint. I made the four pointwise facts (transition_eq_zero/one, eventuallyEq_zero/self) private. The two substantive ones (contDiff_transition_smul, decay_transition_smul) cannot be private: ofNonnegDecay is @[expose]d (required so its *_apply* lemmas are provable and exported to a/b Schwartz downstream), and an exposed definition may not reference private declarations in its proof fields — I confirmed this against the compiler (Unknown identifier … A private declaration … would need to be public). Un-exposing ofNonnegDecay instead breaks the rfl/simp apply lemmas ("definitions that need to be unfolded … must be exposed"). So the minimal public surface is exactly these two lemmas — which are anyway the genuine content (the two Schwartz conditions for the cutoff product). I added a comment documenting this.

2. exists_smooth_cutoff "dead code" — keeping it, respectfully. It's a direct deliverable of the task ("First, prove that such an STF exists"), and the standalone statement of PR Existence of smooth cutoff function #316, so it documents that dependency relationship even though ofNonnegDecay uses the rescaled 1 - 2x/a form directly. I'd rather keep it as the explicit existence result than inline-only. Open to marking it @[deprecated]-style or moving it if you'd prefer it clearly flagged as reference-only.

3. Docstring overstates Iⱼ'_bounding wiring — fixed. Softened both a/b decay docstrings to "should follow from Iⱼ'_bounding (after integrating the bound)" rather than implying it's already invoked.

Nice-to-have

4. @[simp] ofNonnegDecay_apply — done. Added the rfl unfolding lemma and routed ofNonnegDecay_apply_of_nonneg/_of_le_half through it.

5. Name ofNonnegDecay — keeping it, reasoning below. Every SchwartzMap-constructor needs smoothness, so that isn't distinguishing; the unusual input here — the thing that makes this a non-trivial bridge rather than SchwartzMap.mk — is that decay is required only on [0,∞). That's the headline the name captures. Spelling out cutoff/half-line/smoothness would make it unwieldy without adding information. Happy to reconsider a concrete alternative if you have one.

6. Split decay at 0 not 1 — done. The compact case is now exactly the transition interval [a/2, 0]; dropped the arbitrary 1 and the bound is now |a| ^ k * C₁.

7. Docstring reflow — fixed.

Rebuilt clean (only the intended sorrys remain) and #print axioms unchanged. The one honest caveat you flagged — that this PR delivers the bridge, not the analytic 1-D inputs — is exactly the intended scope ("based on the Schwartzness of their one-dimensional counterparts"); the remaining sorrys are the corrected, now-true 1-D statements, left for follow-up.

---

Generated by Claude Code

[thefundamentaltheor3m]

🔍 Independent Review — Round 2

Overall. I reviewed the current HEAD (993a2f8) independently. The structural core — SchwartzMap.ofNonnegDecay as the bridge from "smooth on a right half-line + decay on [0,∞)" to a genuine Schwartz function — is the right abstraction, cleanly built, and I independently confirm it compiles with no sorry and only standard axioms (#print axioms ofNonnegDecay/ofNonnegDecay_apply_of_nonneg/exists_smooth_cutoff → [propext, Classical.choice, Quot.sound]). I also independently checked the mathematics of the restated 1-D statements and they are true (details below). Round 1 was comprehensive and the follow-up commit addressed most of it; I found little new, and nothing blocking.

Verification I ran. lake build SpherePacking.ForMathlib.RadialSchwartz.SmoothCutoff → clean (2753 jobs). Axioms as above. Line lengths: max 100 codepoints across all three files (no violations). I₁'_bounding (IntegralEstimates/I1.lean:212) and I₆'_bounding (I6.lean:116) exist and are fully proven.

---

1. Faithfulness to the ask

✅ The restated 1-D statements are mathematically TRUE — I checked each independently.

• I₆'_smoothOn : ContDiffOn ℝ ∞ I₆' (Ioi (-2)) (a/Schwartz.lean:88): integrand of size e^{-(2+x)πt} converges iff x > -2. ✓
• J₆'_smoothOn : ContDiffOn ℝ ∞ J₆' (Ioi (-1)) (b/Schwartz.lean:77): integrand e^{-(1+x)πt} converges iff x > -1. ✓
• The a = -2 vs a = -1 asymmetry is forced, not arbitrary. ofNonnegDecay requires the transition to vanish inside the smoothness domain Ioi a (the smoothness split in contDiff_transition_smul at x = a relies on x ≤ a ⟹ x < a/2). Since I₆'/J₆' are smooth only on (-2,∞)/(-1,∞), the thresholds must differ. This is correct and the module docstrings explain it well.
• The ∀ x ≥ 0 decay restriction is likewise necessary (the Iⱼ'/Jⱼ' grow like e^{-πxt} as x → -∞). ✓

This is the crux and it's right: the pre-PR obligations were false (smoothness/decay on all of ℝ); the new ones are true, and the cutoff repairs Schwartzness.

🟡 should-fix (defensible scope) — the 23 analytic sorrys, and a refinement of the Round-1 base-case suggestion. The PR delivers the bridge and reduction, not the analytic inputs; given the title ("based on the Schwartzness of their one-dimensional counterparts") this is defensible scope. One independent correction to the Round-1 suggestion to "wire I₁'_bounding into the k=n=0 case": I read I₁'_bounding — it gives ‖I₁' r‖ ≤ ∫_{Ici 1} C₀·e^{-2πs}·e^{-πr/s}, and for r ≥ 0 the last factor is ≤ 1, so the k=n=0 bound does follow. But each Iⱼ'_decay_nonneg is ∀ k n, so discharging k=n=0 alone closes no lemma — it would leave an orphan partial proof inside a still-sorryd statement. So leaving each decay lemma whole-sorry is actually the correct granularity; I'd recommend a tracked follow-up issue for the ∀ k n decay (Leibniz + the IntegralEstimates bounds) rather than partial in-lemma wiring. The current docstrings ("should follow from Iⱼ'_bounding … after integrating the bound") are appropriately hedged now.

2. Idiomaticity & Mathlib quality

✅ ofNonnegDecay (SmoothCutoff.lean:135) is well-designed and near-mathlibable. Stated over a general target E : NormedAddCommGroup/NormedSpace ℝ (correct — iterated derivatives + decay make sense for any target) with the source fixed to ℝ (correct — the half-line is ℝ-specific). Mathlib has no constructor for "Schwartz from half-line smoothness + one-sided decay", so this is a genuine gap-filler; modulo the domain content the shape would be a reasonable mathlib addition (at most generalise/API-first: it currently ships with three _apply lemmas, which is the right minimal API). Naming is on-convention (_smoothOn, _decay_nonneg, _apply_of_nonneg, _coe).

✅ The public/private split is not just acceptable but minimal — I confirm the author's Round-1 resolution. Exposing ofNonnegDecay forces the declarations directly referenced in its proof fields (contDiff_transition_smul, decay_transition_smul, SmoothCutoff.lean:89,101) to be public, while the four pointwise facts they call can stay private. That is exactly the smallest public surface; nothing to change here. The explanatory comment at :60-67 documents it well.

🟢 nice-to-have — avoid ≥/> in the disjunction lemmas. rcases lt_or_ge a x (:93), rcases lt_or_ge x (a / 2) (:112), rcases le_or_gt x 0 (:119) produce a ≥ x / x > 0 branches; the orientation convention prefers lt_or_le / le_or_lt, which give the definitionally-equal x ≤ a / 0 < x forms and read more uniformly. Purely cosmetic.

3. Efficiency

✅ Both substantive proofs are near-minimal. contDiff_transition_smul uses fun_prop + contDiffAt_const.congr_of_eventuallyEq; decay_transition_smul is a clean three-region bound (vanish / compact-continuity / decay) and the max (|a|^k * C₁) C₂ constant is tight after the Round-1 split-at-0 fix. This is the "analysis boilerplate that doesn't golf further" category — no missed positivity/gcongr/fun_prop, no nested-have bloat. by norm_num for (-2 : ℝ) < 0 is correct (positivity can't prove < 0). Nothing to flag.

4. Clarity, conciseness, cleanliness, modularity

✅ Docstrings and modularity are a strength. The reusable bridge lives in ForMathlib/RadialSchwartz/SmoothCutoff.lean, the domain wiring in the MagicFunction files; module docstrings carry the (appropriate) strategy prose. The Iⱼ_coe : ⇑Iⱼ = RadialFunctions.Iⱼ / a_coe theorems are the cleanest possible statement of "Iⱼ/a is Schwartz", and I verified them against Basic.lean (RadialFunctions.Iⱼ x = Iⱼ'(‖x‖²), sq_nonneg _ supplies 0 ≤ ‖x‖²) — sound.

🟢 nice-to-have — exists_smooth_cutoff (SmoothCutoff.lean:46) remains unused. Keeping it is a faithful reading of the task ("first prove such an STF exists") and records #316's statement, so I agree with keeping it — but a one-line comment on the theorem itself stating it is reference-only and not used by ofNonnegDecay (the module docstring hints at this, the declaration does not) would prevent a future reader from hunting for its call site.

---

Done well

• Correctly diagnoses that the pre-PR 1-D sorrys were false statements and fixes them by restricting to Ioi a / [0,∞) plus a cutoff — the central value of the PR, and it is right.
• ofNonnegDecay: clean, general over E, sorry-free, standard axioms, minimal API (verified).
• The a-parameter is forced by the I₆'/J₆' smoothness domains and recovers the requested STF (smoothTransition (x+1)) at a = -2.
• Minimal-public-surface helper split; tight decay constant; excellent module docs and file placement.

Severity ranking

• Blocking: none — builds clean, axioms clean, the structural goal is met and the restated hypotheses are true.
• Should-fix: track the 23 (now-true) 1-D smoothness/decay sorrys in a follow-up issue; do not partially wire k=n=0 (it closes no ∀ k n lemma).
• Nice-to-have: lt_or_ge/le_or_gt → lt_or_le/le_or_lt; add an on-declaration "reference-only / unused" note to exists_smooth_cutoff.

Solid work — the bridge is the correct abstraction and the corrected 1-D statements are the right foundation for the follow-up.

---

Independent Round-2 review generated by Claude Code

---

Generated by Claude Code

[thefundamentaltheor3m]

Response to Round 2 review

Thanks — and I appreciate the independent confirmation that the restated 1-D statements are mathematically true and that the a = -2 / a = -1 threshold asymmetry is forced (the transition must vanish inside Ioi a). Addressed in c64f3b5.

Should-fix — track the 23 analytic sorrys in a follow-up issue. Agreed in spirit, and thanks for refining the Round-1 base-case point (you're right: since each Iⱼ'_decay_nonneg is ∀ k n, discharging k = n = 0 in isolation closes no lemma — whole-lemma sorry is the correct granularity, which is why I only softened the docstring rather than wiring in a partial proof). These sorrys are the same smoothness/decay facts that were already sorry before this PR — the PR restates them correctly (they were previously false as global statements) but deliberately doesn't discharge them, per the "based on the Schwartzness of the 1-D counterparts" scope. I've left them clearly documented at the top of each Smooth/Decay section. I haven't unilaterally opened a tracking issue since that's the maintainer's call on an existing repo — happy to open one (listing the 11 a-side + 12 b-side obligations and the blueprint refs) if you'd like.

Nice-to-have (b) — flag exists_smooth_cutoff as reference-only. Done: added an on-declaration note that it's a standalone existence result recording the #316 connection and is not used by ofNonnegDecay.

Nice-to-have (a) — lt_or_ge/le_or_gt → lt_or_le/le_or_lt. This one doesn't apply to the pinned mathlib (the v4.30.0 bump): lt_or_le/le_or_lt don't exist there, and I confirmed against the compiler that lt_or_ge/le_or_gt are already the clean-orientation lemmas in this version — lt_or_ge (a b) : a < b ∨ b ≤ a and le_or_gt (a b) : a ≤ b ∨ b < a, i.e. the RHS disjunct is ≤/<, not ≥/>. So no change needed (the suggested names are from a different mathlib snapshot). Kept as-is.

Rebuilt clean; axioms unchanged.

---

Generated by Claude Code

[thefundamentaltheor3m]

🔍 Independent Review — Round 3

Overall. I reviewed the current HEAD (c64f3b5) independently and rebuilt it clean (lake build SpherePacking.ForMathlib.RadialSchwartz.SmoothCutoff → 2753 jobs, only the intended sorrys). The structural core — SchwartzMap.ofNonnegDecay as the bridge from "smooth on Ioi a + decay on [0,∞)" to a genuine Schwartz function — is the right abstraction and is correct; I re-derived the decay_transition_smul three-region split and its bounds by hand and confirm they are exhaustive and valid (details below). Rounds 1–2 were thorough and the resolutions hold, so I focused on digging for things they missed. I found one concrete, previously-unflagged code-quality issue (@[simps!] generating unused re/im simp lemmas); beyond that, I confirm little remains.

---

1. Faithfulness to the ask ✅ (confirmed, nothing new)

The a = -2 / a = -1 threshold asymmetry is forced by the I₆'/J₆' smoothness domains (Ioi (-2)/Ioi (-1)), the [0,∞) decay restriction is necessary, and the restated 1-D obligations are true where the pre-PR global ones were false. I independently re-checked the two pointwise facts under a < 0: transition_eq_zero (SmoothCutoff.lean:73) via x ≤ a/2 ⟹ 2x/a ≥ 1 ⟹ 1 - 2x/a ≤ 0, and transition_eq_one (:77) via 0 ≤ x ⟹ 2x/a ≤ 0 ⟹ 1 ≤ 1 - 2x/a — both correct. The decay case split x < a/2 / a/2 ≤ x ≤ 0 / x > 0 (:116,123) is exhaustive, and the middle-region bound ‖x‖ ≤ |a| (:127-128) is valid (a = -|a| ≤ a/2 ≤ x ≤ 0 ≤ |a|). The 23 analytic sorrys are the corrected 1-D inputs the title scopes out — agreed with Rounds 1–2 that this is defensible.

2. Idiomaticity & Mathlib quality

🟠 should-fix (NEW) — @[simps!] on the four ℂ-valued Schwartz defs emits 8 unused, non-idiomatic simp lemmas that split into re/im. a'/a (a/Schwartz.lean:215,225) and b'/b (b/Schwartz.lean:204,214) carry @[simps!]. Because SchwartzMap has no custom apply simps projection (its projections are [toFun, smooth', decay'], verified via initialize_simps_projections?), @[simps!] with simpRhs := true descends through the target ℂ = {re, im} and generates, as global @[simp] lemmas:

a'_toFun_re, a'_toFun_im, a_toFun_re, a_toFun_im   (+ b analogues)

e.g. a_toFun_re : (a x).re = (I₁' (‖x‖^2)).re + (I₂' (‖x‖^2)).re + … + (I₆' (‖x‖^2)).re. I verified all 8 exist and are simp-tagged, and that nothing in the repo references any of them (grep for _toFun/toFun_re/toFun_im finds only an unrelated hit in JacobiTheta/Derivative.lean). They are pure simp-set noise: they expose the toFun field and split the magic functions into real/imaginary components, which is never wanted here — the real API is the hand-written a_coe/a'_apply_of_nonneg (and b analogues), which use explicit simp only [...] and don't touch these. On main this file sat behind #exit (dead), so this PR is what first makes these live declarations.

Concrete fix: delete the @[simps!] attribute from all four defs. There is no clean @[simps] replacement (SchwartzMap is not a constructor application, so @[simps] errors and demands !; @[simps apply] fails — no apply projection), and no apply-lemma is needed since a_coe/*_apply_of_nonneg already cover downstream use. Verification: I confirmed the 8 lemmas exist, are @[simp], and are unreferenced by name; I did not run a full downstream rebuild with the attribute removed, so please lake build after deleting (the risk is only an anonymous simp relying on a re/im split of a/b, which is very unlikely given none of the four importers reference these names).

✅ ofNonnegDecay remains well-designed — general over E, source fixed to ℝ, minimal API, sorry-free. The minimal public/private surface (Round 1) and its documenting comment (:62-71) are correct. Naming on-convention.

3. Efficiency ✅

Both substantive proofs are near-minimal (fun_prop + contDiffAt_const.congr_of_eventuallyEq; the compact/vanish/decay bound with tight max (|a|^k * C₁) C₂). by norm_num for (-2 : ℝ) < 0 is right. No missed positivity/gcongr. Nothing to flag. (I do not re-raise the lt_or_ge/le_or_gt point — confirmed against this toolchain that these are already the clean-orientation lemmas; the Round-2 rebuttal is correct.)

4. Clarity, cleanliness, modularity ✅

Module docstrings are accurate — I checked the transition spellings: a = -2 ⟹ smoothTransition (x+1) vanishing on (-∞,-1], a = -1 ⟹ smoothTransition (2x+1) vanishing on (-∞,-1/2] — both match 1 - 2x/a. File placement (bridge in ForMathlib, wiring in MagicFunction) is good. The Iⱼ_coe/a_coe theorems are the cleanest statement of "is Schwartz" and check out against Basic.lean (RadialFunctions.Iⱼ x = Iⱼ' (‖x‖^2), sq_nonneg supplies 0 ≤ ‖x‖^2).

🟢 nice-to-have — ofNonnegDecay_apply_of_le_half (SmoothCutoff.lean:158) is exported but unused (Round 1 noted it). Defensible as symmetric API for a reusable file; no action needed unless you're trimming.

---

Done well

• The bridge is the correct abstraction, correct, sorry-free, standard axioms; the corrected 1-D statements are true where the pre-PR globals were false.
• a-parameter forced by the I₆'/J₆' domains; recovers the requested STF at a = -2.
• Tight proofs, minimal public surface, accurate docstrings, good modularity — Rounds 1–2 resolutions all hold.

Severity ranking

• Blocking: none — builds clean, axioms clean, structural goal met, restated hypotheses true.
• Should-fix: drop @[simps!] from a'/a/b'/b — it emits 8 unused, non-idiomatic re/im-splitting @[simp] lemmas (simp-set hygiene); confirm with a rebuild.
• Nice-to-have: ofNonnegDecay_apply_of_le_half is unused (keep as API or trim).

Genuinely solid PR; the one new item is cosmetic simp-hygiene, not correctness.

---

Independent Round-3 review generated by Claude Code

---

Generated by Claude Code

[thefundamentaltheor3m]

Response to Round 3 review

Nice catch — this is a real issue the first two rounds missed. Fixed in 20580b0.

Should-fix — @[simps!] generating 8 junk global @[simp] lemmas. Confirmed and removed all four @[simps!] attributes (a', a, b', b). You're right about the root cause: SchwartzMap has no apply simps-projection, so @[simps!]'s simpRhs descended into ℂ = {re, im} and produced a'_toFun_re, a_toFun_im, and the b analogues — unused and non-idiomatic. (These attributes pre-dated this PR; I'd carried them over unchanged in the rewrite, so thanks for scrutinizing them rather than assuming they were load-bearing.) The intended API is the hand-written a_coe/b_coe and *_apply_of_nonneg.

I did the downstream rebuild you flagged as untested: full lake build succeeds (3453 jobs) with the attributes gone — nothing referenced the generated lemmas by name or picked them up implicitly via simp. And I confirmed your finding that @[simps apply]/@[simps] aren't viable substitutes here (no apply projection), so plain removal is correct.

Nice-to-have — ofNonnegDecay_apply_of_le_half unused. Keeping it: it's the natural symmetric companion to ofNonnegDecay_apply_of_nonneg (the function's two defining regimes — 1 on [0,∞), 0 on (-∞, a/2]), so it rounds out the API and will be handy for anyone reasoning about the cutoff's left tail. Low cost, and it builds with standard axioms.

Thanks for digging past the earlier rounds rather than re-confirming them.

---

Generated by Claude Code

[thefundamentaltheor3m]

🔍 Independent Review — Round 4

Overall. I reviewed the current HEAD independently, with no assumptions carried over from the earlier rounds, and rebuilt the core clean (lake build SpherePacking.ForMathlib.RadialSchwartz.SmoothCutoff → 2753 jobs, only the intended sorrys in the a/b files). The SchwartzMap.ofNonnegDecay bridge is the right abstraction and is correct; I re-derived the three-region decay split and the two pointwise transition facts by hand and confirm they are exhaustive and valid. Rounds 1–3 were thorough and every resolution holds. I looked specifically for things all three missed and found nothing blocking or should-fix; only two very minor nice-to-haves, both optional. In short: the PR is essentially clean.

Independent re-verification (correctness)

• transition_eq_zero/transition_eq_one (SmoothCutoff.lean:73,77): under a < 0, x ≤ a/2 ⟹ 1 - 2x/a ≤ 0 and 0 ≤ x ⟹ 1 ≤ 1 - 2x/a. Both correct.
• contDiff_transition_smul split at x (:97): the a < x branch uses f smooth at x ∈ Ioi a; the x ≤ a branch has the product ≡ 0 near x (via x ≤ a < a/2). Points of (a, a/2] land in the first branch, where both factors are smooth — the boundary is handled cleanly, and Ioi a is exactly the minimal smoothness hypothesis (matching I₆'_smoothOn : … (Ioi (-2))).
• decay_transition_smul (:105): case split x < a/2 / a/2 ≤ x ≤ 0 / x > 0 is exhaustive; middle-region bound ‖x‖ ≤ |a| holds (a = -|a| ≤ a/2 ≤ x ≤ 0 ≤ |a|); constant max (|a|^k · C₁) C₂ is valid. ✓
• Module/section docstrings: I checked the transition spellings against 1 - 2x/a — a=-2 ⟹ smoothTransition (x+1) vanishing on (-∞,-1]; a=-1 ⟹ smoothTransition (2x+1) vanishing on (-∞,-1/2]. Both accurate.
• Iⱼ_coe/a_coe (and b): checked against Basic.lean — RadialFunctions.Iⱼ x = Iⱼ' (‖x‖^2), and funext fun _ ↦ …_apply_of_nonneg (sq_nonneg _) is sound because ⇑(schwartzMap_multidimensional_of_schwartzMap_real …) x reduces to Iⱼ' (‖x‖^2). Sound.

1. Faithfulness ✅

Confirmed, nothing new. The a = -2 / a = -1 asymmetry is forced by the I₆'/J₆' smoothness domains, the [0,∞) decay restriction is necessary, and the restated 1-D obligations are true where the pre-PR globals were false. The remaining analytic sorrys are the (corrected) 1-D inputs the title explicitly scopes out — defensible, as Rounds 1–3 agreed.

2. Idiomaticity & mathlib quality

🟢 nice-to-have (NEW) — exists_smooth_cutoff sits in the root namespace (SmoothCutoff.lean:50, before namespace SchwartzMap). For a ForMathlib file, a generic name like exists_smooth_cutoff in the root namespace is mild global-namespace pollution — mathlib would want it under a namespace. Since it's the reference-only #316 statement (correctly documented as such), a natural home would be Real.exists_smooth_cutoff (it is fundamentally a fact about Real.smoothTransition). Purely cosmetic; not worth a rebuild on its own.

🟢 nice-to-have (NEW) — the decay predicate is spelled out verbatim three times (decay_transition_smul :106, ofNonnegDecay :141, the variable block :148), and re-appears at all 12 Iⱼ'_decay_nonneg/Jⱼ'_decay_nonneg call sites. A named abbreviation (e.g. a def/abbrev HasDecayOn f (Ici 0) or similar) would DRY the ofNonnegDecay signature and make it read at a glance. This is a genuine trade-off (an extra predicate def has its own cost, and mathlib sometimes does repeat), so I flag it only as an optional readability note, not a request.

Otherwise ofNonnegDecay remains well-designed (general over E, source fixed to ℝ, minimal _apply API, sorry-free), the minimal public/private surface is correct and documented, and naming is on-convention (_smoothOn, _decay_nonneg, _apply_of_nonneg, _coe).

3. Efficiency ✅

Both substantive proofs are near-minimal (fun_prop + contDiffAt_const.congr_of_eventuallyEq; the vanish/compact/decay bound with tight max (|a|^k · C₁) C₂). by norm_num for (-2 : ℝ) < 0 is right (positivity can't prove < 0). No missed positivity/gcongr/fun_prop, no have-bloat. I do not re-raise the lt_or_ge/le_or_gt orientation point — confirmed against this toolchain that these are already the clean-orientation lemmas (the Round-2 rebuttal is correct).

4. Clarity, cleanliness, modularity ✅

Docstrings are accurate (checked above), file placement is good (bridge in ForMathlib, wiring in MagicFunction), and the @[simps!]-generated junk lemmas flagged in Round 3 are gone. The Iⱼ_coe/a_coe/b_coe theorems are the cleanest possible statement of "is Schwartz" and are currently unused downstream — that's fine, they are the intended public API for the follow-up.

Done well

• The bridge is the correct abstraction, correct, sorry-free, standard axioms; corrected 1-D statements are true where the pre-PR globals were false.
• a-parameter forced by the I₆'/J₆' domains; recovers the requested STF at a = -2.
• Tight proofs, minimal public surface, accurate docstrings, good modularity — all Rounds 1–3 resolutions hold, and I could not find a fourth-round correctness or hygiene defect.

Severity ranking

• Blocking: none — builds clean, structural goal met, restated hypotheses true, math re-verified by hand.
• Should-fix: none new. (Standing item, already agreed: track the analytic 1-D sorrys in a follow-up.)
• Nice-to-have: namespace exists_smooth_cutoff (e.g. Real.); optionally DRY the thrice-repeated decay predicate.

Genuinely clean PR. The remaining items are cosmetic; the core is solid.

---

Independent Round-4 review generated by Claude Code

---

Generated by Claude Code

[thefundamentaltheor3m]

Response to Round 4 review

Thanks for the independent hand-derivation of the transition facts, the case-splits, and the _coe reductions — good to have the correctness cross-checked from scratch. Both nice-to-haves are genuinely new; addressed in 307c9a3.

Nice-to-have 1 — exists_smooth_cutoff in root namespace. Agreed, fixed. Renamed to Real.exists_smooth_cutoff (it's a fact about real functions built from Real.smoothTransition, so that's its idiomatic home, and it removes the root-namespace pollution in a ForMathlib file). The declaration is unused, so the move is safe; updated the docstring reference. Rebuilt clean.

Nice-to-have 2 — DRY the ∀ k n, ∃ C, ∀ x ≥ 0, … decay predicate into a named def. I'm going to decline this one, deliberately — and I think it's a genuine trade-off rather than a clear win:

• The task's explicit brief was to write minimal new definitions and lean on existing infrastructure. Mathlib has no [0,∞)-restricted decay predicate, so a named HasNonnegDecay-style def would be net-new API introduced solely for surface sugar.
• The 12 call sites are the Iⱼ'_decay_nonneg/Jⱼ'_decay_nonneg statements — which are exactly the sorry obligations a future contributor will discharge. Keeping the quantifier structure spelled out in situ makes those obligations self-documenting at the point of proof, rather than hidden behind a def they'd have to go unfold.
• In ofNonnegDecay's signature, the inline form shows a caller precisely what they must supply without a jump-to-definition.

If the maintainers would prefer the abstraction (e.g. if this decay notion recurs elsewhere in the project), I'm happy to introduce SchwartzMap.HasNonnegDecay and thread it through — but absent that reuse, I'd rather honor the minimal-new-definitions directive.

Standing item unchanged: the analytic 1-D sorrys remain the intended follow-up scope; happy to open a tracking issue on request.

---

Generated by Claude Code

[thefundamentaltheor3m]

🔍 Independent Review — Round 5

Overall. I reviewed the current HEAD from scratch, with no assumptions carried from Rounds 1–4, and independently re-verified the mathematics and the mechanical claims. The SchwartzMap.ofNonnegDecay bridge is the right abstraction and is correct; I rebuilt the core clean and re-checked the axioms myself. The PR is essentially clean. I did find two new, verified items that all four prior rounds missed — both minor, one a straight style-rule violation for a ForMathlib file. Nothing blocking.

Verification I ran (this round, from scratch).

• lake build SpherePacking.ForMathlib.RadialSchwartz.SmoothCutoff → clean, 2753 jobs.
• #print axioms SchwartzMap.ofNonnegDecay → [propext, Classical.choice, Quot.sound] (no sorryAx); ofNonnegDecay_apply_of_nonneg likewise. MagicFunction.FourierEigenfunctions.a_coe → additionally sorryAx, i.e. it correctly inherits the analytic sorrys and nothing more. So the "no sorry / standard axioms for SmoothCutoff.lean" claim holds, and no sorry leaks into a declaration that shouldn't carry one.
• Line widths: 0 violations at 100 codepoints across all three files (measured in codepoints, not bytes).
• Re-derived by hand: transition_eq_zero/transition_eq_one (a<0, x≤a/2 ⟹ 1-2x/a≤0; 0≤x ⟹ 1≤1-2x/a) ✓; the contDiff split at x=a (points of (a,a/2] fall in the a<x branch where both factors are genuinely smooth; x≤a<a/2 gives the vanishing branch) ✓; the decay 3-region split x<a/2 / a/2≤x≤0 / x>0 is exhaustive with valid bound ‖x‖≤|a| on the middle (a=-|a|≤a/2≤x≤0≤|a|) ✓. The a=-2/a=-1 asymmetry is forced by the I₆'/J₆' smoothness domains, as Rounds 2–4 established. Iⱼ_coe/a_coe reductions check out against Basic.lean.

---

2. Idiomaticity & Mathlib quality

🟠 should-fix (NEW) — ≥ in statements violates the "never ≥" orientation rule. Two spots in the ForMathlib file:

• Real.exists_smooth_cutoff (SmoothCutoff.lean:51): … ∧ ∀ x : ℝ, x ≥ 0 → f x = 1.
• The decay predicate ∀ x ≥ (0 : ℝ), …, spelled in decay_transition_smul (:106), ofNonnegDecay (:141), the variable block (:148), and mirrored at all 12 Iⱼ'/Jⱼ'_decay_nonneg statements in a/b/Schwartz.lean`.

Mathlib's orientation convention (and this repo's own /cleanup audit item 19) is "Use ≤, never ≥; use <, never >" in statements, because simp/gcongr lemmas match on _ ≤ _ and won't fire on _ ≥ _. Note this is distinct from the Round-2 lt_or_ge/le_or_gt point (those are unavoidable lemma names in this toolchain; keeping them is right). The clean-cut fix is exists_smooth_cutoff's hypothesis:

theorem Real.exists_smooth_cutoff :
    ∃ f : ℝ → ℝ, ContDiff ℝ ∞ f ∧ (∀ x : ℝ, x ≤ -1 → f x = 0) ∧ ∀ x : ℝ, 0 ≤ x → f x = 1 :=

(the proof fun _ hx ↦ smoothTransition.one_of_one_le (by linarith) is unaffected). For the decay predicate the strict reading wants ∀ x, 0 ≤ x → …; I acknowledge the bounded-binder ∀ x ≥ 0 is common in practice and mirrors the [0,∞) restriction deliberately, so I rank the predicate half nice-to-have and the bare-implication half of exists_smooth_cutoff should-fix. Either way, for a file explicitly staged for mathlib this is the kind of thing a reviewer flags.

🟢 nice-to-have (NEW) — Filter in open Real Set Filter (SmoothCutoff.lean:40) is unused. I verified this by compiling a scratch copy with the open reduced to open Real Set — it builds clean (2753 jobs). filter_upwards is a tactic (no open needed) and the Filter.EventuallyEq/Iio_mem_nhds/Ioi_mem_nhds references resolve via dot-notation or root/Topology-scoped names. Drop Filter from the open list.

Otherwise ofNonnegDecay remains well-designed (general over E, source fixed to ℝ, minimal _apply API, sorry-free), the minimal public/private split is correct and documented, and the Round-3 @[simps!] junk is gone.

1. Faithfulness ✅

Confirmed independently, nothing new. The restated 1-D obligations are true where the pre-PR globals were false; the 23 analytic sorrys are the corrected 1-D inputs the title scopes out ("based on the Schwartzness of their one-dimensional counterparts") — a legitimate reading, not a hidden gap. ofNonnegDecay's construction is correct as re-derived above.

3. Efficiency ✅

Both substantive proofs are near-minimal (fun_prop + contDiffAt_const.congr_of_eventuallyEq; the vanish/compact/decay bound with tight max (|a|^k · C₁) C₂). by norm_num for (-2 : ℝ) < 0 is right. No missed positivity/gcongr/fun_prop, no have-bloat.

4. Clarity, cleanliness, modularity ✅

Docstrings accurate (I re-checked the a=-2 ⟹ x+1 / a=-1 ⟹ 2x+1 transition spellings and the vanishing intervals). Bridge in ForMathlib, wiring in MagicFunction — good separation. The Iⱼ_coe/a_coe/b_coe theorems are the cleanest statement of "is Schwartz".

---

Done well

• The bridge is the correct abstraction, correct, sorry-free, standard axioms — independently re-confirmed this round by hand-derivation and #print axioms, not by trusting prior rounds.
• The a-parameter is forced by the I₆'/J₆' smoothness domains and recovers the requested STF at a = -2.
• Every Round 1–4 resolution still holds at HEAD.

Severity ranking

• Blocking: none — builds clean, axioms clean, structural goal met, math re-verified by hand.
• Should-fix: rewrite x ≥ 0 → f x = 1 as 0 ≤ x → f x = 1 in Real.exists_smooth_cutoff (orientation rule; ForMathlib-bound). (Standing item unchanged: the analytic 1-D sorrys are the intended follow-up.)
• Nice-to-have: drop the unused Filter open (:40, verified); optionally re-orient the ∀ x ≥ 0 decay predicate to ∀ x, 0 ≤ x → ….

Genuinely clean PR; the two new items are cosmetic/style, not correctness.

---

Independent Round-5 review generated by Claude Code

---

Generated by Claude Code

[thefundamentaltheor3m]

Response to Round 5 review

Thanks for reviewing from scratch and re-deriving the transition facts, case-splits, and _coe reductions independently rather than trusting the record. Both new items were valid; fixed in ea71f79.

Should-fix — ≥ violates the project's inequality-orientation convention. Fixed, and I went further than the single flagged case for consistency: re-oriented all ≥ in statements to ≤.

• Real.exists_smooth_cutoff: x ≥ 0 → f x = 1 → 0 ≤ x → f x = 1.
• The ∀ x ≥ (0 : ℝ), … decay predicate (in ofNonnegDecay, decay_transition_smul, and all 12 Iⱼ'/Jⱼ' decay lemmas) → ∀ x, (0 : ℝ) ≤ x → ….
  These are all defeq rewrites, so no proofs changed. Good call flagging this as distinct from the Round-2 lt_or_ge point — that one was unavoidable lemma names, whereas these are our own statements, which the orientation gate does govern.

Nice-to-have — unused Filter in the open list. Removed (open Real Set Filter → open Real Set); confirmed the file still builds, matching your scratch-copy check. (𝓝 comes from open scoped Topology, and the EventuallyEq/eq_of_nhds uses are all dot-notation, so nothing needed the namespace.)

All three files rebuild clean (only the intended analytic sorrys remain). That leaves the standing scope item — the 23 corrected-but-deferred 1-D smoothness/decay obligations — as the only outstanding work, which is the intended follow-up.

---

Generated by Claude Code

[thefundamentaltheor3m]

To be superseded by #444 (see docstring).