Raise ConvexOptimization SymbolicAnalysis floor to 0.5.3 (soundness); Symbolics floor 7.40

[ChrisRackauckas-Claude]

Summary

lib/ConvexOptimization/Project.toml allowed SymbolicAnalysis = "0.3, 0.5", so resolvers can land on 0.3.7/0.3.8 (missing Mapreducer/Mapper DCP rules) or on 0.5.0–0.5.2 (still carrying September false-certificate bugs). This PR narrows compat to SymbolicAnalysis = "0.5.3".

Floor basis is SOUNDNESS, not just coverage. ConvexOptimization's nested-atom path (PR #1376) certifies the original expression with SymbolicAnalysis.analyze, so a SymbolicAnalysis release that still returns a false convexity certificate becomes a silent wrong answer. SymbolicAnalysis fixed a series of false certificates in September. By tag containment:

• Fixes for Fix three unsound certificates (exp.(x), dot(x,x), tr(X*X)) SymbolicAnalysis.jl#157, No arguments are passed to Nlopt.jl optimisers #159, Made NLopt.jl interface properly handle options & minor changes to MOI #160, Common return code #161, Harmonised interfaces and added common arguments #163, Fixed MOI warning #164 first appear in v0.5.2
• Fixes for Common interface design #162 (binary minus) and Add NLopt maxsense support #169 (restoring the / rule that v0.5.2 shipped broken) first appear in v0.5.3

So v0.5.3 is the first release with all of them. (#174 in v0.5.5 adds coverage only.)

This drops support for 0.3.x and 0.5.0–0.5.2 — a compat narrowing that warrants a minor version bump when ConvexOptimization is released.

Bisect (Julia 1.12, analyze of probe expressions)

Coverage probes (Mapreducer/Mapper gap on un-lowered expressions):

SymbolicAnalysis	sumabs	minimum	variadic min	max(abs)	Verdict
0.3.7	UnknownCurvature	UnknownCurvature	rule ERROR	UnknownCurvature	FAIL
0.3.8	UnknownCurvature	UnknownCurvature	rule ERROR	UnknownCurvature	FAIL
0.3.9	Convex	Concave	Concave	Convex	PASS (first with #120/#123)
0.5.0	Convex	Concave	Concave	Convex	PASS
0.5.1–0.5.3	Convex	Concave	Concave	Convex	PASS
0.5.6	Convex	Concave	Concave	Convex	PASS

0.3.9 is the first release that certifies these expressions, but 0.4 is a Symbolics-6 dead-end and the soundness floor above requires ≥0.5.3 on the maintained Symbolics-7 line.

Verification

Scratch env developing this checkout’s lib/ConvexOptimization, SA pinned:

export JULIA_PKG_SERVER="" TMPDIR=.../jobs/1380-cursor/tmp
julia +1.12 --project=verify-053 -e 'using Pkg; Pkg.develop(...); Pkg.add(PackageSpec(name="SymbolicAnalysis", version="0.5.3")); ...'
OPTIMIZATION_TEST_GROUP=Core julia +1.12 --project=verify-053 -e 'using Pkg; Pkg.test("ConvexOptimization")'

Core at floor (SymbolicAnalysis 0.5.3)

Status `.../verify-053/Project.toml`
⌃ [4297ee4d] SymbolicAnalysis v0.5.3
Test Summary: | Pass  Total    Time
Core          |  529    529  7m40.6s
     Testing ConvexOptimization tests passed
VERIFY_EXIT 053: 0

Earlier checks (still relevant)

• Core @ SA 0.5.0: 529/529 (coverage floor; now superseded by soundness floor)
• Core @ SA 0.5.6: 529/529
• SA 0.3.9 correctly unsatisfiable against the old "0.5" floor; 0.5.0–0.5.2 are now also out of range

Symbolics floor 7.39 → 7.40.0 (commit 82bab12)

With #1376 on master, the downgrade-sublibraries / test (lib/ConvexOptimization) lane fails at the floors with 744 passed and 2 errored, at core_tests.jl:1219 and :1445. Both errors come from scalarized norm(::Vector{Num}) expanding to sqrt(sum(abs2, …)) instead of staying a norm atom, which Symbolics 7.40.0 fixes (Symbolics PR #1992). Codex gpt-6-luna bisected this on Julia 1.10.12:

SymbolicAnalysis	Symbolics	SymbolicUtils	ConvexOptimization tests
0.5.3	7.39.2	4.46.6	744 passed, 2 errored
0.5.3	7.40.0	4.46.6	789/789
0.5.6	7.42.0	4.49.0	789/789

The SymbolicUtils entry 4.46 → 4.46.6 makes explicit the minimum that SymbolicAnalysis 0.5.3 already forces. Neither change adds or removes a dependency.

What was NOT verified

• Full GitHub Actions downgrade-sublibraries matrix (workflow file intentionally untouched; it still skips SymbolicAnalysis).
• Non-Core test groups / other sublibraries.
• Constraint-atom solve probes from ConvexOptimization: allow atoms inside <= and >= constraint components #1377 on that PR’s branch (master still requires affine-in-cone constraints; the analyze probes cover the underlying SA gap).

Compat note

Drops 0.3.x and 0.5.0–0.5.2. Treat as a compat-narrowing change; bump ConvexOptimization’s minor when releasing.

Closes #1380

Please ignore this draft until reviewed by @ChrisRackauckas.

Harness: Cursor Agent CLI 2026.09.26-dd393fe; model: auto; transcript: /home/crackauc/sandbox/agent-jobs/Optimization.jl/jobs/1380-cursor/log-fu2.txt on amdci2.julia.csail.mit.edu