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

  • Counterexample fixtureCE-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.

  • Counterexample fixtureCE-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

  • Counterexample fixtureCE-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.

  • Counterexample fixtureCE-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

Why each source is not this result: the search records

Nearest sources, checked 2 September 2026

The full search record

Relationships

Evidence references

Reviewed inputs and supporting evidence; these are not proof prerequisites.

Open next door