Cycle–Krylov spectral slice (#70 square-moment descent)

The finite-dimensional linear algebra closing the cycle–Krylov–kernel proof of square-moment descent (docs/sqmoment-cycle-krylov.md), kept in its own file because it imports inner-product-space machinery that must not pollute Lovasz.lean (known simp-conflict issue).

Contents

• inner_eq_zero_of_orthogonal_pos_powers — the abstract lemma over a finite-dimensional real inner product space: if A is self-adjoint, u ∈ range A, and e ⊥ A^q u for all q ≥ 1, then e ⊥ u. Proof by orthogonal projection onto the positive-power Krylov span K: the residual w = u - proj_K u satisfies A w = 0 (since A² w ∈ K and ‖A w‖² = ⟪w, A² w⟫ = 0), hence ⟪w, u⟫ = ⟪w, A z⟫ = ⟪A w, z⟫ = 0, hence ‖w‖² = 0, so u ∈ K and e ⊥ u.
• sqrtScale / conjAdj — transport of the W-weighted inner product wInner to EuclideanSpace ℝ (Fin T) via √W-rescaling; conjAdj is the conjugated operator, i.e. the symmetric matrix S(t,s) = √(W t) · B t s · √(W s).
• wInner_eq_zero_of_iter_orthogonal — the weighted instantiation in terms of weightedAdj / weightedAdjIter.
• sqMoment_eq_of_closedWalkProfile_eq — the assembled spectral slice: equal closed-walk profiles at all lengths ≥ 3 force equal square moments. After this, the remaining content of sqMoment_descends_of_rootedProfileEquiv is pure graph plumbing (rooted cycles realize closedWalkProfile, and rpe kills their differences).

The abstract finite-dimensional lemma

theorem Graphon.Lovasz.mem_span_pos_powers_of_mem_range {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (A : E →ₗ[ℝ] E) (hA : ∀ (x y : E), inner ℝ (A x) y = inner ℝ x (A y)) {u : E} (hu : u ∈ A.range) : u ∈ Submodule.span ℝ (Set.range fun (q : ℕ) => (A ^ (q + 1)) u)

Krylov span membership for range elements — the projection core of the spectral slice, extracted as a standalone lemma: if A is self-adjoint and u ∈ range A, then u lies in the span of its own positive A-powers. (The "missing zeroth power" is recovered because u ∈ range A forces the ker A-component of u to vanish.)

theorem Graphon.Lovasz.inner_eq_zero_of_orthogonal_pos_powers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (A : E →ₗ[ℝ] E) (hA : ∀ (x y : E), inner ℝ (A x) y = inner ℝ x (A y)) {u : E} (hu : u ∈ A.range) {e : E} (he : ∀ (q : ℕ), inner ℝ e ((A ^ (q + 1)) u) = 0) : inner ℝ e u = 0

Krylov-kernel lemma: in a finite-dimensional real inner product space, if A is self-adjoint, u lies in the range of A, and e is orthogonal to A^q u for every q ≥ 1, then e is orthogonal to u itself.

The direct-sum (common-coefficient) lemma

noncomputable def Graphon.Lovasz.prodMapL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : E →ₗ[ℝ] E) : WithLp 2 (E × E) →ₗ[ℝ] WithLp 2 (E × E)

The block-diagonal operator A ⊕ A on WithLp 2 (E × E).

Equations

• Graphon.Lovasz.prodMapL2 A = ↑(WithLp.linearEquiv 2 ℝ (E × E)).symm ∘ₗ A.prodMap A ∘ₗ ↑(WithLp.linearEquiv 2 ℝ (E × E))

theorem Graphon.Lovasz.prodMapL2_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : E →ₗ[ℝ] E) (x : WithLp 2 (E × E)) : (prodMapL2 A) x = WithLp.toLp 2 (A x.ofLp.1, A x.ofLp.2)

theorem Graphon.Lovasz.prodMapL2_selfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : E →ₗ[ℝ] E) (hA : ∀ (x y : E), inner ℝ (A x) y = inner ℝ x (A y)) (x y : WithLp 2 (E × E)) : inner ℝ ((prodMapL2 A) x) y = inner ℝ x ((prodMapL2 A) y)

prodMapL2 A inherits self-adjointness from A (for the L² product inner product).

theorem Graphon.Lovasz.prodMapL2_pow_toLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : E →ₗ[ℝ] E) (q : ℕ) (a b : E) : (prodMapL2 A ^ q) (WithLp.toLp 2 (a, b)) = WithLp.toLp 2 ((A ^ q) a, (A ^ q) b)

Powers of prodMapL2 A act componentwise as powers of A.

theorem Graphon.Lovasz.pair_mem_common_pos_power_span {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (A : E →ₗ[ℝ] E) (hA : ∀ (x y : E), inner ℝ (A x) y = inner ℝ x (A y)) {u v : E} (hu : u ∈ A.range) (hv : v ∈ A.range) : ∃ (s : Finset ℕ) (c : ℕ → ℝ), ∑ q ∈ s, c q • (A ^ (q + 1)) u = u ∧ ∑ q ∈ s, c q • (A ^ (q + 1)) v = v

Common Krylov coefficients for a pair (the direct-sum trick): if u and v both lie in the range of a self-adjoint A, then there are COMMON coefficients expressing each of them as a combination of its own positive A-powers. Obtained by applying mem_span_pos_powers_of_mem_range to the block operator on WithLp 2 (E × E) and projecting the two coordinates.

Note a triple (or longer) version with REPEATED vectors needs nothing more: the slots of a multilinear form repeat u or v, and this pair of common expansions feeds every slot.

The k-fold direct-sum (family common-coefficient) lemma

noncomputable def Graphon.Lovasz.piMapL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : ℕ) (A : E →ₗ[ℝ] E) : (PiLp 2 fun (x : Fin m) => E) →ₗ[ℝ] PiLp 2 fun (x : Fin m) => E

The block-diagonal operator ⨁_{i : Fin m} A on PiLp 2 (fun _ : Fin m => E) (the Fin m-fold generalization of prodMapL2).

Equations

• Graphon.Lovasz.piMapL2 m A = ↑(WithLp.linearEquiv 2 ℝ (Fin m → E)).symm ∘ₗ (LinearMap.pi fun (i : Fin m) => A ∘ₗ LinearMap.proj i) ∘ₗ ↑(WithLp.linearEquiv 2 ℝ (Fin m → E))

theorem Graphon.Lovasz.piMapL2_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : ℕ) (A : E →ₗ[ℝ] E) (x : PiLp 2 fun (x : Fin m) => E) : (piMapL2 m A) x = WithLp.toLp 2 fun (i : Fin m) => A (x.ofLp i)

theorem Graphon.Lovasz.piMapL2_selfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : ℕ) (A : E →ₗ[ℝ] E) (hA : ∀ (x y : E), inner ℝ (A x) y = inner ℝ x (A y)) (x y : PiLp 2 fun (x : Fin m) => E) : inner ℝ ((piMapL2 m A) x) y = inner ℝ x ((piMapL2 m A) y)

piMapL2 m A inherits self-adjointness from A.

theorem Graphon.Lovasz.piMapL2_pow_toLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : ℕ) (A : E →ₗ[ℝ] E) (q : ℕ) (w : Fin m → E) : (piMapL2 m A ^ q) (WithLp.toLp 2 w) = WithLp.toLp 2 fun (i : Fin m) => (A ^ q) (w i)

Powers of piMapL2 m A act componentwise as powers of A.

theorem Graphon.Lovasz.common_krylov_coefficients_fin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (m : ℕ) (A : E →ₗ[ℝ] E) (hA : ∀ (x y : E), inner ℝ (A x) y = inner ℝ x (A y)) {w : Fin m → E} (hw : ∀ (i : Fin m), w i ∈ A.range) : ∃ (s : Finset ℕ) (c : ℕ → ℝ), ∀ (i : Fin m), ∑ q ∈ s, c q • (A ^ (q + 1)) (w i) = w i

Common Krylov coefficients for a finite family (the k-fold direct-sum trick): if every member of a family w : Fin m → E lies in the range of a self-adjoint A, there are COMMON coefficients expressing each member as a combination of its own positive A-powers. Generalizes pair_mem_common_pos_power_span; obtained from the block operator on PiLp 2 (fun _ : Fin m => E) by projecting each coordinate.

Transport of the W-weighted form to Euclidean space

noncomputable def Graphon.Lovasz.sqrtScale {T : ℕ} (W f : Fin T → ℝ) : EuclideanSpace ℝ (Fin T)

√W-rescaling into EuclideanSpace ℝ (Fin T): an isometry from the wInner W form to the standard inner product (for W > 0).

Equations

• Graphon.Lovasz.sqrtScale W f = WithLp.toLp 2 fun (t : Fin T) => √(W t) * f t

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

The conjugated weighted adjacency, as a plain function: the symmetric matrix S(t,s) = √(W t) · B t s · √(W s) applied to x.

Equations

• Graphon.Lovasz.conjAdjFun B W x t = ∑ s : Fin T, √(W t) * B t s * √(W s) * x s

noncomputable def Graphon.Lovasz.conjAdj {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) : EuclideanSpace ℝ (Fin T) →ₗ[ℝ] EuclideanSpace ℝ (Fin T)

The conjugated weighted adjacency as a linear endomorphism of EuclideanSpace ℝ (Fin T).

Equations

• Graphon.Lovasz.conjAdj B W = { toFun := fun (x : EuclideanSpace ℝ (Fin T)) => WithLp.toLp 2 (Graphon.Lovasz.conjAdjFun B W x.ofLp), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Graphon.Lovasz.conjAdj_apply {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (x : EuclideanSpace ℝ (Fin T)) : (conjAdj B W) x = WithLp.toLp 2 (conjAdjFun B W x.ofLp)

theorem Graphon.Lovasz.inner_sqrtScale {T : ℕ} (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (f g : Fin T → ℝ) : inner ℝ (sqrtScale W f) (sqrtScale W g) = wInner W f g

sqrtScale carries wInner W to the Euclidean inner product.

theorem Graphon.Lovasz.conjAdj_sqrtScale {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (f : Fin T → ℝ) : (conjAdj B W) (sqrtScale W f) = sqrtScale W (weightedAdj B W f)

sqrtScale intertwines weightedAdj and conjAdj.

theorem Graphon.Lovasz.conjAdj_selfAdjoint {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (x y : EuclideanSpace ℝ (Fin T)) : inner ℝ ((conjAdj B W) x) y = inner ℝ x ((conjAdj B W) y)

conjAdj is self-adjoint for the Euclidean inner product (from hB).

theorem Graphon.Lovasz.conjAdj_pow_sqrtScale {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (q : ℕ) (f : Fin T → ℝ) : (conjAdj B W ^ q) (sqrtScale W f) = sqrtScale W (weightedAdjIter B W q f)

sqrtScale intertwines iterates: (conjAdj)^q ∘ sqrtScale = sqrtScale ∘ M^[q].

theorem Graphon.Lovasz.sqrtScale_injective {T : ℕ} (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) : Function.Injective (sqrtScale W)

sqrtScale is injective for positive weights.

theorem Graphon.Lovasz.sqrtScale_smul {T : ℕ} (W : Fin T → ℝ) (c : ℝ) (f : Fin T → ℝ) : sqrtScale W (c • f) = c • sqrtScale W f

sqrtScale commutes with scalar multiples.

theorem Graphon.Lovasz.sqrtScale_sum {T : ℕ} (W : Fin T → ℝ) {ι : Type u_1} (s : Finset ι) (F : ι → Fin T → ℝ) : sqrtScale W (∑ q ∈ s, F q) = ∑ q ∈ s, sqrtScale W (F q)

sqrtScale commutes with finite sums.

theorem Graphon.Lovasz.weightedAdj_pair_common_coeffs {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) {f g : Fin T → ℝ} (hf : ∃ (z : Fin T → ℝ), weightedAdj B W z = f) (hg : ∃ (z : Fin T → ℝ), weightedAdj B W z = g) : ∃ (s : Finset ℕ) (c : ℕ → ℝ), ∑ q ∈ s, c q • weightedAdjIter B W (q + 1) f = f ∧ ∑ q ∈ s, c q • weightedAdjIter B W (q + 1) g = g

Common Krylov coefficients in the weighted setting: if f and g both lie in the range of weightedAdj B W, there are COMMON coefficients expressing each as a combination of its own positive weightedAdjIter-powers. This is the algebraic core of the K₂,₃-arms cube proof (and of the k ≥ 4 lift): every slot of the multilinear polarization can be expanded with the SAME coefficient family.

Trilinear polarization — the graph-free cube core

noncomputable def Graphon.Lovasz.wTriple {T : ℕ} (W f g h : Fin T → ℝ) : ℝ

The weighted trilinear form T₃(f, g, h) = ∑ t, W t * f t * g t * h t.

Equations

• Graphon.Lovasz.wTriple W f g h = ∑ t : Fin T, W t * f t * g t * h t

theorem Graphon.Lovasz.wTriple_comm₁₂ {T : ℕ} (W f g h : Fin T → ℝ) : wTriple W f g h = wTriple W g f h

theorem Graphon.Lovasz.wTriple_comm₁₃ {T : ℕ} (W f g h : Fin T → ℝ) : wTriple W f g h = wTriple W h g f

theorem Graphon.Lovasz.wTriple_sum₁ {T : ℕ} {ι : Type u_1} (W : Fin T → ℝ) (s : Finset ι) (F : ι → Fin T → ℝ) (g h : Fin T → ℝ) : wTriple W (∑ a ∈ s, F a) g h = ∑ a ∈ s, wTriple W (F a) g h

theorem Graphon.Lovasz.wTriple_smul₁ {T : ℕ} (W : Fin T → ℝ) (r : ℝ) (f g h : Fin T → ℝ) : wTriple W (r • f) g h = r * wTriple W f g h

theorem Graphon.Lovasz.wTriple_sum₂ {T : ℕ} {ι : Type u_1} (W : Fin T → ℝ) (s : Finset ι) (f : Fin T → ℝ) (G : ι → Fin T → ℝ) (h : Fin T → ℝ) : wTriple W f (∑ b ∈ s, G b) h = ∑ b ∈ s, wTriple W f (G b) h

theorem Graphon.Lovasz.wTriple_smul₂ {T : ℕ} (W : Fin T → ℝ) (r : ℝ) (f g h : Fin T → ℝ) : wTriple W f (r • g) h = r * wTriple W f g h

theorem Graphon.Lovasz.wTriple_sum₃ {T : ℕ} {ι : Type u_1} (W : Fin T → ℝ) (s : Finset ι) (f g : Fin T → ℝ) (H : ι → Fin T → ℝ) : wTriple W f g (∑ d ∈ s, H d) = ∑ d ∈ s, wTriple W f g (H d)

theorem Graphon.Lovasz.wTriple_smul₃ {T : ℕ} (W : Fin T → ℝ) (r : ℝ) (f g h : Fin T → ℝ) : wTriple W f g (r • h) = r * wTriple W f g h

theorem Graphon.Lovasz.cube_gap_polarization {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i j : Fin T) : 4 * (∑ t : Fin T, W t * B i t ^ 3 - ∑ t : Fin T, W t * B j t ^ 3) = 3 * wTriple W (rowDiff B i j) (rowSum B i j) (rowSum B i j) + wTriple W (rowDiff B i j) (rowDiff B i j) (rowDiff B i j)

Pointwise cube factorization: 4·gap₃ = 3·T₃(ε, u, u) + T₃(ε, ε, ε) (from 4(x³ - y³) = 3(x-y)(x+y)² + (x-y)³).

theorem Graphon.Lovasz.rowDiff_eq_weightedAdj {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (i j : Fin T) : rowDiff B i j = weightedAdj B W fun (t : Fin T) => (if t = i then 1 else 0) / W t - (if t = j then 1 else 0) / W t

ε = rowDiff is also in the range of weightedAdj (mirror of rowSum_eq_weightedAdj).

noncomputable def Graphon.Lovasz.polarizedCubeObs {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i j : Fin T) (a b c : ℕ) : ℝ

The polarized cube observable (algebraic form): the trilinear polarization of the rooted K₂,₃-with-arms profile difference at arm lengths (a, b, c) — one ε-placement per root edge, plus the all-ε term. The graph slice will identify 4 · (the K₂,₃-arms profile difference) with this.

Equations

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

theorem Graphon.Lovasz.cubeGap_eq_zero_of_polarized_obs {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (i j : Fin T) (hobs : ∀ (a b c : ℕ), polarizedCubeObs B W i j (a + 1) (b + 1) (c + 1) = 0) : ∑ t : Fin T, W t * B i t ^ 3 = ∑ t : Fin T, W t * B j t ^ 3

The graph-free cube core: if every polarized cube observable (at positive arm lengths) vanishes, the cube gap is zero. With the (separate) graph slice identifying polarizedCubeObs with 4 · the rooted K₂,₃-arms profile difference, this reduces cubeMoment_descends_of_rootedProfileEquiv to pure graph plumbing.

k-linear polarization — the graph-free power-moment core (k ≥ 4 lift)

noncomputable def Graphon.Lovasz.wMulti {T : ℕ} (k : ℕ) (W : Fin T → ℝ) (f : Fin k → Fin T → ℝ) : ℝ

The weighted k-linear form T_k(f) = ∑ t, W t * ∏ l, f l t (the Fin k-slot generalization of wTriple).

Equations

• Graphon.Lovasz.wMulti k W f = ∑ t : Fin T, W t * ∏ l : Fin k, f l t

theorem Graphon.Lovasz.wMulti_expansion {T : ℕ} {ι : Type u_1} [DecidableEq ι] (k : ℕ) (W : Fin T → ℝ) (s : Finset ι) (c : ι → ℝ) (F : Fin k → ι → Fin T → ℝ) (f : Fin k → Fin T → ℝ) (hf : ∀ (l : Fin k), ∑ a ∈ s, c a • F l a = f l) : wMulti k W f = ∑ φ ∈ Fintype.piFinset fun (x : Fin k) => s, (∏ l : Fin k, c (φ l)) * wMulti k W fun (l : Fin k) => F l (φ l)

Multilinear expansion with common coefficients (k-ary analog of wTriple_triple_expansion, in one shot via Finset.prod_univ_sum): a k-linear form whose every slot has a shared-coefficient finite expansion equals the sum over coefficient tuples of weighted evaluations.

theorem Graphon.Lovasz.pow_gap_polarization {T : ℕ} (k : ℕ) (W f g : Fin T → ℝ) : 2 ^ k * (∑ t : Fin T, W t * f t ^ k - ∑ t : Fin T, W t * g t ^ k) = 2 * ∑ S ∈ Finset.univ.powerset with Odd S.card, wMulti k W fun (l : Fin k) => if l ∈ S then fun (t : Fin T) => f t - g t else fun (t : Fin T) => f t + g t

k-th power-gap polarization (sum form): the weighted power-moment gap polarizes into the odd-subset wMulti evaluations of (ε, u)-slot assignments.

noncomputable def Graphon.Lovasz.polarizedPowObs {T : ℕ} (k : ℕ) (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i j : Fin T) (φ : Fin k → ℕ) : ℝ

The polarized k-th power observable: the odd-subset polarization of the rooted K₂,ₖ-arms profile difference at arm-length vector φ (the k-ary generalization of polarizedCubeObs; the graph slice will identify 2^(k-1) · the K₂,ₖ-arms profile difference with this).

Equations

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

theorem Graphon.Lovasz.powGap_eq_zero_of_polarized_obs {T : ℕ} (k : ℕ) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (i j : Fin T) (hobs : ∀ (φ : Fin k → ℕ), (polarizedPowObs k B W i j fun (l : Fin k) => φ l + 1) = 0) : ∑ t : Fin T, W t * B i t ^ k = ∑ t : Fin T, W t * B j t ^ k

The graph-free k-th power core: if every polarized k-th power observable at positive arm lengths vanishes, the k-th power-moment gap is zero. With the (since-proved) graph slice identifying polarizedPowObs with 2^(k-1) · the rooted K₂,ₖ-arms profile difference, this reduces powerSum_descends_of_rootedProfileEquiv (k ≥ 4) to pure graph plumbing.

theorem Graphon.Lovasz.wInner_eq_zero_of_iter_orthogonal {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (eps u : Fin T → ℝ) (hu : ∃ (z : Fin T → ℝ), weightedAdj B W z = u) (hortho : ∀ (q : ℕ), wInner W eps (weightedAdjIter B W (q + 1) u) = 0) : wInner W eps u = 0

The weighted Krylov-kernel lemma (target shape of the spectral slice): if u is in the range of weightedAdj B W and eps is wInner-orthogonal to all positive weightedAdjIter-iterates of u, then eps ⊥ u.

The assembled spectral slice

theorem Graphon.Lovasz.sqMoment_eq_of_closedWalkProfile_eq {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (i j : Fin T) (hcw : ∀ (m : ℕ), closedWalkProfile B W i (m + 3) = closedWalkProfile B W j (m + 3)) : sqMoment B W i = sqMoment B W j

Square moments from closed walks — the spectral slice of the cycle–Krylov proof, fully assembled: if two vertices have equal closed-walk profiles at every length ≥ 3, their W-weighted square moments agree.

Combines (from SimpleRank.lean): sqMoment_sub_eq_wInner (gap = ⟪ε, u⟫_W), rowSum_eq_weightedAdj (u ∈ Im M), closedWalkProfile_sub_eq_wInner (closed-walk diffs = ⟪ε, M^[q] u⟫_W), and the weighted Krylov-kernel lemma above. The remaining content of sqMoment_descends_of_rootedProfileEquiv is graph plumbing: rooted cycles realize closedWalkProfile (rootedProfile_rootedCycleGraph_eq_closedWalkProfile, formerly a focused sorry in Lovasz.lean, since proved there), and rpe makes their profiles agree.

The assembled theorem: square-moment descent

theorem Graphon.Lovasz.sqMoment_descends_of_rootedProfileEquiv {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) {i j : Fin T} (h : rootedProfileEquiv B W i j) : sqMoment B W i = sqMoment B W j

Square-moment descent (#70 minimal test case) — PROVED.

If i and j are rooted-profile equivalent (twin-freeness NOT needed), their W-weighted square moments agree. This was the designated first obstruction beyond the simple rooted algebra: ∑ t, W t * B i t ^ 2 is inherently a multigraph observable (double edge i–t), yet rooted simple CYCLES pin it.

Assembly of the cycle–Krylov–kernel proof (docs/sqmoment-cycle-krylov.md): rpe applied to rootedCycleGraph (m+1) + the bridge rootedProfile_rootedCycleGraph_eq_closedWalkProfile (proved in Lovasz.lean) give equal closed-walk profiles at all lengths ≥ 3, and sqMoment_eq_of_closedWalkProfile_eq (the spectral slice) concludes.

Supersedes the version formerly in SimpleRank.lean that was derived from the (then still open, strictly stronger — since proved below) classwise_sqMoment_descends; this proof is sorry-free and drops the htwin hypothesis.

The K₂,₃-with-arms graph family (the cube's graph bridge)

Vertex layout on Fin (4 + a + b + c + 1): 0 the root, 1, 2, 3 the anchors (root-adjacent), 4 the hub, then three internal blocks of sizes a, b, c (so the arm from anchor l + 1 to the hub has length armLen + 1 ≥ 1 — positive arm lengths by construction, matching the (a+1, b+1, c+1) indices of polarizedCubeObs).

def Graphon.Lovasz.armLen (a b c l : ℕ) : ℕ

Internal count of arm l ∈ {0,1,2}.

Equations

• Graphon.Lovasz.armLen a b c l = if l = 0 then a else if l = 1 then b else c

def Graphon.Lovasz.armStart (a b l : ℕ) : ℕ

Start of the internal block of arm l ∈ {0,1,2} (as a raw value).

Equations

• Graphon.Lovasz.armStart a b l = if l = 0 then 5 else if l = 1 then 5 + a else 5 + a + b

def Graphon.Lovasz.armSeq (a b c l s : ℕ) : ℕ

The s-th vertex value along arm l: s = 0 is the anchor l + 1, steps 1 .. armLen are the internals, s = armLen + 1 is the hub 4.

Equations

• Graphon.Lovasz.armSeq a b c l s = if s = 0 then l + 1 else if s ≤ Graphon.Lovasz.armLen a b c l then Graphon.Lovasz.armStart a b l + s - 1 else 4

def Graphon.Lovasz.k23Arms (a b c : ℕ) : SimpleGraph (Fin (4 + a + b + c + 1))

The rooted K₂,₃-with-arms graph: root 0 adjacent to anchors 1, 2, 3; arm l a path of length armLen + 1 from anchor l + 1 to the hub 4.

Equations

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

@[implicit_reducible]

instance Graphon.Lovasz.instDecidableRelFinHAddNatOfNatAdjK23Arms (a b c : ℕ) : DecidableRel (k23Arms a b c).Adj

Equations

• Graphon.Lovasz.instDecidableRelFinHAddNatOfNatAdjK23Arms a b c u v = id inferInstance

theorem Graphon.Lovasz.armSeq_lt (a b c : ℕ) {l s : ℕ} (hl : l < 3) (hs : s ≤ armLen a b c l + 1) : armSeq a b c l s < 4 + a + b + c + 1

Arm vertices stay in range.

theorem Graphon.Lovasz.armSeq_pos (a b c : ℕ) {l s : ℕ} (hl : l < 3) : 0 < armSeq a b c l s

Arm vertices are never the root.

@[reducible, inline]

abbrev Graphon.Lovasz.K23EdgeIdx (a b c : ℕ) : Type

The edge index type of k23Arms: three root edges plus, per arm, armLen + 1 chain edges.

Equations

• Graphon.Lovasz.K23EdgeIdx a b c = (Fin 3 ⊕ (l : Fin 3) × Fin (Graphon.Lovasz.armLen a b c ↑l + 1))

def Graphon.Lovasz.k23Edge (a b c : ℕ) : K23EdgeIdx a b c → Sym2 (Fin (4 + a + b + c + 1))

The edge family of k23Arms, indexed by K23EdgeIdx.

Equations

• Graphon.Lovasz.k23Edge a b c (Sum.inl l) = s(0, ⟨↑l + 1, ⋯⟩)
• Graphon.Lovasz.k23Edge a b c (Sum.inr ⟨l, s⟩) = s(⟨Graphon.Lovasz.armSeq a b c ↑l ↑s, ⋯⟩, ⟨Graphon.Lovasz.armSeq a b c (↑l) (↑s + 1), ⋯⟩)

theorem Graphon.Lovasz.k23Edge_mem (a b c : ℕ) (idx : K23EdgeIdx a b c) : k23Edge a b c idx ∈ (k23Arms a b c).edgeSet

Every indexed edge is an edge of k23Arms.

theorem Graphon.Lovasz.k23Arms_edgeFinset (a b c : ℕ) : (k23Arms a b c).edgeFinset = Finset.image (k23Edge a b c) Finset.univ

Edge classification for k23Arms (reusable form): the edge finset is the image of the indexed family — three root-anchor edges plus the three anchor-to-hub arm chains, and nothing else.

theorem Graphon.Lovasz.k23Edge_injective (a b c : ℕ) : Function.Injective (k23Edge a b c)

The indexed edge family is injective (no duplicate edges).

theorem Graphon.Lovasz.k23Arms_prod_eq {T : ℕ} (a b c : ℕ) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (τ : Fin (4 + a + b + c + 1) → Fin T) : ∏ e ∈ (k23Arms a b c).edgeFinset, B (τ (Quot.out e).1) (τ (Quot.out e).2) = (∏ l : Fin 3, B (τ 0) (τ ⟨↑l + 1, ⋯⟩)) * ∏ l : Fin 3, ∏ s : Fin (armLen a b c ↑l + 1), B (τ ⟨armSeq a b c ↑l ↑s, ⋯⟩) (τ ⟨armSeq a b c (↑l) (↑s + 1), ⋯⟩)

Edge-product factorization for k23Arms: the edge product splits into the three root-edge factors times the three independent arm-chain products.

One-arm chain collapse

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

The (q+1)-edge arm kernel from x to y (q internal vertices), defined recursively — the normal form the internal sums collapse to.

Equations

• Graphon.Lovasz.armSum B W 0 x✝¹ x✝ = B x✝¹ x✝
• Graphon.Lovasz.armSum B W q.succ x✝¹ x✝ = ∑ t : Fin T, W t * B x✝¹ t * Graphon.Lovasz.armSum B W q t x✝

def Graphon.Lovasz.chainPath {T : ℕ} (q : ℕ) (x y : Fin T) (σ : Fin q → Fin T) (s : ℕ) : Fin T

Path-position function for a free-standing arm: 0 ↦ x, 1..q ↦ σ, q+1 ↦ y (the Fin T-valued mirror of armSeq).

Equations

• Graphon.Lovasz.chainPath q x y σ s = if h0 : s = 0 then x else if h : s ≤ q then σ ⟨s - 1, ⋯⟩ else y

theorem Graphon.Lovasz.armChain_sum_eq_armSum {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (q : ℕ) (x y : Fin T) : ∑ σ : Fin q → Fin T, (∏ k : Fin q, W (σ k)) * ∏ s : Fin (q + 1), B (chainPath q x y σ ↑s) (chainPath q x y σ (↑s + 1)) = armSum B W q x y

One-arm collapse: summing the internal vertices of an arm chain gives the recursive kernel armSum.

theorem Graphon.Lovasz.sum_weight_mul_armSum {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (q : ℕ) (f : Fin T → ℝ) (y : Fin T) : ∑ x : Fin T, W x * f x * armSum B W q x y = weightedAdjIter B W (q + 1) f y

One-arm collapse, weighted form (the consumer shape): summing the anchor against the root edge and the arm kernel yields weightedAdjIter at the hub.

Block-structured assignments (the global split)

def Graphon.Lovasz.appendFn {T m n : ℕ} (σ₁ : Fin m → Fin T) (σ₂ : Fin n → Fin T) : Fin (m + n) → Fin T

Concatenation of two assignment blocks (dif-based, so the value lemmas are definitional — no castAdd/natAdd juggling downstream).

Equations

• Graphon.Lovasz.appendFn σ₁ σ₂ i = if h : ↑i < m then σ₁ ⟨↑i, h⟩ else σ₂ ⟨↑i - m, ⋯⟩

theorem Graphon.Lovasz.appendFn_low {T m n : ℕ} (σ₁ : Fin m → Fin T) (σ₂ : Fin n → Fin T) {i : Fin (m + n)} (h : ↑i < m) : appendFn σ₁ σ₂ i = σ₁ ⟨↑i, h⟩

theorem Graphon.Lovasz.appendFn_high {T m n : ℕ} (σ₁ : Fin m → Fin T) (σ₂ : Fin n → Fin T) {i : Fin (m + n)} (h : ¬↑i < m) : appendFn σ₁ σ₂ i = σ₂ ⟨↑i - m, ⋯⟩

def Graphon.Lovasz.appendEquiv (T m n : ℕ) : (Fin m → Fin T) × (Fin n → Fin T) ≃ (Fin (m + n) → Fin T)

The block-splitting equivalence for assignment spaces.

Equations

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

theorem Graphon.Lovasz.sum_fin_split {T : ℕ} {β : Type u_1} [AddCommMonoid β] (m n : ℕ) (f : (Fin (m + n) → Fin T) → β) : ∑ σ : Fin (m + n) → Fin T, f σ = ∑ σ₁ : Fin m → Fin T, ∑ σ₂ : Fin n → Fin T, f (appendFn σ₁ σ₂)

Sum splitting along a block decomposition of the assignment space.

theorem Graphon.Lovasz.prod_appendFn {T m n : ℕ} (g : Fin T → ℝ) (σ₁ : Fin m → Fin T) (σ₂ : Fin n → Fin T) : ∏ u : Fin (m + n), g (appendFn σ₁ σ₂ u) = (∏ u : Fin m, g (σ₁ u)) * ∏ u : Fin n, g (σ₂ u)

Weight-product splitting along a block decomposition.

def Graphon.Lovasz.k23Assign {T : ℕ} (a b c : ℕ) (x : Fin 3 → Fin T) (h₁ : Fin 1 → Fin T) (σa : Fin a → Fin T) (σb : Fin b → Fin T) (σc : Fin c → Fin T) : Fin (4 + a + b + c) → Fin T

The structured K₂,₃-arms assignment: anchors, hub, and the three internal arm blocks, assembled into a flat assignment.

Equations

• Graphon.Lovasz.k23Assign a b c x h₁ σa σb σc = Graphon.Lovasz.appendFn (Graphon.Lovasz.appendFn (Graphon.Lovasz.appendFn (Graphon.Lovasz.appendFn x h₁) σa) σb) σc

theorem Graphon.Lovasz.k23Assign_anchor {T : ℕ} (a b c : ℕ) (x : Fin 3 → Fin T) (h₁ : Fin 1 → Fin T) (σa : Fin a → Fin T) (σb : Fin b → Fin T) (σc : Fin c → Fin T) {j : ℕ} (hj : j < 3) : k23Assign a b c x h₁ σa σb σc ⟨j, ⋯⟩ = x ⟨j, hj⟩

Reconstruction: anchor values.

theorem Graphon.Lovasz.k23Assign_hub {T : ℕ} (a b c : ℕ) (x : Fin 3 → Fin T) (h₁ : Fin 1 → Fin T) (σa : Fin a → Fin T) (σb : Fin b → Fin T) (σc : Fin c → Fin T) : k23Assign a b c x h₁ σa σb σc ⟨3, ⋯⟩ = h₁ 0

Reconstruction: the hub value.

theorem Graphon.Lovasz.k23Assign_arm0 {T : ℕ} (a b c : ℕ) (x : Fin 3 → Fin T) (h₁ : Fin 1 → Fin T) (σa : Fin a → Fin T) (σb : Fin b → Fin T) (σc : Fin c → Fin T) {k : ℕ} (hk : k < a) : k23Assign a b c x h₁ σa σb σc ⟨4 + k, ⋯⟩ = σa ⟨k, hk⟩

Reconstruction: arm-0 internal values.

theorem Graphon.Lovasz.k23Assign_arm1 {T : ℕ} (a b c : ℕ) (x : Fin 3 → Fin T) (h₁ : Fin 1 → Fin T) (σa : Fin a → Fin T) (σb : Fin b → Fin T) (σc : Fin c → Fin T) {k : ℕ} (hk : k < b) : k23Assign a b c x h₁ σa σb σc ⟨4 + a + k, ⋯⟩ = σb ⟨k, hk⟩

Reconstruction: arm-1 internal values.

theorem Graphon.Lovasz.k23Assign_arm2 {T : ℕ} (a b c : ℕ) (x : Fin 3 → Fin T) (h₁ : Fin 1 → Fin T) (σa : Fin a → Fin T) (σb : Fin b → Fin T) (σc : Fin c → Fin T) {k : ℕ} (hk : k < c) : k23Assign a b c x h₁ σa σb σc ⟨4 + a + b + k, ⋯⟩ = σc ⟨k, hk⟩

Reconstruction: arm-2 internal values.

theorem Graphon.Lovasz.k23Arms_eval {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (v : Fin T) (a b c : ℕ) : rootedProfile B W v (k23Arms a b c) = wTriple W (weightedAdjIter B W (a + 1) fun (t : Fin T) => B v t) (weightedAdjIter B W (b + 1) fun (t : Fin T) => B v t) (weightedAdjIter B W (c + 1) fun (t : Fin T) => B v t)

Raw evaluation of the K₂,₃-arms profile (PROVED — the brittle Fin/edge-product slice, isolated here per plan; an earlier revision carried a SORRY marker while the plumbing was pending): the rooted profile factorizes through the hub as a wTriple of weightedAdjIters of the root's row. Mathematically: summing each arm's internals gives the walk kernel K_{armLen+1}(anchor, hub); summing each anchor against its root edge gives (M^{armLen+1} (B v ·))(hub); the hub sum is wTriple. Machine-precision validated in scripts/validate_cube_k23_arms.py.

theorem Graphon.Lovasz.weightedAdj_sub {T : ℕ} (B : Fin T → Fin T → ℝ) (W f g : Fin T → ℝ) : (weightedAdj B W fun (t : Fin T) => f t - g t) = fun (t : Fin T) => weightedAdj B W f t - weightedAdj B W g t

weightedAdj is subtractive (mirror of weightedAdj_add).

theorem Graphon.Lovasz.weightedAdjIter_sub {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (q : ℕ) (f g : Fin T → ℝ) : (weightedAdjIter B W q fun (t : Fin T) => f t - g t) = fun (t : Fin T) => weightedAdjIter B W q f t - weightedAdjIter B W q g t

Iterates of weightedAdj are subtractive.

theorem Graphon.Lovasz.rootedProfile_k23Arms_sub_eq_polarizedCubeObs {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (i j : Fin T) (a b c : ℕ) : 4 * (rootedProfile B W i (k23Arms a b c) - rootedProfile B W j (k23Arms a b c)) = polarizedCubeObs B W i j (a + 1) (b + 1) (c + 1)

The cube's graph bridge (proved modulo k23Arms_eval): 4 · the K₂,₃-arms profile difference is exactly the polarized cube observable at arm lengths (a+1, b+1, c+1).

The Hadamard-power lift (historical planning note; since closed)

Historical note (resolved): this section's "open content" has since been closed — powerSum_descends_of_rootedProfileEquiv is proved below for ALL k (k = 3 via the K₂,₃-arms bridge, k ≥ 4 via the K₂,ₖ-arms bridge). The analysis below is retained as the design record.

With the square moment closed, the route to the full rank theorem vertexOrbitRel_of_rootedProfileEquiv runs through ALL weighted power sums of the rows: powerSum_descends_of_rootedProfileEquiv below (k ≥ 3 was the open content), then weighted_powersum_determines_measure (proved, in Lovasz.lean) recovers equality of the W-weighted row-value measures (rowValueMeasure_eq_of_rootedProfileEquiv).

Status of k ≥ 3 at the time (then the genuine open math): writing ε = B i - B j, the gap is ⟨ε, ρᵢ^{∘(k-1)} + ρᵢ^{∘(k-2)}∘ρⱼ + ⋯ + ρⱼ^{∘(k-1)}⟩_W (Hadamard powers of the rows). The available rpe-killed observables with d root edges give d-leg kernels from the Hadamard-ordinary closure of walk kernels (theta graphs; at most ONE bare-B factor per Hadamard bundle — parallel edges are multigraph). The k = 2 proof recovered the forbidden diagonal 2-tensor via u ∈ Im M; k ≥ 3 needs the analogous recovery of the diagonal k-tensor, one level up. Note B^{∘(k-1)} itself is NOT in the observable kernel algebra (even off the root), so the lift is a genuine extension, not a substitution.

theorem Graphon.Lovasz.cubeMoment_descends_of_rootedProfileEquiv {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) {i j : Fin T} (h : rootedProfileEquiv B W i j) : ∑ t : Fin T, W t * B i t ^ 3 = ∑ t : Fin T, W t * B j t ^ 3

Cube-moment descent — MATHEMATICALLY RESOLVED (2026-06-10); formalization COMPLETE (an earlier revision carried a SORRY marker pending the K₂,₃-arms plumbing, which has since landed — see k23Arms_eval and rootedProfile_k23Arms_sub_eq_polarizedCubeObs).

The K₂,₃-ARMS proof (machine-precision validated, scripts/validate_cube_k23_arms.py; mechanism UNIFORM in k — at k = 2 the K₂,₂-with-arms graph IS the rooted cycle, recovering the proved case):

1. Arms identity: for the rooted K₂,₃-with-arms graph (root adjacent to anchors t₁,t₂,t₃; internal hub y; arm l a path of length a_l ≥ 1 from t_l to y — a SIMPLE graph), the profile difference is exactly (1/4)·Σ_{|S| odd} T₃(M^{a_l}ε [l∈S], M^{a_l}u [l∉S]) where T₃(f,g,h) = ∑ t, W t * f t * g t * h t (trilinear polarization of the three root edges; arms act as M-powers). rpe kills these for all arms.
2. Common expansion (direct-sum trick): (ε, u) ∈ Im (M ⊕ M), self-adjoint, so the k = 2 projection lemma applied to E ⊕ E yields COMMON coefficients c_q with ε = Σ_{q≥1} c_q M^q ε AND u = Σ_{q≥1} c_q M^q u simultaneously.
3. Reconstruction: gap₃ = (1/4)·Σ_{|S| odd} T₃(ε[S], u[S^c]) = Σ_{a⃗≥1} c_{a₁}c_{a₂}c_{a₃} · ObsDiff(a⃗) = 0. ∎ Only hB, hW needed.

How it was found: the LM falsification run (k=2 harness, cube gap pinned) went infeasible at T=4 already at the base m≤3 family; at T=5 it was exactly feasible at m≤3 and the top m=4 separators were the four rooted K₂,₃'s — identifying the family, after which the identity is three lines.

Superseded analysis (kept as history; the earlier residual-branch frontier is BYPASSED by the right family): in eigenbasis coordinates the theta/wedge/ triangle-wedge families force F ≡ 0 generically but left open the branch G = 0 ∧ f_λf_μ = -g_λg_μ ≠ 0 ∧ F ≠ 0; the K₂,₃-arms constraints close the gap without case analysis.

Formalization plan (as executed): trilinear polarization lemma (generalizing wInner_sub_iter_add), the direct-sum common-coefficient lemma (from inner_eq_zero_of_orthogonal_pos_powers's projection core applied to E ⊕ E — extract the span-membership statement), and the K₂,₃-arms graph family + evaluation bridge (generalizing rootedCycleGraph + rootedProfile_rootedCycleGraph_eq_closedWalkProfile).

The K₂,ₖ-with-arms family (k ≥ 4 lift) — structured-vertex design

The cube case used k23Arms, a SimpleGraph (Fin (4 + a + b + c + 1)) built from explicit offset arithmetic (armSeq, armStart, nested appendFn). That layout does not scale to an arbitrary number k of arms: the dependent block offsets become unmanageable.

Instead we reason on a structured finite vertex type K2kVertex k armLen and transport the graph to Fin (n + 1) only at the boundary forced by rootedProfile, which is hardwired to SimpleGraph (Fin (n + 1)) with the root at position 0. All human reasoning stays on the constructors; the Fin version is a pure transport artifact (SimpleGraph.comap along an equivalence that pins the root to 0).

inductive Graphon.Lovasz.K2kVertex (k : ℕ) (armLen : Fin k → ℕ) : Type

Structured vertex type of the rooted K₂,ₖ-with-arms graph: a root, one anchor per arm l : Fin k, a shared hub, and armLen l internal vertices on arm l. Arm l is the path anchor l — internal l 0 — ⋯ — internal l (armLen l - 1) — hub (when armLen l = 0 the arm degenerates to the single edge anchor l — hub).

• root {k : ℕ} {armLen : Fin k → ℕ} : K2kVertex k armLen
• anchor {k : ℕ} {armLen : Fin k → ℕ} (l : Fin k) : K2kVertex k armLen
• hub {k : ℕ} {armLen : Fin k → ℕ} : K2kVertex k armLen
• internal {k : ℕ} {armLen : Fin k → ℕ} (l : Fin k) (s : Fin (armLen l)) : K2kVertex k armLen

@[implicit_reducible]

instance Graphon.Lovasz.instDecidableEqK2kVertex {k✝ : ℕ} {armLen✝ : Fin k✝ → ℕ} : DecidableEq (K2kVertex k✝ armLen✝)

Equations

• Graphon.Lovasz.instDecidableEqK2kVertex = Graphon.Lovasz.instDecidableEqK2kVertex.decEq

def Graphon.Lovasz.instDecidableEqK2kVertex.decEq {k✝ : ℕ} {armLen✝ : Fin k✝ → ℕ} (x✝ x✝¹ : K2kVertex k✝ armLen✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq Graphon.Lovasz.K2kVertex.root Graphon.Lovasz.K2kVertex.root = isTrue ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq Graphon.Lovasz.K2kVertex.root (Graphon.Lovasz.K2kVertex.anchor l) = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq Graphon.Lovasz.K2kVertex.root Graphon.Lovasz.K2kVertex.hub = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq Graphon.Lovasz.K2kVertex.root (Graphon.Lovasz.K2kVertex.internal l s) = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq (Graphon.Lovasz.K2kVertex.anchor l) Graphon.Lovasz.K2kVertex.root = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq (Graphon.Lovasz.K2kVertex.anchor a) (Graphon.Lovasz.K2kVertex.anchor b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq (Graphon.Lovasz.K2kVertex.anchor l) Graphon.Lovasz.K2kVertex.hub = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq (Graphon.Lovasz.K2kVertex.anchor l) (Graphon.Lovasz.K2kVertex.internal l_1 s) = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq Graphon.Lovasz.K2kVertex.hub Graphon.Lovasz.K2kVertex.root = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq Graphon.Lovasz.K2kVertex.hub (Graphon.Lovasz.K2kVertex.anchor l) = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq Graphon.Lovasz.K2kVertex.hub Graphon.Lovasz.K2kVertex.hub = isTrue ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq Graphon.Lovasz.K2kVertex.hub (Graphon.Lovasz.K2kVertex.internal l s) = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq (Graphon.Lovasz.K2kVertex.internal l s) Graphon.Lovasz.K2kVertex.root = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq (Graphon.Lovasz.K2kVertex.internal l s) (Graphon.Lovasz.K2kVertex.anchor l_1) = isFalse ⋯
• Graphon.Lovasz.instDecidableEqK2kVertex.decEq (Graphon.Lovasz.K2kVertex.internal l s) Graphon.Lovasz.K2kVertex.hub = isFalse ⋯

@[reducible, inline]

abbrev Graphon.Lovasz.K2kRest (k : ℕ) (armLen : Fin k → ℕ) : Type

The NON-root vertices of K2kVertex as an explicit Fintype: anchors ⊕ hub ⊕ internals. Carries the cardinality computation and lets us pin the root to position 0 of the Fin transport.

Equations

• Graphon.Lovasz.K2kRest k armLen = (Fin k ⊕ Unit ⊕ (l : Fin k) × Fin (armLen l))

def Graphon.Lovasz.k2kVertexOptionEquiv (k : ℕ) (armLen : Fin k → ℕ) : K2kVertex k armLen ≃ Option (K2kRest k armLen)

K2kVertex is root adjoined to K2kRest (root ↦ none). This single equivalence supplies the Fintype instance and pins the root for the Fin transport.

Equations

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

@[implicit_reducible]

instance Graphon.Lovasz.instFintypeK2kVertex (k : ℕ) (armLen : Fin k → ℕ) : Fintype (K2kVertex k armLen)

Equations

• Graphon.Lovasz.instFintypeK2kVertex k armLen = Fintype.ofEquiv (Option (Graphon.Lovasz.K2kRest k armLen)) (Graphon.Lovasz.k2kVertexOptionEquiv k armLen).symm

def Graphon.Lovasz.k2kRestCard (k : ℕ) (armLen : Fin k → ℕ) : ℕ

Number of NON-root vertices: k anchors + 1 hub + ∑ armLen internals.

Equations

• Graphon.Lovasz.k2kRestCard k armLen = k + 1 + ∑ l : Fin k, armLen l

theorem Graphon.Lovasz.k2kRest_card (k : ℕ) (armLen : Fin k → ℕ) : Fintype.card (K2kRest k armLen) = k2kRestCard k armLen

noncomputable def Graphon.Lovasz.K2kVertex_equivFin (k : ℕ) (armLen : Fin k → ℕ) : K2kVertex k armLen ≃ Fin (k2kRestCard k armLen + 1)

Vertex equivalence to Fin (n + 1) with the root pinned to 0 — the position simpleEvalAt/rootedProfile fix to the labelled vertex. Built as K2kVertex ≃ Option (K2kRest) ≃ Option (Fin n) ≃ Fin (n + 1); the last step (finSuccEquiv n).symm sends none ↦ 0, and the root is the unique preimage of none.

Equations

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

@[simp]

theorem Graphon.Lovasz.K2kVertex_equivFin_root (k : ℕ) (armLen : Fin k → ℕ) : (K2kVertex_equivFin k armLen) K2kVertex.root = 0

def Graphon.Lovasz.K2kVertex.armNode (k : ℕ) (armLen : Fin k → ℕ) (l : Fin k) (s : ℕ) : K2kVertex k armLen

The s-th vertex along arm l: 0 ↦ anchor, 1 .. armLen ↦ internal, anything beyond armLen ↦ hub. The structured analogue of armSeq, valued in the constructors (no Fin-offset arithmetic). When armLen l = 0 the chain is just anchor l —(s=0)→ hub —(s=1)→ hub, i.e. the single edge anchor l — hub.

Equations

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

theorem Graphon.Lovasz.K2kVertex.armNode_succ_ne (k : ℕ) (armLen : Fin k → ℕ) (l : Fin k) {s : ℕ} (hs : s ≤ armLen l) : armNode k armLen l s ≠ armNode k armLen l (s + 1)

Consecutive arm vertices differ (needed for loopless).

def Graphon.Lovasz.k2kArmsStructured (k : ℕ) (armLen : Fin k → ℕ) : SimpleGraph (K2kVertex k armLen)

The structured rooted K₂,ₖ-with-arms graph on K2kVertex k armLen: the root is adjacent to every anchor l; arm l is the path anchor l — internal l 0 — ⋯ — internal l (armLen l - 1) — hub (the consecutive pairs armNode l s — armNode l (s+1) for s ≤ armLen l). All reasoning about the family happens here; the Fin version k2kArms is a transport of this.

Equations

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

@[implicit_reducible]

instance Graphon.Lovasz.instDecidableRelK2kVertexAdjK2kArmsStructured (k : ℕ) (armLen : Fin k → ℕ) : DecidableRel (k2kArmsStructured k armLen).Adj

Equations

• Graphon.Lovasz.instDecidableRelK2kVertexAdjK2kArmsStructured k armLen x✝¹ x✝ = id inferInstance

noncomputable def Graphon.Lovasz.k2kArms (k : ℕ) (armLen : Fin k → ℕ) : SimpleGraph (Fin (k2kRestCard k armLen + 1))

The Fin-indexed K₂,ₖ-with-arms graph consumed by rootedProfile: the structured graph pulled back along the root-pinned equivalence. Because K2kVertex_equivFin .root = 0, position 0 of Fin (n + 1) is the root — the position simpleEvalAt/rootedProfile fix to the labelled vertex.

Equations

• Graphon.Lovasz.k2kArms k armLen = SimpleGraph.comap (⇑(Graphon.Lovasz.K2kVertex_equivFin k armLen).symm) (Graphon.Lovasz.k2kArmsStructured k armLen)

@[implicit_reducible]

noncomputable instance Graphon.Lovasz.instDecidableRelFinHAddNatK2kRestCardOfNatAdjK2kArms (k : ℕ) (armLen : Fin k → ℕ) : DecidableRel (k2kArms k armLen).Adj

Equations

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

@[reducible, inline]

abbrev Graphon.Lovasz.K2kEdgeIdx (k : ℕ) (armLen : Fin k → ℕ) : Type

The edge index type of k2kArmsStructured: k root-anchor edges plus, per arm l, the armLen l + 1 chain edges.

Equations

• Graphon.Lovasz.K2kEdgeIdx k armLen = (Fin k ⊕ (l : Fin k) × Fin (armLen l + 1))

def Graphon.Lovasz.k2kEdge (k : ℕ) (armLen : Fin k → ℕ) : K2kEdgeIdx k armLen → Sym2 (K2kVertex k armLen)

The edge family of k2kArmsStructured, indexed by K2kEdgeIdx.

Equations

• Graphon.Lovasz.k2kEdge k armLen (Sum.inl l) = s(Graphon.Lovasz.K2kVertex.root, Graphon.Lovasz.K2kVertex.anchor l)
• Graphon.Lovasz.k2kEdge k armLen (Sum.inr ⟨l, s⟩) = s(Graphon.Lovasz.K2kVertex.armNode k armLen l ↑s, Graphon.Lovasz.K2kVertex.armNode k armLen l (↑s + 1))

theorem Graphon.Lovasz.k2kEdge_mem (k : ℕ) (armLen : Fin k → ℕ) (idx : K2kEdgeIdx k armLen) : k2kEdge k armLen idx ∈ (k2kArmsStructured k armLen).edgeSet

Every indexed edge is an edge of k2kArmsStructured.

theorem Graphon.Lovasz.k2kArmsStructured_edgeFinset (k : ℕ) (armLen : Fin k → ℕ) : (k2kArmsStructured k armLen).edgeFinset = Finset.image (k2kEdge k armLen) Finset.univ

Edge classification for the K₂,ₖ-with-arms family: the edge finset is exactly the image of the indexed family k2kEdge — the k root-anchor edges plus the k arm chains, and nothing else. This is the structured, reusable form (the analogue of k23Arms_edgeFinset); the eventual k2kArms_eval will reindex the edge product of the Fin graph through this.

Commit 1 — Fin/structured edge transport + edge-product factorization

def Graphon.Lovasz.K2kVertex.armOf {k : ℕ} {armLen : Fin k → ℕ} : K2kVertex k armLen → Option (Fin k)

Arm index of a vertex (anchors/internals carry their arm; root/hub none). Used to recover (l, s) from a chain endpoint in k2kEdge_injective.

Equations

• Graphon.Lovasz.K2kVertex.root.armOf = none
• (Graphon.Lovasz.K2kVertex.anchor l).armOf = some l
• Graphon.Lovasz.K2kVertex.hub.armOf = none
• (Graphon.Lovasz.K2kVertex.internal l s).armOf = some l

def Graphon.Lovasz.K2kVertex.stepOf {k : ℕ} {armLen : Fin k → ℕ} : K2kVertex k armLen → ℕ

Step (depth) of a vertex along its arm (0 for anchor, s+1 for internal s); 0 on root/hub (irrelevant there).

Equations

• Graphon.Lovasz.K2kVertex.root.stepOf = 0
• (Graphon.Lovasz.K2kVertex.anchor l).stepOf = 0
• Graphon.Lovasz.K2kVertex.hub.stepOf = 0
• (Graphon.Lovasz.K2kVertex.internal l s).stepOf = ↑s + 1

theorem Graphon.Lovasz.K2kVertex.armOf_armNode {k : ℕ} {armLen : Fin k → ℕ} {l : Fin k} {s : ℕ} (hs : s ≤ armLen l) : (armNode k armLen l s).armOf = some l

theorem Graphon.Lovasz.K2kVertex.stepOf_armNode {k : ℕ} {armLen : Fin k → ℕ} {l : Fin k} {s : ℕ} (hs : s ≤ armLen l) : (armNode k armLen l s).stepOf = s

theorem Graphon.Lovasz.K2kVertex.armNode_ne_root {k : ℕ} {armLen : Fin k → ℕ} (l : Fin k) (s : ℕ) : armNode k armLen l s ≠ root

theorem Graphon.Lovasz.K2kVertex.armNode_eq_hub_of_gt {k : ℕ} {armLen : Fin k → ℕ} {l : Fin k} {s : ℕ} (h : armLen l < s) : armNode k armLen l s = hub

theorem Graphon.Lovasz.k2kEdge_injective (k : ℕ) (armLen : Fin k → ℕ) : Function.Injective (k2kEdge k armLen)

The indexed edge family is injective (each (l, s) recovered from the non-hub chain endpoint via armOf/stepOf; the reversed orientation is killed by omega). The structured analogue of armSeq_pair_inj.

theorem Graphon.Lovasz.k2kArmsStructured_prod_eq {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (Φ : K2kVertex k armLen → Fin T) : ∏ E ∈ (k2kArmsStructured k armLen).edgeFinset, B (Φ (Quot.out E).1) (Φ (Quot.out E).2) = (∏ l : Fin k, B (Φ K2kVertex.root) (Φ (K2kVertex.anchor l))) * ∏ l : Fin k, ∏ s : Fin (armLen l + 1), B (Φ (K2kVertex.armNode k armLen l ↑s)) (Φ (K2kVertex.armNode k armLen l (↑s + 1)))

Edge-product factorization on the structured graph (the analogue of k23Arms_prod_eq): the edge product splits into the k root-edge factors and the k independent arm-chain products.

theorem Graphon.Lovasz.comap_symm_edgeFinset {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] (e : V ≃ W) (G : SimpleGraph V) [DecidableRel G.Adj] : (SimpleGraph.comap (⇑e.symm) G).edgeFinset = Finset.map e.toEmbedding.sym2Map G.edgeFinset

Edge finset of a graph pulled back along an equivalence's inverse is the Sym2-image of the source edge finset (generic transport lemma).

theorem Graphon.Lovasz.k2kArms_edgeFinset_transport (k : ℕ) (armLen : Fin k → ℕ) : (k2kArms k armLen).edgeFinset = Finset.map (K2kVertex_equivFin k armLen).toEmbedding.sym2Map (k2kArmsStructured k armLen).edgeFinset

Edge-finset transport for the Fin-rooted graph: k2kArms' edges are the K2kVertex_equivFin-images of the structured graph's edges.

theorem Graphon.Lovasz.k2kArms_prod_eq_structured {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (τ : Fin (k2kRestCard k armLen + 1) → Fin T) : ∏ E ∈ (k2kArms k armLen).edgeFinset, B (τ (Quot.out E).1) (τ (Quot.out E).2) = (∏ l : Fin k, B (τ ((K2kVertex_equivFin k armLen) K2kVertex.root)) (τ ((K2kVertex_equivFin k armLen) (K2kVertex.anchor l)))) * ∏ l : Fin k, ∏ s : Fin (armLen l + 1), B (τ ((K2kVertex_equivFin k armLen) (K2kVertex.armNode k armLen l ↑s))) (τ ((K2kVertex_equivFin k armLen) (K2kVertex.armNode k armLen l (↑s + 1))))

Edge-product factorization on the Fin graph (transport + structured factorization combined): the rootedProfile edge product over k2kArms factors, through K2kVertex_equivFin, into the k root-edge factors and the k arm-chain products. This is the replacement for the brittle k23Arms offset work; k2kArms_eval consumes it directly.

Commit 2 — structured eval expansion (reindex + per-arm collapse)

noncomputable def Graphon.Lovasz.k2kRestEquivFin (k : ℕ) (armLen : Fin k → ℕ) : K2kRest k armLen ≃ Fin (k2kRestCard k armLen)

The non-root part of K2kVertex_equivFin as a standalone equivalence K2kRest ≃ Fin (k2kRestCard) (definitionally the rest-equiv inside K2kVertex_equivFin).

Equations

• Graphon.Lovasz.k2kRestEquivFin k armLen = Fintype.equivFinOfCardEq ⋯

theorem Graphon.Lovasz.K2kVertex_equivFin_some (k : ℕ) (armLen : Fin k → ℕ) (r : K2kRest k armLen) : (K2kVertex_equivFin k armLen) ((k2kVertexOptionEquiv k armLen).symm (some r)) = ((k2kRestEquivFin k armLen) r).succ

Vertex → Fin-position value lemma: a non-root vertex r (as a K2kRest element adjoined via k2kVertexOptionEquiv.symm) sits at position (k2kRestEquivFin r).succ — i.e. one past the root (which is 0). This is the sole fact about the opaque rest-equiv the reindexing needs.

def Graphon.Lovasz.extendV {T k : ℕ} {armLen : Fin k → ℕ} (v : Fin T) (ρ : K2kRest k armLen → Fin T) : K2kVertex k armLen → Fin T

The structured assignment K2kVertex → Fin T with root ↦ v and each non-root vertex r taking the value ρ r.

Equations

• Graphon.Lovasz.extendV v ρ w = ((Graphon.Lovasz.k2kVertexOptionEquiv k armLen) w).elim v ρ

@[simp]

theorem Graphon.Lovasz.extendV_root {T k : ℕ} {armLen : Fin k → ℕ} (v : Fin T) (ρ : K2kRest k armLen → Fin T) : extendV v ρ K2kVertex.root = v

@[simp]

theorem Graphon.Lovasz.extendV_anchor {T k : ℕ} {armLen : Fin k → ℕ} (v : Fin T) (ρ : K2kRest k armLen → Fin T) (l : Fin k) : extendV v ρ (K2kVertex.anchor l) = ρ (Sum.inl l)

@[simp]

theorem Graphon.Lovasz.extendV_hub {T k : ℕ} {armLen : Fin k → ℕ} (v : Fin T) (ρ : K2kRest k armLen → Fin T) : extendV v ρ K2kVertex.hub = ρ (Sum.inr (Sum.inl ()))

@[simp]

theorem Graphon.Lovasz.extendV_internal {T k : ℕ} {armLen : Fin k → ℕ} (v : Fin T) (ρ : K2kRest k armLen → Fin T) (l : Fin k) (s : Fin (armLen l)) : extendV v ρ (K2kVertex.internal l s) = ρ (Sum.inr (Sum.inr ⟨l, s⟩))

theorem Graphon.Lovasz.extendV_armNode {T k : ℕ} {armLen : Fin k → ℕ} (v : Fin T) (ρ : K2kRest k armLen → Fin T) (l : Fin k) {s : ℕ} (hs : s ≤ armLen l + 1) : extendV v ρ (K2kVertex.armNode k armLen l s) = chainPath (armLen l) (ρ (Sum.inl l)) (ρ (Sum.inr (Sum.inl ()))) (fun (j : Fin (armLen l)) => ρ (Sum.inr (Sum.inr ⟨l, j⟩))) s

On arm l, extendV ∘ armNode is exactly the free-standing chainPath from the anchor value to the hub value over the arm's internal values.

theorem Graphon.Lovasz.k2kArms_edge_prod_transport {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (τ : Fin (k2kRestCard k armLen + 1) → Fin T) : ∏ E ∈ (k2kArms k armLen).edgeFinset, B (τ (Quot.out E).1) (τ (Quot.out E).2) = ∏ E ∈ (k2kArmsStructured k armLen).edgeFinset, B (τ ((K2kVertex_equivFin k armLen) (Quot.out E).1)) (τ ((K2kVertex_equivFin k armLen) (Quot.out E).2))

Edge-product transport (product form): the Fin-graph edge product equals the structured edge product with vertices read through K2kVertex_equivFin.

theorem Graphon.Lovasz.rootedProfile_k2kArms_eq_structSum {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (v : Fin T) : rootedProfile B W v (k2kArms k armLen) = ∑ ρ : K2kRest k armLen → Fin T, (∏ r : K2kRest k armLen, W (ρ r)) * ∏ E ∈ (k2kArmsStructured k armLen).edgeFinset, B (extendV v ρ (Quot.out E).1) (extendV v ρ (Quot.out E).2)

Reindexing the eval onto structured assignments: the rooted profile of k2kArms is the sum over structured non-root assignments ρ : K2kRest → Fin T of the structured weight × edge product (root pinned to v).

def Graphon.Lovasz.assignEquiv {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) : (K2kRest k armLen → Fin T) ≃ (Fin k → Fin T) × Fin T × ((l : Fin k) → Fin (armLen l) → Fin T)

Assignment splitting equivalence: a non-root structured assignment is exactly a triple (anchor values, hub value, per-arm internal values). Built directly so the component value lemmas are rfl.

Equations

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

@[simp]

theorem Graphon.Lovasz.assignEquiv_symm_inl {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (p : (Fin k → Fin T) × Fin T × ((l : Fin k) → Fin (armLen l) → Fin T)) (l : Fin k) : (assignEquiv k armLen).symm p (Sum.inl l) = p.1 l

@[simp]

theorem Graphon.Lovasz.assignEquiv_symm_hub {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (p : (Fin k → Fin T) × Fin T × ((l : Fin k) → Fin (armLen l) → Fin T)) : (assignEquiv k armLen).symm p (Sum.inr (Sum.inl ())) = p.2.1

@[simp]

theorem Graphon.Lovasz.assignEquiv_symm_inr {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (p : (Fin k → Fin T) × Fin T × ((l : Fin k) → Fin (armLen l) → Fin T)) (l : Fin k) (j : Fin (armLen l)) : (assignEquiv k armLen).symm p (Sum.inr (Sum.inr ⟨l, j⟩)) = p.2.2 l j

theorem Graphon.Lovasz.k2kRest_weight_prod {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (W : Fin T → ℝ) (ρ : K2kRest k armLen → Fin T) : ∏ r : K2kRest k armLen, W (ρ r) = (∏ l : Fin k, W (ρ (Sum.inl l))) * (W (ρ (Sum.inr (Sum.inl ()))) * ∏ l : Fin k, ∏ j : Fin (armLen l), W (ρ (Sum.inr (Sum.inr ⟨l, j⟩))))

Factorization of the structured vertex-weight product over the three vertex blocks (anchors / hub / internals).

theorem Graphon.Lovasz.k2kArms_eval_expanded {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (v : Fin T) : rootedProfile B W v (k2kArms k armLen) = ∑ hub : Fin T, W hub * ∑ anchors : Fin k → Fin T, ∏ l : Fin k, W (anchors l) * B v (anchors l) * armSum B W (armLen l) (anchors l) hub

Structured eval expansion (Commit 2b): the rooted profile of k2kArms expands as a hub sum of an anchor sum of per-arm armSum kernels.

Commit 3 — wMulti collapse + polarization bridge

theorem Graphon.Lovasz.k2kArms_eval {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (v : Fin T) : rootedProfile B W v (k2kArms k armLen) = wMulti k W fun (l : Fin k) => weightedAdjIter B W (armLen l + 1) fun (t : Fin T) => B v t

3.1 — k2kArms evaluation in wMulti form: the rooted profile is the weighted k-linear form of the root-row walk kernels M^{armLen l + 1}(B v).

theorem Graphon.Lovasz.prod_sub_prod_polarization (k : ℕ) (a b : Fin k → ℝ) : 2 ^ k * (∏ l : Fin k, a l - ∏ l : Fin k, b l) = 2 * ∑ S ∈ Finset.univ.powerset with Odd S.card, ∏ l : Fin k, if l ∈ S then a l - b l else a l + b l

Multilinear product polarization (per-slot generalization of pow_sub_pow_expand): 2^k (∏ a − ∏ b) is 2 · the odd-subset sum of the slot products with a−b inside the subset and a+b outside.

theorem Graphon.Lovasz.rootedProfile_k2kArms_sub_eq_polarizedPowObs {T : ℕ} (k : ℕ) (armLen : Fin k → ℕ) (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (i j : Fin T) : (2 * polarizedPowObs k B W i j fun (l : Fin k) => armLen l + 1) = 2 ^ k * (rootedProfile B W i (k2kArms k armLen) - rootedProfile B W j (k2kArms k armLen))

3.2 — the graph bridge: 2 · the polarized k-th power observable at arm lengths armLen l + 1 equals 2^k · the rooted K₂,ₖ-arms profile difference (the k-ary generalization of rootedProfile_k23Arms_sub_eq_polarizedCubeObs; at k = 3, 2^3 = 8 = 2·4).

theorem Graphon.Lovasz.powerSum_descends_of_rootedProfileEquiv {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) {i j : Fin T} (h : rootedProfileEquiv B W i j) (k : ℕ) : ∑ t : Fin T, W t * B i t ^ k = ∑ t : Fin T, W t * B j t ^ k

Weighted power sums descend — now PROVED for ALL k (k ≤ 2 directly, k = 3 via cubeMoment_descends_of_rootedProfileEquiv, k ≥ 4 via the K₂,ₖ-arms bridge rootedProfile_k2kArms_sub_eq_polarizedPowObs feeding powGap_eq_zero_of_polarized_obs).

weighted_powersum_determines_measure upgrades this to equality of the W-weighted row-value measures, the key step toward the rank theorem vertexOrbitRel_of_rootedProfileEquiv.

theorem Graphon.Lovasz.rowValueMeasure_eq_of_rootedProfileEquiv {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) {i j : Fin T} (h : rootedProfileEquiv B W i j) (a : ℝ) : ∑ t : Fin T with B i t = a, W t = ∑ t : Fin T with B j t = a, W t

Row-value measures descend (now unconditional): under rooted-profile equivalence, the W-weighted preimage masses of the two rows agree at every value — the rows are equal as weighted value measures.

Single-vertex decoration — the gluing primitive for the weight-mod crux

decorateAt F H u glues H onto vertex u of F (identifying H's root with u). Its rooted profile factorizes: the H-block contributes rootedProfile B W (value at u) H to each F-assignment. Decorating EVERY unlabeled vertex by H then realizes the modified weight W · (profile of H), which is the engine of rootedProfileEquiv_weightMod.

def Graphon.Lovasz.hDecorEmb {n m : ℕ} (u : Fin (n + 1)) : Fin (m + 1) ↪ Fin (n + 1) ⊕ Fin m

Embedding of H's vertices into Fin (n+1) ⊕ Fin m: the root 0 ↦ inl u (identified with vertex u of F), and Fin.succ k ↦ inr k.

Equations

• Graphon.Lovasz.hDecorEmb u = { toFun := Fin.cons (Sum.inl u) fun (k : Fin m) => Sum.inr k, inj' := ⋯ }

def Graphon.Lovasz.decorateAtSum {n m : ℕ} (F : SimpleGraph (Fin (n + 1))) (H : SimpleGraph (Fin (m + 1))) (u : Fin (n + 1)) : SimpleGraph (Fin (n + 1) ⊕ Fin m)

The structured single-vertex decoration on Fin (n+1) ⊕ Fin m: F on the inl block, ⊔ H glued with its root at u (via hDecorEmb).

Equations

• Graphon.Lovasz.decorateAtSum F H u = SimpleGraph.map (⇑Function.Embedding.inl) F ⊔ SimpleGraph.map (⇑(Graphon.Lovasz.hDecorEmb u)) H

noncomputable def Graphon.Lovasz.decorVertexEquiv (n m : ℕ) : Fin (n + 1) ⊕ Fin m ≃ Fin (n + m + 1)

Fin (n+1) ⊕ Fin m ≃ Fin (n+m+1) with the F-root inl 0 ↦ 0 (so the decorated graph's root is F's root).

Equations

• Graphon.Lovasz.decorVertexEquiv n m = finSumFinEquiv.trans (finCongr ⋯)

@[simp]

theorem Graphon.Lovasz.decorVertexEquiv_inl_zero (n m : ℕ) : (decorVertexEquiv n m) (Sum.inl 0) = 0

noncomputable def Graphon.Lovasz.decorateAt {n m : ℕ} (F : SimpleGraph (Fin (n + 1))) (H : SimpleGraph (Fin (m + 1))) (u : Fin (n + 1)) : SimpleGraph (Fin (n + m + 1))

Single-vertex decoration as a SimpleGraph (Fin (n+m+1)) (transported from the structured form), consumable by rootedProfile.

Equations

• Graphon.Lovasz.decorateAt F H u = SimpleGraph.comap (⇑(Graphon.Lovasz.decorVertexEquiv n m).symm) (Graphon.Lovasz.decorateAtSum F H u)

@[implicit_reducible]

instance Graphon.Lovasz.instDecidableRelSumFinHAddNatOfNatAdjDecorateAtSum {n m : ℕ} (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] (u : Fin (n + 1)) : DecidableRel (decorateAtSum F H u).Adj

Equations

• Graphon.Lovasz.instDecidableRelSumFinHAddNatOfNatAdjDecorateAtSum F H u = id inferInstance

@[implicit_reducible]

noncomputable instance Graphon.Lovasz.instDecidableRelFinHAddNatOfNatAdjDecorateAt {n m : ℕ} (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] (u : Fin (n + 1)) : DecidableRel (decorateAt F H u).Adj

Equations

• Graphon.Lovasz.instDecidableRelFinHAddNatOfNatAdjDecorateAt F H u = SimpleGraph.instDecidableComapAdj (⇑(Graphon.Lovasz.decorVertexEquiv n m).symm) (Graphon.Lovasz.decorateAtSum F H u)

theorem Graphon.Lovasz.decorateAtSum_edge_disjoint {n m : ℕ} (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] (u : Fin (n + 1)) : Disjoint (SimpleGraph.map (⇑Function.Embedding.inl) F).edgeFinset (SimpleGraph.map (⇑(hDecorEmb u)) H).edgeFinset

The F-block and H-block edge sets of decorateAtSum are disjoint: an H-edge has at most one Sum.inl endpoint (only its root maps there), while an F-edge has two — so a shared edge would force a self-loop in H.

theorem Graphon.Lovasz.decorateAt_prod_eq {T n m : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] (u : Fin (n + 1)) (τ : Fin (n + m + 1) → Fin T) : ∏ E ∈ (decorateAt F H u).edgeFinset, B (τ (Quot.out E).1) (τ (Quot.out E).2) = (∏ e ∈ F.edgeFinset, B (τ ((decorVertexEquiv n m) (Sum.inl (Quot.out e).1))) (τ ((decorVertexEquiv n m) (Sum.inl (Quot.out e).2)))) * ∏ e ∈ H.edgeFinset, B (τ ((decorVertexEquiv n m) ((hDecorEmb u) (Quot.out e).1))) (τ ((decorVertexEquiv n m) ((hDecorEmb u) (Quot.out e).2)))

Edge-product transport + split (Commit 1 steps 1–2): the rootedProfile edge product over decorateAt F H u factors, through decorVertexEquiv, into the F-edge product and the H-edge product.

theorem Graphon.Lovasz.rootedProfile_cons {T n : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (v : Fin T) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] : rootedProfile B W v F = ∑ σ : Fin n → Fin T, (∏ w : Fin n, W (σ w)) * ∏ e ∈ F.edgeFinset, B (Fin.cons v σ (Quot.out e).1) (Fin.cons v σ (Quot.out e).2)

rootedProfile in Fin.cons form (re-derived here; the SimpleRank version is private).

theorem Graphon.Lovasz.decorVertexEquiv_inl_val (n m : ℕ) (x : Fin (n + 1)) : ↑((decorVertexEquiv n m) (Sum.inl x)) = ↑x

theorem Graphon.Lovasz.decorVertexEquiv_inr_val (n m : ℕ) (z : Fin m) : ↑((decorVertexEquiv n m) (Sum.inr z)) = n + 1 + ↑z

theorem Graphon.Lovasz.consAppend_inl {T n m : ℕ} (v : Fin T) (σF : Fin n → Fin T) (σH : Fin m → Fin T) (x : Fin (n + 1)) : Fin.cons v (appendFn σF σH) ((decorVertexEquiv n m) (Sum.inl x)) = Fin.cons v σF x

F-side assignment value lemma: under the block assignment appendFn σF σH, the value at an F-vertex inl x is Fin.cons v σF x.

theorem Graphon.Lovasz.consAppend_hDecorEmb {T n m : ℕ} (v : Fin T) (σF : Fin n → Fin T) (σH : Fin m → Fin T) (u : Fin (n + 1)) (a : Fin (m + 1)) : Fin.cons v (appendFn σF σH) ((decorVertexEquiv n m) ((hDecorEmb u) a)) = Fin.cons (Fin.cons v σF u) σH a

H-side assignment value lemma: under appendFn σF σH, the value at an H-vertex hDecorEmb u a is Fin.cons (Fin.cons v σF u) σH a — i.e. H rooted at the value vertex u receives.

theorem Graphon.Lovasz.rootedProfile_decorate_vertex {T n m : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (v : Fin T) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] (u : Fin (n + 1)) : rootedProfile B W v (decorateAt F H u) = ∑ σ : Fin n → Fin T, ((∏ w : Fin n, W (σ w)) * ∏ e ∈ F.edgeFinset, B (Fin.cons v σ (Quot.out e).1) (Fin.cons v σ (Quot.out e).2)) * rootedProfile B W (Fin.cons v σ u) H

Single-vertex decoration factorization (Commit 1 target — PROVED): gluing H at vertex u multiplies each F-assignment's contribution by the H-profile rooted at the value u receives. Analogue of rootedProfile_rootAttach, but the attachment point is an arbitrary unlabeled vertex, not a fresh pendant root.

Proof plan: transport the edge product to decorateAtSum (comap along decorVertexEquiv, as in k2kArms_prod_eq_structured); the structured edge set is the disjoint union (F.map inl).edgeFinset ∪ (H.map (hDecorEmb u)).edgeFinset, so the product splits into the F-edge product and the H-edge product; reindex the assignment sum over Fin (n+m) → Fin T into (Fin n → Fin T) × (Fin m → Fin T); the H-factor, with its root pinned to the value at u, sums to rootedProfile B W (Fin.cons v σ u) H.

All-vertex decoration (Route B) — glue a copy of H at EVERY unlabeled

vertex of F. One fixed structured vertex type Fin(n+1) ⊕ (Fin n × Fin m): inl 0 = F-root, inl (succ w) = unlabeled vertex w, inr (w, z) = the z-th internal vertex of the H-copy glued at w. Decorating all vertices realizes the modified weight W · (profile of H), the engine of rootedProfileEquiv_weightMod.

def Graphon.Lovasz.embedHCopy {n m : ℕ} (w : Fin n) : Fin (m + 1) ↪ Fin (n + 1) ⊕ Fin n × Fin m

Embedding of the w-th H-copy: root 0 ↦ inl (succ w), succ z ↦ inr (w, z).

Equations

• Graphon.Lovasz.embedHCopy w = { toFun := Fin.cons (Sum.inl w.succ) fun (z : Fin m) => Sum.inr (w, z), inj' := ⋯ }

def Graphon.Lovasz.decorateAllSum {n m : ℕ} (F : SimpleGraph (Fin (n + 1))) (H : SimpleGraph (Fin (m + 1))) : SimpleGraph (Fin (n + 1) ⊕ Fin n × Fin m)

The structured all-vertex decoration: F on the inl block, joined with one H-copy per unlabeled vertex (via Finset.sup, not iSup, to keep decidability and edge-finset instances controllable).

Equations

• Graphon.Lovasz.decorateAllSum F H = SimpleGraph.map (⇑Function.Embedding.inl) F ⊔ Finset.univ.sup fun (w : Fin n) => SimpleGraph.map (⇑(Graphon.Lovasz.embedHCopy w)) H

noncomputable def Graphon.Lovasz.decorAllVertexEquiv (n m : ℕ) : Fin (n + 1) ⊕ Fin n × Fin m ≃ Fin (n + n * m + 1)

Fin (n+1) ⊕ (Fin n × Fin m) ≃ Fin (n + n*m + 1) with inl 0 ↦ 0.

Equations

• Graphon.Lovasz.decorAllVertexEquiv n m = ((Equiv.refl (Fin (n + 1))).sumCongr finProdFinEquiv).trans (finSumFinEquiv.trans (finCongr ⋯))

@[simp]

theorem Graphon.Lovasz.decorAllVertexEquiv_inl_zero (n m : ℕ) : (decorAllVertexEquiv n m) (Sum.inl 0) = 0

theorem Graphon.Lovasz.decorAllVertexEquiv_inl_val (n m : ℕ) (x : Fin (n + 1)) : ↑((decorAllVertexEquiv n m) (Sum.inl x)) = ↑x

noncomputable def Graphon.Lovasz.decorateAll {n m : ℕ} (F : SimpleGraph (Fin (n + 1))) (H : SimpleGraph (Fin (m + 1))) : SimpleGraph (Fin (n + n * m + 1))

All-vertex decoration as a SimpleGraph (Fin (n+n*m+1)).

Equations

• Graphon.Lovasz.decorateAll F H = SimpleGraph.comap (⇑(Graphon.Lovasz.decorAllVertexEquiv n m).symm) (Graphon.Lovasz.decorateAllSum F H)

theorem Graphon.Lovasz.decorateAllSum_sup_adj {n m : ℕ} (H : SimpleGraph (Fin (m + 1))) (x y : Fin (n + 1) ⊕ Fin n × Fin m) : (Finset.univ.sup fun (w : Fin n) => SimpleGraph.map (⇑(embedHCopy w)) H).Adj x y ↔ ∃ (w : Fin n), (SimpleGraph.map (⇑(embedHCopy w)) H).Adj x y

Finset.sup-adjacency over Fin n is the existential of the per-w adjacencies.

@[implicit_reducible]

instance Graphon.Lovasz.instDecidableRelSumFinHAddNatOfNatProdAdjSupSimpleGraphUnivMapCoeEmbeddingEmbedHCopy {n m : ℕ} (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] : DecidableRel (Finset.univ.sup fun (w : Fin n) => SimpleGraph.map (⇑(embedHCopy w)) H).Adj

Equations

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

@[implicit_reducible]

instance Graphon.Lovasz.instDecidableRelSumFinHAddNatOfNatProdAdjDecorateAllSum {n m : ℕ} (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] : DecidableRel (decorateAllSum F H).Adj

Equations

• Graphon.Lovasz.instDecidableRelSumFinHAddNatOfNatProdAdjDecorateAllSum F H x y = id (⋯.mpr (⋯.mpr inferInstance))

@[implicit_reducible]

noncomputable instance Graphon.Lovasz.instDecidableRelFinHAddNatHMulOfNatAdjDecorateAll {n m : ℕ} (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] : DecidableRel (decorateAll F H).Adj

Equations

• Graphon.Lovasz.instDecidableRelFinHAddNatHMulOfNatAdjDecorateAll F H = SimpleGraph.instDecidableComapAdj (⇑(Graphon.Lovasz.decorAllVertexEquiv n m).symm) (Graphon.Lovasz.decorateAllSum F H)

theorem Graphon.Lovasz.embedHCopy_apply_ne {n m : ℕ} {w w' : Fin n} (hww : w ≠ w') (a a' : Fin (m + 1)) : (embedHCopy w) a ≠ (embedHCopy w') a'

The w-th and w'-th H-copies have disjoint vertex images for w ≠ w'.

theorem Graphon.Lovasz.decorateAll_Hcopy_disjoint {n m : ℕ} (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] {w w' : Fin n} (hww : w ≠ w') : Disjoint (SimpleGraph.map (⇑(embedHCopy w)) H).edgeFinset (SimpleGraph.map (⇑(embedHCopy w')) H).edgeFinset

Distinct H-copies have disjoint edge sets (disjoint vertex images).

theorem Graphon.Lovasz.decorateAll_F_sup_disjoint {n m : ℕ} (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] : Disjoint (SimpleGraph.map (⇑Function.Embedding.inl) F).edgeFinset (Finset.univ.sup fun (w : Fin n) => SimpleGraph.map (⇑(embedHCopy w)) H).edgeFinset

The F-block is disjoint from every H-copy block: a sup-edge has at most one Sum.inl endpoint, an F-edge has two.

theorem Graphon.Lovasz.decorateAllSum_sup_edgeFinset {n m : ℕ} (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] : (Finset.univ.sup fun (w : Fin n) => SimpleGraph.map (⇑(embedHCopy w)) H).edgeFinset = Finset.univ.biUnion fun (w : Fin n) => (SimpleGraph.map (⇑(embedHCopy w)) H).edgeFinset

The Finset.sup of the H-copies has edge finset the disjoint union of the per-copy edge finsets.

theorem Graphon.Lovasz.decorateAll_prod_eq {T n m : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] (τ : Fin (n + n * m + 1) → Fin T) : ∏ E ∈ (decorateAll F H).edgeFinset, B (τ (Quot.out E).1) (τ (Quot.out E).2) = (∏ e ∈ F.edgeFinset, B (τ ((decorAllVertexEquiv n m) (Sum.inl (Quot.out e).1))) (τ ((decorAllVertexEquiv n m) (Sum.inl (Quot.out e).2)))) * ∏ w : Fin n, ∏ e ∈ H.edgeFinset, B (τ ((decorAllVertexEquiv n m) ((embedHCopy w) (Quot.out e).1))) (τ ((decorAllVertexEquiv n m) ((embedHCopy w) (Quot.out e).2)))

Edge-product transport + split (B2): the rootedProfile edge product over decorateAll F H factors, through decorAllVertexEquiv, into the F-edge product times the product over the n H-copy edge products.

theorem Graphon.Lovasz.decorAllVertexEquiv_inr_val (n m : ℕ) (w : Fin n) (z : Fin m) : ↑((decorAllVertexEquiv n m) (Sum.inr (w, z))) = n + 1 + ↑(finProdFinEquiv (w, z))

theorem Graphon.Lovasz.consAppendAll_inl {T n m : ℕ} (v : Fin T) (σF : Fin n → Fin T) (σHflat : Fin (n * m) → Fin T) (x : Fin (n + 1)) : Fin.cons v (appendFn σF σHflat) ((decorAllVertexEquiv n m) (Sum.inl x)) = Fin.cons v σF x

B3 F-side value lemma: under appendFn σF σHflat, the value at an F-vertex inl x is Fin.cons v σF x.

theorem Graphon.Lovasz.consAppendAll_embedHCopy {T n m : ℕ} (v : Fin T) (σF : Fin n → Fin T) (σHflat : Fin (n * m) → Fin T) (w : Fin n) (a : Fin (m + 1)) : Fin.cons v (appendFn σF σHflat) ((decorAllVertexEquiv n m) ((embedHCopy w) a)) = Fin.cons (Fin.cons v σF w.succ) (fun (z : Fin m) => σHflat (finProdFinEquiv (w, z))) a

B3 H-side value lemma: under appendFn σF σHflat, the w-th H-copy's assignment is Fin.cons (Fin.cons v σF w.succ) (fun z => σHflat (finProdFinEquiv (w,z))) — i.e. the w-th copy rooted at the value F-vertex w receives.

noncomputable def Graphon.Lovasz.flatAssignEquiv (T n m : ℕ) : (Fin n → Fin m → Fin T) ≃ (Fin (n * m) → Fin T)

Flat ↔ curried assignment equivalence: a flat assignment over the n*m internal H-copy vertices is the same as n separate H-copy assignments, matched via finProdFinEquiv.

Equations

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

theorem Graphon.Lovasz.flatAssignEquiv_apply_fpfe {T n m : ℕ} (σH : Fin n → Fin m → Fin T) (w : Fin n) (z : Fin m) : (flatAssignEquiv T n m) σH (finProdFinEquiv (w, z)) = σH w z

theorem Graphon.Lovasz.flatAssignEquiv_weight_prod {T n m : ℕ} (W : Fin T → ℝ) (σH : Fin n → Fin m → Fin T) : ∏ k : Fin (n * m), W ((flatAssignEquiv T n m) σH k) = ∏ w : Fin n, ∏ z : Fin m, W (σH w z)

theorem Graphon.Lovasz.decorateAll_Hflat_collapse {T n m : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] (r : Fin n → Fin T) : ∑ σ : Fin (n * m) → Fin T, (∏ k : Fin (n * m), W (σ k)) * ∏ w : Fin n, ∏ e ∈ H.edgeFinset, B (Fin.cons (r w) (fun (z : Fin m) => σ (finProdFinEquiv (w, z))) (Quot.out e).1) (Fin.cons (r w) (fun (z : Fin m) => σ (finProdFinEquiv (w, z))) (Quot.out e).2) = ∏ w : Fin n, rootedProfile B W (r w) H

n-fold H-copy collapse (B3 engine): summing the flat internal-vertex assignment factors the contribution of the n glued H-copies into a product of n rooted profiles, each rooted at the value r w its anchor vertex receives.

theorem Graphon.Lovasz.rootedProfile_decorateAll {T n m : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (v : Fin T) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] : rootedProfile B W v (decorateAll F H) = ∑ σF : Fin n → Fin T, ((∏ w : Fin n, W (σF w)) * ∏ e ∈ F.edgeFinset, B (Fin.cons v σF (Quot.out e).1) (Fin.cons v σF (Quot.out e).2)) * ∏ w : Fin n, rootedProfile B W (σF w) H

B3 — all-vertex decoration factorization (the key theorem): decorating every unlabeled vertex of F with a copy of H multiplies each F-assignment's contribution by the product, over unlabeled vertices w, of the H-profile rooted at the value w receives. The engine of rootedProfileEquiv_weightMod.

theorem Graphon.Lovasz.rootedProfile_weightMul_of_profile_mem_span {T n m : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (H : SimpleGraph (Fin (m + 1))) [DecidableRel H.Adj] : InRootedProfileSpan B W fun (v : Fin T) => rootedProfile B (fun (t : Fin T) => W t * rootedProfile B W t H) v F

B4 — single-profile weight modification stays in the span: modifying the weight W by the rooted profile of a single graph H turns the profile of F into the profile of the all-vertex decoration decorateAll F H, which is a bare profile and hence in InRootedProfileSpan B W. This is the single-H case of rootedProfileEquiv_weightMod; the general g ∈ span case follows by linearity.

Per-vertex-family decoration (decorateAllFam) — the Σ-indexed generalization

decorateAll glues ONE graph H at every unlabeled vertex; for the general g = ∑_k c_k · rootedProfileFun B W H_k we must glue a possibly DIFFERENT graph Hfam w at each unlabeled vertex w. Sizes vary with w, so the internal vertices form a Σ-type (w : Fin n) × Fin (mfam w) (flattened via finSigmaFinEquiv, never common-size padding, which would scale the profile by (∑ W)^extra — zero for signed W).

def Graphon.Lovasz.embedHCopyFam {n : ℕ} {mfam : Fin n → ℕ} (w : Fin n) : Fin (mfam w + 1) ↪ Fin (n + 1) ⊕ (w' : Fin n) × Fin (mfam w')

Embedding of the w-th H-copy (family version): 0 ↦ inl (succ w), succ z ↦ inr ⟨w, z⟩.

Equations

• Graphon.Lovasz.embedHCopyFam w = { toFun := Fin.cons (Sum.inl w.succ) fun (z : Fin (mfam w)) => Sum.inr ⟨w, z⟩, inj' := ⋯ }

def Graphon.Lovasz.decorateAllFamSum {n : ℕ} {mfam : Fin n → ℕ} (F : SimpleGraph (Fin (n + 1))) (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) : SimpleGraph (Fin (n + 1) ⊕ (w' : Fin n) × Fin (mfam w'))

The structured per-vertex-family decoration.

Equations

• Graphon.Lovasz.decorateAllFamSum F Hfam = SimpleGraph.map (⇑Function.Embedding.inl) F ⊔ Finset.univ.sup fun (w : Fin n) => SimpleGraph.map (⇑(Graphon.Lovasz.embedHCopyFam w)) (Hfam w)

noncomputable def Graphon.Lovasz.decorAllFamVertexEquiv {n : ℕ} (mfam : Fin n → ℕ) : Fin (n + 1) ⊕ (w' : Fin n) × Fin (mfam w') ≃ Fin (n + ∑ w : Fin n, mfam w + 1)

Fin (n+1) ⊕ ((w : Fin n) × Fin (mfam w)) ≃ Fin (n + (∑ w, mfam w) + 1) with inl 0 ↦ 0.

Equations

• Graphon.Lovasz.decorAllFamVertexEquiv mfam = ((Equiv.refl (Fin (n + 1))).sumCongr finSigmaFinEquiv).trans (finSumFinEquiv.trans (finCongr ⋯))

@[simp]

theorem Graphon.Lovasz.decorAllFamVertexEquiv_inl_zero {n : ℕ} (mfam : Fin n → ℕ) : (decorAllFamVertexEquiv mfam) (Sum.inl 0) = 0

noncomputable def Graphon.Lovasz.decorateAllFam {n : ℕ} {mfam : Fin n → ℕ} (F : SimpleGraph (Fin (n + 1))) (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) : SimpleGraph (Fin (n + ∑ w : Fin n, mfam w + 1))

Per-vertex-family decoration as a SimpleGraph (Fin (n + (∑ mfam) + 1)).

Equations

• Graphon.Lovasz.decorateAllFam F Hfam = SimpleGraph.comap (⇑(Graphon.Lovasz.decorAllFamVertexEquiv mfam).symm) (Graphon.Lovasz.decorateAllFamSum F Hfam)

theorem Graphon.Lovasz.decorateAllFamSum_sup_adj {n : ℕ} {mfam : Fin n → ℕ} (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) (x y : Fin (n + 1) ⊕ (w' : Fin n) × Fin (mfam w')) : (Finset.univ.sup fun (w : Fin n) => SimpleGraph.map (⇑(embedHCopyFam w)) (Hfam w)).Adj x y ↔ ∃ (w : Fin n), (SimpleGraph.map (⇑(embedHCopyFam w)) (Hfam w)).Adj x y

@[implicit_reducible]

instance Graphon.Lovasz.instDecidableRelSumFinHAddNatOfNatSigmaAdjSupSimpleGraphUnivMapCoeEmbeddingEmbedHCopyFam {n : ℕ} {mfam : Fin n → ℕ} (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) [(w : Fin n) → DecidableRel (Hfam w).Adj] : DecidableRel (Finset.univ.sup fun (w : Fin n) => SimpleGraph.map (⇑(embedHCopyFam w)) (Hfam w)).Adj

Equations

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

@[implicit_reducible]

instance Graphon.Lovasz.instDecidableRelSumFinHAddNatOfNatSigmaAdjDecorateAllFamSum {n : ℕ} {mfam : Fin n → ℕ} (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) [(w : Fin n) → DecidableRel (Hfam w).Adj] : DecidableRel (decorateAllFamSum F Hfam).Adj

Equations

• Graphon.Lovasz.instDecidableRelSumFinHAddNatOfNatSigmaAdjDecorateAllFamSum F Hfam x y = id (⋯.mpr (⋯.mpr inferInstance))

@[implicit_reducible]

noncomputable instance Graphon.Lovasz.instDecidableRelFinHAddNatSumUnivOfNatAdjDecorateAllFam {n : ℕ} {mfam : Fin n → ℕ} (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) [(w : Fin n) → DecidableRel (Hfam w).Adj] : DecidableRel (decorateAllFam F Hfam).Adj

Equations

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

theorem Graphon.Lovasz.embedHCopyFam_apply_ne {n : ℕ} {mfam : Fin n → ℕ} {w w' : Fin n} (hww : w ≠ w') (a : Fin (mfam w + 1)) (a' : Fin (mfam w' + 1)) : (embedHCopyFam w) a ≠ (embedHCopyFam w') a'

theorem Graphon.Lovasz.decorateAllFam_Hcopy_disjoint {n : ℕ} {mfam : Fin n → ℕ} (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) [(w : Fin n) → DecidableRel (Hfam w).Adj] {w w' : Fin n} (hww : w ≠ w') : Disjoint (SimpleGraph.map (⇑(embedHCopyFam w)) (Hfam w)).edgeFinset (SimpleGraph.map (⇑(embedHCopyFam w')) (Hfam w')).edgeFinset

theorem Graphon.Lovasz.decorateAllFam_F_sup_disjoint {n : ℕ} {mfam : Fin n → ℕ} (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) [(w : Fin n) → DecidableRel (Hfam w).Adj] : Disjoint (SimpleGraph.map (⇑Function.Embedding.inl) F).edgeFinset (Finset.univ.sup fun (w : Fin n) => SimpleGraph.map (⇑(embedHCopyFam w)) (Hfam w)).edgeFinset

theorem Graphon.Lovasz.decorateAllFamSum_sup_edgeFinset {n : ℕ} {mfam : Fin n → ℕ} (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) [(w : Fin n) → DecidableRel (Hfam w).Adj] : (Finset.univ.sup fun (w : Fin n) => SimpleGraph.map (⇑(embedHCopyFam w)) (Hfam w)).edgeFinset = Finset.univ.biUnion fun (w : Fin n) => (SimpleGraph.map (⇑(embedHCopyFam w)) (Hfam w)).edgeFinset

theorem Graphon.Lovasz.decorateAllFam_prod_eq {T n : ℕ} {mfam : Fin n → ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) [(w : Fin n) → DecidableRel (Hfam w).Adj] (τ : Fin (n + ∑ w : Fin n, mfam w + 1) → Fin T) : ∏ E ∈ (decorateAllFam F Hfam).edgeFinset, B (τ (Quot.out E).1) (τ (Quot.out E).2) = (∏ e ∈ F.edgeFinset, B (τ ((decorAllFamVertexEquiv mfam) (Sum.inl (Quot.out e).1))) (τ ((decorAllFamVertexEquiv mfam) (Sum.inl (Quot.out e).2)))) * ∏ w : Fin n, ∏ e ∈ (Hfam w).edgeFinset, B (τ ((decorAllFamVertexEquiv mfam) ((embedHCopyFam w) (Quot.out e).1))) (τ ((decorAllFamVertexEquiv mfam) ((embedHCopyFam w) (Quot.out e).2)))

Edge-product transport + split (C3 / B2-analog): the rootedProfile edge product over decorateAllFam F Hfam factors into the F-edge product times the product over the n per-vertex H-copy edge products.

theorem Graphon.Lovasz.decorAllFamVertexEquiv_inl_val {n : ℕ} (mfam : Fin n → ℕ) (x : Fin (n + 1)) : ↑((decorAllFamVertexEquiv mfam) (Sum.inl x)) = ↑x

theorem Graphon.Lovasz.decorAllFamVertexEquiv_inr_val {n : ℕ} (mfam : Fin n → ℕ) (w : Fin n) (z : Fin (mfam w)) : ↑((decorAllFamVertexEquiv mfam) (Sum.inr ⟨w, z⟩)) = n + 1 + ↑(finSigmaFinEquiv ⟨w, z⟩)

theorem Graphon.Lovasz.consAppendAllFam_inl {T n : ℕ} {mfam : Fin n → ℕ} (v : Fin T) (σF : Fin n → Fin T) (σHflat : Fin (∑ w : Fin n, mfam w) → Fin T) (x : Fin (n + 1)) : Fin.cons v (appendFn σF σHflat) ((decorAllFamVertexEquiv mfam) (Sum.inl x)) = Fin.cons v σF x

C3 F-side value lemma: under appendFn σF σHflat, the value at an F-vertex inl x is Fin.cons v σF x.

theorem Graphon.Lovasz.consAppendAllFam_embedHCopyFam {T n : ℕ} {mfam : Fin n → ℕ} (v : Fin T) (σF : Fin n → Fin T) (σHflat : Fin (∑ w : Fin n, mfam w) → Fin T) (w : Fin n) (a : Fin (mfam w + 1)) : Fin.cons v (appendFn σF σHflat) ((decorAllFamVertexEquiv mfam) ((embedHCopyFam w) a)) = Fin.cons (Fin.cons v σF w.succ) (fun (z : Fin (mfam w)) => σHflat (finSigmaFinEquiv ⟨w, z⟩)) a

C3 H-side value lemma: under appendFn σF σHflat, the w-th H-copy's assignment is Fin.cons (Fin.cons v σF w.succ) (fun z => σHflat (finSigmaFinEquiv ⟨w, z⟩)).

noncomputable def Graphon.Lovasz.flatAssignEquivFam {n : ℕ} (mfam : Fin n → ℕ) (T : ℕ) : ((w : Fin n) → Fin (mfam w) → Fin T) ≃ (Fin (∑ w : Fin n, mfam w) → Fin T)

Family flat ↔ curried assignment equivalence: a flat assignment over the ∑ mfam internal vertices is the same as n dependent per-copy assignments, matched via finSigmaFinEquiv.

Equations

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

theorem Graphon.Lovasz.flatAssignEquivFam_apply_fse {T n : ℕ} {mfam : Fin n → ℕ} (σH : (w : Fin n) → Fin (mfam w) → Fin T) (w : Fin n) (z : Fin (mfam w)) : (flatAssignEquivFam mfam T) σH (finSigmaFinEquiv ⟨w, z⟩) = σH w z

theorem Graphon.Lovasz.flatAssignEquivFam_weight_prod {T n : ℕ} {mfam : Fin n → ℕ} (W : Fin T → ℝ) (σH : (w : Fin n) → Fin (mfam w) → Fin T) : ∏ k : Fin (∑ w : Fin n, mfam w), W ((flatAssignEquivFam mfam T) σH k) = ∏ w : Fin n, ∏ z : Fin (mfam w), W (σH w z)

theorem Graphon.Lovasz.decorateAllFam_Hflat_collapse {T n : ℕ} {mfam : Fin n → ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) [(w : Fin n) → DecidableRel (Hfam w).Adj] (r : Fin n → Fin T) : ∑ σ : Fin (∑ w : Fin n, mfam w) → Fin T, (∏ k : Fin (∑ w : Fin n, mfam w), W (σ k)) * ∏ w : Fin n, ∏ e ∈ (Hfam w).edgeFinset, B (Fin.cons (r w) (fun (z : Fin (mfam w)) => σ (finSigmaFinEquiv ⟨w, z⟩)) (Quot.out e).1) (Fin.cons (r w) (fun (z : Fin (mfam w)) => σ (finSigmaFinEquiv ⟨w, z⟩)) (Quot.out e).2) = ∏ w : Fin n, rootedProfile B W (r w) (Hfam w)

n-fold family H-copy collapse (C3 engine): summing the flat internal assignment factors the n per-vertex glued copies into a product of the n rooted profiles rootedProfile B W (r w) (Hfam w).

theorem Graphon.Lovasz.rootedProfile_decorateAllFam {T n : ℕ} {mfam : Fin n → ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (v : Fin T) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) [(w : Fin n) → DecidableRel (Hfam w).Adj] : rootedProfile B W v (decorateAllFam F Hfam) = ∑ σF : Fin n → Fin T, ((∏ w : Fin n, W (σF w)) * ∏ e ∈ F.edgeFinset, B (Fin.cons v σF (Quot.out e).1) (Fin.cons v σF (Quot.out e).2)) * ∏ w : Fin n, rootedProfile B W (σF w) (Hfam w)

C3 — per-vertex-family decoration factorization: decorating each unlabeled vertex w of F with Hfam w multiplies each F-assignment's contribution by ∏ w, rootedProfile B W (σF w) (Hfam w). The varying-graph generalization of rootedProfile_decorateAll.

Decorated power sums — the bridge to classwise row-value measures

rowValueMeasure_eq_of_rootedProfileEquiv gives equality of the GLOBAL W-weighted row-value measures. The next step toward the rank theorem vertexOrbitRel_of_rootedProfileEquiv is equality INSIDE each rooted-profile atom class — obtained by decorating the power sums with atom indicators.

theorem Graphon.Lovasz.InRootedProfileSpan.finset_sum' {T : ℕ} {B : Fin T → Fin T → ℝ} {W : Fin T → ℝ} {α : Type u_1} (S : Finset α) (g : α → Fin T → ℝ) (hg : ∀ a ∈ S, InRootedProfileSpan B W (g a)) : InRootedProfileSpan B W fun (v : Fin T) => ∑ a ∈ S, g a v

Finite-sum closure of the rooted-profile span (CycleKrylov-local copy of the private Lovasz helper, built from .zero/.add).

theorem Graphon.Lovasz.weightMod_profile_mem_span {T n : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] {g : Fin T → ℝ} (hg : InRootedProfileSpan B W g) : InRootedProfileSpan B W fun (v : Fin T) => rootedProfile B (fun (t : Fin T) => W t * g t) v F

C3 — modified-weight profile stays in the span (PROVED). For any g in the (B, W)-rooted-profile span and any graph F, the modified-weight profile v ↦ rootedProfile B (W·g) v F lies in InRootedProfileSpan B W.

Construction: expanding g = ∑_k c_k · rootedProfileFun B W H_k from hg, the per-vertex product ∏_w g(σ w) = ∑_φ ∏_w c_{φ w} · rootedProfile B W (σ w) H_{φ w} (Finset.prod_univ_sum); distributing turns rootedProfile B (W·g) v F into ∑_φ (∏_w c_{φ w}) · rootedProfile B W v (decorateAllFam F (fun w => H_{φ w})), a finite linear combination of bare profiles of per-vertex glued graphs — hence in the span by InRootedProfileSpan.{finset_sum, smul}. The single-H case (decorateAllFam constant) is rootedProfile_weightMul_of_profile_mem_span (B4). The general case uses the per-vertex-family glue decorateAllFam (a Σ-indexed generalization of decorateAll, sizes handled by finSigmaFinEquiv, not casts).

theorem Graphon.Lovasz.rootedProfileEquiv_weightMod {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) {i j : Fin T} (h : rootedProfileEquiv B W i j) {g : Fin T → ℝ} (hg : InRootedProfileSpan B W g) : rootedProfileEquiv B (fun (t : Fin T) => W t * g t) i j

Weight modification preserves rooted-profile equivalence (C4 — PROVED modulo the focused span-membership lemma weightMod_profile_mem_span). For any g in the (B, W)-rooted-profile span, rooted-profile-equivalent vertices stay equivalent under the modified weight W · g. The analytic content is discharged: the modified-weight profile lies in the span (weightMod_profile_mem_span), and span elements are constant on rpe-classes (InRootedProfileSpan.const_on_rpe).

theorem Graphon.Lovasz.decoratedPowerSum_descends_of_rootedProfileEquiv {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) {i j : Fin T} (h : rootedProfileEquiv B W i j) {g : Fin T → ℝ} (hg : InRootedProfileSpan B W g) (k : ℕ) : ∑ t : Fin T, W t * g t * B i t ^ k = ∑ t : Fin T, W t * g t * B j t ^ k

Decorated power sums descend (PROVED, via rootedProfileEquiv_weightMod above). For g in the rooted-profile span (e.g. an atom indicator rpeIndicator C), the g-decorated power sums of rpe-equivalent rows agree at every degree k. With g = 1_C and k = 2 this is classwise_sqMoment_descends; in general it gives equality of the row-value measures inside every atom class.

Proof: shift g by a positive constant c so g + c > 0 and stays in the span, apply powerSum_descends_of_rootedProfileEquiv at the positive weight W·(g + c) (rpe-preserved by rootedProfileEquiv_weightMod) and at W, then subtract (∑ W·g·B^k = ∑ W·(g+c)·B^k − c·∑ W·B^k).

theorem Graphon.Lovasz.classwise_sqMoment_descends {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (_htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {i j : Fin T} (h : rootedProfileEquiv B W i j) {g : Fin T → ℝ} (hg : ∀ (a b : Fin T), rootedProfileEquiv B W a b → g a = g b) : ∑ t : Fin T, W t * B i t ^ 2 * g t = ∑ t : Fin T, W t * B j t ^ 2 * g t

Classwise square-moment descent (PROVED — no twin-free needed). For any atom-invariant g, the g-decorated square moments of rpe-equivalent rows agree. The k = 2 specialization of decoratedPowerSum_descends_of_rootedProfileEquiv, with span membership supplied by the K=1 fullness theorem InRootedProfileSpan.of_const_on_rpe (atom-invariant ⟹ in the span). The htwin hypothesis is retained for API compatibility but is unused — the weight-modification route closes this WITHOUT twin-freeness, unlike the older singular-M stratum route.

theorem Graphon.Lovasz.classwise_rowValueMeasure_eq_of_rootedProfileEquiv {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) {i j : Fin T} (h : rootedProfileEquiv B W i j) (r : Fin T) (a : ℝ) : ∑ t : Fin T with B i t = a, W t * rpeIndicator B W r t = ∑ t : Fin T with B j t = a, W t * rpeIndicator B W r t

Classwise row-value measures descend (PROVED). Under rooted-profile equivalence i ~ j, the two rows B i and B j have the SAME W-weighted value distribution INSIDE every atom class C = atom(r) (the rpe-class of a representative r). Phrased with the atom-restricting weight W · rpeIndicator B W r (which is W on the class and 0 off it), so the indicator-weighted preimage mass ∑_{t : B i t = a} W t · 1_{atom(r)}(t) is exactly the W-mass of {t ∈ atom(r) : B i t = a} — see classwise_rowValueMeasure_eq_filter for the class-filtered restatement.

The classwise refinement of rowValueMeasure_eq_of_rootedProfileEquiv: apply weighted_powersum_determines_measure with weight W · rpeIndicator B W r, whose moments descend by decoratedPowerSum_descends_of_rootedProfileEquiv (span membership from rpeIndicator_mem_span). The bridge to the orbit/rank theorem.

Chunk A — the atom-class coherent structure

The invariants needed to build a weighted coherent configuration on the atom partition of rootedProfileEquiv. atomTransMeasure q i a = the W-mass of the value-a fibre of row B i restricted to atom class atom(q) — the "transition measure" from the atom of i to the atom of q. The key fact (atomTransMeasure_eq_of_rpe) is that it depends only on the atom of i, not the representative — exactly the coherent-configuration coherence condition. This is the constructive input for the orbit/rank theorem vertexOrbitRel_of_rootedProfileEquiv; it does NOT yet build automorphisms (equal W-masses give a coupling, not a bijection, with arbitrary positive real weights).

theorem Graphon.Lovasz.atom_row_value_measure_eq {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) {i j : Fin T} (h : rootedProfileEquiv B W i j) (r : Fin T) (a : ℝ) : (∑ t : Fin T, W t * rpeIndicator B W r t * if B i t = a then 1 else 0) = ∑ t : Fin T, W t * rpeIndicator B W r t * if B j t = a then 1 else 0

Indicator-if form of classwise row-value-measure equality (wrapper around classwise_rowValueMeasure_eq_of_rootedProfileEquiv): for rpe-equivalent i, j and any atom representative r and value a, the atom-restricted value masses agree.

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

The total W-mass of the atom class of r (= ∑_{t ∈ atom(r)} W t).

Equations

• Graphon.Lovasz.atomWeight B W r = ∑ t : Fin T, W t * Graphon.Lovasz.rpeIndicator B W r t

theorem Graphon.Lovasz.atomWeight_pos {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (r : Fin T) : 0 < atomWeight B W r

Every atom class has positive W-weight (it contains its representative r, and W r > 0).

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

Atom transition measure: the W-mass of the value-a fibre of row B i inside atom class atom(q). (The source atom is the atom of i.)

Equations

• Graphon.Lovasz.atomTransMeasure B W q i a = ∑ t : Fin T, W t * Graphon.Lovasz.rpeIndicator B W q t * if B i t = a then 1 else 0

theorem Graphon.Lovasz.atomTransMeasure_eq_of_rpe {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) {i j : Fin T} (h : rootedProfileEquiv B W i j) (q : Fin T) (a : ℝ) : atomTransMeasure B W q i a = atomTransMeasure B W q j a

Coherence: the atom transition measure depends only on the ATOM of i, not the chosen representative — the coherent-configuration condition.

theorem Graphon.Lovasz.atom_row_signature_eq {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) {i j : Fin T} (h : rootedProfileEquiv B W i j) (q : Fin T) : (fun (a : ℝ) => atomTransMeasure B W q i a) = fun (a : ℝ) => atomTransMeasure B W q j a

Row signature equality inside atoms (the coherent-configuration object): rpe-equivalent rows B i, B j have the SAME atom-restricted value distribution (a ↦ atomTransMeasure q i a) for every target atom q.

§7 — atoms = orbits (#70 paper-root), via the DIRECT multigraph route

The #70 rank theorem vertexOrbitRel_of_rootedProfileEquiv factors through the PROVED, axiom-clean multigraph Lemma 2.4 tupleEquivMulti_implies_orbit:

rootedProfileEquiv → tupleEquivMulti → vertexOrbitRel.

The middle arrow was the only remaining content when this section was written — the focused bridge tupleEquivMulti_of_rootedProfileEquiv (simple-rpe ⟹ multigraph tuple-equivalence at K=1) — and it is now PROVED below, closing #70. No marker/augmentation is needed: tupleEquivMulti uses the SAME (B,W), with multigraphs as the PROBES. These declarations were relocated here from SimpleRank.lean (they have no upstream consumers) because the bridge's eventual proof uses the decorated/classwise power-sum machinery defined above.

theorem Graphon.Lovasz.starProbe_descends {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) {i j : Fin T} (h : rootedProfileEquiv B W i j) (a : ℕ) : (multiLabeledEvalK 1 1 (starProbe a) B W fun (x : Fin 1) => i) = multiLabeledEvalK 1 1 (starProbe a) B W fun (x : Fin 1) => j

Tree-fragment, base case: the multiplicity-a star probe descends — its evaluation is the a-th weighted power sum, which descends by powerSum_descends.

theorem Graphon.Lovasz.decoratedProbe_descends {T m : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (a : ℕ) (Mχ : MultiLabeledGraph 1 m) (hχ : ∀ (p q : Fin T), rootedProfileEquiv B W p q → (multiLabeledEvalK 1 m Mχ B W fun (x : Fin 1) => p) = multiLabeledEvalK 1 m Mχ B W fun (x : Fin 1) => q) {i j : Fin T} (h : rootedProfileEquiv B W i j) : (multiLabeledEvalK 1 (m + 1) (decoratedProbe a Mχ) B W fun (x : Fin 1) => i) = multiLabeledEvalK 1 (m + 1) (decoratedProbe a Mχ) B W fun (x : Fin 1) => j

Tree-fragment, inductive step: if the sub-probe Mχ descends (its evaluation is atom-invariant), then the decorated star probe decoratedProbe a Mχ descends. Its evaluation ∑ₜ W t · B i t ^ a · χ(t) is a decorated power sum with χ in the span (of_const_on_rpe), so decoratedPowerSum_descends applies. Together with starProbe_descends this gives, by induction on tree depth, that EVERY tree (= WL) multigraph probe descends — the part of tupleEquivMulti_of_rootedProfileEquiv already in reach.

theorem Graphon.Lovasz.rootedMultiEval_ofSimple_mem {T n : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (F : SimpleGraph (Fin (n + 1))) [DecidableRel F.Adj] : InRootedProfileSpan B W fun (v : Fin T) => multiLabeledEvalK 1 n (MultiLabeledGraph.ofSimple F) B W fun (x : Fin 1) => v

Base case (simple M): a 0/1-multigraph ofSimple F evaluates to the rooted profile of F, so it lies in the span directly (of_profile).

theorem Graphon.Lovasz.rootedMultiEval_starProbe_mem {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (a : ℕ) : InRootedProfileSpan B W fun (v : Fin T) => multiLabeledEvalK 1 1 (starProbe a) B W fun (x : Fin 1) => v

Base case (root-incident multi-edge / power sum): the multiplicity-a star probe evaluates to ∑ₜ W t · B v t ^ a, atom-invariant by powerSum_descends, hence in the span by of_const_on_rpe (non-circular — the descent is independently proved).

theorem Graphon.Lovasz.rootedMultiEval_decoratedProbe_mem {T m : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (a : ℕ) (Mχ : MultiLabeledGraph 1 m) (hMχ : InRootedProfileSpan B W fun (v : Fin T) => multiLabeledEvalK 1 m Mχ B W fun (x : Fin 1) => v) : InRootedProfileSpan B W fun (v : Fin T) => multiLabeledEvalK 1 (m + 1) (decoratedProbe a Mχ) B W fun (x : Fin 1) => v

Base case (tree / decorated probe): if the sub-probe Mχ lies in the span, so does decoratedProbe a Mχ — atom-invariance via decoratedProbe_descends (using const_on_rpe of the Mχ-membership), then of_const_on_rpe.

theorem Graphon.Lovasz.rootedProfileSpan_pairDiagonal {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) {g h : Fin T → ℝ} (hg : InRootedProfileSpan B W g) (hh : InRootedProfileSpan B W h) : InRootedProfileSpan B W fun (v : Fin T) => ∑ s : Fin T, W s * B v s * g s * h s

Warm-up diagonal primitive (one neighbour, PROVED): for g, h in the span, the "same-vertex" decorated first moment v ↦ ∑ₛ W s · B v s · g s · h s lies in the span — via InRootedProfileSpan.mul then .weightedAdj. This extracts a coincidence at ONE neighbour; the internal doubled edge needs the two-variable coincidence detector (tupleEquivSimple_preserves_diagonal).

def Graphon.Lovasz.commonNeighborGraph : SimpleGraph (Fin (1 + 2))

Common-neighbour simple graph: two labels 0, 1 both joined to the single unlabeled vertex 2 (no 0–1 edge). Its rooted evaluation reads ⟨B(ξ 0), B(ξ 1)⟩_W.

Equations

• Graphon.Lovasz.commonNeighborGraph = SimpleGraph.fromEdgeSet {s(0, 2), s(1, 2)}

@[implicit_reducible]

noncomputable instance Graphon.Lovasz.instDecidableRelFinHAddNatOfNatAdjCommonNeighborGraph : DecidableRel commonNeighborGraph.Adj

Equations

• Graphon.Lovasz.instDecidableRelFinHAddNatOfNatAdjCommonNeighborGraph = Classical.decRel Graphon.Lovasz.commonNeighborGraph.Adj

theorem Graphon.Lovasz.commonNeighborGraph_edgeFinset : commonNeighborGraph.edgeFinset = {s(0, 2), s(1, 2)}

theorem Graphon.Lovasz.simpleEvalAt_commonNeighbor {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (ξ : Fin 2 → Fin T) : simpleEvalAt B W commonNeighborGraph ξ = ∑ t : Fin T, W t * B (ξ 0) t * B (ξ 1) t

Common-neighbour evaluation: simpleEvalAt commonNeighborGraph ξ = ∑ₜ W t · B (ξ 0) t · B (ξ 1) t = ⟨B (ξ 0), B (ξ 1)⟩_W.

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

Coincidence detector (tupleEquivSimple preserves the diagonal) — the KEY book step for internal multi-edge elimination (formerly a FOCUSED SORRY; PROVED below). If two 2-tuples are simple-equivalent and one is diagonal (ξ 0 = ξ 1), so is the other.

Mechanism (non-circular, settled): instantiate tupleEquivSimple at the common-neighbour simple graph (two labels both joined to one unlabeled vertex), whose eval is ⟨B (ξ 0), B (ξ 1)⟩_W = ∑ᵤ W u · B (ξ 0) u · B (ξ 1) u. For diagonal ξ (so ξ 0 = ξ 1 = s) this and the single-label squares give ⟨B (ξ' 0), B (ξ' 1)⟩_W = ‖B (ξ' 0)‖²_W = ‖B (ξ' 1)‖²_W = sqMoment s (single-label restriction + sqMoment_descends), whence ‖B (ξ' 0) − B (ξ' 1)‖²_W = s − 2s + s = 0, so B (ξ' 0) = B (ξ' 1) (positive W); twin-free then forces ξ' 0 = ξ' 1. Uses only proved tools. Consequence: the diagonal indicator is constant on tupleEquivSimple-classes ⟹ in the simple closure (of_const_on_tupleEquivSimple, the Lagrange-over-values step), the primitive that extracts the internal B s t².

theorem Graphon.Lovasz.diagIndicator_mem_simpleClosure {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) : InSimpleProfileClosure B W 2 fun (ξ : Fin 2 → Fin T) => if ξ 0 = ξ 1 then 1 else 0

Diagonal indicator in the simple profile closure (PROVED): the function ξ ↦ [ξ 0 = ξ 1] lies in the K = 2 simple-profile closure. Since tupleEquivSimple_preserves_diagonal shows it is constant on tupleEquivSimple-classes, the proved Lagrange-fullness of_const_on_tupleEquivSimple puts it in the closure. This is the clean algebraic diagonal extractor (the idempotent that detects vertex coincidence).

theorem Graphon.Lovasz.InRootedProfileSpan.of_tupleSimpleEvalSpan {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {f : (Fin 1 → Fin T) → ℝ} (h : InTupleSimpleEvalSpan B W f) : InRootedProfileSpan B W fun (v : Fin T) => f fun (x : Fin 1) => v

K=1 bridge: simple-eval span ⟹ rooted-profile span. At K = 1 the carrier types coincide (Σ n, SimpleGraph (Fin (n + 1)) in both) and rootedProfileFun B W F v = simpleEvalAt B W F (·↦v) definitionally (rootedProfile := simpleEvalAt _ _ _ (fun _ : Fin 1 => ·)), so a Fin 1-tuple simple-eval span element, read at the constant tuple, is a rooted-profile span element with the SAME data.

theorem Graphon.Lovasz.rootedMultiEval_mem_rootedProfileSpan {T n : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) (M : MultiLabeledGraph 1 n) : InRootedProfileSpan B W fun (v : Fin T) => multiLabeledEvalK 1 n M B W fun (x : Fin 1) => v

Rooted multigraph evaluations lie in the simple rooted-profile span (THE #70 paper-root — the K=1 case of InTupleMultiEvalSpan.toSimple, i.e. Lovász Lemma 2.5 specialized to a single root). For every rooted multigraph probe M, the function v ↦ multiLabeledEvalK 1 n M B W (·↦v) lies in InRootedProfileSpan B W.

PROVED via the (formerly canonical-residue, since-proved) InTupleMultiEvalSpan.toSimple (Lovász §3 / Lemma 2.5): the K=1 multigraph eval lies in the multigraph-eval span (of_multi); toSimple hB hW htwin collapses it into the simple-eval span (this is where the Hadamard-square obstruction — internal multiplicity ≥2 — genuinely lives, equivalently InTupleSimpleEvalSpan.mul); the K=1 bridge of_tupleSimpleEvalSpan repackages it as a rooted-profile span element. This consolidates #70 onto the single canonical residue: the direct diagonal-extraction route (diagIndicator_mem_simpleClosure, tupleEquivSimple_preserves_diagonal, the decorated/star machinery) bottoms out at the same closure→linear-span gap, so the honest dependency is toSimple, not a separate multi-edge-elimination theorem.

theorem Graphon.Lovasz.tupleEquivMulti_of_rootedProfileEquiv {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (t : Fin T), 0 < W t) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {i j : Fin T} (h : rootedProfileEquiv B W i j) : tupleEquivMulti B W (fun (x : Fin 1) => i) fun (x : Fin 1) => j

The simple → multigraph bridge at K=1 (PROVED, via rootedMultiEval_mem_rootedProfileSpan, itself proved above — closing #70). Rooted simple-profile equivalence implies MULTIGRAPH tuple-equivalence: every multigraph probe evaluates identically on rpe-equivalent vertices. Immediate from membership of each rooted multigraph eval in the simple span (rootedMultiEval_mem_rootedProfileSpan) and the fact that span elements are constant on rpe-classes (InRootedProfileSpan.const_on_rpe).

theorem Graphon.Lovasz.vertexOrbitRel_of_rootedProfileEquiv {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) {i j : Fin T} (h : rootedProfileEquiv B W i j) : vertexOrbitRel B W i j

The K=1 simple-graph rank theorem (#70): rooted-profile equivalence implies vertex-orbit equivalence — the atoms of the rooted simple-profile algebra are exactly the (B, W)-automorphism orbits. Fully PROVED: routes through the focused bridge tupleEquivMulti_of_rootedProfileEquiv (proved above) and the proved multigraph Lemma 2.4.

theorem Graphon.Lovasz.algebraAtomRel_eq_vertexOrbitRel {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) (i j : Fin T) : algebraAtomRel B W i j ↔ vertexOrbitRel B W i j

Atoms = orbits, packaged form of the rank theorem. Fully PROVED, via tupleEquivMulti_of_rootedProfileEquiv (proved above) and vertexOrbitRel_of_rootedProfileEquiv.

theorem Graphon.Lovasz.InRootedProfileSpan.of_const_on_orbit_noncircular {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (hW : ∀ (i : Fin T), 0 < W i) (htwin : ∀ (i j : Fin T), i ≠ j → B i ≠ B j) (f : Fin T → ℝ) (hf : ∀ (i j : Fin T), vertexOrbitRel B W i j → f i = f j) : InRootedProfileSpan B W f

Non-circular of_const_on_orbit — an orbit-invariant function is atom-invariant (atoms = orbits) hence in the span (of_const_on_rpe). Replaces the cyclically-proved InRootedProfileSpan.of_const_on_orbit in Lovasz.lean. Fully PROVED, via tupleEquivMulti_of_rootedProfileEquiv (proved above).

Eval spans as Submodules + Phase C1+D rank skeleton

MOVED upstream to Lovasz.lean (§ the rank-theorem section, 2026-07-02): the submodule packaging (simpleEvalSubmodule/multiEvalSubmodule/orbitInvariantSubmodule + membership iffs and inclusions) and the full rank skeleton (incl. instFintypeOrbitClass and the PROVED simpleEvalSubmodule_eq_orbitInvariantSubmodule) now live directly after simpleEvalAt_aut_invariant in Lovasz.lean, where the Cai–Govorov machinery they need is in scope. All names resolve through the import chain.