claimroutine

Good advice yields short nonempty answer set

Good advice gives a witness and an answer set of size between 1 and 2rs2^{r_{\rm s}}
gives the short answer set
Claim·§5.4 Obtaining many useful row fibers·inside lemGood row advice is common and gives short answer sets

Statement (paper)

For every positive integer kk, every family satisfying Equation , and every good row advice, one can select deterministically (using only (U,T,A,S0)(U,T,A,S_0) and the fixed table family) at most rsr_{\rm s} column specifications Mqj=tjMq_j=t_j with qj∈LUq_j\in L_U, tj∈Kt_j\in K, and a target Mz+uMz+u with z∈LUz\in L_U, u∈Ku\in K, e0⊤z=1e_0^\top z=1, satisfying the definition of goodness with the same agreement guarantee. Consequently, with Z=span⁡{qj}Z=\Span\{q_j\}, the answer set A=(z+Z)∩{v∈LU:e0⊤v=1}\mathcal A=(z+Z)\cap\{v\in L_U:e_0^\top v=1\} is nonempty and satisfies 1≤∣A∣≤2rs1\le|\mathcal A|\le 2^{r_{\rm s}}.

In plain English

For any good row advice, one can deterministically pick at most rsr_{\rm s} column specifications Mqj=tjMq_j=t_j and a target Mz+uMz+u with e0⊤z=1e_0^\top z=1, preserving the goodness agreement guarantee. The resulting answer set A=(z+Z)∩{v∈LU:e0⊤v=1}\mathcal A=(z+Z)\cap\{v\in L_U:e_0^\top v=1\}, with Z=span⁡{qj}Z=\Span\{q_j\}, is nonempty and has size at most 2rs2^{r_{\rm s}}.

Why it's here

This claim turns the abstract notion of a good row advice into a concrete, explicitly determined witness depending only on (U,T,A,S0)(U,T,A,S_0) and the table family. Because ZZ has dimension at most rsr_{\rm s} and zz itself lies in A\mathcal A, the answer set has between 11 and 2rs2^{r_{\rm s}} elements, which gives the short candidate list needed in the parent lemma's bound.
Classified routine:
Bookkeeping consequence of the definition of good row advice: fixing a canonical choice of witnesses, then counting an affine subspace over GF(2) of dimension at most r_s (at most 2^{r_s} points, nonempty since it contains z).

Uses

Nothing else in the paper

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.