Result · DS-TILT-DUAL-CERTIFICATE

A tilted dual brackets the profiled optimum

Proved here, no precedent foundindependently auditedpublication: internal

Read the proof and evidence →

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 gap

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

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

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

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

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.

Relationships

Rests on

The full chain beneath it

Enables

Raises

Verified by

Open next door

Local graph
Local map of Scalar-POI tilt-DP gives a valid two-sided certificate with an exact saddle closure gate2 prerequisites to the left, 3 results it enables or questions it raises to the right, 4 boundary cases below.Variational form of the profiled objectiveVariational form of t…Scalar efficient-score upper problem is exactly solvable by dynamic programmingScalar efficient-scor…Profiled compile verdict is selected by an observable certificate stateProfiled compile verd…Best practical Ds solver with theorem-backed certificateBest practical Ds sol…Exact bit complexity of the variable-dimension tilt-DP dualExact bit complexity…Scalar-POI tilt-DP gives a valid two-sided certificate with an exact saddle closure gateScalar-POI tilt-DP gi…Publication-grade audit of the DS19 tilt-DP certificate complexPublication-grade aud…CE-DS-TILT-DUAL-GAP-001CE-DS-TILT-DUAL-GAP-0…CE-DS-TILT-DUAL-GAP-002CE-DS-TILT-DUAL-GAP-0…CE-DS-TILT-DUAL-TIE-MASK-001CE-DS-TILT-DUAL-TIE-M…CE-DS-NONCENTERED-SINGULAR-DESTINATION-001CE-DS-NONCENTERED-SIN…
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.