The Derivative of a Constructible Function is Constructible
Pith reviewed 2026-05-19 00:48 UTC · model grok-4.3
The pith
The derivative of a constructible function is itself constructible.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The central claim is that the class of constructible functions on globally subanalytic sets is stable under differentiation: if a function can be expressed as a finite sum of finite products of globally subanalytic functions and logarithms of positive globally subanalytic functions, then its ordinary derivative is again expressible in exactly the same form.
What carries the argument
The finite-sum-of-finite-products form of constructible functions, built from globally subanalytic functions and logarithms of positive globally subanalytic functions, which is preserved by the product rule, chain rule, and the fact that derivatives of subanalytic functions remain subanalytic.
If this is right
- If f is constructible then its derivative f' is constructible.
- Any finite number of successive derivatives of a constructible function remains constructible.
- Differentiation can be freely inserted into expressions involving parametric integration of constructible functions without leaving the class.
- The set of constructible functions is closed under the operations of addition, multiplication, and differentiation.
Where Pith is reading between the lines
- The same closure argument might extend to partial derivatives or to functions of several variables on subanalytic sets.
- One could check whether the class remains closed when logarithms are replaced by other elementary functions whose derivatives stay subanalytic.
- The result supplies a concrete differential ring inside the larger o-minimal structure generated by globally subanalytic sets.
Load-bearing premise
The definition of constructible functions as finite sums and products of globally subanalytic functions and their logarithms must capture all the functions whose derivatives can be rewritten in the same form.
What would settle it
An explicit globally subanalytic function f together with a logarithm term whose derivative cannot be rewritten as any finite sum of finite products of globally subanalytic functions and logarithms of positive globally subanalytic functions.
read the original abstract
The notion of constructible functions in the setting of tame real geometry has been introduced by Cluckers and Dan Miller in their work on parametric integration of globally subanalytic functions. A function on a globally subanalytic set is called constructible if it is a finite sum of finite products of globally subanalytic functions and the logarithm of positive globally subanalytic functions. We show that the class of constructible functions is stable under taking derivatives.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proves that the class of constructible functions on globally subanalytic sets—defined as finite sums of finite products of globally subanalytic functions and logarithms of positive globally subanalytic functions—is closed under differentiation. The argument applies the product, chain, and quotient rules to the given finite-sum-of-products form, with the base case that derivatives of globally subanalytic functions remain globally subanalytic (on the open set where they exist) taken from the literature on tame geometry.
Significance. If the result holds, the stability under differentiation supplies a basic closure property that complements the parametric integration results of Cluckers and Miller. It is a modest but useful addition to the toolkit for constructible functions in o-minimal and subanalytic geometry, with no free parameters or ad-hoc axioms introduced.
major comments (1)
- [§2] The central argument rests on the fact that the derivative of a globally subanalytic function remains globally subanalytic. This is invoked without an internal proof or a precise citation to a theorem that covers the precise domain and singularities; a short reference or one-paragraph recall in §2 would make the base case fully self-contained.
minor comments (1)
- [Abstract] The abstract and introduction should explicitly note that the derivative is taken only on the open set where it exists and is continuous, to avoid any ambiguity about the domain of the resulting constructible function.
Simulated Author's Rebuttal
We thank the referee for their careful reading of the manuscript, their positive evaluation of its significance, and their recommendation for minor revision. We address the major comment below.
read point-by-point responses
-
Referee: [§2] The central argument rests on the fact that the derivative of a globally subanalytic function remains globally subanalytic. This is invoked without an internal proof or a precise citation to a theorem that covers the precise domain and singularities; a short reference or one-paragraph recall in §2 would make the base case fully self-contained.
Authors: We agree that the manuscript would benefit from greater self-containment on this point. The fact that the derivative of a globally subanalytic function remains globally subanalytic (on the open set where the derivative exists) is a standard result in the theory of subanalytic sets and o-minimal structures. In the revised version we will insert a short paragraph in §2 that recalls this fact, specifies the relevant open domain, and supplies a precise citation to the appropriate theorem in the literature on tame geometry. revision: yes
Circularity Check
No significant circularity; direct stability proof using external facts on subanalytic sets
full rationale
The paper defines constructible functions as finite sums of products involving globally subanalytic functions and logarithms of positive globally subanalytic functions. It proves closure under differentiation by applying the product rule, chain rule, and quotient rule to this explicit form, with the base case that the derivative of a globally subanalytic function remains globally subanalytic (where defined) taken from the established literature on tame geometry rather than proved or assumed internally. No equation or step reduces the target result to a redefinition of the input class, a fitted parameter renamed as a prediction, or a self-citation chain. The argument is a self-contained deductive proof relying on independent, externally verifiable properties of subanalytic sets.
Axiom & Free-Parameter Ledger
axioms (1)
- domain assumption Properties of globally subanalytic sets as developed in prior tame geometry literature
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.