Lemma 3.4: the sets $C_a=\phi_a(S)$ partition $V(Z)$ into induced copies of $G[S]$

Throughout, $G$ is a finite simple graph whose vertex set is partitioned into $k$ non-empty independent domains $V(G)=V_1\sqcup\cdots\sqcup V_k$, $A$ and $B$ are finite non-empty sets with $|A|=|B|=M$, and $\mathcal F=\{f_v:A\to B\}_{v\in V(G)}$ is a family of maps with copy maps $\phi_a(v)=(\mathrm{dom}(v),f_v(a))$, images $W_a=\phi_a(V(G))$ and target graph $Z$ on $[k]\times B$ (Section 3.1).

Let $t\ge2$, let $\mathcal F$ be $t$-locally coherent, and let $S=\{\sigma_1,\dots,\sigma_k\}$ be a set of source vertices with $\sigma_i\in V_i$. Then the sets

partition the vertex set of $Z$ into $M=N/k$ parts, and each $C_a$ induces a copy of $G[S]$ via $\sigma_i\mapsto\phi_a(\sigma_i)$.

This is the covering guarantee of the construction, and it holds simultaneously for every choice of one vertex per domain.

Formalization Note $S$ is a map $[k]\to V(G)$ with $\mathrm{dom}(\sigma_i)=i$. "The $C_a$ partition $V(Z)$" is the bijectivity of $(a,i)\mapsto\phi_a(\sigma_i)$ from $A\times[k]$ onto $[k]\times B$; "induces a copy" is that $\phi_a(\sigma_i)\sim_Z\phi_a(\sigma_{i'})$ iff $\sigma_i\sim_G\sigma_{i'}$.

Differences from the source:

• encoding: standing assumptions of §3.1 (domain partition of G; A, B finite nonempty with |A| = |B| = M) → binders IsDomainPartition G dom, [Fintype A] [Nonempty A] [Fintype B], Fintype.card A = Fintype.card B; reason: the section's standing assumptions written as hypotheses; same instances
• encoding: domains 1, …, k and vertex set [k] × B of Z → domains Fin k = {0, …, k−1}, vertex type Fin k × B, family f : V → A → B; reason: Lean indexing convention; same instances
• encoding: {C_a} partitions V(Z) into M = N/k parts, each inducing a copy of G[S] → (a, i) ↦ ϕ_a(σ_i) is a bijection A × Fin k → Fin k × B, and ϕ_a(σ_i) ~ ϕ_a(σ_i') ↔ σ_i ~ σ_i'; reason: a bijection from A × [k] is a partition into |A| = M parts of k vertices; the adjacency iff on the parts is the induced isomorphism; same instances