lemmaroutine

Nonzero entries of M_0 have few differing coordinates

Lemma·lem:swaps-support·§4.2 The matrices M_0 and C^B

Statement (paper)

For all u,y∈Bu,y\in\mathcal B, if M0[u,y]≠0M_0[u,y]\ne0, then ∣{s∈[Q]:ay(s)≠du(s)}∣⩽R−1. \bigl|\{s\in[Q]:a_y(s)\ne d_u(s)\}\bigr|\le R-1.

In plain English

If the entry M0[u,y]M_0[u,y] is nonzero for u,y∈Bu,y\in\mathcal B, then the tuples aya_y and dud_u disagree in at most R−1R-1 of the QQ coordinates s∈[Q]s\in[Q].

Why it's here

This is a support (sparsity) property of M0M_0: nonzero entries occur only between index pairs that are close, differing in fewer than RR coordinates. Later results such as the layout lemma can use this locality to control where nonzero entries of M0M_0 can lie.
Classified routine:
A direct support check that follows from how M_0 is defined (its nonzero entries come from at most R-1 coordinate swaps). It is bookkeeping on the paper's own construction, not a new idea.

Uses

Nothing else in the paper

Used by

lemLayout data is efficiently constructible

Sources

PaperOpen
Section
§4.2 The matrices M_0 and C^B
Page
—
Label
lem:swaps-support
Line
main_full_version.tex:2288
Leannot aligned

Phase 2 aligns this node to a Lean declaration.