claimroutineinferred_dep

Determinant and Cramer's rule contradiction

Claim·§4.3 Excluding bounded total variation·inside propTotal variation S cannot stay bounded

Statement (paper)

For an outcome satisfying the three tests, with all displayed quantities bounded by

B

and with , the difference equations

\Delta Z/D_j+\Delta W D_j+\Delta Z\Delta W=E_j

with

|E_j|\le 8B\tau

(

j=1,2,3

) force, via the determinant (of absolute value at least

r^3/B^3

) and Cramer's rule, the bound

|\Delta Z|\le 64B^5\tau/r^3<r/2

, contradicting

|\sigma(Z_{\widehat p}-Z_p)|\ge r

In plain English

For a good outcome passing the three tests, with all quantities bounded by

B

and the separation conditions holding, the three difference equations

\Delta Z/D_j+\Delta W D_j+\Delta Z\Delta W=E_j

with

|E_j|\le 8B\tau

force

|\Delta Z|\le 64B^5\tau/r^3<r/2

. This contradicts

|\sigma(Z_{\widehat p}-Z_p)|\ge r

Why it's here

This finishes the proof that

S

cannot stay bounded. Subtracting the unknowns

\Delta W

and

\Delta Z\Delta W

leaves a linear system in

\Delta Z

whose determinant is at least

r^3/B^3

in absolute value because the

D_j

are separated. Cramer's rule then makes

\Delta Z

tiny, against the separation

|\sigma(Z_{\widehat p}-Z_p)|\ge r

of the good outcome from the previous claim, so no such outcome can exist.

Classified routine:

A direct linear-algebra step: a Vandermonde-type determinant bounded below via the separation of the D_j, then Cramer's rule, applied to the good outcome provided by the previous claim (claim-ht-bounded-4).

Uses

claimPositive-probability good outcome exists

Used by

Nothing in the paper

Sources

PaperOpen

Section: §4.3 Excluding bounded total variation
Page: —
Label: —
Line: sections/03-heights.tex:330

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Determinant and Cramer's rule contradiction" rests on claim-ht-bounded-4