Result · DS-STRIP-DP-DELTA-CONSISTENCY
An interval rule is consistent on an explicit law
Proved here, no precedent foundindependently auditedpublication: internal
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
- CE-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.
- CE-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
- Scalar efficient-score upper problem is exactly solvable by dynamic programmingDS-SCALAR-EFFICIENT-DP
- Exact off-class global basin transfers to empirical exchange-stable optimaDS-NONCENTERED-GLOBAL-BASIN-TRANSFER
The full chain beneath it
- D-optimal efficient-score quantization upper-bounds global DsDS-EFFICIENT-SCORE-GLOBAL-UPPER
- Variational form of the profiled objectiveDS-PROFILED-VARIATIONAL
- Margins dichotomy at global finite Ds optima (conditionally centered laws, scalar nuisance)OPEN-DS-MARGINS-AT-OPTIMA
- Inhabitation reduces to a scalar root equation per lawDS-STABLE-BASINS-FIXED-POINT-GATE
- Full-data efficient-score dominationDS-EFFICIENT-SCORE-DOMINATION
- Ds objective is the logdet of efficient/profiled Schur informationDS-SCHUR
- Quantized Fisher-information identityFI-QUANT-IDENTITY
- Full in-bin Ds profiling is singular when K<=dDS-FULL-PROFILE-K-LE-D-SINGULAR
- A finite global Ds optimum can be a degenerate exact tie classDS-GLOBAL-TIE-DEGENERACY
- Conditional finite-to-population Ds bridgeOPEN-DS-FINITE-POP-BRIDGE
- Population stationary geometry for profiled DsOPEN-DS-POP-COMMON-METRIC
- Conditional centering empties the margin-certified stable branchDS-STABLE-BASINS-CENTERED-OBSTRUCTION
- Rank ceiling for K hard categoriesFI-RANK-CEILING
- Exact profiled leverage stability boundDS-EXCHANGE-LEVERAGE-BOUND
- Restricted affine-max empirical consistencyCONSISTENCY-RESTRICTED-AFFINE
- Approximate finite Ds efficient-Voronoi necessity boundDS-OKN-BOUND
- Ds first-order gradient is an efficient semimetricDS-GRADIENT-EFFICIENT-SEMIMETRIC
- Infinitesimal cell-transfer identityGENERAL-FIRST-VARIATION
- Exact weighted rank-two relocationD-RANK2-MOVE
- Exact finite Ds one-point objective oracleDS-EXACT-MOVE-ORACLE
- Exact finite D log-determinant gainD-LOGDET-GAIN
Enables
- Best practical Ds solver with theorem-backed certificateOPEN-DS-PRACTICAL-CERTIFIED-SOLVER
- Profiled compile verdict is selected by an observable certificate stateDS-PROFILED-COMPILE-CERTIFICATE
- Vector-parameter margins dichotomy beyond the scalar DS15 classOPEN-DS-MARGINS-NONCENTERED
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.