claimroutineinferred_dep

Shortcode contradiction forces large good set

Rare good fibers would contradict the shortcode theorem, so Pr⁡[B]≥η\Pr[B]\ge\eta
gives good-fiber mass at each pair
Claim·§5.4 Obtaining many useful row fibers·inside lemGood row advice is common and gives short answer sets

Statement (paper)

For the modified function, every slice of the allowed type has modified agreement less than 3α/43\alpha/4 (if its row fiber was good, every entry of that fiber lies in BB and its modified agreement is less than α/4\alpha/4; otherwise the original agreement with each target on the slice was less than α/2\alpha/2 and the randomized matches add less than α/4\alpha/4), so the hypotheses of Theorem  would contradict the modified function's acceptance of at least 2η2\eta unless BB is large. Consequently Pr⁡[B]≥η\Pr[B]\ge\eta.

In plain English

For the modified function (with random values placed on BB), every allowed slice has modified agreement below 3α/43\alpha/4, so Theorem 5.1 would contradict the modified function's acceptance of at least 2η2\eta unless BB is large. Hence Pr⁡[B]≥η\Pr[B]\ge\eta.

Why it's here

This is the contradiction step of the parent's argument. Agreement on a slice splits into a part from good row fibers (which lie in BB and are below α/4\alpha/4) or from non-good fibers (original agreement below α/2\alpha/2), plus the randomized matches (below α/4\alpha/4, by the previous claim). So the shortcode theorem's conclusion fails for the modified function, which has acceptance at least 2η2\eta if Pr⁡[B]<η\Pr[B]<\eta (by the first claim), forcing Pr⁡[B]≥η\Pr[B]\ge\eta.
Classified routine:
This is the contradiction step of the parent lemma. It splits a slice's agreement into the parts covered by the two earlier claims and then applies the inverse shortcode theorem (Theorem 5.1), so it is bookkeeping that follows directly from those nodes.

Uses

thmInverse shortcode theoremclaimRandomizing good fibers keeps acceptance 2etaclaimRandom replacements match few on slices

Used by

claimGood advice mass lower bound

Sources

PaperOpen
Section
§5.4 Obtaining many useful row fibers
Page
—
Label
—
Line
sections/04-matrix.tex:396
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Shortcode contradiction forces large good set" rests on claim-lem-good-row-advice-1
  • info
    inferred_dep
    outline: "Shortcode contradiction forces large good set" rests on claim-lem-good-row-advice-2