Result · DS-STRIP-DP-DELTA-CONSISTENCY

An interval rule is consistent on an explicit law

Proved here, no precedent foundindependently auditedpublication: internal

Read the proof and evidence →

Meaning

The zero-tilt interval dynamic program approaches the profiled value on the audited law without implying exchange stability or compilation authority.

Statement

On the audited DS18 law X,Z iid Uniform[-1,1], S=(X,3X^2-1+Z), K=3, let z_tilde_N be the exact interval-DP labeling of the raw uncentered X_i=T_0,i. Almost surely it is regular eventually and Delta_N=v_hat_3,N(X)-Phi_hat_Ds(z_tilde_N)=I_hat_psilambda(z_tilde_N)^2/I_hat_lambdalambda(z_tilde_N)->0, because the empirical scalar-DP cells converge to the unique equal-third rule, the cross block tends to 0, and the nuisance block tends to 32/81. The audited DS18 finite-N disagreement inequality therefore applies to this polynomial-time labeling rule.

Assumptions

  • the exact named DS18 law; d_psi=d_lambda=1; K=3; iid equal weights; exact scores

  • scores are not sample-centered and every empirical moment is about the origin

  • the DP uses beta=0 and exact scalar intervals; ties are null under the continuous X law

  • audited: the uncentered between value equals the centered between value plus the labeling-independent xbar^2, so z_tilde_N is exactly the empirical 3-means labeling of the X_i and DS18's selection-independent event Omega_0 applies to it without a profiled-optimality hypothesis

  • audited: the DS18 finite-N disagreement bound applies with the labeling's own Delta_N because z_tilde_N has own-codebook distortion excess 0 <= Delta_N; the bound was verified exactly on 12 dyadic samples up to N=4096

Where it stops

Audited 2 Sep 2026: verified. Delta-consistency is a value statement only. It does not imply one-point exchange stability, selection by local ascent, perturbation robustness, or compile authorization.

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.

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

Evidence references

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

Rests on

The full chain beneath it

Enables

Verified by

Open next door

Local graph
Local map of The beta-zero strip DP is value-consistent on the exact DS18 law2 prerequisites to the left, 3 results it enables or questions it raises to the right, 2 boundary cases below.Scalar efficient-score upper problem is exactly solvable by dynamic programmingScalar efficient-scor…Exact off-class global basin transfers to empirical exchange-stable optimaExact off-class globa…Best practical Ds solver with theorem-backed certificateBest practical Ds sol…Profiled compile verdict is selected by an observable certificate stateProfiled compile verd…Vector-parameter margins dichotomy beyond the scalar DS15 classVector-parameter marg…The beta-zero strip DP is value-consistent on the exact DS18 lawThe beta-zero strip D…Publication-grade audit of the DS19 tilt-DP certificate complexPublication-grade aud…CE-DS-INTERVAL-SEED-UNSTABLE-001CE-DS-INTERVAL-SEED-U…CE-DS-NONCENTERED-POPULATION-CUT-UNSTABLE-001CE-DS-NONCENTERED-POP…
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.