Verification record · AUDIT-DS-PRACTICAL-CERTIFIED-SOLVER
Publication-grade audit of the DS19 tilt-DP certificate complex
Verification recordpublication: internalno direct precedent found
Statement
Independent adversarial audit of OPEN-DS-PRACTICAL-CERTIFIED-SOLVER and its DS19 components. Verdict: DS-TILT-DUAL-CERTIFICATE verified with hardened assumptions; DS-TILT-DUAL-STRONG-DUALITY-FAILS verified with corrected minimality wording; DS-STRIP-DP-DELTA-CONSISTENCY verified; DS-MATRIX-TILT-NONQUASICONVEX verified; the DS19 clauses of DS-PROFILED-COMPILE-CERTIFICATE verified with a tie-mask caveat; the umbrella remains reduced, with a narrower remainder. Hardenings: (H1) the tie lemma -- at a fixed tilt an optimal labeling exists in which every group of equal tilted values is wholly in one cell or split only among pure-tied cells, so the interval DP value is tie-order independent and O(KN^2) (O(KN) after sorting) holds with ties; (H2) the saddle gate is set-valued, and a deterministic DP tie policy can return a non-closing member of D(beta*) even when the bracket closes (CE-DS-TILT-DUAL-TIE-MASK-001), so a reported open interval is not a gap certificate; (H3) the certified-epsilon bracket's bit model is made explicit (singleton-versus-rest coercivity radius, cutting-plane LP lower certificate, rounding discipline); (H4) support minimality holds for K=3 only -- CE-DS-TILT-DUAL-GAP-002 (N=3, K=2, gap 1/6, exact d=1/2) is the overall minimum -- and the exact dual minimum of fixture 001 is 44729/4232 at beta*=-8/23 (exact gap 534361/781333); (H5) zero-weight rows are excluded and the collapsed-atom versus unrestricted-row domain is named. Scope widened: at d_lambda=1 the exact dual minimizer is computable in polynomial bit complexity for every K by root-separation bisection on the one-sided DP derivatives (audit proof, implemented and certified on every catalogue table); for fixed d_lambda>=2 and variable K exact minimisation is arithmetic-polynomial by Toledo (1993) parametric search. Independent falsification: 125,491 canonical partitions with zero weak-duality, DS11, contiguity or refinement violations; closure iff saddle on 54/54 exact-d tables; 184 tie orders; 12 exact DS18 samples up to N=4096 with the Delta identity and disagreement bound exact; Tier B rebuilt from raw rows.
Assumptions
source frozen at research-ds-practical-certified-solver@2c9cb77 with the study handoff at 0564f03
the independent instrument py/audit_ds_practical_certified_solver.py does not import, extend or translate py/ds_practical_certified_solver.py and does not import the scorequant library; every claim-relevant quantity is fractions.Fraction, quadratic irrationals are exact in Q(sqrt D)
the audit does not re-prove the audited DS11 and DS18 nodes or DS8; it checks that DS19 uses them inside their registered hypotheses
Toledo (1993) is cited for the fixed-d_lambda variable-K arithmetic-complexity statement from its primary text; its bit complexity is not claimed
no src/, public API, example, benchmark or compile-path change is authorized by this audit
independent publication-grade verification and hardening of the DS19 certificate complex; authorizes removal of the 'unaudited' warnings, not a compile path
Where it stops
Verified does not mean deployable: a closed regular saddle certifies finite globality of the exhibited labeling only; an open reported bracket certifies nothing about the gap; the primal side of the bracket can sit far below the global value; no held-out or population statement is made outside the named DS18 law.
Refuted by
- CE-DS-TILT-DUAL-GAP-002
The scalar-POI tilt-dual duality gap needs N>=4 (support minimality of CE-DS-TILT-DUAL-GAP-001 across all K). FALSE: at N=3, K=2 the exact dual minimum strictly exceeds the exact global profiled value, and N=3 is the smallest support at which any exact-K>=2 problem has more than one labeling.
- CE-DS-TILT-DUAL-TIE-MASK-001
A deterministic tilt-DP implementation that reports an open bracket [Phi^+(z_DP), d] has exhibited a duality gap. FALSE: the bracket closes exactly (g^+ = d) but the DP-optimal set at the dual minimizer contains a non-closing labeling, which a deterministic tie policy can return.
Bounded by
- CE-DS-TILT-DUAL-GAP-001
The scalar-interest tilt-dual bracket is always exact: min_beta max_z between(S_psi-beta S_lambda; z) equals the exact global profiled-Ds value. FALSE: two explicit tilt quadratics give a rational lower certificate strictly above the exhaustive global optimum.
- CE-DS-MATRIX-TILT-NONQUASICONVEX-001
For d_psi > 1, the outer matrix-tilt ceiling B -> max_z log det V_z(B) is convex or at least quasiconvex merely because every V_z is matrix-convex and log det is monotone.
Closest prior work
- Li, Mathias (2000)Extremal Characterizations of the Schur Complement and Resulting Inequalities
- Silvey, Titterington (1973)A Geometric Approach to Optimal Design Theory
- Pukelsheim, Titterington (1983)General Differential and Lagrangian Theory for Optimal Experimental Design
- Fisher (1958)On Grouping for Maximum Homogeneity
- Wang, Song (2011)Ckmeans.1d.dp: Optimal k-means Clustering in One Dimension by Dynamic Programming
- Grønlund (2017)Fast Exact k-Means, k-Medians and Bregman Divergence Clustering in 1D
- Megiddo (1983)Applying Parallel Computation Algorithms in the Design of Serial Algorithms
- Toledo (1993)Maximizing Non-Linear Concave Functions in Fixed Dimension
- Carstensen (1983)Complexity of some parametric integer and network programming problems
- Gajjar, Radhakrishnan (2019)Parametric Shortest Paths in Planar Graphs
- Pollard (1981)Strong Consistency of K-Means Clustering
Why each source is not this result: the search records
Nearest sources, checked 2 September 2026
Relationships
Evidence references
Reviewed inputs and supporting evidence; these are not proof prerequisites.
- Best practical Ds solver with theorem-backed certificateOPEN-DS-PRACTICAL-CERTIFIED-SOLVER
- Scalar-POI tilt-DP gives a valid two-sided certificate with an exact saddle closure gateDS-TILT-DUAL-CERTIFICATE
- The scalar-POI tilt dual can have an order-one strong-duality gapDS-TILT-DUAL-STRONG-DUALITY-FAILS
- The beta-zero strip DP is value-consistent on the exact DS18 lawDS-STRIP-DP-DELTA-CONSISTENCY
- The multivariate-POI matrix-tilt outer ceiling need not be quasiconvexDS-MATRIX-TILT-NONQUASICONVEX
- Profiled compile verdict is selected by an observable certificate stateDS-PROFILED-COMPILE-CERTIFICATE
- Exact bit complexity of the variable-dimension tilt-DP dualOPEN-DS-TILT-DUAL-EXACT-COMPLEXITY
- Variational form of the profiled objectiveDS-PROFILED-VARIATIONAL
- Publication-grade audit of the DS18 exact off-(L) basin and empirical transferAUDIT-DS-NONCENTERED-GLOBAL-BASIN-TRANSFER