Cross-matrix super-surjective transfer (Cai–Govorov Lemma 5.1, two-matrix form)

Port of the proved single-matrix chunk 3A of Graphon/Lovasz.lean (testEvalEq_implies_orbit_super / superMap) to the CROSS-matrix setting: the left tuple ξ : Fin K → Fin T probes (B, W) and the right tuple ψ : Fin K → Fin T' probes (B', W'), with matched test-moment profiles as the input interface.

The deliverable is the partition form (cross_super_partition): classes C : Fin T → Finset (Fin T') that are nonempty, pairwise disjoint, covering, with W t = ∑_{t' ∈ C t} W' t' and the block-averaged edge relation. The star/edge tests cannot separate a fractional refinement across two matrices of different sizes, so bijectivity is NOT proved here; the consumer (Graphon/MatrixDetermination.lean) combines the two symmetric partitions, forcing T = T' by counting, whence all classes are singletons and the partition collapses to a weight- and entry-preserving bijection.

Only LEFT twin-freeness is needed for the partition.

Main statements

• class_balance_two — the aligned-Vandermonde extraction over two DIFFERENT index types (the port of Lovasz.aligned_moments_class_balance_of_bound, whose two families shared one index type).
• exists_large_const_image_subset — pigeonhole: a ψ-constant subset of size ≥ M inside each ξ-fibre of size ≥ T'·M.
• cross_super_partition — the partition deliverable.

The two-sided aligned-Vandermonde extraction

theorem Graphon.CrossSuper.class_balance_two {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {s : ℕ} (x : ι → Fin s → ℝ) (y : κ → Fin s → ℝ) (a : ι → ℝ) (b : κ → ℝ) (N : ℕ) (hNx : ∀ (c : Fin s), (Finset.image (fun (i : ι) => x i c) Finset.univ).card ≤ N) (hNy : ∀ (c : Fin s), (Finset.image (fun (j : κ) => y j c) Finset.univ).card ≤ N) (hmom : ∀ (k : Fin s → ℕ), (∀ (c : Fin s), k c < 2 * N) → ∑ i : ι, a i * ∏ c : Fin s, x i c ^ k c = ∑ j : κ, b j * ∏ c : Fin s, y j c ^ k c) (z : Fin s → ℝ) : ∑ i : ι with x i = z, a i = ∑ j : κ with y j = z, b j

Aligned-Vandermonde extraction over two index types (port of Lovasz.aligned_moments_class_balance_of_bound; there the two profile families shared one index type, here ι and κ differ). If the moment sums of the two weighted profile families agree for every exponent vector bounded by 2·N (with N bounding the number of distinct values of every coordinate on each side), then the a-mass and b-mass of every profile level set agree.

Pigeonhole and block regrouping

theorem Graphon.CrossSuper.exists_large_const_image_subset {T T' K : ℕ} (ξ : Fin K → Fin T) (ψ : Fin K → Fin T') (M : ℕ) (hT' : 0 < T') (hξ : ∀ (v : Fin T), T' * M ≤ {i : Fin K | ξ i = v}.card) (v : Fin T) : ∃ (gv : Fin T'), ∃ J ⊆ {i : Fin K | ξ i = v}, M ≤ J.card ∧ ∀ i ∈ J, ψ i = gv

Pigeonhole (port of Lovasz.exists_large_const_image_subset). Inside each ξ-fibre of size ≥ T'·M there is a subset of size ≥ M on which ψ is constant.

theorem Graphon.CrossSuper.prod_biUnion_const {T K : ℕ} {J : Fin T → Finset (Fin K)} (hdisj : (↑Finset.univ).PairwiseDisjoint J) {f : Fin K → ℝ} {c : Fin T → ℝ} (hc : ∀ (v : Fin T), ∀ i ∈ J v, f i = c v) {k : Fin T → ℕ} (hcard : ∀ (v : Fin T), (J v).card = k v) : ∏ i ∈ Finset.univ.biUnion J, f i = ∏ v : Fin T, c v ^ k v

Regroup a product over a pairwise-disjoint union ⋃ᵥ J v of a function that is constant (= c v) on each block into ∏ᵥ (c v) ^ (k v), where k v is the block size (port of Lovasz.prod_biUnion_const).

theorem Graphon.CrossSuper.class_balance_two' {ι : Type u_1} {κ : Type u_2} {γ : Type u_3} [Fintype ι] [Fintype κ] [Fintype γ] (x : ι → γ → ℝ) (y : κ → γ → ℝ) (a : ι → ℝ) (b : κ → ℝ) (N : ℕ) (hNx : ∀ (c : γ), (Finset.image (fun (i : ι) => x i c) Finset.univ).card ≤ N) (hNy : ∀ (c : γ), (Finset.image (fun (j : κ) => y j c) Finset.univ).card ≤ N) (hmom : ∀ (k : γ → ℕ), (∀ (c : γ), k c < 2 * N) → ∑ i : ι, a i * ∏ c : γ, x i c ^ k c = ∑ j : κ, b j * ∏ c : γ, y j c ^ k c) (z : γ → ℝ) : ∑ i : ι with x i = z, a i = ∑ j : κ with y j = z, b j

class_balance_two over an arbitrary finite coordinate type (reindexed through Fintype.equivFin).

Aligned star moments and the weight balance

theorem Graphon.CrossSuper.exists_exponent_label_set {T T' K : ℕ} {J : Fin T → Finset (Fin K)} (hJcard : ∀ (v : Fin T), 2 * (T + T') ≤ (J v).card) (k : Fin T → ℕ) (hk : ∀ (v : Fin T), k v < 2 * (T + T')) : ∃ (Kf : Fin T → Finset (Fin K)), (∀ (v : Fin T), Kf v ⊆ J v) ∧ ∀ (v : Fin T), (Kf v).card = k v

Exponent label-set selection (port of Lovasz.exists_exponent_label_set): inside given blocks of size ≥ 2·(T+T'), select sub-blocks of exact sizes k v.

theorem Graphon.CrossSuper.fiber_blocks_pairwiseDisjoint {T K : ℕ} {ξ : Fin K → Fin T} {J : Fin T → Finset (Fin K)} (hsub : ∀ (v : Fin T), J v ⊆ {i : Fin K | ξ i = v}) : (↑Finset.univ).PairwiseDisjoint J

Blocks lying in distinct ξ-fibres are pairwise disjoint.

theorem Graphon.CrossSuper.aligned_star_moments {T T' K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (B' : Fin T' → Fin T' → ℝ) (W' : Fin T' → ℝ) (ξ : Fin K → Fin T) (ψ : Fin K → Fin T') (g : Fin T → Fin T') (J : Fin T → Finset (Fin K)) (hsub : ∀ (v : Fin T), J v ⊆ {i : Fin K | ξ i = v}) (hJcard : ∀ (v : Fin T), 2 * (T + T') ≤ (J v).card) (hconst : ∀ (v : Fin T), ∀ i ∈ J v, ψ i = g v) (hstar : ∀ (S : Finset (Fin K)), ∑ t : Fin T, W t * ∏ i ∈ S, B (ξ i) t = ∑ t' : Fin T', W' t' * ∏ i ∈ S, B' (ψ i) t') (k : Fin T → ℕ) (hk : ∀ (v : Fin T), k v < 2 * (T + T')) : ∑ t : Fin T, W t * ∏ v : Fin T, B v t ^ k v = ∑ t' : Fin T', W' t' * ∏ v : Fin T, B' (g v) t' ^ k v

Aligned star-moment bridge (port of Lovasz.aligned_moments_of_testEvalEq_super). With ξ ≡ v and ψ ≡ g v on each block J v, the star-test equalities specialize, for every bounded exponent vector k, to the aligned cross-moment identity.

noncomputable def Graphon.CrossSuper.matchClass {T T' : ℕ} (B : Fin T → Fin T → ℝ) (B' : Fin T' → Fin T' → ℝ) (g : Fin T → Fin T') (t : Fin T) : Finset (Fin T')

The matching class of a left vertex t: right vertices whose g-probed profile equals the column profile of t.

Equations

• Graphon.CrossSuper.matchClass B B' g t = {t' : Fin T' | ∀ (v : Fin T), B v t = B' (g v) t'}

theorem Graphon.CrossSuper.cross_weight_balance {T T' : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (B' : Fin T' → Fin T' → ℝ) (W' : Fin T' → ℝ) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) (g : Fin T → Fin T') (haligned : ∀ (k : Fin T → ℕ), (∀ (v : Fin T), k v < 2 * (T + T')) → ∑ t : Fin T, W t * ∏ v : Fin T, B v t ^ k v = ∑ t' : Fin T', W' t' * ∏ v : Fin T, B' (g v) t' ^ k v) (t : Fin T) : W t = ∑ t' ∈ matchClass B B' g t, W' t'

Weight balance (port of Lovasz.aligned_star_moments_weight_balance): left twin-freeness collapses the left profile level set to {t}, so the two-sided Vandermonde extraction reads W t = ∑_{t' ∈ matchClass t} W' t'.

Aligned edge moments and the pair balance

theorem Graphon.CrossSuper.aligned_edge_moments {T T' K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (B' : Fin T' → Fin T' → ℝ) (W' : Fin T' → ℝ) (ξ : Fin K → Fin T) (ψ : Fin K → Fin T') (g : Fin T → Fin T') (J : Fin T → Finset (Fin K)) (hsub : ∀ (v : Fin T), J v ⊆ {i : Fin K | ξ i = v}) (hJcard : ∀ (v : Fin T), 2 * (T + T') ≤ (J v).card) (hconst : ∀ (v : Fin T), ∀ i ∈ J v, ψ i = g v) (hedge : ∀ (Sₗ Sτ : Finset (Fin K)), ∑ t : Fin T, ∑ u : Fin T, (W t * W u * B t u * ∏ i ∈ Sₗ, B (ξ i) t) * ∏ i ∈ Sτ, B (ξ i) u = ∑ t' : Fin T', ∑ u' : Fin T', (W' t' * W' u' * B' t' u' * ∏ i ∈ Sₗ, B' (ψ i) t') * ∏ i ∈ Sτ, B' (ψ i) u') (k l : Fin T → ℕ) (hk : ∀ (v : Fin T), k v < 2 * (T + T')) (hl : ∀ (v : Fin T), l v < 2 * (T + T')) : ∑ x : Fin T, ∑ y : Fin T, (W x * W y * B x y * ∏ v : Fin T, B v x ^ k v) * ∏ v : Fin T, B v y ^ l v = ∑ x' : Fin T', ∑ y' : Fin T', (W' x' * W' y' * B' x' y' * ∏ v : Fin T, B' (g v) x' ^ k v) * ∏ v : Fin T, B' (g v) y' ^ l v

Aligned edge-moment bridge (port of Lovasz.aligned_edge_moments_of_testEvalEq_super). With ξ ≡ v and ψ ≡ g v on each block, the edge-test equalities specialize to the aligned cross pair-moment identity.

theorem Graphon.CrossSuper.cross_edge_balance {T T' : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (B' : Fin T' → Fin T' → ℝ) (W' : Fin T' → ℝ) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) (g : Fin T → Fin T') (haligned : ∀ (k l : Fin T → ℕ), (∀ (v : Fin T), k v < 2 * (T + T')) → (∀ (v : Fin T), l v < 2 * (T + T')) → ∑ x : Fin T, ∑ y : Fin T, (W x * W y * B x y * ∏ v : Fin T, B v x ^ k v) * ∏ v : Fin T, B v y ^ l v = ∑ x' : Fin T', ∑ y' : Fin T', (W' x' * W' y' * B' x' y' * ∏ v : Fin T, B' (g v) x' ^ k v) * ∏ v : Fin T, B' (g v) y' ^ l v) (t u : Fin T) : W t * W u * B t u = ∑ t' ∈ matchClass B B' g t, ∑ u' ∈ matchClass B B' g u, W' t' * W' u' * B' t' u'

Pair balance (port of Lovasz.aligned_edge_moments_pair_balance): left twin-freeness collapses the left pair level set to {(t, u)}, so the two-sided 2D Vandermonde extraction reads the block-averaged edge relation.

The partition deliverable

theorem Graphon.CrossSuper.cross_super_partition {T T' K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (B' : Fin T' → Fin T' → ℝ) (W' : Fin T' → ℝ) (hB_symm : ∀ (i j : Fin T), B i j = B j i) (hW_pos : ∀ (i : Fin T), 0 < W i) (hW'_pos : ∀ (i : Fin T'), 0 < W' i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) (hT' : 0 < T') (ξ : Fin K → Fin T) (ψ : Fin K → Fin T') (hsup : ∀ (v : Fin T), T' * (2 * (T + T')) ≤ {i : Fin K | ξ i = v}.card) (hmatch : ∀ (c : Lovasz.TestCoord K), Lovasz.testMoment B W c ξ = Lovasz.testMoment B' W' c ψ) : ∃ (C : Fin T → Finset (Fin T')), (∀ (t : Fin T), (C t).Nonempty) ∧ (∀ (t u : Fin T), t ≠ u → Disjoint (C t) (C u)) ∧ (∀ (t' : Fin T'), ∃ (t : Fin T), t' ∈ C t) ∧ (∀ (t : Fin T), W t = ∑ t' ∈ C t, W' t') ∧ ∀ (t u : Fin T), W t * W u * B t u = ∑ t' ∈ C t, ∑ u' ∈ C u, W' t' * W' u' * B' t' u'

Cross-matrix super partition (Cai–Govorov Lemma 5.1, two-matrix partition form). From matched test-moment profiles of a left tuple ξ with fibers of size ≥ T'·2·(T+T') and a right tuple ψ, the right vertex set partitions into classes C t (one per left vertex) with matching weights and block-averaged entries. Only LEFT twin-freeness is used.