WHEN CAN ONE OBTAIN CERTIFICATES OF OPTIMALITY USING POSITIVSTELLENSÄTZE?
arXiv:2609.08736v1 [cs.AI] 8 Sep 2026
NAYOON KIM, ALLEN GEHRET, SHENYUAN MA, AND JAKUB MAREČEK Abstract. We study certificates of positivity and optimality for learning problems whose objectives and constraints need not be polynomial. We isolate an axiomatic core of Fischer’s constructive strict and weak Positivstellensätze and prove the resulting theorems for abstract function algebras over ordered fields. The framework separates two roles that can otherwise be conflated: objective and constraint functions may be built from broad classes of continuous or definable operations, while the auxiliary primitives used to construct a certificate satisfy explicit scalar and closure axioms. We give instances over continuous and definable function algebras, including ordered fields not closed under square roots, derive lower-bound and global-optimality certificates, and analyze both expanded term length and shared computation-graph complexity.
1. Introduction There is substantial interest in guarantees of optimality for neural-network training. Two difficulties arise from activation functions: sigmoid is smooth but non-semialgebraic, whereas ReLU is semialgebraic but nonsmooth. Many available certificates rely on semialgebraicity or smoothness. Several approaches to such certificates have been developed, including branch-and-bound proof systems [15], cutting-plane proof systems [7, 36], Positivstellensätze, and several others [3, 22, 24, 25, 31] based on convexifications. Branch-and-bound and polyhedral proof systems are also used in ReLU-network verification [15]. Independently, strong lower bounds are known for branching and cutting-plane proof systems on difficult instance classes [8, 13]. A concise representation of a certificate family does not by itself make semantic verification tractable. Positivstellensätze have been developed in real algebraic geometry [29]. Related semialgebraic methods have been used to estimate Lipschitz constants of ReLU networks [5] and to represent and certify Monotone Deep Equilibrium models [6]. The challenge is the computational complexity of obtaining such certificates, which remains prohibitive for many practical applications, even when sparsity [33–35] and nonnegativity [21] are exploited. Here we focus on the Positivstellensatz approach. More precisely, we ask which Sätze can provide explicit algebraic certificates for deep-learning problems, and how such certificates can be constructed. Many classical Sätze contain a nonconstructive step and therefore do not immediately yield an effective construction. An exception to this is the Positivstellensätze for differentiable functions by Fischer (2011) [12], a constructive generalization of the earlier Positivstellensatz for definable functions on o-minimal structures by Acquistapace, Andradas, and Broglia (2002) [1]. Fischer’s construction, inspired in part by [1], has an explicit structure that permits the present axiomatic formulation. Two features of Fischer’s formulation [12] make systematic reuse of the construction less direct: (1) The main theorems and proofs are presented in the setting of (definable families of) definable C r -functions on a definably complete real closed field. Fischer also gives Banach-space and Peano-differentiable variants, explaining that minor variations of the definable proofs yield Date: September 9, 2026.
1
these results and indicating the required substitutions rather than writing out separate full proofs. (2) The construction is too reliant on the fact that the scalar √ field is a real-closed field (such as R). This is mainly because the square-root function · plays a seemingly essential role. The first point, 1, suggests a single axiomatic framework containing these settings as special cases. √ The second, 2, asks how far the construction can be generalized by replacing functions such as “ ·”. 1.1. Contributions and organization. Sections 3 and 4 introduce the axiomatic setting and state the strict and weak Positivstellensätze (Theorems 4.1 and 4.4). Section 5 gives examples that satisfy the axiomatic Positivstellensatz but are not direct instances of the hypotheses in [12], including examples over fields without square roots, such as Q, and examples using variants of common neural-network activation functions. Section 6 gives optimality certificates and a neural-network application. Section 7 analyzes the complexity of Fischer’s construction. Appendix A gives the universal terms and proof architecture. Appendices B and C contain the proofs of the strict and weak theorems. Appendix D verifies the function-algebra criteria for various examples, including Fischer’s definable C r setting. Appendix E derives the exact term-length and shared-graph complexity bounds and discusses the small-arity cases. 2. Background Polynomials that can be written as a sum of squares (SOS) of polynomials are obviously nonnegative; however, the converse is false by Hilbert (1888). The next question is whether all the nonnegative polynomials are SOS of rational functions; this is Hilbert’s 17th problem (1900) which was answered in the affirmative by Artin (1927). This motivates the study of certificates of positivity. Let g, f1 , . . . , fk be polynomials in R[X] = R[X1 , . . . , Xn ]. The preordering T (f1 , . . . , fk ) generated by f1 , . . . , fk is the smallest collection of polynomials that contains all squares, each fi , and is closed under addition and multiplication. Any element of this set is tautologically nonnegative on the basic closed semialgebraic set \ {fi (x) ≥ 0} ⊆ Rn , F = 1≤i≤k
so it serves as an algebraic witness for nonnegativity. Classical polynomial Positivstellensätze certify positivity (or nonnegativity) of g on F by producing such a witness, or variants thereof. The Krivine–Stengle Positivstellensatz (1964, 1974) [18, 32] gives a certificate with a multiplier in the preordering: g ≥ 0 on F if and only if there exist µ ∈ N and a1 , a2 ∈ T (f1 , . . . , fk ) such that (g 2µ + a1 )g = a2 . Schmüdgen’s Positivstellensatz removes the multiplier under a compactness assumption on F (1991) [30]: if F is compact and g > 0 on F , then g belongs to the preordering: g ∈ T (f1 , . . . , fk ) Putinar then reduces the structure from a preordering (multiplicative cone) to a quadratic module (additive cone), provided the quadratic module is Archimedean (1993) [28]: if g > 0 on F , then: X g = σ0 + σi fi (σi SOS) 1≤i≤k
Beyond polynomial rings, Gamboa proved a Positivstellensatz for rings of continuous functions [14]. Later, Acquistapace–Andradas–Broglia proved strict and weak Positivstellensätze for definable C r -functions in o-minimal expansions of real closed fields [1]. Fischer subsequently gave an explicit finite construction, preserved definability uniformly in parameters, treated the smooth case, and gave Banach-space variants [12]. We formulate the construction using scalar and function-algebra 2
axioms. The resulting terms are independent of the particular function algebra and scalar field; only verification of the axioms depends on the instance. Other nonpolynomial positivity results use different certificate mechanisms. Dinh and Pham obtain sums-of-squares representations for nonnegative definable C p -functions under additional hypotheses on the zero set, with coefficients of class C p−2 [9]. Lasserre–Putinar study positivity and optimization in finitely generated algebras of Borel or semialgebraic functions by lifting to polynomial optimization [20], while Marshall–Netzer use hidden positivity and quadratic modules in real function algebras [23]. These frameworks are complementary to the present closure-axiom approach rather than direct substitutes for the universal constructions below. 3. Setup Throughout, our main running example is the collection C 0 (U, R) of continuous real-valued functions on an open set U ⊆ Rn . Here we have an underlying space X = U , a field of scalars R = R, and an algebra A = C 0 (U, R). To obtain further examples, we consider more general choices of space, scalars, and algebra: X is an arbitrary set, R is a model-theoretic structure (cf. [2, Appendix B]) satisfying some first-order axioms, and A is a collection of functions X → R satisfying some closure axioms. In Sections 3 and 4, X is arbitrary. We often consider a one-sorted first-order language L, an L-structure R = (R; . . .) of “scalars”, and a collection A of R-valued functions X → R. Thus A ⊆ RX , and A satisfies the closure properties specified below. The language L allows us to state and prove Theorems 4.1 and 4.4 independently of a particular function algebra. Interpretations of L-terms also define functions in RX uniformly: Definition 3.1. Suppose t(z1 , . . . , zn ) is an L-term, R = (R; . . .) is an L-structure, and f1 , . . . , fn : X → R are elements of RX ; then we define a new element t(f1 , . . . , fn ) of RX as follows: t(f1 , . . . , fn ) : X → R,
x 7→ t(f1 , . . . , fn )(x) := tR (f1 (x), . . . , fn (x))
where tR : Rn → R is the interpretation of the L-term t(z1 , . . . , zn ) in the L-structure R. We begin with the language LoF of ordered fields: LoF := {≤, 0, 1, −, +, ·, (·)−1 } Let ToF be the LoF -theory whose models are precisely the ordered fields R = (R; ≤, +, ·) where all function symbols have their usual interpretation; we declare 0 to be a default value by setting 0−1 := 0. Below, all languages we introduce will extend LoF , and all theories will extend ToF . Suppose R = (R; . . .) is a model of ToF . The first two axioms we wish to impose on a collection A ⊆ RX of functions X → R are the following: (A0) The collection A is a unital commutative ring of functions X → R, i.e., (A0a) the constant functions X → R, x 7→ 0, 1 are elements of A (A0b) if f ∈ A, then −f ∈ A (A0c) if f, g ∈ A, then f + g, f · g ∈ A (A1) if f ∈ A, and {f > 0} = X, then f −1 ∈ A. Under the axioms (A0) and (A1), the collection A has the natural structure of a Q-algebra, which partly motivates our use of the word algebra. We use the term more broadly below for function rings satisfying the stated closure axioms, and impose (A1) only where it is needed: it is included with the strict axioms (AsP), but not the weak axioms (AwP). 3
Main Example 3.2. Suppose R = (R; ≤, +, ·) is the usual ordered field of real numbers, construed as an LoF -structure in a natural way, thus making it a model of ToF . Likewise, let X = U ⊆ Rn be an open subset of Rn , for some n, and set A = C 0 (U, R) be the R-algebra of continuous R-valued functions U → R. Then A satisfies axioms (A0) and (A1). We prove all claims about this running Main Example in subsection D.3. Main Non-Example 3.3 (for (A1)). Let n ≥ 1, suppose R = (R; ≤, +, ·), and consider A = R[X] = R[X1 , . . . , Xn ], the ring of polynomials over R in the indeterminates X1 , . . . , Xn ; we construe A as a collection of functions Rn → R in the usual way. Then A satisfies axiom (A0) but does not satisfy axiom (A1). Indeed, we have f := 1 + X12 + · · · + Xn2 ∈ A and f > 0 on Rn , however f −1 ̸∈ A since f −1 is bounded on Rn but not constant. Consequently, A cannot satisfy the strict axioms (AsP) given below, so the Strict Positivstellensatz 4.1 does not apply to this choice of A. We show below in 4.7 that the Weak Positivstellensatz 4.4 also does not apply to this choice of A. Convention 3.4. If R satisfies ToF and f : X → R, then we set {f ≥ 0} := {x ∈ X : f (x) ≥ 0} ⊆ X. A similar notation is used likewise for {f > 0}, {f = 0}, {f ≤ 0}, and {f < 0}. 3.1. The languages. We equip the scalar fields with additional primitives. Their intended roles are specified in subsection 3.2; the corresponding language extensions of LoF add the following function symbols: • a unary function σ; it produces nonnegative values (for example, |x|, x2 , or x2d ) √ • a unary function ρ; it is a partial inverse of σ (for example, x) • a unary function ξ; it is a generalized “positive part” or activation-type function (for example, ReLU(x) := max(0, x) or exp(−1/t) · 1{t > 0}) √ • a unary function δ; it is strictly positive and dominates twice its input (for example, 2 1 + x2 or 2 ReLU(x) + 1) • a binary function ν; it is a partial proxy for the max function: it is positive whenever either input is positive, and is bounded by its second input whenever p the first input is nonpositive and the second input is positive (for example, max(x, y) or x2 + y 2 + x) We define extensions of LoF by these function symbols as follows: LwP := LoF ∪ {σ, ρ, ξ} ⊆ LsP := LwP ∪ {δ, ν} Main Example 3.5. To continue with example 3.2, we expand the LoF -structure R = (R; . . .) to an LsP -structure by interpreting the new function symbols in LsP \ LoF as follows for every x, y ∈ R: p σ(x) := x2 , ρ(x) := |x|, ξ(x) := ReLU2 (x), p p δ(x) := 2 1 + x2 , ν(x, y) := x2 + y 2 + x Figure 1 shows these functions: 3.2. The scalar theories. Let TwP be the LwP -theory extending ToF whose models R = (R; ξ, σ, ρ) satisfy for every a, b ∈ R: (Tξ1) ξ(a) ≥ 0 (Tξ2) ξ(a) > 0 iff a > 0 (Tσ1) σ(a) ≥ 0 (Tσ2) if a, b ≥ 0, then σ(a · b) = σ(a) · σ(b) (Tρ) if a ≥ 0, then ρ(a) ≥ 0 (Tσρ) if a ≥ 0, then σ(ρ(a)) = a Let TsP be the LsP -theory extending TwP whose models R = (R; ξ, σ, ρ, δ, ν) additionally satisfy for every a, b ∈ R: (Tδ) 0 < δ(a) and 2a ≤ δ(a) 4
Figure 1. The auxiliary functions σ, ρ, ξ, δ, ν in Main Example 3.5. (Tν1) if a > 0 or b > 0, then ν(a, b) > 0, and (Tν2) if a ≤ 0 and b > 0, then ν(a, b) ≤ b Main Example 3.6. The LsP -structure R = (R; . . .) from example 3.5 is a model of TwP and TsP . 4. Main results 4.1. Strict Positivstellensatz. For the Strict Positivstellensatz 4.1 below, we consider a model R of TsP as well as the following additional axioms on our algebra A ⊆ RX of functions X → R: (A2) if f ∈ A, then ξ(f ) ∈ A (A3s) if f ∈ A and {f > 0} = X, then σ(f ), ρ(f ) ∈ A (A4s) if f, g ∈ A and {f ≥ 0} ⊆ {g ̸= 0}, then: ξ(f ) · g −1 ∈ A (Aδ) if f ∈ A, then δ(f ) ∈ A (Aν) if f, g ∈ A and {f ≤ 0} ⊆ {g > 0}, then ν(f, g) ∈ A (AsP) the conjunction of axioms (A0), (A1), (A2), (A3s), (A4s), (Aδ), and (Aν). Strict Positivstellensatz 4.1. (cf. [12, Theorem 1.1]) For each k ≥ 0, there exist LsP -terms t̃i (z0 , . . . , zk ) for i = 0, . . . , k such that for every R satisfying TsP , every A ⊆ RX satisfying (AsP), and every g, f1 , . . . , fk ∈ A, if T 1≤i≤k {fi ≥ 0} ⊆ {g > 0}, then each ti := t̃i (g, f1 , . . . , fk ) lies in A, is strictly positive on X, and P g = σ(t0 ) + 1≤i≤k σ(ti )fi .
5
Proof strategy. The strict and weak constructions follow the same pattern. The constraints are first compressed into a single function h satisfying \ {fi ≥ 0} ⊆ {h ≥ 0} ⊆ {g > 0} 1≤i≤k
in the strict case, with the analogous nonnegative relation in the weak case. The sign analysis then involves only g and h. The ξ-terms distinguish the relevant sign cases for (g, h). The resulting functions, together with the representation of h in terms of the original constraints, give the certificate. The explicit terms are given in Appendix A; Appendices B and C contain the corresponding verifications. □ The statement of 4.1 provides the T LsP -terms t̃i independently of the particular R, A, g, f1 , . . . , fk ; it requires only TsP , (AsP), and 1≤i≤k {fi ≥ 0} ⊆ {g > 0}. Main Example 4.2. Continuing with example 3.6, the algebra A = C 0 (U, R) satisfies (AsP). Example 4.3. Appendix E.3 gives the k = 0 terms, the complete k = 1 strict and weak identities as formulae, and the expanded lengths for k = 2. 4.2. Weak Positivstellensatz. For the Weak Positivstellensatz 4.4 below, we consider a model R of TwP as well as the following additional axioms on our algebra A ⊆ RX of functions X → R: (A3w) if f ∈ A and {f ≥ 0} = X, then σ(f ), ρ(f ) · ξ(f ) ∈ A (A4w) if f ∈ A, then ξ(−f ) · (f )−1 ∈ A (A5w) if g, h ∈ A and {h ≥ 0} ⊆ {g ≥ 0}, then: ξ(g 2 ) · ξ(g + 4h) · (g + h)−1 ∈ A (AwP) the conjunction of (A0), (A2), (A3w), (A4w), and (A5w). In particular, the weak theorem does not require axiom (A1), i.e., closure under inverses of all everywhere-positive functions. Proposition C.12 below gives a non-Archimedean example satisfying (AwP) but not (A1), so axiom (A1) is not a consequence of the remaining weak axioms. Weak Positivstellensatz 4.4. (cf. [12, Theorem 1.2]) For each k ≥ 0, there exist LwP -terms t̃i (z0 , . . . , zk ) for i = −1, 0, . . . , k such that for every R satisfying TwP , every A ⊆ RX satisfying (AwP), and every g, f1 , . . . , fk ∈ A, if T F := 1≤i≤k {fi ≥ 0} ⊆ {g ≥ 0}, then we have: σ(p) · g = σ(t0 ) +
P
1≤i≤k σ(ti ) · fi
where each ti := t̃i (g, f1 , . . . , fk ) (i = 0, 1, . . . , k) is a nonnegative function in A; and p := t̃−1 (g, f1 , . . . , fk ) is a nonnegative function in A satisfying: {p = 0} = {g = 0} The proof of 4.4 is given in Appendix C. Main Example 4.5. Continuing with example 4.2, the algebra A = C 0 (U, R) also satisfies (AwP). Example 4.6. The zero-constraint sanity check and the complete one-constraint formulae are given in Appendices A.3 and E.3. Main Non-Example 4.7 (for (A2)). Continuing with 3.3, we claim that there is no choice of function ξ : R → R so that both the structure (R; ≤, +, ·, ξ) satisfies (Tξ1)-(Tξ2) and the algebra A = R[X1 , . . . , Xn ] (n ≥ 1) satisfies (A2); indeed, otherwise applying (A2) to f = X1 , there would be a polynomial P ∈ R[X1 , . . . , Xn ] such that P (x1 , . . . , xn ) = ξ(x1 ) for all (x1 , . . . , xn ) ∈ Rn . 6
Restricting this identity to tuples (t, 0, . . . , 0) ∈ Rn yields a univariate polynomial q(t) such that q(t) = ξ(t) for all t ∈ R, contradicting (Tξ1)-(Tξ2) as a univariate polynomial with infinitely many zeros must be identically zero. Consequently, A cannot satisfy the weak axioms (AwP) either, so the Weak Positivstellensatz 4.4 also does not apply to this choice of A. 5. Examples We give several Positivstellensätze that are instances of 4.1 and 4.4. Fischer’s original setting is discussed in Appendix D.5. 5.1. Using the binary step function as ξ. Outside the continuous setting, one may use for ξ the binary step function (with ξ(0) = 0): ( 0, x ≤ 0, R → R, x 7−→ 1, x > 0. Choose any scalar primitives σ, ρ, ξ, δ, ν on an ordered field R that satisfy the scalar theories TwP and TsP . Expand the scalar structure by those chosen primitives, let X be a definable set, and take A to be the algebra of all functions X → R definable in that expanded structure. Closure of definability under composition then supplies every algebra axiom used by the two Positivstellensätze. Corollary 5.1. For any such choice of scalar primitives, the corresponding full definable-function algebra A satisfies axioms (AsP) and (AwP). Thus the framework permits arbitrary, including discontinuous, primitive choices subject to the scalar axioms; the price of this formal freedom is that one works in the full definable-function algebra. Appendix D.1 gives the precise setup and two limiting variants. 5.2. Alternative choices of σ, ρ, ξ, δ, ν in the main example (activation functions). We consider alternative choices of σ, ρ, ξ, δ, ν in Main Example 3.5. The following proposition gives sufficient conditions: Proposition 5.2. If the real ordered field R is expanded to a model of TsP such that: (1) ξ : R → R is continuous, (2) the restrictions of σ and ρ to (0, +∞) are continuous, (3) δ : R → R is continuous, and (4) ν : Dν → R is continuous, where Dν := {(a, b) ∈ R2 : if a ≤ 0, then b > 0}, then the algebra A = C 0 (U, R) satisfies (AsP). If instead R is expanded to a model of TwP such that: (5) ξ : R → R is continuous and ξ(t) ≺ t at 0+ , i.e., limt↓0 ξ(t)/t = 0, (6) σ : [0, +∞) → R is continuous, and (7) t 7→ ξ(t)ρ(t) : [0, +∞) → R is continuous, then the algebra A = C 0 (U, R) satisfies (AwP). Proof. See subsection D.2, in particular Corollaries D.6 and D.11, for more general statements and their proofs. □ Examples of functions σ, ρ, ξ, δ, ν satisfying the scalar axioms and the conditions of Proposition 5.2 are easy to construct. We consider a few choices of ξ: • (Power gates) For any α ∈ (0, +∞), the function ξ = ReLUα satisfies 5.2(1); if moreover α > 1, then ξ additionally satisfies 5.2(5); if instead α ∈ (0, 1], then condition 5.2(5) fails.
7
• Let F : R → R be continuous, differentiable at 0, and strictly increasing on [0, +∞). Define ξF as follows. It satisfies (Tξ1), (Tξ2), and the conditions in 5.2(1,5). ( (F (t) − F (0))2 if t > 0 ξF : R → R, t 7→ ξF (t) := 0 if t ≤ 0 Applying this construction to the common activation functions GELU, sigmoid, and softplus (cf. [19]) gives, for t > 0, ξ1 (t) := GELU2 (t) ξ2 (t) := (sigmoid(t) − 1/2)2 ξ3 (t) := (softplus(t) − log 2)2
Figure 2. Alternative choices of ξ based on common activation functions 5.3. Q-valued continuous functions. In [12], the implicit model R of ToF is always a real closed field in terms of √ (cf. D.5). This is primarily because the implicit ρ, δ, ν functions there are defined ·, a function which an arbitrary ordered field might not support. We give a C 0 example over an ordered field that need not be real closed, and state it for R = Q. This is an exact rational-arithmetic model, or an algebraic idealization of exact computation. It does not model ordinary floating-point or fixed-point arithmetic, where rounding, overflow, exceptional values, and inexact inversion require an error-aware semantics. Consider the ordered field (Q; ≤, +, ·) as a model Q = (Q; . . .) of ToF in the natural way. Expand Q to an LsP -structure by interpreting the new function symbols as follows for every x, y ∈ Q: σ(x) := ReLU(x),
ρ(x) := ReLU(x),
ξ(x) := ReLU2 (x)
δ(x) := 2 ReLU(x) + 1, ν(x, y) := max(x, y) Next, equip Q with the order topology, and let X be an arbitrary topological space. Let A = C 0 (X, Q) be the collection of all continuous functions X → Q. We have the following (see subsection D.4): Corollary 5.3. Q satisfies TsP and A satisfies axioms (AsP) and (AwP). 6. Optimality certificates and an application to neural networks The Positivstellensätze give the following optimization-theoretic reformulation: Corollary 6.1 (Lower-bound and optimality certificates). Let g, f1 , . . . , fk ∈ A and fix L ∈ R. Set \ F := {fi ≥ 0}. 1≤i≤k
Assume additionally that every constant function X → R belongs to A. 8
(Strict case) Suppose R satisfies TsP and A satisfies (AsP). Then the following are equivalent: (S1) There exists η > 0 such that: F ⊆ {g − (L + η) > 0} (S2) There exists η > 0 and strictly positive functions t0 , . . . , tk ∈ A, such that P g − (L + η) = σ(t0 ) + 1≤i≤k σ(ti )fi For every η witnessing (S1), the functions in (S2) may be chosen uniformly by applying the Strict Positivstellensatz 4.1 to the functions g − (L + η), f1 , . . . , fk ∈ A. (Weak case) Suppose R satisfies TwP and A satisfies (AwP). Then the following are equivalent: (W1) We have: F ⊆ {g − L ≥ 0} (W2) There exist nonnegative functions p, t0 , . . . , tk ∈ A such that P σ(p) · (g − L) = σ(t0 ) + 1≤i≤k σ(ti )fi and {p = 0} = {g − L = 0} Under (W1), the functions (W2) may be chosen uniformly by applying the Weak Positivstellensatz 4.4 to the functions g − L, f1 , . . . , fk ∈ A. If F = ̸ ∅ and g ⋆ := inf x∈F g(x) exists as an element of R, then (S1) is equivalent to L < g ⋆ , while (W1) is equivalent to L ≤ g ⋆ . In particular, for every x⋆ ∈ F , the point x⋆ is a global minimizer of g on F if and only if (W2) holds with L = g(x⋆ ). To illustrate the corollary, consider the problem of empirical risk minimization subject to pairwise output-consistency constraints motivated by individual fairness [11, 16, 17]. Let Nθ : Rp → Rm be a neural network with fixed architecture and trainable parameters θ ∈ Rn . Let {(zj , yj )}4j=1 be four labeled samples, where (z1 , z2 ) and (z3 , z4 ) are designated matched pairs, for example pairs that differ only in a protected attribute. Given a continuous training loss ℓ : Rm × Rm → R≥0 , a continuous output discrepancy d : Rm × Rm → R≥0 , and a user-specified tolerance ε > 0, define the functions: 4 1X g(θ) := ℓ(Nθ (zj ), yj ), fi (θ) := ε − d(Nθ (z2i−1 ), Nθ (z2i )), i = 1, 2 4 j=1
and the feasible region: F := {f1 ≥ 0} ∩ {f2 ≥ 0} Thus the training problem is inf θ∈F g(θ). Suppose the network is built from continuous operations and activations, such as ReLU, GeLU, or Mish. Then g, f1 , f2 belong to the ambient algebra A = C 0 (Rn , R) of the Main Example. Consequently, for any feasible parameter vector θ⋆ ∈ F , Corollary 6.1 implies that θ⋆ is a global minimizer if and only if there exist nonnegative functions p, t0 , t1 , t2 ∈ A such that: p2 · (g − g(θ⋆ )) = t20 + t21 f1 + t22 f2
and {p = 0} = {g = g(θ⋆ )}
The witnesses may be chosen by substituting g − g(θ⋆ ), f1 , f2 into the universal terms t̃i supplied by the Weak Positivstellensatz 4.4. Here A is an ambient function algebra, not the class of functions represented by the fixed network. The auxiliary primitives σ, ρ, ξ, δ, ν used to construct the certificates need not be the activation functions used by Nθ . Likewise, if L < inf θ∈F g(θ), then for some η > 0 there exist strictly positive t0 , t1 , t2 ∈ A such that: g − (L + η) = t20 + t21 f1 + t22 f2 Alternative admissible certificate primitives may be chosen using Proposition 5.2, independently of the activation functions used in Nθ ; for definable discontinuous networks, one may instead work in the corresponding definable-function algebra of subsection 5.1. 9
6.1. A rational-valued optimality certificate. We instantiate Corollary 6.1 over the non-realclosed ordered field Q. Let 1 ∈Z⊆Q Q(x) := x + 2 and consider inf Q(x) subject to f (x) := x − 1 ≥ 0. x∈Q
The feasible point x⋆
= 1 has value Q(x⋆ ) = 1. Choose the weak certificate primitives from
subsection 5.3, σ(a) = ρ(a) = ReLUQ (a), ξ(a) = ReLUQ (a)2 , and let A be the algebra of all functions Q → Q definable in (Q; <, +, ·, Q). The functions Q and f belong to A, and Q(x) ≥ 1 whenever f (x) ≥ 0. The k = 1 weak construction yields nonnegative p, t0 , t1 ∈ A with p(x)(Q(x) − 1) = t0 (x) + t1 (x)(x − 1),
{p = 0} = {Q − 1 = 0}.
After simplifying the resulting expressions, one obtains 28 42 3 16 , x < 1 , (1 − Q(x)) (1 − x) 1 − Q(x) + (1 − x) 2 1 p(x) = 0, ≤ x < 32 , 2 (Q(x) − 1)72 , x ≥ 23 , 28 45 3 16 , x < 1 , (1 − Q(x)) (1 − x) 1 − Q(x) + (1 − x) 2 1 t0 (x) = 0, ≤ x < 32 , 2 (Q(x) − 1)73 , x ≥ 32 , and ( 17 (1 − Q(x))28 (1 − x)41 1 − Q(x) + (1 − x)3 , x < 12 , t1 (x) = 0, x ≥ 21 . The identity is checked separately on the three displayed regions, and {p = 0} = [ 12 , 32 ) ∩ Q = {Q − 1 = 0}. Hence Q(x) ≥ 1 for every feasible x, while x⋆ = 1 attains this value. Thus x⋆ is a global minimizer. 7. Complexity analysis We measure the expanded length of the universal terms. Following [2, Appendix B], we construe L-terms as admissible words over an alphabet consisting of the function symbols of L, together with an infinite collection of variables z0 , z1 , z2 , . . .. In particular, an L-term t is a string of symbols from this alphabet and thus has a well-defined length lh(t) ∈ N≥1 . The following gives the lengths of the terms provided by Fischer’s construction (see E.1): Proposition 7.1. Suppose k ≥ 1. The length of the term appearing on the right-hand side of 4.1 is: P lh(σ(t̃0 (z0 , . . . , zk )) + 1≤i≤k σ(t̃i (z0 , . . . , zk )) · zi ) = 72k 3 + 232k 2 + 224k + 51 = Θ(k 3 ) The lengths of the terms appearing on the left- and right-hand side of 4.4 are: lh(σ(t̃−1 (z0 , . . . , zk )) · z0 ) = 532k + 467 = Θ(k) lh(σ(t̃0 (z0 , . . . , zk )) +
P
1≤i≤k σ(t̃i (z0 , . . . , zk )) · zi )
= 707k 2 + 1370k + 649 = Θ(k 2 )
Appendix E.3 includes the complete one-constraint identities with every shared subterm inlined. The formulae were produced by maintained symbolic code implementing the recursive constructions rather than transcribed by hand, and are intended to show the resulting expression trees. 10
7.1. Shared straight-line computation graphs. Expanded term length counts every repeated occurrence of an identical subterm. For the complexity analysis, we use the shared straight-line directed-acyclic-graph model defined precisely in Appendix E.2: all certificate outputs are computed jointly, syntactically identical subexpressions share one node, fan-out is free, each scalar primitive (including inversion) has unit cost, and finite sums and numerals are formed by balanced binary addition trees. This is the standard term-graph model [27]. Proposition 7.2 (Shared-graph complexity). For either the strict or weak construction with k constraints, the universal certificate has a shared straight-line computation graph of size O(k) and depth O(log(k + 1)), treating z0 , . . . , zk as inputs and each scalar primitive as a unit-cost operation. If the inputs are themselves represented jointly by graphs of total size S and maximum depth D, the composed certificate graph has size S + O(k) and depth D + O(log(k + 1)). Proof. See Appendix E.2, where the cost model and the sharing convention are fixed before the strict and weak constructions are counted. □ These bounds concern evaluation of the explicit universal terms under the specified sharing model. Expanded term length counts every repeated occurrence of a shared subterm, whereas Proposition 7.2 counts each shared subexpression once. Thus the graph bound concerns evaluation of the given terms; it says nothing about finding smaller equivalent terms or deciding equality of arbitrary terms. These bounds concern evaluation of the fixed universal terms and do not give a polynomial-time method for the associated optimization problems. Pardalos and Schnitger proved that, even for constrained indefinite quadratic programs, deciding whether a given feasible point is a local minimizer and deciding whether a local minimum is strict are NP-hard [26]. In a Euclidean instance with fixed radius r > 0, local optimality can be expressed by adjoining r2 − ∥x − x⋆ ∥2 ≥ 0 and certifying nonnegativity of g − g(x⋆ ) on the resulting neighborhood; strictness additionally requires x⋆ to be the only feasible zero. The radius and the required semantic conditions are not supplied by Proposition 7.2. 8. Conclusions We have extracted the formal mechanism of Fischer’s Positivstellensatz construction into scalar and function-algebra axioms. The strict and weak constructions give universal terms under these axioms. The examples include ordered fields that are not real closed, exact rational arithmetic, and variants of standard activation functions. The complexity analysis separates expanded term length from evaluation using shared computation graphs. For the constructions considered here, the expanded strict certificate has cubic length in the number of constraints, while the shared computation graph has linear size and logarithmic depth. These bounds concern the explicit certificate constructions and do not establish optimality, efficient certificate discovery, or polynomial-time algorithms for the associated optimization problems. Several questions remain open. The present axioms do not cover R[X], which is a central setting for classical Positivstellensätze. It remains unknown whether there exists an algebra A satisfying ((AwP)∖(A5w))+(A5w− ) but not (A5w); see Remark C.10. It is open whether analogous constructions exist in the noncommutative setting. 9. Acknowledgements We are grateful to the three anonymous reviewers, whose comments helped improve the paper. This work has received funding from the European Union’s Horizon Europe research and innovation programme under grant agreement No. 101070568. LLM-based tools, primarily ChatGPT, were used in preparing this manuscript for brainstorming, checking dependencies, revising exposition, and 11
identifying possible gaps or ambiguities. The human authors assume responsibility for the content of the manuscript, including every mathematical statement, citation, and wording choice.
12
Appendix A. Universal terms and proof architecture The appendices are organized by mathematical role. This appendix gives the term conventions, universal constructions, common sign geometry, and basic scalar consequences. Appendices B and C prove the strict and weak Positivstellensätze. Appendix D verifies the function-algebra examples, including Fischer’s definable C r setting. Appendix E gives the compact term-length derivation, the shared-graph model used in the complexity statements, and the small-arity discussion. A.1. Term conventions. Convention A.1. We use the following notational conventions for terms: • For the binary functions + and ·, we write s + t and s · t (infix notation) instead of +(s, t) and ·(s, t) (prefix notation). • We may write s − t instead of s + (−t). P • Given k ≥ 0 and terms t1 , . . . , tk , we define the term 1≤i≤k ti by recursion on k as follows: P P if k = 0, then 1≤i≤0 ti := 0 (the empty sum), if k = 1, then 1≤i≤1 ti := t1 , and if k ≥ 2, P P then 1≤i≤k ti := ( 1≤i≤k−1 ti ) + tk . P • We may regard natural numbers k ≥ 2 as terms via k := 1≤i≤k 1, e.g., 2 = 1 + 1, 3 = (1 + 1) + 1, etc. • For powers, set s0 := 1, s1 := s, and, for every m ≥ 1, define sm+1 := sm · s. Thus positive powers are repeated products with no leading unit; in particular, z02 abbreviates z0 · z0 . • We may denote s · (t)−1 as either s/t or st . • Since we will be working always in (extensions of) the ambient theory ToF (where addition and multiplication are associative), we may write s + t + r and s · t · r instead of, e.g., (s + t) + r and (s · t) · r as no ambiguity will arise when it comes to evaluating such terms. If disambiguation is necessary, we adhere to a left-associative convention. A.2. Universal constructions. A.2.1. Strict construction. We state directly how the LsP -terms t̃i are constructed (extracted from the construction in [12]); set z := (z0 , . . . , zk ): ε̃(z0 , z1 , z2 ) := ν(z0 , z1 ) · (δ(z2 ))−1 P ψ̃(z1 , . . . , zk ) := 1≤i≤k ξ(−zi ) · zi ε̃i (z) := ε̃(z0 , −ψ̃(z1 , . . . , zk ) · (1 + · · · + 1)−1 , zi ) (for i = 1, . . . , k) | {z } k times
s̃i (z) := ρ(ξ(−zi ) + ε̃i (z)) (for i = 1, . . . , k) P h̃(z) := 1≤i≤k σ(s̃i (z)) · zi φ̃1 (z) := ξ(z0 + (1 + 1 + 1 + 1) · h̃(z)) φ̃2 (z) := ξ(−(z0 + h̃(z))) φ̃3 (z) := ξ(−z0 · h̃(z)) φ̃(z) := φ̃1 (z) + φ̃2 (z) + φ̃3 (z) w̃(z) := (z0 · φ̃1 (z) · (z0 + h̃(z))−1 + (z0 + h̃(z)) · φ̃2 (z) · (h̃(z))−1 + φ̃3 (z)) · (φ̃(z))−1 ũ(z) := z0 + (−w̃(z) · h̃(z)) t̃0 (z) := ρ(ũ(z)) t̃i (z) := ρ(w̃(z)) · s̃i (z) (for i = 1, . . . , k) 13
A.2.2. Weak construction. We state directly how the LwP -terms t̃i are constructed (also extracted from the construction in [12]); set z := (z0 , . . . , zk ): h̃(z1 , . . . , zk ) :=
P
1≤i≤k σ(ξ(−zi )) · zi
φ̃1 (z) := ξ(z0 + (1 + 1 + 1 + 1) · h̃(z)) φ̃2 (z) := ξ(−(z0 + h̃(z))) φ̃3 (z) := ξ(−z0 · h̃(z)) φ̃(z) := φ̃1 (z) + φ̃2 (z) + φ̃3 (z) q̃(z) := φ̃(z) · ξ(z02 ) · (ξ(−h̃(z)) + ξ(z0 ) · ξ(z0 + h̃(z))) ω̃1 (z) := φ̃3 (z) · q̃(z) · (φ̃(z))−1 ω̃2 (z) := q̃(z) · φ̃2 (z) · (z0 + h̃(z)) · (h̃(z) · φ̃(z))−1 ω̃3 (z) := q̃(z) · φ̃1 (z) · z0 · ((z0 + h̃(z)) · φ̃(z))−1 ω̃(z) := ω̃1 (z) + ω̃2 (z) + ω̃3 (z) ũ(z) := q̃(z) · z0 − ω̃(z) · h̃(z) ψ̃1 (z) := ξ(ũ(z)) Ψ̃1 (z) := ξ(ũ(z)) · ρ(ũ(z)) ψ̃2 (z) := ξ(ω̃(z)) Ψ̃2 (z) := ξ(ω̃(z)) · ρ(ω̃(z)) ψ̃3 (z) := ξ(q̃(z)) Ψ̃3 (z) := ξ(q̃(z)) · ρ(q̃(z)) t̃−1 (z) := ψ̃1 (z) · ψ̃2 (z) · Ψ̃3 (z) t̃0 (z) := Ψ̃1 (z) · ψ̃2 (z) · ψ̃3 (z) t̃i (z) := ψ̃1 (z) · Ψ̃2 (z) · ψ̃3 (z) · ξ(−zi ) (for i = 1, . . . , k) Remark A.2 (Uniform term evaluation). A fixed first-order term may be evaluated simultaneously on a parameterized family. If the input functions are jointly definable in (x, s), then the resulting family is jointly definable because definability is closed under composition. Membership of each fiber in a chosen function algebra is a separate closure question and is checked at the stages listed in the axiom-use map. A.3. Zero-constraint sanity check. When k = 0, the strict construction reduces to g = σ(ρ(g)). For the weak construction, the universal identity reduces to σ(p)g = σ(t0 ), where q = ξ(g 2 )ξ(g)3 , p = ξ(qg)ξ(q)2 ρ(q), t0 = ξ(qg)ρ(qg)ξ(q)2 . The weak theorem also gives {p = 0} = {g = 0}. These formulas provide a quick boundary-case check on the term conventions and on the leading multiplier in the weak identity. 14
A.4. Proof architecture and common sign geometry. Both constructions first compress the constraint list into a single auxiliary function h and then use the same three sign gates. Their dependency patterns are: strict: (g, f1 , . . . , fk ) ⇝ (ψ, εi , si ) ⇝ h ⇝ (φ1 , φ2 , φ3 , w) ⇝ (u, ti ), weak: (g, f1 , . . . , fk ) ⇝ h ⇝ (φ1 , φ2 , φ3 , q) ⇝ ω ⇝ u ⇝ (p, ti ). Lemma A.3 (Common sign geometry). Let g, h : X → R satisfy {h ≥ 0} ⊆ {g ≥ 0}, and put U1 := {g + 4h > 0},
U2 := {g + h < 0},
U3 := {g > 0} ∩ {h < 0}.
Then: (1) on U1 one has g + h > 0 and g + h ≥ 43 g; (2) on U2 one has h < 0, hence (g + h)/h > 0; (3) on U3 one has −gh > 0; (4) U1 ∪ U2 ∪ U3 = X \ ({g = 0} ∩ {h = 0}). If the stronger inclusion {h ≥ 0} ⊆ {g > 0} holds, then U1 , U2 , U3 cover all of X. Proof. On U1 , if h ≥ 0, then g ≥ 0 and g + h > 0, while g + h ≥ g ≥ 43 g. If h < 0, then g + 4h > 0 gives g > 0 and h > −g/4, hence g + h > 3g/4. If g + h < 0 and h ≥ 0, the assumed implication gives g ≥ 0, a contradiction; this proves (2), and (3) is immediate. For (4), suppose a point lies outside U1 ∪ U2 ∪ U3 . Then g + 4h ≤ 0 and g + h ≥ 0, so 3h ≤ 0. If h < 0, then g + h ≥ 0 forces g > 0, placing the point in U3 ; hence h = 0. The two displayed inequalities then give g = 0. The converse is immediate. Under the stronger inclusion, g = h = 0 is impossible because h ≥ 0 would imply g > 0. □ With φ1 := ξ(g + 4h), φ2 := ξ(−(g + h)), φ3 := ξ(−gh), axiom (Tξ2) gives {φj > 0} = Uj . Thus Lemma A.3 gives the cover used in the strict proof and the denominator-safety estimates used in the weak proof and in the Fischer regularity argument. The closure axioms enter the constructions at the following stages; all other steps use only ring operations from (A0). Construction
Purpose
Non-ring closure axioms
Strict ψ Strict εi Strict si Strict w Strict ti
detect violated constraints positive correction with a pointwise bound lift positive coefficients through σ ◦ ρ glue the three sign-region formulas take the final positive roots
(A2) (Aδ), (Aν), (A1) (A3s) (A2), (A4s), (A1) (A3s)
Weak h Weak φ, q Weak ω1 Weak ω2 Weak ω3 Weak ψj , Ψj
detect violated constraints form the sign gates and regularizing factor cancel the common factor φ in q cancel φ and regularize division by h cancel φ and regularize division by g + h Hilbert–17 factorizations of u, ω, q
(A2), (A3w) (A2) (A2) (A2), (A4w) (A2), (A5w) (A2), (A3w)
In the three weak ωi rows, the factor φ occurring in q cancels pointwise. On {φ = 0} = {g = 0} ∩ {h = 0}, both the raw terms and their cancelled expressions vanish. Thus these steps do not use (A1).
15
A.5. Scalar consequences and pathologies for σ and ρ. In this subsection we establish in Lemma A.4 some basic properties of σ and ρ needed later. We also construct in Example A.5 a highly pathological example of a (σ, ρ)-pair which demonstrates some properties which are not consequences of the axioms. Lemma A.4. In every model R = (R; . . .) of TwP we have for every a ∈ R: (1) σ(1) = 1 (2) ρ(0) = 0 (3) σ(0) = 0, (4) if a > 0, then σ(a) > 0, and (5) if a > 0, then ρ(a) > 0. Moreover, the restriction ρ : [0, +∞) → [0, +∞) is injective, and the restriction σ : [0, +∞) → [0, +∞) is surjective. Proof. (1) We have ρ(1) ≥ 0 and σ(ρ(1)) = 1 by (Tρ) and (Tσρ). Thus (Tσ2) and (Tσρ) yield: 1 = σ(ρ(1)) = σ(ρ(1) · 1) = σ(ρ(1)) · σ(1) = 1 · σ(1) = σ(1) (2) If ρ(0) > 0, then ρ(0)−1 > 0, so by (Tσ2) and (Tσρ): σ(1) = σ(ρ(0) · ρ(0)−1 ) = σ(ρ(0)) · σ(ρ(0)−1 ) = 0 contradicting (1). Thus ρ(0) = 0. (3) By (Tσρ) we have σ(ρ(0)) = 0, and by (2) we have ρ(0) = 0, hence σ(0) = 0. (4) Suppose a > 0. By (1) and (Tσ2) we have: 1 = σ(1) = σ(a · a−1 ) = σ(a) · σ(a−1 ) Thus σ(a) ̸= 0. Since σ(a) ≥ 0 by (Tσ1), this gives σ(a) > 0. (5) Suppose a > 0, thus ρ(a) ≥ 0 and σ(ρ(a)) = a > 0 by (Tρ) and (Tσρ). If ρ(a) = 0, then by (3), a = σ(ρ(a)) = σ(0) = 0 a contradiction. Thus ρ(a) > 0. Finally, for injectivity of ρ, suppose a, b ≥ 0 satisfy ρ(a) = ρ(b). Applying σ yields a = σ(ρ(a)) = σ(ρ(b)) = b by (Tσρ); the surjectivity of the (restriction of) σ likewise follows by (Tσρ). □ The axioms TwP do not determine whether ρ is surjective, whether σ is injective, or whether either function is monotone on [0, +∞). The following example shows this. Example A.5 (Wild σ and ρ). We will construct functions σ, ρ : R → R which satisfy the scalar axioms involving σ, ρ, and such that for every interval (a, b) ⊆ [0, +∞): • (ρ nowhere surjective) (a, b) ̸⊆ ρ[(0, +∞)], • (σ nowhere injective) the restriction σ|(a,b) : (a, b) → R is not injective, and • (σ and ρ nowhere monotone) neither σ nor ρ is monotone (=weakly increasing or weakly decreasing) when restricted to (a, b). The example uses the Axiom of Choice (AC), through the construction below. Construction. We construct additive maps on R with the required algebraic properties. Since R is an infinite-dimensional vector space over Q, there exists a Q-linear isomorphism: H : R→R⊕R Its existence follows, for example, from the existence of a Hamel basis for R over Q. Next, let π1 : R ⊕ R → R be projection onto the first coordinate, and let ι1 : R → R ⊕ R, 16
t 7→ (t, 0)
be the inclusion of the first summand. Define additive maps: L := π1 ◦ H : R → R,
M := H −1 ◦ ι1 : R → R
Then: • L ◦ M = idR , • L is surjective and not injective, and • M is injective and not surjective. First, we claim that L and M are discontinuous. Indeed, a continuous additive map R → R must be of the form x 7→ cx for some c ∈ R (this is a classical fact due to Cauchy which easily follows from the much stronger [4, Theorem 1.1.7]). But such a map is either 0 or bijective. Next, again by [4, 1.1.7], any additive map R → R which is monotone on a nonempty interval is automatically continuous. Since L and M are discontinuous, it follows that neither L nor M is monotone on any nonempty interval. We transfer L, M to (0, +∞) via log and exp. Define: ( exp(L(log(x))) if x > 0 σ : R → R, x 7→ σ(x) := 0 if x ≤ 0 and
( exp(M (log(x))) if x > 0 ρ : R → R, x 7→ ρ(x) := 0 if x ≤ 0 We verify the scalar axioms involving σ, ρ: (Tσ1) This is immediate by definition. (Tρ) This is immediate by definition. (Tσ2) Let a, b ≥ 0. If ab = 0, then σ(ab) = σ(0) = 0, while at least one of σ(a), σ(b) is also 0, so σ(ab) = 0 = σ(a)σ(b). If both a, b > 0, then by additivity of L: σ(ab) = exp(L(log(ab))) = exp(L(log a + log b)) = exp(L(log a) + L(log b)) = σ(a)σ(b) (Tσρ) Let a ≥ 0. If a = 0, then σ(ρ(0)) = σ(0) = 0. If a > 0, then: σ(ρ(a)) = σ(exp(M (log a))) = exp(L(M (log a))) = exp(log a) = a We verify the three pathologies; let (a, b) ⊆ [0, +∞), i.e., 0 ≤ a < b < +∞. (ρ nowhere surjective) Set V := M [R] ⊆ R. Then V is a proper Q-subspace of R, and thus V does not contain any open interval. It follows that exp[V ] ⊆ (0, +∞) also contains no open interval. However, for x > 0 we have ρ(x) = exp(M (log x)) ∈ exp[V ], hence ρ[(0, +∞)] ⊆ exp(V ), hence also does not contain any open interval. (σ nowhere injective) Since {0} ⊊ ker(L) ⊊ R, it follows that ker(L) is dense in R and co-dense in R (i.e., R \ ker(L) is dense in R). Thus there exists some u ∈ R and 0 ̸= k ∈ ker(L) such that: log(a) < u < u + k < log(b) Set x := eu and y := eu+k . Then x, y ∈ (a, b) and x ̸= y. But: σ(x) = exp(L(u)) and σ(y) = exp(L(u + k)) = exp(L(u) + L(k)) = exp(L(u)) since k ∈ ker(L). Hence σ(x) = σ(y). (σ and ρ nowhere monotone) Suppose towards a contradiction that σ were monotone on (a, b). Since log : (a, b) → (log a, log b) and exp : R → (0, +∞) are strictly increasing homeomorphisms (using the convention in the interval (log a, log b) that log 0 := −∞), the function L = log ◦σ ◦ exp would then be monotone on (log a, log b), contradicting the fact above that L is not monotone on any open interval. Thus σ is not monotone on (a, b).
17
The same argument applies to ρ, using M = log ◦ρ ◦ exp on (log a, log b). Hence ρ is not monotone on (a, b) either. □ Appendix B. Proof of the strict Positivstellensatz In this appendix we prove the Strict Positivstellensatz 4.1, which will be established as Lemma B.5(2) and Corollary B.6 below. The overall strategy of the proof is to carry out Fischer’s construction in [12] in the axiomatic setting. This is done by constructing a sequence of functions X → R: fi ⇝ (ψ, εi , si ) ⇝ h ⇝ (φi , φ, w) ⇝ (u, ti ) as defined by the sequence of LsP -terms presented in the strict construction of subsection A.2, all while checking along the way that they have the desired properties in the axiomatic setting. First we observe the role of the term ε̃(z0 , z1 , z2 ): Lemma B.1. (cf. [12, Lemma 2.1]) Let R |= TsP , let A ⊆ RX satisfy (A0), (A1), (Aδ), (Aν), and let g, φ, f ∈ A. Assume {g ≤ 0} ⊆ {φ > 0} Then the function ε := ε̃(g, φ, f ) = ν(g, φ) · (δ(f ))−1 : X → R satisfies: (1) ε ∈ A (2) ε > 0 on X, and (3) ε · f < φ on {g ≤ 0} Proof. (1) Since g, φ, f ∈ A, axiom (Aδ) gives δ(f ) ∈ A. By (Tδ) we have 0 < δ(f (x)) for all x ∈ X, so δ(f ) > 0 on X. Hence (δ(f ))−1 ∈ A by (A1). Next, by assumption {g ≤ 0} ⊆ {φ > 0} so axiom (Aν) applies to the pair (g, φ), and yields ν(g, φ) ∈ A. Therefore ε = ν(g, φ) · (δ(f ))−1 ∈ A by (A0). (2) Fix x ∈ X. If g(x) > 0, then by (Tν1) we have ν(g(x), φ(x)) > 0; if g(x) ≤ 0, then by assumption φ(x) > 0, and again (Tν1) gives ν(g(x), φ(x)) > 0. Since both ν(g, φ) > 0 on X and (δ(f ))−1 > 0 on X, it follows that ε > 0 on X. (3) Fix x ∈ {g ≤ 0}. Then φ(x) > 0 by assumption, and by (Tν2): ν(g(x), φ(x)) ≤ φ(x) There are two cases. Case 1: (f (x) ≤ 0) Then: ε(x)f (x) ≤ 0 < φ(x) Case 2: (f (x) > 0) Then by (Tδ): 2f (x) ≤ δ(f (x)) Since δ(f (x)) > 0, we get: 0 <
f (x) 1 ≤ δ(f (x)) 2
Thus: ε(x)f (x) = ν(g(x), φ(x))
f (x) φ(x) ≤ < φ(x) δ(f (x)) 2
□
For the rest of this subsection, we fix k ≥ 0, a model R |= TsP , an algebra A ⊆ RX satisfying (AsP), and functions g, f1 , . . . , fk ∈ A satisfying: \ F := {fi ≥ 0} ⊆ {g > 0}, 1≤i≤k
Our first two lemmas follow the arguments of (the proof of) [12, Lemma 2.2]. 18
First define the following functions X → R: X
ψ := ψ̃(f1 , . . . , fk ) =
ξ(−fi ) · fi
1≤i≤k
εi := ε̃i (g, f1 , . . . , fk ) = ε̃(g, −ψ/k, fi ) (for i = 1, . . . , k) si := s̃i (g, f1 , . . . , fk ) = ρ(ξ(−fi ) + εi ) (for i = 1, . . . , k)
The functions ψ, εi , si have the following properties: Lemma B.2. We have: (1) ψ ∈ A, ψ ≤ 0 on X, and {g ≤ 0} ⊆ {ψ < 0}. Moreover, if k ≥ 1, we have for each i = 1, . . . , k: (2) εi ∈ A, εi > 0 on X, and on {g ≤ 0} we have: εi fi < −ψ/k; (3) si ∈ A, si > 0 on X, and σ(si ) = ξ(−fi ) + εi P Proof. (1) Since each fi ∈ A, axiom (A2) gives ξ(−fi ) ∈ A, hence ψ = 1≤i≤k ξ(−fi )fi ∈ A by (A0). Next, fix x ∈ X. By (Tξ1), for each i we have ξ(−fi (x)) ≥ 0. Also, by (Tξ2), ξ(−fi (x)) > 0 iff −fi (x) > 0 iff fi (x) < 0. Therefore, for each i we have ξ(−fi (x))fi (x) ≤ 0; indeed, if fi (x) ≥ 0, then ξ(−fi (x)) = 0, and if fi (x) < 0, then ξ(−fi (x)) > 0. Summing over i yields ψ(x) ≤ 0. T Next suppose g(x) ≤ 0, which implies k ≥ 1. Since 1≤i≤k {fi ≥ 0} ⊆ {g > 0}, it is impossible for fi (x) ≥ 0 for all i since otherwise x ∈ F . Thus for some i we must have fi (x) < 0, and thus ξ(−fi (x))fi (x) < 0. All other summands ξ(−fj (x))fj (x) of ψ(x) are ≤ 0, so altogether we have ψ(x) < 0. Assume now k ≥ 1, and fix i ∈ {1, . . . , k}. (2) By (1) we have {g ≤ 0} ⊆ {ψ < 0}, hence {g ≤ 0} ⊆ {−ψ/k > 0}, since k > 0. Moreover, −ψ/k ∈ A as a consequence of (A0) and (A1). Thus Lemma B.1 applied with φ := −ψ/k and f := fi , shows that εi = ε̃(g, −ψ/k, fi ) ∈ A, that εi > 0 on X, and that on {g ≤ 0} we have εi fi < −ψ/k. (3) Since −fi ∈ A, axiom (A2) yields ξ(−fi ) ∈ A; together with εi ∈ A from (2) this gives ξ(−fi ) + εi ∈ A. Moreover, ξ(−fi ) ≥ 0 on X by (Tξ1), and εi > 0 on X by (2), so ξ(−fi ) + εi > 0 on X. Hence axiom (A3s) applies and we obtain: si = ρ(ξ(−fi ) + εi ) ∈ A Since the input of ρ is strictly positive, Lemma A.4(5) yields si > 0 on X. Finally, axiom (Tσρ) gives: σ(si ) = σ(ρ(ξ(−fi ) + εi )) = ξ(−fi ) + εi □ Next define the following function X → R: h := h̃(g, f1 , . . . , fk ) =
X
σ(si ) · fi
1≤i≤k
The function h has the following properties: Lemma B.3. (cf. [12, Lemma 2.2]) The function h belongs to A and satisfies: X h = ψ+ εi fi and F ⊆ {h ≥ 0} ⊆ {g > 0} 1≤i≤k 19
Proof. There are two cases: P Case 1: (k = 0) In this case, we have h = 0 ∈ A by (A0) and ψ + 1≤i≤k εi fi = ψ + 0 = ψ = 0 (using our empty summation convention), thus the identity holds. Furthermore, in this case we have T {h ≥ 0} = X, and the assumption 1≤i≤k {fi ≥ 0} ⊆ {g > 0} reduces to saying X = {g > 0}. Thus the two inclusion relations follow trivially. Case 2: (k ≥ 1) Since each si ∈ A and si > 0 on X by Lemma B.2(3), axiom (A3s) gives σ(si ) ∈ A for all i = 1, . . . , k. Hence h ∈ A by (A0). For the identity note that by Lemma B.2(3): X X X X X h = σ(si )fi = (ξ(−fi ) + εi )fi = ξ(−fi )fi + εi fi = ψ + εi fi 1≤i≤k
1≤i≤k
1≤i≤k
1≤i≤k
1≤i≤k
For the first inclusion, suppose x ∈ F , i.e., fi (x) ≥ 0 for all i. Since σ(si (x)) ≥ 0 for all i (by (Tσ1)), it follows that each summand σ(si (x))fi (x) ≥ 0, and thus h(x) ≥ 0. We prove the second inclusion by establishing the contrapositive. Let x ∈ X and suppose g(x) ≤ 0. By Lemma B.2(2), for each i we have εi (x)fi (x) < −ψ(x)/k. Summing over all i yields: X εi (x)fi (x) < −ψ(x) 1≤i≤k
Using the identity for h, we obtain h(x) = ψ(x) +
X
εi (x)fi (x) < ψ(x) − ψ(x) = 0
1≤i≤k
Thus x ∈ {h < 0}. This shows the inclusion {h ≥ 0} ⊆ {g > 0}.
□
For Lemmas B.4 and B.5 and Corollary B.6 below, we follow the arguments of (the proof of) [12, Theorem 1.1]. Next define the following functions X → R: φ1 := φ̃1 (g, f1 , . . . , fk ) = ξ(g + 4h) φ2 := φ̃2 (g, f1 , . . . , fk ) = ξ(−(g + h)) φ3 := φ̃3 (g, f1 , . . . , fk ) = ξ(−gh) φ := φ̃(g, f1 , . . . , fk ) = φ1 + φ2 + φ3 gφ1 (g + h)φ2 w := w̃(g, f1 , . . . , fk ) = + + φ3 /φ g+h h The functions φi , φ, w satisfy the following properties: Lemma B.4. We have: (1) φ1 , φ2 , φ3 , φ ∈ A and φ > 0 on X, (2) w ∈ A, w > 0 on X, and: g(x) g(x) + h(x) w(x) = g(x) + h(x) h(x)
if h(x) ≥ 0 if g(x) ≤ 0
Proof. Below we will freely use the fact {h ≥ 0} ⊆ {g > 0} from Lemma B.3 several times. (1) Since g, h ∈ A by Lemma B.3, axiom (A0) gives g + 4h, −(g + h), −gh ∈ A, hence by (A2) we have φ1 , φ2 , φ3 ∈ A, and thus also φ ∈ A by (A0). It remains to show φ > 0 on X. Let U1 , U2 , U3 be the sign regions from Lemma A.3. By (Tξ2), {φj > 0} = Uj
(j = 1, 2, 3). 20
The stronger inclusion {h ≥ 0} ⊆ {g > 0} from Lemma B.3 implies, by Lemma A.3, that U1 ∪ U2 ∪ U3 = X. Hence at every point at least one φj is positive. Since all three are nonnegative by (Tξ1), their sum φ is strictly positive on X. (2) First we will show w ∈ A. This relies on the following two disjointness claims: • {g + 4h ≥ 0} ∩ {g + h = 0} = ∅. Indeed, suppose x ∈ X is such that g(x) + h(x) = 0, i.e., h(x) = −g(x). Suppose towards a contradiction that g(x) + 4h(x) ≥ 0, then −3g(x) = g(x) + 4h(x) ≥ 0 implies g(x) ≤ 0 and thus h(x) ≥ 0, contradicting {h ≥ 0} ⊆ {g > 0}. • {−(g + h) ≥ 0} ∩ {h = 0} = ∅. Indeed, if x ∈ X is such that h(x) = 0, then g(x) > 0; thus −(g(x) + h(x)) = −g(x) < 0, i.e., x ̸∈ {−(g + h) ≥ 0}. Thus by (A4s) we get ξ(g + 4h)(g + h)−1 = φ1 (g + h)−1 ∈ A and ξ(−(g + h))h−1 = φ2 h−1 ∈ A. Next, since φ > 0 on X by (1), we have φ−1 ∈ A by (A1). It now follows that w ∈ A by (A0). Finally, we must show w > 0 on X and the indicated formula for w(x). Let x ∈ X be arbitrary, there are three cases to consider: Case 1: h(x) ≥ 0. Then g(x) > 0, so x ∈ U1 . Also x ̸∈ U2 since g(x) + h(x) > 0, and x ̸∈ U3 since h(x) ≥ 0. Thus φ1 (x) > 0 and φ2 (x) = φ3 (x) = 0. Thus: g(x)φ1 (x) g(x) w(x) = /φ(x) = g(x) + h(x) g(x) + h(x) Since g(x) > 0 and h(x) ≥ 0, it follows that w(x) > 0. Case 2: g(x) ≤ 0. Then necessarily h(x) < 0, so x ∈ U2 . Also, x ̸∈ U1 , for otherwise g(x) + 4h(x) > 0 with h(x) < 0 would imply g(x) > −4h(x) > 0, a contradiction. Furthermore, x ̸∈ U3 since g(x) ≤ 0. Thus φ2 (x) > 0 and φ1 (x) = φ3 (x) = 0. Thus: (g(x) + h(x))φ2 (x) g(x) + h(x) w(x) = /φ(x) = h(x) h(x) Finally, since g(x) + h(x) < 0 and h(x) < 0, we get w(x) > 0. Case 3: g(x) > 0 and h(x) < 0. Then φ3 (x) > 0. We distinguish three subcases: Subcase 3a: g(x) + h(x) < 0. First we claim φ1 (x) = 0; otherwise, if g(x) + 4h(x) > 0 we have together with g(x) + h(x) < 0 that 3h(x) > 0, a contradiction. Thus g(x)φ1 (x)/(g(x) + h(x)) = 0. Also φ2 (x) > 0, and thus (g(x) + h(x))φ2 (x)/h(x) > 0. It now follows that w(x) > 0. g(x)φ1 (x) Subcase 3b: g(x) + h(x) = 0. Then g(x)+h(x) = 0 by definition of 0−1 = 0. Also (g(x) + h(x))φ2 (x)/h(x) = 0 as well. Thus w(x) > 0. g(x)φ1 (x) 2 (x) Subcase 3c: g(x) + h(x) > 0. Then g(x)+h(x) ≥ 0; φ2 (x) = 0 and so (g(x)+h(x))φ = 0. It follows h(x) that w(x) > 0. □ Finally, define the following functions X → R: u := ũ(g, f1 , . . . , fk ) := g − wh t0 := t̃0 (g, f1 , . . . , fk ) = ρ(u) ti := t̃i (g, f1 , . . . , fk ) = ρ(w)si
(for i = 1, . . . , k)
The functions u, ti satisfy the following properties: Lemma B.5. We have for i = 0, . . . , k: (1) u ∈ A and u > 0 on X, (2) ti ∈ A and ti > 0 on X, and (3) if i ≥ 1, then σ(ti ) = wσ(si ). Proof. (1) Since g, w, h ∈ A by Lemmas B.4( 2) and B.3, it follows that u ∈ A since A is a ring by (A0). It remains to show u > 0 on X. Let x ∈ X be arbitrary, there are two cases: 21
Case 1: (h(x) ≥ 0). Then by Lemma B.4(2) we have in this case: w(x) =
g(x) g(x) + h(x)
hence:
g(x)h(x) g(x)2 = g(x) + h(x) g(x) + h(x) However, since {h ≥ 0} ⊆ {g > 0} by Lemma B.3, it follows that g(x) + h(x) > 0 and g(x)2 > 0, thus u(x) > 0. Case 2: (h(x) < 0) There are two subcases: Subcase 2a: (g(x) ≤ 0) Then by Lemma B.4(2) we have: u(x) = g(x) − w(x)h(x) = g(x) −
w(x) =
g(x) + h(x) h(x)
and thus u(x) = g(x) − w(x)h(x) = g(x) − (g(x) + h(x)) = −h(x) > 0 Subcase 2b: (g(x) > 0) Then since w(x) > 0 by Lemma B.4(2) and h(x) < 0, we have: u(x) = g(x) − w(x)h(x) = g(x) + w(x)(−h(x)) > 0 (2) Since u ∈ A and u > 0 on X by (1), axiom (A3s) gives t0 = ρ(u) ∈ A. Moreover, by Lemma A.4(5), we have t0 > 0 on X. Likewise, since w ∈ A and w > 0 on X by Lemma B.4(2), axiom (A3s) and Lemma A.4(5) give ρ(w) ∈ A and ρ(w) > 0 on X. Thus for i ≥ 1 we have ti = ρ(w)si ∈ A by (A0), and ti > 0 on X because we also have si > 0 on X by Lemma B.2(3). (3) Let i ≥ 1. Since w > 0 on X by Lemma B.4(2), we have ρ(w) > 0 on X by Lemma A.4(5). Also we have si > 0 on X by Lemma B.2(3). Therefore by (Tσ2) and (Tσρ) we have: σ(ti ) = σ(ρ(w)si ) = σ(ρ(w))σ(si ) = wσ(si )
□
In conclusion, we have: Corollary B.6. X
g = σ(t0 ) +
σ(ti )fi
1≤i≤k
Proof. Note that: X X σ(t0 ) + σ(ti )fi = σ(ρ(u)) + wσ(si )fi 1≤i≤k
(by definition of t0 and Lemma B.5(3))
1≤i≤k
= u+w
X
σ(si )fi
(by (Tσρ) and u > 0 on X by Lemma B.5(1))
1≤i≤k
= u + wh (by definition of h) = (g − wh) + wh (by definition of u) = g
22
□
Appendix C. Proof of the weak Positivstellensatz In this appendix we prove the Weak Positivstellensatz 4.4, which will be established as Corollary C.9 below. The overall strategy is similar to the proof in the previous Appendix B. Namely, we will construct a sequence of functions in X → R: fi ⇝ h ⇝ φ ⇝ q ⇝ ω ⇝ u ⇝ (ψi , Ψi ) ⇝ (p, ti ) as defined by the sequence of LwP -terms presented in the weak construction of subsection A.2, all while checking along the way that they have the desired properties in the axiomatic setting. First, we have a σ-version of Hilbert’s 17th problem, in the sense that a nonnegative function f ∈ A can be written as a quotient of σ-values of functions from A in the following sense: Hilbert–17 Lemma C.1. (cf. [12, Lemma 2.3]) Let R |= TwP , let A ⊆ RX satisfy (A0), (A2), and (A3w), and let f ∈ A. If f ≥ 0 on X, then the functions ψ := ξ(f )
Ψ := ρ(f ) · ξ(f )
and
satisfy: (1) the functions ψ, Ψ, σ(ψ), σ(Ψ) are in A and are nonnegative on X, (2) σ(ψ) · f = σ(Ψ), and (3) {ψ = 0} = {Ψ = 0} = {f = 0}. Proof. (1) Since f ∈ A, axiom (A2) gives ψ = ξ(f ) ∈ A. Also, by (Tξ1), we have ψ ≥ 0 on X. Since f ≥ 0 and f ∈ A, axiom (A3w) applied to f yields Ψ = ρ(f ) · ξ(f ) ∈ A. Moreover, by (Tρ) and (Tξ1), both ρ(f ) and ξ(f ) are nonnegative on X, hence Ψ ≥ 0 on X. Finally, axiom (A3w) yields σ(ψ), σ(Ψ) ∈ A and axiom (Tσ1) gives that they are nonnegative on X. (2) Fix x ∈ X. Since f (x) ≥ 0, we have ρ(f (x)) ≥ 0 by (Tρ), and also ψ(x) = ξ(f (x)) ≥ 0 by (Tξ1). Hence (Tσ2) applies to ρ(f (x))ψ(x), giving σ(Ψ(x)) = σ(ρ(f (x))ψ(x)) = σ(ρ(f (x)))σ(ψ(x)) Since f (x) ≥ 0, axiom (Tσρ) gives σ(ρ(f (x))) = f (x). Thus σ(Ψ(x)) = f (x)σ(ψ(x)). Since x ∈ X was arbitrary, this yields σ(ψ) · f = σ(Ψ). (3) Fix x ∈ X. Since f (x) ≥ 0, by (Tξ2) we have ψ(x) = ξ(f (x)) > 0 iff f (x) > 0. Because f (x) ≥ 0, this is equivalent to ψ(x) = 0 iff f (x) = 0. Hence {ψ = 0} = {f = 0}. It remains to prove {Ψ = 0} = {f = 0}. If f (x) = 0, then ξ(f (x)) = ξ(0) = 0, and ρ(f (x)) = ρ(0) = 0, hence Ψ(x) = 0. Conversely, suppose Ψ(x) = 0. Since f ≥ 0 on X, if f (x) ̸= 0, then f (x) > 0. By (Tξ2) we have ξ(f (x)) > 0, and by Lemma A.4(5) we have ρ(f (x)) > 0. Hence Ψ(x) = ρ(f (x))ξ(f (x)) > 0 a contradiction. Thus f (x) = 0.
□
For the rest of this subsection, we fix k ≥ 0, a model R |= TwP , an algebra A ⊆ RX satisfying (AwP), and functions g, f1 , . . . , fk ∈ A satisfying: \ F := {fi ≥ 0} ⊆ {g ≥ 0} 1≤i≤k
Define the following function X → R: h := h̃(f1 , . . . , fk ) =
X
σ(ξ(−fi ))fi
1≤i≤k
Lemma C.2. The function h belongs to A and satisfies: h ≤ 0 on X,
F = {h = 0} = {h ≥ 0} ⊆ {g ≥ 0} 23
Proof. First, since fi ∈ A, axiom (A2) gives ξ(−fi ) ∈ A. By axiom (A3w), applied to the nonnegative function ξ(−fi ), we obtain σ(ξ(−fi )) ∈ A. Hence by (A0) we conclude h ∈ A. Next we will show h ≤ 0; let x ∈ X be arbitrary. For each i we have ξ(−fi (x)) ≥ 0 by (Tξ1), hence also σ(ξ(−fi (x))) ≥ 0 by (Tσ1). Now consider the sign of the factor fi (x): • If fi (x) ≥ 0, then −fi (x) ≤ 0, so by (Tξ2) we get ξ(−fi (x)) = 0, and hence: σ(ξ(−fi (x)))fi (x) = 0 • If fi (x) < 0, then ξ(−fi (x)) > 0 by (Tξ2), and thus σ(ξ(−fi (x))) > 0 by Lemma A.4(4). Since fi (x) < 0 we get: σ(ξ(−fi (x)))fi (x) < 0 Thus each summand of h(x) is ≤ 0, hence h(x) ≤ 0. Thus h ≤ 0 on X, and so {h = 0} = {h ≥ 0}. To show F ⊆ {h = 0}, suppose fi (x) ≥ 0 for all i. Then σ(ξ(−fi (x)))fi (x) = 0 for all i, as indicated above. Summing gives h(x) = 0. Finally, to show {h = 0} ⊆ F ⊆ {g ≥ 0}, suppose h(x) = 0. Then by the above it must be the case that fi (x) ≥ 0 for every i, i.e., x ∈ F . The inclusion F ⊆ {g ≥ 0} is true by assumption. □ Define the following functions X → R: φ1 := φ̃1 (g, f1 , . . . , fk ) = ξ(g + 4h) φ2 := φ̃2 (g, f1 , . . . , fk ) = ξ(−(g + h)) φ3 := φ̃3 (g, f1 , . . . , fk ) = ξ(−gh) φ := φ̃(g, f1 , . . . , fk ) = φ1 + φ2 + φ3 Lemma C.3. The functions φ1 , φ2 , φ3 , φ satisfy: (1) φ1 , φ2 , φ3 ∈ A, (2) φ1 , φ2 , φ3 , φ ≥ 0 on X, and (3) {φ = 0} = {g = 0} ∩ {h = 0}. Proof. (1) Since g ∈ A by assumption and h ∈ A by Lemma C.2, it follows from (A0) and (A2) that φ1 , φ2 , φ3 , φ ∈ A. (2) This is immediate from (Tξ1). (3) Lemma C.2 gives {h ≥ 0} = {h = 0} ⊆ {g ≥ 0}, so Lemma A.3 applies. By (Tξ2), the positive sets of φ1 , φ2 , φ3 are precisely the corresponding sign regions U1 , U2 , U3 . Since the φj are nonnegative, φ(x) = 0 ⇐⇒ x ∈ / U1 ∪ U2 ∪ U3 . Lemma A.3(4) identifies the latter complement with {g = 0} ∩ {h = 0}. □ Define the following function X → R: q := q̃(g, f1 , . . . , fk ) = φ · ξ(g 2 ) · (ξ(−h) + ξ(g) · ξ(g + h)) Lemma C.4. The function q satisfies: (1) q ∈ A, (2) q ≥ 0 on X, and (3) {q = 0} = {g = 0}. Proof. (1) Since h, φ ∈ A by Lemmas C.2 and C.3(1), it follows from (A0) and (A2) that q ∈ A. (2) Since each factor in q is ≥ 0 on X by Lemma C.3(2) and (Tξ1), it follows that q ≥ 0 on X. (3) Let x ∈ X be arbitrary. First, if g(x) = 0, then g(x)2 = 0, so ξ(g(x)2 ) = 0, hence q(x) = 0. Conversely, suppose g(x) ̸= 0. Then g(x)2 > 0, so ξ(g(x)2 ) > 0 by (Tξ2). Also, by Lemma C.3(3), x ̸∈ {g = 0} ∩ {h = 0} = {φ = 0} implies φ(x) > 0. It remains to show: ξ(−h(x)) + ξ(g(x))ξ(g(x) + h(x)) > 0 24
If g(x) < 0, then h(x) ̸= 0 by Lemma C.2; since h ≤ 0, this gives h(x) < 0, so ξ(−h(x)) > 0. If g(x) > 0, then either h(x) < 0, in which case again ξ(−h(x)) > 0, or h(x) = 0, in which case g(x) + h(x) = g(x) > 0, so ξ(g(x))(ξ(g(x) + h(x))) > 0. Since every factor in q(x) is > 0, it follows that q(x) > 0. Thus q(x) = 0 implies g(x) = 0, and we conclude {q = 0} = {g = 0}. □ Define the following functions X → R: qφ3 φ qφ2 (g + h) ω2 := ω̃2 (g, f1 , . . . , fk ) = hφ qφ1 g ω3 := ω̃3 (g, f1 , . . . , fk ) = (g + h)φ ω := ω1 + ω2 + ω3 ω1 := ω̃1 (g, f1 , . . . , fk ) =
Remark C.5. The function ω plays the same role as “qw extended by 0” in the proof of [12, Theorem 1.2]. We avoid directly defining a function “w” as this is not guaranteed to be in the algebra A. Lemma C.6. The function ω satisfies: (1) ω ∈ A, (2) ω ≥ 0 on X, (3) {ω = 0} = {g = 0}, and (4) for every x ∈ X with g(x) ̸= 0: q(x)g(x) − ω(x)h(x) > 0 Proof. (1) First, we observe that the ωi are equal to the following functions: ω1 = ξ(g 2 )(ξ(−h) + ξ(g)ξ(g + h))φ3 ξ(g 2 )(ξ(−h) + ξ(g)ξ(g + h))φ2 (g + h) h 2 ξ(g )(ξ(−h) + ξ(g)ξ(g + h))φ1 g ω3 = g+h To see this, we do a case distinction on whether x ∈ {φ = 0} = {g = 0} ∩ {h = 0} or not; cf. Lemma C.3(3). If x ∈ {φ = 0}, then each ωi (x) = 0, and each of the expressions on the right-hand side are also = 0 since g(x) = h(x) = 0. Otherwise, if φ(x) ̸= 0, then in the definition of ωi we can expand the definition of q and cancel φ(x) from the numerator and denominator without changing the value of the function. These are pointwise identities under the totalized-inverse convention; they neither assert that φ−1 ∈ A nor use axiom (A1). By (A0), to show ω ∈ A, it suffices to show each ωi ∈ A. First, it easily follows from (A0), (A2), and Lemma C.3(1) that ω1 ∈ A. For ω2 , note first that: φ2 · ξ(g) · ξ(g + h) = 0 pointwise: if φ2 (x) > 0, then −(g(x) + h(x)) > 0, so g(x) + h(x) < 0, hence ξ(g(x) + h(x)) = 0 by (Tξ2); and if φ2 (x) = 0, then the product is 0. Thus: ω2 =
ξ(g 2 )ξ(−h)φ2 (g + h) h Now, ξ(g 2 ), ξ(−h), φ2 , g + h ∈ A, and by (A4w) applied to h, also ξ(−h)/h ∈ A. Hence ω2 ∈ A. ω2 =
25
For ω3 we will use axiom (A5w). By Lemma C.2, we have {h ≥ 0} ⊆ {g ≥ 0}, so (A5w) applies to the pair (g, h) and yields: ξ(g 2 )ξ(g + 4h) ξ(g 2 )φ1 = ∈ A g+h g+h Multiplying this by g ∈ A and by ξ(−h) + ξ(g)ξ(g + h) ∈ A, we get ω3 ∈ A. (2) We show each ωi ≥ 0 on X. For ω1 , this is immediate from the rewritten formula: every factor is ≥ 0. For ω2 , use from above: g+h ω2 = ξ(g 2 )ξ(−h)φ2 · h If φ2 (x) = 0, then ω2 (x) = 0. If φ2 (x) > 0, then g(x) + h(x) < 0. Since h ≤ 0, necessarily h(x) < 0, so (g(x) + h(x))/h(x) ≥ 0. Thus ω2 (x) ≥ 0. For ω3 , if φ1 (x) = 0, then ω3 (x) = 0. If φ1 (x) > 0, then g(x) + 4h(x) > 0. Since h(x) ≤ 0, this gives g(x) > 0. Also g(x) + h(x) > 0; otherwise g(x) + h(x) ≤ 0 and h(x) < 0, so g(x) + 4h(x) = (g(x) + h(x)) + 3h(x) < 0, a contradiction. Hence g(x)/(g(x) + h(x)) > 0, and therefore ω3 (x) ≥ 0. (3) Let x ∈ X be arbitrary. If g(x) = 0, then q(x) = 0 by Lemma C.4(3), so each ωi (x) = 0, and thus ω(x) = 0. Conversely, suppose g(x) ̸= 0. Then q(x) > 0 by Lemma C.4(2,3), and φ(x) > 0 by Lemma C.3(2,3). We show ω(x) > 0. There are two cases. Case 1: (g(x) < 0) Then h(x) < 0 by Lemma C.2. Also φ2 (x) > 0, since g(x) + h(x) < 0. Hence ω2 (x) > 0, so ω(x) > 0. Case 2: (g(x) > 0) There are two subcases. Case 2a: (h(x) = 0) Then φ1 (x) > 0 and ω3 (x) =
q(x)φ1 (x)g(x) > 0 (g(x) + 0)φ(x)
and so ω(x) > 0. Case 2b: (h(x) < 0) Then φ3 (x) = ξ(−g(x)h(x)) > 0, so ω1 (x) =
q(x)φ3 (x) > 0 φ(x)
which again yields ω(x) > 0. (4) Fix x ∈ X such that g(x) ̸= 0; note that q(x) > 0 by Lemma C.4(2,3) and ω(x) > 0 by parts (2) and (3). There are two cases. Case 1: (g(x) > 0) There are two subcases. Case 1a: (h(x) = 0) Then ω(x)h(x) = 0, so q(x)g(x) − ω(x)h(x) = q(x)g(x) > 0. because q(x) > 0. Case 1b: (h(x) < 0) In this case, we have q(x), g(x), ω(x), −h(x) > 0, and thus: q(x)g(x) − ω(x)h(x) = q(x)g(x) + ω(x)(−h(x)) > 0 Case 2: (g(x) < 0) Then h(x) < 0 by Lemma C.2. Moreover, φ2 (x) > 0, while φ1 (x) = φ3 (x) = 0; indeed, g(x) + 4h(x) ≤ g(x) < 0, and −g(x)h(x) < 0. Therefore: ω(x) = ω2 (x) =
g(x) + h(x) q(x)φ2 (x)(g(x) + h(x)) = q(x) h(x)φ(x) h(x)
since φ(x) = φ2 (x). Consequently, q(x)g(x) − ω(x)h(x) = q(x)g(x) − q(x)(g(x) + h(x)) = −q(x)h(x) > 0 26
□
Define the following function X → R: u := ũ(g, f1 , . . . , fk ) = qg − ωh Lemma C.7. The function u satisfies: (1) u ∈ A, (2) u ≥ 0 on X, and (3) {u = 0} = {g = 0}. Proof. (1) We have g, q, ω, h ∈ A by Lemmas C.4(1), C.6(1), and C.2, thus u ∈ A by (A0). (2 and 3) Fix x ∈ X. If g(x) = 0, then Lemma C.6(3) gives ω(x) = 0, and hence: u(x) = q(x)g(x) − ω(x)h(x) = q(x) · 0 − 0 · h(x) = 0 If g(x) ̸= 0, then by Lemma C.6(4) we have: u(x) = q(x)g(x) − ω(x)h(x) > 0 Thus u ≥ 0 on X, and moreover {u = 0} = {g = 0}.
□
Define the following functions X → R: ψ1 := ψ̃1 (g, f1 , . . . , fk ) = ξ(u) Ψ1 := Ψ̃1 (g, f1 , . . . , fk ) = ξ(u)ρ(u) ψ2 := ψ̃2 (g, f1 , . . . , fk ) = ξ(ω) Ψ2 := Ψ̃2 (g, f1 , . . . , fk ) = ξ(ω)ρ(ω) ψ3 := ψ̃3 (g, f1 , . . . , fk ) = ξ(q) Ψ3 := Ψ̃3 (g, f1 , . . . , fk ) = ξ(q)ρ(q) Lemma C.8. We have: (1) For each i = 1, 2, 3, the functions ψi , Ψi belong to A and are nonnegative on X. (2) The following identities hold: σ(ψ1 ) · u = σ(Ψ1 ),
σ(ψ2 ) · ω = σ(Ψ2 ),
σ(ψ3 ) · q = σ(Ψ3 )
(3) The following zero-set equalities hold: {ψ1 = 0} = {Ψ1 = 0} = {u = 0} {ψ2 = 0} = {Ψ2 = 0} = {ω = 0} {ψ3 = 0} = {Ψ3 = 0} = {q = 0} Proof. We argue in the same way for each pair (ψi , Ψi ). For (ψ1 , Ψ1 ), since u ∈ A and u ≥ 0 on X by Lemma C.7(1,2), the Hilbert–17 Lemma C.1 applied to f := u yields: • ψ1 , Ψ1 , σ(ψ1 ), σ(Ψ1 ) ∈ A and are nonnegative on X, • σ(ψ1 ) · u = σ(Ψ1 ), and • {ψ1 = 0} = {Ψ1 = 0} = {u = 0} For (ψ2 , Ψ2 ), apply Lemma C.1 to f := ω, using Lemma C.6(1,2). For (ψ3 , Ψ3 ), apply Lemma C.1 to f := q, using Lemma C.4(1,2). These three applications yield exactly (1), (2), and (3). □
27
Finally, define the following functions X → R: p := t̃−1 (g, f1 , . . . , fk ) = ψ1 ψ2 Ψ3 t0 := t̃0 (g, f1 , . . . , fk ) = Ψ1 ψ2 ψ3 ti := t̃i (g, f1 , . . . , fk ) = ψ1 Ψ2 ψ3 ξ(−fi ) (for i = 1, . . . , k) The functions p, t0 , ti satisfy the following properties: Corollary C.9. The functions p, t0 , . . . , tk belong to A and are nonnegative on X; moreover, {p = 0} = {g = 0} and σ(p)g = σ(t0 ) +
X
σ(ti )fi .
1≤i≤k
Proof. By Lemma C.8(1), for i = 1, 2, 3 we have that ψi , Ψi ∈ A and are ≥ 0 on X. Since also ξ(−fi ) ∈ A and ξ(−fi ) ≥ 0 on X by (A2) and (Tξ1), it follows from (A0) that the functions p, t0 , . . . , tk all belong to A and are nonnegative on X. Next we show {p = 0} = {g = 0}. Since p = ψ1 ψ2 Ψ3 and R is a field, we have: {p = 0} = {ψ1 = 0} ∪ {ψ2 = 0} ∪ {Ψ3 = 0} By Lemma C.8(3), this gives: {p = 0} = {u = 0} ∪ {ω = 0} ∪ {q = 0} Using Lemma C.7(3), Lemma C.6(3), and Lemma C.4(3), we obtain: {p = 0} = {g = 0} ∪ {g = 0} ∪ {g = 0} = {g = 0} Finally we prove the identity; we use that the functions ψi , Ψi , ξ(−fi ) are nonnegative on X: X X σ(t0 ) + σ(ti )fi = σ(t0 ) + σ(ψ1 Ψ2 ψ3 ξ(−fi ))fi (by definition of ti ) 1≤i≤k
1≤i≤k
= σ(t0 ) +
X
σ(ψ1 Ψ2 ψ3 )σ(ξ(−fi ))fi
(by (Tσ2))
1≤i≤k
X
= σ(t0 ) + σ(ψ1 Ψ2 ψ3 )
σ(ξ(−fi ))fi
1≤i≤k
= σ(Ψ1 ψ2 ψ3 ) + σ(ψ1 Ψ2 ψ3 )h (by definition of h) = σ(ψ2 )σ(ψ3 )σ(Ψ1 ) + σ(ψ1 )σ(ψ3 )σ(Ψ2 )h (by (Tσ2)) = σ(ψ2 )σ(ψ3 )σ(ψ1 )u + σ(ψ1 )σ(ψ3 )σ(ψ2 )ωh (by Lemma C.8(2)) = σ(ψ1 )σ(ψ2 )σ(ψ3 )(u + ωh) = σ(ψ1 )σ(ψ2 )σ(ψ3 )qg
(by definition of u)
= σ(ψ1 )σ(ψ2 )σ(Ψ3 )g
(by Lemma C.8(2))
= σ(ψ1 ψ2 Ψ3 )g = σ(p)g
(by (Tσ2))
(by definition of p)
□
Remark C.10. In the overall proof of 4.4, the axioms (A4w) and (A5w) are only used once each in the proof of Lemma C.6(1) above to show that ω2 , ω3 ∈ A. In particular, the Weak Positivstellensatz 4.4 is still true with the same proof if we replace (A4w) and (A5w) with the a priori weaker axioms: 28
(A4w− ) if g, h ∈ A, then: ξ(g 2 ) · ξ(−h) · ξ(−(g + h)) · (g + h) · (h)−1 ∈ A (A5w− ) if g, h ∈ A and {h ≥ 0} ⊆ {g ≥ 0}, then: ξ(g 2 )(ξ(−h) + ξ(g) · ξ(g + h)) · ξ(g + 4h) · g · (g + h)−1 ∈ A The potential upside to doing this is to broaden the class of examples. Indeed, if A is an algebra which satisfies (A0) and (A2), then (A4w)⇒(A4w− ) and (A5w)⇒(A5w− ). If the additional reciprocalclosure axiom (A1) is assumed, Lemma C.11 below shows that no extra generality is gained by considering (A4w− ). Without (A1), we do not claim that (A4w− ) implies (A4w). On the other hand, we do not have an example of an algebra which satisfies ((AwP)∖(A5w))+(A5w− ) but not (A5w). Lemma C.11. Suppose B ⊆ RX satisfies (A0), (A1), and (A2). Then B satisfies (A4w) if and only if B satisfies (A4w− ). Proof. (⇒) Let g, h ∈ B be arbitrary. By (A4w) applied to h, we have ξ(−h) · h−1 ∈ B. Also, by (A0) and (A2), ξ(g 2 ), ξ(−(g + h)), and g + h all lie in B. Multiplying all of these together yields: ξ(g 2 ) · ξ(−h) · ξ(−(g + h)) · (g + h) · (h)−1 ∈ B (⇐) Let f ∈ B be arbitrary; we will show ξ(−f ) · f −1 ∈ B. Consider the pair (g, h) = (−(1 + f 2 ), f ) ∈ B 2 . Note that g + h = −(f 2 − f + 1). Set p := f 2 − f + 1, so p ∈ B by (A0), and p > 0 on X; indeed: 1 2 3 + > 0 p = f− 2 4 Moreover, g 2 = (1 + f 2 )2 > 0 on X. Hence by (Tξ2) we have ξ(g 2 ) > 0 and ξ(p) > 0 on X. Next define β := ξ(g 2 ) · ξ(p) · p, which is in B by (A0) and (A2); moreover, β > 0 on X. Thus β −1 ∈ B by (A1). Now, by (A4w− ) applied to (g, h) we have: ξ(g 2 ) · ξ(−f ) · ξ(−(g + f )) · (g + f ) · f −1 ∈ B Using −(g + f ) = p and g + f = −p yields: ξ(g 2 ) · ξ(−f ) · ξ(p) · (−p) · f −1 = −β · ξ(−f ) · f −1 ∈ B Finally, multiplying by −β −1 yields ξ(−f ) · f −1 ∈ B.
□
C.1. Independence of reciprocal closure from the weak package. The omission of (A1) from (AwP) is genuine. The following example shows that reciprocal closure for arbitrary everywherepositive functions is not forced by the weak scalar theory together with (A0), (A2), (A3w), (A4w), and (A5w). Proposition C.12. There exist a model R |= TwP , a set X, and a function ring A ⊆ RX satisfying (AwP) but not (A1). Proof. Let R be a non-Archimedean ordered field, and let O := {a ∈ R : |a| ≤ n for some n ∈ N} be its ring of finite elements. If |a| ≤ m and |b| ≤ n, then |a + b| ≤ m + n and |ab| ≤ mn, so O is a subring; its definition also makes it convex. It is moreover a valuation ring: if a = ̸ 0 and a ∈ / O, then |a| > n for every n ∈ N, so |a−1 | < 1 and hence a−1 ∈ O. For a ∈ R, write a+ := max{a, 0}, and interpret the weak scalar primitives by σ(a) = ρ(a) = ξ(a) := a+ .
29
Then R = (R; σ, ρ, ξ) satisfies TwP . Indeed, the sign axioms for ξ and σ are immediate; if a, b ≥ 0, then σ(ab) = ab = σ(a)σ(b), and if a ≥ 0, then ρ(a) = a ≥ 0 and σ(ρ(a)) = a. Let X := {∗}, and identify A := O with the corresponding ring of constant functions X → R. Axiom (A0) holds because O is a unital subring of R, while (A2) holds because 0 ≤ a+ ≤ |a| for every a ∈ O and O is convex. If a ∈ O is nonnegative, then σ(a) = a ∈ O,
ρ(a)ξ(a) = a2 ∈ O,
so (A3w) holds. For (A4w), totalized inversion gives, for every a ∈ O, ( −1, a < 0, ξ(−a)a−1 = 0, a ≥ 0, which belongs to O. It remains to check (A5w). Let g, h ∈ O satisfy the singleton version of its side condition, namely h ≥ 0 ⇒ g ≥ 0, and set E := ξ(g 2 )ξ(g + 4h)(g + h)−1 = g 2 (g + 4h)+ (g + h)−1 . If g + 4h ≤ 0, then E = 0. Suppose g + 4h > 0. If h ≥ 0, then g ≥ 0 by the side condition; if h < 0, then g > −4h > 0. Thus g ≥ 0. When g = 0 we again have E = 0. When g > 0, either h ≥ 0, in which case g + h ≥ g, or h < 0, in which case g + 4h > 0 gives h > −g/4. In either case, 3 g + h ≥ g > 0. 4 Consequently, g 2 (g + 4h) 4 0≤E= ≤ g(g + 4h). g+h 3 The right-hand side belongs to O, and convexity of O therefore gives E ∈ O. Hence (A5w) holds, so A satisfies (AwP). Finally, choose H ∈ R with H > n for every n ∈ N, and set ε := H −1 . Then 0 < ε < 1, so ε ∈ O, whereas ε−1 = H ∈ / O. Thus the positive constant function ε lies in A but its reciprocal does not, and (A1) fails. □ Appendix D. Function-algebra criteria and examples This appendix verifies the closure axioms in increasingly structured settings. We begin with the full definable-function algebra because it shows most directly that any scalar primitives satisfying the scalar theories can be used. We then turn to continuous algebras, the real and rational examples, and finally Fischer’s definable C r setting. D.1. Arbitrary definable primitives. Fix any interpretations of σ, ρ, ξ, δ, ν on an ordered field R that make the scalar expansion a model of TwP and TsP . Let L contain the ordered-field language together with symbols for those chosen primitives, let R be the resulting L-structure, let X ⊆ Rn be a nonempty definable set, and let A be the collection of all definable functions X → R. Corollary D.1. The algebra A satisfies axioms (AsP) and (AwP). Proof. Every expression required by an algebra axiom is obtained from functions in A by composing them with one of the named scalar primitives or with an ordered-field operation. Such compositions are definable. The side conditions in (A1), (A3s), (A4s), (Aν), and (A5w) specify when the 30
corresponding definable expression is used; they do not alter definability. Hence every required function belongs to A. □ Thus any primitive choices satisfying the scalar theories may be used, including discontinuous choices such as the binary step function for ξ. The scalar axioms must hold, and the algebra considered here is the full definable-function algebra in the expanded structure. Example D.2 (o-minimal structures). If the expanded scalar structure is o-minimal, every definable function is piecewise C r for each fixed r ∈ N by C r -cell decomposition [10, Theorem 7.3]. Discontinuous definable primitives, including the binary step function, are permitted. Example D.3 (All functions). In the maximal expansion that names every subset of every finite Cartesian power of R, the graph of every function X → R is definable. Thus A = RX . D.2. Continuous-function algebras. In this subsection we ask the question: How much freedom do we have in choosing σ, ρ, ξ, δ, ν in the case of C 0 (X, R) examples? As an answer we provide sufficient conditions in Corollaries D.6 and D.11 below; this yields Proposition 5.2 above as a special case when R = R and X = U ⊆ Rn is open. In this subsection, fix a scalar model R = (R; . . .) |= ToF . We equip R with the order topology, products Rn with the product topology, and subsets X ⊆ Rn with the subspace topology. Note that the functions − : R → R, +, · : R2 → R, and (·)−1 : R̸= → R are continuous. Given −∞ ≤ a < b ≤ +∞ from R±∞ , define the open interval: (a, b) := {x ∈ R : a < x < b} ⊆ R We also put |a| := max(a, −a) for a ∈ R. In the rest of this subsection, we fix an arbitrary topological space X, and fix the algebra A = C 0 (X, R) of all continuous functions X → R. The following well-known fact about composition of continuous functions is key to transforming questions about membership in A into questions about functions on R: Lemma D.4. Let Y ⊆ Rm , let H : Y → R be continuous, and let f1 , . . . , fm ∈ C 0 (X, R) be such that (f1 (x), . . . , fm (x)) ∈ Y for every x ∈ X. Then the map: H(f1 , . . . , fm ) : X → R,
x 7→ H(f1 , . . . , fm )(x) := H(f1 (x), . . . , fm (x))
belongs to C 0 (X, R). The next lemma is the key for axiom (A4s). Define the set: S := {(x, y) ∈ R2 : if x ≥ 0, then y ̸= 0} ⊆ R2 Define a function Ψ = Ψξ as follows: Ψ : S → R,
ξ(x) y (x, y) 7→ Ψ(x, y) := 0
if y ̸= 0 if y = 0
Lemma D.5. Suppose ξ : R → R satisfies (Tξ1) and (Tξ2). If ξ is continuous, then Ψ is continuous. Proof. Let (x0 , y0 ) ∈ S be arbitrary. We show that Ψ is continuous at (x0 , y0 ). There are two cases. Case 1: (y0 = ̸ 0) Since (x, y) 7→ y is continuous, there is an open neighbourhood U of (x0 , y0 ) in R2 such that y ̸= 0 for all (x, y) ∈ U . On U ∩ S we have Ψ(x, y) = 31
ξ(x) y
Now (x, y) 7→ x is continuous, ξ is continuous by assumption, and inversion is continuous on R̸= . Hence Ψ is continuous on U ∩ S, in particular at (x0 , y0 ). Case 2: (y0 = 0) We have x0 < 0 by definition of S. Since (x, y) 7→ x is continuous, there is an open neighbourhood U of (x0 , y0 ) in R2 such that x < 0 for all (x, y) ∈ U . By (Tξ1) and (Tξ2), we have ξ(x) = 0 whenever x ≤ 0. Hence ξ(x) = 0 for all (x, y) ∈ U , and therefore Ψ = 0 on U ∩ S. In particular, Ψ is continuous at (x0 , y0 ). □ Corollary D.6. Expand R to a model of TsP such that: (1) ξ : R → R is continuous, (2) the restrictions of σ and ρ to (0, +∞) are continuous, (3) δ : R → R is continuous, and (4) ν : Dν → R is continuous, where Dν := {(a, b) ∈ R2 : if a ≤ 0, then b > 0}. Then the algebra A = C 0 (X, R) satisfies the axioms (AsP). Proof. Let f, g ∈ A be arbitrary. We will use Lemma D.4 in each of the following. (A0) Since 0, 1, −, +, · are continuous on R, it follows that 0, 1, −f, f + g, f · g ∈ A. (A1) If f > 0 on X, then since (·)−1 : R̸= → R is continuous, it follows that f −1 ∈ A. (A2) By assumption ξ : R → R is continuous. Thus ξ(f ) ∈ A. (A3s) By assumption σ, ρ are continuous on (0, +∞). Thus if f > 0 on X, then σ(f ), ρ(f ) ∈ A. (A4s) Suppose {f ≥ 0} ⊆ {g ̸= 0}. Then we have (f (x), g(x)) ∈ S for every x ∈ X. By assumption ξ : R → R is continuous, and so by Lemma D.5 the function Ψξ : S → R is continuous; thus the function Ψξ (f, g) = ξ(f ) · g −1 lies in A. (Aδ) By assumption δ : R → R is continuous, thus δ(f ) ∈ A. (Aν) Assume {f ≤ 0} ⊆ {g > 0}. Then (f (x), g(x)) ∈ Dν for all x ∈ X. Since ν : Dν → R is continuous by assumption, it follows that ν(f, g) ∈ A. □ For the weak case, we introduce the following asymptotic relation on functions R → R: Definition D.7. Suppose f, g : R → R. We say f is strictly dominated by g at 0+ (notation: f ≺ g at 0+ ) if for every ε ∈ (0, +∞), there exists δ ∈ (0, +∞) such that |f (t)| < ε|g(t)| for every t ∈ (0, δ). Our next lemma is helpful for axiom (A4w). First define a function Θ = Θξ as follows: ξ(−x) if x ̸= 0 Θ : R → R, x 7→ Θ(x) := x 0 if x = 0 Lemma D.8. Suppose ξ : R → R satisfies (Tξ1) and (Tξ2). If ξ is continuous, then (1) Θ is continuous on R̸= , and (2) Θ is continuous on R if and only if ξ(t) ≺ t at 0+ . Proof. Assume ξ is continuous. is continuous on R̸= . (1) Since inversion is continuous on R̸= , the function x 7→ ξ(−x) x (2) (⇒) Since Θ(0) = 0 and Θ is continuous at 0, for every ε > 0 there exists δ > 0 such that |x| < δ
⇒
|Θ(x)| < ε
Let t ∈ R satisfy 0 < t < δ. Then | − t| < δ, so |Θ(−t)| < ε. But Θ(−t) =
ξ(t) ξ(t) = − −t t
and since ξ(t) ≥ 0 by (Tξ1), this gives: ξ(t) = |Θ(−t)| < ε t 32
Thus ξ(t) < εt, proving ξ(t) ≺ t at 0+ . (⇐) Now additionally assume ξ(t) ≺ t at 0+ . By (1) it remains to prove that Θ is continuous at 0. Let ε > 0 be arbitrary. Since ξ(t) ≺ t at 0+ , there exists δ > 0 such that: ⇒
0 < t < δ
ξ(t) < εt
Let x ∈ R satisfy |x| < δ. It suffices to show |Θ(x)| < ε. If x = 0, then Θ(x) = 0, so we are done. If x > 0, then −x < 0, so by (Tξ1) and (Tξ2) we have ξ(−x) = 0. Hence Θ(x) = 0 and we are done. Now suppose x < 0, then t := −x satisfies 0 < t < δ, so ξ(−x) = ξ(t) < εt = ε(−x) Since x < 0, dividing by −x gives: |Θ(x)| =
ξ(−x) x
=
ξ(−x) < ε −x
□
For axiom (A5w), define the following set and function. Define the set: Q := {(x, y) ∈ R2 : if y ≥ 0, then x ≥ 0} ⊆ R2 Given ξ : R → R, define a function Φ = Φξ as follows: Φ : Q → R,
ξ(x + 4y) x+y (x, y) 7→ Φ(x, y) := 0
if x + y ̸= 0 if x + y = 0
Proposition D.9. Suppose ξ : R → R satisfies (Tξ1) and (Tξ2). If ξ is continuous, then (1) Φ is continuous on Q \ {(0, 0)}, and (2) Φ is continuous on Q if and only if ξ(t) ≺ t at 0+ . Proof. Assume ξ is continuous. (1) Let (x0 , y0 ) ∈ Q \ {(0, 0)} be arbitrary. We will show that Φ is continuous at (x0 , y0 ). There are two cases. Case 1: (x0 + y0 = ̸ 0) Since (x, y) 7→ x + y is continuous, there is an open neighbourhood U of (x0 , y0 ) in R2 such that x + y ̸= 0 for every (x, y) ∈ U . On U ∩ Q we therefore have ξ(x + 4y) x+y Now (x, y) 7→ x + 4y is continuous, ξ is continuous by assumption, and inversion is continuous on R̸= . Hence Φ is continuous on U ∩ Q, in particular at (x0 , y0 ). Case 2: (x0 + y0 = 0) Then x0 = −y0 . By definition of Q, we must have y0 ≤ 0 and x0 ≥ 0. Hence y0 < 0 < x0 since (x0 , y0 ) ̸= (0, 0). We have x0 + 4y0 = −3x0 < 0. Since (x, y) 7→ x + 4y is continuous, there is an open neighbourhood U of (x0 , y0 ) in R2 such that x + 4y < 0 for all (x, y) ∈ U . Now by (Tξ1) and (Tξ2), we have ξ(x + 4y) = 0 on U , so Φ = 0 on U ∩ Q. Thus Φ is continuous at (x0 , y0 ). (2) (⇒) Assume Φ is continuous on Q, hence at (0, 0). Since Φ(0, 0) = 0, for every ε > 0 there exists δ > 0 such that whenever (x, y) ∈ Q and Φ(x, y) =
|x| < δ,
|y| < δ,
we have: |Φ(x, y)| < ε Let t ∈ R satisfy 0 < t < δ. Then (t, 0) ∈ Q, and Φ(t, 0) = 33
ξ(t) t
Indeed, t + 0 ̸= 0 and t + 4 · 0 = t. Therefore: ξ(t) = |Φ(t, 0)| < ε t where we used ξ(t) ≥ 0 by (Tξ1). Hence ξ(t) < εt for all 0 < t < δ. This proves ξ(t) ≺ t at 0+ . (⇐) Now assume ξ(t) ≺ t at 0+ . We will show that Φ is continuous at (0, 0). Let ε > 0 be arbitrary. Since ξ(t) ≺ t at 0+ , there exists δ0 > 0 such that ε 0 < t < δ0 ⇒ ξ(t) < t 4 Set δ := δ0 /8, and let (x, y) ∈ Q satisfy: |x| < δ,
|y| < δ
It suffices to show |Φ(x, y)| < ε, which we do now. If x + y = 0, then Φ(x, y) = 0 by definition, so we are done. Thus suppose x + y = ̸ 0. If ξ(x + 4y) = 0, then again Φ(x, y) = 0, so we are done. Hence we may also assume ξ(x + 4y) > 0, i.e., x + 4y > 0 by (Tξ2). We show x + y > 0. There are two cases: • If y ≥ 0, then because (x, y) ∈ Q, we have x ≥ 0, so x + y ≥ 0. Since we are assuming x + y ̸= 0, it follows that x + y > 0. • If y < 0, then also x + y > 0; indeed, if x + y ≤ 0, then x + 4y = (x + y) + 3y < 0, a contradiction. Thus x + y > 0. Next, since |x| < δ and |y| < δ, we have: 0 < x + 4y ≤ |x| + 4|y| < 5δ < 8δ = δ0 Hence by the choice of δ0 :
ε (x + 4y) 4 It remains to compare x + 4y and x + y. We claim that: ξ(x + 4y) <
x + 4y ≤ 4(x + y) Indeed: • if y ≥ 0, then x ≥ 0, so x + 4y ≤ 4x + 4y = 4(x + y) • if y < 0, then: x + 4y = (x + y) + 3y < x + y ≤ 4(x + y) Combining the above inequalities, we get: ξ(x + 4y) (ε/4)(x + 4y) (ε/4) · 4(x + y) 0 ≤ Φ(x, y) = < ≤ = ε x+y x+y x+y Thus |Φ(x, y)| < ε whenever (x, y) ∈ Q and |x|, |y| < δ. The following lemma gives full continuity of ρ on [0, +∞) from a priori weaker assumptions: Lemma D.10. Expand R to a model of TwP such that: (1) ξ is continuous, (2) the restriction σ : [0, +∞) → R is continuous at 0, and (3) t 7→ ξ(t)ρ(t) is continuous on [0, +∞). Then: 34
□
(4) for every ε > 0, there exists η > 0 such that if y ≥ ε, then σ(y) ≥ η, and (5) ρ is continuous on [0, +∞). Proof. (4) We use Lemma A.4, namely: σ(0) = 0,
σ(1) = 1,
a > 0 ⇒ σ(a) > 0
Fix ε > 0. Since σ is continuous at 0 and σ(0) = 0, there exists δ0 > 0 such that 0 ≤ z < δ0
⇒
σ(z) < 1
Set:
εδ0 and η := σ(c) 2 Since c > 0, Lemma A.4 gives η = σ(c) > 0. We claim that if y ≥ ε, then σ(y) ≥ η. Suppose not. Then for some y ≥ ε we have σ(y) < η = σ(c). Since y ≥ ε > 0, put z := c/y. Then: c c δ0 0 < z = ≤ = < δ0 y ε 2 and hence σ(z) < 1 by the choice of δ0 . On the other hand, since c > 0 and y −1 > 0, axiom (Tσ2) gives: c :=
σ(z) = σ(cy −1 ) = σ(c)σ(y −1 ) Also: 1 = σ(1) = σ(yy −1 ) = σ(y)σ(y −1 ) again by (Tσ2). Since y > 0, Lemma A.4 gives σ(y) > 0, so σ(y −1 ) = 1/σ(y). Therefore: σ(z) =
σ(c) > 1 σ(y)
contradicting σ(z) < 1. (5) We first prove continuity at 0. By Lemma A.4, we have ρ(0) = 0. Let ε > 0. By (4), choose η > 0 such that: y ≥ ε ⇒ σ(y) ≥ η We claim that: 0 ≤ t < η ⇒ ρ(t) < ε Indeed, suppose 0 ≤ t < η and ρ(t) ≥ ε. Since t ≥ 0, axiom (Tρ) gives ρ(t) ≥ 0. Applying the defining property of η to y := ρ(t) gives σ(ρ(t)) ≥ η. But by (Tσρ), σ(ρ(t)) = t, contradicting t < η. Hence ρ(t) < ε whenever 0 ≤ t < η. Since also ρ(t) ≥ 0 for t ≥ 0, this proves |ρ(t) − ρ(0)| = ρ(t) < ε for all 0 ≤ t < η. Thus ρ is continuous at 0. Now let a > 0 be arbitrary. By (Tξ2), ξ(a) > 0. Since ξ is continuous, there is a neighbourhood I ⊆ (0, +∞) of a such that ξ(t) ̸= 0 for every t ∈ I. On I we have: ρ(t) =
ξ(t)ρ(t) ξ(t)
The numerator ξ(t)ρ(t) is continuous by assumption, the denominator ξ is continuous and nonvanishing on I, and inversion is continuous on R̸= . Hence ρ is continuous at a. □ Corollary D.11. Expand R to a model of TwP such that: (1) ξ is continuous and ξ(t) ≺ t at 0+ , (2) σ is continuous on [0, +∞), and (3) t 7→ ξ(t)ρ(t) is continuous on [0, +∞). 35
Then the algebra A = C 0 (X, R) satisfies the axioms (AwP). Moreover, ρ is continuous on [0, +∞) and thus A satisfies the stronger axiom: (A3w+ ) if f ∈ A and {f ≥ 0} = X, then σ(f ), ρ(f ) ∈ A Proof. Suppose f, g, h ∈ A. We use Lemma D.4. Axioms (A0) and (A2) follow as in Corollary D.6. The same argument also proves (A1), although (A1) is not part of (AwP). (A3w) Suppose f ≥ 0 on X. By assumption the functions σ and t 7→ ρ(t) · ξ(t) are continuous on [0, +∞). Thus σ(f ), ρ(f ) · ξ(f ) ∈ A. (A4w) By assumption we have ξ : R → R is continuous and ξ(t) ≺ t at 0+ . Thus by Lemma D.8 it follows that Θ : R → R is continuous. Thus Θ(f ) = ξ(−f ) · f −1 ∈ A. (A5w) Suppose {h ≥ 0} ⊆ {g ≥ 0}; then (g(x), h(x)) ∈ Q for every x ∈ X. By Proposition D.9, the function Φ : Q → R is continuous. Hence Φ(g, h) = ξ(g + 4h) · (g + h)−1 ∈ A. Also ξ(g 2 ) ∈ A by (A0) and (A2), so multiplication in A gives ξ(g 2 ) · ξ(g + 4h) · (g + h)−1 ∈ A, as required by (A5w). Finally, Lemma D.10 implies ρ is continuous on [0, +∞). Thus if f ≥ 0 on X, then ρ(f ) ∈ A. Thus the stronger axiom (A3w+ ) holds. □ D.2.1. Some common choices of σ, ρ, ξ, δ, ν. For the remainder of this subsection, we consider common choices of σ, ρ, ξ, δ, ν available over arbitrary ordered fields and verify their basic properties. First, define the function ReLU = ReLUR on R as follows: ReLU : R → R,
x 7→ ReLU(x) := max(0, x)
The following lemma gives the corresponding scalar axioms and continuity properties: Lemma D.12. The function ReLU : R → R is continuous. Moreover, suppose s ∈ N satisfies s ≥ 1, and define the following functions R → R: ξ := ReLUs ,
σ := ReLU,
ρ := ReLU,
δ := 2 ReLU +1
Then: (1) axioms (Tξ1), (Tξ2), (Tσ1), (Tσ2), (Tρ), (Tσρ), (Tδ) all hold, (2) ξ, σ, ρ, δ are all continuous, and (3) if s ≥ 2, then ξ(t) ≺ t at 0+ . Proof. Let r := ReLU, so: ( 0 if x ≤ 0 r(x) = max(0, x) = x if x > 0 We first show that r is continuous. Let a ∈ R, there are three cases: Case 1: (a < 0) Choose δ := (−a)/2 > 0. If |x − a| < δ, then −a a x < a+δ = a+ = < 0 2 2 so r(x) = 0 = r(a). Thus r is continuous at a. Case 2: (a > 0) Choose δ := a/2 > 0. If |x − a| < δ, then a x > a−δ = > 0 2 so r(x) = x. Hence r agrees locally with the identity map near a, and thus is continuous at a.
36
Case 3: (a = 0) Given ε > 0, choose δ := ε. If |x| < δ, then either x ≤ 0, in which case r(x) = 0, or x > 0, in which case r(x) = x < δ = ε. Thus: |r(x) − r(0)| = |r(x)| < ε Thus r is continuous at 0. (1) Now we check the axioms; in the following let a range over R. (Tξ1) r(a) ≥ 0, hence ξ(a) = r(a)s ≥ 0. (Tξ2) We have ξ(a) > 0
⇔
r(a)s > 0
⇔
r(a) > 0
⇔
a > 0
Indeed, if r(a) = 0, then r(a)s = 0, while if r(a) > 0, then r(a)s > 0. (Tσ1) This is clear since σ(a) = r(a) ≥ 0. (Tσ2) Suppose a, b ≥ 0. Then ab ≥ 0, and hence: σ(ab) = r(ab) = ab = r(a)r(b) = σ(a)σ(b) (Tρ) If a ≥ 0, then ρ(a) = r(a) = a ≥ 0. (Tσρ) Moreover, if a ≥ 0 we have: σ(ρ(a)) = r(r(a)) = r(a) = a (Tδ) Since r(a) ≥ 0: δ(a) = 2r(a) + 1 > 0 If a ≥ 0, then r(a) = a, so δ(a) = 2a + 1 ≥ 2a If a < 0, then r(a) = 0, so δ(a) = 1 > 0 > 2a (2) Since constant functions, addition, and multiplication are all continuous on R, it follows that ξ, σ, ρ, δ are all continuous. (3) Assume s ≥ 2. We show that ξ(t) ≺ t at 0+ . Let ε > 0. Choose δ := ε/(1 + ε). Then δ ∈ (0, 1), and δ < ε. If 0 < t < δ, then 0 < t < 1 and t < ε. Since s − 1 ≥ 1, we have: 0 ≤ ts−1 ≤ t < ε Therefore: ξ(t) = r(t)s = ts = ts−1 t < εt We next consider the choice ν = max. in our examples: Lemma D.13. Define the function ν := max : R2 → R. Then: (1) axioms (Tν1) and (Tν2) both hold, and (2) ν is continuous. Proof. (1) Let (a, b) range over R2 . (Tν1) Suppose a > 0 or b > 0. If a > 0, then: ν(a, b) = max(a, b) ≥ a > 0 Likewise, if b > 0, then ν(a, b) > 0. (Tν2) Suppose a ≤ 0 and b > 0. Then a < b, so: ν(a, b) = max(a, b) = b In particular, ν(a, b) ≤ b. (2) It remains to prove continuity. Note that for every (x, y) we have: max(x, y) = y + ReLU(x − y) 37
□
By Lemma D.12, the ReLU function is continuous, hence so is ν = max : R2 → R.
□
In general, the function x 7→ x2 : [0, +∞) → [0, +∞) is injective but need not be surjective (e.g., R = Q); in the event that this function is surjective, we define the square root function: √ √ · : [0, +∞) → [0, +∞), x 7→ x := the unique y ∈ [0, +∞) such that y 2 = x √ and we say R is closed under square roots. If we choose to use the · function we have: √ Lemma D.14. Suppose R is closed under square roots. Then · : [0, +∞) → [0, +∞) is strictly increasing and continuous. Moreover, define the functions σ, ρ, δ, ν as follows: p p p σ(x) := x2 , ρ(x) := |x|, δ(x) := 2 1 + x2 , ν(x, y) := x2 + y 2 + x Then: (1) axioms (Tσ1), (Tσ2), (Tρ), (Tσρ), (Tδ), (Tν1), and (Tν2) all hold, (2) σ, ρ are continuous, (3) δ : R → R is continuous, and (4) ν : R2 → R is continuous. Proof. First, the square map x 7→ x2 is strictly increasing on [0, +∞); indeed, if 0 ≤ u < v, then: v 2 − u2 = (v − u)(v + u) > 0 Since R is closed under square roots, the square map [0, +∞) → [0, +∞) is strictly increasing √ bijective. Hence its inverse · is √ also strictly increasing. Next we prove continuity of ·. Let a ∈ [0, +∞). There are two cases: 2 2 Case 1: (a = 0) √ Let ε > 0 and set√η := ε > 0. If x ∈ [0, +∞) and x < η, then 0 ≤ x < ε . By monotonicity of ·, this implies 0 ≤ x < ε. Thus: √ √ | x − 0| < ε √ Case 2: (a > 0) Put b := a > 0. Let ε > 0 and set η := εb > 0. If x ∈ [0, +∞) satisfies |x − a| < η, then, using √ √ √ |x − a| = |( x)2 − b2 | = | x − b|( x + b) √ and using x + b ≥ b > 0, we obtain: √ |x − a| |x − a| ≤ < ε | x − b| = √ b x+b Hence: √ √ | x − a| < ε (1) Let a, b range over R. (Tσ1) We have σ(a) = a2 ≥ 0. (Tσ2) Note that: σ(ab) = (ab)2 = a2 b2 = σ(a)σ(b) (Tρ) If a ≥ 0, then |a| = a, so: p √ ρ(a) = |a| = a ≥ 0 (Tσρ) If a ≥ 0, then:
p √ σ(ρ(a)) = ( |a|)2 = ( a)2 = a √ (Tδ) Since 1 + a2 > 0, we have 1 + a2 > 0, and therefore: p δ(a) = 2 1 + a2 > 0
38
Also a2 ≤ 1 + a2 . Since |a| ≥ 0 and
√
1 + a2 ≥ 0, monotonicity of the square root gives: p √ 1 + a2 |a| = a2 ≤
Therefore:
p 2a ≤ 2|a| ≤ 2 1 + a2 = δ(a) (Tν1) Suppose a > 0 or b > 0. If a > 0, then: p a2 + b2 + a ≥ a > 0 ν(a, b) =
If b > 0, then a2 < a2 + b2 , so by monotonicity of the square root: p √ |a| = a2 < a2 + b 2 Hence:
p ν(a, b) = a2 + b2 + a > |a| + a ≥ 0 (Tν2) Suppose a ≤ 0 < b. Then b − a > 0. We claim that: p a2 + b2 ≤ b − a
Since both sides are nonnegative, it suffices to square. We have: since −ab ≥ 0. Hence
√
a2 + b2 ≤ (b − a)2 = a2 + b2 − 2ab a2 + b2 ≤ b − a. Therefore: p ν(a, b) = a2 + b2 + a ≤ (b − a) + a = b
Finally, the continuity assumptions in (2), (3), and (4) follow from the fact we just established that the square root function is continuous. □ D.3. The main continuous example. In this subsection we verify the claims made about the running Main Example 3.2, 3.5, 3.6, 4.2, and 4.5 as an easy consequence from the material in subsection D.2. The main example is already covered by [12]; the novelty is the axiomatic approach. First, recall that in the main example, the scalar structure is an LsP -structure: R = (R; ≤, 0, 1, −, +, ·, (·)−1 , σ, ρ, ξ, δ, ν) where: • the LoF -reduct (R; ≤, 0, 1, −, +, ·, (·)−1 ) of R is the usual ordered field of real numbers where all symbols have their usual interpretation with the convention 0−1 := 0, and • the additional function symbols in LsP \ LoF are interpreted as follows for every x, y ∈ R: p σ(x) := x2 , ρ(x) := |x|, ξ(x) := ReLU2 (x), p p δ(x) := 2 1 + x2 , ν(x, y) := x2 + y 2 + x Corollary D.15. The LsP structure R is a model of TwP and TsP . Proof. First, the LoF -reduct of R is the usual ordered field of real numbers, so R |= ToF . Next, axioms (Tξ1) and (Tξ2) follow from Lemma D.12(1). Finally, axioms (Tσ1), (Tσ2), (Tρ), (Tσρ), (Tδ), (Tν1), and (Tν2) follow from Lemma D.14(1). □ Next, we recall the algebra. Let U ⊆ Rn be an open set and define A := C 0 (U, R) to be the collection of all continuous function U → R. Corollary D.16. The algebra A = C 0 (U, R) satisfies all axioms (AsP) and (AwP). Proof. By Corollary D.15 we know that R is a model of TwP and TsP . Thus it suffices to check that all the continuity/asymptotic assumptions of Corollaries D.6 and D.11 are satisfied. However, these follow from Lemmas D.12 and D.14. □ 39
D.4. The Q-valued continuous example. In this subsection we verify the claims about the example Q = (Q; . . .) from subsection 5.3. This example is not a direct instance of the hypotheses in [12], since that construction uses a square-root primitive on the scalar field, whereas the present Q-valued instance uses primitives adapted to Q. We recall the example: first, consider the ordered field (Q; ≤, +, ·) as a model Q = (Q; . . .) of ToF in the natural way. Expand Q to an LsP -structure by interpreting the new function symbols as follows for every x, y ∈ Q: σ(x) := ReLU(x),
ρ(x) := ReLU(x),
δ(x) := 2 ReLU(x) + 1,
ξ(x) := ReLU2 (x)
ν(x, y) := max(x, y)
Corollary D.17. The LsP -structure Q is a model of TwP and TsP . Proof. First, the LoF -reduct of Q is the usual ordered field of rational numbers, so Q |= ToF . Next, axioms (Tξ1), (Tξ2), (Tσ1), (Tσ2), (Tρ), (Tσρ), and (Tδ) follow from Lemma D.12(1). Finally, axioms (Tν1) and (Tν2) follow from Lemma D.13(1). □ Now recall the algebra: equip Q with the order topology, and let X be an arbitrary topological space. Let A = C 0 (X, Q) be the collection of all continuous functions X → Q. Corollary D.18. The algebra A = C 0 (X, Q) satisfies all axioms (AsP) and (AwP). Proof. By Corollary D.17 we know that Q is a model of TwP and TsP . Thus it suffices to check that all the continuity/asymptotic assumptions of Corollaries D.6 and D.11 are satisfied. However, these follow from Lemmas D.12 and D.13. □ D.5. Fischer’s definable C r setting. We recover Fischer’s definable strict and weak theorems from the axiomatic framework, using slightly different notation from [12]. The assumptions below are stated in the form used by Fischer rather than derived from stronger background claims. Fix r ∈ N ∪ {∞} and d, k ∈ N≥1 . Let R be a real closed field, let L extend LoF , and let R be a definably complete L-expansion of R. Here “definable” means definable in R with parameters from R. If r = ∞, assume in addition that R defines a smooth exponential function, as in [12, Section 1]. These hypotheses provide the definable differential calculus used below. Fix a definable C r -manifold M ⊆ Rn and a definable index set S ⊆ Rm . By definition, a definable family of definable C r -functions M → R is a definable function: f : M ×S →R such that for each s ∈ S, the function: fs : M → R, x 7→ fs (x) := f (x, s) r is a definable C -function. We may write fs to denote either the family or the particular instance. For the rest of this subsection we fix definable families gs , f1,s , . . . , fk,s of definable C r -functions M → R. We also consider the definable set-valued map: F : S ⇒ M,
s 7→ Fs :=
\
{fi,s ≥ 0}
1≤i≤k
With this setup, we now state Fischer’s theorems (with proofs below):
40
Corollary D.19. (Definable Strict Positivstellensatz; [12, Theorem 1.1]) Suppose gs > 0 on Fs and Fs ̸= ∅ for each s. Then there exists definable families v0,s , . . . , vk,s of definable C r -functions M → R such that each vi,s is strictly positive on M , and: X 2d 2d gs = v0,s + vi,s fi,s for every s ∈ S. 1≤i≤k
Corollary D.20. (Definable Weak Positivstellensatz; [12, Theorem 1.2]) Assume in addition that M has pure dimension n. Suppose gs ≥ 0 on Fs and Fs ̸= ∅ for all s. Then there exists definable families v0,s , . . . , vk,s , ps of definable C r -functions M → R such that: X 2d 2d p2d g = v + vi,s fi,s s s 0,s 1≤i≤k
and {ps = 0} ⊆ {gs = 0} for every s ∈ S. We apply the axiomatic framework to Fischer’s theorems. First we expand R to an L ∪ LsP -structure: • The choices of σ and ρ are determined by d as follows: p σ(x) := x2d , ρ(x) := 2d |x| • The choice of ξ is determined by r. If r < ∞ then we choose: ξ(x) := ReLU2r+2 (x) and if r = ∞, then we choose: ( exp(−1/x) if x > 0 ξ(x) := 0 if x ≤ 0 • Finally we define δ, ν by: p δ(x) := 2 1 + x2 ,
ν(x, y) :=
p x2 + y 2 + x
Each of these functions σ, ρ, ξ, δ, ν is definable in the original L-structure R. Moreover, we have: Lemma D.21. The L ∪ LsP -structure R is a model of TwP and TsP . Proof. First we check the ξ-axioms. If r < ∞, then ξ = ReLU2r+2 and thus (Tξ1) and (Tξ2) are already established by Lemma D.12 with s := 2r + 2. If r = ∞, then ξ(x) = exp(−1/x) for x > 0, and = 0 otherwise. Since exp(x) > 0 for all x, we immediately get ξ(a) ≥ 0 and ξ(a) > 0 iff a > 0. Thus (Tξ1) and (Tξ2) also hold in this case as well. Next, (Tδ), (Tν1) and (Tν2) follow from Lemma D.14. It remains only to check the 2d-analogue of the σ, ρ part of Lemma D.14. This is immediate. For every a ∈ R, σ(a) = a2d ≥ 0, so (Tσ1) holds. If a, b ≥ 0, then: σ(ab) = (ab)2d = a2d b2d = σ(a)σ(b) √ √ so (Tσ2) holds. If a ≥ 0, then ρ(a) = 2d a ≥ 0, and σ(ρ(a)) = ( 2d a)2d = a. Thus (Tρ) and (Tσρ) hold as well. □ The next lemma isolates the regularity facts needed to verify axioms (A3w), (A4w), and (A5w) for Fischer’s algebra of definable C r functions. Lemma D.22 (Regularity of the auxiliary functions). Let ρ and ξ be the functions fixed above. (1) The total function U : R → R given by U (t) := ρ(t)ξ(t) is definable and C r . (2) The total function V : R → R given by V (t) := ξ(−t)t−1 , with 0−1 = 0, is definable and C r .
41
(3) If g, h : M → R are definable C r functions satisfying {h ≥ 0} ⊆ {g ≥ 0}, then Wg,h := ξ(g 2 )ξ(g + 4h)(g + h)−1 is a definable C r function on M . Proof. Definability is immediate, so only regularity at the zero sets requires verification. Suppose first that r < ∞, so ξ(t) = (t+ )2r+2 . For t > 0, U (t) = t2r+2+1/(2d) , while U (t) = 0 for t ≤ 0. Every derivative through order r on the positive half-line is a constant multiple of t2r+2+1/(2d)−j and tends to 0 as t ↓ 0. Thus the zero extension is C r . Likewise, ( −(−t)2r+1 , t < 0, V (t) = 0, t ≥ 0, which is C r . For (3), work in a local chart and write Dℓ for the ℓth derivative. Put U := {g + 4h > 0}. Away from {g + h = 0} the conclusion follows from the usual calculus rules. If a point of {g + h = 0} does not lie in the closure of U, then ξ(g + 4h), and hence Wg,h , vanishes on a neighborhood of that point. At a point of {g + h = 0} ∩ U, Lemma A.3 forces g = h = 0 and gives 3 g + h ≥ g ≥ 0 on U. 4 On U, one has ξ(g 2 ) = g 4r+4 . An induction using the product and reciprocal rules gives, for every 0 ≤ ℓ ≤ r, 4r+4 g g 4r+4−ℓ Dℓ = τℓ , g+h (g + h)ℓ+1 where τℓ is continuous (tensor-valued in local coordinates). After shrinking the chart, τℓ is bounded, and therefore 4r+4 g Dℓ ≤ Cℓ g 4r+3−2ℓ −→ 0 (0 ≤ ℓ ≤ r). g+h By the Leibniz rule, multiplication by the globally C r gate ξ(g + 4h) preserves the vanishing of every boundary derivative through order r. Extend the function and these derivatives by 0 on the singular set. Induction on the derivative order then shows that the resulting total function is C r . This is the derivative estimate used in Fischer’s proof of Theorem 1.2 [12, proof of Theorem 1.2]. Now suppose r = ∞. We use the standard flatness estimate t−N exp(−1/t) −→ 0
(t ↓ 0)
for every N : choosing an integer m > N and using exp(s) ≥ sm /m! with s = 1/t gives the claim. Every derivative of t1/(2d) exp(−1/t) for t > 0, and of exp(1/t)/t for t < 0, is a finite sum of the same exponential factor times a power of t−1 , so all one-sided derivatives tend to 0 and (1)–(2) follow. For (3), the same product-and-reciprocal induction shows that each derivative on U is a finite sum bounded near a common zero by C g −N exp(−1/g 2 ) for some N , using again g + h ≥ 3g/4. Flatness makes every such bound tend to 0. At singular points outside U the function vanishes locally, and the same derivative-by-derivative pasting argument proves smoothness. This is the smooth analogue of Fischer’s finite-order estimate. □ Next, we define X and A: X := M,
A := {h : M → R : h is a definable C r -function}
Lemma D.23. The algebra A satisfies (AsP) and (AwP). 42
Proof. (A0) The constant functions 0, 1 are definable C r . If f, g ∈ A, then −f, f + g, and f g are also definable C r by the usual calculus rules. (A1) Suppose f ∈ A and f > 0 on M . Then 1/f is definable, and since f has no zeros, the reciprocal rule shows 1/f is C r . Hence f −1 ∈ A. (A2) By construction, each ξ : R → R is a definable C r -function. Thus if f ∈ A, then ξ(f ) ∈ A. (A3s) √ Suppose f ∈ A and f > 0 on M . Then σ(f ) = f 2d ∈ A because it is polynomial in f . Also ρ(f ) = 2d f ∈ A because f takes values in (0, +∞), where t 7→ t1/2d is C r . (A4s) Follows exactly as in the continuous case since C r is a local property (cf. Lemma D.5 and Corollary D.6). 2 > 0 on M and the restriction x 7→ √x : (0, +∞) → R is C r , it (Aδ) Suppose f ∈ A. Since 1 + f p follows that δ(f ) = 2 1 + f 2 ∈ A. (Aν) If p f, g ∈ A is such that {f ≤ 0} ⊆ {g > 0}, then f 2 + g 2 > 0 on M , it likewise follows that ν(f, g) = f 2 + g 2 + f ∈ A. (A3w) If f ∈ A and f ≥ 0 on M , Lemma D.22(1) gives ρ(f )ξ(f ) = U (f ) ∈ A. Also σ(f ) = f 2d ∈ A. (A4w) Lemma D.22(2) gives ξ(−f ) · f −1 = V (f ) ∈ A. (A5w) If g, h ∈ A and {h ≥ 0} ⊆ {g ≥ 0}, Lemma D.22(3) gives ξ(g 2 )ξ(g + 4h)(g + h)−1 ∈ A.
□
Proof of Corollaries D.19 and D.20. We first prove Corollary D.19. Let t̃0 (z0 , . . . , zk ), . . . , t̃k (z0 , . . . , zk ) be the LsP -terms provided by the axiomatic Strict Positivstellensatz 4.1. For i = 0, . . . , k consider the definable function: vi := M × S → R,
(x, s) 7→ vi (x, s) := t̃i (gs (x), f1,s (x), . . . , fk,s (x))
Now let s ∈ S be arbitrary, and define vi,s : M → R by x 7→ vi (x, s). Note that we do not a priori know that vi,s is in A, i.e., is a C r -function. However we have gs > 0 on Fs by assumption. Thus by Lemmas D.21 and D.23 the collection R, A, and gs , f1,s , . . . , fk,s satisfies the assumptions of the axiomatic Strict Positivstellensatz 4.1. Thus we conclude: • each vi,s lies in A, i.e., vi,s is a definable C r -function M → R, • each vi,s is strictly positive on X = M , and • the desired positivity certificate holds: X 2d 2d gs = v0,s + vi,s fi,s 1≤i≤k
For Corollary D.20 the proof is similar. One now considers the terms t̃−1 , t̃0 , . . . , t̃k provided by the axiomatic Weak Positivstellensatz 4.4 and constructs functions p, v0 , . . . , vk : M × S → R. Joint definability follows from Remark A.2. For each fixed s, membership in the algebra A supplied by Lemmas D.21 and D.23 gives the required fiberwise C r regularity. The certificate follows, and the present construction in fact yields the stronger conclusion {ps = 0} = {gs = 0} for every s ∈ S, which implies Fischer’s published inclusion.
□
Remark D.24 (Comparison with the source theorem). Fischer’s Theorem 1.2 states {ps = 0} ⊆ {gs = 0} [12, Theorem 1.2]. We have stated that conclusion in Corollary D.20; the equality above is a strengthening furnished by the particular universal multiplier constructed here. The construction follows Fischer’s explicit differentiable-function construction and the earlier definable-function results of Acquistapace–Andradas–Broglia [1, 12].
43
Appendix E. Complexity of the universal constructions E.1. Expanded term length. We prove Proposition 7.1 by the recursive length rules below. Tables 1 and 2 retain the intermediate lengths and representative calculations, which together give enough information for a direct hand check without printing every repetitive substitution. Suppose L is a one-sorted language. Unique readability gives the following recursive definition: n X lh(zi ) = 1, lh(f t1 · · · tn ) = 1 + lh(tj ). j=1
Thus lh(0) = lh(1) = 1, unary operations add one node, and each binary operation adds one node to the lengths of its two arguments. For k ≥ 1, ! k k X X lh ti = k − 1 + lh(ti ), lh(1 + · · · + 1) = 2k − 1. | {z } i=1
i=1
k times
Lemma E.1. For k ≥ 1, the intermediate strict terms have the lengths in Table 1, and consequently the strict certificate’s right-hand side has length 72k 3 + 232k 2 + 224k + 51 = Θ(k 3 ). Proof. The recursive length rules give the entries in Table 1. Term
Length
ψ̃ ε̃i s̃i h̃ φ̃1 φ̃2 , φ̃3 φ̃ w̃ ũ t̃0 t̃i
6k − 1 8k + 7 8k + 12 8k 2 + 16k − 1 8k 2 + 16k + 10 8k 2 + 16k + 3 24k 2 + 48k + 18 72k 2 + 144k + 46 80k 2 + 160k + 49 80k 2 + 160k + 50 72k 2 + 152k + 60
Table 1. Strict intermediate term lengths. For a representative calculation, lh(ψ̃) = (k − 1) +
k X
lh(ξ(−zi )zi ) = (k − 1) + 5k = 6k − 1,
i=1
and hence lh(h̃) = (k − 1) +
k X
3 + lh(s̃i ) = 8k 2 + 16k − 1.
i=1
All other rows follow by the same substitution. Finally, ! k X lh σ(t̃0 ) + σ(t̃i )zi = 4k + 1 + lh(t̃0 ) + klh(t̃i ) i=1
= 72k 3 + 232k 2 + 224k + 51. 44
□
Lemma E.2. For k ≥ 1, the intermediate weak terms have the lengths in Table 2. Consequently the left- and right-hand sides of the weak certificate have lengths 532k + 467 = Θ(k),
707k 2 + 1370k + 649 = Θ(k 2 ),
respectively. Proof. The same recursion gives the entries in Table 2. Term
Length
h̃ φ̃1 φ̃2 , φ̃3 φ̃ q̃ ω̃1 , ω̃2 , ω̃3 ω̃ ũ ψ̃1 , Ψ̃1 ψ̃2 , Ψ̃2 ψ̃3 , Ψ̃3 t̃−1 t̃0 t̃i
7k − 1 7k + 10 7k + 3 21k + 18 35k + 31 63k + 55, 77k + 57, 70k + 66 210k + 180 252k + 215 252k + 216, 504k + 433 210k + 181, 420k + 363 35k + 32, 70k + 65 532k + 464 749k + 648 707k + 617
Table 2. Weak intermediate term lengths. Substituting these entries into the two certificate expressions gives lh(σ(t̃−1 )z0 ) = 3 + lh(t̃−1 ) = 532k + 467 and lh σ(t̃0 ) +
k X
! σ(t̃i )zi
= 4k + 1 + lh(t̃0 ) + klh(t̃i )
i=1
= 707k 2 + 1370k + 649.
□
Lemmas E.1 and E.2 prove Proposition 7.1. E.2. Shared straight-line computation graphs. Definition E.3 (Cost model). A shared straight-line computation graph is a finite directed acyclic graph with input nodes z0 , . . . , zk , constant nodes 0, 1, and operation nodes labelled by the scalar primitives −, +, ·, (·)−1 , σ, ρ, ξ, δ, ν. All requested certificate outputs are computed jointly. Syntactically identical subexpressions are represented by one node, and the value of a node may feed arbitrarily many later nodes at no additional cost. Each primitive application contributes one node; inversion is a unit-cost primitive. Finite sums and the numeral k = 1 + · · · + 1 are formed by balanced binary addition trees and may themselves be shared. Size is the total number of nodes, including inputs and constants, and depth is the maximum number of operation nodes on a directed path to an output. Proof of Proposition 7.2. In the strict construction, the balanced sums defining ψ̃ and h̃, together with the shared numeral k, use O(k) nodes and depth O(log(k + 1)). For each i, the nodes for ε̃i , s̃i , 45
and t̃i add only a constant amount once the common nodes ψ̃, h̃, φ̃, w̃, ũ are shared. The final sum is balanced. Thus the joint graph has size O(k) and depth O(log(k + 1)). The weak construction is analogous. The balanced sum h̃ and the common nodes φ̃, q̃, ω̃, ũ, ψ̃j , Ψ̃j are shared. Each t̃i adds only the individual gate ξ(−zi ) and a constant number of multiplication nodes; the final certificate sum is balanced. Hence the same size and depth bounds hold. If the input functions are already represented jointly by graphs of total size S and maximum depth D, identify their output nodes with z0 , . . . , zk . This adds the universal graph’s O(k) nodes and adds at most O(log(k + 1)) operation levels after the deepest input, giving size S + O(k) and depth D + O(log(k + 1)). □ E.3. Small-arity expansions. Appendix A.3 gives the boundary case k = 0. The following four formulae give the complete k = 1 identities after every shared subterm has been inlined. They were produced by maintained symbolic code implementing the recursive terms, with a separate check of the reported formal lengths. The code is an authoring and regression-checking tool, not a substitute for the proofs above. The formulae show the resulting literal expression trees; in the displays, division is written using the primitive inverse notation of the term language. Under the length convention of Proposition 7.1, the strict right-hand side has length 579 for k = 1, while the weak left- and right-hand sides have lengths 999 and 2726. We continue to omit k = 2: the corresponding lengths are 2003 for the strict right-hand side and 1531 and 6217 for the weak left- and right-hand sides. These numbers concern the particular universal constructions used here and are not lower bounds for all possible certificates.
46
The strict one-constraint identity, fully inlined Formal right-hand-side length: 579
g = f1 · σ(ρ((g · (f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) +g)−1 · ξ(4 · f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) + g) +(f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) + g) · (f1 )−1 ·(σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))))−1 · ξ(−f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) − g) + ξ(−f1 · g· σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))))) · (ξ(−f1 · g· σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 )))) + ξ(−f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) − g) + ξ(4 · f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) + g))−1 ) · ρ((δ(f1 ))−1 ·ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) + σ(ρ(−f1 · (g · (f1 · σ(ρ((δ(f1 ))−1 ·ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) + g)−1 · ξ(4 · f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) + g) + (f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 ·ξ(−f1 )) + ξ(−f1 ))) + g) · (f1 )−1 · (σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))))−1 · ξ(−f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) +ξ(−f1 ))) − g) + ξ(−f1 · g · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 ))+ ξ(−f1 ))))) · (ξ(−f1 · g · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 ))+ ξ(−f1 )))) + ξ(−f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 )))− g) + ξ(4 · f1 · σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) + g))−1 ·σ(ρ((δ(f1 ))−1 · ν(g, −f1 · ξ(−f1 )) + ξ(−f1 ))) + g))
Every occurrence of every shared subterm is printed again. The display is meant to be seen as a whole, not checked line by line. 47
The weak one-constraint identity, fully inlined: left-hand side Formal left-hand-side length: 999
g · σ(ρ((ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 ))))· (ξ(−f1 · g · σ(ξ(−f1 ))) + ξ(−f1 · σ(ξ(−f1 )) − g) + ξ(4 · f1 ·σ(ξ(−f1 )) + g)) · ξ(g 2 )) · ξ((ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g)+ ξ(−f1 · σ(ξ(−f1 )))) · (ξ(−f1 · g · σ(ξ(−f1 ))) + ξ(−f1 · σ(ξ(−f1 )) − g) + ξ(4 · f1 · σ(ξ(−f1 )) + g)) · ξ(g 2 )) · ξ(−f1 ·(g · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 ))))· (f1 · σ(ξ(−f1 )) + g)−1 · ξ(g 2 ) · ξ(4 · f1 · σ(ξ(−f1 )) + g)+ (f1 · σ(ξ(−f1 )) + g) · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 ·σ(ξ(−f1 )))) · (f1 )−1 · (σ(ξ(−f1 )))−1 · ξ(g 2 ) · ξ(−f1 · σ(ξ(−f1 )) − g) + (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · ξ(g 2 ) · ξ(−f1 · g · σ(ξ(−f1 )))) · σ(ξ(−f1 )) + g ·(ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 ))))· (ξ(−f1 · g · σ(ξ(−f1 ))) + ξ(−f1 · σ(ξ(−f1 )) − g) + ξ(4 · f1 ·σ(ξ(−f1 )) + g)) · ξ(g 2 )) · ξ(g · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) +ξ(−f1 · σ(ξ(−f1 )))) · (f1 · σ(ξ(−f1 )) + g)−1 · ξ(g 2 ) · ξ(4 ·f1 · σ(ξ(−f1 )) + g) + (f1 · σ(ξ(−f1 )) + g) · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 )−1 · (σ(ξ(−f1 )))−1 · ξ(g 2 ) · ξ(−f1 · σ(ξ(−f1 )) − g) + (ξ(g) · ξ(f1 ·σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · ξ(g 2 ) · ξ(−f1 · g· σ(ξ(−f1 )))))
This is the multiplier side σ(e t−1 )g. 48
The weak one-constraint identity, fully inlined: first square The σ(te0 ) summand on the right-hand side
σ(ρ(−f1 · (g · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 · σ(ξ(−f1 )) + g)−1 · ξ(g 2 ) · ξ(4 · f1 · σ(ξ(−f1 )) + g) + (f1 · σ(ξ(−f1 )) + g) · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) +g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 )−1 · (σ(ξ(−f1 )))−1 · ξ(g 2 )· ξ(−f1 · σ(ξ(−f1 )) − g) + (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 ·σ(ξ(−f1 )))) · ξ(g 2 ) · ξ(−f1 · g · σ(ξ(−f1 )))) · σ(ξ(−f1 )) + g ·(ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (ξ(−f1 ·g · σ(ξ(−f1 ))) + ξ(−f1 · σ(ξ(−f1 )) − g) + ξ(4 · f1 · σ(ξ(−f1 )) + g)) · ξ(g 2 )) · ξ((ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g)+ ξ(−f1 · σ(ξ(−f1 )))) · (ξ(−f1 · g · σ(ξ(−f1 ))) + ξ(−f1 · σ(ξ(−f1 )) − g) + ξ(4 · f1 · σ(ξ(−f1 )) + g)) · ξ(g 2 )) · ξ(−f1 · (g · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 ·σ(ξ(−f1 )) + g)−1 · ξ(g 2 ) · ξ(4 · f1 · σ(ξ(−f1 )) + g) + (f1 · σ(ξ(−f1 )) + g) · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 )−1 · (σ(ξ(−f1 )))−1 · ξ(g 2 ) · ξ(−f1 · σ(ξ(−f1 )) − g) + (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · ξ(g 2 ) · ξ(−f1 · g · σ(ξ(−f1 )))) · σ(ξ(−f1 )) + g ·(ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (ξ(−f1 ·g · σ(ξ(−f1 ))) + ξ(−f1 · σ(ξ(−f1 )) − g) + ξ(4 · f1 · σ(ξ(−f1 )) + g)) · ξ(g 2 )) · ξ(g · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g)+ ξ(−f1 · σ(ξ(−f1 )))) · (f1 · σ(ξ(−f1 )) + g)−1 · ξ(g 2 ) · ξ(4· f1 · σ(ξ(−f1 )) + g) + (f1 · σ(ξ(−f1 )) + g) · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 )−1 · (σ(ξ(−f1 )))−1 ·ξ(g 2 ) · ξ(−f1 · σ(ξ(−f1 )) − g) + (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) +ξ(−f1 · σ(ξ(−f1 )))) · ξ(g 2 ) · ξ(−f1 · g · σ(ξ(−f1 )))))
Together, the two right-hand summands have formal length 2726. 49
The weak one-constraint identity, fully inlined: constraint square The f1 σ(te1 ) summand on the right-hand side
f1 · σ(ρ(g · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) ·(f1 · σ(ξ(−f1 )) + g)−1 · ξ(g 2 ) · ξ(4 · f1 · σ(ξ(−f1 )) + g)+ (f1 · σ(ξ(−f1 )) + g) · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 )−1 · (σ(ξ(−f1 )))−1 · ξ(g 2 ) · ξ(−f1 · σ(ξ(−f1 )) − g) + (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · ξ(g 2 ) · ξ(−f1 · g · σ(ξ(−f1 )))) · ξ(−f1 )· ξ((ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (ξ(−f1 ·g · σ(ξ(−f1 ))) + ξ(−f1 · σ(ξ(−f1 )) − g) + ξ(4 · f1 · σ(ξ(−f1 )) + g)) · ξ(g 2 )) · ξ(−f1 · (g · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) +g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 · σ(ξ(−f1 )) + g)−1 · ξ(g 2 )· ξ(4 · f1 · σ(ξ(−f1 )) + g) + (f1 · σ(ξ(−f1 )) + g) · (ξ(g) · ξ(f1 ·σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 )−1 · (σ(ξ(−f1 )))−1 · ξ(g 2 ) · ξ(−f1 · σ(ξ(−f1 )) − g) + (ξ(g) · ξ(f1 ·σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · ξ(g 2 ) · ξ(−f1 · g· σ(ξ(−f1 )))) · σ(ξ(−f1 )) + g · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g)+ ξ(−f1 · σ(ξ(−f1 )))) · (ξ(−f1 · g · σ(ξ(−f1 ))) + ξ(−f1 · σ(ξ(−f1 )) − g) + ξ(4 · f1 · σ(ξ(−f1 )) + g)) · ξ(g 2 )) · ξ(g · (ξ(g) ·ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 · σ(ξ(−f1 )) + g)−1 · ξ(g 2 ) · ξ(4 · f1 · σ(ξ(−f1 )) + g) + (f1 · σ(ξ(−f1 )) + g) · (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · (f1 )−1 · (σ(ξ(−f1 )))−1 · ξ(g 2 ) · ξ(−f1 · σ(ξ(−f1 )) − g) + (ξ(g) · ξ(f1 · σ(ξ(−f1 )) + g) + ξ(−f1 · σ(ξ(−f1 )))) · ξ(g 2 ) · ξ(−f1 · g · σ(ξ(−f1 )))))
The repeated structure is precisely what the shared straight-line graph reuses. 50
References [1] Francesca Acquistapace, Carlos Andradas, and Fabrizio Broglia. The Positivstellensatz for definable functions on o-minimal structures. Illinois Journal of Mathematics, 46(3):685–693, 2002. doi: 10.1215/ijm/1258130979. URL https://doi.org/10.1215/ijm/1258130979. [2] Matthias Aschenbrenner, Lou van den Dries, and Joris van der Hoeven. Asymptotic differential algebra and model theory of transseries, volume 195 of Annals of Mathematics Studies. Princeton University Press, Princeton, NJ, 2017. ISBN 978-0-691-17543-0. doi: 10.1515/9781400885411. URL https://doi.org/10.1515/9781400885411. [3] Stefan Balauca, Mark Niklas Müller, Yuhao Mao, Maximilian Baader, Marc Fischer, and Martin Vechev. Gaussian loss smoothing enables certified training with tight convex relaxations. Transactions on Machine Learning Research, 2025. [4] N. H. Bingham, C. M. Goldie, and J. L. Teugels. Regular variation, volume 27 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 1987. ISBN 0-521-30787-2. doi: 10.1017/CBO9780511721434. URL https://doi.org/10.1017/ CBO9780511721434. [5] Tong Chen, Jean B Lasserre, Victor Magron, and Edouard Pauwels. Semialgebraic optimization for lipschitz constants of relu networks. In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems, volume 33, pages 19189–19200. Curran Associates, Inc., 2020. URL https://proceedings.neurips.cc/paper_ files/paper/2020/file/dea9ddb25cbf2352cf4dec30222a02a5-Paper.pdf. [6] Tong Chen, Jean B. Lasserre, Victor Magron, and Edouard Pauwels. Semialgebraic representation of monotone deep equilibrium models and applications to certification. In Marc’Aurelio Ranzato, Alina Beygelzimer, Yann Dauphin, Percy S. Liang, and Jenn Wortman Vaughan, editors, Advances in Neural Information Processing Systems, volume 34, pages 27146–27159. Curran Associates, Inc., 2021. URL https://proceedings.neurips.cc/paper_files/paper/2021/ file/e3b21256183cf7c2c7a66be163579d37-Paper.pdf. [7] Susanna F. De Rezende, Noah Fleming, Duri Andrea Janett, Jakob Nordström, and Shuo Pang. Truly supercritical trade-offs for resolution, cutting planes, monotone circuits, and Weisfeiler–Leman. In Proceedings of the 57th Annual ACM Symposium on Theory of Computing, pages 1371–1382. Association for Computing Machinery, 2025. doi: 10.1145/3717823.3718271. URL https://doi.org/10.1145/3717823.3718271. [8] Santanu S Dey, Yatharth Dubey, and Marco Molinaro. Lower bounds on the size of general branch-and-bound trees. Mathematical Programming, 198(1):539–559, 2023. [9] Si Tiep Dinh and Tien Son Pham. Representations of nonnegative functions and global optimality conditions. Optimization, 2026. doi: 10.1080/02331934.2026.2684634. URL https://doi.org/ 10.1080/02331934.2026.2684634. Published online 10 June 2026; preprint arXiv:2105.08278. [10] Lou van den Dries. Tame topology and o-minimal structures, volume 248 of London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge, 1998. ISBN 0-521-59838-9. doi: 10.1017/CBO9780511525919. [11] Cynthia Dwork, Moritz Hardt, Toniann Pitassi, Omer Reingold, and Richard Zemel. Fairness through awareness. In Proceedings of the 3rd innovations in theoretical computer science conference, pages 214–226, 2012. [12] Andreas Fischer. Positivstellensätze for differentiable functions. Positivity, 15(2):297–307, 2011. ISSN 1385-1292,1572-9281. doi: 10.1007/s11117-010-0077-5. URL https://doi.org/10.1007/ s11117-010-0077-5. [13] Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson. On the power and limitations of branch and cut. In Valentine Kabanets, editor, 36th Computational Complexity Conference (CCC 2021), volume 200 of 51
Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1–6:30, Dagstuhl, Germany, 2021. Schloss Dagstuhl–Leibniz-Zentrum für Informatik. doi: 10.4230/LIPIcs.CCC.2021.6. URL https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.6. [14] José M. Gamboa. A positivstellensatz for rings of continuous functions. Journal of Pure and Applied Algebra, 45(3):211–212, 1987. doi: 10.1016/0022-4049(87)90070-3. URL https: //doi.org/10.1016/0022-4049(87)90070-3. [15] Joey Huchette, Gonzalo Muñoz, Thiago Serra, and Calvin Tsay. When deep learning meets polyhedral theory: A survey. INFORMS Journal on Computing, 2026. doi: 10.1287/ijoc.2024. 0902. URL https://doi.org/10.1287/ijoc.2024.0902. Published online March 12, 2026. [16] Christopher Jung, Michael Kearns, Seth Neel, Aaron Roth, Logan Stapleton, and Zhiwei Steven Wu. An algorithmic framework for fairness elicitation. arXiv preprint arXiv:1905.10660, 2019. [17] Andrii Kliachkin, Jana Lepšová, Gilles Bareilles, and Jakub Mareček. Benchmarking stochastic approximation algorithms for fairness-constrained training of deep neural networks. In The Fourteenth International Conference on Learning Representations, 2026. URL https: //openreview.net/forum?id=JxmjzC6syB. [18] J.-L. Krivine. Anneaux préordonnés. J. Analyse Math., 12:307–326, 1964. ISSN 0021-7670,15658538. doi: 10.1007/BF02807438. URL https://doi.org/10.1007/BF02807438. [19] Vladimír Kunc and Jiří Kléma. Three decades of activations: A comprehensive survey of 400 activation functions for neural networks. arXiv preprint arXiv:2402.09092, 2024. [20] Jean B. Lasserre and Mihai Putinar. Positivity and optimization for semi-algebraic functions. SIAM Journal on Optimization, 20(6):3364–3383, 2010. doi: 10.1137/090775221. URL https: //doi.org/10.1137/090775221. [21] Ngoc Hoang Anh Mai, Victor Magron, Jean-Bernard Lasserre, and Kim-Chuan Toh. Tractable hierarchies of convex relaxations for polynomial optimization on the nonnegative orthant. Computational Optimization and Applications, 94(3):851–905, 2026. doi: 10.1007/s10589-026-00782-4. URL https://doi.org/10.1007/s10589-026-00782-4. [22] Yuhao Mao, Yani Zhang, and Martin Vechev. Expressiveness of multi-neuron convex relaxations in neural network certification. In The Fourteenth International Conference on Learning Representations, 2026. URL https://openreview.net/forum?id=f07Kf4pD0f. [23] Murray Marshall and Tim Netzer. Positivstellensätze for real function algebras. Mathematische Zeitschrift, 270(3–4):889–901, 2012. doi: 10.1007/s00209-010-0831-1. URL https://doi.org/ 10.1007/s00209-010-0831-1. [24] Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. Prima: general and precise neural network certification via scalable convex hull approximations. Proc. ACM Program. Lang., 6(POPL), January 2022. doi: 10.1145/3498704. URL https: //doi.org/10.1145/3498704. [25] Alessandro De Palma, Rudy R Bunel, Krishnamurthy Dj Dvijotham, M. Pawan Kumar, Robert Stanforth, and Alessio Lomuscio. Expressive losses for verified robustness via convex combinations. In The Twelfth International Conference on Learning Representations, 2024. URL https://openreview.net/forum?id=mzyZ4wzKlM. [26] P. M. Pardalos and G. Schnitger. Checking local optimality in constrained quadratic programming is NP-hard. Operations Research Letters, 7(1):33–35, February 1988. doi: 10.1016/0167-6377(88)90049-1. URL https://doi.org/10.1016/0167-6377(88)90049-1. [27] Detlef Plump. Term graph rewriting. Handbook Of Graph Grammars And Computing By Graph Transformation: Volume 2: Applications, Languages and Tools, pages 3–61, 1999. [28] Mihai Putinar. Positive polynomials on compact semi-algebraic sets. Indiana Univ. Math. J., 42(3):969–984, 1993. ISSN 0022-2518,1943-5258. doi: 10.1512/iumj.1993.42.42045. URL https://doi.org/10.1512/iumj.1993.42.42045. 52
[29] Claus Scheiderer. A course in real algebraic geometry—positivity and sums of squares, volume 303 of Graduate Texts in Mathematics. Springer, Cham, 2024. ISBN 978-3-031-692123; 978-3-031-69213-0. doi: 10.1007/978-3-031-69213-0. URL https://doi.org/10.1007/ 978-3-031-69213-0. [30] Konrad Schmüdgen. The K-moment problem for compact semi-algebraic sets. Math. Ann., 289(2):203–206, 1991. ISSN 0025-5831,1432-1807. doi: 10.1007/BF01446568. URL https: //doi.org/10.1007/BF01446568. [31] Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 31. Curran Associates, Inc., 2018. URL https://proceedings.neurips.cc/paper_ files/paper/2018/file/f2f446980d8e971ef3da97af089481c3-Paper.pdf. [32] Gilbert Stengle. A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann., 207:87–97, 1974. ISSN 0025-5831,1432-1807. doi: 10.1007/BF01362149. URL https: //doi.org/10.1007/BF01362149. [33] Jie Wang, Victor Magron, and Jean-Bernard Lasserre. Chordal-tssos: a moment-sos hierarchy that exploits term sparsity with chordal extension. SIAM Journal on optimization, 31(1): 114–141, 2021. [34] Zi Wang, Bin Hu, Aaron J Havens, Alexandre Araujo, Yang Zheng, Yudong Chen, and Somesh Jha. On the scalability and memory efficiency of semidefinite programs for lipschitz constant estimation of neural networks. In The Twelfth International Conference on Learning Representations, 2024. [35] Anton Xue, Lars Lindemann, Alexander Robey, Hamed Hassani, George J Pappas, and Rajeev Alur. Chordal sparsity for Lipschitz constant estimation of deep neural networks. In 2022 IEEE 61st Conference on Decision and Control (CDC), pages 3389–3396. IEEE, 2022. [36] Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. General cutting planes for bound-propagation-based neural network verification. In S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems, volume 35, pages 1656–1670. Curran Associates, Inc., 2022. URL https://proceedings.neurips.cc/paper_files/paper/2022/ file/0b06c8673ebb453e5e468f7743d8f54e-Paper-Conference.pdf. (Nayoon Kim, Allen Gehret, Shenyuan Ma, and Jakub Mareček) Czech Technical University in Prague, Artificial Intelligence Center, Charles Square 13, Prague 2, Czech Republic Email address, Nayoon Kim, corresponding author: [email protected]
53