Documentation

Graphon.Lovasz

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 sorry tokens repository-wide): the §4 bridge multiLabeledEvalK_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 in MatrixDetermination.lean is likewise proved. Also, the module now imports Graphon.CaiGovorov, so the "self-contained, no Graphon.* 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 MultiLabeledGraphGraphon.Lovasz.MultiLabeledGraph adapter, since the types live in different namespaces).

Module structure (planned) #

§1 — Multigraph carrier (DECLARED below) #

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

§3 — Trace operator and quotient — STUBS #

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

References #

§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:

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

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

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

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

Instances For

    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).

      Equations
      Instances For
        noncomputable def Graphon.Lovasz.multiLabeledEvalK {T : } (K n : ) (M : MultiLabeledGraph K n) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :

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

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable def Graphon.Lovasz.multiLabeledEvalKLoop {T : } (K n : ) (M : MultiLabeledGraphLoop K n) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :

          Multigraph evaluation with self-loops.

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

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Graphon.Lovasz.multiLabeledEvalKLoop_of_toLoop {T K n : } (M : MultiLabeledGraph K n) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :

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

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

            Automorphism invariance of multiLabeledEvalKLoop.

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

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

            Orbit invariance of multiLabeledEvalKLoop (corollary).

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

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

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

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

            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
              theorem Graphon.Lovasz.multiLabeledEvalK_ofSimple {T K n : } (F : SimpleGraph (Fin (n + K))) [DecidableRel F.Adj] (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :
              multiLabeledEvalK K n (MultiLabeledGraph.ofSimple F) B W φ = σ : Fin nFin T, have τ := fun (v : Fin (n + K)) => if h : v < K then φ v, h else σ v - K, ; (∏ v : Fin n, W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)

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

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

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

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

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

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

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

              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
                  theorem Graphon.Lovasz.multiLabeledEvalK_perSym2_add {T K n : } (B : Fin TFin T) (M₁ M₂ : MultiLabeledGraph K n) (τ : Fin (n + K)Fin T) :
                  e : Sym2 (Fin (n + K)), B (τ (Quot.out e).1) (τ (Quot.out e).2) ^ (M₁.add M₂).mult e = (∏ e : Sym2 (Fin (n + K)), B (τ (Quot.out e).1) (τ (Quot.out e).2) ^ M₁.mult e) * e : Sym2 (Fin (n + K)), B (τ (Quot.out e).1) (τ (Quot.out e).2) ^ M₂.mult e

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

                  theorem Graphon.Lovasz.multiLabeledEvalK_empty {T K n : } (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :
                  multiLabeledEvalK K n (MultiLabeledGraph.empty K n) B W φ = σ : Fin nFin T, v : Fin n, W (σ v)

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

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

                  Same-vertex add factorization (general n).

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

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

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

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

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

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

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

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

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

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

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

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem Graphon.Lovasz.MultiLabeledGraph.glue_mult_pair {K n₁ n₂ : } (M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (a b : Fin (n₁ + n₂ + K)) :
                        (M₁.glue M₂).mult s(a, b) = (match glueCast₁ K n₁ n₂ a, glueCast₁ K n₁ n₂ b with | some u', some v' => M₁.mult s(u', v') | x, x_1 => 0) + match glueCast₂ K n₁ n₂ a, glueCast₂ K n₁ n₂ b with | some u', some v' => M₂.mult s(u', v') | x, x_1 => 0

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

                        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
                          @[simp]
                          theorem Graphon.Lovasz.starProbe_mult {a : } (e : Sym2 (Fin (1 + 1))) :
                          (starProbe a).mult e = if e = s(0, 1) then a else 0
                          theorem Graphon.Lovasz.multiLabeledEvalK_starProbe {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (i : Fin T) (a : ) :
                          (multiLabeledEvalK 1 1 (starProbe a) B W fun (x : Fin 1) => i) = t : Fin T, W t * B i t ^ a

                          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.

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

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

                          Equations
                          Instances For
                            def Graphon.Lovasz.glueEmb₂ (K n₁ n₂ : ) :
                            Fin (n₂ + K) Fin (n₁ + n₂ + K)

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

                            Equations
                            Instances For
                              @[simp]
                              theorem Graphon.Lovasz.glueCast₁_glueEmb₁ (K n₁ n₂ : ) (v : Fin (n₁ + K)) :
                              glueCast₁ K n₁ n₂ ((glueEmb₁ K n₁ n₂) v) = some v

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

                              @[simp]
                              theorem Graphon.Lovasz.glueCast₂_glueEmb₂ (K n₁ n₂ : ) (v : Fin (n₂ + K)) :
                              glueCast₂ K n₁ n₂ ((glueEmb₂ K n₁ n₂) v) = some v

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

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

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

                              theorem Graphon.Lovasz.glueCast₂_of_val_ge (K n₁ n₂ : ) (v : Fin (n₁ + n₂ + K)) (h : v n₁ + K) :
                              glueCast₂ K n₁ n₂ v = some v - n₁,

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

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

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

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

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

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

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

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

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def Graphon.Lovasz.gluePart₂ {K n₁ n₂ : } (_M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (e : Sym2 (Fin (n₁ + n₂ + K))) :

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

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem Graphon.Lovasz.MultiLabeledGraph.glue_mult_eq_add {K n₁ n₂ : } (M₁ : MultiLabeledGraph K n₁) (M₂ : MultiLabeledGraph K n₂) (e : Sym2 (Fin (n₁ + n₂ + K))) :
                                  (M₁.glue M₂).mult e = gluePart₁ M₁ M₂ e + gluePart₂ M₁ M₂ e

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

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

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

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

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

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

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

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

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

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

                                  Disjoint glue factorization of multigraph evaluations.

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

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

                                  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.

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

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

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

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

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

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

                                      §3.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 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).

                                      def Graphon.Lovasz.multiTau {T : } (K n : ) (φ : Fin KFin T) (σ : Fin nFin T) :
                                      Fin (n + K)Fin 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).

                                      Equations
                                      Instances For
                                        theorem Graphon.Lovasz.multiLabeledEvalK_eq_tau {T K n : } (M : MultiLabeledGraph K n) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :
                                        multiLabeledEvalK K n M B W φ = σ : Fin nFin T, (∏ v : Fin n, W (σ v)) * e : Sym2 (Fin (n + K)), B (multiTau K n φ σ (Quot.out e).1) (multiTau K n φ σ (Quot.out e).2) ^ M.mult e

                                        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
                                          @[simp]
                                          theorem Graphon.Lovasz.edgeProbe_mult {a : } (e : Sym2 (Fin (0 + 2))) :
                                          (edgeProbe a).mult e = if e = s(0, 1) then a else 0
                                          theorem Graphon.Lovasz.multiLabeledEvalK_edgeProbe {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (φ : Fin 2Fin T) (a : ) :
                                          multiLabeledEvalK 2 0 (edgeProbe a) B W φ = B (φ 0) (φ 1) ^ a

                                          Edge-probe evaluation: reads B (φ 0) (φ 1) ^ a.

                                          def Graphon.Lovasz.rerootCast {m : } (v : Fin (m + 2)) :
                                          Option (Fin (m + 1))

                                          Partial inverse of Fin.succ on Fin (m + 2): index 0none, k+1some k. Used to define reroot1's multiplicity.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem Graphon.Lovasz.rerootCast_succ {m : } (w : Fin (m + 1)) :
                                            theorem Graphon.Lovasz.rerootCast_eq_some {m : } {v : Fin (m + 2)} {u : Fin (m + 1)} (h : rerootCast v = some u) :
                                            v = u.succ
                                            def Graphon.Lovasz.succEmb (m : ) :
                                            Fin (m + 1) Fin (m + 2)

                                            Fin.succ as an embedding Fin (m + 1) ↪ Fin (m + 2).

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem Graphon.Lovasz.succEmb_apply {m : } (w : Fin (m + 1)) :
                                              (succEmb m) w = w.succ

                                              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
                                                @[simp]
                                                theorem Graphon.Lovasz.reroot1_mult_map_succ {m : } ( : MultiLabeledGraph 1 m) (e' : Sym2 (Fin (m + 1))) :
                                                (reroot1 ).mult (Sym2.map (⇑(succEmb m)) e') = .mult e'
                                                theorem Graphon.Lovasz.multiLabeledEvalK_reroot1 {T m : } ( : MultiLabeledGraph 1 m) (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (φ : Fin 2Fin T) :
                                                multiLabeledEvalK 2 m (reroot1 ) B W φ = multiLabeledEvalK 1 m B W fun (x : Fin 1) => φ 1

                                                Reroot evaluation: reroot1 evaluated at φ reads 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 (its old root now the leaf label 1) to the root–leaf edgeProbe a (labels 01), 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
                                                  theorem Graphon.Lovasz.multiLabeledEvalK_decoratedProbe {T m : } (a : ) ( : MultiLabeledGraph 1 m) (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (i : Fin T) :
                                                  (multiLabeledEvalK 1 (m + 1) (decoratedProbe a ) B W fun (x : Fin 1) => i) = t : Fin T, W t * B i t ^ a * multiLabeledEvalK 1 m B W fun (x : Fin 1) => t

                                                  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.

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

                                                  Automorphism invariance of multiLabeledEvalK.

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

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

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

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

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

                                                  §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).

                                                  inductive Graphon.Lovasz.InSimpleProfileClosure {T : } (B : Fin TFin T) (W : Fin T) (K : ) :
                                                  ((Fin KFin T))Prop

                                                  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.

                                                  Instances For
                                                    theorem Graphon.Lovasz.InSimpleProfileClosure.descends {T K : } {B : Fin TFin T} {W : Fin T} {f : (Fin KFin T)} (hf : InSimpleProfileClosure B W K f) {ξ ξ' : Fin KFin T} (h : ∀ (n' : ) (F : SimpleGraph (Fin (n' + K))) [inst : DecidableRel F.Adj], (∑ σ : Fin n'Fin T, have τ := fun (v : Fin (n' + K)) => if h : v < K then ξ v, h else σ v - K, ; (∏ v : Fin n', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) = σ : Fin n'Fin T, have τ := fun (v : Fin (n' + K)) => if h : v < K then ξ' v, h else σ v - K, ; (∏ v : Fin n', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) :
                                                    f ξ = f ξ'

                                                    Closure functions descend to h_simple-equivalent tuples. Takes the inlined tupleEquivSimple-form hypothesis (matching #62's h_simple).

                                                    theorem Graphon.Lovasz.InSimpleProfileClosure.zero {T : } (B : Fin TFin T) (W : Fin T) (K : ) :
                                                    InSimpleProfileClosure B W K fun (x : Fin KFin T) => 0

                                                    Zero is in the closure (empty Finset.sum gives 0; or smul 0 any member).

                                                    theorem Graphon.Lovasz.InSimpleProfileClosure.sub {T K : } {B : Fin TFin T} {W : Fin T} {f g : (Fin KFin T)} (hf : InSimpleProfileClosure B W K f) (hg : InSimpleProfileClosure B W K g) :
                                                    InSimpleProfileClosure B W K fun (ξ : Fin KFin T) => f ξ - g ξ

                                                    Closure under subtraction: f - g ∈ closure if both are.

                                                    theorem Graphon.Lovasz.InSimpleProfileClosure.finset_sum {T K : } (B : Fin TFin T) (W : Fin T) {α : Type u_1} (S : Finset α) (g : α(Fin KFin T)) (hg : aS, InSimpleProfileClosure B W K (g a)) :
                                                    InSimpleProfileClosure B W K fun (ξ : Fin KFin T) => aS, g a ξ

                                                    Closure under Finset.sum over an index set.

                                                    theorem Graphon.Lovasz.InSimpleProfileClosure.finset_prod {T K : } (B : Fin TFin T) (W : Fin T) {α : Type u_1} (S : Finset α) (g : α(Fin KFin T)) (hg : aS, InSimpleProfileClosure B W K (g a)) :
                                                    InSimpleProfileClosure B W K fun (ξ : Fin KFin T) => aS, g a ξ

                                                    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:

                                                    1. Lagrange fullness: prove of_const_on_tupleEquivSimple — every tupleEquivSimple-invariant function is in the closure. Pure Lagrange interpolation, ~200 LOC. Mirrors K=1 of_const_on_orbit.

                                                    2. 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).

                                                    3. 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) #

                                                    theorem Graphon.Lovasz.InSimpleProfileClosure.of_const_on_tupleEquivSimple {T K : } (B : Fin TFin T) (W : Fin T) (f : (Fin KFin T)) (hf : ∀ (ξ ξ' : Fin KFin T), (∀ (n' : ) (F : SimpleGraph (Fin (n' + K))) [inst : DecidableRel F.Adj], Graphon.Lovasz.inlineSimpleEval✝ B W F ξ = Graphon.Lovasz.inlineSimpleEval✝ B W F ξ')f ξ = f ξ') :

                                                    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:

                                                    theorem Graphon.Lovasz.multiLabeledEvalK_eq_of_orbit {T K n : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (M : MultiLabeledGraph K n) {ξ ξ' : Fin KFin T} (h_orbit : ∃ (σ : Equiv.Perm (Fin T)), (∀ (i : Fin T), W (σ i) = W i) (∀ (i j : Fin T), B (σ i) (σ j) = B i j) ∀ (i : Fin K), ξ' i = σ (ξ i)) :
                                                    multiLabeledEvalK K n M B W ξ = multiLabeledEvalK K n M B W ξ'

                                                    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).

                                                    theorem Graphon.Lovasz.label_unlabeled_square_with_background_descends {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {ξ ξ' : Fin KFin T} (h_orbit : ∃ (σ : Equiv.Perm (Fin T)), (∀ (i : Fin T), W (σ i) = W i) (∀ (i j : Fin T), B (σ i) (σ j) = B i j) ∀ (i : Fin K), ξ' i = σ (ξ i)) (a : Fin K) (r : Fin K) :
                                                    t : Fin T, W t * B (ξ a) t ^ 2 * b : Fin K, B t (ξ b) ^ r b = t : Fin T, W t * B (ξ' a) t ^ 2 * b : Fin K, B t (ξ' b) ^ r b

                                                    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:

                                                    The bridge theorem (§4 below) is exactly tupleEquivSimpletupleEquivMulti. The reverse direction tupleEquivMultitupleEquivSimple 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.

                                                    def Graphon.Lovasz.tupleEquivSimple {T K : } (B : Fin TFin T) (W : Fin T) (ξ ξ' : Fin KFin T) :

                                                    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
                                                      def Graphon.Lovasz.tupleEquivMulti {T K : } (B : Fin TFin T) (W : Fin T) (ξ ξ' : Fin KFin T) :

                                                      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
                                                      Instances For
                                                        def Graphon.Lovasz.tupleEquivLoop {T K : } (B : Fin TFin T) (W : Fin T) (ξ ξ' : Fin KFin T) :

                                                        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 tupleEquivSimpletupleEquivLoop via the Lovász §3 rank theorem.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem Graphon.Lovasz.tupleEquivMulti_of_tupleEquivLoop {T K : } (B : Fin TFin T) (W : Fin T) {ξ ξ' : Fin KFin T} (h : tupleEquivLoop B W ξ ξ') :
                                                          tupleEquivMulti B W ξ ξ'

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

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

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

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

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

                                                          Mathematical content: η ↦ B(η a, η a) is orbit-invariant. The proof reduces to the K=1 case (via tupleEquivSimple_restrict_along) which routes through rooted_profiles_separate_vertex_orbits — PROVED via rootedProfileEquiv_imp_vertexOrbitRel (the rank-theorem route; the historical #77 closed-walk route was refuted and removed).

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

                                                          Multi ⟹ simple (trivial direction).

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

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

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

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

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

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

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

                                                          def Graphon.Lovasz.IsWeightedAutomorphism {T : } (B : Fin TFin T) (W : Fin T) (σ : Equiv.Perm (Fin T)) :

                                                          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
                                                            def Graphon.Lovasz.tupleOrbitRel {T K : } (B : Fin TFin T) (W : Fin T) (ξ ξ' : Fin KFin T) :

                                                            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
                                                            Instances For
                                                              def Graphon.Lovasz.restrictTuple {T k : } (ξ : Fin (k + 1)Fin T) :
                                                              Fin kFin T

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

                                                              Equations
                                                              Instances For
                                                                noncomputable def Graphon.Lovasz.rangeFinset {T k : } (φ : Fin kFin T) :

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

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

                                                                Equations
                                                                Instances For
                                                                  noncomputable def Graphon.Lovasz.deficit {T k : } (φ : Fin kFin T) :

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

                                                                  Equations
                                                                  Instances For
                                                                    theorem Graphon.Lovasz.rangeFinset_card_le {T k : } (φ : Fin kFin T) :
                                                                    theorem Graphon.Lovasz.rangeFinset_snoc {T k : } (φ : Fin kFin T) (a : Fin T) :
                                                                    theorem Graphon.Lovasz.deficit_lt_of_not_mem {T k : } (φ : Fin kFin T) (a : Fin T) (ha : arangeFinset φ) :

                                                                    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 iff deficit = 0.

                                                                    theorem Graphon.Lovasz.exists_not_mem_rangeFinset {T k : } (φ : Fin kFin T) (h : ¬Function.Surjective φ) :
                                                                    ∃ (a : Fin T), arangeFinset φ

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

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

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

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

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

                                                                    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:

                                                                    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.

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

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

                                                                    Equations
                                                                    Instances For
                                                                      theorem Graphon.Lovasz.coeffRestrictSimple_pos_at_restrict {T k : } (B : Fin TFin T) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (μ : Fin (k + 1)Fin T) :

                                                                      Positivity of coeffRestrictSimple at its own restriction.

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

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

                                                                      Existence of an extension witness from positive coefficient.

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

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

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

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

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

                                                                      the product trace identity (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).

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

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

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        theorem Graphon.Lovasz.out_pair_eq' {T' : } {V : Type u_1} (Bm : Fin T'Fin T') (hB : ∀ (i j : Fin T'), Bm i j = Bm j i) (g : VFin T') (x y : V) :
                                                                        Bm (g (Quot.out s(x, y)).1) (g (Quot.out s(x, y)).2) = Bm (g x) (g y)

                                                                        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.

                                                                        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).

                                                                        def Graphon.Lovasz.labVertex {K : } (i : Fin K) :
                                                                        Fin (1 + K)

                                                                        Embed label i : Fin K as the vertex of value i in Fin (1 + K).

                                                                        Equations
                                                                        Instances For

                                                                          The single unlabeled vertex (value K) in Fin (1 + K).

                                                                          Equations
                                                                          Instances For

                                                                            Cai–Govorov test graph Gχ: the unlabeled vertex is joined to exactly the labels in S ⊆ Fin K.

                                                                            Equations
                                                                            Instances For
                                                                              theorem Graphon.Lovasz.starTestGraph_edge_injOn {K : } (S : Finset (Fin K)) (i : Fin K) :
                                                                              i Si'S, s(labVertex i, unlVertex) = s(labVertex i', unlVertex)i = i'
                                                                              theorem Graphon.Lovasz.tau_apply_labVertex {K T : } (ξ : Fin KFin T) (σ : Fin 1Fin T) (i : Fin K) :
                                                                              (if h : (labVertex i) < K then ξ (labVertex i), h else σ (labVertex i) - K, ) = ξ i

                                                                              The simpleEvalAt label map sends labVertex i to ξ i (stated in the beta-reduced dite form produced by out_pair_eq').

                                                                              theorem Graphon.Lovasz.tau_apply_unlVertex {K T : } (ξ : Fin KFin T) (σ : Fin 1Fin T) :
                                                                              (if h : unlVertex < K then ξ unlVertex, h else σ unlVertex - K, ) = σ 0

                                                                              The simpleEvalAt label map sends unlVertex to σ 0 (beta-reduced dite form).

                                                                              theorem Graphon.Lovasz.simpleEvalAt_starTestGraph {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (S : Finset (Fin K)) (ξ : Fin KFin T) :
                                                                              simpleEvalAt B W (starTestGraph S) ξ = t : Fin T, W t * iS, B (ξ i) t

                                                                              Closed form for Gχ: simpleEvalAt B W (starTestGraph S) ξ = ∑ₜ W t · ∏_{i∈S} B (ξ i) t.

                                                                              Cai–Govorov edge-test graph Gλτ (two unlabeled vertices) #

                                                                              def Graphon.Lovasz.labVertex2 {K : } (i : Fin K) :
                                                                              Fin (2 + K)

                                                                              Embed label i : Fin K as the vertex of value i in Fin (2 + K).

                                                                              Equations
                                                                              Instances For

                                                                                The first unlabeled vertex (value K, mapped to σ 0) in Fin (2 + K).

                                                                                Equations
                                                                                Instances For

                                                                                  The second unlabeled vertex (value K + 1, mapped to σ 1) in Fin (2 + K).

                                                                                  Equations
                                                                                  Instances For
                                                                                    def Graphon.Lovasz.edgeTestGraph {K : } (Sₗ : Finset (Fin K)) :
                                                                                    SimpleGraph (Fin (2 + K))

                                                                                    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 .

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      theorem Graphon.Lovasz.edgeTestGraph_edge_injOn_Sₗ {K : } (Sₗ : Finset (Fin K)) (i : Fin K) :
                                                                                      i Sₗi'Sₗ, s(labVertex2 i, unlVertex0) = s(labVertex2 i', unlVertex0)i = i'
                                                                                      theorem Graphon.Lovasz.edgeTestGraph_edge_injOn_Sτ {K : } ( : Finset (Fin K)) (i : Fin K) :
                                                                                      i i', s(labVertex2 i, unlVertex1) = s(labVertex2 i', unlVertex1)i = i'
                                                                                      theorem Graphon.Lovasz.tau2_apply_labVertex2 {K T : } (ξ : Fin KFin T) (σ : Fin 2Fin T) (i : Fin K) :
                                                                                      (if h : (labVertex2 i) < K then ξ (labVertex2 i), h else σ (labVertex2 i) - K, ) = ξ i

                                                                                      simpleEvalAt label map: labVertex2 i ↦ ξ i (beta-reduced dite form).

                                                                                      theorem Graphon.Lovasz.tau2_apply_unlVertex0 {K T : } (ξ : Fin KFin T) (σ : Fin 2Fin T) :
                                                                                      (if h : unlVertex0 < K then ξ unlVertex0, h else σ unlVertex0 - K, ) = σ 0

                                                                                      simpleEvalAt label map: unlVertex0 ↦ σ 0 (beta-reduced dite form).

                                                                                      theorem Graphon.Lovasz.tau2_apply_unlVertex1 {K T : } (ξ : Fin KFin T) (σ : Fin 2Fin T) :
                                                                                      (if h : unlVertex1 < K then ξ unlVertex1, h else σ unlVertex1 - K, ) = σ 1

                                                                                      simpleEvalAt label map: unlVertex1 ↦ σ 1 (beta-reduced dite form).

                                                                                      theorem Graphon.Lovasz.simpleEvalAt_edgeTestGraph {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (Sₗ : Finset (Fin K)) (ξ : Fin KFin T) :
                                                                                      simpleEvalAt B W (edgeTestGraph Sₗ ) ξ = t : Fin T, t' : Fin T, (W t * W t' * B t t' * iSₗ, B (ξ i) t) * i, B (ξ i) t'

                                                                                      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) #

                                                                                      def Graphon.Lovasz.SuperSurjective {K T : } (ξ : Fin KFin T) :

                                                                                      ξ : 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).

                                                                                      Equations
                                                                                      Instances For
                                                                                        theorem Graphon.Lovasz.prod_label_eq_prod_mult {K T : } (B : Fin TFin T) (ξ : Fin KFin T) (S : Finset (Fin K)) (t : Fin T) :
                                                                                        iS, B (ξ i) t = v : Fin T, B v t ^ {iS | ξ i = v}.card

                                                                                        Regroup a product over labels into a product over host vertices weighted by multiplicity: ∏_{i∈S} B (ξ i) t = ∏_v (B v t) ^ |{i∈S : ξ i = v}|.

                                                                                        theorem Graphon.Lovasz.tupleEquivSimple_starTestGraph_mult {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {ξ ξ' : Fin KFin T} (h : tupleEquivSimple B W ξ ξ') (S : Finset (Fin K)) :
                                                                                        t : Fin T, W t * v : Fin T, B v t ^ {iS | ξ i = v}.card = t : Fin T, W t * v : Fin T, B v t ^ {iS | ξ' i = v}.card

                                                                                        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.

                                                                                        structure Graphon.Lovasz.TestEvalEq {K T : } (B : Fin TFin T) (W : Fin T) (ξ ξ' : Fin KFin T) :

                                                                                        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 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.

                                                                                        Instances For
                                                                                          theorem Graphon.Lovasz.TestEvalEq.of_tupleEquivSimple {K T : } {B : Fin TFin T} {W : Fin T} {ξ ξ' : Fin KFin T} (h : tupleEquivSimple B W ξ ξ') :
                                                                                          TestEvalEq B W ξ ξ'

                                                                                          Full simple-equivalence yields the test-graph interface.

                                                                                          theorem Graphon.Lovasz.aligned_moments_class_balance {T : } (x y : Fin TFin T) (a b : Fin T) (hmom : ∀ (k : Fin T), (∀ (j : Fin T), k j < 2 * T)t : Fin T, a t * j : Fin T, x t j ^ k j = t : Fin T, b t * j : Fin T, y t j ^ k j) (z : Fin T) :
                                                                                          t : Fin T with x t = z, a t = t : Fin T with y t = z, b t

                                                                                          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.

                                                                                          theorem Graphon.Lovasz.aligned_moments_class_balance_of_bound {ι : Type u_1} [Fintype ι] {s : } (x y : ιFin s) (a b : ι) (N : ) (hNx : ∀ (c : Fin s), (Finset.image (fun (i : ι) => x i c) Finset.univ).card N) (hNy : ∀ (c : Fin s), (Finset.image (fun (i : ι) => y i c) Finset.univ).card N) (hmom : ∀ (k : Fin s), (∀ (c : Fin s), k c < 2 * N)i : ι, a i * c : Fin s, x i c ^ k c = i : ι, b i * c : Fin s, y i c ^ k c) (z : Fin s) :
                                                                                          i : ι with x i = z, a i = i : ι with y i = z, b i

                                                                                          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.

                                                                                          theorem Graphon.Lovasz.aligned_star_moments_profile_balance {T : } (B : Fin TFin T) (W : Fin T) (s : Fin TFin T) (haligned : ∀ (k : Fin T), (∀ (j : Fin T), k j < 2 * T)t : Fin T, W t * j : Fin T, B j t ^ k j = t : Fin T, W t * j : Fin T, B (s j) t ^ k j) (z : Fin T) :
                                                                                          t : Fin T with (fun (j : Fin T) => B j t) = z, W t = t : Fin T with (fun (j : Fin T) => B (s j) t) = z, W t

                                                                                          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.

                                                                                          theorem Graphon.Lovasz.aligned_star_moments_weight_balance {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (htwin : ∀ (i j : Fin T), i jB i B j) (s : Fin TFin T) (haligned : ∀ (k : Fin T), (∀ (j : Fin T), k j < 2 * T)t : Fin T, W t * j : Fin T, B j t ^ k j = t : Fin T, W t * j : Fin T, B (s j) t ^ k j) (t : Fin T) :
                                                                                          W t = u : Fin T with ∀ (j : Fin T), B j t = B (s j) u, W u

                                                                                          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.

                                                                                          theorem Graphon.Lovasz.aligned_star_moments_support {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (s : Fin TFin T) (haligned : ∀ (k : Fin T), (∀ (j : Fin T), k j < 2 * T)t : Fin T, W t * j : Fin T, B j t ^ k j = t : Fin T, W t * j : Fin T, B (s j) t ^ k j) (t : Fin T) :
                                                                                          ∃ (u : Fin T), ∀ (j : Fin T), B j t = B (s j) 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 #

                                                                                          theorem Graphon.Lovasz.exists_large_const_image_subset {K T : } (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (j : Fin T) :
                                                                                          ∃ (s_j : Fin T), J{i : Fin K | ξ i = j}, 2 * T J.card iJ, ξ' i = s_j

                                                                                          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.)

                                                                                          noncomputable def Graphon.Lovasz.superMap {K T : } (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (j : Fin T) :
                                                                                          Fin T

                                                                                          The preliminary Cai–Govorov map s : Fin T → Fin T: the constant ξ'-value on a large subset of each ξ-fibre.

                                                                                          Equations
                                                                                          Instances For
                                                                                            noncomputable def Graphon.Lovasz.superFiberSubset {K T : } (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (j : Fin T) :

                                                                                            The chosen large ξ'-constant subset of the ξ-fibre over j.

                                                                                            Equations
                                                                                            Instances For
                                                                                              theorem Graphon.Lovasz.superFiberSubset_subset {K T : } (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (j : Fin T) :
                                                                                              superFiberSubset ξ ξ' j{i : Fin K | ξ i = j}
                                                                                              theorem Graphon.Lovasz.superFiberSubset_card {K T : } (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (j : Fin T) :
                                                                                              2 * T (superFiberSubset ξ ξ' j).card
                                                                                              theorem Graphon.Lovasz.superFiberSubset_mem_left {K T : } (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (j : Fin T) {i : Fin K} (hi : i superFiberSubset ξ ξ' j) :
                                                                                              ξ i = j
                                                                                              theorem Graphon.Lovasz.superFiberSubset_image_const {K T : } (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (j : Fin T) (i : Fin K) :
                                                                                              i superFiberSubset ξ ξ' jξ' i = superMap ξ ξ' j
                                                                                              theorem Graphon.Lovasz.superFiberSubset_disjoint {K T : } (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) {j j' : Fin T} (hjj : j j') :
                                                                                              Disjoint (superFiberSubset ξ ξ' j) (superFiberSubset ξ ξ' j')

                                                                                              Distinct fibres give disjoint chosen subsets (each lies in a distinct ξ-fibre).

                                                                                              Chunk 3A.3: aligned moments from selected labels #

                                                                                              theorem Graphon.Lovasz.exists_exponent_label_set {K T : } (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (k : Fin T) (hk : ∀ (j : Fin T), k j < 2 * T) :
                                                                                              ∃ (Kf : Fin TFinset (Fin K)), (∀ (j : Fin T), Kf jsuperFiberSubset ξ ξ' j) ∀ (j : Fin T), (Kf j).card = k j

                                                                                              For any bounded exponent vector k, select inside each ξ-fibre's distinguished subset a sub-subset of size exactly k j.

                                                                                              theorem Graphon.Lovasz.aligned_moments_of_testEvalEq_super {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (k : Fin T) :
                                                                                              (∀ (j : Fin T), k j < 2 * T)t : Fin T, W t * j : Fin T, B j t ^ k j = t : Fin T, W t * j : Fin T, B (superMap ξ ξ' j) t ^ 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.

                                                                                              theorem Graphon.Lovasz.superMap_support {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (t : Fin T) :
                                                                                              ∃ (u : Fin T), ∀ (j : Fin T), B j t = B (superMap ξ ξ' j) u

                                                                                              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.

                                                                                              Chunk 3A.4: superMap is bijective #

                                                                                              theorem Graphon.Lovasz.superMap_injective {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') :

                                                                                              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.)

                                                                                              theorem Graphon.Lovasz.superMap_bijective {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') :

                                                                                              superMap is bijective (injective endomap of a finite type).

                                                                                              noncomputable def Graphon.Lovasz.superPerm {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') :

                                                                                              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
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem Graphon.Lovasz.superPerm_apply {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (j : Fin T) :
                                                                                                (superPerm B hB W hW htwin ξ ξ' h) j = superMap ξ ξ' j

                                                                                                Chunk 3A.5: aligned edge moments (edgeTestGraph) #

                                                                                                theorem Graphon.Lovasz.aligned_edge_moments_of_testEvalEq_super {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (k l : Fin T) :
                                                                                                (∀ (j : Fin T), k j < 2 * T)(∀ (j : Fin T), l j < 2 * T)x : Fin T, y : Fin T, (W x * W y * B x y * j : Fin T, B j x ^ k j) * j : Fin T, B j y ^ l j = x : Fin T, y : Fin T, (W x * W y * B x y * j : Fin T, B (superMap ξ ξ' j) x ^ k j) * j : Fin T, B (superMap ξ ξ' j) y ^ l j

                                                                                                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.

                                                                                                theorem Graphon.Lovasz.aligned_edge_moments_pair_balance {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (z₁ z₂ : Fin T) :
                                                                                                (∑ p : Fin T × Fin T, if (fun (j : Fin T) => B j p.1) = z₁ (fun (j : Fin T) => B j p.2) = z₂ then W p.1 * W p.2 * B p.1 p.2 else 0) = p : Fin T × Fin T, if (fun (j : Fin T) => B (superMap ξ ξ' j) p.1) = z₁ (fun (j : Fin T) => B (superMap ξ ξ' j) p.2) = z₂ then W p.1 * W p.2 * B p.1 p.2 else 0

                                                                                                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 #

                                                                                                noncomputable def Graphon.Lovasz.superInv {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (t : Fin T) :
                                                                                                Fin T

                                                                                                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
                                                                                                Instances For
                                                                                                  theorem Graphon.Lovasz.superInv_spec {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (t j : Fin T) :
                                                                                                  B j t = B (superMap ξ ξ' j) (superInv B hB W hW htwin ξ ξ' h t)
                                                                                                  theorem Graphon.Lovasz.superInv_unique {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') {t u : Fin T} (hu : ∀ (j : Fin T), B j t = B (superMap ξ ξ' j) u) :
                                                                                                  u = superInv B hB W hW htwin ξ ξ' h t
                                                                                                  theorem Graphon.Lovasz.superInv_injective {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') :
                                                                                                  Function.Injective (superInv B hB W hW htwin ξ ξ' h)
                                                                                                  theorem Graphon.Lovasz.superInv_bijective {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') :
                                                                                                  Function.Bijective (superInv B hB W hW htwin ξ ξ' h)
                                                                                                  theorem Graphon.Lovasz.superInv_preserves_W {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (t : Fin T) :
                                                                                                  W (superInv B hB W hW htwin ξ ξ' h t) = W t

                                                                                                  Weight preservation for superInv. The support fibre of t is the singleton {superInv t}, so weight balance gives W (superInv t) = W t.

                                                                                                  theorem Graphon.Lovasz.superInv_preserves_B {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (a b : Fin T) :
                                                                                                  B (superInv B hB W hW htwin ξ ξ' h a) (superInv B hB W hW htwin ξ ξ' h b) = B a b

                                                                                                  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.

                                                                                                  theorem Graphon.Lovasz.superInv_eq_superMap {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') :
                                                                                                  superInv B hB W hW htwin ξ ξ' h = superMap ξ ξ'

                                                                                                  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 #

                                                                                                  theorem Graphon.Lovasz.superMap_preserves_B {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (a b : Fin T) :
                                                                                                  B (superMap ξ ξ' a) (superMap ξ ξ' b) = B a b
                                                                                                  theorem Graphon.Lovasz.superMap_preserves_W {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (a : Fin T) :
                                                                                                  W (superMap ξ ξ' a) = W a
                                                                                                  theorem Graphon.Lovasz.superMap_isWeightedAutomorphism {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') :
                                                                                                  IsWeightedAutomorphism B W (superPerm B hB W hW htwin ξ ξ' h)

                                                                                                  The super-surjective orbit automorphism. superPerm is a weighted automorphism of (B, W) — the certified output of chunk 3A.5.

                                                                                                  theorem Graphon.Lovasz.one_extra_label_moment {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (i₀ : Fin K) (k : Fin T) (hk : ∀ (j : Fin T), k j < T) :
                                                                                                  t : Fin T, W t * B (ξ i₀) t * j : Fin T, B j t ^ k j = t : Fin T, W t * B (ξ' i₀) (superMap ξ ξ' t) * j : Fin T, B j t ^ k j

                                                                                                  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.

                                                                                                  theorem Graphon.Lovasz.superMap_agrees_on_all_labels {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') (i : Fin K) :
                                                                                                  ξ' i = superMap ξ ξ' (ξ i)

                                                                                                  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₀).

                                                                                                  theorem Graphon.Lovasz.testEvalEq_implies_orbit_super {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : TestEvalEq B W ξ ξ') :
                                                                                                  tupleOrbitRel B W ξ ξ'

                                                                                                  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.

                                                                                                  theorem Graphon.Lovasz.tupleEquivSimple_implies_orbit_super {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) ( : SuperSurjective ξ) (h : tupleEquivSimple B W ξ ξ') :
                                                                                                  tupleOrbitRel B W ξ ξ'

                                                                                                  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
                                                                                                    theorem Graphon.Lovasz.multiLabeledEvalK_castUnlabeled {T K a b : } (hab : a = b) (M : MultiLabeledGraph K a) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :

                                                                                                    The multigraph evaluation is invariant under the val-preserving unlabeled re-cast.

                                                                                                    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
                                                                                                      theorem Graphon.Lovasz.multiLabeledEvalK_sum_extra_labels {K m n T : } (M : MultiLabeledGraph (K + m) n) (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (φ : Fin KFin T) :
                                                                                                      ρ : Fin mFin T, (∏ j : Fin m, W (ρ j)) * multiLabeledEvalK (K + m) n M B W (Fin.append φ ρ) = multiLabeledEvalK K (n + m) (traceIterExtraLabels m M) B W φ

                                                                                                      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 #

                                                                                                      theorem Graphon.Lovasz.simpleEvalAt_eq_multi' {T K n : } (B : Fin TFin T) (W : Fin T) (F : SimpleGraph (Fin (n + K))) [DecidableRel F.Adj] (ξ : Fin KFin T) :

                                                                                                      Local (public) connector: simpleEvalAt is multiLabeledEvalK on ofSimple (the file-local analog of the private simpleEvalAt_eq_multi in Lovasz).

                                                                                                      def Graphon.Lovasz.unlabelExtras {K m n : } (G : SimpleGraph (Fin (n + (K + m)))) :
                                                                                                      SimpleGraph (Fin (n + m + K))

                                                                                                      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
                                                                                                        theorem Graphon.Lovasz.traceIterExtraLabels_mult {K n : } (m : ) (M : MultiLabeledGraph (K + m) n) (e : Sym2 (Fin (n + m + K))) :

                                                                                                        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.

                                                                                                        theorem Graphon.Lovasz.traceIterExtraLabels_ofSimple_eval {T K m n : } (B : Fin TFin T) (W : Fin T) (G : SimpleGraph (Fin (n + (K + m)))) [DecidableRel G.Adj] (ξ : Fin KFin T) :

                                                                                                        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) #

                                                                                                        @[reducible, inline]
                                                                                                        abbrev Graphon.Lovasz.ExtendsFin {K T m : } (ξ : Fin KFin T) (μ : Fin (K + m)Fin T) :

                                                                                                        μ : 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
                                                                                                        Instances For
                                                                                                          noncomputable def Graphon.Lovasz.extensionWeightFin {K T m : } (W : Fin T) (μ : Fin (K + m)Fin T) :

                                                                                                          The W-product over the m extra label values of μ.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            def Graphon.Lovasz.appendExtensionEquiv {K T m : } (ξ : Fin KFin T) :
                                                                                                            (Fin mFin T) { μ : Fin (K + m)Fin T // ExtendsFin ξ μ }

                                                                                                            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
                                                                                                              theorem Graphon.Lovasz.sum_extensions_eq_sum_rho {K T m n : } (B : Fin TFin T) (W : Fin T) (G : SimpleGraph (Fin (n + (K + m)))) [DecidableRel G.Adj] (ξ : Fin KFin T) :
                                                                                                              μ : { μ : Fin (K + m)Fin T // ExtendsFin ξ μ }, extensionWeightFin W μ * simpleEvalAt B W G μ = ρ : Fin mFin T, (∏ j : Fin m, W (ρ j)) * simpleEvalAt B W G (Fin.append ξ ρ)
                                                                                                              theorem Graphon.Lovasz.sum_extensions_eval {K T m n : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (G : SimpleGraph (Fin (n + (K + m)))) [DecidableRel G.Adj] (ζ : Fin KFin T) :
                                                                                                              μ : { μ : Fin (K + m)Fin T // ExtendsFin ζ μ }, extensionWeightFin W μ * simpleEvalAt B W G μ = simpleEvalAt B W (unlabelExtras G) ζ

                                                                                                              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).

                                                                                                              theorem Graphon.Lovasz.extension_sum_identity {K T m n : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {ξ ξ' : Fin KFin T} (h : tupleEquivSimple B W ξ ξ') (G : SimpleGraph (Fin (n + (K + m)))) [DecidableRel G.Adj] :
                                                                                                              μ : { μ : Fin (K + m)Fin T // ExtendsFin ξ μ }, extensionWeightFin W μ * simpleEvalAt B W G μ = ν : { ν : Fin (K + m)Fin T // ExtendsFin ξ' ν }, extensionWeightFin W ν * simpleEvalAt B W G ν

                                                                                                              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) #

                                                                                                              noncomputable def Graphon.Lovasz.coverExtra (T : ) :
                                                                                                              Fin (T * (2 * T ^ 2))Fin T

                                                                                                              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
                                                                                                              Instances For
                                                                                                                noncomputable def Graphon.Lovasz.superExt {K T : } (ξ : Fin KFin T) :
                                                                                                                Fin (K + T * (2 * T ^ 2))Fin T

                                                                                                                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
                                                                                                                  theorem Graphon.Lovasz.superExt_extends {K T : } (ξ : Fin KFin T) :
                                                                                                                  theorem Graphon.Lovasz.coverExtra_fiber_card {T : } (v : Fin T) :
                                                                                                                  {j : Fin (T * (2 * T ^ 2)) | coverExtra T j = v}.card = 2 * T ^ 2

                                                                                                                  Chunk 3B.2b: separation (contrapositive of the super-surjective case) #

                                                                                                                  theorem Graphon.Lovasz.not_tupleEquivSimple_of_not_orbit {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ : Fin KFin T) (μ : Fin (K + T * (2 * T ^ 2))Fin T) (hnotorbit : ¬tupleOrbitRel B W (superExt ξ) μ) :

                                                                                                                  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.

                                                                                                                  Equations
                                                                                                                  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.

                                                                                                                    Equations
                                                                                                                    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).

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        theorem Graphon.Lovasz.MultiLabeledGraph.ext' {K n : } {M₁ M₂ : MultiLabeledGraph K n} (h : M₁.mult = M₂.mult) :
                                                                                                                        M₁ = M₂

                                                                                                                        Multigraphs with equal multiplicity functions are equal (multNoLoop is a proposition).

                                                                                                                        toSimple is a section of ofSimple on multiplicity-≤-1 multigraphs.

                                                                                                                        theorem Graphon.Lovasz.simpleEvalAt_toSimple {T K n : } (B : Fin TFin T) (W : Fin T) (M : MultiLabeledGraph K n) (hM : M.SimpleMult) (ξ : Fin KFin T) :

                                                                                                                        Evaluating the simple graph M.toSimple agrees with the multigraph evaluation of M, provided all multiplicities are ≤ 1.

                                                                                                                        Invariant suppliers: ofSimple, the test graphs, and empty #

                                                                                                                        theorem Graphon.Lovasz.MultiLabeledGraph.ofSimple_noLabelPairs {K n : } (F : SimpleGraph (Fin (n + K))) [DecidableRel F.Adj] (hF : ∀ (a b : Fin (n + K)), a < Kb < Ks(a, b)F.edgeFinset) :

                                                                                                                        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.

                                                                                                                        glueCast characterizations and invariant preservation under glue #

                                                                                                                        theorem Graphon.Lovasz.glueCast₁_some_val {K n₁ n₂ : } {v : Fin (n₁ + n₂ + K)} {u : Fin (n₁ + K)} (h : glueCast₁ K n₁ n₂ v = some u) :
                                                                                                                        u = v v < n₁ + K
                                                                                                                        theorem Graphon.Lovasz.glueCast₂_some_val {K n₁ n₂ : } {v : Fin (n₁ + n₂ + K)} {u : Fin (n₂ + K)} (h : glueCast₂ K n₁ n₂ v = some u) :
                                                                                                                        v < K u = v n₁ + K v u = v - n₁
                                                                                                                        theorem Graphon.Lovasz.glueCast₁_ne_none_of_lt {K n₁ n₂ : } {v : Fin (n₁ + n₂ + K)} (hv : v < n₁ + K) :
                                                                                                                        glueCast₁ K n₁ n₂ v none
                                                                                                                        theorem Graphon.Lovasz.glueCast₂_ne_none_of_lt {K n₁ n₂ : } {v : Fin (n₁ + n₂ + K)} (hv : v < K) :
                                                                                                                        glueCast₂ K n₁ n₂ v none
                                                                                                                        theorem Graphon.Lovasz.MultiLabeledGraph.glue_simpleMult {K n₁ n₂ : } {M₁ : MultiLabeledGraph K n₁} {M₂ : MultiLabeledGraph K n₂} (h₁ : M₁.SimpleMult) (h₂ : M₂.SimpleMult) (hlp₂ : M₂.NoLabelPairs) :
                                                                                                                        (M₁.glue M₂).SimpleMult

                                                                                                                        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.

                                                                                                                        theorem Graphon.Lovasz.MultiLabeledGraph.glue_noLabelPairs {K n₁ n₂ : } {M₁ : MultiLabeledGraph K n₁} {M₂ : MultiLabeledGraph K n₂} (h₁ : M₁.NoLabelPairs) (h₂ : M₂.NoLabelPairs) :
                                                                                                                        (M₁.glue M₂).NoLabelPairs

                                                                                                                        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.

                                                                                                                        def Graphon.Lovasz.glueSigma {K : } (p q : (n : ) × MultiLabeledGraph K n) :
                                                                                                                        (n : ) × MultiLabeledGraph K n

                                                                                                                        Sigma-packaged disjoint glue of two multigraphs with arbitrary unlabeled sizes.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          def Graphon.Lovasz.glueList {K : } (l : List ((n : ) × MultiLabeledGraph K n)) :
                                                                                                                          (n : ) × MultiLabeledGraph K n

                                                                                                                          Fold a list of multigraphs into one by repeated disjoint gluing (empty multigraph base).

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            theorem Graphon.Lovasz.multiLabeledEvalK_glueList {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (l : List ((n : ) × MultiLabeledGraph K n)) (μ : Fin KFin T) :
                                                                                                                            multiLabeledEvalK K (glueList l).fst (glueList l).snd B W μ = (List.map (fun (p : (n : ) × MultiLabeledGraph K n) => multiLabeledEvalK K p.fst p.snd B W μ) l).prod

                                                                                                                            Iterated glue factorization: the evaluation of glueList l is the product of the component evaluations.

                                                                                                                            theorem Graphon.Lovasz.glueList_noLabelPairs {K : } (l : List ((n : ) × MultiLabeledGraph K n)) (hlp : pl, p.snd.NoLabelPairs) :

                                                                                                                            glueList inherits NoLabelPairs from its components.

                                                                                                                            theorem Graphon.Lovasz.glueList_simpleMult {K : } (l : List ((n : ) × MultiLabeledGraph K n)) (hs : pl, p.snd.SimpleMult) (hlp : pl, p.snd.NoLabelPairs) :

                                                                                                                            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.

                                                                                                                            @[reducible, inline]

                                                                                                                            Test-moment coordinates: inl S is the star test Gχ S; inr (Sₗ, Sτ) the edge test.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              noncomputable def Graphon.Lovasz.testMoment {K T : } (B : Fin TFin T) (W : Fin T) (c : TestCoord K) (μ : Fin KFin T) :

                                                                                                                              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
                                                                                                                                noncomputable def Graphon.Lovasz.coordGraph {K : } (c : TestCoord K) :
                                                                                                                                (n : ) × MultiLabeledGraph K n

                                                                                                                                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
                                                                                                                                  theorem Graphon.Lovasz.coordGraph_eval {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (c : TestCoord K) (μ : Fin KFin T) :
                                                                                                                                  noncomputable def Graphon.Lovasz.expGraph {K : } (k : TestCoord K) :
                                                                                                                                  (n : ) × MultiLabeledGraph K n

                                                                                                                                  The exponent graph: glue k c copies of each test coordinate's graph.

                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    theorem Graphon.Lovasz.expGraph_eval {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (k : TestCoord K) (μ : Fin KFin T) :
                                                                                                                                    multiLabeledEvalK K (expGraph k).fst (expGraph k).snd B W μ = c : TestCoord K, testMoment B W c μ ^ k c

                                                                                                                                    Closed form of the exponent graph: its evaluation is the product of test-moment powers.

                                                                                                                                    noncomputable def Graphon.Lovasz.expTestGraph {K : } (k : TestCoord K) :

                                                                                                                                    The exponent graph, converted back to an honest simple graph (chunk 4B).

                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      theorem Graphon.Lovasz.simpleEvalAt_expTestGraph {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (k : TestCoord K) (μ : Fin KFin T) :
                                                                                                                                      simpleEvalAt B W (expTestGraph k) μ = c : TestCoord K, testMoment B W c μ ^ k c

                                                                                                                                      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.

                                                                                                                                      theorem Graphon.Lovasz.testEvalEq_iff_moments {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {ξ ξ' : Fin KFin T} :
                                                                                                                                      TestEvalEq B W ξ ξ' ∀ (c : TestCoord K), testMoment B W c ξ = testMoment B W c ξ'

                                                                                                                                      The TestEvalEq interface is equivalent to matching of all test moments.

                                                                                                                                      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).

                                                                                                                                      theorem Graphon.Lovasz.extension_power_moments {K T m : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {ξ ξ' : Fin KFin T} (h : tupleEquivSimple B W ξ ξ') (k : TestCoord (K + m)) :
                                                                                                                                      ρ : Fin mFin T, (∏ j : Fin m, W (ρ j)) * c : TestCoord (K + m), testMoment B W c (Fin.append ξ ρ) ^ k c = ρ : Fin mFin T, (∏ j : Fin m, W (ρ j)) * c : TestCoord (K + m), testMoment B W c (Fin.append ξ' ρ) ^ k c

                                                                                                                                      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 ξ.

                                                                                                                                      noncomputable def Graphon.Lovasz.testProfile {K T : } (B : Fin TFin T) (W : Fin T) (μ : Fin KFin T) :

                                                                                                                                      The test-moment profile as a Fin-indexed vector (transport along Fintype.equivFin), for the graph-free Vandermonde engines.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        theorem Graphon.Lovasz.testProfile_eq_iff {K T : } {B : Fin TFin T} {W : Fin T} {μ ν : Fin KFin T} :
                                                                                                                                        testProfile B W μ = testProfile B W ν ∀ (c : TestCoord K), testMoment B W c μ = testMoment B W c ν
                                                                                                                                        theorem Graphon.Lovasz.exists_matching_extension {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) {ξ ξ' : Fin KFin T} (h : tupleEquivSimple B W ξ ξ') :
                                                                                                                                        ∃ (ρ' : Fin (T * (2 * T ^ 2))Fin T), ∀ (c : TestCoord (K + T * (2 * T ^ 2))), testMoment B W c (Fin.append ξ' ρ') = testMoment B W c (superExt ξ)

                                                                                                                                        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 #

                                                                                                                                        theorem Graphon.Lovasz.tupleEquivSimple_implies_orbit_general {K T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (v : Fin T), 0 < W v) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ ξ' : Fin KFin T) (h : tupleEquivSimple B W ξ ξ') :
                                                                                                                                        tupleOrbitRel B W ξ ξ'

                                                                                                                                        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).

                                                                                                                                        theorem Graphon.Lovasz.multigraphEval_in_simpleProfileClosure {T K n : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (M : MultiLabeledGraph K n) (h_sq_moment : ∀ {ξ₀ ξ₀' : Fin KFin T}, (∀ (n' : ) (F : SimpleGraph (Fin (n' + K))) [inst : DecidableRel F.Adj], (∑ σ : Fin n'Fin T, have τ := fun (v : Fin (n' + K)) => if h : v < K then ξ₀ v, h else σ v - K, ; (∏ v : Fin n', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) = σ : Fin n'Fin T, have τ := fun (v : Fin (n' + K)) => if h : v < K then ξ₀' v, h else σ v - K, ; (∏ v : Fin n', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2))∀ (c : Fin K), t : Fin T, W t * B (ξ₀ c) t ^ 2 = t : Fin T, W t * B (ξ₀' c) t ^ 2) :
                                                                                                                                        InSimpleProfileClosure B W K fun (ξ : Fin KFin T) => multiLabeledEvalK K n M B W ξ

                                                                                                                                        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:

                                                                                                                                        1. n = 0 / mults ≤ 1: dispatched in-line via existing infrastructure (multiLabeledEvalK_tupleEquiv_invariant_n_zero / simple-graph correspondence + h_equiv).

                                                                                                                                        2. LL-excess sub-case (every mult≥2 edge is label-label): CLOSED via multigraphEval_LL_excess_descends_aux (strong induction on M.LLSum; iterated single-edge peel; base case reduces to a simple graph). Polynomial decomposition à la Lovász §3.2 (F₁F₂-product).

                                                                                                                                        3. 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.

                                                                                                                                        theorem Graphon.Lovasz.multiLabeledEvalK_tupleEquiv_invariant {T K n : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (M : MultiLabeledGraph K n) (_h_sq_moment : ∀ {ξ₀ ξ₀' : Fin KFin T}, (∀ (n'' : ) (F : SimpleGraph (Fin (n'' + K))) [inst : DecidableRel F.Adj], (∑ σ : Fin n''Fin T, have τ := fun (v : Fin (n'' + K)) => if h : v < K then ξ₀ v, h else σ v - K, ; (∏ v : Fin n'', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) = σ : Fin n''Fin T, have τ := fun (v : Fin (n'' + K)) => if h : v < K then ξ₀' v, h else σ v - K, ; (∏ v : Fin n'', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2))∀ (c : Fin K), t : Fin T, W t * B (ξ₀ c) t ^ 2 = t : Fin T, W t * B (ξ₀' c) t ^ 2) {ξ ξ' : Fin KFin T} (h_simple : ∀ (n' : ) (F : SimpleGraph (Fin (n' + K))) [inst : DecidableRel F.Adj], (∑ σ : Fin n'Fin T, have τ := fun (v : Fin (n' + K)) => if h : v < K then ξ v, h else σ v - K, ; (∏ v : Fin n', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) = σ : Fin n'Fin T, have τ := fun (v : Fin (n' + K)) => if h : v < K then ξ' v, h else σ v - K, ; (∏ v : Fin n', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) :
                                                                                                                                        multiLabeledEvalK K n M B W ξ = multiLabeledEvalK K n M B W ξ'

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

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

                                                                                                                                        • PRIMARY ROOT: connection_matrix_rank_theorem (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.

                                                                                                                                        theorem Graphon.Lovasz.coeffRestrictSimple_equiv {T k : } (B : Fin TFin T) (W : Fin T) (hB : ∀ (i j : Fin T), B i j = B j i) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (h_sq_moment : ∀ {ξ₀ ξ₀' : Fin kFin T}, (∀ (n'' : ) (F : SimpleGraph (Fin (n'' + k))) [inst : DecidableRel F.Adj], (∑ σ : Fin n''Fin T, have τ := fun (v : Fin (n'' + k)) => if h : v < k then ξ₀ v, h else σ v - k, ; (∏ v : Fin n'', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) = σ : Fin n''Fin T, have τ := fun (v : Fin (n'' + k)) => if h : v < k then ξ₀' v, h else σ v - k, ; (∏ v : Fin n'', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2))∀ (c : Fin k), t : Fin T, W t * B (ξ₀ c) t ^ 2 = t : Fin T, W t * B (ξ₀' c) t ^ 2) (μ : Fin (k + 1)Fin T) {ξ ξ' : Fin kFin T} (h : tupleEquivSimple B W ξ ξ') :

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

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

                                                                                                                                        Proof outline (mirrors MatrixDetermination.coeffRestrict_equiv):

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

                                                                                                                                        Modulo (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.

                                                                                                                                        theorem Graphon.Lovasz.tupleEquivSimple_extend {T k : } (B : Fin TFin T) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (hB : ∀ (i j : Fin T), B i j = B j i) (htwin : ∀ (i j : Fin T), i jB i B j) (h_sq_moment : ∀ {ξ₀ ξ₀' : Fin kFin T}, (∀ (n'' : ) (F : SimpleGraph (Fin (n'' + k))) [inst : DecidableRel F.Adj], (∑ σ : Fin n''Fin T, have τ := fun (v : Fin (n'' + k)) => if h : v < k then ξ₀ v, h else σ v - k, ; (∏ v : Fin n'', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) = σ : Fin n''Fin T, have τ := fun (v : Fin (n'' + k)) => if h : v < k then ξ₀' v, h else σ v - k, ; (∏ v : Fin n'', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2))∀ (c : Fin k), t : Fin T, W t * B (ξ₀ c) t ^ 2 = t : Fin T, W t * B (ξ₀' c) t ^ 2) {ξ ξ' : Fin kFin T} (h : tupleEquivSimple B W ξ ξ') (μ : Fin (k + 1)Fin T) ( : restrictTuple μ = ξ) :
                                                                                                                                        ∃ (ν : Fin (k + 1)Fin T), restrictTuple ν = ξ' tupleEquivSimple B W μ ν

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

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

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

                                                                                                                                        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.

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

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

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

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

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

                                                                                                                                        theorem Graphon.Lovasz.tupleEquivSimple_restrict_along {T k T' : } (B : Fin TFin T) (W : Fin T) (hB : ∀ (i j : Fin T), B i j = B j i) {φ ψ : Fin kFin T} (r : Fin T' Fin k) (h : tupleEquivSimple B W φ ψ) :
                                                                                                                                        tupleEquivSimple B W (φ r) (ψ r)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                                                                                                                        §3.95 — Connection-matrix rank theorem (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):

                                                                                                                                        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 tupleEquivSimpletupleOrbitRel. 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.)

                                                                                                                                        theorem Graphon.Lovasz.tupleOrbitRel_refl {T K : } (B : Fin TFin T) (W : Fin T) (ξ : Fin KFin T) :
                                                                                                                                        tupleOrbitRel B W ξ ξ

                                                                                                                                        tupleOrbitRel is reflexive.

                                                                                                                                        Witnessed by the identity automorphism.

                                                                                                                                        theorem Graphon.Lovasz.tupleOrbitRel_symm {T K : } (B : Fin TFin T) (W : Fin T) {ξ ξ' : Fin KFin T} (h : tupleOrbitRel B W ξ ξ') :
                                                                                                                                        tupleOrbitRel B W ξ' ξ

                                                                                                                                        tupleOrbitRel is symmetric.

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

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

                                                                                                                                        tupleOrbitRel is transitive.

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

                                                                                                                                        theorem Graphon.Lovasz.tupleOrbitRel_equivalence {T K : } (B : Fin TFin T) (W : Fin T) :

                                                                                                                                        tupleOrbitRel is an equivalence relation.

                                                                                                                                        def Graphon.Lovasz.tupleOrbitSetoid {T : } (B : Fin TFin T) (W : Fin T) (K : ) :
                                                                                                                                        Setoid (Fin KFin T)

                                                                                                                                        Setoid on tuples induced by tupleOrbitRel.

                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          def Graphon.Lovasz.OrbitClass (T K : ) (B : Fin TFin T) (W : Fin T) :

                                                                                                                                          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
                                                                                                                                          Instances For
                                                                                                                                            noncomputable def Graphon.Lovasz.orbitIndicator {T K : } (B : Fin TFin T) (W : Fin T) (ξ : Fin KFin T) :
                                                                                                                                            (Fin KFin T)

                                                                                                                                            Orbit indicator of a K-tuple ξ.

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

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              theorem Graphon.Lovasz.orbitIndicator_orbit_invariant {T K : } (B : Fin TFin T) (W : Fin T) {ξ ξ_alt : Fin KFin T} (h : tupleOrbitRel B W ξ ξ_alt) :
                                                                                                                                              orbitIndicator B W ξ = orbitIndicator B W ξ_alt

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

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

                                                                                                                                              theorem Graphon.Lovasz.orbitIndicator_self {T K : } (B : Fin TFin T) (W : Fin T) (ξ : Fin KFin T) :
                                                                                                                                              orbitIndicator B W ξ ξ = 1

                                                                                                                                              orbitIndicator ξ ξ = 1 (reflexivity).

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

                                                                                                                                              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 degreeKNOWN-FALSE / OFF-AXIS (refuted 2026-05-14 by C₅ ⊔ C₆ counterexample at K=1).

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

                                                                                                                                              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.

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

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

                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                def Graphon.Lovasz.sameTupleEdgeProfile {T K : } (B : Fin TFin T) (ξ ξ' : Fin KFin T) :

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

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  def Graphon.Lovasz.sameTupleDegreeProfile {T K : } (B : Fin TFin T) (W : Fin T) (ξ ξ' : Fin KFin T) :

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

                                                                                                                                                  Equations
                                                                                                                                                  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.

                                                                                                                                                    def Graphon.Lovasz.vertexOrbitRel {T : } (B : Fin TFin T) (W : Fin T) (i j : Fin T) :

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

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      noncomputable def Graphon.Lovasz.rootedProfile {T n : } (B : Fin TFin T) (W : Fin T) (i : Fin T) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] :

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

                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        def Graphon.Lovasz.rootedProfileEquiv {T : } (B : Fin TFin T) (W : Fin T) (i j : Fin T) :

                                                                                                                                                        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
                                                                                                                                                        Instances For
                                                                                                                                                          theorem Graphon.Lovasz.rootedProfileEquiv_of_vertexOrbitRel {T : } (B : Fin TFin T) (W : Fin T) {i j : Fin T} (h : vertexOrbitRel B W i j) :

                                                                                                                                                          Forward direction (trivial): vertex orbit ⟹ rooted-profile equivalence. Follows from automorphism invariance of simpleEvalAt.

                                                                                                                                                          noncomputable def Graphon.Lovasz.rootedOrbitIndicator {T : } (B : Fin TFin T) (W : Fin T) (i : Fin T) :
                                                                                                                                                          Fin T

                                                                                                                                                          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
                                                                                                                                                          Instances For
                                                                                                                                                            noncomputable def Graphon.Lovasz.rootedProfileFun {T n : } (B : Fin TFin T) (W : Fin T) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] :
                                                                                                                                                            Fin T

                                                                                                                                                            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
                                                                                                                                                            Instances For

                                                                                                                                                              Algebra of rooted simple-graph profiles (K=1 rank theorem) #

                                                                                                                                                              def Graphon.Lovasz.InRootedProfileSpan {T : } (B : Fin TFin T) (W f : Fin T) :

                                                                                                                                                              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
                                                                                                                                                                theorem Graphon.Lovasz.InRootedProfileSpan.of_profile {T n : } (B : Fin TFin T) (W : Fin T) (F : SimpleGraph (Fin (n + 1))) [hF : DecidableRel F.Adj] :

                                                                                                                                                                The rooted profile of a single graph is in the span (singleton sum).

                                                                                                                                                                theorem Graphon.Lovasz.InRootedProfileSpan.zero {T : } (B : Fin TFin T) (W : Fin T) :
                                                                                                                                                                InRootedProfileSpan B W fun (x : Fin T) => 0

                                                                                                                                                                Zero function is in the span (empty sum).

                                                                                                                                                                theorem Graphon.Lovasz.InRootedProfileSpan.add {T : } {B : Fin TFin T} {W f₁ f₂ : Fin T} (h₁ : InRootedProfileSpan B W f₁) (h₂ : InRootedProfileSpan B W f₂) :
                                                                                                                                                                InRootedProfileSpan B W (f₁ + f₂)

                                                                                                                                                                Closure under addition.

                                                                                                                                                                theorem Graphon.Lovasz.InRootedProfileSpan.smul {T : } {B : Fin TFin T} {W : Fin T} (c : ) {f : Fin T} (h : InRootedProfileSpan B W f) :
                                                                                                                                                                InRootedProfileSpan B W fun (v : Fin T) => c * f v

                                                                                                                                                                Closure under scalar multiplication.

                                                                                                                                                                theorem Graphon.Lovasz.rootedProfileFun_bot {T : } (B : Fin TFin T) (W : Fin T) :
                                                                                                                                                                rootedProfileFun B W = fun (x : Fin T) => 1

                                                                                                                                                                The empty graph on Fin 1 has rooted profile equal to 1 at every vertex.

                                                                                                                                                                theorem Graphon.Lovasz.InRootedProfileSpan.one {T : } (B : Fin TFin T) (W : Fin T) :
                                                                                                                                                                InRootedProfileSpan B W fun (x : Fin T) => 1

                                                                                                                                                                Constant function 1 is in the rooted-profile span (via the empty graph).

                                                                                                                                                                theorem Graphon.Lovasz.InRootedProfileSpan.const {T : } (B : Fin TFin T) (W : Fin T) (c : ) :
                                                                                                                                                                InRootedProfileSpan B W fun (x : Fin T) => c

                                                                                                                                                                Constant function c is in the rooted-profile span.

                                                                                                                                                                def Graphon.Lovasz.rootedProductEmb₁ (n₁ n₂ : ) :
                                                                                                                                                                Fin (n₁ + 1) Fin (n₁ + n₂ + 1)

                                                                                                                                                                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
                                                                                                                                                                  def Graphon.Lovasz.rootedProductEmb₂ (n₁ n₂ : ) :
                                                                                                                                                                  Fin (n₂ + 1) Fin (n₁ + n₂ + 1)

                                                                                                                                                                  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
                                                                                                                                                                    noncomputable def Graphon.Lovasz.rootedProduct {n₁ n₂ : } (F₁ : SimpleGraph (Fin (n₁ + 1))) (F₂ : SimpleGraph (Fin (n₂ + 1))) :
                                                                                                                                                                    SimpleGraph (Fin (n₁ + n₂ + 1))
                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For

                                                                                                                                                                      Exact-shape application lemmas for the rooted-product embeddings. These unfold the where-defined toFun directly, so rfl works.

                                                                                                                                                                      @[simp]
                                                                                                                                                                      theorem Graphon.Lovasz.rootedProductEmb₁_val {n₁ n₂ : } (v : Fin (n₁ + 1)) :
                                                                                                                                                                      ((rootedProductEmb₁ n₁ n₂) v) = v
                                                                                                                                                                      @[simp]
                                                                                                                                                                      theorem Graphon.Lovasz.rootedProductEmb₂_val_zero {n₁ n₂ : } (v : Fin (n₂ + 1)) (h : v = 0) :
                                                                                                                                                                      ((rootedProductEmb₂ n₁ n₂) v) = 0
                                                                                                                                                                      @[simp]
                                                                                                                                                                      theorem Graphon.Lovasz.rootedProductEmb₂_val_pos {n₁ n₂ : } (v : Fin (n₂ + 1)) (h : v 0) :
                                                                                                                                                                      ((rootedProductEmb₂ n₁ n₂) v) = v + n₁

                                                                                                                                                                      Disjointness helpers between the two embedding images.

                                                                                                                                                                      theorem Graphon.Lovasz.rootedProductEmb₁_val_le {n₁ n₂ : } (v : Fin (n₁ + 1)) :
                                                                                                                                                                      ((rootedProductEmb₁ n₁ n₂) v) n₁

                                                                                                                                                                      rootedProductEmb₁ image vertices have val ≤ n₁.

                                                                                                                                                                      theorem Graphon.Lovasz.rootedProductEmb₂_val_alt {n₁ n₂ : } (v : Fin (n₂ + 1)) :
                                                                                                                                                                      ((rootedProductEmb₂ n₁ n₂) v) = 0 ((rootedProductEmb₂ n₁ n₂) v) n₁ + 1

                                                                                                                                                                      rootedProductEmb₂ image vertices have val = 0 or val ≥ n₁ + 1.

                                                                                                                                                                      theorem Graphon.Lovasz.rootedProductEmb₁_eq_iff {n₁ n₂ : } (v : Fin (n₁ + 1)) (w : Fin (n₁ + n₂ + 1)) :
                                                                                                                                                                      (rootedProductEmb₁ n₁ n₂) v = w v = w

                                                                                                                                                                      Image of rootedProductEmb₁ is exactly the vertices with val ≤ n₁.

                                                                                                                                                                      theorem Graphon.Lovasz.rootedProductEmb₂_eq_root_iff {n₁ n₂ : } (v : Fin (n₂ + 1)) (h : v = 0) (w : Fin (n₁ + n₂ + 1)) :
                                                                                                                                                                      (rootedProductEmb₂ n₁ n₂) v = w w = 0

                                                                                                                                                                      Image of rootedProductEmb₂ at root (v.val = 0) is the root in big graph.

                                                                                                                                                                      theorem Graphon.Lovasz.rootedProductEmb₂_eq_unlabeled_iff {n₁ n₂ : } (v : Fin (n₂ + 1)) (h : v 0) (w : Fin (n₁ + n₂ + 1)) :
                                                                                                                                                                      (rootedProductEmb₂ n₁ n₂) v = w w = v + n₁

                                                                                                                                                                      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.

                                                                                                                                                                      theorem Graphon.Lovasz.simpleEvalAt_rootedProduct {T n₁ n₂ : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (F₁ : SimpleGraph (Fin (n₁ + 1))) [DecidableRel F₁.Adj] (F₂ : SimpleGraph (Fin (n₂ + 1))) [DecidableRel F₂.Adj] (v : Fin T) :
                                                                                                                                                                      rootedProfile B W v (rootedProduct F₁ F₂) = rootedProfile B W v F₁ * rootedProfile B W v F₂
                                                                                                                                                                      theorem Graphon.Lovasz.InRootedProfileSpan.mul {T : } {B : Fin TFin T} (hB : ∀ (i j : Fin T), B i j = B j i) {W f₁ f₂ : Fin T} (h₁ : InRootedProfileSpan B W f₁) (h₂ : InRootedProfileSpan B W f₂) :
                                                                                                                                                                      InRootedProfileSpan B W fun (v : Fin T) => f₁ v * f₂ v

                                                                                                                                                                      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) #

                                                                                                                                                                      theorem Graphon.Lovasz.InRootedProfileSpan.const_on_rpe {T : } {B : Fin TFin T} {W f : Fin T} (h : InRootedProfileSpan B W f) {i j : Fin T} (hij : rootedProfileEquiv B W i j) :
                                                                                                                                                                      f i = f j

                                                                                                                                                                      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.

                                                                                                                                                                      theorem Graphon.Lovasz.rootedOrbitIndicator_const_on_orbit {T : } (B : Fin TFin T) (W : Fin T) (i a b : Fin T) :

                                                                                                                                                                      Orbit indicators are constant on orbit classes (trivial, since the indicator value depends only on the orbit of v).

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

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

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

                                                                                                                                                                      Status (2026-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.

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

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

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

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

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

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

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

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

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

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

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

                                                                                                                                                                      Proved as a contradiction proof from orbit_separation_by_simple_graph (the contrapositive form — formerly the canonical sorry, since proved).

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

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

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

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

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

                                                                                                                                                                      Steps in the inductive case m = k + 1:

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

                                                                                                                                                                      Status (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, so B(t, t) terms never appear in simple-graph evaluations. Cannot be extracted directly.
                                                                                                                                                                      • W-preservation pointwise W(χ i) = W(i): single-unlabeled- vertex graphs evaluate to ∑_t W(t), ξ-independent. Row-sum graphs give scalar equations ∑_t W(t) B(i, t) = ∑_t W(t) B(χ i, t), not pointwise W.

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

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

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

                                                                                                                                                                      §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.

                                                                                                                                                                      def Graphon.Lovasz.InTupleSimpleEvalSpan {T K : } (B : Fin TFin T) (W : Fin T) (f : (Fin KFin T)) :

                                                                                                                                                                      Membership predicate for the K-tuple simple-eval ℝ-span.

                                                                                                                                                                      Equations
                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                      Instances For
                                                                                                                                                                        theorem Graphon.Lovasz.InTupleSimpleEvalSpan.of_simple {T K n : } (B : Fin TFin T) (W : Fin T) (F : SimpleGraph (Fin (n + K))) [hF : DecidableRel F.Adj] :
                                                                                                                                                                        InTupleSimpleEvalSpan B W fun (ξ : Fin KFin T) => simpleEvalAt B W F ξ

                                                                                                                                                                        Simple-graph evaluation lies in the span (singleton sum).

                                                                                                                                                                        theorem Graphon.Lovasz.InTupleSimpleEvalSpan.zero {T K : } (B : Fin TFin T) (W : Fin T) :
                                                                                                                                                                        InTupleSimpleEvalSpan B W fun (x : Fin KFin T) => 0

                                                                                                                                                                        Zero is in the span (empty sum).

                                                                                                                                                                        theorem Graphon.Lovasz.InTupleSimpleEvalSpan.add {T K : } {B : Fin TFin T} {W : Fin T} {f₁ f₂ : (Fin KFin T)} (h₁ : InTupleSimpleEvalSpan B W f₁) (h₂ : InTupleSimpleEvalSpan B W f₂) :
                                                                                                                                                                        InTupleSimpleEvalSpan B W (f₁ + f₂)

                                                                                                                                                                        Closure under addition. Mirrors InRootedProfileSpan.add (K=1): re-index via Sum to sidestep Fin.addCases motive issues.

                                                                                                                                                                        theorem Graphon.Lovasz.InTupleSimpleEvalSpan.one {T K : } (B : Fin TFin T) (W : Fin T) :
                                                                                                                                                                        InTupleSimpleEvalSpan B W fun (x : Fin KFin T) => 1

                                                                                                                                                                        Constant function 1 is in the span.

                                                                                                                                                                        The empty simple graph (n = 0, no edges) on Fin (0 + K) evaluates to 1 via simpleEvalAt_bot_zero.

                                                                                                                                                                        theorem Graphon.Lovasz.InTupleSimpleEvalSpan.const {T K : } (B : Fin TFin T) (W : Fin T) (c : ) :
                                                                                                                                                                        InTupleSimpleEvalSpan B W fun (x : Fin KFin T) => c

                                                                                                                                                                        Constant function c is in the span.

                                                                                                                                                                        Direct construction (avoids forward ref to .smul): use a single empty-graph term with coefficient c.

                                                                                                                                                                        theorem Graphon.Lovasz.InTupleSimpleEvalSpan.smul {T K : } {B : Fin TFin T} {W : Fin T} (c : ) {f : (Fin KFin T)} (h : InTupleSimpleEvalSpan B W f) :
                                                                                                                                                                        InTupleSimpleEvalSpan B W fun (ξ : Fin KFin T) => c * f ξ

                                                                                                                                                                        Closure under scalar multiplication.

                                                                                                                                                                        theorem Graphon.Lovasz.InTupleSimpleEvalSpan.finset_sum {T K : } {B : Fin TFin T} {W : Fin T} {ι : Type u_1} (s : Finset ι) (g : ι(Fin KFin T)) (hg : is, InTupleSimpleEvalSpan B W (g i)) :
                                                                                                                                                                        InTupleSimpleEvalSpan B W fun (ξ : Fin KFin T) => is, g i ξ

                                                                                                                                                                        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).

                                                                                                                                                                        def Graphon.Lovasz.InTupleMultiEvalSpan {T K : } (B : Fin TFin T) (W : Fin T) (f : (Fin KFin T)) :

                                                                                                                                                                        Membership predicate for the K-tuple multigraph-eval ℝ-span.

                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For
                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.of_multi {T K n : } (B : Fin TFin T) (W : Fin T) (M : MultiLabeledGraph K n) :
                                                                                                                                                                          InTupleMultiEvalSpan B W fun (ξ : Fin KFin T) => multiLabeledEvalK K n M B W ξ

                                                                                                                                                                          Multigraph evaluation lies in the span (singleton sum).

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.zero {T K : } (B : Fin TFin T) (W : Fin T) :
                                                                                                                                                                          InTupleMultiEvalSpan B W fun (x : Fin KFin T) => 0

                                                                                                                                                                          Zero is in the span (empty sum).

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.add {T K : } {B : Fin TFin T} {W : Fin T} {f₁ f₂ : (Fin KFin T)} (h₁ : InTupleMultiEvalSpan B W f₁) (h₂ : InTupleMultiEvalSpan B W f₂) :
                                                                                                                                                                          InTupleMultiEvalSpan B W (f₁ + f₂)

                                                                                                                                                                          Closure under addition. Mirrors InTupleSimpleEvalSpan.add: re-index via Sum to sidestep Fin.addCases motive issues.

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.one {T K : } (B : Fin TFin T) (W : Fin T) :
                                                                                                                                                                          InTupleMultiEvalSpan B W fun (x : Fin KFin T) => 1

                                                                                                                                                                          Constant function 1 is in the span (empty multigraph at n = 0).

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.const {T K : } (B : Fin TFin T) (W : Fin T) (c : ) :
                                                                                                                                                                          InTupleMultiEvalSpan B W fun (x : Fin KFin T) => c

                                                                                                                                                                          Constant function c is in the span.

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.smul {T K : } {B : Fin TFin T} {W : Fin T} (c : ) {f : (Fin KFin T)} (h : InTupleMultiEvalSpan B W f) :
                                                                                                                                                                          InTupleMultiEvalSpan B W fun (ξ : Fin KFin T) => c * f ξ

                                                                                                                                                                          Closure under scalar multiplication.

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.finset_sum {T K : } {B : Fin TFin T} {W : Fin T} {ι : Type u_1} (s : Finset ι) (g : ι(Fin KFin T)) (hg : is, InTupleMultiEvalSpan B W (g i)) :
                                                                                                                                                                          InTupleMultiEvalSpan B W fun (ξ : Fin KFin T) => is, g i ξ

                                                                                                                                                                          Finset sum closure: sums of in-span functions are in-span.

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.mul {T K : } {B : Fin TFin T} (hB : ∀ (i j : Fin T), B i j = B j i) {W : Fin T} {f₁ f₂ : (Fin KFin T)} (h₁ : InTupleMultiEvalSpan B W f₁) (h₂ : InTupleMultiEvalSpan B W f₂) :
                                                                                                                                                                          InTupleMultiEvalSpan B W fun (ξ : Fin KFin T) => f₁ ξ * f₂ ξ

                                                                                                                                                                          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.

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleSimpleEvalSpan.toMulti {T K : } {B : Fin TFin T} {W : Fin T} {f : (Fin KFin T)} (h : InTupleSimpleEvalSpan B W f) :

                                                                                                                                                                          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.

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.aut_invariant {T K : } (B : Fin TFin T) (W : Fin T) {f : (Fin KFin T)} (h : InTupleMultiEvalSpan B W f) (σ : Equiv.Perm (Fin T)) ( : IsWeightedAutomorphism B W σ) (ξ : Fin KFin T) :
                                                                                                                                                                          f (σ ξ) = f ξ

                                                                                                                                                                          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).

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.finset_prod {T K : } {B : Fin TFin T} (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {ι : Type u_1} (s : Finset ι) (g : ι(Fin KFin T)) (hg : is, InTupleMultiEvalSpan B W (g i)) :
                                                                                                                                                                          InTupleMultiEvalSpan B W fun (ξ : Fin KFin T) => is, g i ξ

                                                                                                                                                                          Finset product closure (needs symmetric B because it uses .mul). Mirrors InRootedProfileSpan.finset_prod.

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.eval_sub_const {T K n : } (B : Fin TFin T) (W : Fin T) (M : MultiLabeledGraph K n) (w : ) :
                                                                                                                                                                          InTupleMultiEvalSpan B W fun (ζ : Fin KFin T) => multiLabeledEvalK K n M B W ζ - w

                                                                                                                                                                          multiLabeledEvalK M · - w is in the span. Mirrors profile_sub_const.

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.lagrange_factor {T K n : } (B : Fin TFin T) (W : Fin T) (M : MultiLabeledGraph K n) (ξ η : Fin KFin T) :
                                                                                                                                                                          InTupleMultiEvalSpan B W fun (ζ : Fin KFin T) => (multiLabeledEvalK K n M B W ζ - multiLabeledEvalK K n M B W η) / (multiLabeledEvalK K n M B W ξ - multiLabeledEvalK K n M B W η)

                                                                                                                                                                          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.

                                                                                                                                                                          theorem Graphon.Lovasz.InTupleMultiEvalSpan.descends {T K : } {B : Fin TFin T} {W : Fin T} {f : (Fin KFin T)} (hf : InTupleMultiEvalSpan B W f) {ξ ξ' : Fin KFin T} ( : tupleEquivMulti B W ξ ξ') :
                                                                                                                                                                          f ξ = f ξ'

                                                                                                                                                                          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.

                                                                                                                                                                          theorem Graphon.Lovasz.exists_sep_of_not_tupleEquivMulti {T K : } {B : Fin TFin T} {W : Fin T} {η μ : Fin KFin T} (h : ¬tupleEquivMulti B W η μ) :
                                                                                                                                                                          ∃ (n : ) (M : MultiLabeledGraph K n), multiLabeledEvalK K n M B W η multiLabeledEvalK K n M B W μ

                                                                                                                                                                          From non-equivalence, extract a separating multigraph. Definitional (¬ tupleEquivMulti literally negates "all evals agree"), hence non-cyclic — does NOT invoke multiEval_separates_orbits.

                                                                                                                                                                          noncomputable def Graphon.Lovasz.tupleEquivMultiIndicator {T K : } (B : Fin TFin T) (W : Fin T) (μ : Fin KFin T) :
                                                                                                                                                                          (Fin KFin T)

                                                                                                                                                                          tupleEquivMulti-class indicator of μ: 1 on μ's equivalence class, 0 elsewhere.

                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            theorem Graphon.Lovasz.tupleEquivMultiIndicator_nonneg {T K : } (B : Fin TFin T) (W : Fin T) (μ η : Fin KFin T) :

                                                                                                                                                                            The class indicator is nonnegative (it is 0/1-valued). Needed for Phase-5 trace positivity.

                                                                                                                                                                            theorem Graphon.Lovasz.tupleEquivMultiClassIndicator_mem_multiSpan {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (μ : Fin KFin T) :

                                                                                                                                                                            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.

                                                                                                                                                                            noncomputable def Graphon.Lovasz.traceLastTupleFun {T K : } (W : Fin T) (f : (Fin (K + 1)Fin T)) :
                                                                                                                                                                            (Fin KFin T)

                                                                                                                                                                            Trace operator on functions: sum out the last label with W-weight. The function-level analog of MultiLabeledGraph.trace / Lovász's tr.

                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              theorem Graphon.Lovasz.InTupleMultiEvalSpan.traceLast {T K : } {B : Fin TFin T} (hB : ∀ (i j : Fin T), B i j = B j i) {W : Fin T} {f : (Fin (K + 1)Fin T)} (hf : InTupleMultiEvalSpan B W f) :

                                                                                                                                                                              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.

                                                                                                                                                                              theorem Graphon.Lovasz.tupleEquivMulti_refl {T K : } (B : Fin TFin T) (W : Fin T) (ξ : Fin KFin T) :
                                                                                                                                                                              tupleEquivMulti B W ξ ξ

                                                                                                                                                                              tupleEquivMulti is reflexive.

                                                                                                                                                                              theorem Graphon.Lovasz.tupleEquivMulti_symm {T K : } {B : Fin TFin T} {W : Fin T} {ξ ξ' : Fin KFin T} (h : tupleEquivMulti B W ξ ξ') :
                                                                                                                                                                              tupleEquivMulti B W ξ' ξ

                                                                                                                                                                              tupleEquivMulti is symmetric.

                                                                                                                                                                              theorem Graphon.Lovasz.tupleEquivMulti_extend_one {T k : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) {ξ ξ' : Fin kFin T} (h : tupleEquivMulti B W ξ ξ') (μ : Fin (k + 1)Fin T) ( : restrictTuple μ = ξ) :
                                                                                                                                                                              ∃ (ν : Fin (k + 1)Fin T), restrictTuple ν = ξ' tupleEquivMulti B W μ ν

                                                                                                                                                                              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₁) #

                                                                                                                                                                              def Graphon.Lovasz.insLabelEmb (K n : ) :
                                                                                                                                                                              Fin (n + K) Fin (n + (K + 1))

                                                                                                                                                                              Embed Fin (n+K) ↪ Fin (n+(K+1)) skipping index K (labels <K fixed, unlabeled ≥K shifted up one), making index K a fresh isolated label.

                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                def Graphon.Lovasz.unInsLabel (K n : ) (w : Fin (n + (K + 1))) :
                                                                                                                                                                                Option (Fin (n + K))

                                                                                                                                                                                Partial inverse of insLabelEmb: none exactly at the new label ⟨K⟩.

                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  theorem Graphon.Lovasz.unInsLabel_insLabelEmb (K n : ) (v : Fin (n + K)) :
                                                                                                                                                                                  unInsLabel K n ((insLabelEmb K n) v) = some v
                                                                                                                                                                                  theorem Graphon.Lovasz.insLabelEmb_eq_of_unInsLabel (K n : ) {w : Fin (n + (K + 1))} {u : Fin (n + K)} (h : unInsLabel K n w = some u) :
                                                                                                                                                                                  w = (insLabelEmb K n) u

                                                                                                                                                                                  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
                                                                                                                                                                                    theorem Graphon.Lovasz.addIsoLabel_mult_map_emb {K n : } (M : MultiLabeledGraph K n) (e' : Sym2 (Fin (n + K))) :
                                                                                                                                                                                    M.addIsoLabel.mult (Sym2.map (⇑(insLabelEmb K n)) e') = M.mult e'
                                                                                                                                                                                    theorem Graphon.Lovasz.multiLabeledEvalK_addIsoLabel {T K n : } (M : MultiLabeledGraph K n) (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (ζ : Fin (K + 1)Fin T) :

                                                                                                                                                                                    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).

                                                                                                                                                                                    theorem Graphon.Lovasz.tupleEquivMulti_restrict {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {ξ ξ' : Fin (K + 1)Fin T} (h : tupleEquivMulti B W ξ ξ') :

                                                                                                                                                                                    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.

                                                                                                                                                                                    theorem Graphon.Lovasz.tupleEquivMulti_id_preserves_B {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {χ : Fin TFin T} (h : tupleEquivMulti B W (fun (i : Fin T) => i) χ) (a b : Fin T) :
                                                                                                                                                                                    a bB (χ a) (χ b) = B a b

                                                                                                                                                                                    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 #

                                                                                                                                                                                    def Graphon.Lovasz.restrictAlongEmb {k l : } (e : Fin k Fin l) (n : ) :
                                                                                                                                                                                    Fin (n + k) Fin (n + l)

                                                                                                                                                                                    Embed Fin (n+k) ↪ Fin (n+l) along a label injection e : Fin k ↪ Fin l: labels i < k map to label e i; unlabeled vertices shift from [k, k+n) to [l, l+n).

                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      noncomputable def Graphon.Lovasz.unembAlong {k l : } (e : Fin k Fin l) (n : ) (w : Fin (n + l)) :
                                                                                                                                                                                      Option (Fin (n + k))

                                                                                                                                                                                      Partial inverse of restrictAlongEmb: none on labels outside range e (the isolated labels).

                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        theorem Graphon.Lovasz.restrictAlongEmb_val_lt {k l : } (e : Fin k Fin l) (n : ) (v : Fin (n + k)) (hv : v < k) :
                                                                                                                                                                                        ((restrictAlongEmb e n) v) = (e v, hv)
                                                                                                                                                                                        theorem Graphon.Lovasz.restrictAlongEmb_val_ge {k l : } (e : Fin k Fin l) (n : ) (v : Fin (n + k)) (hv : ¬v < k) :
                                                                                                                                                                                        ((restrictAlongEmb e n) v) = l + (v - k)
                                                                                                                                                                                        theorem Graphon.Lovasz.unembAlong_restrictAlongEmb {k l : } (e : Fin k Fin l) (n : ) (v : Fin (n + k)) :
                                                                                                                                                                                        theorem Graphon.Lovasz.restrictAlongEmb_eq_of_unembAlong {k l n : } (e : Fin k Fin l) {w : Fin (n + l)} {u : Fin (n + k)} (h : unembAlong e n w = some u) :

                                                                                                                                                                                        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
                                                                                                                                                                                          theorem Graphon.Lovasz.multiTau_restrictAlongEmb {T k l n : } (e : Fin k Fin l) (ζ : Fin lFin T) (σ : Fin nFin T) (v : Fin (n + k)) :
                                                                                                                                                                                          multiTau l n ζ σ ((restrictAlongEmb e n) v) = multiTau k n (ζ e) σ v
                                                                                                                                                                                          theorem Graphon.Lovasz.multiLabeledEvalK_restrictAlong {T k l n : } (e : Fin k Fin l) (M : MultiLabeledGraph k n) (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (ζ : Fin lFin T) :
                                                                                                                                                                                          theorem Graphon.Lovasz.tupleEquivMulti_restrict_along {T k l : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (e : Fin k Fin l) {ξ ξ' : Fin lFin T} (h : tupleEquivMulti B W ξ ξ') :
                                                                                                                                                                                          tupleEquivMulti B W (ξ e) (ξ' e)

                                                                                                                                                                                          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.

                                                                                                                                                                                          theorem Graphon.Lovasz.weighted_powersum_determines_measure {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x y W : ι) (hmom : ∀ (k : ), i : ι, W i * x i ^ k = i : ι, W i * y i ^ k) (a : ) :
                                                                                                                                                                                          i : ι with x i = a, W i = i : ι with y i = a, W i

                                                                                                                                                                                          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.

                                                                                                                                                                                          theorem Graphon.Lovasz.weighted_powersum_zero_imp_fiber_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (z g : ι) (hz : ∀ (k : ), i : ι, g i * z i ^ k = 0) (a : ) :
                                                                                                                                                                                          i : ι with z i = a, g i = 0

                                                                                                                                                                                          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.)

                                                                                                                                                                                          theorem Graphon.Lovasz.tupleEquivMulti_k1_powersum_eq {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {i j : Fin T} (h : tupleEquivMulti B W (fun (x : Fin 1) => i) fun (x : Fin 1) => j) (a : ) :
                                                                                                                                                                                          t : Fin T, W t * B i t ^ a = t : Fin T, W t * B j t ^ a

                                                                                                                                                                                          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).

                                                                                                                                                                                          theorem Graphon.Lovasz.tupleEquivMulti_k1_rowMeasure_eq {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {i j : Fin T} (h : tupleEquivMulti B W (fun (x : Fin 1) => i) fun (x : Fin 1) => j) (v : ) :
                                                                                                                                                                                          t : Fin T with B i t = v, W t = t : Fin T with B j t = v, W t

                                                                                                                                                                                          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
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem Graphon.Lovasz.twoLeafProbe_mult {a b : } (e : Sym2 (Fin (1 + 2))) :
                                                                                                                                                                                            (twoLeafProbe a b).mult e = if e = s(0, 2) then a else if e = s(1, 2) then b else 0
                                                                                                                                                                                            theorem Graphon.Lovasz.multiLabeledEvalK_twoLeafProbe {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (φ : Fin 2Fin T) (a b : ) :
                                                                                                                                                                                            multiLabeledEvalK 2 1 (twoLeafProbe a b) B W φ = t : Fin T, W t * (B (φ 0) t ^ a * B (φ 1) t ^ b)

                                                                                                                                                                                            Two-leaf-probe evaluation: reads the joint moment ∑ₜ W t · B (φ 0) t ^ a · B (φ 1) t ^ b.

                                                                                                                                                                                            theorem Graphon.Lovasz.tupleEquivMulti_preserves_diagonal_of_k1 {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {i j : Fin T} (h : tupleEquivMulti B W (fun (x : Fin 1) => i) fun (x : Fin 1) => j) :
                                                                                                                                                                                            B i i = B j j

                                                                                                                                                                                            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.

                                                                                                                                                                                            theorem Graphon.Lovasz.tupleEquivMulti_preserves_diagonal {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {ξ ξ' : Fin KFin T} (h : tupleEquivMulti B W ξ ξ') (c : Fin K) :
                                                                                                                                                                                            B (ξ c) (ξ c) = B (ξ' c) (ξ' c)

                                                                                                                                                                                            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).

                                                                                                                                                                                            theorem Graphon.Lovasz.tupleEquivMulti_id_preserves_B_full {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {χ : Fin TFin T} (h : tupleEquivMulti B W (fun (i : Fin T) => i) χ) (i j : Fin T) :
                                                                                                                                                                                            B (χ i) (χ j) = B i j

                                                                                                                                                                                            Full B-preservation for the bijective case = off-diagonal (proved) + diagonal (residue).

                                                                                                                                                                                            theorem Graphon.Lovasz.tupleEquivMulti_id_bijective {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {χ : Fin TFin T} (h : tupleEquivMulti B W (fun (i : Fin T) => i) χ) :

                                                                                                                                                                                            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
                                                                                                                                                                                              theorem Graphon.Lovasz.liftLabelPerm_apply_of_lt {K n : } (ρ : Equiv.Perm (Fin K)) (v : Fin (n + K)) (h : v < K) :
                                                                                                                                                                                              (liftLabelPerm ρ) v = (ρ v, h),
                                                                                                                                                                                              theorem Graphon.Lovasz.liftLabelPerm_apply_of_ge {K n : } (ρ : Equiv.Perm (Fin K)) (v : Fin (n + K)) (h : ¬v < K) :
                                                                                                                                                                                              (liftLabelPerm ρ) v = v
                                                                                                                                                                                              theorem Graphon.Lovasz.multiTau_liftLabelPerm {T K n : } (ρ : Equiv.Perm (Fin K)) (ζ : Fin KFin T) (σ : Fin nFin T) (v : Fin (n + K)) :
                                                                                                                                                                                              multiTau K n ζ σ ((liftLabelPerm ρ) v) = multiTau K n (ζ ρ) σ v

                                                                                                                                                                                              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
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                theorem Graphon.Lovasz.multiLabeledEvalK_relabel {T K n : } (ρ : Equiv.Perm (Fin K)) (M : MultiLabeledGraph K n) (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (ζ : Fin KFin T) :
                                                                                                                                                                                                multiLabeledEvalK K n M B W (ζ ρ) = multiLabeledEvalK K n (MultiLabeledGraph.relabel ρ M) B W ζ
                                                                                                                                                                                                theorem Graphon.Lovasz.tupleEquivMulti_relabel {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) {ξ ξ' : Fin KFin T} (h : tupleEquivMulti B W ξ ξ') (ρ : Equiv.Perm (Fin K)) :
                                                                                                                                                                                                tupleEquivMulti B W (ξ ρ) (ξ' ρ)

                                                                                                                                                                                                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 #

                                                                                                                                                                                                theorem Graphon.Lovasz.snoc_restrict_eq_of_bijective {S : } {ζ : Fin (S + 1)Fin (S + 1)} {t : Fin (S + 1)} ( : Function.Bijective ζ) (hsnoc : Function.Bijective (Fin.snoc (ζ Fin.castSucc) t)) :
                                                                                                                                                                                                t = ζ (Fin.last S)

                                                                                                                                                                                                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).

                                                                                                                                                                                                theorem Graphon.Lovasz.tupleEquivMulti_bijective_of_equiv {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {η ξ : Fin TFin T} (h : tupleEquivMulti B W η ξ) ( : Function.Bijective ξ) :

                                                                                                                                                                                                Equivalence transfers bijectivity: if η ~ ξ and ξ is bijective, so is η. Proof: relabel both sides by ξ⁻¹ so the RHS becomes id, then apply tupleEquivMulti_id_bijective.

                                                                                                                                                                                                theorem Graphon.Lovasz.tupleEquivMulti_traceLast_collapse {S : } (B : Fin (S + 1)Fin (S + 1)) (hB : ∀ (i j : Fin (S + 1)), B i j = B j i) (W : Fin (S + 1)) (hW : ∀ (i : Fin (S + 1)), 0 < W i) (htwin : ∀ (i j : Fin (S + 1)), i jB i B j) {ξ ζ : Fin (S + 1)Fin (S + 1)} ( : Function.Bijective ξ) (hζbij : Function.Bijective ζ) (hζξ : tupleEquivMulti B W ζ ξ) :

                                                                                                                                                                                                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).

                                                                                                                                                                                                theorem Graphon.Lovasz.tupleEquivMulti_bijective_preserves_W_last {S : } (B : Fin (S + 1)Fin (S + 1)) (hB : ∀ (i j : Fin (S + 1)), B i j = B j i) (W : Fin (S + 1)) (hW : ∀ (i : Fin (S + 1)), 0 < W i) (htwin : ∀ (i j : Fin (S + 1)), i jB i B j) {ξ ξ' : Fin (S + 1)Fin (S + 1)} (h : tupleEquivMulti B W ξ ξ') ( : Function.Bijective ξ) (hξ' : Function.Bijective ξ') :
                                                                                                                                                                                                W (ξ' (Fin.last S)) = W (ξ (Fin.last S))

                                                                                                                                                                                                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).

                                                                                                                                                                                                theorem Graphon.Lovasz.tupleEquivMulti_id_preserves_W {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {χ : Fin TFin T} (h : tupleEquivMulti B W (fun (i : Fin T) => i) χ) ( : Function.Bijective χ) (i : Fin T) :
                                                                                                                                                                                                W (χ i) = W i

                                                                                                                                                                                                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.

                                                                                                                                                                                                theorem Graphon.Lovasz.tupleEquivMulti_bijective_case {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {χ : Fin TFin T} (h : tupleEquivMulti B W (fun (i : Fin T) => i) χ) :
                                                                                                                                                                                                tupleOrbitRel B W (fun (i : Fin T) => i) χ

                                                                                                                                                                                                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.

                                                                                                                                                                                                theorem Graphon.Lovasz.tupleEquivMulti_surjective_case {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {ξ ξ' : Fin KFin T} (hξ_surj : Function.Surjective ξ) (h : tupleEquivMulti B W ξ ξ') :
                                                                                                                                                                                                tupleOrbitRel B W ξ ξ'

                                                                                                                                                                                                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).

                                                                                                                                                                                                theorem Graphon.Lovasz.tupleEquivMulti_implies_orbit {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {ξ ξ' : Fin KFin T} (h : tupleEquivMulti B W ξ ξ') :
                                                                                                                                                                                                tupleOrbitRel B W ξ ξ'

                                                                                                                                                                                                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.

                                                                                                                                                                                                theorem Graphon.Lovasz.multiEval_separates_orbits {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {ξ η : Fin KFin T} (h : ¬tupleOrbitRel B W ξ η) :
                                                                                                                                                                                                ∃ (n : ) (M : MultiLabeledGraph K n), multiLabeledEvalK K n M B W ξ multiLabeledEvalK K n M B W η

                                                                                                                                                                                                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.)

                                                                                                                                                                                                theorem Graphon.Lovasz.tupleOrbitIndicator_mem_multiEvalSpan {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ : Fin KFin T) :

                                                                                                                                                                                                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.

                                                                                                                                                                                                noncomputable def Graphon.Lovasz.multiLabeledTerm {T : } (K n : ) (M : MultiLabeledGraph K n) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) (σ : Fin nFin T) :

                                                                                                                                                                                                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
                                                                                                                                                                                                  theorem Graphon.Lovasz.multiLabeledEvalK_eq_sum_term {T K n : } (M : MultiLabeledGraph K n) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :
                                                                                                                                                                                                  multiLabeledEvalK K n M B W φ = σ : Fin nFin T, multiLabeledTerm K n M B W φ σ

                                                                                                                                                                                                  multiLabeledEvalK as the Finset.univ sum of multiLabeledTerm.

                                                                                                                                                                                                  noncomputable def Graphon.Lovasz.injMultiLabeledEvalK {T : } (K n : ) (M : MultiLabeledGraph K n) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :

                                                                                                                                                                                                  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
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    noncomputable def Graphon.Lovasz.wexpMultiLabeledEvalKLoop {T : } (K n : ) (M : MultiLabeledGraphLoop K n) (wexp : Fin n) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :

                                                                                                                                                                                                    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
                                                                                                                                                                                                      theorem Graphon.Lovasz.wexpMultiLabeledEvalKLoop_one {T K n : } (M : MultiLabeledGraphLoop K n) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :
                                                                                                                                                                                                      wexpMultiLabeledEvalKLoop K n M (fun (x : Fin n) => 1) B W φ = multiLabeledEvalKLoop K n M B W φ

                                                                                                                                                                                                      Sanity: the enriched evaluator with all exponents 1 recovers multiLabeledEvalKLoop.

                                                                                                                                                                                                      def Graphon.Lovasz.tupleEquivMultiInj {T K : } (B : Fin TFin T) (W : Fin T) (ξ ξ' : Fin KFin T) :

                                                                                                                                                                                                      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
                                                                                                                                                                                                        theorem Graphon.Lovasz.multiLabeledEvalK_eq_inj_add_nonInj {T K n : } (M : MultiLabeledGraph K n) (B : Fin TFin T) (W : Fin T) (φ : Fin KFin T) :
                                                                                                                                                                                                        multiLabeledEvalK K n M B W φ = injMultiLabeledEvalK K n M B W φ + σ : Fin nFin T with ¬Function.Injective σ, multiLabeledTerm K n M B W φ σ

                                                                                                                                                                                                        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 tupleEquivMultitupleEquivMultiInj 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).

                                                                                                                                                                                                        theorem Graphon.Lovasz.simpleEvalAt_aut_invariant {T K n : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (F : SimpleGraph (Fin (n + K))) [DecidableRel F.Adj] (σ : Equiv.Perm (Fin T)) (hσ_aut : IsWeightedAutomorphism B W σ) (ξ : Fin KFin T) :
                                                                                                                                                                                                        simpleEvalAt B W F (σ ξ) = simpleEvalAt B W F ξ

                                                                                                                                                                                                        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 Submodules. 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.

                                                                                                                                                                                                        noncomputable def Graphon.Lovasz.simpleEvalSubmodule {T : } (B : Fin TFin T) (W : Fin T) (K : ) :
                                                                                                                                                                                                        Submodule ((Fin KFin T))

                                                                                                                                                                                                        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
                                                                                                                                                                                                          noncomputable def Graphon.Lovasz.multiEvalSubmodule {T : } (B : Fin TFin T) (W : Fin T) (K : ) :
                                                                                                                                                                                                          Submodule ((Fin KFin T))

                                                                                                                                                                                                          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
                                                                                                                                                                                                            theorem Graphon.Lovasz.mem_simpleEvalSubmodule_iff {T K : } (B : Fin TFin T) (W : Fin T) (f : (Fin KFin T)) :

                                                                                                                                                                                                            Submodule membership coincides with the existing simple-eval span predicate InTupleSimpleEvalSpan.

                                                                                                                                                                                                            theorem Graphon.Lovasz.mem_multiEvalSubmodule_iff {T K : } (B : Fin TFin T) (W : Fin T) (f : (Fin KFin T)) :

                                                                                                                                                                                                            Submodule membership coincides with the existing multigraph-eval span predicate InTupleMultiEvalSpan.

                                                                                                                                                                                                            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.

                                                                                                                                                                                                            def Graphon.Lovasz.orbitInvariantSubmodule {T : } (B : Fin TFin T) (W : Fin T) (K : ) :
                                                                                                                                                                                                            Submodule ((Fin KFin T))

                                                                                                                                                                                                            The submodule of (B, W)-automorphism-invariant functions of a K-tuple.

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              theorem Graphon.Lovasz.tupleMultiEval_span_aut_invariant {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (f : (Fin KFin T)) (h_aut_inv : ∀ (σ : Equiv.Perm (Fin T)), IsWeightedAutomorphism B W σ∀ (ξ : Fin KFin T), f (σ ξ) = f ξ) :

                                                                                                                                                                                                              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.

                                                                                                                                                                                                              : multigraph evaluations are automorphism-invariant.

                                                                                                                                                                                                              theorem Graphon.Lovasz.orbitInvariantSubmodule_le_multiEvalSubmodule {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) :

                                                                                                                                                                                                              : every automorphism-invariant function lies in the multigraph-eval span (non-circular, via tupleMultiEval_span_aut_invariant).

                                                                                                                                                                                                              theorem Graphon.Lovasz.multiEvalSubmodule_eq_orbitInvariantSubmodule {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) :

                                                                                                                                                                                                              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.

                                                                                                                                                                                                              theorem Graphon.Lovasz.simpleEvalSubmodule_le_orbitInvariantSubmodule {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) :

                                                                                                                                                                                                              Easy inclusion simpleEvalSubmoduleorbitInvariantSubmodule: simple-graph evaluations are automorphism-invariant (simpleEvalAt_aut_invariant). Completes the clean frame simpleEvalSubmoduleorbitInvariantSubmodule = multiEvalSubmodule; the sole #70 residue is the reverse inclusion.

                                                                                                                                                                                                              Corollary simpleEvalSubmodulemultiEvalSubmodule (the never-in-doubt inclusion), directly via InTupleSimpleEvalSpan.toMulti.

                                                                                                                                                                                                              @[implicit_reducible]
                                                                                                                                                                                                              noncomputable instance Graphon.Lovasz.instFintypeOrbitClass {T K : } {B : Fin TFin T} {W : Fin T} :
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              noncomputable def Graphon.Lovasz.orbitInvariantToClassFun {T K : } (B : Fin TFin T) (W : Fin T) :

                                                                                                                                                                                                              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
                                                                                                                                                                                                                noncomputable def Graphon.Lovasz.orbitInvariantEquiv {T K : } (B : Fin TFin T) (W : Fin T) :

                                                                                                                                                                                                                Orbit-invariant functions ≅ functions on the orbit quotient.

                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                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).

                                                                                                                                                                                                                  theorem Graphon.Lovasz.eval_rep_annihilator_zero {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (c : OrbitClass T K B W) (hc : ∀ (n : ) (F : SimpleGraph (Fin (n + K))) (inst : DecidableRel F.Adj), q : OrbitClass T K B W, c q * simpleEvalAt B W F (Quotient.out q) = 0) :
                                                                                                                                                                                                                  c = 0

                                                                                                                                                                                                                  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).

                                                                                                                                                                                                                  noncomputable def Graphon.Lovasz.evalRepPairing {T K : } (B : Fin TFin T) (W : Fin T) :
                                                                                                                                                                                                                  (OrbitClass T K B W) →ₗ[] ((Fin KFin T)) →ₗ[]

                                                                                                                                                                                                                  The representative pairing ⟨c, f⟩ := ∑ q, c q · f (Quotient.out q) as a bilinear map (mirrors orbitInnerBil).

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    @[simp]
                                                                                                                                                                                                                    theorem Graphon.Lovasz.evalRepPairing_apply {T K : } (B : Fin TFin T) (W : Fin T) (c : OrbitClass T K B W) (f : (Fin KFin T)) :
                                                                                                                                                                                                                    ((evalRepPairing B W) c) f = q : OrbitClass T K B W, c q * f (Quotient.out q)
                                                                                                                                                                                                                    theorem Graphon.Lovasz.simpleEvalSubmodule_finrank_ge_orbitClass {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) :

                                                                                                                                                                                                                    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.

                                                                                                                                                                                                                    theorem Graphon.Lovasz.simpleEvalSubmodule_eq_orbitInvariantSubmodule {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) :

                                                                                                                                                                                                                    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.

                                                                                                                                                                                                                    theorem Graphon.Lovasz.orbitInvariantSubmodule_le_simpleEvalSubmodule {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) :

                                                                                                                                                                                                                    The hard inclusion orbitInvariantSubmodulesimpleEvalSubmodule.

                                                                                                                                                                                                                    Corollaries of the rank collapse: the former §3 residues #

                                                                                                                                                                                                                    theorem Graphon.Lovasz.InTupleMultiEvalSpan.toSimple {T K : } {B : Fin TFin T} (hB : ∀ (i j : Fin T), B i j = B j i) {W : Fin T} (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {f : (Fin KFin T)} (h : InTupleMultiEvalSpan B W f) :

                                                                                                                                                                                                                    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.

                                                                                                                                                                                                                    theorem Graphon.Lovasz.InTupleSimpleEvalSpan.mul {T K : } {B : Fin TFin T} (hB : ∀ (i j : Fin T), B i j = B j i) {W : Fin T} (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {f₁ f₂ : (Fin KFin T)} (h₁ : InTupleSimpleEvalSpan B W f₁) (h₂ : InTupleSimpleEvalSpan B W f₂) :
                                                                                                                                                                                                                    InTupleSimpleEvalSpan B W fun (ξ : Fin KFin T) => f₁ ξ * f₂ ξ

                                                                                                                                                                                                                    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).

                                                                                                                                                                                                                    theorem Graphon.Lovasz.orbitIndicator_aut_invariant {T K : } (B : Fin TFin T) (W : Fin T) (ξ : Fin KFin T) (τ : Equiv.Perm (Fin T)) (hτ_aut : IsWeightedAutomorphism B W τ) (η : Fin KFin T) :
                                                                                                                                                                                                                    orbitIndicator B W ξ (τ η) = orbitIndicator B W ξ η

                                                                                                                                                                                                                    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).

                                                                                                                                                                                                                    theorem Graphon.Lovasz.tupleOrbitIndicator_mem_simpleEvalSpan {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (ξ : Fin KFin T) :

                                                                                                                                                                                                                    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.

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

                                                                                                                                                                                                                    Orbit indicators lie in the ℝ-span of simple-graph evaluations (Lovász §3 fullness, 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.

                                                                                                                                                                                                                    theorem Graphon.Lovasz.tupleSimpleEval_span_aut_invariant {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (f : (Fin KFin T)) (h_aut_inv : ∀ (σ : Equiv.Perm (Fin T)), IsWeightedAutomorphism B W σ∀ (ξ : Fin KFin T), f (σ ξ) = f ξ) :
                                                                                                                                                                                                                    theorem Graphon.Lovasz.tupleEquivSimple_implies_orbit_via_2_5 {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {ξ ξ' : Fin KFin T} (h : tupleEquivSimple B W ξ ξ') :
                                                                                                                                                                                                                    tupleOrbitRel B W ξ ξ'

                                                                                                                                                                                                                    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.

                                                                                                                                                                                                                    theorem Graphon.Lovasz.InRootedProfileSpan.of_const_on_orbit {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (f : Fin T) (hf : ∀ (i j : Fin T), vertexOrbitRel B W i jf i = f j) :

                                                                                                                                                                                                                    §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:

                                                                                                                                                                                                                    1. Orbit-invariance of sqMoment i := ∑ t, W t · B i t ^ 2. Direct from IsWeightedAutomorphism via Equiv.sum_comp.
                                                                                                                                                                                                                    2. Rooted-profile span representation via InRootedProfileSpan.of_const_on_orbit (the K=1 rank theorem).
                                                                                                                                                                                                                    3. K → K=1 reduction: given tupleEquivSimple ξ ξ' at K-level and a : Fin K, derive rootedProfile B W (ξ a) F = rootedProfile B W (ξ' a) F for every simple F : SimpleGraph (Fin (n+1)). Built via a Fin (n+1) ↪ Fin (n+K) embedding that routes the K=1 label to coordinate a and stations the unlabeled vertices at positions K..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.

                                                                                                                                                                                                                    theorem Graphon.Lovasz.label_unlabeled_square_moment_descends {T K : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {ξ ξ' : Fin KFin T} (h_simple : ∀ (n' : ) (F : SimpleGraph (Fin (n' + K))) [inst : DecidableRel F.Adj], (∑ σ : Fin n'Fin T, have τ := fun (v : Fin (n' + K)) => if h : v < K then ξ v, h else σ v - K, ; (∏ v : Fin n', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) = σ : Fin n'Fin T, have τ := fun (v : Fin (n' + K)) => if h : v < K then ξ' v, h else σ v - K, ; (∏ v : Fin n', W (σ v)) * eF.edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2)) (a : Fin K) :
                                                                                                                                                                                                                    t : Fin T, W t * B (ξ a) t ^ 2 = t : Fin T, W t * B (ξ' a) t ^ 2

                                                                                                                                                                                                                    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) #

                                                                                                                                                                                                                    theorem Graphon.Lovasz.rootedOrbitIndicator_mem_rootedProfileSpan {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (i : Fin T) :
                                                                                                                                                                                                                    ∃ (N : ) (g : Fin N(n : ) × (F : SimpleGraph (Fin (n + 1))) × DecidableRel F.Adj) (c : Fin N), rootedOrbitIndicator B W i = fun (v : Fin T) => k : Fin N, c k * rootedProfileFun B W (g k).snd.fst v

                                                                                                                                                                                                                    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:

                                                                                                                                                                                                                    theorem Graphon.Lovasz.rootedProfileEquiv_imp_vertexOrbitRel {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {i j : Fin T} (h : rootedProfileEquiv B W i j) :

                                                                                                                                                                                                                    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.

                                                                                                                                                                                                                    theorem Graphon.Lovasz.rootedProfileEquiv_iff_vertexOrbitRel {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) (i j : Fin T) :

                                                                                                                                                                                                                    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).

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

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

                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      noncomputable def Graphon.Lovasz.weightedAdjIter {T : } (B : Fin TFin T) (W : Fin T) :
                                                                                                                                                                                                                      (Fin T)Fin T

                                                                                                                                                                                                                      Iterated weighted adjacency: A^m as a function.

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        noncomputable def Graphon.Lovasz.closedWalkProfile {T : } (B : Fin TFin T) (W : Fin T) (i : Fin T) :

                                                                                                                                                                                                                        Closed-walk profile at vertex i of length m.

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

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

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

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        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:

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

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

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

                                                                                                                                                                                                                          Empirical evidence (cumulative across 4 falsification scripts):

                                                                                                                                                                                                                          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:

                                                                                                                                                                                                                          Earlier empirical evidence turned out to be incomplete:

                                                                                                                                                                                                                          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
                                                                                                                                                                                                                            @[simp]
                                                                                                                                                                                                                            theorem Graphon.Lovasz.rootedCycleGraph_adj_iff {m : } (a b : Fin (m + 2)) :
                                                                                                                                                                                                                            (rootedCycleGraph m).Adj a b a + 1 = b b + 1 = a a = 0 b = m + 1 a = m + 1 b = 0

                                                                                                                                                                                                                            Adjacency unfolding lemma for rootedCycleGraph.

                                                                                                                                                                                                                            Loopless property unfolding.

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

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

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

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

                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              @[simp]
                                                                                                                                                                                                                              theorem Graphon.Lovasz.cycleSucc_val_of_lt {m : } (j : Fin (m + 2)) (hj : j + 1 < m + 2) :
                                                                                                                                                                                                                              (cycleSucc j) = j + 1
                                                                                                                                                                                                                              @[simp]
                                                                                                                                                                                                                              theorem Graphon.Lovasz.cycleSucc_val_of_eq {m : } (j : Fin (m + 2)) (hj : j = m + 1) :
                                                                                                                                                                                                                              (cycleSucc j) = 0

                                                                                                                                                                                                                              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).

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

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

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

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

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

                                                                                                                                                                                                                              theorem Graphon.Lovasz.rootedProfile_rootedCycleGraph_eq_closedWalkProfile {T m : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (i : Fin T) :

                                                                                                                                                                                                                              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).

                                                                                                                                                                                                                              theorem Graphon.Lovasz.rooted_profiles_separate_vertex_orbits {T : } (B : Fin TFin T) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i jB i B j) {i j : Fin T} (h : ¬vertexOrbitRel B W i j) :
                                                                                                                                                                                                                              ∃ (n : ) (F : SimpleGraph (Fin (n + 1))) (x : DecidableRel F.Adj), rootedProfile B W i F rootedProfile B W j F

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

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

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

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

                                                                                                                                                                                                                              STATUS: 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).

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

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

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

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

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

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

                                                                                                                                                                                                                              Status: PROVED (the separation input comes from the rank-theorem route; the historical #77 closed-walk paper-root was refuted and removed).

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

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

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

                                                                                                                                                                                                                              Status: PROVED — 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.

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

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

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

                                                                                                                                                                                                                              This avoids the n+1 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.