Lovász §3 — Connection-matrix algebra and the multigraph bridge

This module is forward-looking infrastructure for closing the canonical algebraic root in Graphon/MatrixDetermination.lean:

private theorem multiLabeledEvalK_tupleEquiv_invariant

at MatrixDetermination.lean:7150. That sorry is the precise Lovász TR-2004-82 §3 content: simple-graph tupleEquiv ⟹ all multigraph evaluations agree.

Module status

Scaffolding stage: this module mirrors the multigraph carrier (MultiLabeledGraph, multiLabeledEvalK, MultiLabeledGraph.ofSimple) from MatrixDetermination.lean and states the bridge theorem here as the canonical sorry. Other infrastructure stubs (algebra, trace operator, quotient) are listed but not yet declared.

Self-contained: imports only Mathlib basics, no Graphon.* dependencies. Can be developed independently.

Adapter pattern: when the bridge proof lands here, the MatrixDetermination.lean consumer call sites get updated to invoke Graphon.Lovasz.multiLabeledEvalK_tupleEquiv_invariant (after wiring through a small MultiLabeledGraph ↔ Graphon.Lovasz.MultiLabeledGraph adapter, since the types live in different namespaces).

Module structure (planned)

§1 — Multigraph carrier (DECLARED below)

• MultiLabeledGraph K n — structure with mult : Sym2 (Fin (n + K)) → ℕ and multNoLoop.
• multiLabeledEvalK — sum-over-σ of W-product times B-power-product.
• MultiLabeledGraph.ofSimple — embed a simple graph as a 0/1 multiplicity multigraph.
• multiLabeledEvalK_ofSimple — embedding preserves evaluation.

§2 — Algebra of multigraphs (Lovász's 𝒢_k) — STUBS

• MultiLabeledGraph.empty — empty multigraph (mult ≡ 0).
• MultiLabeledGraph.add — same-vertex pointwise addition.
• MultiLabeledGraph.glue — disjoint glue (Lovász's F₁F₂ product); analog of labeledEvalK_glue (~250 lines future work).
• multiLabeledEvalK_empty — empty evaluation = 1 (n = 0) or appropriate W-sum-product (n ≥ 1).
• multiLabeledEvalK_glue — glue evaluation factors as product.

§3 — Trace operator and quotient — STUBS

• multiLabeledEvalK.trace — fold last label into a new unlabeled.
• tupleEquivMulti — multigraph version of tupleEquiv.
• multiLabeledEvalK_trace_closure — Lovász eq. 6, page 7.

§4 — The bridge theorem (DECLARED, sorry'd)

• multiLabeledEvalK_tupleEquiv_invariant — bridge.

References

• Lovász, "The rank of connection matrices and the dimension of graph algebras", arXiv:math/0408232, Microsoft Research TR-2004-82, 2004.

§1 — Multigraph carrier

Design note (2026-05-17): the current MultiLabeledGraph carrier forbids self-loops via multNoLoop. This is a restriction relative to Lovász's full framework (TR-2004-82 §2, p. 3) where self-loops are allowed via edge-multiset semantics.

Why this matters for closing #62 and downstream:

• The IH-free versions of Claims 4.3/4.4 (needed for #70) require extracting B(ψ i, ψ i) = B(i, i) (diagonal preservation). With multNoLoop, this is NOT extractable even via multigraph evaluations. A self-loop at label-position i with multiplicity 1 evaluates to B(ξ i, ξ i) directly.
• Pointwise W-preservation W(ψ i) = W(i) requires either: (a) a W-factor at label vertices (our current eval only includes W at unlabeled), OR (b) a "vertex weight" multigraph operator analogous to self-loops.

Recommended next-session design (separate-carrier approach):

1. Add MultiLabeledGraphLoop K n carrier WITHOUT multNoLoop.
2. Define multiLabeledEvalKLoop mirror including B(τx, τx)^M.mult s(x,x).
3. Lift current MultiLabeledGraph content via injection MultiLabeledGraph → MultiLabeledGraphLoop. Existing #62 results transfer to no-loop multigraphs trivially.
4. State the full Lovász Theorem 2.2 over MultiLabeledGraphLoop: simple-graph h_simple ⟹ multi-loop evaluation equivalence.
5. Use specific self-loop multigraphs to extract B(ψ i, ψ i) = B(i, i) and derive IH-free Claims 4.3/4.4.

W-pointwise (W(ψ i) = W(i)) is a separate open design question:

• Current eval multiLabeledEvalK only includes W at UNLABELED vertices.
• Lovász's framework allows vertex weights α(v) at all vertices (with α(label) = 1 by convention in homomorphism counts).
• Extracting W(ψ i) for label i requires a different evaluator (e.g., with vertex weight at labels) or going through aut-from-orbit.
• Likely resolution: aut-from-orbit route — once we have orbit equivalence (via #70 closure with self-loops), aut preservation of W follows from IsWeightedAutomorphism.W_preserves. So W-pointwise is a CONSEQUENCE, not a primitive, of orbit equivalence.

Conclusion: extend with self-loop carrier first (Path A), defer W-pointwise as a downstream derivation.

structure Graphon.Lovasz.MultiLabeledGraph (K n : ℕ) : Type

• mult : Sym2 (Fin (n + K)) → ℕ
• multNoLoop (x : Fin (n + K)) : self.mult s(x, x) = 0

structure Graphon.Lovasz.MultiLabeledGraphLoop (K n : ℕ) : Type

Lovász k-labeled multigraph with self-loops on Fin (n + K).

Same as MultiLabeledGraph but WITHOUT the multNoLoop constraint. Allows self-loops s(x, x) to carry positive multiplicity, matching Lovász TR-2004-82 §2 (p. 3) "graphs" with edge-multiset semantics.

Used as the target carrier for the full rank theorem (closing #62's mult-≥-2 sub-case and unlocking IH-free Claims 4.3/4.4). See §1 design note above.

• mult : Sym2 (Fin (n + K)) → ℕ

def Graphon.Lovasz.MultiLabeledGraph.toLoop {K n : ℕ} (M : MultiLabeledGraph K n) : MultiLabeledGraphLoop K n

Inject MultiLabeledGraph into MultiLabeledGraphLoop (forget the multNoLoop constraint).

Equations

• M.toLoop = { mult := M.mult }

noncomputable def Graphon.Lovasz.multiLabeledEvalK {T : ℕ} (K n : ℕ) (M : MultiLabeledGraph K n) (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (φ : Fin K → Fin T) : ℝ

Multigraph evaluation at a labeled tuple φ : Fin K → Fin T.

Sum over unlabeled assignments σ : Fin n → Fin T of W-product times B-power-product (per Sym2-pair, raised to its multiplicity). Reduces to a simple-graph labeledEvalK when all multiplicities are 0 or 1 (see multiLabeledEvalK_ofSimple).

Equations

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

noncomputable def Graphon.Lovasz.multiLabeledEvalKLoop {T : ℕ} (K n : ℕ) (M : MultiLabeledGraphLoop K n) (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (φ : Fin K → Fin T) : ℝ

Multigraph evaluation with self-loops.

Mirror of multiLabeledEvalK for MultiLabeledGraphLoop. The B^mult product runs over the FULL Sym2 (Fin (n + K)), including diagonal pairs s(x, x) which contribute B(τ x, τ x)^M.mult s(x, x).

When M.mult s(x, x) = 0 for all x (i.e., M = M_noLoop.toLoop for some M_noLoop : MultiLabeledGraph), this reduces to multiLabeledEvalK (see multiLabeledEvalKLoop_of_toLoop).

Equations

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

theorem Graphon.Lovasz.multiLabeledEvalKLoop_of_toLoop {T K n : ℕ} (M : MultiLabeledGraph K n) (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (φ : Fin K → Fin T) : multiLabeledEvalKLoop K n M.toLoop B W φ = multiLabeledEvalK K n M B W φ

No-loop reduction: when injected from MultiLabeledGraph, the loop-aware evaluator agrees with multiLabeledEvalK (diagonal terms contribute B^0 = 1).

theorem Graphon.Lovasz.multiLabeledEvalKLoop_aut_invariant {T K n : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (M : MultiLabeledGraphLoop K n) (σ : Equiv.Perm (Fin T)) (hσ_W : ∀ (i : Fin T), W (σ i) = W i) (hσ_B : ∀ (i j : Fin T), B (σ i) (σ j) = B i j) (φ : Fin K → Fin T) : multiLabeledEvalKLoop K n M B W (⇑σ ∘ φ) = multiLabeledEvalKLoop K n M B W φ

Automorphism invariance of multiLabeledEvalKLoop.

Mirrors multiLabeledEvalK_aut_invariant. The proof transfers directly because the only difference is the domain of the Sym2 product (with vs without diagonals), and hσ_B applies uniformly to diagonal pairs too.

theorem Graphon.Lovasz.multiLabeledEvalKLoop_orbit_invariant {T K n : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (M : MultiLabeledGraphLoop K n) {ξ ξ' : Fin K → Fin T} (h : ∃ (σ : Equiv.Perm (Fin T)), (∀ (i : Fin T), W (σ i) = W i) ∧ (∀ (i j : Fin T), B (σ i) (σ j) = B i j) ∧ ∀ (i : Fin K), ξ' i = σ (ξ i)) : multiLabeledEvalKLoop K n M B W ξ = multiLabeledEvalKLoop K n M B W ξ'

Orbit invariance of multiLabeledEvalKLoop (corollary).

theorem Graphon.Lovasz.multiLabeledEvalKLoop_n_zero_of_diag {T K : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (M : MultiLabeledGraphLoop K 0) {ξ ξ' : Fin K → Fin T} (h_offdiag : ∀ (a b : Fin K), a ≠ b → B (ξ a) (ξ b) = B (ξ' a) (ξ' b)) (h_diag : ∀ (a : Fin K), B (ξ a) (ξ a) = B (ξ' a) (ξ' a)) : multiLabeledEvalKLoop K 0 M B W ξ = multiLabeledEvalKLoop K 0 M B W ξ'

Loop n=0 bridge (step 4 of #79). At n = 0, the loop multigraph evaluation is a product of B-power factors over Sym2 (Fin K), including diagonal pairs s(a, a) weighted by their multiplicity. Equality between ξ and ξ' holds given:

• per-pair B-equality at non-diagonal label positions (h_offdiag, derivable from tupleEquivSimple), and
• per-vertex diagonal observable (h_diag, the data needed beyond simple-graph equivalence — supplied by the rank theorem).

This isolates the diagonal observable as the SOLE additional input needed for the n=0 loop case.

noncomputable def Graphon.Lovasz.MultiLabeledGraph.ofSimple {K n : ℕ} (F : SimpleGraph (Fin (n + K))) [DecidableRel F.Adj] : MultiLabeledGraph K n

Simple-graph embedding into the multigraph carrier.

For any F : SimpleGraph (Fin (n + K)) with decidable adjacency, the 0/1-multiplicity multigraph has mult e = if e ∈ F.edgeFinset then 1 else 0. multNoLoop follows from SimpleGraph.loopless.

Equations

• Graphon.Lovasz.MultiLabeledGraph.ofSimple F = { mult := fun (e : Sym2 (Fin (n + K))) => if e ∈ F.edgeFinset then 1 else 0, multNoLoop := ⋯ }

theorem Graphon.Lovasz.multiLabeledEvalK_ofSimple {T K n : ℕ} (F : SimpleGraph (Fin (n + K))) [DecidableRel F.Adj] (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (φ : Fin K → Fin T) : multiLabeledEvalK K n (MultiLabeledGraph.ofSimple F) B W φ = ∑ σ : Fin n → Fin T, have τ := fun (v : Fin (n + K)) => if h : ↑v < K then φ ⟨↑v, h⟩ else σ ⟨↑v - K, ⋯⟩; (∏ v : Fin n, W (σ v)) * ∏ e ∈ F.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)

multiLabeledEvalK of ofSimple F matches the simple-graph σ-sum body (the analog of MatrixDetermination.lean:7156).

The 0/1-multigraph evaluation reduces to the simple-graph form:

• For e ∈ F.edgeFinset: B^1 = B (factor present).
• For e ∉ F.edgeFinset: B^0 = 1 (no contribution).

The RHS is the simple-graph evaluation pattern (analog of labeledEvalK F); its product is over F.edgeFinset rather than all of Sym2.

§2 — Algebra of multigraphs (Lovász's 𝒢_k)

Bounded building blocks: empty, add (same-vertex pointwise addition), and the basic multiLabeledEvalK_empty reduction. The heavyweight glue (Lovász's F₁F₂ product, disjoint union of unlabeled vertices) is deferred to a future session — it requires a multigraph analog of labeledEvalK_glue (~250 lines).

The corresponding evaluation factorization for add is non-trivial even at the same vertex set (W-product gets squared), so it's treated as a separate algebra step coupled with the disjoint-glue construction in Lovász's framework. Stub theorems are listed in module docstring above.

def Graphon.Lovasz.MultiLabeledGraph.empty (K n : ℕ) : MultiLabeledGraph K n

The empty multigraph: zero multiplicity on every Sym2-pair.

Equations

• Graphon.Lovasz.MultiLabeledGraph.empty K n = { mult := fun (x : Sym2 (Fin (n + K))) => 0, multNoLoop := ⋯ }

def Graphon.Lovasz.MultiLabeledGraph.add {K n : ℕ} (M₁ M₂ : MultiLabeledGraph K n) : MultiLabeledGraph K n

Pointwise addition of multiplicities (same vertex set). The addition operation in the quantum-graph algebra 𝒢_k at fixed unlabeled-vertex count.

Equations

• M₁.add M₂ = { mult := fun (e : Sym2 (Fin (n + K))) => M₁.mult e + M₂.mult e, multNoLoop := ⋯ }

theorem Graphon.Lovasz.multiLabeledEvalK_perSym2_add {T K n : ℕ} (B : Fin T → Fin T → ℝ) (M₁ M₂ : MultiLabeledGraph K n) (τ : Fin (n + K) → Fin T) : ∏ e : Sym2 (Fin (n + K)), B (τ (Quot.out e).1) (τ (Quot.out e).2) ^ (M₁.add M₂).mult e = (∏ e : Sym2 (Fin (n + K)), B (τ (Quot.out e).1) (τ (Quot.out e).2) ^ M₁.mult e) * ∏ e : Sym2 (Fin (n + K)), B (τ (Quot.out e).1) (τ (Quot.out e).2) ^ M₂.mult e

Per-Sym2 add factorization: for ANY function τ, the product over Sym2 of B(τ ·)(τ ·) ^ (M₁.mult + M₂.mult) factors as the product of B^M₁.mult and B^M₂.mult.

theorem Graphon.Lovasz.multiLabeledEvalK_empty {T K n : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (φ : Fin K → Fin T) : multiLabeledEvalK K n (MultiLabeledGraph.empty K n) B W φ = ∑ σ : Fin n → Fin T, ∏ v : Fin n, W (σ v)

Empty multigraph evaluation: every B-power factor is B^0 = 1, so the σ-sum body collapses to the W-product.

theorem Graphon.Lovasz.multiLabeledEvalK_add_perσ {T K n : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (M₁ M₂ : MultiLabeledGraph K n) (φ : Fin K → Fin T) : multiLabeledEvalK K n (M₁.add M₂) B W φ = ∑ σ : Fin n → Fin T, have τ := fun (v : Fin (n + K)) => if h : ↑v < K then φ ⟨↑v, h⟩ else σ ⟨↑v - K, ⋯⟩; (∏ v : Fin n, W (σ v)) * ((∏ e : Sym2 (Fin (n + K)), B (τ (Quot.out e).1) (τ (Quot.out e).2) ^ M₁.mult e) * ∏ e : Sym2 (Fin (n + K)), B (τ (Quot.out e).1) (τ (Quot.out e).2) ^ M₂.mult e)

Same-vertex add factorization (general n).

For any pair M₁ M₂ : MultiLabeledGraph K n, the multigraph evaluation of M₁.add M₂ does NOT factor as the product of evaluations in general: the W-product gets shared once but the B-product factors via pow_add. Compare with Lovász's F₁F₂ product (disjoint glue), which DOES factor cleanly.

Result: per-σ factorization holds, but the σ-sum doesn't distribute.

§3 — Disjoint-glue product (Lovász's F₁F₂)

The disjoint-glue product is the multiplication operation in the quantum-graph algebra 𝒢_k. Vertex space: Fin ((n₁ + n₂) + K). Labels (val < K) are shared. M₁'s unlabeled occupy positions K..K+n₁-1; M₂'s unlabeled occupy positions K+n₁..K+n₁+n₂-1.

Multiplicity at e ∈ Sym2(Fin ((n₁+n₂)+K)):

• Label-label (both endpoints val < K): M₁.mult e + M₂.mult e (using Sym2.map identity-on-labels embeddings).
• M₁-only (both endpoints val < K + n₁, not both labels): M₁.mult of the lift via emb₁.
• M₂-only (both endpoints val < K or val ≥ K + n₁): M₂.mult of the lift via emb₂.
• Cross (one M₁-unlabeled, one M₂-unlabeled): 0.

def Graphon.Lovasz.glueCast₁ (K n₁ n₂ : ℕ) (v : Fin (n₁ + n₂ + K)) : Option (Fin (n₁ + K))

M₁-side cast: project a vertex v : Fin ((n₁+n₂)+K) into Fin (n₁+K) when its val lies in M₁'s scope (i.e. val < n₁+K). Returns none for M₂-unlabeled vertices (val ≥ n₁+K).

Equations

• Graphon.Lovasz.glueCast₁ K n₁ n₂ v = if h : ↑v < n₁ + K then some ⟨↑v, h⟩ else none

def Graphon.Lovasz.glueCast₂ (K n₁ n₂ : ℕ) (v : Fin (n₁ + n₂ + K)) : Option (Fin (n₂ + K))

M₂-side cast: project a vertex v : Fin ((n₁+n₂)+K) into Fin (n₂+K) when its val is either a label (val < K, mapped to itself) or M₂-unlabeled (val ≥ n₁+K, shifted back by n₁). Returns none for M₁-unlabeled vertices.

Equations

• Graphon.Lovasz.glueCast₂ K n₁ n₂ v = if h : ↑v < K then some ⟨↑v, ⋯⟩ else if h2 : ↑v ≥ n₁ + K then some ⟨↑v - n₁, ⋯⟩ else none

def Graphon.Lovasz.MultiLabeledGraph.glue {K n₁ n₂ : ℕ} (M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) : MultiLabeledGraph K (n₁ + n₂)

Disjoint glue of two k-labeled multigraphs (Lovász's F₁F₂ product).

Vertex space Fin ((n₁+n₂)+K): labels at positions 0..K-1 (shared); M₁'s unlabeled at K..K+n₁-1; M₂'s unlabeled at K+n₁..K+n₁+n₂-1. Multiplicity at e adds the M₁-contribution (when both endpoints are in M₁'s scope) and the M₂-contribution (when both endpoints are labels or in M₂'s shifted unlabeled range). Cross-type pairs (one M₁-unlabeled, one M₂-unlabeled) contribute 0.

Equations

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

theorem Graphon.Lovasz.MultiLabeledGraph.glue_mult_pair {K n₁ n₂ : ℕ} (M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (a b : Fin (n₁ + n₂ + K)) : (M₁.glue M₂).mult s(a, b) = (match glueCast₁ K n₁ n₂ a, glueCast₁ K n₁ n₂ b with | some u', some v' => M₁.mult s(u', v') | x, x_1 => 0) + match glueCast₂ K n₁ n₂ a, glueCast₂ K n₁ n₂ b with | some u', some v' => M₂.mult s(u', v') | x, x_1 => 0

Unfold lemma for MultiLabeledGraph.glue.mult at an unordered pair s(a, b).

def Graphon.Lovasz.glueEmb₁ (K n₁ n₂ : ℕ) : Fin (n₁ + K) ↪ Fin (n₁ + n₂ + K)

Identity-on-labels embedding Fin (n₁ + K) ↪ Fin ((n₁ + n₂) + K).

Equations

• Graphon.Lovasz.glueEmb₁ K n₁ n₂ = { toFun := fun (v : Fin (n₁ + K)) => ⟨↑v, ⋯⟩, inj' := ⋯ }

def Graphon.Lovasz.glueEmb₂ (K n₁ n₂ : ℕ) : Fin (n₂ + K) ↪ Fin (n₁ + n₂ + K)

Embedding Fin (n₂ + K) ↪ Fin ((n₁ + n₂) + K): labels (val < K) are preserved; M₂'s unlabeled vertices (val ≥ K) are shifted by n₁.

Equations

• Graphon.Lovasz.glueEmb₂ K n₁ n₂ = { toFun := fun (v : Fin (n₂ + K)) => if h : ↑v < K then ⟨↑v, ⋯⟩ else ⟨n₁ + ↑v, ⋯⟩, inj' := ⋯ }

@[simp]

theorem Graphon.Lovasz.glueCast₁_glueEmb₁ (K n₁ n₂ : ℕ) (v : Fin (n₁ + K)) : glueCast₁ K n₁ n₂ ((glueEmb₁ K n₁ n₂) v) = some v

glueCast₁ K n₁ n₂ (glueEmb₁ K n₁ n₂ v) = some v.

@[simp]

theorem Graphon.Lovasz.glueCast₂_glueEmb₂ (K n₁ n₂ : ℕ) (v : Fin (n₂ + K)) : glueCast₂ K n₁ n₂ ((glueEmb₂ K n₁ n₂) v) = some v

glueCast₂ K n₁ n₂ (glueEmb₂ K n₁ n₂ v) = some v.

theorem Graphon.Lovasz.glueCast₁_of_val_lt (K n₁ n₂ : ℕ) (v : Fin (n₁ + n₂ + K)) (h : ↑v < n₁ + K) : glueCast₁ K n₁ n₂ v = some ⟨↑v, h⟩

For an M₁-side vertex (val < n₁ + K), glueCast₁ evaluated at it is some of its restriction. Allows treating M₁-only positions explicitly.

theorem Graphon.Lovasz.glueCast₂_of_val_ge (K n₁ n₂ : ℕ) (v : Fin (n₁ + n₂ + K)) (h : ↑v ≥ n₁ + K) : glueCast₂ K n₁ n₂ v = some ⟨↑v - n₁, ⋯⟩

For an M₂-unlabeled vertex (val ≥ n₁ + K), glueCast₂ returns some ⟨v.val - n₁, _⟩.

theorem Graphon.Lovasz.glueCast₂_of_label (K n₁ n₂ : ℕ) (v : Fin (n₁ + n₂ + K)) (h : ↑v < K) : glueCast₂ K n₁ n₂ v = some ⟨↑v, ⋯⟩

For a label vertex (val < K), glueCast₂ returns some ⟨v.val, _⟩.

theorem Graphon.Lovasz.glueCast₂_of_M1_unlabeled (K n₁ n₂ : ℕ) (v : Fin (n₁ + n₂ + K)) (hge : ↑v ≥ K) (hlt : ↑v < n₁ + K) : glueCast₂ K n₁ n₂ v = none

For an M₁-unlabeled vertex (K ≤ val < n₁ + K), glueCast₂ returns none.

theorem Graphon.Lovasz.glueCast₁_of_M2_unlabeled (K n₁ n₂ : ℕ) (v : Fin (n₁ + n₂ + K)) (h : ↑v ≥ n₁ + K) : glueCast₁ K n₁ n₂ v = none

For an M₂-unlabeled vertex (val ≥ n₁ + K), glueCast₁ returns none.

def Graphon.Lovasz.gluePart₁ {K n₁ n₂ : ℕ} (M₁ : MultiLabeledGraph K n₁) (_M₂ : MultiLabeledGraph K n₂) (e : Sym2 (Fin (n₁ + n₂ + K))) : ℕ

The first additive part of (M₁.glue M₂).mult: contribution from M₁ (zero outside M₁'s scope, computed via glueCast₁).

Equations

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

def Graphon.Lovasz.gluePart₂ {K n₁ n₂ : ℕ} (_M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (e : Sym2 (Fin (n₁ + n₂ + K))) : ℕ

The second additive part of (M₁.glue M₂).mult: contribution from M₂ (zero outside M₂'s scope, computed via glueCast₂).

Equations

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

theorem Graphon.Lovasz.MultiLabeledGraph.glue_mult_eq_add {K n₁ n₂ : ℕ} (M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (e : Sym2 (Fin (n₁ + n₂ + K))) : (M₁.glue M₂).mult e = gluePart₁ M₁ M₂ e + gluePart₂ M₁ M₂ e

(M₁.glue M₂).mult = gluePart₁ + gluePart₂.

theorem Graphon.Lovasz.gluePart₁_emb₁ {K n₁ n₂ : ℕ} (M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (a b : Fin (n₁ + K)) : gluePart₁ M₁ M₂ s((glueEmb₁ K n₁ n₂) a, (glueEmb₁ K n₁ n₂) b) = M₁.mult s(a, b)

gluePart₁ evaluated at (glueEmb₁ a, glueEmb₁ b) returns M₁.mult s(a, b).

theorem Graphon.Lovasz.gluePart₂_emb₂ {K n₁ n₂ : ℕ} (M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (a b : Fin (n₂ + K)) : gluePart₂ M₁ M₂ s((glueEmb₂ K n₁ n₂) a, (glueEmb₂ K n₁ n₂) b) = M₂.mult s(a, b)

gluePart₂ evaluated at (glueEmb₂ a, glueEmb₂ b) returns M₂.mult s(a, b).

theorem Graphon.Lovasz.gluePart₁_eq_zero_of_not_mem_image {K n₁ n₂ : ℕ} (M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (e : Sym2 (Fin (n₁ + n₂ + K))) (h : ¬∃ (e' : Sym2 (Fin (n₁ + K))), Sym2.map (⇑(glueEmb₁ K n₁ n₂)) e' = e) : gluePart₁ M₁ M₂ e = 0

gluePart₁ is zero outside the image of glueEmb₁.sym2Map.

theorem Graphon.Lovasz.gluePart₂_eq_zero_of_not_mem_image {K n₁ n₂ : ℕ} (M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (e : Sym2 (Fin (n₁ + n₂ + K))) (h : ¬∃ (e' : Sym2 (Fin (n₂ + K))), Sym2.map (⇑(glueEmb₂ K n₁ n₂)) e' = e) : gluePart₂ M₁ M₂ e = 0

gluePart₂ is zero outside the image of glueEmb₂.sym2Map.

theorem Graphon.Lovasz.multiLabeledEvalK_glue {T K n₁ n₂ : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (φ : Fin K → Fin T) : multiLabeledEvalK K (n₁ + n₂) (M₁.glue M₂) B W φ = multiLabeledEvalK K n₁ M₁ B W φ * multiLabeledEvalK K n₂ M₂ B W φ

Disjoint glue factorization of multigraph evaluations.

Lovász's F₁F₂ product (multigraph version): the evaluation of a glued multigraph factors as the product of evaluations. Generalizes labeledEvalK_glue from SimpleGraph to MultiLabeledGraph (with multiplicities). The proof factors over σ-sums via sum_piFinAdd_factor, the W-products via Fin.prod_univ_add, and the Sym2 B-products via pow_add + prod_Sym2_embᵢ_factor.

§3.5 — Trace operator (Lovász eq. 6)

def Graphon.Lovasz.MultiLabeledGraph.trace {K n : ℕ} (M : MultiLabeledGraph (K + 1) n) : MultiLabeledGraph K (n + 1)

Trace operator on multigraphs. Folds the last label of a (K+1)-labeled multigraph into a new unlabeled vertex, yielding a K-labeled multigraph with n + 1 unlabeled vertices.

Vertex spaces Fin (n + (K + 1)) and Fin ((n + 1) + K) have the same cardinality; the multiplicity is pulled back via the val-preserving Fin.cast.

Equations

• M.trace = { mult := fun (e : Sym2 (Fin (n + 1 + K))) => M.mult (Sym2.map (Fin.cast ⋯) e), multNoLoop := ⋯ }

def Graphon.Lovasz.MultiLabeledGraph.promote {K n : ℕ} (M : MultiLabeledGraph K (n + 1)) : MultiLabeledGraph (K + 1) n

Promotion (section of trace): from MultiLabeledGraph K (n+1) build MultiLabeledGraph (K+1) n by reindexing the val-equal vertex space via the inverse cast. Round-trip property: M.promote.trace = M (definitionally up to Sym2.map_id).

Equations

• M.promote = { mult := fun (e : Sym2 (Fin (n + (K + 1)))) => M.mult (Sym2.map (Fin.cast ⋯) e), multNoLoop := ⋯ }

theorem Graphon.Lovasz.MultiLabeledGraph.trace_promote {K n : ℕ} (M : MultiLabeledGraph K (n + 1)) : M.promote.trace = M

Trace-promote round-trip: closing the last label of a promoted multigraph recovers the original. Both sides have val-equal vertex spaces Fin ((n+1)+K); multiplicities agree pointwise via the cast composition identity.

theorem Graphon.Lovasz.multiLabeledEvalK_sum_last_label {T K n : ℕ} (M : MultiLabeledGraph (K + 1) n) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (φ : Fin K → Fin T) : ∑ t : Fin T, W t * multiLabeledEvalK (K + 1) n M B W (Fin.snoc φ t) = multiLabeledEvalK K (n + 1) M.trace B W φ

Trace-closure identity (Lovász eq. 6, p. 7).

Summing multiLabeledEvalK (K+1) n M B W over the last label t of a (K+1)-tuple Fin.snoc φ t, weighted by W(t), equals multiLabeledEvalK K (n+1) M.trace B W φ — i.e., closing the last label into a new unlabeled vertex.

Multigraph analog of labeledEvalK_sum_last_label (MatrixDetermination.lean:4906). Requires B symmetric since the vertex-space cast Fin ((n+1)+K) ↔ Fin (n+(K+1)) reindexes Sym2 pairs through Sym2.map (Fin.cast _) and Quot.out may pick swapped orientations.

theorem Graphon.Lovasz.multiLabeledEvalK_promote_unfold {T K n : ℕ} (M : MultiLabeledGraph K (n + 1)) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (ξ : Fin K → Fin T) : multiLabeledEvalK K (n + 1) M B W ξ = ∑ t : Fin T, W t * multiLabeledEvalK (K + 1) n M.promote B W (Fin.snoc ξ t)

Promote-unfolding identity: a multigraph evaluation at level (K, n+1) unfolds into a W-weighted sum (over the value t of the new label) of the promoted multigraph at level (K+1, n). Direct corollary of multiLabeledEvalK_sum_last_label and MultiLabeledGraph.trace_promote.

§3.5 — Automorphism-invariance of multigraph evaluation

A bounded preliminary: any (B, W)-automorphism σ : Fin T ≃ Fin T acts trivially on multigraph evaluations (substitute τ ∘ σ in the σ-sum). This is the standard symmetry observation, NOT the bridge content (which would say simple-graph tupleEquiv implies multi evaluations agree).

The orbit-based corollary: if ξ' = σ ∘ ξ for some aut σ, then multiEval M ξ = multiEval M ξ'. This is bounded (~30 lines) and serves as a stepping-stone for the full bridge.

theorem Graphon.Lovasz.multiLabeledEvalK_aut_invariant {T K n : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (M : MultiLabeledGraph K n) (σ : Equiv.Perm (Fin T)) (hσ_W : ∀ (i : Fin T), W (σ i) = W i) (hσ_B : ∀ (i j : Fin T), B (σ i) (σ j) = B i j) (φ : Fin K → Fin T) : multiLabeledEvalK K n M B W (⇑σ ∘ φ) = multiLabeledEvalK K n M B W φ

Automorphism invariance of multiLabeledEvalK.

If σ : Fin T ≃ Fin T is a (B, W)-automorphism (preserves W and B), then for any multigraph M and any labeled tuple φ, multiLabeledEvalK M (σ ∘ φ) = multiLabeledEvalK M φ.

theorem Graphon.Lovasz.multiLabeledEvalK_orbit_invariant {T K n : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (M : MultiLabeledGraph K n) {ξ ξ' : Fin K → Fin T} (h : ∃ (σ : Equiv.Perm (Fin T)), (∀ (i : Fin T), W (σ i) = W i) ∧ (∀ (i j : Fin T), B (σ i) (σ j) = B i j) ∧ ∀ (i : Fin K), ξ' i = σ (ξ i)) : multiLabeledEvalK K n M B W ξ = multiLabeledEvalK K n M B W ξ'

Orbit-based invariance: corollary of multiLabeledEvalK_aut_invariant. If ξ' = σ ∘ ξ for some (B, W)-automorphism σ, multigraph evaluations agree.

theorem Graphon.Lovasz.multiLabeledEvalK_tupleEquiv_invariant_n_zero {T K : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (M : MultiLabeledGraph K 0) {ξ ξ' : Fin K → Fin T} (h_simple : ∀ (n' : ℕ) (F : SimpleGraph (Fin (n' + K))) [inst : DecidableRel F.Adj], (∑ σ : Fin n' → Fin T, have τ := fun (v : Fin (n' + K)) => if h : ↑v < K then ξ ⟨↑v, h⟩ else σ ⟨↑v - K, ⋯⟩; (∏ v : Fin n', W (σ v)) * ∏ e ∈ F.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) = ∑ σ : Fin n' → Fin T, have τ := fun (v : Fin (n' + K)) => if h : ↑v < K then ξ' ⟨↑v, h⟩ else σ ⟨↑v - K, ⋯⟩; (∏ v : Fin n', W (σ v)) * ∏ e ∈ F.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) : multiLabeledEvalK K 0 M B W ξ = multiLabeledEvalK K 0 M B W ξ'

Bridge for n = 0 (label-only multigraphs). The simplest non-trivial case: when M has no unlabeled vertices, multiLabeledEvalK reduces to a product of B-power factors over Sym2 (Fin K). The simple-graph tupleEquiv hypothesis (h_simple) applied to single-edge graphs gives B-equality at each non-loop pair, and multNoLoop handles the diagonal.

theorem Graphon.Lovasz.multiLabeledEvalK_tupleEquiv_invariant {T K n : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (M : MultiLabeledGraph K n) {ξ ξ' : Fin K → Fin T} (h_simple : ∀ (n' : ℕ) (F : SimpleGraph (Fin (n' + K))) [inst : DecidableRel F.Adj], (∑ σ : Fin n' → Fin T, have τ := fun (v : Fin (n' + K)) => if h : ↑v < K then ξ ⟨↑v, h⟩ else σ ⟨↑v - K, ⋯⟩; (∏ v : Fin n', W (σ v)) * ∏ e ∈ F.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) = ∑ σ : Fin n' → Fin T, have τ := fun (v : Fin (n' + K)) => if h : ↑v < K then ξ' ⟨↑v, h⟩ else σ ⟨↑v - K, ⋯⟩; (∏ v : Fin n', W (σ v)) * ∏ e ∈ F.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) : multiLabeledEvalK K n M B W ξ = multiLabeledEvalK K n M B W ξ'

The multigraph bridge — SECONDARY paper root (general, non-twin-free version).

Dependency hierarchy (post-2026-05-12 architectural decision):

• PRIMARY ROOT: connection_matrix_rank_theorem at L3018 (Lovász §3 Theorem 2.2, simple-graph form, requires twin-free).
• SECONDARY: this bridge (no twin-free hypothesis; strictly stronger statement).

For the twin-free version that downstream consumers actually need, use multiLabeledEvalK_tupleEquiv_invariant_twinFree (already proved modulo connection_matrix_rank_theorem). This general bridge can be treated as off-axis if all consumers can use the twin-free variant.

Every multigraph evaluation descends through the simple-graph version of tupleEquiv. This is the Lovász §3 content (Theorem 2.2 / Lemma 2.5) translated to our framework: simple-graph tupleEquiv ⟹ all multigraph evaluations agree.

Hypothesis form (h_simple): for every level-K simple graph F : SimpleGraph (Fin (n' + K)) (with any n' unlabeled vertices), the simple-graph evaluations at ξ and ξ' agree. This is the inlined definition of tupleEquiv B W ξ ξ'.

Status (2026-05-17): designated PRIMARY PAPER-ROOT theorem (Lovász TR-2004-82 Theorem 2.2 / Lemma 2.5 content). The n = 0 case is dispatched via multiLabeledEvalK_tupleEquiv_invariant_n_zero. The general n case requires the connection-matrix / idempotent- decomposition argument from Lovász §3 — substantial spectral/rank infrastructure (~300-500 LOC) beyond a quick closure. Natural induction on n via promote_unfold needs a "lifted simple-equivalence" hypothesis at level K + 1, which does NOT follow from the level-K h_simple alone.

Downstream impact (closes #62 ⟹ unlocks):

• IH-free Claims 4.3/4.4 (via multigraph evaluations giving B-diagonal + W-pointwise data, currently unavailable in simple-graph framework alone).
• Task #70 (orbit_separation_by_simple_graph).
• Remaining MatrixDetermination chain.

Treat as foundational citation for downstream consumers until a dedicated paper-root formalization project is undertaken.

§3.8 — Equivalence predicates and Lovász Lemma 2.5

This section introduces the two equivalence relations on label-tuples that bracket the bridge theorem:

• tupleEquivSimple — agreement of all simple-graph evaluations (Lovász TR-2004-82 §2, p. 6). This is the simple-graph tupleEquiv inlined here so this module needs no dependency on Graphon/MatrixDetermination.lean.
• tupleEquivMulti — agreement of all multigraph evaluations (the natural multigraph generalization).

The bridge theorem (§4 below) is exactly tupleEquivSimple → tupleEquivMulti. The reverse direction tupleEquivMulti → tupleEquivSimple is trivial because multiLabeledEvalK of MultiLabeledGraph.ofSimple F recovers the simple-graph evaluation (multiLabeledEvalK_ofSimple).

Lovász Lemma 2.5 (informal): if B is twin-free, then tupleEquivMulti ξ ξ' if and only if ξ and ξ' lie in the same (B, W)-automorphism orbit.

• The forward direction (orbit ⟹ multi-equivalence) is the trivial corollary multiLabeledEvalK_orbit_invariant (already proved above): aut-invariance of multigraph evaluation gives equality on every multigraph automatically.
• The reverse direction (multi-equivalence ⟹ orbit) is the deep paper content. Lovász's proof goes through the connection-matrix rank / idempotent decomposition argument (TR-2004-82 §3): the connection matrix M(B, W) ∈ ℝ^{T^k × T^k} factors through twin-free quotients, and equal multi-eval rows are exactly orbit equivalences.

def Graphon.Lovasz.tupleEquivSimple {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (ξ ξ' : Fin K → Fin T) : Prop

Simple-graph tuple equivalence (Lovász §2, p. 6).

Two label maps ξ, ξ' : Fin K → Fin T are simple-equivalent iff every level-K simple graph (with any number n' of unlabeled vertices) evaluates equally on them. This is the simple-graph tupleEquiv inlined to avoid a MatrixDetermination dependency.

Equations

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

def Graphon.Lovasz.tupleEquivMulti {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (ξ ξ' : Fin K → Fin T) : Prop

Multigraph tuple equivalence.

Two label maps ξ, ξ' : Fin K → Fin T are multi-equivalent iff every level-K multigraph (with any number n of unlabeled vertices) evaluates equally on them. This is the natural multigraph generalization of tupleEquivSimple.

Equations

• Graphon.Lovasz.tupleEquivMulti B W ξ ξ' = ∀ (n : ℕ) (M : Graphon.Lovasz.MultiLabeledGraph K n), Graphon.Lovasz.multiLabeledEvalK K n M B W ξ = Graphon.Lovasz.multiLabeledEvalK K n M B W ξ'

def Graphon.Lovasz.tupleEquivLoop {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (ξ ξ' : Fin K → Fin T) : Prop

Loop-multigraph tuple equivalence.

Two label maps ξ, ξ' : Fin K → Fin T are loop-multi-equivalent iff every level-K multigraph with self-loops evaluates equally on them. Strictly stronger than tupleEquivMulti (loop case includes diagonal contributions). The target of task #79: prove tupleEquivSimple → tupleEquivLoop via the Lovász §3 rank theorem.

Equations

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

theorem Graphon.Lovasz.tupleEquivMulti_of_tupleEquivLoop {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {ξ ξ' : Fin K → Fin T} (h : tupleEquivLoop B W ξ ξ') : tupleEquivMulti B W ξ ξ'

Loop ⟹ multi (trivial direction via the toLoop injection).

theorem Graphon.Lovasz.tupleEquivLoop_of_orbit {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {ξ ξ' : Fin K → Fin T} (h : ∃ (σ : Equiv.Perm (Fin T)), (∀ (i : Fin T), W (σ i) = W i) ∧ (∀ (i j : Fin T), B (σ i) (σ j) = B i j) ∧ ∀ (i : Fin K), ξ' i = σ (ξ i)) : tupleEquivLoop B W ξ ξ'

Lovász Lemma 2.5 (loop), forward direction (orbit ⟹ loop equiv).

Diagonal observable (#79, 2026-05-17 / 2026-05-18).

The theorem diagonal_observable_of_tupleEquivSimple is defined LATER in this file (after diagonal_observable_K1), at the position where all required dependencies (tupleEquivSimple_restrict_along, rooted_profiles_separate_vertex_orbits) are in scope.

Mathematical content: η ↦ B(η a, η a) is orbit-invariant. The proof reduces to the K=1 case (via tupleEquivSimple_restrict_along) which routes through rooted_profiles_separate_vertex_orbits (#77 paper-root). This collapses #79's diagonal observable into the #77 spectral chain, more direct than the rank-theorem route.

theorem Graphon.Lovasz.tupleEquivSimple_of_tupleEquivMulti {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {ξ ξ' : Fin K → Fin T} (h : tupleEquivMulti B W ξ ξ') : tupleEquivSimple B W ξ ξ'

Multi ⟹ simple (trivial direction).

If ξ ξ' agree on every multigraph evaluation, they agree on every simple-graph evaluation, since MultiLabeledGraph.ofSimple F reduces to the simple-graph form (multiLabeledEvalK_ofSimple).

theorem Graphon.Lovasz.tupleEquivMulti_of_orbit {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {ξ ξ' : Fin K → Fin T} (h : ∃ (σ : Equiv.Perm (Fin T)), (∀ (i : Fin T), W (σ i) = W i) ∧ (∀ (i j : Fin T), B (σ i) (σ j) = B i j) ∧ ∀ (i : Fin K), ξ' i = σ (ξ i)) : tupleEquivMulti B W ξ ξ'

Lovász Lemma 2.5, forward direction (orbit ⟹ multi-equivalence).

If ξ and ξ' lie in the same (B, W)-automorphism orbit (ξ' i = σ (ξ i) for some weighted automorphism σ), then they agree on every multigraph evaluation. Immediate corollary of multiLabeledEvalK_orbit_invariant.

§3.9 — Lovász Lemma 2.4 scaffolding (Claims 4.1–4.4)

This subsection introduces the named helpers and Claims used in Lovász TR-2004-82's proof of Lemma 2.4. The chain mirrors the (private) chain already proved in Graphon/MatrixDetermination.lean as tupleEquiv_restrict / tupleEquiv_extend / tupleEquiv_bijective_case / tupleEquiv_surjective_case / tupleEquiv_implies_tupleOrbitRel, but adapted to the inline tupleEquivSimple predicate to avoid the import cycle with MatrixDetermination. The current status:

• Claim 4.1 (tupleEquivSimple_restrict) — proved.
• Claim 4.2 (tupleEquivSimple_extend) — proved MODULO the named sub-sorry product_trace_identity_simple (the LIST-product trace identity; the Lovász §3 deep content). The class-constancy step coeffRestrictSimple_equiv is now proved as a wrapper around functional_span_zero + product_trace_identity_simple. The single-graph trace identity case is fully proved here.
• Claim 4.3 (tupleEquivSimple_bijective_case) — proved (restriction + IH at T-1 + bijection-uniqueness).
• Claim 4.4 (tupleEquivSimple_surjective_case) — proved via the helpers tupleEquivSimple_restrict_along (restriction along an arbitrary label-index injection) and tupleEquivSimple_id_bijective (twin-free + W>0 forces tupleEquivSimple B W id χ to make χ bijective).

The main theorem tupleEquivSimple_implies_orbit is wired below via strong induction on K, with the architectural sorry localized to the non-surjective branch (mirroring tupleEquiv_implies_tupleOrbitRel).

def Graphon.Lovasz.IsWeightedAutomorphism {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (σ : Equiv.Perm (Fin T)) : Prop

Weighted automorphism predicate.

A permutation σ : Equiv.Perm (Fin T) is a (B, W)-automorphism iff it preserves both the weight vector W and the matrix B entrywise.

Equations

• Graphon.Lovasz.IsWeightedAutomorphism B W σ = ((∀ (i : Fin T), W (σ i) = W i) ∧ ∀ (i j : Fin T), B (σ i) (σ j) = B i j)

def Graphon.Lovasz.tupleOrbitRel {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (ξ ξ' : Fin K → Fin T) : Prop

Tuple-orbit relation (Lovász TR-2004-82 §2, p. 5).

Two tuples ξ ξ' : Fin K → Fin T are orbit-related iff some (B, W)-automorphism σ conjugates one to the other: ξ' i = σ (ξ i). This is the explicit-σ form of the existential conclusion of tupleEquivSimple_implies_orbit.

Equations

• Graphon.Lovasz.tupleOrbitRel B W ξ ξ' = ∃ (σ : Equiv.Perm (Fin T)), Graphon.Lovasz.IsWeightedAutomorphism B W σ ∧ ∀ (i : Fin K), ξ' i = σ (ξ i)

def Graphon.Lovasz.restrictTuple {T k : ℕ} (ξ : Fin (k + 1) → Fin T) : Fin k → Fin T

Restriction of a (k+1)-tuple to its first k coordinates via Fin.castSucc. Lovász's φ' notation (TR-2004-82 §4).

Equations

• Graphon.Lovasz.restrictTuple ξ i = ξ i.castSucc

noncomputable def Graphon.Lovasz.rangeFinset {T k : ℕ} (φ : Fin k → Fin T) : Finset (Fin T)

Range of a tuple φ : Fin k → Fin T as a Finset (Fin T).

Used as the well-founded measure in the deficit-induction proof of tupleEquivSimple_implies_orbit's non-surjective branch.

Equations

• Graphon.Lovasz.rangeFinset φ = Finset.image φ Finset.univ

noncomputable def Graphon.Lovasz.deficit {T k : ℕ} (φ : Fin k → Fin T) : ℕ

Deficit of φ : Fin k → Fin T: T - |range φ|. Zero iff φ is surjective. The deficit strictly decreases when extending by a fresh element (see deficit_lt_of_not_mem), giving the well-founded measure used in Lovász's "extend-and-recurse" plan for Lemma 2.4's non-surjective branch.

Equations

• Graphon.Lovasz.deficit φ = T - (Graphon.Lovasz.rangeFinset φ).card

theorem Graphon.Lovasz.rangeFinset_card_le {T k : ℕ} (φ : Fin k → Fin T) : (rangeFinset φ).card ≤ T

theorem Graphon.Lovasz.rangeFinset_snoc {T k : ℕ} (φ : Fin k → Fin T) (a : Fin T) : rangeFinset (Fin.snoc φ a) = insert a (rangeFinset φ)

theorem Graphon.Lovasz.deficit_lt_of_not_mem {T k : ℕ} (φ : Fin k → Fin T) (a : Fin T) (ha : a ∉ rangeFinset φ) : deficit (Fin.snoc φ a) < deficit φ

Deficit strictly decreases on snoc with a fresh element.

If a ∉ range φ, then deficit (Fin.snoc φ a) < deficit φ. This is the key well-founded measure decrease that drives Lovász's "extend-and-recurse" argument in tupleEquivSimple_implies_orbit.

theorem Graphon.Lovasz.surjective_iff_rangeFinset_eq_univ {T k : ℕ} (φ : Fin k → Fin T) : Function.Surjective φ ↔ rangeFinset φ = Finset.univ

Surjectivity reads off rangeFinset = univ.

theorem Graphon.Lovasz.deficit_eq_zero_iff_surjective {T k : ℕ} (φ : Fin k → Fin T) : deficit φ = 0 ↔ Function.Surjective φ

Surjectivity iff deficit = 0.

theorem Graphon.Lovasz.exists_not_mem_rangeFinset {T k : ℕ} (φ : Fin k → Fin T) (h : ¬Function.Surjective φ) : ∃ (a : Fin T), a ∉ rangeFinset φ

If φ is not surjective, some a : Fin T is missing from the range.

theorem Graphon.Lovasz.tupleEquivSimple_of_tupleOrbitRel {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {ξ ξ' : Fin K → Fin T} (h : tupleOrbitRel B W ξ ξ') : tupleEquivSimple B W ξ ξ'

Orbit ⟹ simple-equivalence (forward direction of Lemma 2.5, specialized to simple graphs). If ξ ξ' are (B, W)-orbit related, they agree on every simple-graph evaluation. Used inside the strong induction to normalize ψ by σ⁻¹ before extending the base.

This is the simple-graph specialization of tupleEquivMulti_of_orbit (via tupleEquivSimple_of_tupleEquivMulti). Direct proof here avoids the multigraph detour.

theorem Graphon.Lovasz.tupleEquivSimple_restrict {T k : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) {ξ ξ' : Fin (k + 1) → Fin T} (h : tupleEquivSimple B W ξ ξ') : tupleEquivSimple B W (restrictTuple ξ) (restrictTuple ξ')

Claim 4.1 — Restriction preserves tupleEquivSimple (Lovász TR-2004-82 §4, p. 6, "first paragraph").

If ξ ξ' : Fin (k+1) → Fin T are simple-equivalent, then their restrictions to the first k coordinates (via Fin.castSucc) are also simple-equivalent.

Proof: any simple graph F' on Fin (n + k) lifts to a simple graph F on Fin (n + (k + 1)) via the embedding Fin.succAboveEmb p with p = ⟨k, _⟩ (skip the pivot position k). The level-(k+1) evaluation of F at ξ equals the level-k evaluation of F' at restrictTuple ξ, because the embedding leaves the unlabeled vertices untouched while reindexing the label slot. The hypothesis applied at F then transfers to F'.

This is the simple-graph analog of tupleEquiv_restrict (line 4461 of MatrixDetermination.lean).

§3.9.1 — Restriction-weight coefficient (Claim 4.2 architecture)

The proof of Claim 4.2 (tupleEquivSimple_extend) below routes through a coeffRestrictSimple "restriction weight" coefficient:

coeffRestrictSimple B W μ ξ := ∑ t : Fin T, [tupleEquivSimple B W μ (snoc ξ t)] · W t

i.e., the total W-mass of extensions t of ξ that are simple-equivalent (at level k + 1) to the given (k + 1)-tuple μ.

Three lemmas drive the assembly:

• coeffRestrictSimple_pos_at_restrict — the coefficient is positive at ξ = restrictTuple μ (witnessed by t = μ (Fin.last k), which makes the indicator tupleEquivSimple μ μ true by reflexivity).
• coeffRestrictSimple_equiv — class constancy: simple-equivalence of ξ and ξ' transfers coeffRestrictSimple B W μ ξ = coeffRestrictSimple B W μ ξ'. PROVED via functional_span_zero
  • product_trace_identity_simple (the latter is a focused sub-sorry capturing the Lovász §3 deep content).
• exists_extension_of_coeffRestrictSimple_pos — from positivity, some t makes the indicator true, yielding the extension.

The class-constancy step is now proved structurally. The single remaining architectural hurdle is the LIST-product trace identity product_trace_identity_simple (Lovász §3 / DecLabeledGraph).

noncomputable def Graphon.Lovasz.coeffRestrictSimple {T k : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (μ : Fin (k + 1) → Fin T) (ξ : Fin k → Fin T) : ℝ

Restriction-weight coefficient for a (k+1)-tuple μ at a level-k base ξ. Sums W t over t : Fin T such that the extended tuple Fin.snoc ξ t is simple-equivalent to μ.

Equations

• Graphon.Lovasz.coeffRestrictSimple B W μ ξ = ∑ t : Fin T, if Graphon.Lovasz.tupleEquivSimple B W μ (Fin.snoc ξ t) then W t else 0

theorem Graphon.Lovasz.coeffRestrictSimple_pos_at_restrict {T k : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (μ : Fin (k + 1) → Fin T) : 0 < coeffRestrictSimple B W μ (restrictTuple μ)

Positivity of coeffRestrictSimple at its own restriction.

Under 0 < W, the coefficient coeffRestrictSimple B W μ (restrictTuple μ) is strictly positive: the term t = μ (Fin.last k) contributes W t > 0 (the indicator tupleEquivSimple μ μ holds by reflexivity), and all other terms are nonneg.

theorem Graphon.Lovasz.exists_extension_of_coeffRestrictSimple_pos {T k : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (μ : Fin (k + 1) → Fin T) (ψ : Fin k → Fin T) (hpos : 0 < coeffRestrictSimple B W μ ψ) : ∃ (a : Fin T), tupleEquivSimple B W μ (Fin.snoc ψ a)

Existence of an extension witness from positive coefficient.

If the restriction-weight coefficient coeffRestrictSimple B W μ ψ is strictly positive (under 0 ≤ W), then there is some a : Fin T such that Fin.snoc ψ a is simple-equivalent to μ at level k + 1.

§3.9.2 — Functional-span machinery (port of MD functional_span_zero)

To prove coeffRestrictSimple_equiv we use the standard finite Stone-Weierstrass-style lemma: given a separating, unital, multiplicatively closed family f : I → Q → ℝ and a d : Q → ℝ that is orthogonal to every f i (under the counting measure), d = 0.

This is a verbatim port of MatrixDetermination.functional_span_zero (L5004) — self-contained, ~100 lines of finite induction on the support of d. Used below to conclude that the class-weight difference between ξ and ξ' over the level-(k+1) tupleEquivSimple-quotient vanishes, given orthogonality from a product trace identity.

§3.9.3 — Simple-graph evaluation, single-graph trace identity, and

the product trace identity (named focused sorry).

We package the simple-graph evaluation body that appears inside tupleEquivSimple as a noncomputable definition simpleEvalAt, prove the single-graph trace identity directly from multiLabeledEvalK_sum_last_label, and state the LIST-product trace identity as a focused sorry. The product identity is the genuine Lovász §3 content (it requires the connection-matrix / DecLabeledGraph machinery in MatrixDetermination.lean, ~3000 lines), and is the SOLE remaining gap for coeffRestrictSimple_equiv below.

noncomputable def Graphon.Lovasz.simpleEvalAt {T K n : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (F : SimpleGraph (Fin (n + K))) [DecidableRel F.Adj] (ξ : Fin K → Fin T) : ℝ

Simple-graph evaluation extracted as a named definition (matching the body of tupleEquivSimple and the RHS of multiLabeledEvalK_ofSimple).

Equations

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

theorem Graphon.Lovasz.coeffRestrictSimple_equiv {T k : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (μ : Fin (k + 1) → Fin T) {ξ ξ' : Fin k → Fin T} (h : tupleEquivSimple B W ξ ξ') : coeffRestrictSimple B W μ ξ = coeffRestrictSimple B W μ ξ'

Class-constancy of the restriction-weight coefficient (Lovász TR-2004-82 §4 core; the IH-free heart of Claim 4.2).

If ξ and ξ' are simple-equivalent at level k, the restriction weight coeffRestrictSimple B W μ ξ is invariant under replacing ξ by ξ'.

Proof outline (mirrors MatrixDetermination.coeffRestrict_equiv):

1. Reduction to class-constant g: it suffices to prove ∑_t W(t) g (snoc ξ t) = ∑_t W(t) g (snoc ξ' t) for every class-constant g : (Fin (k+1) → Fin T) → ℝ. Take g to be the indicator of [μ]; this recovers coeffRestrictSimple_equiv.
2. Apply functional_span_zero: on the level-(k+1) quotient by tupleEquivSimple, use the class-weight difference as d and lists of simpleEvalAt evaluations as the test family. Constants come from the empty list; multiplicative closure from list concatenation; separation from the definition of tupleEquivSimple; orthogonality from product_trace_identity_simple.

Modulo: the named architectural sorry product_trace_identity_simple (the genuine Lovász §3 content; ~3000 lines via DecLabeledGraph in MatrixDetermination.lean). Everything else is closed.

theorem Graphon.Lovasz.tupleEquivSimple_extend {T k : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (hB : ∀ (i j : Fin T), B i j = B j i) {ξ ξ' : Fin k → Fin T} (h : tupleEquivSimple B W ξ ξ') (μ : Fin (k + 1) → Fin T) (hμ : restrictTuple μ = ξ) : ∃ (ν : Fin (k + 1) → Fin T), restrictTuple ν = ξ' ∧ tupleEquivSimple B W μ ν

Claim 4.2 — Extension lemma (Lovász TR-2004-82 §4, p. 6, "second paragraph").

If ξ ξ' : Fin k → Fin T are simple-equivalent at level k, then for every level-(k+1) extension μ of ξ (restrictTuple μ = ξ) there exists a level-(k+1) extension ν of ξ' (restrictTuple ν = ξ') such that μ and ν are simple-equivalent at level k+1.

Proof (this file): build the restriction-weight coefficient coeffRestrictSimple B W μ (sum of W t over t with tupleEquivSimple μ (snoc ξ t)).

• At ξ = restrictTuple μ the coefficient is positive (coeffRestrictSimple_pos_at_restrict, witnessed by t = μ (Fin.last k)).
• Class constancy (coeffRestrictSimple_equiv) transfers positivity from restrictTuple μ (= ξ) to ξ'.
• Positivity yields some a with tupleEquivSimple μ (snoc ξ' a) (exists_extension_of_coeffRestrictSimple_pos); take ν = snoc ξ' a.

Modulo: the named sorry coeffRestrictSimple_equiv (the class constancy step — the IH-free Lovász §4 core).

theorem Graphon.Lovasz.tupleEquivSimple_bijective_case {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (IH_orbit : ∀ {ξ' ψ' : Fin (T - 1) → Fin T}, tupleEquivSimple B W ξ' ψ' → tupleOrbitRel B W ξ' ψ') (ψ : Fin T → Fin T) (hψ_bij : Function.Bijective ψ) (h : tupleEquivSimple B W id ψ) : tupleOrbitRel B W id ψ

Claim 4.3 — Bijective base case (Lovász TR-2004-82 §4, p. 6, "third paragraph").

If ψ : Fin T → Fin T is bijective and tupleEquivSimple B W id ψ holds, then ψ IS a (B, W)-automorphism (orbit relation holds with σ = ψ).

Proof strategy: build single-edge simple graphs F_{i,j} (the graph on Fin T with a single edge {i, j}); their level-T evaluations at id and ψ extract B i j = B (ψ i) (ψ j), giving the B-preservation half. Single-vertex graphs (no edges) similarly extract W preservation via the ∏ W(σ_inner) factor. The pair is exactly IsWeightedAutomorphism B W ψ. (Equiv.ofBijective is used to convert the function-level bijection to Equiv.Perm.)

Status: proved via IH-at-T-1 route (matches tupleEquiv_bijective_case in MatrixDetermination.lean:5339). The proof restricts to the first T-1 coordinates (Claim 4.1), applies IH to extract an automorphism σ agreeing with ψ on those coordinates, then uses bijectivity to force agreement at the last coordinate.

theorem Graphon.Lovasz.tupleEquivSimple_restrict_along {T k T' : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) {φ ψ : Fin k → Fin T} (r : Fin T' ↪ Fin k) (h : tupleEquivSimple B W φ ψ) : tupleEquivSimple B W (φ ∘ ⇑r) (ψ ∘ ⇑r)

Restriction along an arbitrary label-index injection (Lovasz inline analog of MatrixDetermination.tupleEquiv_restrict_along).

For any injection r : Fin T' ↪ Fin k, restricting tuple equivalence along r on the label positions preserves equivalence. Generalizes tupleEquivSimple_restrict (which uses the case r = Fin.castSuccEmb).

Used inside tupleEquivSimple_surjective_case to restrict from Fin k down to Fin T along a section r : Fin T ↪ Fin k of φ.

theorem Graphon.Lovasz.tupleEquivSimple_id_bijective {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (hB : ∀ (i j : Fin T), B i j = B j i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) (IH_orbit : ∀ {ξ' ψ' : Fin (T - 1) → Fin T}, tupleEquivSimple B W ξ' ψ' → tupleOrbitRel B W ξ' ψ') (χ : Fin T → Fin T) (h : tupleEquivSimple B W id χ) : Function.Bijective χ

Auxiliary bijectivity lemma (analog of tupleEquiv_id_bijective from MatrixDetermination.lean:5388).

Under twin-free B with positive weights W, tupleEquivSimple B W id χ forces χ : Fin T → Fin T to be bijective.

Strategy: restrict to Fin (T - 1) via tupleEquivSimple_restrict; apply IH_orbit to obtain an automorphism τ with χ ∘ castSucc = τ ∘ castSucc. If χ(Fin.last) ≠ τ(Fin.last), set v := χ(Fin.last), d := τ(Fin.last); derive B d = B v via (i) single-edge graphs + τ-automorphism (partial row equality on Fin T \ {d}), (ii) an n' = 1 row-sum graph + τ-automorphism reindex (row sum equality), (iii) diagonal isolation using hW > 0. Row equality contradicts htwin, so χ(Fin.last) = τ(Fin.last), hence χ = τ is bijective.

theorem Graphon.Lovasz.tupleEquivSimple_surjective_case {T k : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (hB : ∀ (i j : Fin T), B i j = B j i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) (IH_orbit : ∀ {ξ' ψ' : Fin (T - 1) → Fin T}, tupleEquivSimple B W ξ' ψ' → tupleOrbitRel B W ξ' ψ') (φ ψ : Fin k → Fin T) (hφ_surj : Function.Surjective φ) (h : tupleEquivSimple B W φ ψ) : tupleOrbitRel B W φ ψ

Claim 4.4 — Surjective base case (analog of MatrixDetermination.tupleEquiv_surjective_case_both followed by tupleEquiv_surjective_case).

If φ : Fin k → Fin T is surjective and tupleEquivSimple B W φ ψ, then tupleOrbitRel B W φ ψ.

Proof strategy: pick a section s : Fin T → Fin k with φ ∘ s = id. Restrict the equivalence along s (via tupleEquivSimple_restrict_along) to obtain tupleEquivSimple B W id (ψ ∘ s). Apply tupleEquivSimple_id_bijective (uses hW > 0) to deduce ψ ∘ s is bijective, hence ψ is surjective. Apply Claim 4.3 (tupleEquivSimple_bijective_case) to get an automorphism σ with ψ (s i) = σ i. To extend to all of Fin k: for each j not in im(s), build a variant section s' agreeing with s off φ j but with s' (φ j) = j, extract σ', prove σ = σ' via the standard bijection-uniqueness argument.

theorem Graphon.Lovasz.tupleEquivSimple_ext_eq_of_surj {T k : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {α : Fin k → Fin T} (hα_surj : Function.Surjective α) {a b : Fin T} (h : tupleEquivSimple B W (Fin.snoc α a) (Fin.snoc α b)) : a = b

Surjective-extension uniqueness (tupleEquiv_ext_eq_of_surj analog, MatrixDetermination.lean:10801).

If α : Fin k → Fin T is surjective and B is twin-free, then two simple-equivalent extensions Fin.snoc α a and Fin.snoc α b must have a = b.

Proof strategy: build single-edge simple graphs F_{j, k} on Fin (0 + (k + 1)) for each j : Fin k; the level-(k+1) evaluation gives B (α j) a = B (α j) b. Surjectivity transfers this to ∀ t, B t a = B t b, hence B a = B b by symmetry, contradicting twin-freeness unless a = b.

Status: proved by inlining the single-edge labeledEvalK_singleEdge form directly into the tupleEquivSimple unfolding (n' = 0, Fintype.sum_unique collapses the σ-sum).

§3.95 — Connection-matrix rank theorem (canonical architectural sorry)

This subsection introduces the connection matrix N(K, B, W) over k-labeled (multi-)graphs and states the rank theorem (Lovász TR-2004-82 §3, Theorem 2.2). The rank theorem is the deep Lovász §3 content underlying Lemma 2.4 / Lemma 2.5 in our framework.

Connection matrix N(K, B, W) (Lovász §2, p. 4): rows indexed by label maps ξ : Fin K → Fin T, columns indexed by k-labeled (simple) graphs F. Entry N(K, B, W)[ξ, F] := simpleEvalK F B W ξ. Two rows ξ, ξ' are equal iff tupleEquivSimple B W ξ ξ' holds.

In our framework we do not materialize the matrix explicitly; we instead encode "row equality" as tupleEquivSimple directly. By the definition of tupleEquivSimple (∀ n F, simpleEvalAt ξ = simpleEvalAt ξ'), this is precisely row-extensional equality — the row of ξ in N(K, B, W) IS the function (n, F) ↦ simpleEvalAt B W F ξ.

The forward direction (orbit ⟹ row equality) is proved as tupleEquivSimple_of_tupleOrbitRel (L1619, FULLY PROVED): if two tuples are in the same orbit, their rows agree.

The reverse direction (row equality ⟹ orbit, under twin-free + W > 0) is the rank theorem itself, stated as the proposition

tupleEquivSimple B W ξ ξ' → tupleOrbitRel B W ξ ξ'

under twin-free B and strictly positive W. This is exactly Lovász's Theorem 2.2 ("rk N(K, B, W) = orb_K(B, W)") in the equivalence-class form: distinct rank = distinct orbit, so row equality forces orbit equality.

Status: SORRY'd at the rank theorem. All downstream content (tupleEquivSimple_implies_orbit, tupleEquivMulti_implies_orbit, the twin-free multigraph bridge corollary) routes through this single named sorry. The remaining sorry (general non-twin-free n+1 multigraph bridge, multiLabeledEvalK_tupleEquiv_invariant) is independent.

Reduction to the deep paper content: the proof structure mirrors the strong induction + deficit-induction in tupleEquiv_implies_tupleOrbitRel (MatrixDetermination.lean:10873), with the architectural sorry at the inner-base T - 1 ≥ k + 1 case of the deficit-induction. Closing this requires either a multigraph- evaluation route (diagonal / self-loop extraction) or a direct fiber construction in tupleEquivSimple_surjective_case / tupleEquivSimple_id_bijective that avoids the deficit-1 IH (see MatrixDetermination.lean:11002-11007).

Connection-matrix rank theorem (Lovász TR-2004-82 §3, Theorem 2.2; equivalence-class form) — PRIMARY paper root.

Dependency hierarchy (post-2026-05-12 architectural decision):

• PRIMARY ROOT: the rank theorem (Lovász §3 Theorem 2.2, simple-graph form, twin-free).
• SECONDARY: multiLabeledEvalK_tupleEquiv_invariant at L1315 (general, non-twin-free multigraph form).

Closing the rank theorem discharges everything the downstream matrix-determination chain needs (which all has twin-free hypothesis): tupleEquivSimple_implies_orbit, tupleEquivMulti_implies_orbit, multiLabeledEvalK_tupleEquiv_invariant_twinFree. The secondary multigraph bridge is a strictly stronger non-twin-free statement that may be left as an off-axis generalization.

Under twin-free B and strictly positive W, the rank theorem states tupleEquivSimple ⟹ tupleOrbitRel. The separation contrapositive (orbit_separation_by_simple_graph below) is the canonical primary sorry; the rank theorem is a short contradiction proof from it.

Lovász §3 — Idempotent decomposition: orbit indicators

This section introduces the orbit indicator for (B, W)-automorphism orbits of Fin K → Fin T, plus the named architectural lemma asserting that orbit indicators lie in the ℝ-span of simple-graph evaluations (Lovász §3 multigraph-algebra fullness, restricted to simple graphs under twin-free B).

The canonical primary sorry of the Lovász chain is migrated from orbit_separation_by_simple_graph to orbitIndicator_mem_simpleGraphSpan — a cleaner ℝ-linear-algebra statement that captures the same content.

theorem Graphon.Lovasz.tupleOrbitRel_refl {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (ξ : Fin K → Fin T) : tupleOrbitRel B W ξ ξ

tupleOrbitRel is reflexive.

Witnessed by the identity automorphism.

theorem Graphon.Lovasz.tupleOrbitRel_symm {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {ξ ξ' : Fin K → Fin T} (h : tupleOrbitRel B W ξ ξ') : tupleOrbitRel B W ξ' ξ

tupleOrbitRel is symmetric.

If σ realizes ξ' = σ ∘ ξ, then σ.symm realizes ξ = σ.symm ∘ ξ'.

theorem Graphon.Lovasz.tupleOrbitRel_trans {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {ξ ξ' ξ'' : Fin K → Fin T} (h₁ : tupleOrbitRel B W ξ ξ') (h₂ : tupleOrbitRel B W ξ' ξ'') : tupleOrbitRel B W ξ ξ''

tupleOrbitRel is transitive.

If σ₁ realizes ξ' = σ₁ ∘ ξ and σ₂ realizes ξ'' = σ₂ ∘ ξ', then σ₂ * σ₁ realizes ξ'' = (σ₂ * σ₁) ∘ ξ.

theorem Graphon.Lovasz.tupleOrbitRel_equivalence {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) : Equivalence (tupleOrbitRel B W)

tupleOrbitRel is an equivalence relation.

def Graphon.Lovasz.tupleOrbitSetoid {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (K : ℕ) : Setoid (Fin K → Fin T)

Setoid on tuples induced by tupleOrbitRel.

Equations

• Graphon.Lovasz.tupleOrbitSetoid B W K = { r := Graphon.Lovasz.tupleOrbitRel B W, iseqv := ⋯ }

def Graphon.Lovasz.OrbitClass (T K : ℕ) (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) : Type

Quotient of Fin K → Fin T by the (B, W)-orbit relation.

OrbitClass T K B W parametrizes (B, W)-automorphism orbits of K-tuples. Used as the index set for the idempotent decomposition in Lovász §3.

Equations

• Graphon.Lovasz.OrbitClass T K B W = Quotient (Graphon.Lovasz.tupleOrbitSetoid B W K)

noncomputable def Graphon.Lovasz.orbitIndicator {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (ξ : Fin K → Fin T) : (Fin K → Fin T) → ℝ

Orbit indicator of a K-tuple ξ.

orbitIndicator B W ξ ξ' = 1 if ξ and ξ' are orbit-related and 0 otherwise. Equivalently, the {0,1}-indicator of the orbit-class of ξ (a representative-dependent name for a representative-invariant function — invariance is orbitIndicator_orbit_invariant).

Equations

• Graphon.Lovasz.orbitIndicator B W ξ ξ' = if Graphon.Lovasz.tupleOrbitRel B W ξ ξ' then 1 else 0

theorem Graphon.Lovasz.orbitIndicator_orbit_invariant {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {ξ ξ_alt : Fin K → Fin T} (h : tupleOrbitRel B W ξ ξ_alt) : orbitIndicator B W ξ = orbitIndicator B W ξ_alt

Orbit-invariance of orbitIndicator (as a function of the source).

Replacing the source representative ξ by an orbit-related ξ_alt gives the same indicator function.

theorem Graphon.Lovasz.orbitIndicator_self {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (ξ : Fin K → Fin T) : orbitIndicator B W ξ ξ = 1

orbitIndicator ξ ξ = 1 (reflexivity).

theorem Graphon.Lovasz.orbitIndicator_of_not_orbit {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {ξ ξ' : Fin K → Fin T} (h : ¬tupleOrbitRel B W ξ ξ') : orbitIndicator B W ξ ξ' = 0

orbitIndicator ξ ξ' = 0 when not orbit-related.

theorem Graphon.Lovasz.orbitIndicator_mem_simpleGraphSpan {T K : ℕ} (B : Fin T → Fin T → ℝ) (_hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (_hW : ∀ (i : Fin T), 0 < W i) (_htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) (ξ : Fin K → Fin T) : ∃ (cs : List (ℝ × (n : ℕ) × (F : SimpleGraph (Fin (n + K))) × DecidableRel F.Adj)), orbitIndicator B W ξ = fun (η : Fin K → Fin T) => (List.map (fun (p : ℝ × (n : ℕ) × (F : SimpleGraph (Fin (n + K))) × DecidableRel F.Adj) => p.1 * simpleEvalAt B W p.2.snd.fst η) cs).sum

Orbit indicators lie in the ℝ-span of simple-graph evaluations (Lovász §3 — fullness of the simple-graph evaluation algebra under twin-free B) — SECONDARY / OFF-AXIS (post-2026-05-13 reanalysis).

For any source tuple ξ : Fin K → Fin T, the orbit indicator orbitIndicator B W ξ can be written as an ℝ-linear combination of simple-graph evaluations simpleEvalAt B W F : (Fin K → Fin T) → ℝ (ranging over simple graphs F on Fin (n + K) for various n).

Status reverted to OFF-AXIS: the natural Lagrange-interpolation route produces PRODUCTS of simpleEvalAt (= multigraph evals via glue), not linear combinations. Converting back to a linear combination of simple-graph evals would itself need Lemma 2.5 content — circular.

The PRIMARY ROOT is now orbit_separation_by_simple_graph (the contrapositive form, which doesn't require product expansion). This span theorem is a stronger CONSEQUENCE that may follow from separation + the multigraph bridge.

The representation uses pairs (c, ⟨n, ⟨F, dec⟩⟩) where c : ℝ is a coefficient, n : ℕ is an unlabeled-vertex count, F : SimpleGraph (Fin (n + K)) is a simple labeled graph, and dec : DecidableRel F.Adj is the required decidability witness.

Status: canonical primary sorry (migrated from orbit_separation_by_simple_graph).

Proof approach (Lovász §3): the simple-graph evaluation algebra under twin-free B is dense in the space of orbit-invariant functions; the orbit indicators form a basis of this latter space; hence each indicator is a finite ℝ-linear combination. This is the multigraph-algebra fullness theorem of Lovász §3, restricted to simple graphs under the twin-free hypothesis.

Natural Lagrange-interpolation route (per post-2026-05-13 user analysis): for each orbit class O' ≠ orbit(ξ), pick a separating simple graph F_{O'} (its existence is orbit_separation_by_simple_graph, PROVED from this theorem — a circular dependency). The indicator is the product ∏_{O' ≠ orbit(ξ)} (simpleEvalAt F_{O'} - w_{O'}) / (v_{O'} - w_{O'}) over orbit classes.

Obstacle (multigraph-vs-simple-graph product): expanding the product yields PRODUCTS of simpleEvalAts, which via the glue-multigraph identity are MULTIGRAPH evaluations (since disjoint unions of simple graphs at shared labels can produce label-label multi-edges). Converting these multigraph evals back to simple-graph linear combinations is itself the Lemma 2.5 content. The contrapositive orbit_separation_by_simple_graph does NOT have this issue (it just exhibits a single separating graph) — so the "separation" form may be the actually attackable formulation, with the span form derived from it via a careful product-expansion route.

Orbit separation: edge-or-degree → simple-graph form

Post-2026-05-13 separator_search empirical analysis: across 21K non- orbit pairs at small (T, K), 100% are separated by a SINGLE edge — either label-label or label-to-unlabeled. This motivates an intermediate theorem orbit_separation_by_edge_or_degree giving an explicit edge OR degree-profile witness, from which the simple graph is a single-edge graph (n=0) or a single-edge "rooted star" (n=1).

Falsification: see scripts/falsify_edge_degree_conjecture.py. 64K pairs tested, zero counterexamples.

Orbit separation by edge or degree — KNOWN-FALSE / OFF-AXIS (refuted 2026-05-14 by C₅ ⊔ C₆ counterexample at K=1).

Counterexample: B = adjacency of C₅ ⊔ C₆, W = uniform 1.

• ξ = (0,) (vertex in C₅), ξ' = (5,) (vertex in C₆).
• K = 1: edge profile vacuous (no a ≠ b).
• Weighted degrees agree: both = 2 (regular graphs).
• But no aut σ ∈ Aut(C₅ ⊔ C₆) = D₅ × D₆ sends C₅-vertex to C₆-vertex (component preservation).

Falsification: scripts/falsify_edge_degree_conjecture.py updated with C₅ ⊔ C₆ test; 60 counterexamples found in this single family.

The minimal separating simple graph for this pair is a 5-cycle rooted at the label (n_unlabeled = 4, 5 edges): the label vertex participates in 2 distinct 5-cycles in C₅ but 0 in C₆. Found by scripts/separator_search.py cycles.

Implication: edge + degree profiles are insufficient. The canonical primary sorry must reflect this — restore orbit_separation_by_simple_graph as the abstract primary, with explicit acknowledgment that the separator family includes rooted cycles / paths / trees of unbounded size.

noncomputable def Graphon.Lovasz.weightedDegree {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i : Fin T) : ℝ

Weighted degree of vertex i in (B, W).

Equations

• Graphon.Lovasz.weightedDegree B W i = ∑ t : Fin T, W t * B i t

def Graphon.Lovasz.sameTupleEdgeProfile {T K : ℕ} (B : Fin T → Fin T → ℝ) (ξ ξ' : Fin K → Fin T) : Prop

Same tuple edge profile: ξ and ξ' agree on all label-label B-entries at distinct labels.

Equations

• Graphon.Lovasz.sameTupleEdgeProfile B ξ ξ' = ∀ (a b : Fin K), a ≠ b → B (ξ a) (ξ b) = B (ξ' a) (ξ' b)

def Graphon.Lovasz.sameTupleDegreeProfile {T K : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (ξ ξ' : Fin K → Fin T) : Prop

Same tuple degree profile: ξ and ξ' have equal weighted degrees at every label position.

Equations

• Graphon.Lovasz.sameTupleDegreeProfile B W ξ ξ' = ∀ (a : Fin K), Graphon.Lovasz.weightedDegree B W (ξ a) = Graphon.Lovasz.weightedDegree B W (ξ' a)

§3.95.5 — K=1 rooted profile target

Per 2026-05-14 user directive: introduce a K=1 rooted-profile specialization of the separation theorem. This is the simplest non-trivial Lovász separation form: under twin-free B + W > 0, distinct vertex orbits are separated by some rooted simple graph evaluation.

This statement is empirically valid (C₅ vs C₆ separator is a 5-cycle rooted at the label). Unlike the false edge-or-degree conjecture, the rooted-profile family is unbounded — but the separation IS by a SINGLE simple graph, not a polynomial in multiple.

def Graphon.Lovasz.vertexOrbitRel {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i j : Fin T) : Prop

Vertex orbit relation — K=1 specialization of tupleOrbitRel. Two vertices are orbit-related iff some (B, W)-automorphism maps one to the other.

Equations

• Graphon.Lovasz.vertexOrbitRel B W i j = ∃ (σ : Equiv.Perm (Fin T)), Graphon.Lovasz.IsWeightedAutomorphism B W σ ∧ σ i = j

noncomputable def Graphon.Lovasz.rootedProfile {T n : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i : Fin T) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] : ℝ

Rooted simple-graph profile at vertex i: the simple-graph evaluation with the single label position fixed to i.

Equations

• Graphon.Lovasz.rootedProfile B W i F = Graphon.Lovasz.simpleEvalAt B W F fun (x : Fin 1) => i

noncomputable def Graphon.Lovasz.weightedAdj {T : ℕ} (B : Fin T → Fin T → ℝ) (W f : Fin T → ℝ) (i : Fin T) : ℝ

Weighted adjacency operator A f i := ∑ j, W j · B i j · f j. The key linear operator for the Krylov/path-profile route to separation in the K=1 case.

Equations

• Graphon.Lovasz.weightedAdj B W f i = ∑ j : Fin T, W j * B i j * f j

noncomputable def Graphon.Lovasz.weightedAdjIter {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) : ℕ → (Fin T → ℝ) → Fin T → ℝ

Iterated weighted adjacency: A^m as a function.

Equations

• Graphon.Lovasz.weightedAdjIter B W 0 x✝ = x✝
• Graphon.Lovasz.weightedAdjIter B W m.succ x✝ = Graphon.Lovasz.weightedAdj B W (Graphon.Lovasz.weightedAdjIter B W m x✝)

noncomputable def Graphon.Lovasz.closedWalkProfile {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i : Fin T) : ℕ → ℝ

Closed-walk profile at vertex i of length m.

CW_m(i) := ∑_{v_1,...,v_{m-1}} W(v_1)...W(v_{m-1}) · B(i, v_1) · B(v_1, v_2) · ... · B(v_{m-1}, i)

Compositional form: let g_i(v) := B(v, i). Then for m ≥ 1, CW_m(i) = (A^{m-1} g_i)(i) where A is weightedAdj. Encoded recursively via weightedAdjIter.

For m = 0: trivially 1 (empty product). For m = 1: B(i, i) = 0 for simple graphs without self-loops. For m ≥ 2: well-defined closed walk sum.

Equations

• Graphon.Lovasz.closedWalkProfile B W i 0 = 1
• Graphon.Lovasz.closedWalkProfile B W i m.succ = Graphon.Lovasz.weightedAdjIter B W m (fun (v : Fin T) => B v i) i

§4 — Spectral scaffolding for #77 (deferred)

Per 2026-05-18 design plan, the K=1 spectral closing lemma vertex_orbit_of_closed_walks_eq factors through finite-dimensional spectral theory on the symmetric operator S := D^{1/2} B D^{1/2} where D = diag(W).

Key identity (to be proved as a stepping stone): closedWalkProfile B W i (m + 1) = (S^m)[i, i] / W i for m ≥ 1.

Closure path:

1. Bridge: closed walks ↔ diagonal moments of S^m.
2. Cayley-Hamilton: equality at m = 0..T-1 suffices.
3. Spectral decomposition: S = ∑ λ_k u_k u_k^T (mathlib's Matrix.IsSymm.eigenvectorBasis).
4. Equal spectral diagonals + twin-free → orbit upgrade.

Scaffolding deferred: importing Real.sqrt machinery (Analysis.SpecialFunctions.Pow.*) introduces simp lemmas that conflict with earlier proofs in this file. The spectral work should be done in a SEPARATE FILE Graphon/Spectral.lean that imports the necessary analysis modules without polluting Lovasz.lean. That refactor is the natural next-session task.

K=1 spectral closing chain (former #77 docstring, 2026-05-18).

Empirical evidence (cumulative across 4 falsification scripts):

• 291/291 random + cycle-disjoint-union pairs separated at length ≥ 3.
• 22,096 twin-free simple graphs (T ≤ 6 full enum): 0 counterexamples.
• 7 adversarial known cospectral structures: 0 counterexamples.
• 78 weighted twin-free cases: 0 counterexamples.

The m + 3 offset (length ≥ 3) is required because length-2 closed walks ∑_v W(v) B(i,v)² are inherently multigraph evaluations (edge multiplicity 2) and cannot be realized by simple graphs.

theorem Graphon.Lovasz.vertex_orbit_of_closed_walks_eq {T : ℕ} (_B : Fin T → Fin T → ℝ) (_hB : ∀ (i j : Fin T), _B i j = _B j i) (_W : Fin T → ℝ) (_hW : ∀ (i : Fin T), 0 < _W i) (_htwin : ∀ (i j : Fin T), i ≠ j → _B i ≠ _B j) {i j : Fin T} (_h : ∀ (m : ℕ), closedWalkProfile _B _W i (m + 3) = closedWalkProfile _B _W j (m + 3)) : vertexOrbitRel _B _W i j

K=1 spectral closing lemma (named paper-root for #77).

If two vertices have matching closed-walk profiles at all lengths ≥ 3, then they lie in the same (B, W)-vertex orbit (under twin-free B + W > 0).

This is the positive (contrapositive) form of #77. Stating it explicitly localizes the spectral content of Lovász §3 K=1 to a single named theorem.

Mathematical content: closed walk profiles CW_m(i) = (S^m)[i,i]/W[i] (where S = D^{1/2} B D^{1/2}) determine the spectral diagonal data at i. The conjecture was that Cayley-Hamilton + spectral theory + twin-free could force orbit relation.

STATUS (2026-05-18): REFUTED.

Counterexample: vertices 1 and 5 in the 9-vertex "double-pin tree" have identical (S^m)[i, i] for all m but lie in different orbits (|Aut| = 1). The graph is twin-free. See scripts/spectral_orbit_validation.py.

Implications:

• This theorem is FALSE as stated. The sorry'd statement is retained for architectural documentation; it should NOT be assumed downstream.
• closed_walk_profiles_separate_vertex_orbits (proved below via contrapositive of this) inherits the issue; its statement is also false in this form.
• rooted_profiles_separate_vertex_orbits (the K=1 specialization of Lovász Lemma 2.4) is TRUE but our current proof route via the closed-walk bridge is INVALID. Needs to be re-proved through the full rooted simple-graph family (paths, trees, asymmetric shapes), not just rooted cycles.

Earlier empirical evidence turned out to be incomplete:

• The cospectral_vertex_search.py corpus stopped at T = 6.
• The double-pin counterexample is on T = 9 — outside the prior exhaustive enum range.
• Random/adversarial scripts didn't include this specific graph structure.

Salvaged content: the bridge theorems rootedProfile_rootedCycleGraph_eq_closedWalkProfile and closedWalkProfile_eq_symAdjIter_diag (in Spectral.lean) are still valuable. They translate between representations; what's wrong is the orbit-upgrade INFERENCE from closed walks alone.

theorem Graphon.Lovasz.closed_walk_profiles_separate_vertex_orbits {T : ℕ} (_B : Fin T → Fin T → ℝ) (_hB : ∀ (i j : Fin T), _B i j = _B j i) (_W : Fin T → ℝ) (_hW : ∀ (i : Fin T), 0 < _W i) (_htwin : ∀ (i j : Fin T), i ≠ j → _B i ≠ _B j) {i j : Fin T} (_h : ¬vertexOrbitRel _B _W i j) : ∃ (m : ℕ), closedWalkProfile _B _W i (m + 3) ≠ closedWalkProfile _B _W j (m + 3)

#77 — REFUTED 2026-05-18.

Statement is FALSE: the double-pin tree (T=9) has twin-free B + W = 1 with two non-orbit vertices (1, 5) whose closed-walk profiles agree for all m. Retained as a sorry'd statement to document the counterexample and prevent accidental downstream use.

The proof previously routed through vertex_orbit_of_closed_walks_eq (also REFUTED). Do not assume this theorem in downstream work.

Counterexample: edges (0,1)(1,2)(2,3)(3,7)(0,4)(4,5)(5,6)(4,8); vertices 1 and 5 are spectrally equivalent (closed walks match for all m) but |Aut| = 1, so they are in different orbits.

def Graphon.Lovasz.rootedCycleGraph (m : ℕ) : SimpleGraph (Fin (m + 2))

Rooted cycle graph at length m + 2. Edges are consecutive pairs (j, j+1) plus the wrap edge (0, m+1). The K=1 label placement makes vertex 0 the "root" of the rooted cycle. The m + 2 offset ensures m + 2 ≥ 2, so the graph has at least one edge.

Equations

• Graphon.Lovasz.rootedCycleGraph m = { Adj := fun (a b : Fin (m + 2)) => ↑a + 1 = ↑b ∨ ↑b + 1 = ↑a ∨ ↑a = 0 ∧ ↑b = m + 1 ∨ ↑a = m + 1 ∧ ↑b = 0, symm := ⋯, loopless := ⋯ }

instance Graphon.Lovasz.instDecidableRelFinHAddNatOfNatAdjRootedCycleGraph (m : ℕ) : DecidableRel (rootedCycleGraph m).Adj

Equations

• Graphon.Lovasz.instDecidableRelFinHAddNatOfNatAdjRootedCycleGraph m a b = id inferInstance

@[simp]

theorem Graphon.Lovasz.rootedCycleGraph_adj_iff {m : ℕ} (a b : Fin (m + 2)) : (rootedCycleGraph m).Adj a b ↔ ↑a + 1 = ↑b ∨ ↑b + 1 = ↑a ∨ ↑a = 0 ∧ ↑b = m + 1 ∨ ↑a = m + 1 ∧ ↑b = 0

Adjacency unfolding lemma for rootedCycleGraph.

theorem Graphon.Lovasz.rootedCycleGraph_not_adj_self {m : ℕ} (a : Fin (m + 2)) : ¬(rootedCycleGraph m).Adj a a

Loopless property unfolding.

theorem Graphon.Lovasz.sum_fin_succ_eq_sum_cons {β : Type u_1} {T n : ℕ} [AddCommMonoid β] (f : (Fin (n + 1) → Fin T) → β) : ∑ σ : Fin (n + 1) → Fin T, f σ = ∑ x : Fin T, ∑ σ' : Fin n → Fin T, f (Fin.cons x σ')

Sum decomposition: a sum over Fin (k+1) → α decomposes as a double sum over the head (element of α) and the tail (Fin k → α). Re-indexing via Fin.consEquiv. Used to express the recursive structure of weightedAdjIter as a single sum over walk-coordinate functions.

def Graphon.Lovasz.cycleSucc {m : ℕ} (j : Fin (m + 2)) : Fin (m + 2)

Cyclic successor on Fin (m + 2): maps j to j + 1 modulo m + 2.

Equations

• Graphon.Lovasz.cycleSucc j = if h : ↑j + 1 < m + 2 then ⟨↑j + 1, h⟩ else ⟨0, ⋯⟩

@[simp]

theorem Graphon.Lovasz.cycleSucc_val_of_lt {m : ℕ} (j : Fin (m + 2)) (hj : ↑j + 1 < m + 2) : ↑(cycleSucc j) = ↑j + 1

@[simp]

theorem Graphon.Lovasz.cycleSucc_val_of_eq {m : ℕ} (j : Fin (m + 2)) (hj : ↑j = m + 1) : ↑(cycleSucc j) = 0

theorem Graphon.Lovasz.cycleSucc_adj {m : ℕ} (j : Fin (m + 2)) : (rootedCycleGraph m).Adj j (cycleSucc j)

theorem Graphon.Lovasz.rootedCycleGraph_adj_iff_succ {m : ℕ} (a b : Fin (m + 3)) : (rootedCycleGraph (m + 1)).Adj a b ↔ cycleSucc a = b ∨ cycleSucc b = a

Every edge of rootedCycleGraph (m+1) (for m+3 ≥ 3 vertices) is of the form s(j, cycleSucc j) for some j : Fin (m+3). The m+1 offset ensures the cycle has at least 3 vertices, so the edge map is injective (distinct j give distinct unordered pairs, since a 2-cycle would require m+2 = 2).

theorem Graphon.Lovasz.cycleSucc_cycleSucc_ne {m : ℕ} (k : Fin (m + 3)) : cycleSucc (cycleSucc k) ≠ k

cycleSucc is not its own inverse: cycleSucc (cycleSucc j) ≠ j on Fin (m + 3) (which has at least 3 elements, so no 2-cycles exist).

theorem Graphon.Lovasz.cycleSucc_pair_injective {m : ℕ} : Function.Injective fun (j : Fin (m + 3)) => s(j, cycleSucc j)

The map j ↦ s(j, cycleSucc j) is injective on Fin (m + 3).

theorem Graphon.Lovasz.rootedCycleGraph_edgeFinset_eq {m : ℕ} : (rootedCycleGraph (m + 1)).edgeFinset = Finset.image (fun (j : Fin (m + 3)) => s(j, cycleSucc j)) Finset.univ

The edge finset of rootedCycleGraph (m+1) is exactly the image of the map j ↦ s(j, cycleSucc j) over Fin (m + 3).

theorem Graphon.Lovasz.rootedCycleGraph_edgeProduct_eq {T m : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (τ : Fin (m + 3) → Fin T) : ∏ e ∈ (rootedCycleGraph (m + 1)).edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2) = ∏ j : Fin (m + 3), B (τ j) (τ (cycleSucc j))

For a symmetric B, the τ-parametric edge product over the cycle factors via cycleSucc: each edge s(j, cycleSucc j) contributes B (τ j) (τ (cycleSucc j)), regardless of Quot.out orientation.

theorem Graphon.Lovasz.rootedProfile_rootedCycleGraph_eq_closedWalkProfile {T m : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (i : Fin T) : rootedProfile B W i (rootedCycleGraph (m + 1)) = closedWalkProfile B W i (m + 3)

Bridge lemma: rootedProfile of rootedCycleGraph (m+1) at vertex i equals the closed-walk profile closedWalkProfile B W i (m+3).

Pure combinatorics: the edges of the cycle on Fin (m+3) are exactly {j, j+1} for j : Fin (m+3) plus the wrap {0, m+2}, so the edge product in simpleEvalAt factors as the closed-walk product B(i, σ 0) · B(σ 0, σ 1) · ... · B(σ (m+1), i), matching (weightedAdjIter B W (m+2) g_i)(i) where g_i(v) := B(v, i).

The m + 1 offset on rootedCycleGraph (giving cycle length ≥ 3) is necessary because rootedCycleGraph 0 is a single edge (1 edge), which evaluates to ∑ W(v) B(i,v) (weighted degree), not the closed-walk-of-length-2 profile ∑ W(v) B(i,v)² (which is inherently a multigraph evaluation, requiring edge multiplicity 2).

Status: focused infrastructure sorry. Needed to wire closed_walk_profiles_separate_vertex_orbits into rooted_profiles_separate_vertex_orbits. ~30-80 lines of Fin arithmetic + Quot.out reasoning (down from 100-200 thanks to the cycleSucc helper set).

theorem Graphon.Lovasz.rooted_profiles_separate_vertex_orbits {T : ℕ} (_B : Fin T → Fin T → ℝ) (_hB : ∀ (i j : Fin T), _B i j = _B j i) (_W : Fin T → ℝ) (_hW : ∀ (i : Fin T), 0 < _W i) (_htwin : ∀ (i j : Fin T), i ≠ j → _B i ≠ _B j) {i j : Fin T} (_h : ¬vertexOrbitRel _B _W i j) : ∃ (n : ℕ) (F : SimpleGraph (Fin (n + 1))) (x : DecidableRel F.Adj), rootedProfile _B _W i F ≠ rootedProfile _B _W j F

Rooted profiles separate vertex orbits (Lovász §3 K=1 case). If two vertices are NOT in the same (B, W)-orbit (under twin-free B + W > 0), some rooted simple graph evaluation separates them.

This is the K=1 case of orbit_separation_by_simple_graph, specialized to vertex (single-label) tuples.

Empirical evidence stack (post-2026-05-14 falsification passes):

• Path profiles ALONE: FAIL on cycle-disjoint-union families (scripts/path_profile_search.py). Regular graphs have identical path profiles at every vertex.
• Closed-walk / rooted-cycle profiles: PASS broadly (291/291 pairs on the test corpus, scripts/closed_walk_search.py); zero cospectral-vertex counterexamples on full enumeration of all twin-free simple graphs through T ≤ 6.
• The full rooted simple-graph family (paths + cycles + trees + arbitrary connected) suffices in all tested cases.

STATUS (2026-05-18): PAPER-ROOT (was: proved via closed walks, REFUTED).

Previous proof routed through closed_walk_profiles_separate_vertex_orbits

• the rootedCycleGraph bridge. That route is INVALID — the double-pin tree counterexample (2026-05-18) shows closed walks alone are insufficient even under twin-free + W > 0.

The THEOREM itself is TRUE (Lovász Lemma 2.4 K=1 specialization), but proving it requires the FULL rooted simple-graph family (paths, trees, asymmetric shapes), which is the Lovász §3 rank theorem content.

theorem Graphon.Lovasz.orbit_separation_by_simple_graph_K1 {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {ξ ξ' : Fin 1 → Fin T} (h : ¬tupleOrbitRel B W ξ ξ') : ∃ (n : ℕ) (F : SimpleGraph (Fin (n + 1))) (x : DecidableRel F.Adj), simpleEvalAt B W F ξ ≠ simpleEvalAt B W F ξ'

Bridge from K=1 rooted profile to general orbit separation. At K = 1, orbit_separation_by_simple_graph follows from rooted_profiles_separate_vertex_orbits by reducing the tuple relation to vertex relation.

theorem Graphon.Lovasz.diagonal_observable_K1 {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {ξ ξ' : Fin 1 → Fin T} (h : tupleEquivSimple B W ξ ξ') : B (ξ 0) (ξ 0) = B (ξ' 0) (ξ' 0)

Diagonal observable at K=1 — derived from rooted-profile separation.

For K=1, the diagonal observable B(ξ 0, ξ 0) = B(ξ' 0, ξ' 0) follows from tupleEquivSimple B W ξ ξ' via:

1. tupleEquivSimple at K=1 ⟹ all rooted profiles agree at (ξ 0, ξ' 0).
2. Contrapositive of rooted_profiles_separate_vertex_orbits (proved modulo #77) ⟹ vertexOrbitRel B W (ξ 0) (ξ' 0).
3. Vertex orbit relation gives σ automorphism with σ (ξ 0) = ξ' 0.
4. B(ξ 0, ξ 0) = B(σ (ξ 0), σ (ξ 0)) = B(ξ' 0, ξ' 0) by aut B-preservation.

Status: proved modulo #77 (closed_walk_profiles_separate, K=1 spectral paper-root). Note this reduces diagonal_observable_of_tupleEquivSimple at K=1 to a paper-root we already have (#77) rather than to the rank theorem.

theorem Graphon.Lovasz.diagonal_observable_of_tupleEquivSimple {T K : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {ξ ξ' : Fin K → Fin T} (h : tupleEquivSimple B W ξ ξ') (a : Fin K) : B (ξ a) (ξ a) = B (ξ' a) (ξ' a)

Diagonal observable — general K version, derived from K=1 case via tupleEquivSimple_restrict_along.

For each label position a : Fin K, fix the embedding r : Fin 1 ↪ Fin K sending 0 ↦ a. Restriction gives tupleEquivSimple at K=1 for the single coordinate. Apply diagonal_observable_K1 to conclude.

Status: proved modulo #77 (the K=1 spectral paper-root). This replaces the earlier sorry-stub diagonal_observable_of_tupleEquivSimple that was a placeholder pending the rank-theorem path. Routing through the K=1 spectral chain (#77) is more direct than the rank theorem.

Architectural consequence: #79's diagonal observable now reduces to #77 (K=1 spectral paper-root) rather than to a separate rank theorem. This collapses two paper-roots into one.

Downstream: any consumer of diagonal_observable_of_tupleEquivSimple (e.g., the n=0 loop bridge multiLabeledEvalKLoop_n_zero_of_diag) inherits dependency on #77.

theorem Graphon.Lovasz.orbit_separation_by_simple_graph {T K : ℕ} (B : Fin T → Fin T → ℝ) (_hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (_hW : ∀ (i : Fin T), 0 < W i) (_htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {ξ ξ' : Fin K → Fin T} (_h : ¬tupleOrbitRel B W ξ ξ') : ∃ (n : ℕ) (F : SimpleGraph (Fin (n + K))) (x : DecidableRel F.Adj), simpleEvalAt B W F ξ ≠ simpleEvalAt B W F ξ'

General-K orbit separation theorem (Lovász §3 contrapositive form).

If two tuples ξ ξ' : Fin K → Fin T are NOT in the same (B, W)-orbit, some level-K simple-graph evaluation separates them.

Status (2026-05-17): BLOCKED on multiLabeledEvalK_tupleEquiv_invariant (task #62, primary paper-root). The proof requires:

1. Strong induction on K.
2. Case-split on surjectivity of restrictTuple ξ.
3. For the non-surjective branch: WF measure on (deficit, size), which requires IH-free Claims 4.3/4.4 to avoid a circular IH at deficit-1 size-T-1.

The IH-free Claims need diagonal B(ψ i, ψ i) and pointwise W(ψ i) data, which are NOT extractable from simple-graph evaluations alone (see docstring of tupleEquivSimple_implies_orbit for full analysis). Both require multigraph evaluations — i.e., closing #62.

Path A (recommended): close #62, then derive #70 via IH-free Claims. Path B: direct combinatorial fiber construction (~300-500 LOC). Path C (current): treat as derived paper-root, blocked on #62.

Downstream K=1 specialization (rooted_profiles_separate_vertex_orbits, proved this session) handles the most-used case; this general-K target remains for completeness of the Lovász §3 chain.

theorem Graphon.Lovasz.orbit_separation_id {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {ψ : Fin T → Fin T} (h_no_orbit : ¬tupleOrbitRel B W id ψ) : ∃ (n : ℕ) (F : SimpleGraph (Fin (n + T))) (x : DecidableRel F.Adj), simpleEvalAt B W F id ≠ simpleEvalAt B W F ψ

Orbit separation, identity case — narrowest case of orbit_separation_by_simple_graph where K = T and the source tuple is the identity.

If ψ : Fin T → Fin T is NOT orbit-related to the identity tuple (under twin-free B and W > 0), some simple labeled graph separates the evaluations of id and ψ.

Status: proved as a thin wrapper around the general orbit_separation_by_simple_graph. The narrowed case is exposed as a named entry point for downstream consumers that only need separation against the identity tuple (e.g. the id-bijectivity branch of tupleEquivSimple_id_bijective).

Architectural note (Lovász §3, post-2026-05-12 analysis):

The "natural" reduction strategy — case-split ψ into non-bijective vs bijective — does NOT yield a shorter proof of this narrowed case.

Case A (ψ not bijective): contrapositive of tupleEquivSimple_id_bijective would deduce ¬ tupleEquivSimple B W id ψ and hence supply a separating F, BUT tupleEquivSimple_id_bijective itself depends on IH_orbit : ∀ ξ' ψ', tupleEquivSimple B W ξ' ψ' → tupleOrbitRel B W ξ' ψ' at Fin (T - 1). That IH is exactly the rank theorem at one smaller size, which is unavailable here without circular reasoning.

Case B (ψ bijective): tupleEquivSimple_bijective_case applied contrapositively reduces to a hypothesis-only contradiction; but the forward direction also takes an IH_orbit parameter.

In short, Case A and Case B are both non-trivial at the narrowest case, because the IH_orbit they require is itself the rank theorem at size T - 1. So orbit_separation_id is no easier than the general statement at its base. We therefore route through the canonical orbit_separation_by_simple_graph directly.

theorem Graphon.Lovasz.connection_matrix_rank_theorem {T K : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {ξ ξ' : Fin K → Fin T} (h : tupleEquivSimple B W ξ ξ') : tupleOrbitRel B W ξ ξ'

Connection-matrix rank theorem (Lovász TR-2004-82 §3 Theorem 2.2): under twin-free B and W > 0, tupleEquivSimple ⟹ tupleOrbitRel.

Proved as a contradiction proof from orbit_separation_by_simple_graph (the contrapositive form, where the canonical sorry now lives).

theorem Graphon.Lovasz.tupleEquivSimple_implies_orbit {T K : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {ξ ξ' : Fin K → Fin T} (h : tupleEquivSimple B W ξ ξ') : ∃ (σ : Equiv.Perm (Fin T)), (∀ (i : Fin T), W (σ i) = W i) ∧ (∀ (i j : Fin T), B (σ i) (σ j) = B i j) ∧ ∀ (i : Fin K), ξ' i = σ (ξ i)

Lovász TR-2004-82 Lemma 2.4 (simple-graph form, our framework).

If B is twin-free (i ≠ j → B i ≠ B j) and ξ ξ' agree on every simple-graph k-labeled evaluation (tupleEquivSimple), then they lie in the same (B, W)-automorphism orbit.

Proof structure (paper-faithful strong induction, mirrors tupleEquiv_implies_tupleOrbitRel in MatrixDetermination.lean:10873).

The proof is by strong induction on K, with IH supplied at every level < K (needed both at K - 1 for the restriction step, and at T - 1 for the surjective-base case Claim 4.4).

Steps in the inductive case m = k + 1:

1. Restrict to level k (Claim 4.1, tupleEquivSimple_restrict) and apply IH to extract an automorphism σ realizing the orbit relation between restrictTuple ξ and restrictTuple ξ'.
2. Normalize ξ' by σ.symm so that the first k coordinates agree (using tupleEquivSimple_of_tupleOrbitRel).
3. Express both as Fin.snoc of a common base α := restrictTuple ξ over a single last coordinate.
4. Case split on surjectivity of the base α:
   • α surjective ⟹ Claim "ext-eq-of-surj" (tupleEquivSimple_ext_eq_of_surj) forces the last coordinates to agree, giving orbit immediately.
   • α non-surjective, but ξ surjective ⟹ Claim 4.4 (tupleEquivSimple_surjective_case) at IH level T - 1.
   • Both α and ξ non-surjective: the architectural sorry branch. Lovász's standard plan goes through Claim 4.2 (extend by a fresh element r ∉ range α ∪ {a, b}) and recurses on a strictly smaller (deficit, size) measure. This requires a well-founded induction refactor on (deficit, size) which is beyond a strong Nat-induction on size alone.

Status: proved modulo (i) the Claim 4.2 sub-sorry (product_trace_identity_simple via tupleEquivSimple_extend), and (ii) a refined sorry at the inner-base of the deficit-induction in the non-surjective branch — specifically the case T - 1 ≥ k + 1 (i.e., T ≥ k + 2) where the outer strong-induction-on-K cannot supply the IH at size T - 1 required by tupleEquivSimple_surjective_case.

The architectural sorry has been REFACTORED: the previous "neither α nor ξ surj" case is now CLOSED via deficit-induction (Lovász's "extend-and-recurse") for the sub-case T ≤ k + 1. The residual sub-case T > k + 1 remains as a more specific sorry, requiring either a deeper refactor of tupleEquivSimple_surjective_case / tupleEquivSimple_id_bijective to avoid the deficit-1 IH (see MatrixDetermination.lean:11002-11007) or an alternative argument at that specific inner-base point.

Architectural obstacle (post-2026-05-12 subagent analysis): an IH-free bijective_case_direct / id_bijective_direct would close the residual but is not derivable from simple-graph evaluations alone with current Lovasz infrastructure. Specifically:

• B-preservation diagonal B(χ i, χ i) = B(i, i): simple graphs have no self-loops, so B(t, t) terms never appear in simple-graph evaluations. Cannot be extracted directly.
• W-preservation pointwise W(χ i) = W(i): single-unlabeled- vertex graphs evaluate to ∑_t W(t), ξ-independent. Row-sum graphs give scalar equations ∑_t W(t) B(i, t) = ∑_t W(t) B(χ i, t), not pointwise W.

These require either: (i) Multigraph evaluations (parallel edges / self-loops via multiplicity), reaching to multiLabeledEvalK_* infrastructure. (ii) Direct fiber construction at surjective_case level: σ(t) := ψ(any j with φ j = t), with well-definedness from path-length-2 / cherry motifs. ~300-500 lines of new combinatorial proofs.

The current tupleEquivSimple_id_bijective proof bridges this gap via the IH at T-1 (where deficit-1 supplies the missing automorphism τ to use as a B-aut for change-of-variable). Replacing this without IH requires substantive new infrastructure — beyond a simple refactor.

Claims 4.1, 4.3, 4.4 and tupleEquivSimple_ext_eq_of_surj are all closed inline. The wiring is paper-faithful and matches the structure of the (private) proof in Graphon/MatrixDetermination.lean.

theorem Graphon.Lovasz.tupleEquivMulti_implies_orbit {T K : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {ξ ξ' : Fin K → Fin T} (h : tupleEquivMulti B W ξ ξ') : ∃ (σ : Equiv.Perm (Fin T)), (∀ (i : Fin T), W (σ i) = W i) ∧ (∀ (i j : Fin T), B (σ i) (σ j) = B i j) ∧ ∀ (i : Fin K), ξ' i = σ (ξ i)

Lovász Lemma 2.5, reverse direction (multi-equivalence ⟹ orbit), twin-free hypothesis.

If B is twin-free (rows of B distinct: i ≠ j → B i ≠ B j) and ξ ξ' agree on every multigraph evaluation, then they lie in the same (B, W)-automorphism orbit.

Proof strategy (chain): multi-equivalence ⟹ simple-equivalence (tupleEquivSimple_of_tupleEquivMulti, trivial direction) ⟹ orbit (tupleEquivSimple_implies_orbit, the canonical sorry).

Closed modulo the canonical sorry on tupleEquivSimple_implies_orbit.

§4 — The bridge theorem (canonical sorry)

Stated abstractly: for any pair ξ ξ' such that ALL simple-graph evaluations agree (the simple-graph tupleEquiv predicate), every multigraph evaluation also agrees.

The hypothesis h_simple is the simple-graph version of tupleEquiv, inlined here so this module needs no dependency on Graphon/MatrixDetermination.lean.

theorem Graphon.Lovasz.multiLabeledEvalK_tupleEquiv_invariant_twinFree {T K n : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) (M : MultiLabeledGraph K n) {ξ ξ' : Fin K → Fin T} (h : tupleEquivSimple B W ξ ξ') : multiLabeledEvalK K n M B W ξ = multiLabeledEvalK K n M B W ξ'

Twin-free bridge (corollary). Under twin-freeness, the bridge follows by chaining through the orbit relation:

tupleEquivSimple → orbit (via tupleEquivSimple_implies_orbit) → multi-eval-equality (via multiLabeledEvalK_orbit_invariant).

This avoids the n+1 sorry of the general bridge. It does NOT subsume multiLabeledEvalK_tupleEquiv_invariant: the latter must hold for all B (including B with twins), while this version requires twin-freeness.

This is the RECOMMENDED reduction theorem (per post-2026-05-12 architectural decision): downstream twin-free consumers should route through THIS theorem (and hence the rank theorem) rather than the general non-twin-free bridge at L1327.

Dependency (post-rank-theorem-refactor): this proof routes through tupleEquivSimple_implies_orbit, which is now a thin wrapper over connection_matrix_rank_theorem (the named canonical root). Closing the rank theorem closes this reduction.

The earlier "self-cyclic" concern (about IH-free bijective case needing multigraph diagonal extraction = the bridge) is moot now: the rank theorem is the SINGLE primary root, and the bridge is secondary / off-axis.