Result · OPEN-DS-PRACTICAL-CERTIFIED-SOLVER

The certified profiled solver question closes by reduction

Proved here, no precedent foundindependently auditedpublication: internal

Read the proof and evidence →

Meaning

The settled reduction distinguishes an exhibited saddle, an open bracket, conditional geometry, and refusal; broader exact complexity remains open.

Statement

DS19 closes the deployment-facing question by reduction. For d_psi=1 the tilt-DP construction gives a valid generalized bracket p^+<=g^+<=d and a regular in-bin bracket p_reg<=g_reg<=d, with exact closure iff a concrete DP-optimal labeling satisfies the tilt normal equation. Strong duality is false by an exact order-one N=4 counterexample and, support-minimally, by an exact N=3, K=2 counterexample. Fixed-tilt exact DP evaluation (O(KN) after sorting, ties tolerated), polynomial certified-epsilon dual minimization, exact polynomial-bit minimization at d_lambda=1 for every K, and arithmetic-polynomial exact minimization for fixed d_lambda>=2 (Toledo 1993) are established; exact polynomial bit complexity for fixed d_lambda>=2 with variable K, and any exact statement for variable d_lambda, is isolated as OPEN-DS-TILT-DUAL-EXACT-COMPLEXITY. On the exact DS18 law, the beta-zero interval DP is Delta-consistent almost surely and inherits the audited value-to-disagreement transfer, but not exchange stability, local-ascent selection, or compile authorization. For d_psi>1 the matrix-tilt outer map need not even be quasiconvex. The observable compile decision is therefore: an exhibited regular saddle certifies finite globality; an open bracket reports a bounded interval; projected efficient-score compilation remains the currently established unconditional projected route; a DS14 companion requires all audited sequence hypotheses; otherwise refuse.

Assumptions

  • Tier A certificate: d_psi=1, d_lambda>=1, positive rational finite weights, exact-K nonempty cells, raw uncentered score rows

  • the generalized DS11 pseudo-inverse and ordinary DS9 in-bin comparison domains are reported separately

  • the exact DS18 Delta-consistency corollary uses only the named bounded law, K=3, beta=0, iid equal weights, and exact scores

  • independently audited 2 Sep 2026 (AUDIT-DS-PRACTICAL-CERTIFIED-SOLVER): verified with hardened assumptions; the audit itself authorizes no src or public compile surface, which remains governed by DS-PROFILED-COMPILE-CERTIFICATE

  • a reported open bracket is not a gap certificate (CE-DS-TILT-DUAL-TIE-MASK-001), and the DP-active primal p^+ can sit strictly below g^+

reduced Tier A verdict answering an earlier line of work's deployment question, independently audited, isolating the remaining exact-complexity question in “Foundations”

Where it stops

Tier A is REDUCED, not a proof of exact polynomial bit complexity for fixed d_lambda>=2 with variable K or for variable d_lambda. Delta-consistency is value-only. The Tier B outer map is nonquasiconvex. No generic gate root, local optimizer terminal, measured nuisance floor, open bracket, or audit verdict authorizes compilation.

Refuted by

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

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

Bounded by

  • Counterexample fixtureCE-DS-INTERVAL-SEED-UNSTABLE-001

    The exact efficient-score interval labeling - the DP optimum of the full-sample efficient score, the documented initializer for profiled exchange and the finite analogue of the DS15 degenerate attainer J* - is itself one-point exchange-stable for the in-bin profiled-Ds objective. FALSE: on this exactly centered N=8 sample from the centered06 grid law, relocating row 7 to cell 1 raises the profiled value by 0.447 exactly. The improving move works by growing the binned nuisance block 27-fold (0.0042 -> 0.111): near the interval seed the projection tax is the dominant term and the profiled objective climbs by buying back nuisance information, the finite mechanism behind DS15 Proposition 6's steering.

  • Counterexample fixtureCE-DS-NONCENTERED-POPULATION-CUT-UNSTABLE-001

    The literal labels induced by an isolated nondegenerate population Ds rule are automatically exact one-point exchange-stable on every finite sample. FALSE: on this support-minimal movable N=4 sample from the named off-(L) law, one boundary-scale relocation raises the exact profiled value by 37/14608. The population-to-empirical theorem must select finite global optima or otherwise control exact moves; it cannot identify the raw population-cut labels with a terminal state.

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

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

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.

Why each source is not this result: the search records

Nearest sources, checked 1 September 2026

The full search record

Relationships

Evidence references

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

Rests on

The full chain beneath it

Enables

Raises

Verified by

Open next door

Local graph
Local map of Best practical Ds solver with theorem-backed certificate8 prerequisites to the left, 2 results it enables or questions it raises to the right, 7 boundary cases below.D-optimal efficient-score quantization upper-bounds global DsD-optimal efficient-s…Exact finite Ds one-point objective oracleExact finite Ds one-p…The multivariate-POI matrix-tilt outer ceiling need not be quasiconvexThe multivariate-POI…Exact off-class global basin transfers to empirical exchange-stable optimaExact off-class globa…Variational form of the profiled objectiveVariational form of t…Scalar efficient-score upper problem is exactly solvable by dynamic programmingScalar efficient-scor…The beta-zero strip DP is value-consistent on the exact DS18 lawThe beta-zero strip D…Scalar-POI tilt-DP gives a valid two-sided certificate with an exact saddle closure gateScalar-POI tilt-DP gi…Profiled compile verdict is selected by an observable certificate stateProfiled compile verd…Exact bit complexity of the variable-dimension tilt-DP dualExact bit complexity…Best practical Ds solver with theorem-backed certificateBest practical Ds sol…Publication-grade audit of the DS19 tilt-DP certificate complexPublication-grade aud…CE-DS-MATRIX-TILT-NONQUASICONVEX-001CE-DS-MATRIX-TILT-NON…CE-DS-TILT-DUAL-GAP-001CE-DS-TILT-DUAL-GAP-0…CE-DS-TILT-DUAL-GAP-002CE-DS-TILT-DUAL-GAP-0…CE-DS-INTERVAL-SEED-UNSTABLE-001CE-DS-INTERVAL-SEED-U…CE-DS-NONCENTERED-POPULATION-CUT-UNSTABLE-001CE-DS-NONCENTERED-POP…CE-DS-NONCENTERED-SINGULAR-DESTINATION-001CE-DS-NONCENTERED-SIN…CE-DS-TILT-DUAL-TIE-MASK-001CE-DS-TILT-DUAL-TIE-M…
Prerequisites to the left, what it enables or raises to the right, boundary cases below. Open in the map.

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 ⇔\Leftrightarrow saddle held on 54/54 exact-dd 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 O(KN2)O(KN^2) bound (in fact O(KN)O(KN) 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 D(β∗)\mathcal D(\beta^*) when the bracket closes (CE-DS-TILT-DUAL-TIE-MASK-001, N=3,K=2N=3,K=2, pairwise-distinct tilted values), so a reported open interval is not a gap certificate. (H3) the certified-ε\varepsilon 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 K=3K=3 only; the overall minimum is CE-DS-TILT-DUAL-GAP-002 (N=3,K=2N=3,K=2, g+=1/3g^+=1/3, d=1/2d=1/2, gap 1/61/6); the exact dual minimum of fixture 001 is 44729/423244729/4232 at the rational crossing β∗=−8/23\beta^*=-8/23, exact gap 534361/781333534361/781333, 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 dλ=1d_\lambda=1 the exact dual minimiser is computable in polynomial bit complexity for every KK — the breakpoints are roots of degree-≤2\le2 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 dλ≥2d_\lambda\ge2 and variable KK 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 dλ≥2d_\lambda\ge2 and to variable dλd_\lambda. The audit authorizes no src/ change.

Normalization (protocol A). Tier A has dψ=1d_\psi=1, arbitrary dλ≥1d_\lambda\ge1, 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 KK-cell labeling. The generalized comparison domain uses DS11's pseudo-inverse value Φ+(z)\Phi^+(z); the ordinary in-bin domain is its subset with a nonsingular nuisance block. For β∈Rdλ\beta\in\mathbb R^{d_\lambda}, put

Tβi=sψi−βsλi,Vz(β)=∑b(∑i:zi=bwiTβi)2∑i:zi=bwi.T_{\beta i}=s_{\psi i}-\beta s_{\lambda i},\qquad V_z(\beta)=\sum_b\frac{\bigl(\sum_{i:z_i=b}w_iT_{\beta i}\bigr)^2} {\sum_{i:z_i=b}w_i}.

Let vK(β)=max⁡zVz(β)v_K(\beta)=\max_zV_z(\beta). By scalar contiguity this value is returned by the exact interval DP after sorting TβT_\beta. Let

g+=max⁡zΦ+(z),greg=max⁡z:Iλλ(z)≻0Φ(z),d=min⁡βvK(β).g^+=\max_z\Phi^+(z),\quad g_{\rm reg}=\max_{z:I_{\lambda\lambda}(z)\succ0}\Phi(z),\quad d=\min_\beta v_K(\beta).

For the primal, a tie policy is part of the object. If D(β){\cal D}(\beta) is the set of DP-optimal labelings at β\beta, define

p+=max⁡β, z∈D(β)Φ+(z),preg=max⁡β, z∈D(β), Iλλ(z)≻0Φ(z).p^+=\max_{\beta,\,z\in{\cal D}(\beta)}\Phi^+(z),\qquad p_{\rm reg}=\max_{\beta,\,z\in{\cal D}(\beta),\, I_{\lambda\lambda}(z)\succ0}\Phi(z).

An implementation may use one deterministic member of D(β){\cal D}(\beta); 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 g+=dg^+=d; an open reported interval therefore certifies nothing about the gap.) The information-loss implication is a finite train-sample DsD_s 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,

p+≤g+≤d.\boxed{p^+\le g^+\le d.}

On the ordinary in-bin domain,

preg≤greg≤g+≤d.\boxed{p_{\rm reg}\le g_{\rm reg}\le g^+\le d.}

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 pregp_{\rm reg} is load-bearing.

Moreover the generalized bracket closes, p+=g+=dp^+=g^+=d, iff there are (β∗,z∗)(\beta^*,z^*) such that

z∗∈D(β∗),β∗Iλλ(z∗)=Iψλ(z∗).z^*\in{\cal D}(\beta^*),\qquad \beta^*I_{\lambda\lambda}(z^*)=I_{\psi\lambda}(z^*).

Equivalently, z∗z^* maximizes Vz(β∗)V_z(\beta^*) over labelings and β∗\beta^* minimizes Vz∗(β)V_{z^*}(\beta): it is a saddle pair. If in addition Iλλ(z∗)≻0I_{\lambda\lambda}(z^*)\succ0, the same equality certifies z∗z^* 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 Φ+(z)=min⁡γVz(γ)\Phi^+(z)=\min_\gamma V_z(\gamma). Hence for every z,βz,\beta,

Φ+(z)≤Vz(β)≤max⁡z′Vz′(β)=vK(β).\Phi^+(z)\le V_z(\beta)\le\max_{z'}V_{z'}(\beta)=v_K(\beta).

Taking the indicated maxima and minimum proves weak duality and both lower bounds. If a saddle pair exists, all inequalities are equalities. Conversely, if g+=dg^+=d, choose a primal maximizer z∗z^* and a dual minimizer β∗\beta^*. Then

d=min⁡γVz∗(γ)≤Vz∗(β∗)≤vK(β∗)=d.d=\min_\gamma V_{z^*}(\gamma) \le V_{z^*}(\beta^*) \le v_K(\beta^*)=d.

Thus both inequalities are equalities: z∗z^* is DP-optimal at β∗\beta^*, and DS11's attainment set makes β∗\beta^* satisfy exactly the displayed normal equation. The same pair also gives an attained p+=dp^+=d. 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 vK(β)v_K(\beta) even when equal tilted values are pooled (audit H1, tie lemma: each mixed cell's term (M+tg)2/(W+g)(M+tg)^2/(W+g) is convex in the tied mass gg 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 (β,β+ε)(\beta,\beta+\varepsilon) is contiguous in the order breaking ties by decreasing sλs_\lambda). At a crossing, different row-level refinements can have the same DP value and different derivatives. Any active derivative is a valid subgradient of vKv_K, 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 β\beta, vK(β)v_K(\beta), one active labeling, its exact rational gradient, and the regular/generalized primal values are computable in O(KN2)O(KN^2) rational operations by sorted interval DP. The map vKv_K is a finite maximum of convex quadratics, hence convex. With rational input, full empirical nuisance span, and a requested rational tolerance ε>0\varepsilon>0, a standard separation-oracle convex method therefore returns certified rational lower/upper bounds on dd of width ε\varepsilon in time polynomial in the input bit length and log⁡(1/ε)\log(1/\varepsilon). 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 KK and dλd_\lambda are fixed; the audit widens this (H-scope above): polynomial bit complexity at dλ=1d_\lambda=1 for every KK, and arithmetic-polynomial exact minimisation for fixed dλ≥2d_\lambda\ge2, variable KK (Toledo 1993). The fixed-(K,dλ)(K,d_\lambda) argument follows. The O(N2dλ)O(N^{2d_\lambda}) tilt-order arrangement, including its tie faces, has polynomial size then; each cell has (N−1K−1)\binom{N-1}{K-1} contiguous candidates, and fixed-dimensional real-algebraic comparison of their quadratic envelopes returns the exact minimum. This is not polynomial jointly in variable K,dλK,d_\lambda.

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 min⁡βvK(β)\min_\beta v_K(\beta), with KK and dλd_\lambda 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 ε\varepsilon-accurate convex solve.

Counterexample DS19.3 (strong duality can fail by order one)

CE-DS-TILT-DUAL-GAP-001 is the equal-weight table

(−11/2,39/8),(3/2,−65/8),(7/2,31/8),(9/2,−49/8),(-11/2,39/8),\quad(3/2,-65/8),\quad (7/2,31/8),\quad(9/2,-49/8),

with K=3K=3. All six canonical nonempty partitions are regular, so DS9 and DS11 coincide. Exact enumeration gives

g=g+=greg=11680511816.g=g^+=g_{\rm reg}=\frac{116805}{11816}.

For z1=(0,0,1,2)z_1=(0,0,1,2) and z2=(0,1,2,2)z_2=(0,1,2,2),

q1(β)=92564β2+154β+818,q2(β)=147764β2+24β+1298.q_1(\beta)=\frac{925}{64}\beta^2+\frac{15}{4}\beta+\frac{81}{8}, \quad q_2(\beta)=\frac{1477}{64}\beta^2+24\beta+\frac{129}{8}.

With α=14/25\alpha=14/25, vK(β)≥αq1(β)+(1−α)q2(β)v_K(\beta)\ge \alpha q_1(\beta)+(1-\alpha)q_2(\beta). The mixed quadratic has vertex −10128/29197-10128/29197 and minimum 61717893/583940061717893/5839400. Therefore

d−g≥617178935839400−11680511816=105329256154014175>0.68.\boxed{ d-g\ge \frac{61717893}{5839400}-\frac{116805}{11816} =\frac{105329256}{154014175}>0.68 .}

Since p+≤gp^+\le g, the proposed primal-dual bracket has at least the same gap. The witness is support-minimal for K=3K=3: N=3,K=3N=3,K=3 has only the singleton partition. (Audit H4: over all KK the minimum is N=3,K=2N=3,K=2, CE-DS-TILT-DUAL-GAP-002: rows (−1,0),(0,−1),(1,0)(-1,0),(0,-1),(1,0), equal weights, g+=1/3g^+=1/3, d=1/2d=1/2 exactly at β∗=0\beta^*=0 by the mixture 16β2+12\tfrac16\beta^2+\tfrac12, gap 1/61/6. The exact minimum of the N=4N=4 envelope is 44729/423244729/4232 at β∗=−8/23\beta^*=-8/23.)

This is genuinely Θ(1)\Theta(1), not merely a fixed-size notation. For r→∞r\to\infty, give the four displayed atoms total mass 1−1/r1-1/r and add rr distinct bounded rational atoms of total mass 1/r1/r. Cellwise Cauchy--Schwarz bounds show uniformly, for β\beta in a compact set, that every added-only cell contributes O(1/r)O(1/r), while every cell containing a base atom perturbs its quadratic by O(1/r)O(1/r). 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 O(1/r)O(1/r) and nuisance term O(1/r)O(1/r)) gives dr→dd_r\to d and gr+→g+g_r^+\to g^+. Hence dr−gr+d_r-g_r^+ 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 Δ\Delta-consistent)

On the exact DS18 law, let z~N\tilde z_N be the exact three-interval DP labeling of the uncentered scalar values Xi=T0,iX_i=T_{0,i}. It is computable in polynomial time. Almost surely, it is regular eventually and

0≤ΔN:=v^3,N(X)−Φ^Ds(z~N)=I^ψλ(z~N)2I^λλ(z~N)⟶0.0\le\Delta_N :=\hat v_{3,N}(X)-\hat\Phi_{D_s}(\tilde z_N) =\frac{\hat I_{\psi\lambda}(\tilde z_N)^2} {\hat I_{\lambda\lambda}(\tilde z_N)}\longrightarrow0.

Proof. DP optimality gives I^ψψ(z~N)=v^3,N(X)\hat I_{\psi\psi}(\tilde z_N)=\hat v_{3,N}(X), 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 ±1/3\pm1/3. Bounded scores then transfer all cell moments. Consequently I^ψλ(z~N)→0\hat I_{\psi\lambda}(\tilde z_N)\to0 and I^λλ(z~N)→32/81\hat I_{\lambda\lambda}(\tilde z_N)\to32/81, proving regularity and the limit. ∎

The audited DS18 disagreement inequality therefore applies to z~N\tilde z_N. 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 z~N\tilde z_N, perturbation robustness, or a compile authorization.

Tier B: the matrix-tilt outer problem is not quasiconvex

Weak duality still holds for dψ>1d_\psi>1. 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 {±2ej:j=1,…,4}\{\pm2e_j:j=1,\ldots,4\}, split the first two coordinates as POI and the last two as nuisance, and take K=N=8K=N=8. The singleton partition is the only nonempty partition and its blocks are I2,0,I2I_2,0,I_2. Hence

f(B)=log⁡det⁡(I2+BB⊤).f(B)=\log\det(I_2+BB^\top).

For B0=diag⁡(4,0)B_0=\operatorname{diag}(4,0), B1=diag⁡(0,4)B_1=\operatorname{diag}(0,4), and B1/2=(B0+B1)/2=diag⁡(2,2)B_{1/2}=(B_0+B_1)/2=\operatorname{diag}(2,2), the exact determinants are 17,17,2517,17,25. Thus f(B1/2)>max⁡(f(B0),f(B1))f(B_{1/2})>\max(f(B_0),f(B_1)), 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

  1. 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.
  2. A nonzero bracket reports the interval [preg,d][p_{\rm reg},d] (or [p+,d][p^+,d] when explicitly generalized). It does not authorize the word “optimal”. The counterexample proves the interval may stay macroscopically open.
  3. 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.
  4. A DS14 companion rule requires the complete audited sequence hypotheses and margins (M1)--(M5). A measured nuisance floor, one finite root, or Δ\Delta-consistency alone is diagnostic only.
  5. 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 K≥dψ+dλ+1K\ge d_\psi+d_\lambda+1 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 Θ(1)\Theta(1) duality-gap counterexample, polynomial certified-accuracy computation, and DS18 Δ\Delta-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 dλ=1d_\lambda=1 (bit-polynomial) and for fixed dλd_\lambda (arithmetic-polynomial); does a polynomial bit bound hold for fixed dλ≥2d_\lambda\ge2 with variable KK, and is variable dλd_\lambda hard? The deployment blocker is a selection theorem: which certified or Δ\Delta-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.