Lovász §3 — Connection-matrix algebra and the multigraph bridge #
Historical note (resolved). The header below describes this module's original scaffolding mission (2026-05) and is retained as the design record. Every obligation it presents as live has since been proved in this file, sorry-free (the CI census enforces zero
sorrytokens repository-wide): the §4 bridgemultiLabeledEvalK_tupleEquiv_invariant(general, non-twin-free) and its twin-free corollary, the §2/§3 "stubs" (MultiLabeledGraph.empty/add/glue,multiLabeledEvalK_empty/_glue,tupleEquivMulti), the connection-matrix rank theorem (connection_matrix_rank_theorem) and the simple-graph Lemma 2.4 (tupleEquivSimple_implies_orbit, closed 2026-07-02 via the Cai–Govorov descent, #70). The counterpart inMatrixDetermination.leanis likewise proved. Also, the module now importsGraphon.CaiGovorov, so the "self-contained, noGraphon.*dependencies" line below is historical.
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 (historical — see note above) #
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 withmult : Sym2 (Fin (n + K)) → ℕandmultNoLoop.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 oflabeledEvalK_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 oftupleEquiv.multiLabeledEvalK_trace_closure— Lovász eq. 6, page 7.
§4 — The bridge theorem (DECLARED, sorry'd — since PROVED) #
multiLabeledEvalK_tupleEquiv_invariant— bridge (now proved below).
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). WithmultNoLoop, this is NOT extractable even via multigraph evaluations. A self-loop at label-position i with multiplicity 1 evaluates toB(ξ 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):
- Add
MultiLabeledGraphLoop K ncarrier WITHOUTmultNoLoop. - Define
multiLabeledEvalKLoopmirror includingB(τx, τx)^M.mult s(x,x). - Lift current
MultiLabeledGraphcontent via injectionMultiLabeledGraph → MultiLabeledGraphLoop. Existing #62 results transfer to no-loop multigraphs trivially. - State the full Lovász Theorem 2.2 over
MultiLabeledGraphLoop: simple-graphh_simple⟹ multi-loop evaluation equivalence. - 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
multiLabeledEvalKonly includes W at UNLABELED vertices. - Lovász's framework allows vertex weights
α(v)at all vertices (withα(label) = 1by 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.
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.
Instances For
Inject MultiLabeledGraph into MultiLabeledGraphLoop (forget
the multNoLoop constraint).
Instances For
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.
Instances For
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.
Instances For
No-loop reduction: when injected from MultiLabeledGraph, the
loop-aware evaluator agrees with multiLabeledEvalK (diagonal terms
contribute B^0 = 1).
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.
Orbit invariance of multiLabeledEvalKLoop (corollary).
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 fromtupleEquivSimple), 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.
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
Instances For
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.
The empty multigraph: zero multiplicity on every Sym2-pair.
Equations
Instances For
Pointwise addition of multiplicities (same vertex set). The
addition operation in the quantum-graph algebra 𝒢_k at fixed
unlabeled-vertex count.
Equations
Instances For
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.
Empty multigraph evaluation: every B-power factor is B^0 = 1,
so the σ-sum body collapses to the W-product.
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₁.multof the lift via emb₁. - M₂-only (both endpoints val < K or val ≥ K + n₁):
M₂.multof the lift via emb₂. - Cross (one M₁-unlabeled, one M₂-unlabeled): 0.
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.
Instances For
Unfold lemma for MultiLabeledGraph.glue.mult at an unordered pair s(a, b).
Star probe (Lovász level-1 single-vertex multigraph): the 1-labeled
multigraph on Fin (1 + 1) whose unique edge is the root–leaf pair s(0, 1),
carried with multiplicity a. Evaluating it reads the a-th W-weighted
neighbor moment of a vertex; see multiLabeledEvalK_starProbe.
Equations
Instances For
Star-probe evaluation reads the weighted neighbor moment. For symmetric
B, evaluating the multiplicity-a star probe at the singleton tuple · ↦ i
gives the a-th W-weighted power-sum of the i-row of B, ∑ₜ W t · B i t ^ a.
This grounds the abstract level-1 observable neighborMoment (in
Graphon/Spectral.lean) inside the multigraph orbit-separation algebra: the
single-vertex multigraph evaluations ARE the weighted neighbor moments.
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.
Instances For
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.
Instances For
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) #
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
Instances For
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
Instances For
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.
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.
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.5b — Decorated star probe (refinement-step graph realization) #
Building blocks for realizing the weighted-WL refinement operator refineMoment
(in Graphon/Spectral.lean) as a multigraph evaluation: an edgeProbe (the
root–leaf edge as a 2-labeled graph) and a reroot1 operation (view a 1-labeled
multigraph Mχ as 2-labeled by inserting a fresh isolated label 0, moving its
old root to label 1 via Fin.succ). Gluing them and tracing the leaf label
gives the decorated probe whose evaluation is ∑ₜ W t · B i t ^ a · (Mχ-eval at t).
The coloring τ used inside multiLabeledEvalK: labels (v < K) map via the
tuple φ, unlabeled vertices via the σ-assignment. Named so that evaluations can
be reindexed (the anonymous let in multiLabeledEvalK blocks higher-order
unification).
Instances For
multiLabeledEvalK with its inner let exposed as the named multiTau.
Edge probe (2-labeled, no unlabeled vertices): the single edge
s(0, 1) between the two labels, multiplicity a.
Equations
Instances For
Reroot: view a 1-labeled multigraph as 2-labeled by inserting a fresh
isolated label 0 and shifting every vertex up by one (Fin.succ), so the old
root (label 0) becomes label 1. The new label 0 carries no edges.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reroot evaluation: reroot1 Mχ evaluated at φ reads Mχ at the
singleton tuple given by φ's second label (the new root); the isolated first
label φ 0 does not appear.
Decorated star probe: glue the rerooted Mχ (its old root now the leaf
label 1) to the root–leaf edgeProbe a (labels 0–1), then trace the leaf
label 1 into a new unlabeled vertex. A 1-labeled multigraph (root 0)
realizing the weighted-WL refinement step.
Equations
Instances For
Decorated-probe evaluation realizes the refinement operator. For
symmetric B, evaluating decoratedProbe a Mχ at · ↦ i gives
∑ₜ W t · B i t ^ a · (Mχ-eval at t) — the refined neighbor moment with feature
χ t = multiLabeledEvalK 1 m Mχ B W (· ↦ t).
§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.
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 φ.
Orbit-based invariance: corollary of multiLabeledEvalK_aut_invariant.
If ξ' = σ ∘ ξ for some (B, W)-automorphism σ, multigraph
evaluations agree.
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.
§3.7 — Rank algebra (closure-of-simple-evals) #
Canonical algebraic framework for the multigraph bridge (#62). Per
Lovász TR-2004-82 §3: define the closure of simple-graph evaluations
under +, *, smul, const, prove the closure descends to
tupleEquivSimple-classes (trivial induction), and state the canonical
paper-root: every multigraph evaluation lies in the closure.
The closure uses the inlined simple-graph evaluation form (matching
the h_simple hypothesis of multiLabeledEvalK_tupleEquiv_invariant),
avoiding a forward dependency on simpleEvalAt (defined at L2381).
Closure of simple-graph evaluations (inlined form, before
simpleEvalAt is in scope). A function f : (Fin K → Fin T) → ℝ is in
the closure iff it can be built from simple-graph evaluations using ring
operations. The base case of_simple uses the explicit ∑ σ ... * ∏ B
expansion, matching the h_simple hypothesis of #62.
- of_simple {T : ℕ} {B : Fin T → Fin T → ℝ} {W : Fin T → ℝ} {K : ℕ} (n : ℕ) (F : SimpleGraph (Fin (n + K))) [DecidableRel F.Adj] : InSimpleProfileClosure B W K fun (ξ : Fin K → Fin T) => ∑ σ : Fin n → Fin T, let τ := 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)
- const {T : ℕ} {B : Fin T → Fin T → ℝ} {W : Fin T → ℝ} {K : ℕ} (c : ℝ) : InSimpleProfileClosure B W K fun (x : Fin K → Fin T) => c
- add {T : ℕ} {B : Fin T → Fin T → ℝ} {W : Fin T → ℝ} {K : ℕ} {f g : (Fin K → Fin T) → ℝ} : InSimpleProfileClosure B W K f → InSimpleProfileClosure B W K g → InSimpleProfileClosure B W K fun (ξ : Fin K → Fin T) => f ξ + g ξ
- smul {T : ℕ} {B : Fin T → Fin T → ℝ} {W : Fin T → ℝ} {K : ℕ} (c : ℝ) {f : (Fin K → Fin T) → ℝ} : InSimpleProfileClosure B W K f → InSimpleProfileClosure B W K fun (ξ : Fin K → Fin T) => c * f ξ
- mul {T : ℕ} {B : Fin T → Fin T → ℝ} {W : Fin T → ℝ} {K : ℕ} {f g : (Fin K → Fin T) → ℝ} : InSimpleProfileClosure B W K f → InSimpleProfileClosure B W K g → InSimpleProfileClosure B W K fun (ξ : Fin K → Fin T) => f ξ * g ξ
Instances For
Closure functions descend to h_simple-equivalent tuples. Takes
the inlined tupleEquivSimple-form hypothesis (matching #62's
h_simple).
Closure under subtraction: f - g ∈ closure if both are.
Closure under Finset.sum over an index set.
Closure under Finset.prod over an index set.
§3.8 — Architecture for closing #86 #
The closure infrastructure above (InSimpleProfileClosure with descends,
algebra closures, zero/add/sub/smul/mul/finset_sum/finset_prod)
provides the building blocks. The path to #86:
Lagrange fullness: prove
of_const_on_tupleEquivSimple— everytupleEquivSimple-invariant function is in the closure. Pure Lagrange interpolation, ~200 LOC. Mirrors K=1of_const_on_orbit.Multigraph descent: prove multigraph evaluations are
tupleEquivSimple-invariant. THIS IS THE SUBSTANTIVE LOVÁSZ §3 CONTENT (cannot be assumed; must be proved by the connection-matrix idempotent decomposition or polynomial-decomposition argument).Combine: #86 follows from steps 1 + 2.
Both steps are non-trivial. Step 1 is finite algebra/Lagrange (doable with the K=1 chain pattern). Step 2 is the remaining real Lovász §3 content. Splitting them clarifies what's needed but does not reduce the algebraic burden.
For now, #86 remains the canonical paper-root. Stating step 1 separately would just add a sorry without progress — defer to a focused Lagrange session where the proof can actually close.
Historical note (resolved): the plan above describes the state as of
2026-06. Both steps have since been proved — Step 1 as
of_const_on_tupleEquivSimple (§3.9 below), Step 2 via
multigraphEval_in_simpleProfileClosure and the Cai–Govorov descent —
and #86 is closed.
§3.9 — Lagrange fullness (Step 1 toward #86) #
Step 1 of #86: every function constant on (inlined) tupleEquivSimple-
classes is in InSimpleProfileClosure.
Proof: Lagrange interpolation. For each pair (ξ, ξ') with distinct
simple-graph profiles, fix a separating graph (via mkTupleSimpleSeparator).
Build per-tuple Lagrange indicators via products of inlineSimpleEval_lagrange_factors.
Express any tupleEquivSimple-invariant function as a linear combination of
indicators using finset_sum and smul.
Status (2026-06-10): FULLY PROVED, axiom-clean (an earlier revision of this docstring incorrectly said "currently sorry'd"). #86's remaining content is "multigraph evaluations are tupleEquivSimple-invariant" (Step 2, the substantive Lovász §3 descent).
§3.9.5 — Multiplicity peel infrastructure (for LL-excess sub-case) #
Helpers for closing the LL-excess sub-case of #86 via polynomial decomposition. The key identity is the "single label-label peel":
multiLabeledEvalK M B W ξ = B(ξ_a, ξ_b) * multiLabeledEvalK (M.decAt s(a, b)) B W ξ
valid for any label-label edge (a, b) (both a.val, b.val < K) with
M.mult s(a, b) ≥ 1. Iterating across LL edges reduces M to its
LL-kernel (LL multiplicities all zero), which is a simple graph when
all non-LL multiplicities are ≤ 1.
§3.6.4 — The bridge via h_orbit (Lovász Lemma 2.4) #
KEY INSIGHT (2026-05-26): given h_orbit (Lovász Lemma 2.4
packaged: tupleEquivSimple ξ ξ' ⟹ ∃ σ aut with ξ' = σ ∘ ξ),
the entire multiLabeledEvalK ξ = multiLabeledEvalK ξ' equality
holds by pure change-of-variables for ANY multigraph M.
This sidesteps the entire dispatcher chain (UU isolated, label-U isolated/nonisolated, UU nonisolated, etc.) — the ~2000 LOC of case analysis collapses to ~30 LOC of change-of-variables.
Trade-off: requires h_orbit (Lemma 2.4), which itself has an
architectural sorry at the "both non-surj" branch. But the existing
dispatcher chain ALSO depends on this same sorry (via the K=1 rank
theorem's reliance on k1_orbit_sep_aux → Lemma 2.4 at K=1). So net
no new sorries. (Historical note, resolved: the "both non-surj" branch
was subsequently proved — tupleEquivSimple_implies_orbit, closed
2026-07-02 via the Cai–Govorov descent — so h_orbit is sorry-free.)
Caveats addressed:
- W-product invariance: ∏ W(σ σ_var v) = ∏ W(σ_var v) by W-aut.
- B-product invariance: per edge e, B(τ_e via ξ' at σ σ_var) = B(τ_e via ξ at σ_var) by B-aut + ξ' = σ ξ.
- Sum reindex:
Equiv.arrowCongr (Equiv.refl _) σshifts σ_var.
Multigraph evaluation invariance under orbit relation. Direct change-of-variables proof; closes the entire bridge for ANY multigraph.
§3.6.5 — Mixed-moment theorem for label-extras #
The label-extras mixed moment: given tupleEquivSimple ξ ξ' and an
ambient h_orbit (Lovász Lemma 2.4: simple-equivalence ⟹ orbit),
the ξ-parameterized polynomial moment
∑ t, W t · B (ξ a) t ^ 2 · ∏ b, B t (ξ b) ^ r b
agrees at ξ vs ξ'. This is the substantive content of the
nonisolated label-U case (the doubled edge contributes the square
factor; label-extras incident to the unlabeled endpoint contribute the
background product).
Proof technique: pure change-of-variables. Given h_orbit (which
provides σ : Perm with ξ' = σ ∘ ξ, W and B σ-invariant), substitute
t ↦ σ⁻¹ t in the RHS sum. The σ-aut of B gives B (σ x) (σ y) = B x y,
which transforms each B-factor cleanly. No K=1 rank theorem needed
(unlike the pure square moment, where ξ doesn't appear as a parameter
of the B-product).
Mixed-moment theorem for label-extras. Under h_orbit
(Lovász Lemma 2.4 packaged), the ξ-parameterized moment
∑ t, W t · B (ξ a) t ^ 2 · ∏ b, B t (ξ b) ^ r b
is constant on tupleEquivSimple-classes. Closes the LABEL-extras
branch of the nonisolated subcases via reduction to change-of-variables.
For UNLABELED-extras (incident edges to the doubled endpoint with the
other endpoint also unlabeled), a separate argument is needed; this
mixed moment alone does not close those subcases.
§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-graphtupleEquivinlined here so this module needs no dependency onGraphon/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.
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.
Instances For
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 ξ'
Instances For
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.
Instances For
Loop ⟹ multi (trivial direction via the toLoop injection).
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 — PROVED via
rootedProfileEquiv_imp_vertexOrbitRel (the rank-theorem route; the historical
#77 closed-walk route was refuted and removed).
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).
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 status list below is historical
(it described the state at the time): every item, including the then-named
sub-sorry product_trace_identity_simple and the non-surjective branch,
has since been fully proved. The status at the time:
- Claim 4.1 (
tupleEquivSimple_restrict) — proved. - Claim 4.2 (
tupleEquivSimple_extend) — proved MODULO the named sub-sorryproduct_trace_identity_simple(the LIST-product trace identity; the Lovász §3 deep content). The class-constancy stepcoeffRestrictSimple_equivis now proved as a wrapper aroundfunctional_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 atT-1+ bijection-uniqueness). - Claim 4.4 (
tupleEquivSimple_surjective_case) — proved via the helperstupleEquivSimple_restrict_along(restriction along an arbitrary label-index injection) andtupleEquivSimple_id_bijective(twin-free + W>0 forcestupleEquivSimple 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).
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
Instances For
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)
Instances For
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
Instances For
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
Instances For
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
Instances For
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.
Surjectivity reads off rangeFinset = univ.
Surjectivity iff deficit = 0.
If φ is not surjective, some a : Fin T is missing from the
range.
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.
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 byt = μ (Fin.last k), which makes the indicatortupleEquivSimple μ μtrue by reflexivity).coeffRestrictSimple_equiv— class constancy: simple-equivalence ofξandξ'transferscoeffRestrictSimple B W μ ξ = coeffRestrictSimple B W μ ξ'. PROVED viafunctional_span_zeroproduct_trace_identity_simple(the latter was a focused sub-sorry capturing the Lovász §3 deep content at the time; it has since been proved in §3.9.3).
exists_extension_of_coeffRestrictSimple_pos— from positivity, sometmakes the indicator true, yielding the extension.
The class-constancy step is now proved structurally. What was then the
single remaining architectural hurdle — the LIST-product trace identity
product_trace_identity_simple (Lovász §3 / DecLabeledGraph) — has
since been proved.
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
Instances For
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.
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 (formerly a named focused sorry; since PROVED).
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 prove the LIST-product trace
identity (originally stated here as a focused sorry — the genuine
Lovász §3 content, then the SOLE remaining gap for
coeffRestrictSimple_equiv below; it has since been proved in this
section).
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.
Instances For
Quot.out resolver on a literal Sym2 pair over an ARBITRARY vertex type
(the out_pair_eq generalization needed for structured graphs). Moved here from
CycleKrylov.lean (2026-07-02) so the Cai–Govorov stack below can use it.
The Cai–Govorov stack (formerly Graphon/CaiGovorovOrbit.lean, dissolved 2026-07-02) #
The full Cai–Govorov orbit-separation route for #70, culminating in the general
tupleEquivSimple_implies_orbit_general: equal simple-graph evaluations imply
weighted-automorphism orbit equivalence, with no surjectivity hypothesis.
- Test graphs + closed forms:
starTestGraph S(Gχ, one unlabeled vertex joined toS ⊆ Fin K; eval= ∑ₜ W t · ∏_{i∈S} B (ξ i) t) andedgeTestGraph Sₗ Sτ(Gλτ, two adjacent unlabeled vertices; the double-sum closed form). - Chunk 3A / 4A — the super-surjective case, moment form
(
testEvalEq_implies_orbit_superfrom theTestEvalEqstar/edge interface, with thetupleEquivSimple_implies_orbit_superwrapper): pigeonhole + bounded Vandermonde buildsuperMap/superPerm, edge moments certify it as a weighted automorphism, one-extra-label moments reconcile all labels. - Chunk 3B — eq. (10)
extension_sum_identity(extension-family sums collapse via the iterated trace) with thesuperExt/coverExtrasuper-surjective extension (plus the documented separation corollarynot_tupleEquivSimple_of_not_orbit, not on the live path). - Chunks 4B–4E — the mult ≤ 1
toSimplebridge andglueListproduct law realize test-moment powers as single simple graphs (expTestGraph), so eq. (10) yields the power-moment identityextension_power_moments. - Chunks 4F–4G — the descent: two-family Vandermonde matches an extension of
ξ'againstsuperExt ξ(exists_matching_extension), the super-case runs at levelK + T·2T², and restriction gives the general theorem.
Downstream in this file, the stack fills orbit_separation_by_simple_graph and the
"both non-surjective" branch of tupleEquivSimple_implies_orbit (§3.10), and powers the
rank endgame (simpleEvalSubmodule_finrank_ge_orbitClass and the collapse
simpleEvalSubmodule = orbitInvariantSubmodule, § RankTheorem after
simpleEvalAt_aut_invariant).
Cai–Govorov test graph Gχ: the unlabeled vertex is joined to exactly the
labels in S ⊆ Fin K.
Equations
- Graphon.Lovasz.starTestGraph S = SimpleGraph.fromEdgeSet ↑(Finset.image (fun (i : Fin K) => s(Graphon.Lovasz.labVertex i, Graphon.Lovasz.unlVertex)) S)
Instances For
The simpleEvalAt label map sends labVertex i to ξ i (stated in the
beta-reduced dite form produced by out_pair_eq').
Cai–Govorov edge-test graph Gλτ (two unlabeled vertices) #
Cai–Govorov edge-test graph Gλτ: the two unlabeled vertices are joined to each
other, vertex 0 is joined to the labels in Sₗ, and vertex 1 to the labels in Sτ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
simpleEvalAt label map: labVertex2 i ↦ ξ i (beta-reduced dite form).
simpleEvalAt label map: unlVertex0 ↦ σ 0 (beta-reduced dite form).
simpleEvalAt label map: unlVertex1 ↦ σ 1 (beta-reduced dite form).
Closed form for Gλτ:
simpleEvalAt B W (edgeTestGraph Sₗ Sτ) ξ = ∑ₜ ∑ₜ' W t · W t' · B t t' · ∏_{i∈Sₗ} B (ξ i) t · ∏_{i∈Sτ} B (ξ i) t'.
Chunk 3A: super-surjective orbit separation (Cai–Govorov Lemma 5.1, base case) #
ξ : Fin K → Fin T is super-surjective when every host vertex v is the image of
at least 2·T² labels. This Cai–Govorov hypothesis provides the room to realize every
bounded exponent vector in the Vandermonde argument (by pigeonhole it yields, inside each
ξ-fibre, a ξ'-constant subset of size ≥ 2T, aligning the exponents on both sides).
Instances For
Multiplicity form of the Gχ equation. Simple-equivalence makes the two
host-multiplicity-weighted moment sums agree, for every label subset S.
NB not on the live path: the working bridge to the Vandermonde input is
aligned_moments_of_testEvalEq_super, which derives the moment identity directly from
TestEvalEq.star. Kept as the standalone multiplicity-form record of the Gχ equation.
Test-graph evaluation equality — the moment-level interface to the chunk-3A engine.
Records exactly the two families of simple-graph equalities the super-surjective argument
consumes: the star tests Gχ and the edge tests Gλτ. Weaker than tupleEquivSimple
(which quantifies over ALL simple graphs); the descent step (chunk 4F) produces instances
of this interface from eq. (10) moment matching, where full tupleEquivSimple is not
available.
- star (S : Finset (Fin K)) : simpleEvalAt B W (starTestGraph S) ξ = simpleEvalAt B W (starTestGraph S) ξ'
- edge (Sₗ Sτ : Finset (Fin K)) : simpleEvalAt B W (edgeTestGraph Sₗ Sτ) ξ = simpleEvalAt B W (edgeTestGraph Sₗ Sτ) ξ'
Instances For
Full simple-equivalence yields the test-graph interface.
Aligned-Vandermonde extraction (graph-free core of chunk 3A). If the moment sums of
two profile families x, y (weighted by a, b) agree for every exponent vector bounded
by 2·T, then the a-mass and b-mass over each profile level set agree. The combined index
Fin T ⊕ Fin T turns the equality into a single multivariate Vandermonde cancellation
(Graphon.CaiGovorov.multivariate_vandermonde_class_sums_zero).
NB the exponent bound is 2·T, not T+1: the combined index has 2T points, and with only
T+1 moments the statement is already false at T = 2 (3 equations cannot pin a signed measure
on 4 points). This matches Cai–Govorov's range 0 ≤ k_j < 2m.
Bounded-exponent aligned-Vandermonde extraction. The bounded analogue of
aligned_moments_class_balance: an explicit per-coordinate distinct-value bound N replaces the
implicit cardinality |ι|, and the cancellation runs through the bounded multivariate Vandermonde
(Graphon.CaiGovorov.multivariate_vandermonde_class_sums_zero_of_bound). The combined index has at
most 2·N distinct values per coordinate, matching the exponent range 0 ≤ k_c < 2·N.
Profile-balance specialization: with x t = B · t (the profile/column of t),
y t = B (s ·) t, and weights a = b = W, the aligned moments force the W-mass over each
profile level set to match.
Weight balance. Twin-freeness collapses the left profile level set of t to the
singleton {t}, so the aligned Vandermonde output is exactly W t = ∑_{u : B·t = B(s·)u} W u.
Support. From weight balance and positivity, every host vertex t is matched: there is a
u with B j t = B (s j) u for all j. (The Vandermonde engine builds the matching.)
Chunk 3A.2: pigeonhole and the preliminary map s #
Pigeonhole. Super-surjectivity gives, inside each ξ-fibre over j, a subset J of
size ≥ 2T on which ξ' is constant (value s_j). (ξ' takes ≤ T values on the fibre of
size ≥ 2T², so some value is hit ≥ 2T times.)
The preliminary Cai–Govorov map s : Fin T → Fin T: the constant ξ'-value on a large
subset of each ξ-fibre.
Equations
- Graphon.Lovasz.superMap ξ ξ' hξ j = ⋯.choose
Instances For
The chosen large ξ'-constant subset of the ξ-fibre over j.
Equations
- Graphon.Lovasz.superFiberSubset ξ ξ' hξ j = ⋯.choose
Instances For
Distinct fibres give disjoint chosen subsets (each lies in a distinct ξ-fibre).
Chunk 3A.3: aligned moments from selected labels #
For any bounded exponent vector k, select inside each ξ-fibre's distinguished subset a
sub-subset of size exactly k j.
Aligned-moment bridge. From the star-test equalities (TestEvalEq.star) and
super-surjectivity, the aligned moment identity holds for every bounded exponent vector, with the
right-hand side reindexed by superMap.
This consumes the starTestGraph closed form: the label set S = ⋃ⱼ Kⱼ has ξ ≡ j on Kⱼ (giving
(B j t)^{k j} on the left) and ξ' ≡ superMap j on Kⱼ (giving (B (superMap j) t)^{k j} on the
right) — no injectivity of superMap is needed.
superMap support: every host vertex t is matched
by the preliminary map — there is a u with B j t = B (superMap … j) u for all j. Combines the
aligned-moment bridge with the proved aligned-Vandermonde support lemma.
superMap is injective. If superMap a = superMap b, then for every t the support
witness u gives B a t = B (superMap a) u = B (superMap b) u = B b t, so the rows B a, B b
agree; twin-freeness forces a = b. (No edge tests needed.)
superMap is bijective (injective endomap of a finite type).
The preliminary map as a permutation of Fin T. The orbit-defining automorphism σ will be
exactly this permutation (since ξ' i = superMap (ξ i) on the selected labels, σ = superMap,
not its inverse); edge/weight preservation are established next (3A.5) via edgeTestGraph.
Equations
- Graphon.Lovasz.superPerm B hB W hW htwin ξ ξ' hξ h = Equiv.ofBijective (Graphon.Lovasz.superMap ξ ξ' hξ) ⋯
Instances For
Chunk 3A.5: aligned edge moments (edgeTestGraph) #
Aligned edge-moment bridge (pair analogue of aligned_moments_of_testEvalEq_super).
From the edge-test equalities (TestEvalEq.edge) and super-surjectivity, the aligned
edge-moment identity holds for every pair of bounded exponent vectors k, l, with the
right-hand side reindexed by superMap. This
consumes the edgeTestGraph closed form: with Sₗ = ⋃ⱼ Klⱼ, Sτ = ⋃ⱼ Ktⱼ one has ξ ≡ j on
each block (giving (B j ·)^{k j}/(B j ·)^{l j}) and ξ' ≡ superMap j (giving the reindexed
right-hand side) — no injectivity of superMap is needed.
Aligned edge-moment pair balance. Specializing the bounded extraction engine
aligned_moments_class_balance_of_bound at ι = Fin T × Fin T and coordinate dimension T + T
(gluing the two B-columns of a pair via Fin.append), the aligned edge moments force the
W·W·B-mass over each pair of column profiles (z₁, z₂) to match between the original labelling and
the superMap-reindexed one.
Chunk 3A.5 steps 2–7: the support-witness map and the weighted automorphism #
The support-witness map r = superInv: r t is the unique u with
∀ j, B j t = B (superMap j) u. It turns out to be the orbit automorphism (= superMap).
Equations
- Graphon.Lovasz.superInv B hB W hW htwin ξ ξ' hξ h t = ⋯.choose
Instances For
Weight preservation for superInv. The support fibre of t is the singleton
{superInv t}, so weight balance gives W (superInv t) = W t.
Edge preservation for superInv. Plugging the pair balance at z₁ = B·a, z₂ = B·b:
the left fibre is {(a,b)} (twin-free) and the right fibre is {(superInv a, superInv b)}
(superInv_unique); positivity cancels the weights. So superInv preserves B.
superInv = superMap. Support gives B a b = B (superMap a) (superInv b), and edge
preservation gives B a b = B (superInv a) (superInv b); comparing over all columns
(superInv surjective) and applying twin-freeness identifies the two maps.
Chunk 3A.5 exports: superMap is a weighted automorphism #
The super-surjective orbit automorphism. superPerm is a weighted automorphism of
(B, W) — the certified output of chunk 3A.5.
One-extra-label raw moment identity. Attaching a single distinguished label i₀ to a
star-test graph and selecting disjoint exponent blocks inside the (large) super-fibres minus
{i₀}, the tupleEquivSimple equality on the star graph yields the raw moment identity with one
extra B (ξ i₀) t / B (ξ' i₀) t factor. Reindexing the right-hand side by the orbit permutation
superMap (which preserves W and B) turns B (ξ' i₀) t into B (ξ' i₀) (superMap t) while
restoring the aligned exponent product ∏ⱼ (B j t) ^ k j.
Full-fibre reconciliation (3A.6). Every label i maps under ξ' to superMap (ξ i) —
not only the labels in the selected subsets. The one-extra-label moment identity feeds the
(graph-free) Vandermonde class-sum over Fin T: twin-freeness makes each profile fibre a
singleton, positivity gives B (ξ i₀) t = B (ξ' i₀) (superMap t) for all t, and applying the
automorphism property identifies ξ' i₀ = superMap (ξ i₀).
Chunk 3A core — the super-surjective Cai–Govorov orbit separation, moment form. If ξ
is super-surjective and the star/edge test evaluations agree (TestEvalEq), then ξ' is in the
weighted-automorphism orbit of ξ. Combines superMap_isWeightedAutomorphism with the
full-fibre reconciliation. The TestEvalEq interface (rather than full tupleEquivSimple) is
what the eq. (10) descent step can supply for matched extensions.
Chunk 3A — the super-surjective Cai–Govorov orbit separation. If ξ is super-surjective
and ξ ≈ ξ' (equal simple-graph evaluations), then ξ' is in the weighted-automorphism orbit of
ξ. Wrapper around the moment-form core testEvalEq_implies_orbit_super.
Chunk 3B.1b: iterating the trace over the extra labels #
The trace operator MultiLabeledGraph.trace folds the last label into a new unlabeled
vertex. Iterating it m times folds the last m labels of a (K+m)-labeled multigraph,
yielding a K-labeled multigraph on n + m unlabeled vertices. The closure identity
multiLabeledEvalK_sum_last_label then accumulates into a W-weighted sum over the m
folded label values (ρ : Fin m → Fin T).
Unlabeled re-cast of a multigraph. Reindex the vertex space Fin (b + K) of a target
multigraph onto Fin (a + K) through the val-preserving Fin.cast, when a = b. Used to
reconcile (n + 1) + m with n + (m + 1) in traceIterExtraLabels.
Equations
Instances For
Iterated trace over the last m labels. Folds the last m labels of a (K+m)-labeled
multigraph into m new unlabeled vertices, yielding a K-labeled multigraph on n + m
unlabeled vertices. Recurses on m, threading MultiLabeledGraph.trace and reconciling the
(n+1)+m = n+(m+1) vertex-count mismatch with castUnlabeled.
Equations
Instances For
Eq. (10) core (3B.1 pillar). Unpinning the last m labels: summing the (K+m)-labeled
evaluation over the extra label values ρ, weighted by ∏ⱼ W(ρ j), equals the K-labeled
evaluation of the m-fold trace traceIterExtraLabels m M. Induction on m, peeling the last
label each step via multiLabeledEvalK_sum_last_label. Purely multigraph-side; bridged to simple
graphs by traceIterExtraLabels_ofSimple_eq and fed into extension_sum_identity.
Chunk 3B.1c step 2: the trace-to-simple eval bridge #
Local (public) connector: simpleEvalAt is multiLabeledEvalK on ofSimple
(the file-local analog of the private simpleEvalAt_eq_multi in Lovasz).
Unlabel-extras simple graph. Comap of G along the val-preserving cast
Fin ((n + m) + K) → Fin (n + (K + m)), moving the last m labels back into unlabeled
position. The trace bridge (traceIterExtraLabels_ofSimple_eq) identifies
traceIterExtraLabels m (ofSimple G) with ofSimple (unlabelExtras G).
Equations
Instances For
Net-cast lemma (the crux). The iterated trace/castUnlabeled reindexing collapses to
a single val-preserving Fin.cast: reading a multiplicity of traceIterExtraLabels m M at e
equals reading M's multiplicity at the cast of e.
Graph bridge. Iterating the trace over the extra labels of an ofSimple multigraph
yields the ofSimple multigraph of the unlabel-extras simple graph.
Eval bridge (the step-2 target). Evaluating the traced ofSimple G multigraph equals the
simple-graph evaluation of the unlabel-extras graph.
Chunk 3B.1c steps 3–5: extension family (extras-last) and equation (10) #
μ : Fin (K + m) → Fin T extends ξ if it agrees with ξ on the first K labels.
(abbrev so the subtype {μ // ExtendsFin ξ μ} gets DecidablePred/Fintype automatically.)
Equations
- Graphon.Lovasz.ExtendsFin ξ μ = ∀ (i : Fin K), μ (Fin.castAdd m i) = ξ i
Instances For
The W-product over the m extra label values of μ.
Equations
- Graphon.Lovasz.extensionWeightFin W μ = ∏ j : Fin m, W (μ (Fin.natAdd K j))
Instances For
Extensions of ξ are exactly Fin.append ξ ρ for the free extra-value tuple ρ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extension-sum collapse (one side of eq. (10)). The weighted sum of simpleEvalAt G
over ALL extensions of ζ collapses to a single simple evaluation at ζ — of the
unlabel-extras graph. Extracted from extension_sum_identity; reused by the rank-residue
annihilator argument (chunk 5B).
Equation (10) (Cai–Govorov, the extension-family sum identity). Simple-equivalence at
level K lifts to an equality of extension-family sums at level K + m: unpinning the extra
labels (trace-to-simple bridge) reduces both sides to simpleEvalAt of unlabelExtras G, where
h applies.
Chunk 3B.2a: the concrete super-surjective extension of ξ (extras-last) #
The extra-value tuple that maps 2*T² labels to each host vertex. Uses the product equiv
Fin T × Fin (2*T²) ≃ Fin (T * (2*T²)): label j maps to the vertex component of j.
Equations
- Graphon.Lovasz.coverExtra T j = (finProdFinEquiv.symm j).1
Instances For
The canonical super-surjective extension of ξ: keep ξ on the first K labels, then add
T * (2*T²) extra labels covering every host vertex 2*T² times.
Equations
Instances For
Chunk 3B.2b: separation (contrapositive of the super-surjective case) #
Separation at the super-surjective reference (contrapositive of
tupleEquivSimple_implies_orbit_super at η = superExt ξ): any extension μ not in the
weighted-automorphism orbit of superExt ξ is not simple-equivalent to it — some simple
graph separates them.
NB not on the live descent path: the paper's plan built a finite separating family from this
oracle, but the formalized descent (chunk 4F, exists_matching_extension) runs the
class-balance Vandermonde directly and never consumes this statement. Kept as the documented
separation form of the super-case.
Chunk 4B: the mult ≤ 1 bridge — multigraphs that are secretly simple #
Products of test evaluations are realized (chunks 4C/4D) as glues of ofSimple test
multigraphs. Since the test graphs have no label-label edges, the glued multiplicities never
exceed 1, and such a multigraph converts back to an honest SimpleGraph with the same
evaluation. This section provides the invariants (SimpleMult, NoLabelPairs), the
conversion (toSimple with ofSimple_toSimple/simpleEvalAt_toSimple), and preservation of
the invariants under glue — where label-label pairs are the ONLY place multiplicities add,
which is exactly what NoLabelPairs forbids.
All multiplicities are at most 1 — the multigraph is (the ofSimple image of) a simple
graph.
Instances For
No edge joins two labeled vertices (labels sit at values < K). Under glue, label-label
pairs are the only place multiplicities ADD; this invariant keeps the glue multiplicity-safe.
Instances For
Convert a multigraph back to a simple graph: edges are the multiplicity-1 pairs. Inverse to
MultiLabeledGraph.ofSimple on multiplicity-≤-1 multigraphs (ofSimple_toSimple).
Instances For
Multigraphs with equal multiplicity functions are equal (multNoLoop is a proposition).
toSimple is a section of ofSimple on multiplicity-≤-1 multigraphs.
Evaluating the simple graph M.toSimple agrees with the multigraph evaluation of M,
provided all multiplicities are ≤ 1.
Every starTestGraph edge touches the unlabeled vertex (value K), so there are no
label-label edges.
Every edgeTestGraph edge touches an unlabeled vertex (values K, K+1), so there are no
label-label edges.
glue preserves multiplicity ≤ 1, given NoLabelPairs on the second factor: the only
pairs where the two glue contributions can BOTH be nonzero are label-label pairs, and there
the M₂ contribution vanishes.
glue preserves the no-label-pairs invariant.
Chunk 4C: gluing lists of multigraphs — the iterated product law #
glueList folds a list of K-labeled multigraphs (of varying unlabeled sizes, packaged in a
sigma type) into one by repeated disjoint gluing; its evaluation is the product of the
component evaluations (iterating multiLabeledEvalK_glue), and it inherits the chunk-4B
invariants from its components.
Sigma-packaged disjoint glue of two multigraphs with arbitrary unlabeled sizes.
Instances For
Fold a list of multigraphs into one by repeated disjoint gluing (empty multigraph base).
Equations
Instances For
Iterated glue factorization: the evaluation of glueList l is the product of the
component evaluations.
glueList inherits NoLabelPairs from its components.
glueList inherits SimpleMult from components that also satisfy NoLabelPairs.
Chunk 4D: the test-moment profile and its exponent graphs #
The Vandermonde step classifies extensions by their vector of star/edge test moments
(testMoment). The moment products ∏_c moment_c^{k c} demanded by the multivariate
Vandermonde are realized as simpleEvalAt of a single simple graph expTestGraph k:
glue k c copies of each coordinate's test graph (a multigraph a priori, but mult ≤ 1 by
chunk 4B since test graphs have no label-label edges) and convert back via toSimple.
The closed-form moment of a test coordinate at the tuple μ (the simpleEvalAt value of
the corresponding test graph, see coordGraph_eval).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The test coordinate's graph, as a sigma-packaged ofSimple multigraph.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exponent graph: glue k c copies of each test coordinate's graph.
Equations
- Graphon.Lovasz.expGraph k = Graphon.Lovasz.glueList (List.flatMap (fun (c : Graphon.Lovasz.TestCoord K) => List.replicate (k c) (Graphon.Lovasz.coordGraph c)) Finset.univ.toList)
Instances For
Closed form of the exponent graph: its evaluation is the product of test-moment powers.
The exponent graph, converted back to an honest simple graph (chunk 4B).
Equations
Instances For
The moment-power realization: simpleEvalAt of the exponent test graph is the
product of test-moment powers. This is the input eq. (10) consumes in chunk 4E.
Chunk 4E: the power-moment identity for extension families #
Equation (10) instantiated at the exponent test graphs: simple-equivalence at level K
forces every weighted moment of the level-(K+m) test profile over the extension family of
ξ to match that of ξ'. This is the hmom input for the two-family Vandermonde in the
descent step (chunk 4F).
Power-moment identity (eq. (10) at G := expTestGraph k).
Chunk 4F: matching a super-surjective extension of ξ inside the ξ'-family #
Two-family bounded Vandermonde over the extension families: the power-moment identity
(chunk 4E) matches all weighted test-moment powers, so the class-balance engine equates, at
each profile value, the two weighted masses. At the profile of superExt ξ the ξ-side mass
is positive (it contains ρ = coverExtra T, and W > 0), so the ξ'-side class is
nonempty: some extension of ξ' matches ALL test moments of superExt ξ.
The test-moment profile as a Fin-indexed vector (transport along Fintype.equivFin),
for the graph-free Vandermonde engines.
Equations
- Graphon.Lovasz.testProfile B W μ c = Graphon.Lovasz.testMoment B W ((Fintype.equivFin (Graphon.Lovasz.TestCoord K)).symm c) μ
Instances For
Matching extension (the 4F pivot). If ξ ≈ ξ' (equal simple evaluations), some
extension Fin.append ξ' ρ' of ξ' matches superExt ξ on every test moment.
Chunk 4G: the general descent theorem #
The Cai–Govorov descent — the general simple-graph orbit theorem (#70). If all
simple-graph evaluations at ξ and ξ' agree, then ξ' is in the weighted-automorphism
orbit of ξ — with NO surjectivity hypothesis on either tuple. Route: match an extension of
ξ' against the super-surjective superExt ξ on all test moments (chunk 4F), run the
moment-form super-case (chunk 4A) at level K + T·2T², and restrict the resulting
automorphism to the first K labels. This is the statement of
tupleEquivSimple_implies_orbit (Lovasz.lean §3.10; formerly sorry'd at
its non-surjective branch, now proved via this theorem), proved downstream.
Multigraph descent corollaries (relocated 2026-07-02) #
The former §3.7 descent residues and their consumers, relocated below the Cai–Govorov
stack and PROVED via the orbit route: tupleEquivSimple_implies_orbit_general +
multiLabeledEvalK_eq_of_orbit close every case uniformly (the structural multiplicity
hypotheses and the square-moment inputs are no longer needed by the proofs, but the
statements are preserved — with hW/htwin added to the UU-nonisolated case, whose
unhypothesized form was never provable by this route).
Canonical paper-root for #62: every multigraph evaluation is in the simple-profile closure.
Proof outline (Lovász §3 substantive content, ~300-500 LOC):
The space of functions on tupleEquivSimple-classes forms a finite-
dimensional ℝ-algebra. Simple-graph evaluations span this algebra (by
the rank theorem). Multigraph evaluations factor through this algebra
via the connection-matrix idempotent decomposition. The "subgraph
counts" of all multigraphs are polynomial combinations of subgraph
counts of simple graphs.
Status (2026-05-19): #86 is now a clean wrapper over three cases:
n = 0 / mults ≤ 1: dispatched in-line via existing infrastructure (
multiLabeledEvalK_tupleEquiv_invariant_n_zero/ simple-graph correspondence +h_equiv).LL-excess sub-case (every mult≥2 edge is label-label): CLOSED via
multigraphEval_LL_excess_descends_aux(strong induction onM.LLSum; iterated single-edge peel; base case reduces to a simple graph). Polynomial decomposition à la Lovász §3.2 (F₁F₂-product).Unlabeled-excess sub-case (some mult≥2 edge touches an unlabeled vertex): DISPATCHED to the named paper-root
multigraphEval_unlabeled_excess_descends(the final residual Lovász §3 content; ~300-500 LOC of new spectral/rank infrastructure for the multigraph algebra𝒜_K).
Step 1 (of_const_on_tupleEquivSimple, Lagrange fullness) is PROVED.
Historical note (resolved): at the time of writing, the only remaining
sorry was inside multigraphEval_unlabeled_excess_descends; that lemma was
subsequently proved (Cai–Govorov orbit route, 2026-07-02), so this chain is
sorry-free.
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(later in this file; 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.
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):
- Reduction to class-constant
g: it suffices to prove∑_t W(t) g (snoc ξ t) = ∑_t W(t) g (snoc ξ' t)for every class-constantg : (Fin (k+1) → Fin T) → ℝ. Takegto be the indicator of[μ]; this recoverscoeffRestrictSimple_equiv. - Apply
functional_span_zero: on the level-(k+1)quotient bytupleEquivSimple, use the class-weight difference asdand lists ofsimpleEvalAtevaluations as the test family. Constants come from the empty list; multiplicative closure from list concatenation; separation from the definition oftupleEquivSimple; orthogonality fromproduct_trace_identity_simple.
Modulo (historical): this was originally proved modulo the then-named
architectural sorry product_trace_identity_simple (the genuine Lovász §3
content; ~3000 lines via DecLabeledGraph in MatrixDetermination.lean).
That identity has since been proved above, so this theorem is
unconditionally sorry-free.
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 byt = μ (Fin.last k)). - Class constancy (
coeffRestrictSimple_equiv) transfers positivity fromrestrictTuple μ(=ξ) toξ'. - Positivity yields some
awithtupleEquivSimple μ (snoc ξ' a)(exists_extension_of_coeffRestrictSimple_pos); takeν = snoc ξ' a.
Modulo (historical): this was originally proved modulo the then-named
sorry coeffRestrictSimple_equiv (the class constancy step — the IH-free
Lovász §4 core), which has since been proved above; the chain is
sorry-free.
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.
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 φ.
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.
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.
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 (formerly the canonical #
architectural sorry; since PROVED)
Historical note (resolved): the status prose below describes the state
when this section was the project's canonical sorry. The rank theorem and
its contrapositive orbit_separation_by_simple_graph have since been
proved (connection_matrix_rank_theorem; closed 2026-07-02 via the
Cai–Govorov descent).
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 (historical; both items since proved): 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_invariantat 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) was the
canonical primary sorry (since proved); 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 was migrated from
orbit_separation_by_simple_graph to orbitIndicator_mem_simpleGraphSpan
— a cleaner ℝ-linear-algebra statement that captures the same content.
(Both have since been proved; closed 2026-07-02.)
tupleOrbitRel is reflexive.
Witnessed by the identity automorphism.
tupleOrbitRel is symmetric.
If σ realizes ξ' = σ ∘ ξ, then σ.symm realizes ξ = σ.symm ∘ ξ'.
tupleOrbitRel is transitive.
If σ₁ realizes ξ' = σ₁ ∘ ξ and σ₂ realizes ξ'' = σ₂ ∘ ξ', then
σ₂ * σ₁ realizes ξ'' = (σ₂ * σ₁) ∘ ξ.
tupleOrbitRel is an equivalence relation.
Setoid on tuples induced by tupleOrbitRel.
Equations
- Graphon.Lovasz.tupleOrbitSetoid B W K = { r := Graphon.Lovasz.tupleOrbitRel B W, iseqv := ⋯ }
Instances For
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)
Instances For
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
Instances For
Orbit-invariance of orbitIndicator (as a function of the source).
Replacing the source representative ξ by an orbit-related ξ_alt
gives the same indicator function.
orbitIndicator ξ ξ = 1 (reflexivity).
orbitIndicator ξ ξ' = 0 when not orbit-related.
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 (historical directive;
orbit_separation_by_simple_graph has since been proved) — 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.
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)
Instances For
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)
Instances For
§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.
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
Instances For
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
Instances For
Rooted-profile equivalence: two vertices i, j agree on every
rooted simple-graph evaluation.
This is the K=1 specialization of tupleEquivSimple. By Lovász Lemma 2.4
K=1, under twin-free B + W > 0, this equivalence corresponds exactly to
the vertex orbit relation.
Equations
- Graphon.Lovasz.rootedProfileEquiv B W i j = ∀ (n : ℕ) (F : SimpleGraph (Fin (n + 1))) [inst : DecidableRel F.Adj], Graphon.Lovasz.rootedProfile B W i F = Graphon.Lovasz.rootedProfile B W j F
Instances For
Forward direction (trivial): vertex orbit ⟹ rooted-profile equivalence.
Follows from automorphism invariance of simpleEvalAt.
Rooted orbit indicator of vertex i: the function Fin T → ℝ
mapping each vertex v to 1 if v lies in the (B, W)-orbit of i,
and 0 otherwise.
This is the canonical "test function" for the Lovász §3 K=1 rank theorem:
the orbit indicators span the space of (B, W)-automorphism-invariant
functions on Fin T. The K=1 rank theorem asserts that the rooted-profile
functions span this same space, so each orbit indicator lies in the
rooted-profile ℝ-span.
Equations
- Graphon.Lovasz.rootedOrbitIndicator B W i v = if Graphon.Lovasz.vertexOrbitRel B W i v then 1 else 0
Instances For
Rooted-profile function as a function Fin T → ℝ. For a fixed
simple graph F with one labeled position, rootedProfileFun B W F v
is the rooted simple-graph evaluation with the label fixed to v.
Equations
- Graphon.Lovasz.rootedProfileFun B W F v = Graphon.Lovasz.rootedProfile B W v F
Instances For
Algebra of rooted simple-graph profiles (K=1 rank theorem) #
Membership predicate for the rooted-profile ℝ-span: f : Fin T → ℝ
is in the ℝ-span iff it equals a finite linear combination of
rooted-profile functions rootedProfileFun B W F over simple graphs F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The rooted profile of a single graph is in the span (singleton sum).
Zero function is in the span (empty sum).
Closure under addition.
Closure under scalar multiplication.
Constant function 1 is in the rooted-profile span (via the empty graph).
Embedding of F₁'s vertices into the rooted-product graph: identity
on values (so position 0 → root, positions 1..n₁ → F₁'s unlabeled).
Equations
Instances For
Embedding of F₂'s vertices into the rooted-product graph: position 0
maps to the root (shared with F₁'s root); positions 1..n₂ map to
positions n₁ + 1..n₁ + n₂ (F₂'s unlabeled, disjoint from F₁'s).
Equations
Instances For
Equations
- Graphon.Lovasz.rootedProduct F₁ F₂ = SimpleGraph.map (⇑(Graphon.Lovasz.rootedProductEmb₁ n₁ n₂)) F₁ ⊔ SimpleGraph.map (⇑(Graphon.Lovasz.rootedProductEmb₂ n₁ n₂)) F₂
Instances For
Exact-shape application lemmas for the rooted-product embeddings.
These unfold the where-defined toFun directly, so rfl works.
Disjointness helpers between the two embedding images.
rootedProductEmb₁ image vertices have val ≤ n₁.
rootedProductEmb₂ image vertices have val = 0 or val ≥ n₁ + 1.
Image of rootedProductEmb₁ is exactly the vertices with val ≤ n₁.
Image of rootedProductEmb₂ at root (v.val = 0) is the root in big graph.
Image of rootedProductEmb₂ at unlabeled position (v.val ≠ 0) is v.val + n₁.
Multigraph correspondence: the ofSimple of a rooted product equals
the multigraph glue of the individual ofSimple graphs.
Status: PROVED (an earlier revision of this docstring said "structural
sorry ... reverted to clean sorry pending careful one-shot rewrite"; the
rewrite below has since landed). Proof skeleton: refine MultiLabeledGraph.mk.injEq .. |>.mpr ?_,
funext e, induction e with | h a b => simp only [Sym2.lift_mk]; ...
followed by 6 region-case branches using the helpers
map_emb₁_adj_iff, map_emb₂_adj_iff, rootedProductEmb_*_val_*,
rootedProductEmb_*_eq_*_iff (all proved above this declaration).
Cases by (a-region, b-region) where each can be {root, F₁-only, F₂-only}:
- (root, root): both 0 — no edge (loopless on both F₁, F₂).
- (root, F₁): F₁-side only; F₂-side has glueCast₂ b = none.
- (root, F₂): F₂-side only.
- (F₁, *), (F₂, *): symmetric.
- (F₁, F₂) or (F₂, F₁): cross-region — no edge in rooted product.
Closure barrier in the first attempted impl (historical): omega calls
inside Fin.ext-applications needed explicit hypothesis references rather
than ambient context; ~330 LOC were spent before reverting to a clean sorry.
The careful one-shot rewrite subsequently succeeded — see the proof below.
Closure under multiplication via the rooted product.
Build the pair-product family indexed by Fin N₁ × Fin N₂ using
rootedProduct of each pair of graphs and products of coefficients;
apply simpleEvalAt_rootedProduct to factor each rooted profile, then
conclude via Finset.sum_mul_sum. Requires symmetric B for the
factorization through multiLabeledEvalK_glue.
Lagrange interpolation closure (K=1 rank theorem) #
Functions in the rooted-profile span are constant on rooted-profile-
equivalence classes. Trivial consequence of how the equivalence is
defined: at each rootedProfileFun B W F, equivalent vertices agree by
definition of rootedProfileEquiv, and linear combinations preserve this.
Orbit indicators are constant on orbit classes (trivial, since
the indicator value depends only on the orbit of v).
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-07-02): PROVED — the contrapositive of
tupleEquivSimple_implies_orbit_general (the Cai–Govorov descent,
§ CaiGovorovStack above, axiom-clean).
(Historical note: a 2026-05-17 version of this docstring recorded the theorem as BLOCKED on #62 via IH-free Claims 4.3/4.4, with the analysis that the needed diagonal/pointwise data was not extractable from simple-graph evaluations. The Cai–Govorov route bypasses that obstacle entirely — super-surjective extensions make the data extractable.)
Downstream K=1 specialization (rooted_profiles_separate_vertex_orbits,
proved) handles the most-used case; this general-K target remains for
completeness of the Lovász §3 chain.
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.
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 — formerly the canonical sorry, since proved).
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:
- Restrict to level
k(Claim 4.1,tupleEquivSimple_restrict) and apply IH to extract an automorphismσrealizing the orbit relation betweenrestrictTuple ξandrestrictTuple ξ'. - Normalize
ξ'byσ.symmso that the firstkcoordinates agree (usingtupleEquivSimple_of_tupleOrbitRel). - Express both as
Fin.snocof a common baseα := restrictTuple ξover a single last coordinate. - 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 levelT - 1.- Both
αandξnon-surjective: the architectural sorry branch. Lovász's standard plan goes through Claim 4.2 (extend by a fresh elementr ∉ 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 strongNat-induction onsizealone.
Status (2026-07-02): PROVED, sorry-free. The historically-residual
"both α and φ non-surjective" branch is closed by the Cai–Govorov
descent (tupleEquivSimple_implies_orbit_general, § CaiGovorovStack
above), which needs neither surjectivity nor the deficit-1 IH.
(Earlier state, for the record: the branch had been reduced by
deficit-induction to the inner-base sub-case T > k + 1, which
resisted every IH-based plan — see the historical analysis below.)
Architectural obstacle (post-2026-05-12 subagent analysis;
superseded 2026-07-02 — see below): an IH-free
bijective_case_direct / id_bijective_direct would close the
residual but is not derivable from simple-graph evaluations alone
within this induction scheme. NB the Cai–Govorov route
(tupleEquivSimple_implies_orbit_general,
Graphon/CaiGovorovOrbit.lean) PROVES the full theorem from
simple-graph evaluations alone — super-surjective extensions make the
missing diagonal/pointwise data extractable, bypassing the IH-free
Claims entirely. The analysis below documents the obstruction to the
original plan only:
- B-preservation diagonal
B(χ i, χ i) = B(i, i): simple graphs have no self-loops, soB(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.
§3.10.5a — InTupleSimpleEvalSpan predicate and algebra closure #
The K-tuple analog of InRootedProfileSpan. InTupleSimpleEvalSpan B W f
holds when f : (Fin K → Fin T) → ℝ is a finite ℝ-linear combination
of simple-graph evaluations simpleEvalAt B W F.
This is the canonical "column space" of N(K, B, W), used for stating
Lovász Lemma 2.5. The algebra closure properties (const, add, smul,
mul via gluing) are derived here independently of Lemma 2.4 / the
triangular cycle.
Simple-graph evaluation lies in the span (singleton sum).
Closure under addition. Mirrors InRootedProfileSpan.add (K=1):
re-index via Sum to sidestep Fin.addCases motive issues.
Finset sum closure: sums of in-span functions are in-span.
§3.10.5a-multi — InTupleMultiEvalSpan: the multigraph-eval span #
The multigraph analog of InTupleSimpleEvalSpan. Products of evaluations live
naturally here (disjoint glue = multiplication in Lovász's algebra 𝒢_k), so
.mul is a bounded consequence of the PROVED multiLabeledEvalK_glue — no
simpleEvalAt_tupleProduct is possible, because for K ≥ 2 two simple graphs
sharing a label–label edge would force a Hadamard square B(ξ_a,ξ_b)² that no
simple graph can represent (ofSimple caps multiplicity at 1 while glue
adds). The genuinely hard direction — collapsing this span back to the
simple-graph span — is isolated as InTupleMultiEvalSpan.toSimple (Lovász §3 /
Lemma 2.5 content).
Multigraph evaluation lies in the span (singleton sum).
Closure under addition. Mirrors InTupleSimpleEvalSpan.add:
re-index via Sum to sidestep Fin.addCases motive issues.
Finset sum closure: sums of in-span functions are in-span.
Closure under pointwise multiplication — the bounded payoff of the
multigraph route. Mirrors InRootedProfileSpan.mul, but products factor
through the disjoint glue MultiLabeledGraph.glue and the PROVED
multiLabeledEvalK_glue (no ofSimple/tupleProduct detour, no decidability
alignment). Requires symmetric B for multiLabeledEvalK_glue.
Simple-eval span injects into the multigraph-eval span (the easy
bridge direction). Each simpleEvalAt B W F equals
multiLabeledEvalK (ofSimple F) via simpleEvalAt_eq_multi.
Multigraph-span elements are automorphism-invariant — the easy "≤"
direction of the rank theorem (dim V ≤ #orbits): every span element is constant
on (B, W)-orbits. Lifts multiLabeledEvalK_aut_invariant termwise over the span;
needs no symmetry/positivity of B/W. First foothold toward the global
multiEval_separates_orbits (the reverse #orbits ≤ dim V is the hard residue).
Lagrange construction of orbit indicators in the multigraph span #
The K-tuple analog of the K=1 rank theorem InRootedProfileSpan.of_const_on_orbit,
done entirely in the BOUNDED multigraph algebra. The only non-bounded input is an
INDEPENDENT multigraph separator (multiEval_separates_orbits), stated as a residue
that must NOT be derived from simple-graph separation / Lemma 2.4 (that would
recreate the broken cycle).
Finset product closure (needs symmetric B because it uses .mul).
Mirrors InRootedProfileSpan.finset_prod.
multiLabeledEvalK M · - w is in the span. Mirrors profile_sub_const.
A Lagrange factor (eval M · - eval M η) / (eval M ξ - eval M η) is in the
span. Mirrors InRootedProfileSpan.lagrange_factor.
§3.10.5a-multi — tupleEquivMulti class indicators + trace (Lovász Lemma 2.4 spine) #
The cycle-free spine of Lovász Claim 4.2: every tupleEquivMulti-class indicator lies in
InTupleMultiEvalSpan (Lagrange over the finite tuple space, with separators supplied by the
definition of tupleEquivMulti — non-cyclic, unlike orbit separation). Combined with the trace
operator (InTupleMultiEvalSpan.traceLast, below) this yields the extension lemma without the
square-moment hypothesis that makes the simple-graph Claim 4.2 cyclic.
Span elements are constant on tupleEquivMulti classes (span-descending). Every element of
InTupleMultiEvalSpan is a finite ℝ-combination of multiLabeledEvalK, each constant on
tupleEquivMulti classes by definition; hence so is the combination.
From non-equivalence, extract a separating multigraph. Definitional (¬ tupleEquivMulti
literally negates "all evals agree"), hence non-cyclic — does NOT invoke multiEval_separates_orbits.
tupleEquivMulti-class indicator of μ: 1 on μ's equivalence class, 0 elsewhere.
Equations
- Graphon.Lovasz.tupleEquivMultiIndicator B W μ η = if Graphon.Lovasz.tupleEquivMulti B W η μ then 1 else 0
Instances For
tupleEquivMulti-class indicators lie in the multigraph span (Lovász "∑_{η∈Ψ} η ∈ A″").
Lagrange interpolation over the finite tuple space Fin K → Fin T, with each separating multigraph
coming from the definition of tupleEquivMulti (exists_sep_of_not_tupleEquivMulti). NON-CYCLIC:
unlike tupleOrbitIndicator_mem_multiEvalSpan, it never invokes multiEval_separates_orbits.
Trace operator on functions: sum out the last label with W-weight. The function-level
analog of MultiLabeledGraph.trace / Lovász's tr.
Equations
- Graphon.Lovasz.traceLastTupleFun W f ξ = ∑ t : Fin T, W t * f (Fin.snoc ξ t)
Instances For
InTupleMultiEvalSpan is closed under traceLast (Lovász eq. (6): tr(𝒜″_{k+1}) ⊆ 𝒜″_k).
Pushes the trace through the finite combination via multiLabeledEvalK_sum_last_label.
tupleEquivMulti is reflexive.
tupleEquivMulti is symmetric.
Lovász Claim 4.2 (extension), one step — cycle-free multigraph version.
If ξ ξ' are tupleEquivMulti and μ extends ξ (drops to ξ), there is ν extending ξ'
with μ ~ ν. Proof: the traced class indicator of μ is positive at ξ (the t = μ (last) term,
via W (μ last) > 0), hence positive at ξ' (span-descending), so some extension of ξ' lies in
μ's class. NO square-moment hypothesis — that is the cycle-break vs the simple-graph Claim 4.2.
Claim 4.1 (restriction) for tupleEquivMulti — via "add isolated label" (F ⊗ E₁) #
Add an isolated (K+1)-th label (the F ⊗ E₁ operation): reindex M's vertices via
insLabelEmb (skipping index K), so label K is isolated. Evaluation drops the last label.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add-isolated-label evaluation drops the last label: eval (K+1) (addIsoLabel M) ζ = eval K M (ζ ∘ castSucc). The F ⊗ E₁ identity (the new label contributes nothing).
Lovász Claim 4.1 (restriction) for tupleEquivMulti: dropping the last label preserves
equivalence. Direct multigraph proof via addIsoLabel (F ⊗ E₁), NOT through simple equivalence.
Off-diagonal B-preservation (Lovász Claim 4.3, eq. 7). From tupleEquivMulti id χ, a single
label–label edge reads B (χ a) (χ b) = B a b for a ≠ b. (Loopless ⟹ off-diagonal only; the
diagonal B (χ a) (χ a) = B a a is not a single-edge observable.)
Claim 4.1 (restriction along an injection) — generalizes addIsoLabel #
Partial inverse of restrictAlongEmb: none on labels outside range e (the isolated labels).
Equations
Instances For
Push a multigraph along a label injection: embed M's k labels into the l-label space via
e, with labels outside range e isolated.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lovász Claim 4.1 (restriction along an injection) for tupleEquivMulti: precomposing both
tuples with a label injection e preserves equivalence. Direct multigraph proof via restrictAlongGraph.
Weighted power sums determine the weighted value measure. If ∑_t W t · (x t)^k = ∑_t W t · (y t)^k for all k, then for every value a the W-weighted preimage masses agree:
∑_{t : x t = a} W t = ∑_{t : y t = a} W t. (No positivity of W is needed for this form; the
proof is a Lagrange interpolation that turns moment equality into preimage-mass equality.) Moved
here from Graphon/Spectral.lean so the diagonal residue (below) can use it; the Spectral
neighbor-profile lemmas still reference it via open Graphon.Lovasz.
Signed power sums vanish ⟹ every fibre mass vanishes. If a signed weight g on a finite
index has ∑_i g i · (z i)^k = 0 for all k, then for every value a the g-mass of the fibre
{i : z i = a} is 0. (One-function signed analogue of weighted_powersum_determines_measure,
same Lagrange-interpolation proof.)
Level-1 star-moment extraction. Multigraph equivalence of the singleton tuples · ↦ i,
· ↦ j makes all W-weighted neighbor power-sums of rows i, j agree (read off the star probes
starProbe a via multiLabeledEvalK_starProbe).
Level-1 row-value-measure equality. Consequently the W-weighted value measures of rows i
and j agree: for every value v, the total W-mass of {t : B i t = v} equals that of
{t : B j t = v} (via weighted_powersum_determines_measure). NOTE: this level-1 information is
not sufficient on its own to recover the diagonal B i i — see the discussion at
tupleEquivMulti_preserves_diagonal_of_k1. It is the first rung only.
Two-leaf probe (2-labeled, one unlabeled leaf): label 0 joined to the single leaf by a
edges and label 1 joined to it by b edges (no label–label edge). Evaluating it reads the joint
moment ∑ₜ W t · B (φ 0) t ^ a · B (φ 1) t ^ b.
Equations
Instances For
Diagonal observability residue, K = 1 core — PROVED. If the singleton tuples · ↦ i and
· ↦ j are multigraph-equivalent then their diagonal entries agree, B i i = B j j. The general
tupleEquivMulti_preserves_diagonal reduces here per coordinate via tupleEquivMulti_restrict_along.
Proof (loopless, no rank theory): extend_one gives a full K = 2 equivalence (i,i) ≈ (j, b₁).
The single label–label edge (edgeProbe) reads B i i = B j b₁. The two-leaf probe
(twoLeafProbe a b, both labels joined to one unlabeled leaf), together with the level-1 power-sum
equality i ≈ j, gives ∑ₜ W t · (B j t)ᵃ · (B b₁ t)ᵇ = ∑ₜ W t · (B j t)ᵃ · (B j t)ᵇ for all
a, b; two Lagrange fibre arguments (weighted_powersum_zero_imp_fiber_zero,
weighted_powersum_determines_measure) force the rows equal, B b₁ = B j, so twin-freeness gives
b₁ = j, hence B i i = B j j.
Diagonal observability residue (Route A, the single named hard input for #62/#73).
The remaining honest content of Lovász §3 for the loopless multigraph framework: rooted multigraph
hom-counts determine the diagonal B (ξ c) (ξ c). This is the genuine diagonal-observability
input and is NOT implied by closed walks / single-vertex moments alone (loopless evals see the
diagonal only in aggregate, via the weighted multiset {B(ξc,t)}_t; isolating B(ξc,ξc) pointwise
needs W-preservation + bijectivity, which in turn need the diagonal — the reconstruction circle).
It is therefore distinct from the false closed-walk conjecture and must NOT be conflated with it.
Everything else in the multigraph Lemma 2.4 chain (Lemma 4.1, Claims 4.2–4.4, weight preservation,
assembly) and the Spectral cascade are proved honestly conditional on this one statement. General K
is exactly the per-coordinate K=1 content (reducible via a label embedding).
Full B-preservation for the bijective case = off-diagonal (proved) + diagonal (residue).
Lovász Lemma 4.1 (bijectivity) for tupleEquivMulti. A B-preserving endofunction of a
twin-free graph is bijective. With FULL B-preservation in hand (off-diagonal + diagonal residue),
this is immediate: if χ a = χ b then B a l = B (χ a)(χ l) = B (χ b)(χ l) = B b l for every l,
so rows a and b coincide — contradicting twin-free unless a = b. Injective + finite ⟹ bijective.
(No idempotent-power argument needed; the diagonal residue subsumes it.)
Relabel-invariance for tupleEquivMulti (label permutations) #
Lift a label permutation ρ : Perm (Fin K) to a permutation of the vertex space Fin (n+K),
acting by ρ on the labels (indices < K) and fixing the unlabeled vertices.
Equations
- One or more equations did not get rendered due to their size.
Instances For
multiTau intertwines liftLabelPerm with label-precomposition: tracing the relabeled vertex
under ζ equals tracing under ζ ∘ ρ.
Relabel a multigraph's labels by ρ (via liftLabelPerm ρ⁻¹ on the vertex space).
Equations
- Graphon.Lovasz.MultiLabeledGraph.relabel ρ M = { mult := fun (e : Sym2 (Fin (n + K))) => M.mult (Sym2.map (⇑(Equiv.symm (Graphon.Lovasz.liftLabelPerm ρ))) e), multNoLoop := ⋯ }
Instances For
Relabel-invariance: tupleEquivMulti is closed under precomposing both tuples with a label
permutation ρ. (Used to move any coordinate to the last position for the trace weight argument.)
Commit B.2 — weight preservation via trace-collapse #
Snoc injectivity (isolated): if ζ is bijective and Fin.snoc (ζ ∘ castSucc) t is bijective,
then t = ζ (last) (the only value completing the restriction to a bijection).
Equivalence transfers bijectivity: if η ~ ξ and ξ is bijective, so is η. Proof: relabel
both sides by ξ⁻¹ so the RHS becomes id, then apply tupleEquivMulti_id_bijective.
Trace-collapse: for a bijective tuple ζ in ξ's class, the traced class indicator at the
restriction reads exactly W (ζ last). Only t = ζ (last) keeps snoc (ζ ∘ castSucc) t bijective —
hence in ξ's class (every member is bijective, tupleEquivMulti_bijective_of_equiv).
Last-coordinate W preservation (Lovász Claim 4.3 weight step). For equivalent bijective
tuples, the trace of ξ's class indicator is class-constant (span-descending) and collapses to the
last-coordinate weight on each side, giving W (ξ' last) = W (ξ last).
W preservation for the bijective case (all coordinates): for any coordinate i, relabel to
move i to the last position and apply tupleEquivMulti_bijective_preserves_W_last.
Lovász Claim 4.3 (bijective case): tupleEquivMulti id χ ⟹ tupleOrbitRel id χ. With full
B-preservation (off-diag + diagonal residue) and W-preservation in hand, χ is a weighted
automorphism, so it witnesses the orbit relation.
Lovász Claim 4.4 (surjective case): a surjective tuple equivalent to ξ' is orbit-related.
Choose a section s of ξ; restrict_along s gives id ~ ξ' ∘ s, so the bijective case yields an
automorphism σ with ξ'(s r) = σ r. For arbitrary j with ξ j = r, the replacement injection
ej (which sends r ↦ j and t ↦ s t otherwise) has ξ ∘ ej = id, so ξ' ∘ ej is bijective; this
forces ξ' j = σ r = σ (ξ j).
Lovász Lemma 2.4 (multigraph form): equal rooted multigraph hom-counts imply same
Aut(B,W)-orbit. Induct on the number of missed vertices |univ \ range ξ|: if ξ is surjective,
apply Claim 4.4; otherwise append a missing vertex v (Claim 4.2 lifts ξ' to ν), recurse on the
strictly-larger range, and restrict the resulting automorphism back to the original coordinates.
Independent multigraph separator (Lovász §3). For distinct orbits there is a multigraph whose evaluation distinguishes the tuples.
PROVED, sorry-free: a direct corollary of tupleEquivMulti_implies_orbit
(the honest multigraph Lemma 2.4), independent of
orbit_separation_by_simple_graph / the simple-graph Lemma 2.4 — so no cycle
with the Lemma 2.5 chain. (An earlier docstring here described this as a
sorry'd §3 residue; that is stale — the residue was discharged when the
multigraph Lemma 2.4 chain landed.)
Orbit indicators lie in the multigraph span (Phase B Target 1).
Lagrange interpolation over orbit classes, built in the bounded multigraph
algebra (.finset_prod, .lagrange_factor, .mul, .const, .smul). Orbit
invariance of multiLabeledEvalK makes each factor 1 on the source orbit and 0
on the indexing tuple's class. The ONLY non-bounded input is the independent
separator multiEval_separates_orbits.
P1 scaffolding — enriched evaluators (EXPLORATORY / OFF CRITICAL PATH) #
⚠ Not a reduction. This was built toward multiEval_separates_orbits via a
Lovász hom→injective inclusion–exclusion, on the worry that the enriched
W^{|block|} / diagonal moments were not controlled by plain multiLabeledEvalK
hom counts. A numerical viability gate (scripts/w2_moment_control_gate.py)
refuted that worry: the simplest enriched moment ∑_t W_t² B(i,t) is always in
the plain-eval span V (V is closed under products via multiLabeledEvalK_glue,
which generate the W-powers). Decisively, since that moment is orbit-invariant and
V is a unital subalgebra, w2 ∈ V ⟺ dim V = #orbits ⟺ separation — so controlling
the enriched moments is equivalent to proving multiEval_separates_orbits itself.
There is no inclusion–exclusion shortcut; this enriched machinery does not reduce
the work and is retained only as exploratory infrastructure (it has no critical-path
consumers). The genuine remaining content is the global weighted-hom-determines-
isomorphism / connection-rank theorem. See
~/.claude/plans/multiEval-separates-orbits-scoping.md (GATE RESULT section).
SCAFFOLDING (no endpoint automorphism extraction). The enriched evaluator
wexpMultiLabeledEvalKLoop supports per-vertex W-exponents + self-loops; the
injective-restricted injMultiLabeledEvalK and the split lemma are the IE base.
The per-σ summand of multiLabeledEvalK, factored out so the injective and
non-injective restrictions share one body.
Equations
- One or more equations did not get rendered due to their size.
Instances For
multiLabeledEvalK as the Finset.univ sum of multiLabeledTerm.
Injective-restricted multigraph evaluation: sum the multiLabeledTerm
only over injective unlabeled assignments σ. The first enriched object for the
inclusion–exclusion route (injective σ uses each color once, so no W-powers
arise in its own definition).
Equations
- Graphon.Lovasz.injMultiLabeledEvalK K n M B W φ = ∑ σ : Fin n → Fin T with Function.Injective σ, Graphon.Lovasz.multiLabeledTerm K n M B W φ σ
Instances For
Enriched (vertex-weighted, self-looped) evaluator. Generalizes
multiLabeledEvalKLoop with a per-unlabeled-vertex weight exponent wexp
(so a vertex contributes W(σ v) ^ wexp v) and runs over a MultiLabeledGraphLoop
(self-loops B(c,c)^k allowed). This is the family the Möbius partition-constrained
terms T_P live in: a size-s merged block carries wexp = s and intra-block
edges become self-loops.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Sanity: the enriched evaluator with all exponents 1 recovers
multiLabeledEvalKLoop.
Enriched equivalence: equality of all injective-restricted evaluations. The controlled relation the inclusion–exclusion endpoint would consume.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Inclusion–exclusion foothold: a hom count splits as its injective part plus its non-injective part. The base of the Möbius reduction.
Status note (do not delete) — resolved by the W² gate. The natural next
step would be the full Möbius reduction
injMultiLabeledEvalK = ∑_P μ(⊥,P) · (constrained sum at P), each constrained
sum reindexing to a wexpMultiLabeledEvalKLoop over the quotient (block-size
exponents + self-loops). But this route is not a reduction: the viability gate
scripts/w2_moment_control_gate.py showed the enriched moments (e.g.
∑_t W_t² B(i,t)) ARE controlled by plain multiLabeledEvalK hom counts — they
lie in the product-closed span V — and since they are orbit-invariant and V is
a unital subalgebra, controlling them is equivalent to dim V = #orbits, i.e. to
multiEval_separates_orbits itself. So tupleEquivMulti ⟹ tupleEquivMultiInj
holds but is no easier than the goal. The genuine remaining content is the global
weighted-hom-determines-isomorphism / connection-rank theorem. This scaffolding has
no critical-path consumers (the residues stay multiEval_separates_orbits and
InTupleMultiEvalSpan.toSimple).
Simple-graph evaluations are automorphism-invariant.
For any (B, W)-aut σ and simple graph F, simpleEvalAt B W F (σ ∘ ξ) = simpleEvalAt B W F ξ. Reduces to multiLabeledEvalK_eq_of_orbit
via simpleEvalAt_eq_multi.
The #70 rank theorem: eval spans as Submodules + the finrank collapse #
Moved here from CycleKrylov.lean (submodule packaging, Phase A/B) and the dissolved
SimpleOrbitRank.lean (Phase C1+D + the annihilator argument), 2026-07-02. Sits directly
after simpleEvalAt_aut_invariant and the Cai–Govorov stack — everything it needs.
Eval spans as Submodules (Phase A — foundation for the §3 rank/finrank work) #
The K-tuple simple- and multigraph-eval spans, currently bare existential predicates
(InTupleSimpleEvalSpan / InTupleMultiEvalSpan in Lovasz.lean), are repackaged here
as honest Submodule ℝs. This unlocks finrank/Basis/≤ for the rank argument that
isolates the sole #70 residue InTupleMultiEvalSpan.toSimple. The membership-iffs tie
the new submodules back to the existing predicate API, which stays the interface for
construction.
The K-tuple simple-eval span as a submodule: spanned by the simple-graph
evaluation functions ξ ↦ simpleEvalAt B W F ξ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The K-tuple multigraph-eval span as a submodule: spanned by the multigraph
evaluation functions ξ ↦ multiLabeledEvalK K n M B W ξ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Orbit-invariant submodule and multiEvalSubmodule = orbitInvariant (Phase B) #
The genuinely informative half of the rank framework, and non-circular: the
multigraph-eval submodule equals the submodule of automorphism-invariant functions. The
≥ direction rests on the directly-proved (toSimple-free) tupleOrbitIndicator_mem_multiEvalSpan.
This pins the sole #70 residue to exactly simpleEvalSubmodule = orbitInvariantSubmodule.
Automorphism-invariant ⟹ multigraph-eval span (the multi analog of
tupleSimpleEval_span_aut_invariant, but NON-circular — it consumes the directly-proved
tupleOrbitIndicator_mem_multiEvalSpan, never InTupleMultiEvalSpan.toSimple). Orbit
indicators are a basis of the invariant functions, and each lies in the multi span.
≥: every automorphism-invariant function lies in the multigraph-eval span
(non-circular, via tupleMultiEval_span_aut_invariant).
The multigraph-eval submodule is exactly the automorphism-invariant submodule.
The clean, non-circular pillar of the §3 rank framework: the residue is now precisely
simpleEvalSubmodule = orbitInvariantSubmodule.
Easy inclusion simpleEvalSubmodule ≤ orbitInvariantSubmodule: simple-graph
evaluations are automorphism-invariant (simpleEvalAt_aut_invariant). Completes the
clean frame simpleEvalSubmodule ≤ orbitInvariantSubmodule = multiEvalSubmodule; the
sole #70 residue is the reverse inclusion.
Corollary simpleEvalSubmodule ≤ multiEvalSubmodule (the never-in-doubt
inclusion), directly via InTupleSimpleEvalSpan.toMulti.
Equations
Evaluation-at-orbit-representatives, as a linear map from the orbit-invariant functions to functions on the orbit quotient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Phase C1: finrank orbitInvariantSubmodule = #OrbitClass.
The annihilator lemma (chunk 5B) #
Any c : OrbitClass → ℝ that annihilates every simple evaluation at orbit representatives is
zero. This is STRICTLY stronger than point-separation of the orbit classes (distinct rows can
still be linearly dependent); the signed single-family Vandermonde over
OrbitClass × (Fin m → Fin T) does the real work, powered by the Cai–Govorov descent
ingredients (sum_extensions_eval, expTestGraph, testEvalEq_implies_orbit_super).
The annihilator lemma. If ∑ q, c q · simpleEvalAt F (out q) = 0 for every simple
graph F, then c = 0. Signed Vandermonde over OrbitClass × (Fin m → Fin T) with the
test-moment profile of Fin.append (out q) ρ as classifier: the class of the profile of
superExt (out q₀) consists exactly of pairs (q₀, ρ) (chunk 4A at level K + m forces
q = q₀), and its W-mass is positive, so the class-sum c q₀ · (positive) = 0 kills
c q₀.
The dual-pairing endgame (chunk 5C) #
The representative pairing turns the annihilator lemma into injectivity of a map into the
dual of simpleEvalSubmodule; comparing dimensions gives the lower bound. Transcribes the
hle1 half of connectionMatrix_full_rank_of_orthogonal (Spectral.lean).
The simple-side lower bound (the genuine Lovász §3 content, formerly the sole #70
residue): the simple-eval span has dimension at least the number of orbit classes. The
composite Ψ := subtype.dualMap ∘ evalRepPairing is injective by the annihilator lemma, so
#OrbitClass = finrank (OrbitClass → ℝ) ≤ finrank (Dual simpleEvalSubmodule) = finrank simpleEvalSubmodule.
Phase D: the rank collapse — the simple-eval and orbit-invariant submodules coincide
(unconditional: the lower bound simpleEvalSubmodule_finrank_ge_orbitClass is proved above).
This is the #70 rank theorem.
Corollaries of the rank collapse: the former §3 residues #
Multigraph algebra collapses to the simple-graph algebra (Lovász Lemma 2.5 content).
Under twin-free B and positive W, every multigraph-eval span element is also a
simple-eval span element. Formerly the Hadamard-square residue; now a direct corollary of
the rank collapse: multigraph evals are automorphism-invariant, and orbit-invariant
functions lie in the simple-eval span.
Closure under pointwise multiplication for the simple-graph span (with the twin-free
and positivity hypotheses its earlier docstring recorded as necessary — without them the
statement is false; the label–label Hadamard square obstructs any bounded proof). Routes
through the multigraph algebra: .toMulti, bounded .mul via glue, and the rank-collapse
.toSimple.
§3.10.5 — Lovász Lemma 2.5 (column-space rank theorem) #
Lovász Lemma 2.5 (paper page 6): Let G be a twin-free weighted
graph. The column space of N(k, G) consists of precisely those
functions f : V(G)^k → ℝ invariant under automorphisms of G.
In our notation: f : (Fin K → Fin T) → ℝ is in the span of
{simpleEvalAt B W F : F : SimpleGraph (Fin (n + K))} iff f is
(B, W)-automorphism-invariant on tuples.
Status: orbit-basis decomposition step PROVED. Substance reduces
to tupleOrbitIndicator_mem_simpleEvalSpan (the orbit indicators are
in the simple-eval span — Lovász §3 idempotent construction).
Downstream consequence: closes Lemma 2.4 in full (including the
"both non-surj" branch) via the orbit-indicator argument
(tupleEquivSimple_implies_orbit_via_2_5 below).
Orbit indicators are aut-invariant (easy direction).
For any (B, W)-aut τ, orbitIndicator B W ξ (τ ∘ η) = orbitIndicator B W ξ η because the orbit of ξ is closed under aut composition:
ξ _orbit (τ ∘ η) iff ξ _orbit η (transitivity via τ ∈ aut).
Orbit indicators are in the simple-eval span — now a thin wrapper (sorry-free), no longer the paper-root.
Derived through the multigraph route: orbit indicators lie in the multigraph
span (tupleOrbitIndicator_mem_multiEvalSpan), and the multigraph span collapses
to the simple-eval span (InTupleMultiEvalSpan.toSimple). The genuine Lovász §3
content thus lives entirely in the two honest, non-cyclic residues
multiEval_separates_orbits (orbit separation) and InTupleMultiEvalSpan.toSimple
(Hadamard-square collapse) — neither routes through Lemma 2.4.
Orbit indicators lie in the ℝ-span of simple-graph evaluations (Lovász §3 fullness,
list form). List repackaging of tupleOrbitIndicator_mem_simpleEvalSpan — the
representation uses pairs (c, ⟨n, ⟨F, dec⟩⟩) of a coefficient and a decidably-adjacent
simple labeled graph.
Lemma 2.4 via Lemma 2.5 (the column-space derivation).
Given tupleEquivSimple ξ ξ' (rows of N agree at ξ, ξ'), if ξ and ξ'
were NOT orbit-related, the orbit indicator of [ξ] would distinguish
them. But the orbit indicator is aut-invariant, hence in column span
(by Lemma 2.5), hence its values at ξ and ξ' agree (by row equality).
Contradiction.
§3.10 — label_unlabeled_square_moment_descends via Route 2 #
The K=1 square moment identity is the final paper-root of the unlabeled-excess branch of #86 (the multigraph bridge). Its proof combines:
- Orbit-invariance of
sqMoment i := ∑ t, W t · B i t ^ 2. Direct fromIsWeightedAutomorphismviaEquiv.sum_comp. - Rooted-profile span representation via
InRootedProfileSpan.of_const_on_orbit(the K=1 rank theorem). - K → K=1 reduction: given
tupleEquivSimple ξ ξ'at K-level anda : Fin K, deriverootedProfile B W (ξ a) F = rootedProfile B W (ξ' a) Ffor every simpleF : SimpleGraph (Fin (n+1)). Built via aFin (n+1) ↪ Fin (n+K)embedding that routes the K=1 label to coordinateaand stations the unlabeled vertices at positionsK..K+n-1.
Together: orbit-invariance + rooted-profile span + K→K=1 reduction
collapse the square moment at ξ a and ξ' a to a finite linear
combination of rooted profiles, each of which is preserved by
tupleEquivSimple.
FINAL PAPER-ROOT — K=1 square moment identity, PROVED via Route 2 (rooted-profile span + orbit invariance + K→K=1 reduction).
This is the genuine Lovász §3 bottleneck. Closes the unlabeled-excess branch of #86 (multigraph bridge).
K=1 rank theorem consequences (orbit indicators, Lemma 2.4) #
Rank-theorem target (K=1, span form), now DERIVED from
InRootedProfileSpan.of_const_on_orbit.
The orbit indicator of any vertex lies in the ℝ-span of rooted simple-graph profile functions. Proved by combining:
rootedOrbitIndicator_const_on_orbit: the indicator is orbit-invariant.InRootedProfileSpan.of_const_on_orbit: orbit-invariant functions are in the span (the K=1 rank-theorem paper-root).
Backward direction (Lovász §3 K=1 rank theorem): rooted-profile
equivalence ⟹ vertex orbit, under twin-free B + W > 0.
Proof: derived from rootedOrbitIndicator_mem_rootedProfileSpan by
evaluating the indicator at both i and j. Rooted-profile equivalence
forces the linear combination to agree at both, and reflexivity gives
indicator_i(i) = 1, hence indicator_i(j) = 1, hence vertex orbit.
K=1 Lovász Lemma 2.4 (iff form). Combines the forward direction (orbit ⟹ equiv, free) with the backward direction (equiv ⟹ orbit, the rank-theorem paper-root).
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
Instances For
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✝)
Instances For
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
Instances For
§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:
- Bridge: closed walks ↔ diagonal moments of S^m.
- Cayley-Hamilton: equality at m = 0..T-1 suffices.
- Spectral decomposition: S = ∑ λ_k u_k u_k^T (mathlib's
Matrix.IsSymm.eigenvectorBasis). - 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.
Removed refuted conjecture: vertex_orbit_of_closed_walks_eq #
Deleted as a sorry stub (2026-07-10, issue #19); the refutation documentation is
retained below, and the former statement is quoted for the record. Do NOT reintroduce.
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 statement was retained for a time as a
sorrystub for architectural documentation and has now been removed (this block preserves the record); it must 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.
Former statement (removed):
theorem vertex_orbit_of_closed_walks_eq {T : ℕ}
(_B : Fin T → Fin T → ℝ) (_hB : ∀ i j, _B i j = _B j i)
(_W : Fin T → ℝ) (_hW : ∀ i, 0 < _W i)
(_htwin : ∀ i j, 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 := ...
Removed refuted conjecture: closed_walk_profiles_separate_vertex_orbits #
Deleted as a sorry stub (2026-07-10, issue #19); the refutation documentation is
retained below, and the former statement is quoted for the record. Do NOT reintroduce.
#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. It was retained for a time as a sorry'd statement to document the counterexample and has now been removed (this block preserves the record).
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.
Former statement (removed):
theorem closed_walk_profiles_separate_vertex_orbits {T : ℕ}
(_B : Fin T → Fin T → ℝ) (_hB : ∀ i j, _B i j = _B j i) (_W : Fin T → ℝ)
(_hW : ∀ i, 0 < _W i)
(_htwin : ∀ i j, 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) := ...
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
Instances For
Loopless property unfolding.
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.
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).
The edge finset of rootedCycleGraph (m+1) is exactly the image of
the map j ↦ s(j, cycleSucc j) over Fin (m + 3).
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.
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 (2026-06-10): FULLY PROVED, axiom-clean (an earlier revision of
this docstring incorrectly said "focused infrastructure sorry"). This bridge
is the graph-plumbing half of the cycle–Krylov proof of
sqMoment_descends_of_rootedProfileEquiv (Graphon/CycleKrylov.lean).
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: PROVED, via rootedProfileEquiv_imp_vertexOrbitRel — the FULL rooted
simple-graph family (paths, trees, asymmetric shapes), i.e. the Lovász §3 rank
theorem content.
Historical note: an earlier 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 refuted
closed-walk conjectures were removed (issue #19).
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.
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:
tupleEquivSimpleat K=1 ⟹ all rooted profiles agree at (ξ 0, ξ' 0).- Contrapositive of
rooted_profiles_separate_vertex_orbits(PROVED viarootedProfileEquiv_imp_vertexOrbitRel) ⟹vertexOrbitRel B W (ξ 0) (ξ' 0). - Vertex orbit relation gives
σautomorphism withσ (ξ 0) = ξ' 0. B(ξ 0, ξ 0) = B(σ (ξ 0), σ (ξ 0)) = B(ξ' 0, ξ' 0)by aut B-preservation.
Status: PROVED (the separation input comes from the rank-theorem route; the historical #77 closed-walk paper-root was refuted and removed).
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 — the separation input comes from
diagonal_observable_K1, whose rooted_profiles_separate_vertex_orbits
input is proved via rootedProfileEquiv_imp_vertexOrbitRel (the
rank-theorem route). This replaces the earlier sorry-stub
diagonal_observable_of_tupleEquivSimple that was a placeholder pending
the rank-theorem path.
Historical note: earlier revisions of this docstring said "proved
modulo #77 (the K=1 spectral paper-root)" and that consumers "inherit
dependency on #77"; the #77 closed-walk route was refuted and removed
(issue #19), and the theorem is now unconditionally proved via the
rank-theorem route. Consumers (e.g., the n=0 loop bridge
multiLabeledEvalKLoop_n_zero_of_diag) inherit no open dependency.
§4 — The bridge theorem (formerly the canonical sorry; since PROVED #
— see multiLabeledEvalK_tupleEquiv_invariant above)
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.
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 case of the general bridge (sorry'd when this
was written; since proved). 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.