claimroutine

Some fiber has retention at least eta/2

Some fiber of ff has retention at least η/2\eta/2
averaging step picking the fiber
Claim·§5.1 The inverse shortcode theorem·inside thmInverse shortcode theorem

Statement (paper)

There is a nonempty fiber S=f−1(y)S=f^{-1}(y) whose retention under the matrix step (a uniform M∈SM\in S and M+al⊤M+al^\top with a,la,l uniform) is at least η\eta; moreover, once the dimension thresholds are chosen so that p0=2−ℓ+2−m−2−ℓ−m≤η/2p_0=2^{-\ell}+2^{-m}-2^{-\ell-m}\le\eta/2, the retention of SS conditional on both factors a,la,l being nonzero is at least (η−p0)/(1−p0)≥η/2(\eta-p_0)/(1-p_0)\ge\eta/2.

In plain English

Some nonempty fiber S=f−1(y)S=f^{-1}(y) has retention at least η\eta under the matrix step M↦M+al⊤M\mapsto M+al^\top. Once p0=2−ℓ+2−m−2−ℓ−m≤η/2p_0=2^{-\ell}+2^{-m}-2^{-\ell-m}\le\eta/2, its retention conditional on both aa and ll being nonzero is at least (η−p0)/(1−p0)≥η/2(\eta-p_0)/(1-p_0)\ge\eta/2.

Why it's here

This is an averaging step: the acceptance probability Pr⁡[f(M)=f(M+al⊤)]≥η\Pr[f(M)=f(M+al^\top)]\ge\eta is a weighted average of the retention of the fibers of ff, so one fiber must do at least as well. Discarding the degenerate cases a=0a=0 or l=0l=0 (total probability p0p_0, where the perturbation is trivial) costs little when ℓ,m\ell,m are large, so the fiber still has retention at least η/2\eta/2 for genuine rank-one perturbations, which the next claim lifts to a Grassmann setting.
Classified routine:
A direct averaging argument: the overall acceptance probability is a weighted average of fiber retentions, so some fiber does at least as well. Conditioning away the degenerate events a=0 or l=0 (probability p_0) is elementary probability bookkeeping.

Uses

Nothing else in the paper

Used by

claimMatrix chart lift has Grassmann retention

Sources

PaperOpen
Section
§5.1 The inverse shortcode theorem
Page
—
Label
—
Line
sections/04-matrix.tex:77
Leannot aligned

Phase 2 aligns this node to a Lean declaration.