When Can One Obtain Certificates of Optimality Using Positivstellensaetze?

1. Introduction

• Neural-network optimality certificates must address activation functions that are either non-semialgebraic, like sigmoid, or nonsmooth, like ReLU.Many existing certificates rely on semialgebraicity or smoothness.Source: §1 · p. 1
• The paper focuses on constructing effective Positivstellensatz certificates because classical Sätze are often nonconstructive and certificate computation remains prohibitive in practice.Fischer’s constructive Positivstellensätze for differentiable functions, inspired by the definable-function result, provide the starting point.Source: §1 · p. 1
• The axiomatic reformulation addresses Fischer’s dependence on definable C^r functions over real-closed fields and on square roots, enabling broader function algebras and fields such as Q.The framework is intended to make Fischer’s construction reusable while testing how far it extends beyond real-closed scalar fields.Source: §1 · pp. 1–2

1.1. Contributions and organization.

• The paper develops strict and weak Positivstellensätze, examples and neural-network optimality certificates, and analyses the term-length and shared-graph complexity of Fischer’s construction.Sections 3–7 establish the axioms and theorems, give examples over fields without square roots and activation variants, derive certificates, and study complexity.Source: §1.1 · p. 2

• Hilbert’s 17th problem, answered affirmatively by Artin (1927), established that nonnegative polynomials admit sums-of-squares representations using rational functions, motivating positivity certificates.Source: §2 · p. 2
• Preorderings generated by constraints provide algebraic witnesses for nonnegativity, with Krivine–Stengle certifying g ≥ 0 through a multiplier identity.The certificate has the form (g^2µ + a1)g = a2, with a1 and a2 in the generated preordering.Source: §2 · p. 2
• Schmüdgen removes the multiplier for strictly positive polynomials on compact sets, while Putinar uses an Archimedean quadratic module instead of a preordering.Source: §2 · p. 2
• Positivstellensätze extend beyond polynomial rings to continuous functions and definable Cr-functions, with Fischer adding explicit finite, uniform, smooth, and Banach-space constructions.Source: §2 · p. 2
• The present framework expresses Fischer’s construction through scalar and function-algebra axioms, making resulting terms independent of the function algebra and scalar field while leaving axiom verification instance-specific.Source: §2 · p. 3
• Other nonpolynomial approaches impose zero-set hypotheses, lift to polynomial optimization, or use hidden positivity, and are complementary to the paper’s universal closure-axiom constructions.Source: §2 · p. 3

3. Setup

• The framework takes an arbitrary space X, a scalar structure R satisfying first-order axioms, and an R-valued function algebra A closed under specified operations.Interpretations of first-order L-terms act pointwise on functions, allowing later theorems to be stated independently of a particular algebra.Source: §3 · p. 3
• The axioms require a unital commutative function ring and, where imposed, inverses of everywhere-positive functions; continuous functions satisfy both, while polynomial rings satisfy A0 but not A1.Source: §3 · pp. 3–4

3.1. The languages.

• The extended languages add auxiliary unary and binary primitives σ, ρ, ξ, δ, and ν for nonnegativity, partial inversion, activation, positivity domination, and max-like behavior.Examples include absolute value or powers for σ, square root for ρ, ReLU for ξ and δ, and max-like operations for ν.Source: §3.1 · p. 4

3.2. The scalar theories.

• The scalar theories formalize these primitives through positivity, multiplicativity, partial inversion, and max-proxy axioms extending the ordered-field theory.The real-valued structure from the main continuous-function example satisfies both the weak and strict scalar theories.Source: §3.2 · pp. 4–5

4.1. Strict Positivstellensatz.

• For every k, uniform LsP-terms yield strictly positive certificate functions under TsP and the strict algebra axioms.The terms are independent of the ordered field, algebra, objective, and constraints, and constraints are compressed before sign analysis.Source: §4.1 · pp. 5–6

4. Main results

• The continuous algebra A = C0(U, R) satisfies both the strict and weak axiom systems, so both Positivstellensätze apply to it.This is stated through the continuing main examples for the two theorems.Source: §4.1 · p. 6, §4.2 · p. 6

4.2. Weak Positivstellensatz.

• A non-Archimedean example satisfies (AwP) but not (A1), proving that full inverse closure is not implied by the remaining weak axioms.Thus (A1) is unnecessary for the weak theorem’s assumptions.Source: §4.2 · p. 6
• For every k, uniform LwP-terms produce nonnegative functions in A satisfying the weak certificate representation under TwP and (AwP).The weak axioms omit (A1), closure under inverses of all everywhere-positive functions.Source: §4.2 · p. 6
• The polynomial algebra R[X1, . . . , Xn] cannot satisfy (A2) for any ξ meeting (Tξ1)-(Tξ2), so it also fails (AwP) and the weak theorem does not apply.Applying (A2) to X1 would make ξ a polynomial function, contradicting the stated properties of ξ.Source: §4.2 · pp. 6–7

5. Examples

• The examples instantiate the Positivstellensätze of Sections 4.1 and 4.4 in several function-algebra settings.Source: §5 · p. 7

5.1. Using the binary step function as ξ.

• Arbitrary scalar primitives, including discontinuous choices such as the binary step function, yield full definable-function algebras satisfying (AsP) and (AwP) when they obey TwP and TsP.Closure of definability under composition supplies the algebra axioms.Source: §5.1 · p. 7

5.2. Alternative choices of σ, ρ, ξ, δ, ν in the main example (activation functions).

• Continuity conditions on ξ, σ, ρ, δ, and ν ensure (AsP), while weaker conditions including ξ(t)/t → 0 at 0+ ensure (AwP) for A = C0(U, R).Source: §5.2 · p. 7
• Power gates ReLUα satisfy the continuity condition for every α > 0, while the additional weak-condition requirement holds exactly when α > 1.Source: §5.2 · p. 7
• GELU, sigmoid, and softplus generate admissible choices ξ1(t) = GELU2(t), ξ2(t) = (sigmoid(t) − 1/2)2, and ξ3(t) = (softplus(t) − log 2)2 for t > 0.Source: §5.2 · p. 8, Figure 2 · p. 8

5.3. Q-valued continuous functions.

• Over the ordered field Q, with δ(x) = 2 ReLU(x) + 1 and ν(x, y) = max(x, y), the continuous-function algebra A = C0(X, Q) satisfies (AsP) and (AwP) without requiring real closure.This is an exact rational-arithmetic model rather than a model of ordinary finite-precision arithmetic.Source: §5.3 · p. 8

6. Optimality certificates and an application to neural networks

• Corollary 6.1 characterizes strict and weak lower-bound certificates through positive or nonnegative auxiliary functions under TsP/TwP and AsP/AwP.Strict certificates correspond to L < g⋆, while weak certificates correspond to L ≤ g⋆; a feasible x⋆ is globally minimizing exactly when the weak certificate holds with L = g(x⋆).Source: §6 · p. 9
• For continuous neural networks, the objective and pairwise output-consistency constraints lie in C0(R^n, R), so Corollary 6.1 certifies any feasible global minimizer using nonnegative p, t0, t1, t2.The certificate witnesses can be obtained from universal Weak Positivstellensatz terms and need not use the network’s activation functions; definable discontinuous networks can instead use the corresponding definable-function algebra.Source: §6 · p. 9

6.1. A rational-valued optimality certificate. 

• Over the non-real-closed ordered field Q, the weak construction produces p, t0, t1 ∈ A satisfying p(x)(Q(x) − 1) = t0(x) + t1(x)(x − 1) and {p = 0} = {Q − 1 = 0}.Here the feasible set is defined by x − 1 ≥ 0, and the certificate is built in the algebra of functions Q → Q definable in (Q; <, +, ·, Q).Source: §6.1 · p. 10
• The rational certificate proves Q(x) ≥ 1 for every feasible x, while x⋆ = 1 attains value 1 and is therefore a global minimizer.The identity is verified separately on the three displayed regions, with the zero set of p matching the zero set of Q − 1.Source: §6.1 · p. 10

7. Complexity analysis

• The right-hand side of 4.1 has expanded length 72k^3 + 232k^2 + 224k + 51 = Θ(k^3).Source: §7 · p. 10
• For 4.4, the left-hand term has length 532k + 467 = Θ(k), while the right-hand term has length 707k^2 + 1370k + 649 = Θ(k^2).Source: §7 · p. 10

7.1. Shared straight-line computation graphs.

• Under shared straight-line computation graphs, either strict or weak certificate has size O(k) and depth O(log(k + 1)).With jointly represented inputs of total size S and maximum depth D, the composed graph has size S + O(k) and depth D + O(log(k + 1)).Source: §7.1 · p. 11
• These graph bounds evaluate fixed universal terms but do not provide polynomial-time optimization algorithms or address smaller equivalent terms and arbitrary term equality.Local-optimality and strict-local-minimality decisions for constrained indefinite quadratic programs are NP-hard.Source: §7.1 · p. 11

8. Conclusions

• The framework yields universal strict and weak certificates from scalar and function-algebra axioms, including over non-real-closed ordered fields, with expanded strict length cubic in constraints but shared-graph size linear and depth logarithmic.These bounds concern explicit constructions, not certificate discovery, optimality, or polynomial-time optimization; the axioms do not cover R[X], and further algebraic extensions remain open.Source: §8 · p. 11

Appendix A. Universal terms and proof architecture

• Appendix A organizes the proof infrastructure around term conventions, universal constructions, common sign geometry, and scalar consequences, while Appendices B–E establish the theorems, examples, and complexity analysis.The conventions define infix operations, recursive sums, natural-number terms, powers, division notation, and associativity conventions.Source: Appendix A · p. 13, §A.1 · p. 13

A.2. Universal constructions.

• The strict and weak constructions define LsP- and LwP-terms by composing auxiliary sign, correction, gluing, regularization, and factorization terms from z=(z0,…,zk).The strict construction forms εi, si, h, φj, w, and ti, while the weak construction forms h, φj, ω, u, ψj, Ψj, and ti.Source: §A.2.1 · p. 13

A.2.2. Weak construction.

• The weak construction is uniformly evaluable on jointly definable parameterized families, although membership of each fiber in a chosen function algebra requires separate closure verification.This separates definability under composition from the algebra-specific closure checks recorded in the axiom-use map.Source: §A.2.2 · p. 14

A.3. Zero-constraint sanity check.

• The zero-constraint weak case reduces to explicit formulas for q, p, and t0 and verifies {p = 0} = {g = 0}, providing a boundary-case check on conventions and the leading multiplier.The formulas are q = ξ(g2)ξ(g)3, p = ξ(qg)ξ(q)2ρ(q), and t0 = ξ(qg)ρ(qg)ξ(q)2.Source: §A.3 · p. 14

A.4. Proof architecture and common sign geometry.

• Both proofs first compress the constraints into h and then follow parallel dependency chains through three sign gates to produce the strict or weak certificate terms.The strict chain is (g,f1,…,fk) ⇝ (ψ,εi,si) ⇝ h ⇝ (φ1,φ2,φ3,w) ⇝ (u,ti), whereas the weak chain proceeds through q, ω, and u.Source: §A.4 · p. 15
• The common sign geometry partitions X\({g=0}∩{h=0}) into U1, U2, and U3, with φ1, φ2, and φ3 detecting these regions and supplying the cover and denominator-safety estimates.Under the stronger inclusion {h ≥0} ⊆ {g > 0}, the three regions cover all of X.Source: §A.4 · p. 15
• The axiom-use map assigns non-ring closure axioms to distinct construction stages, while weak φ-cancellation shows that the corresponding steps do not require (A1).Strict stages detect constraints, correct and lift coefficients, glue sign-region formulas, and take positive roots; weak stages regularize division and factorize u, ω, and q.Source: §A.4 · p. 15

Scalar consequences

• The axioms imply σ(1)=1, ρ(0)=0, σ(0)=0, positivity of σ(a) and ρ(a) for a>0, injectivity of ρ on [0,+∞), and surjectivity of σ on [0,+∞).Source: §A.5 · p. 16

Pathologies

• The axioms do not determine whether ρ is surjective, σ is injective, or either function is monotone on [0,+∞).Source: §A.5 · p. 16

Wild σ and ρ

• Using the Axiom of Choice, the construction produces σ and ρ such that on every interval in [0,+∞), ρ is not surjective, σ is not injective, and neither function is monotone.Source: §A.5 · pp. 16–17

Proof strategy

• The proof follows Fischer’s construction by defining a sequence of functions from strict-construction LsP-terms and verifying their properties axiomatically.The construction is carried out for an ordered-field model and an algebra satisfying the stated axioms.Source: Appendix B · p. 18

Auxiliary perturbation

• Under {g ≤0} ⊆ {φ > 0}, ε = ν(g, φ)·(δ(f))^-1 belongs to A, is positive everywhere, and satisfies ε·f < φ on {g ≤0}.This is the basic auxiliary-function lemma used repeatedly in the strict construction.Source: Appendix B · p. 18

Sign-controlled construction

• The construction combines ψ and ε_i with the sign operation ξ and map ρ to obtain positive s_i and a function h whose nonnegative region lies inside {g > 0}.Lemma B.2 establishes the sign properties of ψ and ε_i, while Lemma B.3 establishes h ∈ A and {h ≥0} ⊆ {g > 0}.Source: Appendix B · pp. 19–20

Positive weights

• From g and h, the proof constructs strictly positive φ and w in A, using sign-region decompositions and axiomatic closure under the required divisions.These functions provide the weights needed for the final identity.Source: Appendix B · pp. 20–21

Certificate conclusion

• The final functions u and t_i are positive members of A, satisfy σ(t_i) = wσ(s_i), and yield the strict certificate identity summarized in the concluding calculation.The conclusion combines the weighted terms with u = g − wh to recover g.Source: Appendix B · pp. 21–22

Appendix C. Proof of the weak Positivstellensatz

• The proof builds the weak Positivstellensatz by constructing functions from the weak LwP-term sequence while verifying each required property within the axiomatic function algebra.The strategy mirrors Appendix B but checks algebra membership and pointwise properties under the weak axioms.Source: Appendix C · p. 23
• Hilbert–17 Lemma C.1 converts each nonnegative auxiliary function into paired algebra elements with σ(ψ)·f = σ(Ψ) and matching zero sets, yielding the nonnegative terms used in Corollary C.9.The three applications target u, ω, and q, producing the identities σ(ψ1)·u = σ(Ψ1), σ(ψ2)·ω = σ(Ψ2), and σ(ψ3)·q = σ(Ψ3).Source: Appendix C · pp. 23, 27, 28
• The construction produces q, ω, and u in A, each nonnegative on X with zero set exactly {g = 0}; ω additionally satisfies the case-dependent identities required for reciprocal closure.These auxiliary functions are assembled from h and φ, with ω’s membership relying on weak reciprocal-closure axioms without assuming φ^-1 ∈ A.Source: Appendix C · pp. 24, 25, 27
• With (A0), (A1), and (A2), axiom (A4w) is equivalent to the weaker axiom (A4w−), so weakening it adds no generality under reciprocal closure.The proof derives each direction using the specified closure identities and positivity of p = f^2 − f + 1.Source: Appendix C · p. 29

C.1. Independence of reciprocal closure from the weak package.

• A non-Archimedean ordered field with its finite-element valuation ring yields a function algebra satisfying (AwP) but not reciprocal closure (A1).A positive infinitesimal belongs to the ring, while its reciprocal is an infinite element outside it.Source: §C.1 · pp. 29–30

Appendix D. Function-algebra criteria and examples

• Appendix D begins by verifying closure axioms for increasingly structured function algebras, starting with full definable functions and then treating continuous, real, rational, and Fischer’s definable Cr settings.The framework fixes scalar interpretations of σ, ρ, ξ, δ, and ν satisfying the scalar theories TwP and TsP.Source: Appendix D · p. 30, §D.1 · p. 30

D.1. Arbitrary definable primitives.

• The full definable-function algebra A on a nonempty definable set X satisfies axioms (AsP) and (AwP).Required expressions remain definable because they arise by composing functions with named scalar primitives or ordered-field operations.Source: §D.1 · pp. 30–31
• Any primitive choices satisfying the scalar theories are allowed, including discontinuous primitives such as the binary step function for ξ.The scalar axioms must hold, and the algebra is the full definable-function algebra in the expanded structure.Source: §D.1 · p. 31
• In o-minimal expansions, every definable function is piecewise C^r for each fixed r ∈ N, while discontinuous definable primitives remain permitted.This follows from C^r-cell decomposition [10, Theorem 7.3].Source: §D.1 · p. 31
• In the maximal expansion naming every subset of every finite Cartesian power of R, every function X → R is definable, so A = R^X.Thus the framework includes the algebra of all functions as a special case.Source: §D.1 · p. 31

D.2. Continuous-function algebras.

• Corollary D.6 shows that C0(X, R) satisfies (AsP) when ξ and δ are continuous, σ and ρ are continuous on (0, +∞), and ν is continuous on its domain.These conditions provide sufficient freedom to choose the scalar primitives while preserving the strict axioms.Source: §D.2 · p. 32
• The auxiliary quotient constructions are continuous under ξ’s continuity, with full continuity exactly characterized by ξ(t) ≺ t at 0+ for the weak-case functions Θ and Φ.Θ is continuous on R\{0}, while Φ is continuous on Q\{(0, 0)}; each extends continuously across its singular point precisely under the same asymptotic condition.Source: §D.2 · pp. 32–33
• Lemma D.10 derives continuity of ρ on [0, +∞) from continuity of ξ, continuity of σ at 0, and continuity of t 7→ξ(t)ρ(t).The proof also establishes that every ε > 0 admits η > 0 with y ≥ ε implying σ(y) ≥ η.Source: §D.2 · pp. 34–35
• Corollary D.11 shows that, if ξ is continuous with ξ(t) ≺ t at 0+, σ is continuous on [0, +∞), and t 7→ξ(t)ρ(t) is continuous, then C0(X, R) satisfies (AwP).Because ρ is then continuous on [0, +∞), the algebra also satisfies the stronger axiom (A3w+) for functions nonnegative everywhere.Source: §D.2 · pp. 35–36
• The specified ReLU-based choices satisfy axioms (Tξ1), (Tξ2), (Tσ1), (Tσ2), (Tρ), (Tσρ), and (Tδ), are continuous, and satisfy ξ(t) ≺t at 0+ when s ≥2.The choices are ξ := ReLUs, σ := ReLU, ρ := ReLU, and δ := 2 ReLU +1.Source: §D.2 · p. 36
• When the ordered field is closed under square roots, square-root-based σ, ρ, δ, and ν satisfy the relevant scalar axioms and are continuous.The square-root function itself is strictly increasing and continuous, and ν is a continuous binary operation.Source: §D.2 · p. 38

D.3. The main continuous example.

• The main real-valued LsP-structure is a model of TwP and TsP, and A = C0(U, R) satisfies all axioms (AsP) and (AwP).Here U ⊆ R^n is open and A consists of all continuous functions U → R; the example is already covered by, while the contribution here is axiomatic.Source: §D.3 · p. 39

D.4. The Q-valued continuous example.

• The rational-valued construction adapts its primitives without square roots: Q is a model of TwP and TsP, and A = C0(X, Q) satisfies all axioms (AsP) and (AwP).This applies to Q with its order topology and arbitrary topological space X, using ReLU-based and max primitives.Source: §D.4 · p. 40

D.5. Fischer’s definable Cr setting.

• Under definable completeness, a definable C^r-manifold, and a smooth exponential when r = ∞, Fischer’s theorems apply to definable function families [12].These hypotheses provide the definable differential calculus used in the construction.Source: §D.5 · p. 40
• If gs > 0 on Fs and Fs is nonempty, definable strictly positive multipliers yield a strict Positivstellensatz certificate [12, Theorem 1.1].The certificate functions are definable C^r functions and strictly positive on M.Source: §D.5 · p. 41
• If gs ≥ 0 on Fs, Fs is nonempty, and M has pure dimension n, definable multipliers and ps yield Fischer’s weak Positivstellensatz certificate [12, Theorem 1.2].The construction additionally establishes {ps = 0} ⊆ {gs = 0}.Source: §D.5 · p. 41
• The expanded structure satisfies the scalar axioms TwP and TsP, while the auxiliary functions U and V and the gated composition preserve C^r regularity.These regularity facts are the key ingredients for verifying the weak and strict algebra axioms.Source: §D.5 · pp. 41–42
• The algebra of definable C^r functions on M satisfies both the strict and weak Positivstellensatz axioms, enabling the abstract theorems to produce fiberwise definable certificates.The universal terms are evaluated on the definable data, and each fixed-parameter fiber remains in the algebra.Source: §D.5 · pp. 42–43
• The weak construction gives the stronger equality {ps = 0} = {gs = 0}, improving Fischer’s published inclusion {ps = 0} ⊆ {gs = 0} [12, Theorem 1.2].The equality holds for every parameter s and comes from the particular universal multiplier constructed here.Source: §D.5 · p. 43

E.1. Expanded term length.

• The recursive length rules establish the strict and weak certificate sizes for arbitrary k, with intermediate terms tabulated for direct verification.Unary operations add one node, while binary operations add one node to the lengths of their arguments; Lemmas E.1 and E.2 prove Proposition 7.1.Source: §E.1 · pp. 44–45

E.2. Shared straight-line computation graphs.

• Shared straight-line graphs compute all certificate outputs jointly, reusing identical subexpressions and balanced sums under an explicit size-and-depth cost model.Each primitive application contributes one node, shared values can feed arbitrarily many later nodes, and inversion has unit cost.Source: §E.2 · p. 45
• The strict and weak constructions each achieve graph size O(k) and depth O(log(k + 1)), or size S + O(k) and depth D + O(log(k + 1)) with shared input graphs.The bounds follow because common nodes and balanced final sums are shared across all requested certificate outputs.Source: §E.2 · p. 46

E.3. Small-arity expansions.

• For k = 1, the strict right-hand side has length 579, while the weak left- and right-hand sides have lengths 999 and 2726.For k = 2, the corresponding lengths are 2003, 1531, and 6217; these are properties of the displayed universal constructions, not lower bounds for all certificates.Source: §E.3 · p. 46

The strict one-constraint identity, fully inlined

• The fully inlined strict one-constraint identity has formal right-hand-side length 579 because every occurrence of each shared subterm is printed again.The display is intended to be viewed as a whole rather than checked line by line.Source: The strict one-constraint identity,… · p. 47

The weak one-constraint identity, fully inlined: left-hand side

• The fully inlined weak one-constraint identity has a formal left-hand-side length of 999.Its displayed expression explicitly repeats the constituent operations and subterms of the weak certificate.Source: The weak one-constraint identity,… · p. 48

The weak one-constraint identity, fully inlined: first square

• The first weak-certificate square contributes to the fully expanded expression, whose two right-hand summands together have formal length 2726.The large expansion reflects repeated literal subexpressions in the displayed formula.Source: The weak one-constraint identity,… · p. 49

The weak one-constraint identity, fully inlined: constraint square

• The weak constraint square repeats the same substructure, precisely the pattern reused by the shared straight-line graph.This explicit inlining contrasts with graph representation, where repeated structure is represented once and reused.Source: The weak one-constraint identity,… · p. 50