Documentation

Graphon.MatrixDetermination

Algebraic Determination for Finite Matrices #

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

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

Main definitions #

Main results #

References #

Vandermonde corollary #

Weighted homomorphism sum #

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

Weighted homomorphism sum for a finite matrix.

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

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

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

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

    weightedHomSum is independent of the DecidableRel instance.

    Weighted degree and star graphs #

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

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

    Equations
    Instances For
      source
      def Graphon.starGraph (m : ℕ) :
      SimpleGraph (Fin (m + 1))

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

      Equations
      Instances For
        source
        instance Graphon.starGraphDecRel (m : ℕ) :
        DecidableRel (starGraph m).Adj
        Equations

        Row profile and permutation equivalence #

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

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

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

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

          weightedHomSum for a permuted matrix.

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

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

          Star graph formula #

          Double star graph and bivariate moments #

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

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            instance Graphon.doubleStarGraphDecRel (m p : ℕ) :
            DecidableRel (doubleStarGraph m p).Adj
            Equations
            • One or more equations did not get rendered due to their size.

            Double star formula #

            Classwise row-profile moment extraction #

            Core proof for k > 0 #

            Profile star graph and row-profile power moments #

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

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

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance Graphon.profileStarGraphDecRel (m r p : ℕ) :
              DecidableRel (profileStarGraph m r p).Adj
              Equations
              • One or more equations did not get rendered due to their size.

              Multi-profile star graph and joint refinement #

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

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

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                instance Graphon.multiProfileStarGraphDecRel (m L : ℕ) (r p : Fin L → ℕ) :
                DecidableRel (multiProfileStarGraph m L r p).Adj
                Equations
                • One or more equations did not get rendered due to their size.

                Hierarchical Vandermonde and joint class separation #

                Row-class machinery for collapse #

                Structural lemmas for collapsed matrix #

                Weighted hom sum is preserved by row collapse #

                1-labeled quantum graph evaluation #

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

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

                Equations
                Instances For

                  Root attachment #

                  Graph gluing #

                  2-Labeled evaluation #

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

                  2-labeled evaluation: fix vertices 0 and 1 at colors i and j respectively, sum over all colorings of the remaining n unlabeled vertices. Labeled vertices carry no weight factor (consistent with rootedEval where the root is unweighted). This is the "2-labeled quantum graph evaluation" needed for orbit-breaking: unlike 1-labeled rootedEval, which is invariant under (B,W)-automorphisms, 2-labeled evaluation can probe individual entries B(i,j) via the edge graph.

                  Equations
                  Instances For

                    2-labeled left attachment #

                    2-labeled right attachment #

                    Automorphism invariance layer #

                    Pair-orbit decomposition #

                    Label-edge factorization #

                    Edge-free gluing #

                    Edge-free evaluation algebra #

                    Evaluation algebra closure operators #

                    CT-1 bridge: indistinguishability relations #

                    Lovász TR-2004-82 k-labeled infrastructure #

                    The 5-motif route below (starting at the "Explicit separating motifs" header) was refuted by the C₅ ⊔ C₆ counterexample (scripts/counterexample_C5_C6.py). This section installs the honest book path from Lovász's The rank of connection matrices and the dimension of graph algebras (Microsoft Research Technical Report TR-2004-82, August 2004; https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2004-82.pdf; book form: Large Networks and Graph Limits, AMS Colloquium Publications 60).

                    This is Session A of the pivot: k-labeled evaluation, equivalence, orbit relation, cheap consistency/invariance lemmas, and Claim 4.1 (restriction). Claim 4.2 (trace-extension) is installed as the new honest frontier sorry. The existing CT-1 chain (line 5200) and downstream theorems still route through the known-false motif subclaims for now; rewiring is deferred to a later session after Lemma 2.4 itself has landed.

                    Lovász TR-2004-82 Claim 4.1 and frontier statement (Claim 4.2) #

                    Graph-level trace lemma (combinatorial form of Lovász eq. (6)) #

                    Claim 4.2 via equivalence-class coefficient argument #

                    Product-trace algebra helpers (LL-factor / no-LL-glue interface) #

                    The two helpers below isolate the two "simple" halves of the multiplicative structure needed for product_trace_identity:

                    The remaining gap (inside product_trace_identity) is no longer generic graph products, but specifically: handling the accumulated multiplicity map on label-label edges across the list. That is a decorated (no-LL graph × label-edge-multiplicity-map) layer, not a full multigraph theory. It is the missing algebraic object for the next session.

                    Claim 4.3: bijective equal-cardinality case #

                    Claim 4.4: surjective case #

                    Graph product for k-labeled evaluations (Lovász algebra A_k) #

                    Decorated label-edge multiplicity layer #

                    The algebraic object that naturally arises from products of labeledEvalK evaluations across lists of graphs. Only label-label edges accumulate multiplicities (non-LL edges stay simple via iterated labeledEvalK_glue). This decorated layer is strictly smaller than full multigraph theory and matches the actual obstruction identified in product_trace_identity.

                    The structure couples:

                    The evaluation multiplies a pure-B-power term (from llMult) with the ordinary labeledEvalK of the no-LL graph. Products of decorated graphs compose componentwise: simple graphs via labeledEvalK_prod_no_LL, multiplicities via pointwise addition.

                    Step 1 helper (per user directive for breaking the L6710 cycle): ordinary decorated graph eval is tupleEquiv-invariant.

                    For D : DecLabeledGraph K n with D.llMult vanishing on Sym2 diagonals (holds for all ofSimple/one/mul-built D), and tupleEquiv B W ξ ξ' at level K: D.eval B W ξ = D.eval B W ξ'.

                    Proof: straightforward decomposition into:

                    Diagonal hypothesis: h_noDiag : ∀ x, D.llMult s(x, x) = 0. Diagonal terms B(ξ x, ξ x)^m are not generally tupleEquiv-invariant (SimpleGraph forbids self-loops, so the single-edge trick fails). The hypothesis is sound for all DecLabeledGraphs built via ofSimple/one/mul since those constructors produce llMult that vanishes on diagonals.

                    Traced decorated carrier #

                    DecLabeledGraphTr extends DecLabeledGraph with a lu0Mult : Fin K → ℕ field capturing label-to-unlabeled-position-0 multiplicity. This is the data that arises when tracing a level-(K+1) decorated graph down to level K: LL-cross edges at position K become LU edges to the new unlabeled vertex 0 at level K, with multiplicities.

                    Kept as a separate carrier (rather than enriching DecLabeledGraph in place) to avoid churn in the existing algebra (ofSimple, one, mul, and their eval lemmas). A canonical DecLabeledGraph → DecLabeledGraphTr conversion is provided via DecLabeledGraph.toTr (setting lu0Mult = 0).

                    tupleEquiv-invariance of the traced evaluation — historical context.

                    Per user directive (after the kernel-side refactor lands): this theorem should reduce to an assembly proof using the newly-canonical A_k frontier (starKernel_tupleEquiv_invariant) plus the already-proved trace-descent piece. No new math required.

                    Assembly sketch (forward-referenced definitions — defer to next proving session):

                    Decompose Dtr.eval B W ξ as: LLFactor(ξ) * (σ-sum) where

                    Status: BLOCKED by circular dependency (discovered after the kernel frontier was closed and an assembly attempt was made).

                    Circular dependency (revealed by attempted cash-out): The assembly route needs traceMeasure_eq_of_tupleEquiv (L7810) to descend the σ-sum integrand to the quotient. But traceMeasure_eq_of_tupleEquiv is proved via traceMeasure_simpleGraphEvalOn_eq_of_tupleEquiv (L7788), which in turn calls DecLabeledGraphTr.eval_tupleEquiv_invariant directly (at L7805, inside the product_trace_identity_of_eval_tupleEquiv_invariant application). Cycle:

                    L6746 (Dtr.eval_tupleEquiv_invariant)
  → traceMeasure_eq_of_tupleEquiv (L7810)
  → traceMeasure_simpleGraphEvalOn_eq_of_tupleEquiv (L7788)
  → Dtr.eval_tupleEquiv_invariant  [forward reference to L6746]

                    Resolution options (future session): (a) Refactor: move Dtr.eval_tupleEquiv_invariant to AFTER the traceMeasure/starKernel infrastructure (~L8100+), and rewrite traceMeasure_simpleGraphEvalOn_eq_of_tupleEquiv to NOT directly call Dtr.eval_tupleEquiv_invariant — e.g., by inlining the algebra it relies on, or by making the theorem parametric over multigraph invariance. (b) Direct proof: find a proof of Dtr.eval_tupleEquiv_invariant using ONLY infrastructure declared before L6746 (simple-graph tupleEquiv, labeledEvalK_singleEdge, hB) — NOT via traceMeasure or starKernel. Likely requires a fresh proof technique. (c) Hypothesis relaxation: add h_noSelfLL : ∀ x, Dtr.llMult s(x, x) = 0 to the theorem — needed anyway for the LL-factor diagonal case, and already done in trace_eval. Allows a cleaner proof of the LL factor piece.

                    Partial progress during the attempt (reverted): LL-factor invariance via labeledEvalK_singleEdge + diagonal hypothesis WAS verified to compile. The n = 0 case WAS verified modulo instance-mismatch workarounds. The n = n'+1 Dup construction WAS designed but its completion hit (1) the circular dependency and (2) rewriting motive issues with SimpleGraph.map + Fintype instance shadowing inside DecLabeledGraphTr.eval's body.

                    Recommendation: option (a) — structural refactor. The reorganization itself is ~50 lines; then the Dup assembly lands via the user's original plan.

                    UPDATE (post step-1 analysis — cycle is SEMANTIC): the user's stop-rule for the cycle-breaker attempt is triggered. Tracing the dependency closely:

                    Conclusion: the true root theorem is the generator/trace-descent content, whatever name we give it. Renaming to DecLabeledGraph.trace_tupleEquiv_invariant does not eliminate the content — it relabels. The cycle is semantic, not just file order.

                    Per user's stop-rule: the honest framing is that the frontier is product_trace_identity itself (the generator theorem with specific trace-descent content), NOT Dtr.eval_tupleEquiv_invariant at the arbitrary-Dtr level. The renaming clarifies this: future work should attack the generator theorem directly as the root. A pure file restructure cannot eliminate the content; what's needed is either: (a') New mathematical content for the generator theorem (some form of the A_k algebra argument with specific trace structure). (b') Pivot to explicit Lovász A_k / connection-matrix machinery. (c') Accept current state: 8 sorries total (1 frontier + 4 frozen + 3 architectural), with the algebraic chain wired through a single semantic root.

                    OFF-AXIS (post-bridge consolidation): this theorem is no longer the canonical root. The active chain now routes through multiLabeledEvalK_tupleEquiv_invariant (the multigraph bridge, L7150). This Dtr theorem remains in the file as a documented generalization with its own narrowed sorry (∃ a, lu0Mult a ≥ 1 case at the σ-sum level), but is not on the active proof axis. Future sessions: do NOT route new content through this theorem.

                    The named algebraic residue. σ-sum equality for the trace-origin parallel-edge case: ∃ a, D.trace.lu0Mult a ≥ 2.

                    This is the single residual mathematical obligation for the trace-origin path. The full theorem trace_eval_tupleEquiv_invariant calls this lemma in the dispatch case where lu0Mult ≤ 1 does not hold; all other cases (LL factor, lu0Mult = 0, lu0Mult ≤ 1) are closed.

                    Mathematical content (Lovász TR-2004-82 §3): when at least one label-to-unlabeled-0 multiplicity exceeds 1, the σ-sum body contains B(ξ a, σ 0)^k with k ≥ 2 — parallel B-edges that no simple-graph labeledEvalK can express.

                    Cycle check (per user directive, step 3): the natural reduction to starMultigraphEval_tupleEquiv_invariant_direct (via fixing all σ coordinates except σ 0 and applying the power-sum theorem) is blocked by a transitive cycle:

                    starMultigraphEval_tupleEquiv_invariant_direct  (L9456)
  → traceMeasure_eq_of_tupleEquiv               (L9205)
  → traceMeasure_simpleGraphEvalOn_eq_of_tupleEquiv  (L9179)
  → tr_k_generator_descends                     (L8390)
  → tr_k_binary_product_descends                 (L8369)
  → Ak_trace_stable_generators                  (L8240)
  → weightedInnerProduct_descends               (L8451)
  → DecLabeledGraph.trace_eval_tupleEquiv_invariant  (L7113)
  → trace_parallel_lu0_descends                  (this theorem)

                    Same applies to tupleEquiv_power_sum_invariance (one-liner via the star-multigraph theorem, plus hW + htwin strengthenings).

                    Conclusion (per user step 4): this theorem is the canonical named algebraic root of the Lovász §3 multigraph content. Future attacks must either:

                    Smallest subcase = full content (per user's "smallest independent subcase" inquiry). The simplest non-trivial instance is n = 0, D.trace.lu0Mult = 2 • δ_a (one coordinate with multiplicity 2, all others zero). For this:

                    This is exactly tupleEquiv_single_coord_square_moment (L9700, declared forward of this theorem). That theorem's proof routes through starMultigraphEval_tupleEquiv_invariant → traceMeasure_eq_of_tupleEquiv → tr_k_generator_descends → ... → this theorem. So the smallest case is not independently provable under the current architecture; it's a restatement of the full content.

                    Dependency chain audit (confirmed): tupleEquiv_implies_tupleOrbitRel non-surj branch (L10393, L10530) → tupleEquiv_extend (L10209, calls coeffRestrict_equiv at L10221) → coeffRestrict_equiv (L9956, uses product_trace_identity per docstring) → product_trace_identity (L9910, calls tr_k_generator_descends at L9927) → tr_k_generator_descends → tr_k_binary_product_descends → Ak_trace_stable_generators → weightedInnerProduct_descends → DecLabeledGraph.trace_eval_tupleEquiv_invariant → this theorem.

                    Hence: the non-surj architectural branch cannot close until this theorem closes.

                    Stated with σ-sum-only conclusion (not full D.trace.eval equality); the LL factor handling stays in the consumer theorem.

                    Multigraph carrier — Lovász §2 (paper-faithful) #

                    Per the Lovász §3 extraction (see plan): the canonical formalization target is the multigraph extension of tupleEquiv. A k-labeled multigraph at level K, n unlabeled is given by a multiplicity function on Sym2 (Fin (n + K)). (Lovász §2: "F may have multiple edges, but no loops"; we encode loop-freeness via multNoLoop.)

                    multiLabeledEvalK raises B to the multiplicity power on each Sym2-pair, summing over unlabeled assignments with W-products.

                    Step A: ofSimple — wrap a simple graph as a decorated graph #

                    Step B: one, mul, and their evaluation lemmas #

                    Multigraph / A_k extension frontier (OPEN) #

                    Central open claim. DecLabeledGraphTr.eval_tupleEquiv_invariant — the invariance of the decorated multigraph evaluation under simple-graph tupleEquiv. This is the single mathematical frontier now blocking the IH-free Lovász Lemma-2.4 path. All other critical-path sorries (product_trace_identity, coeffRestrict_equiv, tupleEquiv_extend, and the non-surjective branch of tupleEquiv_implies_tupleOrbitRel) reduce to it transitively.

                    Why it is the frontier. Simple-graph labeledEvalK cannot encode B(ξ a, σ' 0)^m for m ≥ 2: every candidate simple-graph gadget (parallel-edge simulation via pendant unlabeled vertices, subdivision by paths of length 2, fresh copies of the label, etc.) yields (∑ W B)^m — the power of a linear moment — rather than ∑ W B^m — an honest power-sum moment. These are algebraically independent as polynomials in B, so the multigraph invariance cannot be derived as a corollary of simple-graph tupleEquiv by gadget-style reductions.

                    Lovász A_k algebra. The full closure is Lovász's A_k algebra (TR-2004-82 §3–4): the multiplicative closure of labeledEvalK evaluations over simple graphs forms a unital point-separating algebra of class functions on the tupleEquiv-quotient, and invariance of multigraph evaluations follows from this structural closure. Closing eval_tupleEquiv_invariant in Lean likely requires either:

                    1. multigraph tupleEquiv as a primitive with an equivalence proof back to simple-graph tupleEquiv; or
                    2. a polynomial-identity argument extracting higher moments from the rich simple-graph evaluation family (closer to Lovász's original).

                    Downstream consequences (critical path):

                    This section isolates the reduction; the central theorem itself (DecLabeledGraphTr.eval_tupleEquiv_invariant) retains its sorry body at its existing location above.

                    A_k extension project — SKELETON #

                    The multigraph / A_k extension is now the single real frontier for the main Lemma-2.4 path. All other critical-path sorries reduce to it. This section stubs the intermediate theorems and names the concrete targets for the follow-up proving sessions.

                    Dependency DAG (topological order, shortest honest route):

                      Level 1 (frontier)
    tupleEquiv_power_sum_invariance          [STUB]
    tupleEquiv_polynomial_moment_invariance  [STUB — generalizes L1]
      ↓
  Level 2 (core claim)
    DecLabeledGraphTr.eval_tupleEquiv_invariant  [STUB at L6705]
      ↓ (existing reductions, already wired)
  Level 3 (downstream — already proved modulo the frontier)
    product_trace_identity           [L7166, one-liner via Reduction 1]
    coeffRestrict_equiv              [next section, uses L3a]
    tupleEquiv_extend                [next section, uses L3b]
      ↓
  Level 4 (architectural refactor — NEW stubs below)
    tupleEquiv_bijective_case_ext    [STUB — Claim 4.3 via extension]
    tupleEquiv_surjective_case_ext   [STUB — Claim 4.4 via extension]
      ↓
  Level 5 (main theorem — WF rebuild)
    tupleEquiv_implies_tupleOrbitRel  [non-surj branch at L7643, stub]
      ↓
  Level 6 (downstream)
    twinfree_bijection_of_weightedHomSum_eq  [stub at L8790]

                    Why Levels 4–5 are NEW work even after Level 1 lands:

                    The existing tupleEquiv_bijective_case / tupleEquiv_id_bijective (Claim 4.3) and tupleEquiv_surjective_case (Claim 4.4) internally restrict a bijection χ : Fin T → Fin T to size T-1, producing a pair whose joint-range deficit can be 1 (when χ(Fin.last) = Fin.last). A well-founded induction with deficit-primary lex starting at (0, k+1) cannot supply an IH at (1, T-1). The ext-variants below avoid this by instead extending from deficit-0 size-T instances — i.e., consuming tupleEquiv_extend rather than restriction. Proving them requires the extension theorem (Level 1) to be in place first.

                    Each stub below is named, typed, and documented. The sorry bodies are placeholders for future proving sessions; no new algebra is landed here.

                    Level 1 stubs — power-sum / moment invariance #

                    Minimal evaluation object for Level 1 work (starMultigraphEval). The exact quantity that tupleEquiv_power_sum_invariance is about: the W-weighted sum of B-power products indexed by a multiplicity vector m. This is the star-multigraph evaluation (one unlabeled center, K labels, each label incident to the center with multiplicity m_a). Not full multigraph theory, not the full A_k algebra — just the minimal object needed to name the frontier precisely.

                    Project order (per user directive after Level 1 narrowing):

                    1. tupleEquiv_single_coord_square_moment — smallest non-simple seed case: m = 2 • δ_a. The atomic multigraph content.
                    2. tupleEquiv_single_coord_plus_background — one repeated coord r • δ_{a₀} plus an arbitrary 0/1 background on S ⊆ Fin K \ {a₀}. The exact bridge to DecLabeledGraphTr.eval (Level 2 stub).
                    3. Only after (1) and (2) close should the ∃ a, m_a ≥ 2 branch of tupleEquiv_power_sum_invariance be tackled in full generality.
                    A_k algebra infrastructure (Steps 1-4 of the extension project) #

                    Infrastructure for Path (d) — the Lovász A_k algebra argument — following the user's bounded "infrastructure only" directive. Defines the tupleEquiv-quotient, the simple-graph evaluation subalgebra on it, and the three structural facts (constants / multiplication / point-separation). Fullness is stated as a dual of functional_span_zero and left sorry'd for the follow-up proving session.

                    Step 4 — fullness of the simple-graph subalgebra on the #

                    tupleEquiv-quotient

                    Every function g : TupleClass → ℝ is a linear combination of products of labeledEvalK's (i.e. lies in the span of simpleGraphEvalOn L values).

                    This is the finite-dimensional Stone–Weierstrass statement for the algebra generated by {simpleGraphEvalOn L : L} on the finite set TupleClass. Concretely, for each q₀ : TupleClass, an indicator 1_{q₀} is built via Lagrange-interpolation: for each q ≠ q₀, we pick L_{q,q₀} from simpleGraphEvalOn_separates and form the product ∏_{q ≠ q₀} (f_{q, q₀} − f_{q, q₀}(q)) / (f_{q, q₀}(q₀) − f_{q, q₀}(q)) where f_{q, q₀} := simpleGraphEvalOn B W L_{q, q₀}. This evaluates to 1 at q₀ and 0 elsewhere. Any g is then g = ∑_q g(q) · 1_q.

                    The full formalization packages a recursive algebra-closure construction via coeffEval, coeffMul, and indicatorCoeffs below.

                    A_k / tr_k algebra layer — CANONICAL semantic root #

                    Per user directive (after the post-step-1 analysis revealed the cycle is semantic): pivot from the current three-interfaces view to a single named theorem that honestly captures the missing content. The A_k algebra is the unital, multiplicatively closed, point-separating subalgebra of (TupleClass T K B W → ℝ) generated by the simpleGraphEvalOn family — by simpleGraphEvalOn_spans (Step 4, closed), A_k is the full algebra of class functions at level K.

                    The trace operator tr_k : (TupleClass T (K+1) B W → ℝ) → (Fin K → Fin T) → ℝ is defined by pushforward along Fin.snoc:

                      tr_k B W f ξ := ∑ t, W t · f ⟦Fin.snoc ξ t⟧.

                    It lands in class functions on TupleClass T K B W iff its output descends through the level-K tupleEquiv, i.e., iff tupleEquiv B W ξ ξ' → tr_k B W f ξ = tr_k B W f ξ'.

                    The canonical semantic root (tr_k_descends_to_A_k below): this descent property holds for every class function f. All three "frontier" theorems in this file are restatements of this content:

                    Current status: this canonical root is the single live sorry under the A_k framing. The three frontiers above are semantically equivalent restatements — renaming does not eliminate the content.

                    Section-level notes on the canonical root #

                    The trace operator tr_k above sends class functions on TupleClass T (K+1) B W to raw functions on Fin K → Fin T. The key question: does the output descend through the level-K tupleEquiv quotient? This is the content of tr_k_descends_to_A_k below — the SINGLE theorem behind the three current frontiers (DecLabeledGraphTr.eval_tupleEquiv_invariant, traceMeasure_eq_of_tupleEquiv, starMultigraphEval_tupleEquiv_invariant_direct).

                    Per user's post-step-1 analysis, the cycle among those three is the semantic manifestation of having three names for one theorem. tr_k_descends_to_A_k (below) is now the canonically-named target; its proof reduces via simpleGraphEvalOn_spans + tr_k linearity to the generator theorem tr_k_generator_descends, which is the minimal mathematical content.

                    Requires hB (symmetric B), same reason as starKernel_tupleEquiv_invariant: without hB, Quot.out orientations disagree with the fixed-orientation B-argument convention in starKernel / starMultigraphEval.

                    tr_k linearity (trivial, needed for the wrapper proof below) #
                    Generator theorem — the NEW canonical root #

                    Per user directive (narrower than full tr_k_descends_to_A_k): attack the single-generator case first. The full theorem tr_k_descends_to_A_k reduces to this via simpleGraphEvalOn_spans

                    If this generator theorem lands, all three current frontiers collapse:

                    If this theorem resists, the honest conclusion is that the root is specifically "trace of generator products descends", and we should stop renaming and attack the Lovász A_k connection-matrix machinery.

                    Generator theorem context

                    For every list L of (K+1)-labeled simple graphs and tupleEquiv B W ξ ξ' at level K:

                      tr_k B W (simpleGraphEvalOn B W L) ξ = tr_k B W (simpleGraphEvalOn B W L) ξ'.

                    Equivalently (via traceMeasure_pushforward):

                      ∑ t, W t · (L.map (fun p => labeledEvalK p.1 p.2 B W (Fin.snoc ξ t))).prod =
  ∑ t, W t · (L.map (fun p => labeledEvalK p.1 p.2 B W (Fin.snoc ξ' t))).prod.

                    This is the canonical sorry going forward. All downstream theorems (tr_k_descends_to_A_k by wrapper, and the three current frontiers by corollary chain) route through tr_k_generator_descends below.

                    Requires hB: symmetric B (same reason as starKernel_tupleEquiv_invariant).

                    Lovász A_k module — connection-matrix trace stability #

                    Per user directive (paper-faithful framing, scoped narrowly): introduce the class-function algebra on TupleClass T K B W and name the remaining algebraic content after Lovász's connection-matrix trace stability theorem.

                    Connection-matrix view (Lovász TR-2004-82 §3): for a (K+1)-labeled graph F with n unlabeled vertices, the connection matrix M(F) : (Fin K → Fin T) × Fin T → ℝ is defined by M(F)[ξ, t] := labeledEvalK (K+1) n F B W (Fin.snoc ξ t). The trace Tr(M(F)) : (Fin K → Fin T) → ℝ is Tr(M(F))[ξ] := ∑ t, W t · M(F)[ξ, t] = tr_k B W (labeledEvalK F) ξ.

                    Multiplicativity of connection matrices (for graphs F, G with shared labels and disjoint unlabeled vertex sets) says M(F ⊔ G) = M(F) * M(G) (Hadamard product in this indexing). Trace-stability is the assertion that Tr(M(F) * M(G)) descends to a class function on TupleClass T K B W. This is the canonical target per Lovász's paper-faithful proof strategy.

                    Connection-matrix view — paper-faithful frontier #

                    Per user directive (post-Ak_trace_stable_generators session): the actual mathematical content of the remaining sorry is Lovász's connection-matrix trace-stability theorem. Name it in those terms by introducing the column view connCol and phrasing the sorry as a weighted inner product of two columns.

                    Column view. For a list L of (K+1)-labeled simple graphs,

                    connCol B W L ξ t := simpleGraphEvalOn B W L ⟦Fin.snoc ξ t⟧

                    is the (ξ, t)-entry of the connection matrix M(L) (Hadamard product over L of single-graph connection matrices).

                    Frontier. weightedInnerProduct_descends states that the W-weighted inner product of two columns descends through the level-K tupleEquiv quotient:

                    ∑ t, W t · connCol L₁ ξ t · connCol L₂ ξ t =
∑ t, W t · connCol L₁ ξ' t · connCol L₂ ξ' t  whenever tupleEquiv B W ξ ξ'.

                    This is Tr(M(L₁) * M(L₂)) viewed as a function of the row index ξ. Trace stability (Lovász TR-2004-82 §3, Theorem 3.1).

                    Step 4 attempt (and the cycle). The obvious reduction chain

                      LHS = ∑ t, W t · simpleGraphEvalOn B W (L₁ ++ L₂) ⟦Fin.snoc ξ t⟧  [connCol_append]
      = tr_k B W (simpleGraphEvalOn B W (L₁ ++ L₂)) ξ               [defn tr_k]
      = tr_k B W (simpleGraphEvalOn B W (L₁ ++ L₂)) ξ'              [tr_k_generator_descends]
      = RHS.

                    works for |L₁ ++ L₂| ≤ 1 (the tr_k_singleton_descends cases closed by tr_k_generator_descends directly) but loops for |L₁ ++ L₂| ≥ 2: tr_k_generator_descends routes the multi-element case through tr_k_binary_product_descends, which routes through Ak_trace_stable_generators, which (below) routes through weightedInnerProduct_descends. The cycle confirms this is the precise Lovász connection-matrix frontier — not a Lean bookkeeping artifact. Further progress requires the paper-faithful connection-matrix argument (or the graph-gadget route via labeledEvalK_glue, itself sorry'd).

                    Wiring. Ak_trace_stable_generators (below) is now a proved corollary of weightedInnerProduct_descends via pointwise reshape of tr_k-of-product into connCol-inner-product form.

                    Decorated-graph carrier for connCol — concrete assembly #

                    Per user directive: build the closure of weightedInnerProduct_descends via the DecLabeledGraph.ofSimple / mul / trace layer, landing the descent claim at the existing DecLabeledGraphTr.eval_tupleEquiv_invariant sorry (L6913). This collapses two equivalent live sorries into one canonical Lovász §3 frontier theorem.

                    Pipeline:

                    1. connListD L: fold the list into a single DecLabeledGraph (K+1) N via DecLabeledGraph.one + ofSimple + mul.
                    2. connListD_eval: the carrier evaluates to connCol B W L.
                    3. connListD_noSelfLastLL: the LL-multiplicity at the diagonal pair s(Fin.last K, Fin.last K) is zero (simple graphs have no self-loops; ofSimple's llMult is therefore zero on diagonals, and mul preserves this by pointwise sum).
                    4. DecLabeledGraph.trace_eval: ∑_t W(t) · D.eval (snoc ξ t) = D.trace.eval ξ (requires noSelfLastLL).
                    5. DecLabeledGraphTr.eval_tupleEquiv_invariant: D.trace.eval descends through tupleEquiv at level K. (This is the canonical sorry.)
                    Trace measure on (K+1)-tuple classes — canonical frontier #

                    Per user directive (after the K=1 diagnostic confirmed the same A_k content appears at every depth): promote "trace measure descends to the tupleEquiv-quotient" to the canonical frontier. This single statement subsumes the parallel frontiers we have accumulated:

                    The remaining gap is therefore no longer "which functions are in the algebra" (Step 4 settled that) and no longer "is the star-multigraph descent the frontier" — it is "does the trace functional descend to the quotient?" That is the A_k frontier in its cleanest form.

                    Trace descent — the generator theorem + full measure equality #

                    The trace-measure class-invariance theorem is the cleanest statement of "the trace functional descends to the tupleEquiv-quotient". It is the trace-side piece of the two-piece A_k package (the kernel-side piece is below). Proved via the two-piece split:

                    (1) traceMeasure_simpleGraphEvalOn_eq_of_tupleEquiv (generator theorem, below) — the simpleGraphEvalOn pairing is class- invariant. Proved via product_trace_identity + traceMeasure_pushforward. (2) simpleGraphEvalOn_spans (Step 4, previously closed) upgrades pointwise generator equality to full measure equality via Lagrange indicators.

                    hB (symmetry of B) is required because product_trace_identity uses it for the DecLabeledGraph-algebra reduction. If product_trace_identity is later tightened, hB can be dropped.

                    Tuple-level representation theorem (the real frontier) #

                    Per user directive after closing simpleGraphEvalOn_spans (Step 4): the hard mathematical content is now starMultigraphEval respects tupleEquiv, stated as starMultigraphEval_tupleEquiv_invariant_direct below. Once that is known, the span representation is a short corollary by quotient descent (apply simpleGraphEvalOn_spans to the descended function). The representation theorem starMultigraphEval_in_simpleGraphSpan is now algebraic bookkeeping, NOT the frontier.

                    Dependency reorganization (as of this commit):

                      starMultigraphEval_tupleEquiv_invariant_direct    [FRONTIER, sorry]
    ↓ (quotient descent + simpleGraphEvalOn_spans)
  starMultigraphEval_in_simpleGraphSpan             [proved]
    ↓
  starMultigraphEval_tupleEquiv_invariant           [proved, existing]
    ↓ (wires to)
  tupleEquiv_power_sum_invariance
  tupleEquiv_single_coord_square_moment
  tupleEquiv_single_coord_plus_background

                    The frontier is now a pure-equality statement on tuples — cleaner to attack than the existential representation.

                    Proof strategy for the direct frontier (Lovász TR-2004-82 §3–4): multigraph A_k algebra. The span argument is deferred to a cleaner handle via the descent-then-span chain above.

                    Kernel-side refactor (per user directive) #

                    The direct invariance theorem starMultigraphEval_tupleEquiv_invariant_direct is now PROVED via the two A_k pieces:

                    Falsification gate passed (from the previous stub's docstring):

                    Strategy (Lovász A_k): construct starKernel as a fixed element of the algebra generated by simple-graph labeledEvalK's at level K+1. Inclusion-exclusion / Möbius inversion on multigraph configurations.

                    K = 1 diagnostic: trace-measure recasting #

                    Per user directive after falsification: attack K = 1 first as a diagnostic for whether the obstruction is already present at the one-coordinate moment problem, or whether it only arises with coordinate mixing.

                    Recasting (canonical shape at K=1):

                    The annihilation sublemma (the heart of K=1): tupleEquiv B W ξ ξ' → traceMeasureK1 ξ = traceMeasureK1 ξ' as functions on TupleClass T 2 B W.

                    If annihilation lands, simpleGraphEvalOn_spans (Step 4, closed) applied to edgeValClass ^ r gives the K=1, all-r theorem immediately: ∑ q μ_ξ(q) · edgeValClass(q)^r = ∑ q μ_ξ'(q) · edgeValClass(q)^r.

                    Diagnostic finding (per analysis after stating the stub):

                    The annihilation sublemma is equivalent to product_trace_identity at k = 1:

                    ∑ t, W t · ∏_{p ∈ L} labeledEvalK 2 n_p F_p (Fin.snoc ξ t)
  = same for ξ'   (for all lists L)

                    Expanding via simpleGraphEvalOn at level 2, both sides recombine to ∑_q μ_ξ(q) * simpleGraphEvalOn L q which equals ∑_q μ_ξ'(q) * simpleGraphEvalOn L q. And product_trace_identity at k = 1 carries the same multigraph content as the general frontier: LL-edge multiplicities across the list (at K = 1, the only label pair is (0, 1) at level 2; any list with ≥ 2 graphs each containing this LL edge produces multiplicity ≥ 2 — the multigraph obstruction).

                    Conclusion: K = 1 is NOT genuinely easier. The same A_k multigraph closure is required. This localizes the missing content precisely: the "annihilation of trace measures on 2-tuple classes" IS the multigraph A_k content, not a weaker statement.

                    Level 1 (main) — power-sum invariance for arbitrary multiplicity #

                    Level 4 stubs — Claim 4.3 / 4.4 refactored via extension #

                    tupleEquiv_bijective_case_ext and tupleEquiv_surjective_case_ext are declared after tupleEquiv_implies_tupleOrbitRel (the main theorem) since they delegate to it directly. The original Claim 4.3/4.4 ext design called for an upward-extension proof avoiding deficit-1 IHs, but with the main theorem available (modulo the non-surjective architectural sorry), direct delegation is the simplest closure.

                    Level 5 — main theorem via WF induction #

                    The WF rebuild of tupleEquiv_implies_tupleOrbitRel does NOT get its own stub here: it reuses the existing declaration at L7513. Once Levels 1–4 are closed, the non-surjective branch at L7643 closes by:

                    1. WF induction on (deficit, size) lex with deficit primary.
                    2. Extension step via tupleEquiv_extend: deficit strictly decreases.
                    3. Surjective case via tupleEquiv_surjective_case_ext: does not require out-of-range IH (unlike the existing tupleEquiv_surjective_case).
                    4. Restriction step (when deficit preserved): standard.

                    The existing comment at L7643 already documents the architectural picture; no further docstring here.

                    Level 6 — downstream twin-free bijection #

                    twinfree_bijection_of_weightedHomSum_eq (stub at ~L8790) then falls out via the k≥2 case's row-collapse argument, once the Lovász Lemma-2.4 chain above is in place. This is known to be the final step per existing memory notes; no new stub here.

                    End of skeleton. Follow-up proving sessions should target Level 1 first (tupleEquiv_power_sum_invariance), which is both the simplest and the deepest mathematical content in this tree. All other stubs reduce to it by routine assembly modulo the architectural refactors at Level 4.

                    Surjective-base extension uniqueness #

                    Lemma 2.4: tupleEquiv implies tupleOrbitRel #

                    Level 4 ext stubs — delegations to the main theorem #

                    These were originally architectural placeholders for an upward-extension proof. With tupleEquiv_implies_tupleOrbitRel available (modulo the non-surjective architectural sorry inside its strong induction), both ext theorems become trivial delegations. The bijective and surjective cases are fully closed inside the main theorem's strong-rec body.

                    Explicit separating motifs #

                    ⚠ KNOWN-FALSE-FOR-SPARSE-B — retained to prevent cascade.

                    The 5-motif pairProfile route below is refuted by the C₅ ⊔ C₆ counterexample (scripts/counterexample_C5_C6.py): that is a twin-free positive-weight matrix where (0, 0) and (5, 5) have identical 5-motif profiles but lie in different pair orbits under Aut(C₅ ⊔ C₆) = D₅ × D₆.

                    This section is kept intact during the Lovász pivot (Sessions A–E) only so that the live CT-1 chain (lines 4926, 5200) and downstream uses do not cascade. The sorries at vertexOrbit_of_star0_tri0_eq and pairOrbit_of_vertexOrbits_and_path are known-false as stated and must not be relied upon for any general claim. They will be deleted in a future session once the Lovász-based replacement is wired in.

                    Five edge-free 2-labeled graphs whose evaluations form the pairProfile — a 5-tuple that (conjecturally, and confirmed by computation up to T=10 on dense matrices, but FALSE on sparse matrices like C₅ ⊔ C₆) determines pair orbits for twin-free matrices with positive weights.

                    Three-subclaim decomposition of pair orbit determination #

                    Rather than attacking pairOrbitRel_of_pairProfile_eq directly, we factor it through three smaller lemmas:

                    pairOrbitRel_of_pairProfile_eq is assembled from the three.

                    ⚠ Correctness warning: Subclaim (L) is FALSE as stated, and consequently pairOrbitRel_of_pairProfile_eq is also FALSE as stated. Counterexample: C₅ ⊔ C₆ (disjoint union of a 5-cycle and a 6-cycle, as a {0,1}-matrix on Fin 11 with uniform weights W = 1/11). This matrix is symmetric, twin-free, has positive weights, yet every vertex has star0 = 2/11 and tri0 = 0 (no triangles), so the 5-motif pairProfile cannot distinguish any two vertices. In particular, pairs (0,0) and (5,5) have identical profiles but lie in different pair orbits under Aut(C₅ ⊔ C₆) = D₅ × D₆.

                    The earlier computational validation (scripts/vertex_orbit_subclaim.py and scripts/cross_term_coherence.py) missed this because it tested only dense matrices with entries in [0.1, 0.9]. For such dense matrices the subclaims empirically hold, but the proof route cannot extend to the sparse case without strengthening the hypothesis (e.g., requiring ∀ i j, 0 < B i j) or switching to a richer, infinite family of test graphs (see Graphon/LovaszScratch.lean on the lovasz-feasibility branch for the Lovász TR-2004-82 route — itself blocked by the trace-operator infrastructure).

                    The subclaim sorries below are kept in place for documentation and because removing them would cascade through CT-1 and downstream theorems, but they should be understood as known-false-for-sparse-twin-free-B and not relied upon for any general claim. A future session must either:

                    Explicit motif graphs #

                    Each of the five profile components is realized as the labeledEval2 of a specific edge-free 2-labeled graph. The graphs are:

                    Edge-free indistinguishability span characterization #

                    CT-1 assembly #

                    Twin-free bijection #

                    Main theorem #

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

                    Algebraic determination for finite matrices (quotient form).

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

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

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

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

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

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

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