The simple-graph rank theorem, K=1 (task #70) — non-circular algebra-atom framing

This module is the FRESH-PROJECT scaffold for the K=1 simple-graph rank theorem (Lovász TR-2004-82 §3/§4.2 for simple rooted profiles), the last open paper-root after #62/#73 (multigraph reconstruction) closed sorry-free.

Historical note (resolved 2026-07-02). The narrative below describes the scaffold as designed and is retained as the design/history record. The two results it marks "SORRY" have both since been PROVED in Graphon/CycleKrylov.lean: the #70 paper-root vertexOrbitRel_of_rootedProfileEquiv (item 3) and classwise_sqMoment_descends (item 4) — the focused bridge tupleEquivMulti_of_rootedProfileEquiv landed, closing #70. The "triangular cycle" sorry at the "both non-surjective" branch of Lemma 2.4 K=1 (Lovasz.lean) was closed by the Cai–Govorov descent. This file itself is sorry-free (see the inventory at the end of this header).

The problem

Graphon/Lovasz.lean proves InRootedProfileSpan.of_const_on_orbit (orbit-invariant functions lie in the rooted simple-profile span) via mkRootedSeparator → k1_orbit_sep_aux → tupleEquivSimple_implies_orbit — a triangular cycle whose actual sorry sits at the "both non-surjective" branch of Lemma 2.4 K=1 (Lovasz.lean L7589). All three statements are mutually equivalent; none has an independently proved base case.

The non-circular reformulation (this file)

Replace orbit-separators (which need the cycle) by definitional separators:

1. Algebra atoms. algebraAtomRel B W i j ↔ ∀ f ∈ InRootedProfileSpan, f i = f j. This relation is exactly rootedProfileEquiv (algebraAtomRel_iff_rootedProfileEquiv, PROVED below — both directions are trivial). The atoms of the rooted-profile algebra are the rooted-profile-equivalence classes, NOT (a priori) the orbits.

2. Idempotent indicators. For ¬rootedProfileEquiv i j a separating rooted profile exists by definition (exists_rpe_separator — no k1_orbit_sep_aux!). Lagrange interpolation over the atom partition then puts each atom indicator rpeIndicator in the span (rpeIndicator_mem_span), and every atom-invariant function follows (InRootedProfileSpan.of_const_on_rpe). Both PROVED below, non-circularly — only hB (symmetry) is needed, no hW/htwin.

3. The hard theorem (the genuine #70 content, SORRY at the time; since PROVED in Graphon/CycleKrylov.lean): vertexOrbitRel_of_rootedProfileEquiv : atoms = orbits, i.e. rootedProfileEquiv B W i j → vertexOrbitRel B W i j (twin-free B, W > 0). Once proved, of_const_on_orbit is re-derived non-circularly (InRootedProfileSpan.of_const_on_orbit_noncircular, PROVED modulo the hard theorem), and the whole #70 cascade closes.

4. Minimal test case — FULLY PROVED (2026-06-10, sorry-free): plain square-moment descent sqMoment_descends_of_rootedProfileEquiv is formalized in Graphon/CycleKrylov.lean via the cycle–Krylov–kernel argument (see also scripts/validate_sqmoment_cycle_krylov.py): with ε = B i - B j, u = B i + B j, M = B ∘ D_W, rooted (q+2)-cycle differences are exactly ⟨ε, M^q u⟩_W; rpe kills them for q ≥ 1; u = M (D_W⁻¹ (e i + e j)) ∈ Im M and self-adjointness give u ∈ span{M^q u : q ≥ 1}; hence gap = ⟨ε, u⟩_W = 0. Needs only hB, hW — no twin-freeness. The classwise form (classwise_sqMoment_descends, SORRY at the time; since PROVED in Graphon/CycleKrylov.lean) is reduced by the same argument (palindromic decorated cycles) to the singular-M stratum: gap_g = ⟨D_g ε, P_ker(M) (D_g u)⟩_W, zero whenever det B ≠ 0.

5. Decorated tree observables (PROVED, §6): the span is closed under the weighted adjacency step weightedAdj (pendant attachment), so all tree observables with atom-invariant decorations descend; in particular classwise FIRST moments descend (first_moment_descends_of_rootedProfileEquiv) — the atom partition is an equitable partition of (B, W). A uniform span expression of the square moment is impossible by W-grading (see §6 docstring), so the open content is genuinely per-instance: within-atom distributions beyond means.

Known-BAD routes (do not retry; see project memory lovasz-70-orbit-separation-simple)

• closed-walk / trace observables;
• WL / color-refinement / fractional automorphisms (stable_imp_vertexOrbitRel is KNOWN-FALSE — Frucht graph);
• marker gadget (Cor 2.6 augmentation): the square moment leaks one step past the marker (1ᵐ = 1 collapses only marker-incident multi-edges, not the p–t double edge), so the augmented simple profile does not determine it;
• "the proved multigraph theorem shortcuts it": converting multi-separators to simple ones is exactly the cycle.

Sorry inventory of this file (0)

This file is now SORRY-FREE. The #70 paper-root vertexOrbitRel_of_rootedProfileEquiv (and classwise_sqMoment_descends) were relocated to Graphon/CycleKrylov.lean, where #70 was reduced — via the proved multigraph Lemma 2.4 — to the single focused bridge tupleEquivMulti_of_rootedProfileEquiv (simple-rpe ⟹ multigraph equivalence); that bridge has since been PROVED there, closing #70 (2026-07-02).

§1 — rootedProfileEquiv is an equivalence relation

theorem Graphon.Lovasz.rootedProfileEquiv.refl {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i : Fin T) : rootedProfileEquiv B W i i

Reflexivity of rooted-profile equivalence.

theorem Graphon.Lovasz.rootedProfileEquiv.symm {T : ℕ} {B : Fin T → Fin T → ℝ} {W : Fin T → ℝ} {i j : Fin T} (h : rootedProfileEquiv B W i j) : rootedProfileEquiv B W j i

Symmetry of rooted-profile equivalence.

theorem Graphon.Lovasz.rootedProfileEquiv.trans {T : ℕ} {B : Fin T → Fin T → ℝ} {W : Fin T → ℝ} {i j k : Fin T} (h₁ : rootedProfileEquiv B W i j) (h₂ : rootedProfileEquiv B W j k) : rootedProfileEquiv B W i k

Transitivity of rooted-profile equivalence.

§2 — Algebra atoms of the rooted-profile span

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

Algebra-atom relation of the rooted-profile span: two vertices are atom-related iff every function in the span agrees on them. The atoms of the (finite-dimensional, multiplicatively closed) subalgebra InRootedProfileSpan B W ⊆ (Fin T → ℝ) are the classes of this relation.

Equations

• Graphon.Lovasz.algebraAtomRel B W i j = ∀ (f : Fin T → ℝ), Graphon.Lovasz.InRootedProfileSpan B W f → f i = f j

theorem Graphon.Lovasz.algebraAtomRel_iff_rootedProfileEquiv {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i j : Fin T) : algebraAtomRel B W i j ↔ rootedProfileEquiv B W i j

The atom partition is the rooted-profile-equivalence partition — NOT (a priori) the orbit partition. Both directions are trivial and non-circular: generators are in the span (of_profile), and span members are constant on rooted-profile classes (const_on_rpe). Identifying these atoms with orbits is the genuine open theorem vertexOrbitRel_of_rootedProfileEquiv below.

§3 — Definitional separators (the non-circular ingredient)

For the orbit relation, producing a separating rooted profile from ¬ vertexOrbitRel B W i j requires the rank theorem itself (k1_orbit_sep_aux — the cycle). For rooted-profile equivalence the separator is free: it is the literal content of the negated definition. This is what makes the atom framing non-circular.

structure Graphon.Lovasz.RpeSeparator {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i j : Fin T) : Type

Rooted-profile-equivalence separator: explicit witness record for ¬ rootedProfileEquiv B W i j. Mirrors RootedSeparator (private in Lovasz.lean) but is built from the definition of the equivalence, not from the orbit-separation cycle.

• n : ℕ

  Number of unlabeled vertices.

• F : SimpleGraph (Fin (self.n + 1))

  The separating rooted simple graph.

• inst : DecidableRel self.F.Adj

  Bundled decidability instance for F.Adj.

• sep : rootedProfile B W i self.F ≠ rootedProfile B W j self.F

  The separation property.

theorem Graphon.Lovasz.exists_rpe_separator {T : ℕ} {B : Fin T → Fin T → ℝ} {W : Fin T → ℝ} {i j : Fin T} (h : ¬rootedProfileEquiv B W i j) : ∃ (n : ℕ) (F : SimpleGraph (Fin (n + 1))) (inst : DecidableRel F.Adj), rootedProfile B W i F ≠ rootedProfile B W j F

Non-equivalent vertices are separated by some rooted profile — by definition.

noncomputable def Graphon.Lovasz.mkRpeSeparator {T : ℕ} {B : Fin T → Fin T → ℝ} {W : Fin T → ℝ} {i j : Fin T} (h : ¬rootedProfileEquiv B W i j) : RpeSeparator B W i j

Build an RpeSeparator from non-equivalence via Classical.choose.

Equations

• Graphon.Lovasz.mkRpeSeparator h = { n := ⋯.choose, F := ⋯.choose, inst := ⋯.choose, sep := ⋯ }

§4 — Local algebra-closure helpers

File-local re-derivations of closure lemmas that are private in Lovasz.lean (finset_prod, finset_sum, profile_sub_const, lagrange_factor). Verbatim ports; kept private here too.

§5 — Idempotent atom indicators (Lovász §4.2, non-circular)

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

Atom indicator of the rooted-profile-equivalence class of i: the 0/1 function picking out the algebra atom containing i. The §4.2 idempotents of the rooted-profile algebra.

Equations

• Graphon.Lovasz.rpeIndicator B W i v = if Graphon.Lovasz.rootedProfileEquiv B W i v then 1 else 0

theorem Graphon.Lovasz.rpeIndicator_idem {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i : Fin T) : (fun (v : Fin T) => rpeIndicator B W i v * rpeIndicator B W i v) = rpeIndicator B W i

The atom indicators are idempotent (pointwise 0/1).

theorem Graphon.Lovasz.rpeIndicator_const_on_rpe {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i a b : Fin T) : rootedProfileEquiv B W a b → rpeIndicator B W i a = rpeIndicator B W i b

Atom indicators are constant on atoms.

theorem Graphon.Lovasz.rpeIndicator_mem_span {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (i : Fin T) : InRootedProfileSpan B W (rpeIndicator B W i)

Atom indicators lie in the rooted-profile span — the non-circular Lagrange interpolation. Separators come from mkRpeSeparator (definitional), NOT from mkRootedSeparator/k1_orbit_sep_aux (the cycle). Note the hypotheses: only symmetry of B (for InRootedProfileSpan.mul); no twin-freeness, no positivity.

theorem Graphon.Lovasz.InRootedProfileSpan.of_const_on_rpe {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W f : Fin T → ℝ) (hf : ∀ (i j : Fin T), rootedProfileEquiv B W i j → f i = f j) : InRootedProfileSpan B W f

Atom-invariant functions lie in the rooted-profile span — the non-circular K=1 fullness theorem (Lovász §4.2 for the simple rooted algebra). Together with algebraAtomRel_iff_rootedProfileEquiv this says: the span is EXACTLY the functions constant on algebra atoms. The open question (#70) is only whether atoms = orbits.

§6 — Span closure under the weighted adjacency step (decorated trees)

The pendant-attachment construction: given a rooted graph G, attach a new root by a single edge to G's old root. Its rooted profile realizes the weighted adjacency operator weightedAdj B W f i = ∑ t, W t * B i t * f t applied to G's profile. Consequently the rooted-profile span is closed under weightedAdj (InRootedProfileSpan.weightedAdj).

Together with mul/const/of_const_on_rpe, this generates every decorated-tree observable: stars are products of first moments, paths are iterated weightedAdj, and arbitrary trees with atom-invariant decorations at every vertex follow by induction (decorations enter via of_const_on_rpe, multiplied in before each weightedAdj step). In particular the classwise first moments ∑ t, W t * B v t * 1_C(t) (atom C) are atom-invariant functions of the root (first_moment_descends_of_rootedProfileEquiv).

Why no direct expression of the square moment exists (attack step 2, negative): under the scaling W ↦ λW, the profile of a rooted graph with m unlabeled vertices scales as λ^m, while ∑ t, W t * B v t ^ 2 scales as λ¹. A (B, W)-uniform span representation could therefore use only graphs with exactly one unlabeled vertex — K₂ and K₁ — whose profiles are m₁(v) = ∑ t, W t * B v t and 1; generic B refutes sqMoment = a·m₁ + b. So square-moment descent cannot be a uniform algebra identity; it must use the per-instance atom structure (or new mathematics). The constructions below are ported from the rootAttach block of MatrixDetermination.lean (private there), adapted from rootedEval to rootedProfile/simpleEvalAt.

theorem Graphon.Lovasz.InRootedProfileSpan.weightedAdj {T : ℕ} {B : Fin T → Fin T → ℝ} (hB : ∀ (i j : Fin T), B i j = B j i) {W g : Fin T → ℝ} (hg : InRootedProfileSpan B W g) : InRootedProfileSpan B W (Lovasz.weightedAdj B W g)

The rooted-profile span is closed under the weighted adjacency step: if g is in the span, so is weightedAdj B W g = fun v => ∑ t, W t * B v t * g t. Witnessed by pendant attachment on each generator. Non-circular (only hB).

theorem Graphon.Lovasz.first_moment_descends_of_rootedProfileEquiv {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 : ∀ (a b : Fin T), rootedProfileEquiv B W a b → g a = g b) : ∑ t : Fin T, W t * B i t * g t = ∑ t : Fin T, W t * B j t * g t

Classwise first moments descend (attack steps 1+3, PROVED).

If i, j are rooted-profile equivalent and g is any atom-invariant decoration (e.g. the atom indicator 1_C), the g-decorated first moments agree. With g = 1_C this says ∑_{t ∈ C} W t * B i t = ∑_{t ∈ C} W t * B j t for every algebra atom C: the atom partition is an equitable partition of the weighted graph (B, W), and the atom-quotient matrix B̄(D, C) := ∑_{t ∈ C} W t * B(s, t) (any s ∈ D) is well defined.

§7 — THE hard theorem: algebra atoms = orbits (#70 paper-root)

The K=1 simple-graph rank theorem (#70 paper-root) and its two packaged corollaries algebraAtomRel_eq_vertexOrbitRel and InRootedProfileSpan.of_const_on_orbit_noncircular now live in Graphon/CycleKrylov.lean — they are reduced there, via the DIRECT multigraph route, to the single focused bridge tupleEquivMulti_of_rootedProfileEquiv (simple-rpe ⟹ multigraph tuple-equivalence at K=1) composed with the PROVED multigraph Lemma 2.4 tupleEquivMulti_implies_orbit. The reduction needs the decorated/classwise power-sum machinery (decoratedPowerSum_descends_*), which is downstream of this file, so the declarations were relocated to break the import cycle. The three leaf decls had no upstream consumers.

§8 — The minimal obstruction: square-moment descent

§6 proved that first moments with atom-invariant decorations descend. The square moment ∑ t, W t * B i t ^ 2 decomposes over atoms as ∑_C ∑_{t ∈ C} W t * B i t ^ 2, so the sharpest currently-underivable family (attack step 4) is the classwise square moments: within each atom C, the distribution of B(i, ·)|_C beyond its (known) mean. Cycle-type observables (triangles etc. through the root, decorated) give bilinear couplings ∑_{t,s} W t W s B(i,t) B(t,s) B(s,i) 1_C(t) 1_D(s) — quadratic in the row but never the diagonal t = s term in isolation; formalizing those requires a two-point attachment construction (deferred).

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

The W-weighted square moment of row i: ∑ t, W t * B i t ^ 2. This is starProbe 2 (a MULTIGRAPH observable — it needs a double edge i–t); the simple rooted algebra only produces Wᵏ-weighted (k ≥ 2) square moments on coincident unlabeled vertices. It is the sharpest known observable not visibly in the simple span.

Equations

• Graphon.Lovasz.sqMoment B W i = ∑ t : Fin T, W t * B i t ^ 2

theorem Graphon.Lovasz.sqMoment_const_on_orbit {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) {i j : Fin T} (h : vertexOrbitRel B W i j) : sqMoment B W i = sqMoment B W j

The square moment is orbit-invariant (direct, via Equiv.sum_comp).

Cycle–Krylov slice 1 — weighted inner product, self-adjointness, gap identity

Formalization of the algebraic core of the cycle–Krylov–kernel proof (docs/sqmoment-cycle-krylov.md). The operator M is the existing weightedAdj B W (Lovasz.lean); iterates are weightedAdjIter B W q. Slice 2 (separate): the rooted-cycle profile identity cycleDiff q = wInner W (rowDiff B i j) (weightedAdjIter B W q (rowSum B i j)) and the span/range argument closing the gap.

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

Weighted inner product ⟨f, g⟩_W = ∑ t, W t * f t * g t. The form with respect to which weightedAdj B W is self-adjoint (for symmetric B).

Equations

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

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

Row difference ε = B i - B j of the cycle–Krylov argument.

Equations

• Graphon.Lovasz.rowDiff B i j t = B i t - B j t

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

Row sum u = B i + B j of the cycle–Krylov argument.

Equations

• Graphon.Lovasz.rowSum B i j t = B i t + B j t

theorem Graphon.Lovasz.wInner_weightedAdj_comm {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W f g : Fin T → ℝ) : wInner W (weightedAdj B W f) g = wInner W f (weightedAdj B W g)

Self-adjointness of the weighted adjacency operator with respect to wInner W: ⟨M f, g⟩_W = ⟨f, M g⟩_W, using symmetry of B.

theorem Graphon.Lovasz.weightedAdjIter_weightedAdj_comm {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (q : ℕ) (f : Fin T → ℝ) : weightedAdjIter B W q (weightedAdj B W f) = weightedAdj B W (weightedAdjIter B W q f)

Iterates of weightedAdj commute with one application (used to iterate self-adjointness).

theorem Graphon.Lovasz.wInner_weightedAdjIter_comm {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (q : ℕ) (f g : Fin T → ℝ) : wInner W (weightedAdjIter B W q f) g = wInner W f (weightedAdjIter B W q g)

Iterated self-adjointness: ⟨M^[q] f, g⟩_W = ⟨f, M^[q] g⟩_W.

theorem Graphon.Lovasz.sqMoment_sub_eq_wInner {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (i j : Fin T) : sqMoment B W i - sqMoment B W j = wInner W (rowDiff B i j) (rowSum B i j)

The gap identity (Step 4 input of the cycle–Krylov proof): sqMoment i - sqMoment j = ⟨ε, u⟩_W.

theorem Graphon.Lovasz.rowSum_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) : rowSum 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

u ∈ Im M (Step 2 of the cycle–Krylov proof): the row sum is the image under weightedAdj of the W-rescaled pair indicator. Uses hW and symmetry of B.

theorem Graphon.Lovasz.wInner_comm {T : ℕ} (W f g : Fin T → ℝ) : wInner W f g = wInner W g f

Symmetry of the weighted inner product.

theorem Graphon.Lovasz.weightedAdj_add {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 additive.

theorem Graphon.Lovasz.weightedAdjIter_add {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 additive.

theorem Graphon.Lovasz.wInner_sub_iter_add {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (q : ℕ) (f g : Fin T → ℝ) : wInner W (fun (t : Fin T) => f t - g t) (weightedAdjIter B W q fun (t : Fin T) => f t + g t) = wInner W f (weightedAdjIter B W q f) - wInner W g (weightedAdjIter B W q g)

Polarization for self-adjoint iterates: with K = M^[q], ⟨f - g, K (f + g)⟩_W = ⟨f, K f⟩_W - ⟨g, K g⟩_W — the cross terms cancel by (iterated) self-adjointness.

theorem Graphon.Lovasz.closedWalkProfile_eq_wInner {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (v : Fin T) (q : ℕ) : closedWalkProfile B W v (q + 2) = wInner W (fun (t : Fin T) => B v t) (weightedAdjIter B W q fun (t : Fin T) => B v t)

Closed-walk profile as a weighted inner product: CW(v, q+2) = ⟨B v ·, M^[q] (B v ·)⟩_W.

theorem Graphon.Lovasz.closedWalkProfile_sub_eq_wInner {T : ℕ} (B : Fin T → Fin T → ℝ) (hB : ∀ (i j : Fin T), B i j = B j i) (W : Fin T → ℝ) (i j : Fin T) (q : ℕ) : closedWalkProfile B W i (q + 2) - closedWalkProfile B W j (q + 2) = wInner W (rowDiff B i j) (weightedAdjIter B W q (rowSum B i j))

Cycle difference identity, recursive/algebraic form (Step 1 of the cycle–Krylov proof): closed-walk profile differences are exactly ⟨ε, M^[q] u⟩_W. The graph side — rootedProfile of rootedCycleGraph equals closedWalkProfile — is the separate plumbing slice, PROVED as rootedProfile_rootedCycleGraph_eq_closedWalkProfile in Lovasz.lean (an earlier version of this docstring called it a "focused sorry"; stale).

Classwise square-moment descent — now PROVED (no twin-free needed) as classwise_sqMoment_descends in Graphon/CycleKrylov.lean, via decoratedPowerSum_descends_of_rootedProfileEquiv at k = 2 with span membership from InRootedProfileSpan.of_const_on_rpe. Historical notes follow.

If i, j are rooted-profile equivalent and g is atom-invariant, the g-decorated square moments agree. With g = 1_C this is the within-atom square moment ∑_{t ∈ C} W t * B i t ^ 2.

Status after the cycle–Krylov breakthrough (the g = 1 case is PROVED: sqMoment_descends_of_rootedProfileEquiv in Graphon/CycleKrylov.lean):

BEST KNOWN ROUTE (2026-06-10, weight modification — no singular-B issue): for atom-invariant positive g, rooted profiles of (B, W·g) are the (B, W)-profiles with g hung at every unlabeled vertex, hence rpe(B, W) ⟹ rpe(B, W·g); applying the PROVED plain theorem to (B, W·g) gives this classwise statement for positive g, and general atom-invariant g follows by linearity (g = (g + c·1) - c·1). The only missing piece is multi-vertex decoration plumbing: a glue-at-arbitrary-vertex construction (rootAttach only attaches at the root) plus induction hanging one vertex at a time. No new analysis needed.

(Older route, superseded: palindromic decorated cycles reduce the classwise gap to ⟨D_g ε, P₀ (D_g u)⟩_W with P₀ the ker M-projection — closes only det B ≠ 0.) Numerical search for counterexamples (LM cutting-plane, scripts/falsify_classwise_sqmoment.py) found none and went infeasible at both T=4 and T=5 once long-cycle cuts entered.

No harder than #70: it follows from the rank theorem (classwise_sqMoment_of_rank_theorem below).

Minimal test case for the rank theorem — square-moment descent: FULLY PROVED (sorry-free, no twin-freeness) as sqMoment_descends_of_rootedProfileEquiv in Graphon/CycleKrylov.lean, by the cycle–Krylov–kernel argument (docs/sqmoment-cycle-krylov.md): the algebraic slices in this file (sqMoment_sub_eq_wInner, rowSum_eq_weightedAdj, closedWalkProfile_sub_eq_wInner) + the abstract Krylov-kernel lemma + the rooted-cycle bridge in Lovasz.lean. It lives there (not here) because the spectral slice imports inner-product-space machinery that must stay out of the Lovasz.lean import chain.

theorem Graphon.Lovasz.sqMoment_descends_of_rank_theorem {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hrank : ∀ {i j : Fin T}, rootedProfileEquiv B W i j → vertexOrbitRel B W i j) {i j : Fin T} (h : rootedProfileEquiv B W i j) : sqMoment B W i = sqMoment B W j

The reduction direction, made formal: the rank theorem implies square-moment descent. (So the test case is no harder than #70; the conjecture is that it is also the crux.) Stated with the rank theorem as an explicit hypothesis to keep this lemma sorry-free.

theorem Graphon.Lovasz.classwise_sqMoment_of_rank_theorem {T : ℕ} (B : Fin T → Fin T → ℝ) (W : Fin T → ℝ) (hrank : ∀ {a b : Fin T}, rootedProfileEquiv B W a b → vertexOrbitRel B W a b) {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

The classwise reduction direction: the rank theorem implies classwise square-moment descent (reindex by the automorphism; the decoration is atom-invariant, hence invariant along orbits). So the sharpened test case is also no harder than #70. Sorry-free (rank theorem as explicit hypothesis).