Result · DS-TILT-DUAL-CERTIFICATE
A tilted dual brackets the profiled optimum
Proved here, no precedent foundindependently auditedpublication: internal
Meaning
Scalar-interest tilt dynamic programming gives two-sided bounds, with exact closure when an exhibited labelling satisfies the saddle condition.
Scientific context
For a single parameter of interest there is a two-sided certificate: a dynamic program over a tilted scalar score gives a primal value and a dual ceiling, and when a specific gate condition is met the two values coincide and certify a finite global profiled optimum.
Statement
For d_psi=1 and positive finite weights, write V_z(beta)=btw(S_psi-beta S_lambda;z) (uncentered), v_K(beta)=max_z V_z(beta), and Phi^+(z)=min_beta V_z(beta). The DP-active generalized primal p^+, generalized global value g^+, regular in-bin primal p_reg, regular global value g_reg, and dual d=min_beta v_K(beta) obey p^+ <= g^+ <= d and p_reg <= g_reg <= g^+ <= d; d is attained after quotienting the common nuisance-null space. The generalized bracket closes, p^+=g^+=d, iff some labeling z in the DP-optimal set D(beta) at some beta satisfies beta I_lambdalambda(z)=I_psilambda(z); then every Phi^+-maximiser and every dual minimiser form such a pair; if the exhibited z has a nonsingular nuisance block it is an ordinary in-bin global optimum, otherwise it certifies only the DS11 pseudo-inverse problem. Fixed-tilt exact rational evaluation of v_K, an active labeling, the exact one-sided derivatives and the primal values costs O(KN^2) rational operations (O(KN) after sorting) and tolerates exact ties in every tie order (tie lemma). A certified rational epsilon-bracket on d is computable in time polynomial in the input bits and log(1/epsilon) via an observable coercivity radius, a subgradient separation oracle and a cutting-plane LP lower certificate. Exact minimisation is polynomial in bit complexity at d_lambda=1 for every K (root-separation bisection on the one-sided DP derivatives, output rational or a degree-2 algebraic number), and polynomial in arithmetic operations for fixed d_lambda>=2 and variable K (Toledo 1993 parametric search). Exact polynomial bit complexity for fixed d_lambda>=2 with variable K, and any exact statement for variable d_lambda, is OPEN-DS-TILT-DUAL-EXACT-COMPLEXITY.
Assumptions
d_psi=1; d_lambda>=1; finite score table; strictly positive rational weights (a zero-weight row in its own cell makes V_z undefined and is excluded; a zero-weight row sharing a cell is inert); exactly K nonempty cells with N>=K
all empirical second moments are about the score-space origin; no sample centering is performed
the generalized domain uses DS11's Moore-Penrose value; the ordinary in-bin domain separately requires a nonsingular binned nuisance block; a singular DP state is a generalized lower bound only
the comparison domain (collapsed duplicate atoms or unrestricted rows) is named: D(beta) and g^+ are domain-dependent; the tie lemma makes the dual v_K identical on both domains whenever K does not exceed the atom count
the closure gate is set-valued: certification requires exhibiting a concrete DP-optimal labeling whose normal equation holds; a deterministic tie policy may return a non-closing member of D(beta*) when the bracket closes (
CE-DS-TILT-DUAL-TIE-MASK-001), so a reported open interval [Phi^+(z_DP), d] is not evidence of a duality gappolynomial certified-accuracy optimization assumes rational input and a requested rational epsilon and uses a polynomial-bit box radius from singleton-versus-rest partitions, the ellipsoid/GLS rounding discipline, and an exact LP over the collected cuts as the lower certificate
exact minimisation at d_lambda=1 returns an exact rational or quadratic-irrational tilt certified by D-(beta*)<=0<=D+(beta*); the fixed-d_lambda>=2 statement is arithmetic complexity from Toledo 1993, not a bit bound
Where it stops
Audited 2 Sep 2026 (AUDIT-DS-PRACTICAL-CERTIFIED-SOLVER): verified with hardened assumptions. The dual is a ceiling on both domains, but a singular DP state is not an in-bin lower bound. Strong duality is false by CE-DS-TILT-DUAL-GAP-001 and, support-minimally, CE-DS-TILT-DUAL-GAP-002. A reported open bracket is not a gap certificate (CE-DS-TILT-DUAL-TIE-MASK-001). The primal side p^+ can sit strictly below g^+. Crossings-plus-midpoints and epsilon-accurate convex optimization are not exact algebraic solvers. Verification authorizes no src change; compilation remains governed by DS-PROFILED-COMPILE-CERTIFICATE.
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-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.
- CE-DS-NONCENTERED-SINGULAR-DESTINATION-001
An exact global optimum over regular (nonsingular-nuisance) finite labelings is one-point exchange-stable under ANY feasibility convention, so DS18.2's finite stability step needs no convention. FALSE off the null set: on this support-minimal N=4 table from the named off-(L) law, both exact global regular optima reach the single nuisance-singular labeling by one admissible relocation whose DS11 pseudo-inverse value exceeds the regular optimum by exactly 1/96. The in-bin (DS9) convention -- singular destinations are infeasible -- is therefore load-bearing and must be named. This does not refute DS18, whose law makes such tables null.
Closest prior work
A targeted search of the literature found no direct precedent for this statement. That records a search gap, not a novelty claim; the nearest sources are named below.
- 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
- Gajjar, Radhakrishnan (2019)Parametric Shortest Paths in Planar Graphs
Relationships
Rests on
- Variational form of the profiled objectiveDS-PROFILED-VARIATIONAL
- Scalar efficient-score upper problem is exactly solvable by dynamic programmingDS-SCALAR-EFFICIENT-DP
The full chain beneath it
Enables
- Profiled compile verdict is selected by an observable certificate stateDS-PROFILED-COMPILE-CERTIFICATE
- Best practical Ds solver with theorem-backed certificateOPEN-DS-PRACTICAL-CERTIFIED-SOLVER
- Exact bit complexity of the variable-dimension tilt-DP dualOPEN-DS-TILT-DUAL-EXACT-COMPLEXITY
Raises
Verified by
Open next door
Local graph
Proof
DS19. The tilt-DP bracket: weak certification, an order-one gap, and a value-consistent DS18 primal
Independent audit (2 Sep 2026,
AUDITS/AUDIT-DS-PRACTICAL-CERTIFIED-SOLVER-001.md). Verified with
hardened assumptions (Tier A), verified (T5, Tier B), umbrella
reduced with a narrower remainder. Independent exact falsification over
125,491 canonical partitions found zero weak-duality, DS11, contiguity or
refinement violations; closure saddle held on 54/54
exact- tables. Five hardenings, folded into the text below:
(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 the
bound (in fact after sorting, Grønlund et al. 2017)
holds with ties; the frozen text asserted this without proof.
(H2) the saddle gate is set-valued: a deterministic DP tie policy can
return a non-closing member of when the bracket
closes (CE-DS-TILT-DUAL-TIE-MASK-001, , pairwise-distinct
tilted values), so a reported open interval is not a gap certificate.
(H3) the certified- bracket's bit model is explicit:
singleton-versus-rest coercivity radius, subgradient oracle, exact
cutting-plane LP lower certificate, ellipsoid/GLS rounding discipline.
(H4) "support-minimal" holds for only; the overall minimum is
CE-DS-TILT-DUAL-GAP-002 (, , , gap
); the exact dual minimum of fixture 001 is at the
rational crossing , exact gap , so the
registered mixture bound is a lower certificate, as stated.
(H5) zero-weight rows are excluded and the collapsed-atom versus
unrestricted-row domain is named. Scope widened (audit §7.5): at
the exact dual minimiser is computable in polynomial bit
complexity for every — the breakpoints are roots of degree-
polynomials of polynomial height, so a bisection on the exact one-sided DP
derivatives certifies a rational or quadratic-irrational minimiser after
polynomially many probes; for fixed and variable
exact minimisation is arithmetic-polynomial by Toledo (1993) parametric
search. The (EXACT-PARAMETRIC-DP) question below is therefore narrowed to a
polynomial bit bound for fixed and to variable
. The audit authorizes no src/ change.
Normalization (protocol A). Tier A has , arbitrary , and finite positive rational weights. All empirical second moments are about the score-space origin: scores are not sample-centered. The decision variable on the comparison side is a nonempty -cell labeling. The generalized comparison domain uses DS11's pseudo-inverse value ; the ordinary in-bin domain is its subset with a nonsingular nuisance block. For , put
Let . By scalar contiguity this value is returned by the exact interval DP after sorting . Let
For the primal, a tie policy is part of the object. If is the set of DP-optimal labelings at , define
An implementation may use one deterministic member of ; that only weakens its lower bound. (Audit H2: it can also hide a closure — the member it holds need not be the saddle even when ; an open reported interval therefore certifies nothing about the gap.) The information-loss implication is a finite train-sample value interval. It supplies no held-out or population retention statement except in the named DS18 corollary below.
Theorem DS19.1 (the valid bracket and its exact closure gate)
On the generalized domain,
On the ordinary in-bin domain,
Thus the same dual is a ceiling on the whole DS11 pseudo-inverse class and, a fortiori, on DS9. A singular DP state is a valid generalized lower bound but is not an in-bin lower bound; the regular filter in is load-bearing.
Moreover the generalized bracket closes, , iff there are such that
Equivalently, maximizes over labelings and minimizes : it is a saddle pair. If in addition , the same equality certifies as an ordinary in-bin global optimum. At a singular block only the normal equation is meaningful; no quotient slope is asserted.
Proof. DS11 gives . Hence for every ,
Taking the indicated maxima and minimum proves weak duality and both lower bounds. If a saddle pair exists, all inequalities are equalities. Conversely, if , choose a primal maximizer and a dual minimizer . Then
Thus both inequalities are equalities: is DP-optimal at , and DS11's attainment set makes satisfy exactly the displayed normal equation. The same pair also gives an attained . The finite maximum of nonnegative convex quadratics attains its infimum after quotienting directions that are null for every empirical nuisance moment. ∎
Ties and duplicate tilts. Scalar contiguity supplies the exact value even when equal tilted values are pooled (audit H1, tie lemma: each mixed cell's term is convex in the tied mass it receives, so an optimal labeling keeps every tied group in one cell or only in pure-tied cells, and every tie order yields the same DP value; the labeling active on is contiguous in the order breaking ties by decreasing ). At a crossing, different row-level refinements can have the same DP value and different derivatives. Any active derivative is a valid subgradient of , but a closure certificate must exhibit the concrete labeling whose normal equation is checked. A deterministic score-only quantizer must be constant on an exact duplicate-score class; unrestricted finite row assignment is a larger comparison domain and must be named separately.
Theorem DS19.2 (what is polynomial, and the exact-computation reduction)
For a supplied rational , , one active labeling, its exact rational gradient, and the regular/generalized primal values are computable in rational operations by sorted interval DP. The map is a finite maximum of convex quadratics, hence convex. With rational input, full empirical nuisance span, and a requested rational tolerance , a standard separation-oracle convex method therefore returns certified rational lower/upper bounds on of width in time polynomial in the input bit length and . A search radius is observable: singleton-versus-rest nuisance partitions give a positive quadratic coercivity bound on the effective nuisance span; common-null directions are first quotiented out.
Exact algebraic computation was established in the frozen proof only when and are fixed; the audit widens this (H-scope above): polynomial bit complexity at for every , and arithmetic-polynomial exact minimisation for fixed , variable (Toledo 1993). The fixed- argument follows. The tilt-order arrangement, including its tie faces, has polynomial size then; each cell has contiguous candidates, and fixed-dimensional real-algebraic comparison of their quadratic envelopes returns the exact minimum. This is not polynomial jointly in variable .
The study's requested general exact polynomial-time claim is therefore reduced to one explicit assumption/question:
(EXACT-PARAMETRIC-DP) Does the oracle-defined convex envelope , with and part of the input, admit exact algebraic optimization in polynomial bit complexity, including active tie refinements, without materializing its potentially large parametric-DP envelope?
No exact-computation claim is inferred from crossings-plus-midpoints or from an -accurate convex solve.
Counterexample DS19.3 (strong duality can fail by order one)
CE-DS-TILT-DUAL-GAP-001 is the equal-weight table
with . All six canonical nonempty partitions are regular, so DS9 and DS11 coincide. Exact enumeration gives
For and ,
With , . The mixed quadratic has vertex and minimum . Therefore
Since , the proposed primal-dual bracket has at least the same
gap. The witness is support-minimal for : has only the
singleton partition. (Audit H4: over all the minimum is ,
CE-DS-TILT-DUAL-GAP-002: rows , equal weights,
, exactly at by the mixture
, gap . The exact minimum of the
envelope is at .)
This is genuinely , not merely a fixed-size notation. For , give the four displayed atoms total mass and add distinct bounded rational atoms of total mass . Cellwise Cauchy--Schwarz bounds show uniformly, for in a compact set, that every added-only cell contributes , while every cell containing a base atom perturbs its quadratic by . The mixed quadratic above is coercive, so all dual minimizers remain in one compact interval. The same cellwise argument applied to the scalar Schur formula (a base-singular cell has cross term and nuisance term ) gives and . Hence stays bounded below by a positive constant. This construction uses positive weights and makes no split-duplicate assumption.
Theorem DS19.4 (the DS18 strip DP is -consistent)
On the exact DS18 law, let be the exact three-interval DP labeling of the uncentered scalar values . It is computable in polynomial time. Almost surely, it is regular eventually and
Proof. DP optimality gives , so the equality is the ordinary scalar Schur formula, with no centering. DS18's selection-independent uniform codebook event and the unique equal-third scalar optimum imply that the DP cells converge, up to labels, to the fixed cuts . Bounded scores then transfer all cell moments. Consequently and , proving regularity and the limit. ∎
The audited DS18 disagreement inequality therefore applies to
. This is strictly a value statement. The interval seed can
be one-point exchange-unstable (CE-DS-INTERVAL-SEED-UNSTABLE-001), and raw
population-cut labels can be unstable
(CE-DS-NONCENTERED-POPULATION-CUT-UNSTABLE-001). Nothing here proves local
ascent selects the basin, exchange stability of , perturbation
robustness, or a compile authorization.
Tier B: the matrix-tilt outer problem is not quasiconvex
Weak duality still holds for . Convexity and even quasiconvexity
of the proposed outer log-determinant map fail. In
CE-DS-MATRIX-TILT-NONQUASICONVEX-001, take the eight centered equal-weight
rows , split the first two coordinates as POI and
the last two as nuisance, and take . The singleton partition is the
only nonempty partition and its blocks are . Hence
For , , and , the exact determinants are . Thus , disproving quasiconvexity and therefore convexity. The certified ceiling remains valid, but minimizing it is a nonconvex outer problem in general. Tier B closes disproved; no library approximation follows.
Observable decision rule and deployment boundary
- A regular exhibited saddle pair closes the bracket and certifies finite global optimality on both domains. A singular saddle certifies only the generalized DS11 problem.
- A nonzero bracket reports the interval (or when explicitly generalized). It does not authorize the word “optimal”. The counterexample proves the interval may stay macroscopically open.
- The projected full-efficient-score interval rule remains the currently established unconditional projected-problem compiler. It is not silently relabeled as an in-bin profiled solution.
- A DS14 companion rule requires the complete audited sequence hypotheses and margins (M1)--(M5). A measured nuisance floor, one finite root, or -consistency alone is diagnostic only.
- In every other state the correct profiled compile action is refusal.
This result authorizes no src/ or public API change. The theorem and both
counterexamples require a fresh independent audit before any compile surface
can consume them.
Self-adversarial notes. The dual ceiling, primal lower bound, and closure condition name their comparison domains separately. Exact-K nonempty cells are used; empty-cell conventions are not hidden. The fixed-tilt value tolerates ties, but a concrete closure labeling is mandatory. The order-one family does not use duplicate splitting. Cardinality remains for centered regular samples. The DS18 proof uses the raw rows and only a value limit. Estimated scores, score-estimation error, held-out performance, and law perturbations remain outside the claim.
Stop-condition verdict. TIER A REDUCED. Validity on both named domains, the exact saddle closure condition, an exact duality-gap counterexample, polynomial certified-accuracy computation, and DS18 -consistency are settled. General exact polynomial bit-complexity is reduced precisely to (EXACT-PARAMETRIC-DP). TIER B DISPROVED: the outer matrix-tilt map need not be quasiconvex. The deployment question is answered: finite brackets are honest diagnostics/certificates at closure, while compile authorization remains projected-rule, full DS14 companion hypotheses, or refusal.
Next dependency-blocking question. After the audit, (EXACT-PARAMETRIC-DP) is settled at (bit-polynomial) and for fixed (arithmetic-polynomial); does a polynomial bit bound hold for fixed with variable , and is variable hard? The deployment blocker is a selection theorem: which certified or -consistent labeling does a practical solver return, and when does it inherit exchange stability.
From Profiled Ds: from a sample to the population · chapter contents
Independently audited: verified with hardened assumptions (Tier A), verified (Tier B and T5), umbrella reduced to the narrowed `OPEN-DS-TILT-DUAL-EXACT-COMPLEXITY` remainder. The audit report.
Evidence: py/ds_practical_certified_solver.py. Measured, never theorem authority.