Algebraic Determination for Finite Matrices

This file states the algebraic core of the inverse counting lemma: symmetric matrices with entries in [0,1] that yield equal weighted homomorphism sums for all finite graphs are related by a permutation of indices.

This is a purely finite, combinatorial statement with no measure theory.

Main definitions

• Graphon.weightedHomSum - Weighted homomorphism sum for a finite matrix

Main results

• Graphon.matrix_quotient_of_weightedHomSum_eq - Equal weighted hom sums imply quotient equivalence: matching block-constant type classes with equal weights (Lovász [2012] Theorem 5.30, correct weighted formulation)

References

• [L. Lovász, Large Networks and Graph Limits][lovasz2012], Section 5.2

Vandermonde corollary

Weighted homomorphism sum

noncomputable def Graphon.weightedHomSum {k : ℕ} (n : ℕ) (F : SimpleGraph (Fin n)) [DecidableRel F.Adj] (c : Fin k → Fin k → ℝ) (w : Fin k → ℝ) : ℝ

Weighted homomorphism sum for a finite matrix.

For a graph F on Fin n, a matrix c : Fin k → Fin k → ℝ, and weights w : Fin k → ℝ:

weightedHomSum n F c w = ∑ σ : Fin n → Fin k, (∏ v, w (σ v)) * ∏ e ∈ F.edgeFinset, c (σ e.1) (σ e.2)

This is the finite analog of graphon homomorphism density t(F, W), where c plays the role of the graphon kernel and w the cell measures.

Equations

• Graphon.weightedHomSum n F c w = ∑ σ : Fin n → Fin k, (∏ v : Fin n, w (σ v)) * ∏ e ∈ F.edgeFinset, c (σ (Quot.out e).1) (σ (Quot.out e).2)

theorem Graphon.weightedHomSum_congr_decRel {k : ℕ} (n : ℕ) (F : SimpleGraph (Fin n)) (inst₁ inst₂ : DecidableRel F.Adj) (c : Fin k → Fin k → ℝ) (w : Fin k → ℝ) : weightedHomSum n F c w = weightedHomSum n F c w

weightedHomSum is independent of the DecidableRel instance.

Weighted degree and star graphs

noncomputable def Graphon.wDeg {k : ℕ} (c : Fin k → Fin k → ℝ) (w : Fin k → ℝ) (i : Fin k) : ℝ

The weighted degree of index i in matrix c with weights w: wDeg c w i = ∑ j, w j * c i j.

Equations

• Graphon.wDeg c w i = ∑ j : Fin k, w j * c i j

def Graphon.starGraph (m : ℕ) : SimpleGraph (Fin (m + 1))

Star graph on m+1 vertices: vertex 0 is adjacent to vertices 1, ..., m.

Equations

• Graphon.starGraph m = { Adj := fun (u v : Fin (m + 1)) => u = 0 ∧ v ≠ 0 ∨ u ≠ 0 ∧ v = 0, symm := ⋯, loopless := ⋯ }

instance Graphon.starGraphDecRel (m : ℕ) : DecidableRel (starGraph m).Adj

Equations

• Graphon.starGraphDecRel m u v = inferInstanceAs (Decidable (u = 0 ∧ v ≠ 0 ∨ u ≠ 0 ∧ v = 0))

Row profile and permutation equivalence

noncomputable def Graphon.rowProfile {k : ℕ} (c : Fin k → Fin k → ℝ) (w : Fin k → ℝ) (i : Fin k) (m : ℕ) : ℝ

The row profile of index i captures all "higher-order degree" information: rowProfile c w i m = ∑ j, w j * c(i,j) * (wDeg c w j)^m.

Two indices i, i' have the same "type" iff rowProfile c w i = rowProfile c w i' for all m. The key property: caterpillar graph tests extract these profiles, and Vandermonde injectivity shows that matching profiles implies matching rows up to permutation within each type class.

Equations

• Graphon.rowProfile c w i m = ∑ j : Fin k, w j * c i j * Graphon.wDeg c w j ^ m

theorem Graphon.weightedHomSum_perm_eq {k : ℕ} (n : ℕ) (F : SimpleGraph (Fin n)) [DecidableRel F.Adj] (c : Fin k → Fin k → ℝ) (w : Fin k → ℝ) (π : Equiv.Perm (Fin k)) : (weightedHomSum n F (fun (i j : Fin k) => c ((Equiv.symm π) i) ((Equiv.symm π) j)) fun (i : Fin k) => w ((Equiv.symm π) i)) = weightedHomSum n F c w

weightedHomSum for a permuted matrix.

If π is a permutation, then evaluating weightedHomSum on the permuted matrix c' i j := c (π⁻¹ i) (π⁻¹ j) with permuted weights w' i := w (π⁻¹ i) gives the same result as the original.

This is the key equivariance property of the weighted hom sum.

Star graph formula

Double star graph and bivariate moments

def Graphon.doubleStarGraph (m p : ℕ) : SimpleGraph (Fin (m + p + 2))

Double star graph DS(m, p) on m + p + 2 vertices: vertex 0 is connected to vertex 1 (bridge) and to vertices 2, ..., m+1 (left leaves); vertex 1 is connected to vertices m+2, ..., m+p+1 (right leaves).

Equations

• One or more equations did not get rendered due to their size.

instance Graphon.doubleStarGraphDecRel (m p : ℕ) : DecidableRel (doubleStarGraph m p).Adj

Equations

• One or more equations did not get rendered due to their size.

Double star formula

Classwise row-profile moment extraction

Core proof for k > 0

Profile star graph and row-profile power moments

def Graphon.profileStarGraph (m r p : ℕ) : SimpleGraph (Fin (m + r * (p + 1) + 1))

Profile star graph PS(m, r, p) on m + r*(p+1) + 1 vertices.

Root (vertex 0) connects to m plain leaves (vertices 1..m) and r bridge vertices. Each bridge vertex connects to p branch leaves. This graph produces the weighted homomorphism sum ∑ i, w i * (wDeg c w i)^m * (rowProfile c w i p)^r.

Equations

• One or more equations did not get rendered due to their size.

instance Graphon.profileStarGraphDecRel (m r p : ℕ) : DecidableRel (profileStarGraph m r p).Adj

Equations

• One or more equations did not get rendered due to their size.

Multi-profile star graph and joint refinement

def Graphon.multiProfileStarGraph (m L : ℕ) (r p : Fin L → ℕ) : SimpleGraph (Fin (m + Graphon.multiProfileBranchTotal✝ L r p + 1))

Multi-profile star graph MPS(m, L, r, p) on m + ∑ l, r(l)*(p(l)+1) + 1 vertices.

Root (vertex 0) connects to m plain leaves and to r l bridge vertices for each type l. Each bridge of type l connects to p l branch leaves. This graph produces the weighted homomorphism sum ∑ i, w i * (wDeg c w i)^m * ∏ l, (rowProfile c w i (p l))^(r l).

Equations

• One or more equations did not get rendered due to their size.

instance Graphon.multiProfileStarGraphDecRel (m L : ℕ) (r p : Fin L → ℕ) : DecidableRel (multiProfileStarGraph m L r p).Adj

Equations

• One or more equations did not get rendered due to their size.

Hierarchical Vandermonde and joint class separation

Row-class machinery for collapse

Structural lemmas for collapsed matrix

Weighted hom sum is preserved by row collapse

1-labeled quantum graph evaluation

noncomputable def Graphon.rootedEval {k : ℕ} (n : ℕ) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (c : Fin k → Fin k → ℝ) (w : Fin k → ℝ) (i : Fin k) : ℝ

Rooted evaluation: fix vertex 0 at color i, sum over all colorings of non-root vertices. This is the "1-labeled" quantum graph evaluation from Lovász [2012] §5.2.

Equations

• Graphon.rootedEval n F c w i = ∑ σ : Fin n → Fin k, have τ := Fin.cons i σ; (∏ v : Fin n, w (σ v)) * ∏ e ∈ F.edgeFinset, c (τ (Quot.out e).1) (τ (Quot.out e).2)

Root attachment

Sorry targets: gluing and fullness

Gram matching and bijection construction

Twin-free bijection

Main theorem

theorem Graphon.matrix_quotient_of_weightedHomSum_eq {k : ℕ} (c c' : Fin k → Fin k → ℝ) (hc_symm : ∀ (i j : Fin k), c i j = c j i) (hc'_symm : ∀ (i j : Fin k), c' i j = c' j i) (hc_mem : ∀ (i j : Fin k), c i j ∈ Set.Icc 0 1) (hc'_mem : ∀ (i j : Fin k), c' i j ∈ Set.Icc 0 1) (w : Fin k → ℝ) (hw_pos : ∀ (i : Fin k), 0 < w i) (h_eq : ∀ (n : ℕ) (F : SimpleGraph (Fin n)) [inst : DecidableRel F.Adj], weightedHomSum n F c w = weightedHomSum n F c' w) : ∃ (T : ℕ) (type_c : Fin k → Fin T) (type_c' : Fin k → Fin T), (∀ (i₁ i₂ j₁ j₂ : Fin k), type_c i₁ = type_c i₂ → type_c j₁ = type_c j₂ → c i₁ j₁ = c i₂ j₂) ∧ (∀ (i₁ i₂ j₁ j₂ : Fin k), type_c' i₁ = type_c' i₂ → type_c' j₁ = type_c' j₂ → c' i₁ j₁ = c' i₂ j₂) ∧ (∀ (i j i' j' : Fin k), type_c i = type_c' i' → type_c j = type_c' j' → c i j = c' i' j') ∧ ∀ (t : Fin T), ∑ i : Fin k with type_c i = t, w i = ∑ i : Fin k with type_c' i = t, w i

Algebraic determination for finite matrices (quotient form).

If two symmetric matrices with entries in [0,1] have equal weighted homomorphism sums for ALL graphs on ALL vertex counts, then they have the same "type quotient": there exist type classification functions such that both matrices are block-constant on type classes, the block matrices agree, and the total weight per type class matches.

This is the correct formulation of Lovász [2012] Theorem 5.30 for the weighted setting. The permutation formulation (∃ π, c i j = c' (π i) (π j) ∧ w i = w (π i)) is false when type classes have different cardinalities but equal total weights. The quotient formulation is what's needed for the measure-theoretic inverse counting lemma, where atomless measures allow mass redistribution within type classes.

Proof outline (Lovász [2012], Section 5.2)

1. Star graph moment extraction: Testing with K_{1,m} yields degree moments.

2. Vandermonde argument (eq_zero_of_weighted_powers_eq_zero): From the moment equalities, deduce class weight matching for degree classes.

3. Caterpillar/multi-profile tests: Extract the full row profile via double star graphs and multi-profile stars. Hierarchical Vandermonde shows that the matrix is block-constant on type classes (defined by degree + all row profiles).

4. Cross-matrix matching: Show that the block matrices agree between c and c' by comparing conditional moments within each type class.