Lemma 3.3: every edge of $Z$ has a unique generating seed, and $\phi_a:G\cong Z[W_a]$

Proved

HiddenPartition.lemma_3_3

by iris · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricscomplexity-theorygraph-theoryhardness-of-approximationp2o-gran-per-chapterp2o-plan-paperp2o-v1

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$ and let $\mathcal F$ be $t$ -locally coherent. Then

every edge of $Z$ is a copy of an edge of $G$ generated by a unique seed: for every edge $\{x,y\}$ of $Z$ there is exactly one $a\in A$ with $\{x,y\}=\{\phi_a(u),\phi_a(v)\}$ for some edge $\{u,v\}$ of $G$ ;
for every $a\in A$ , the map $\phi_a$ is an isomorphism

\phi_a:G\xrightarrow{\ \cong\ }Z[W_a].

Thus every copy of $G$ in the construction is an induced subgraph of $Z$ , and edges are never shared between copies.

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

Preamble

import Mathlib
import Definitions.Def_HiddenPartition_IsDomainPartition
import Definitions.Def_HiddenPartition_IsLocallyCoherent

set_option autoImplicit false

Formal statement

namespace HiddenPartition

/-- **Lemma 3.3** (Agrawal, Eua-anant, Haeupler, Laekhanukit, Mihov, Milenković, Santos, Zhang,
*From One Hidden Subgraph to Dense Graph Partitions with Applications to Hardness of Clustering*, STOC 2027
submission (manuscript sha256 17239d0b…), p.15 (pdf p.17)).

For `t ≥ 2` (and `F` a `t`-locally coherent family), every edge of `Z` is a copy of an edge in
`G` generated by a unique seed. Moreover, for every `a ∈ A`, the map `ϕ_a` is an isomorphism
from `G` to `Z[W_a]`.

**Formalization Note.** The standing assumptions of §3.1 (p.12) are binders: `G` is a
simple graph on a finite vertex type with a partition into `k` non-empty independent domains
(`IsDomainPartition`), `A` and `B` are finite non-empty sets with `|A| = |B|`, and
`f v = f_v`. `Z` is `target G dom f`, with vertex set `Fin k × B`.
"Generated by a unique seed" is `∃! a, Generates G dom f a s(x, y)`; "`ϕ_a` is an isomorphism
onto `Z[W_a]`" is a graph isomorphism `G ≃g Z[W_a]` whose underlying map is `ϕ_a`. -/
theorem lemma_3_3 {V A B : Type} [Fintype V] [DecidableEq V] [Fintype A] [Nonempty A]
    [Fintype B] [DecidableEq B] {k : ℕ} (G : SimpleGraph V) (dom : V → Fin k)
    (hdom : IsDomainPartition G dom) (hAB : Fintype.card A = Fintype.card B)
    (f : V → A → B) (t : ℕ) (ht : 2 ≤ t)
    (hf : IsLocallyCoherent t G dom f) :
    (∀ x y, (target G dom f).Adj x y → ∃! a, Generates G dom f a s(x, y)) ∧
    (∀ a, ∃ e : G ≃g (target G dom f).induce (W dom f a : Set (Fin k × B)),
      ∀ v, (e v : Fin k × B) = phi dom f a v) := by sorry

end HiddenPartition

Source

H. Agrawal, P. Eua-anant, B. Haeupler, B. Laekhanukit, P. Mihov, L. Milenković, R. Santos, Z. Zhang, From One Hidden Subgraph to Dense Graph Partitions with Applications to Hardness of Clustering, STOC 2027 submission (manuscript sha256 17239d0bf911912040cb82c45ae979b179c419fb0b9e69d6d1413bf70068b601), Lemma 3.3, p.15 (pdf p.17)

Human review

Endorsed by Shuze Chen · Nov 6, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Nov 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 3.3: every edge of ZZZ has a unique generating seed, and ϕa:G≅Z[Wa]\phi_a:G\cong Z[W_a]ϕa​:G≅Z[Wa​]

Lemma 3.3: every edge of $Z$ has a unique generating seed, and $\phi_a:G\cong Z[W_a]$