#70: Cai–Govorov simple-graph orbit separation — general descent theorem + rank theorem (axiom-clean)#2
Merged
Conversation
New file Graphon/CaiGovorov.lean formalizing the elementary Vandermonde
argument of Cai–Govorov (ITCS 2020 / arXiv:1909.03693) §4, the algebraic
engine for the simple-graph orbit-separation route to #70:
* vandermonde_class_sums_zero (Lemma 4.1): power-sum vanishing for
j < |ι| forces each level-set coefficient sum to vanish (values need
NOT be distinct) — generalizes the distinct-node Vandermonde corollary.
* multivariate_vandermonde_class_sums_zero (Cor 4.2): multivariate
version, classifying indices by their s-tuple.
* supporting: vandermonde_coeffs_zero (Fintype injective nodes),
finset_vandermonde_zero, sum_apply_eq_zero_of_fibers bridge, and the
∀f forms vandermonde_apply_eq_zero / multivariate_vandermonde_apply_eq_zero.
Graph-free (Mathlib-only), wired into Graphon.lean root. All four headline
lemmas #print axioms-clean: [propext, Classical.choice, Quot.sound].
New staging file Graphon/CaiGovorovOrbit.lean (imports CycleKrylov + CaiGovorov):
* starTestGraph S (Gχ): one unlabeled vertex joined to labels S ⊆ Fin K.
* simpleEvalAt_starTestGraph: closed form
simpleEvalAt B W (starTestGraph S) ξ = ∑ₜ W t · ∏_{i∈S} B (ξ i) t.
* supporting: labVertex/unlVertex, edge-set characterization + injectivity,
tau_apply_labVertex/tau_apply_unlVertex (the simpleEvalAt let-τ resolution
in the beta-reduced dite form out_pair_eq' produces).
Generalizes the K=2 commonNeighborGraph special case to arbitrary K and any
label subset S. Axiom-clean [propext, Classical.choice, Quot.sound]. The file is
staged downstream for fast iteration; it will be relocated upstream into Lovasz
when wiring tupleEquivSimple_implies_orbit as a wrapper.
Adds the second Cai–Govorov test graph to Graphon/CaiGovorovOrbit.lean:
* edgeTestGraph Sₗ Sτ (Gλτ): two adjacent unlabeled vertices, the first
joined to labels Sₗ, the second to Sτ.
* simpleEvalAt_edgeTestGraph: closed form
∑ₜ ∑ₜ' W t · W t' · B t t' · (∏_{i∈Sₗ} B (ξ i) t) · (∏_{i∈Sτ} B (ξ i) t').
* supporting: labVertex2/unlVertex0/unlVertex1, three pairwise-disjoint edge
groups, edge-set characterization + per-group injectivity, and the n=2
τ-resolution lemmas tau2_apply_labVertex2/unlVertex0/unlVertex1.
(Sλ renamed Sₗ — λ is a reserved Lean token.) Completes chunk 2 (Gχ + Gλτ
closed forms). Axiom-clean [propext, Classical.choice, Quot.sound].
Toward the super-surjective Cai–Govorov orbit separation (chunk 3A), in the
staging file Graphon/CaiGovorovOrbit.lean:
* SuperSurjective ξ := every host vertex has ≥ 2·T² labels mapping to it.
* prod_label_eq_prod_mult: ∏_{i∈S} B (ξ i) t = ∏_v (B v t)^{|{i∈S:ξ i=v}|}
(regroup labels by host-vertex multiplicity).
* tupleEquivSimple_starTestGraph_mult: the Gχ equation in host-multiplicity
form — ∀ S, ∑_t W t ∏_v (B v t)^{m_S^ξ(v)} = ∑_t W t ∏_v (B v t)^{m_S^ξ'(v)} —
the bridge from tupleEquivSimple + the starTestGraph closed form to the
Vandermonde input.
Axiom-clean [propext, Classical.choice, Quot.sound]. Remaining 3A core (next):
pigeonhole alignment (J_j where ξ' constant), choose-subset-of-size-k_j, the
combined-index Fin T⊕Fin T Vandermonde extraction of the bijection σ, s-bijectivity,
the R₊ step, and s=σ via Gλτ.
…, axiom-clean)
Proves the algebraic heart of the super-surjective orbit separation BEFORE any
pigeonhole/subset bookkeeping (per the staging plan): the Vandermonde engine builds
the vertex matching whenever the aligned moment identity is available.
* aligned_moments_class_balance: for x y : Fin T → Fin T → ℝ and weights a b,
if ∑_t a t ∏_j (x t j)^{k j} = ∑_t b t ∏_j (y t j)^{k j} for every exponent
vector bounded by 2·T, then ∑_{x t = z} a t = ∑_{y t = z} b t for every z.
Via the combined index Fin T ⊕ Fin T reduced to
CaiGovorov.multivariate_vandermonde_class_sums_zero.
* aligned_star_moments_profile_balance / _weight_balance / _support:
specializations to x t = B·t, y t = B(s·)t, a = b = W. Twin-freeness collapses
the left profile set to {t}, giving W t = ∑_{u:∀j,B j t=B(s j)u} W u, hence
∃ u, ∀ j, B j t = B (s j) u.
Bound correction: the exponent range is 2·T (= |Fin T ⊕ Fin T|), not T+1 — with T+1
the class-balance statement is already false at T=2. Matches Cai–Govorov's 0≤k_j<2m.
Axiom-clean [propext, Classical.choice, Quot.sound].
Finite-set bookkeeping (no graph evals) producing the Cai–Govorov reindex s:
* exists_large_const_image_subset: super-surjectivity ⟹ inside each ξ-fibre
over j, a subset J of size ≥ 2T on which ξ' is constant. Via the pigeonhole
Finset.exists_le_card_fiber_of_mul_le_card_of_maps_to (ξ' takes ≤ T values on
a fibre of size ≥ 2T²).
* superMap ξ ξ' hξ : Fin T → Fin T, superFiberSubset ξ ξ' hξ j : Finset (Fin K)
(Classical.choice packaging of the witnesses).
* spec lemmas: superFiberSubset_subset / _card (≥ 2T) / _mem_left (ξ i = j) /
_image_const (ξ' i = superMap … j).
Added import Mathlib.Combinatorics.Pigeonhole. Axiom-clean
[propext, Classical.choice, Quot.sound].
…axiom-clean)
Connects tupleEquivSimple to the aligned-Vandermonde core:
* superFiberSubset_disjoint: distinct ξ-fibres ⟹ disjoint chosen subsets.
* exists_exponent_label_set: for bounded k, select Kf j ⊆ superFiberSubset j
with |Kf j| = k j (via Finset.exists_subset_card_eq).
* aligned_moments_of_tupleEquivSimple_super: THE BRIDGE — for every exponent
vector bounded by 2T,
∑_t W t ∏_j (B j t)^{k j} = ∑_t W t ∏_j (B (superMap … j) t)^{k j},
from h 1 (starTestGraph S) with S = ⋃ⱼ Kf j (Finset.prod_biUnion + per-fibre
collapse ξ≡j, ξ'≡superMap j). Uses the raw ∏_{i∈S} B(ξ i) t form, so NO
injectivity of superMap is needed (the user's exists_exponent_label_set second
multiplicity condition is false without injectivity; replaced by the Kf-family
form, equivalent and sufficient).
* superMap_support: ∀ t, ∃ u, ∀ j, B j t = B (superMap … j) u — the matching,
= aligned_star_moments_support ∘ the bridge.
Axiom-clean [propext, Classical.choice, Quot.sound]. The Vandermonde engine now
provably builds the vertex matching from tupleEquivSimple + super-surjectivity.
Turns superMap_support into a permutation candidate, no edge tests:
* superMap_injective: if superMap a = superMap b, the support witness u gives
B a t = B (superMap a) u = B (superMap b) u = B b t for every t, so rows
B a = B b; twin-freeness forces a = b.
* superMap_bijective: injective endomap of a finite type (Finite.injective_iff_bijective).
* superPerm: superMap as Equiv.Perm (Fin T), with @[simp] superPerm_apply.
Orientation checked: σ = superPerm (= superMap, NOT its inverse), since
superFiberSubset_image_const + _mem_left give ξ' i = superMap (ξ i) on the selected
labels. The preservation lemma B j (s x) = B (s j) x does NOT follow from support
alone (genuinely circular), so edge/weight preservation is deferred to 3A.5 (Gλτ).
Axiom-clean [propext, Classical.choice, Quot.sound].
Sharper variants of the Cai–Govorov Vandermonde lemmas in Graphon/CaiGovorov.lean
that bound the exponent range by the number of DISTINCT VALUES per coordinate
rather than by |ι|. Needed for chunk 3A.5 edge preservation: the pair index is
2T² but each profile coordinate takes only ≤ 2T distinct values, so the edge
bridge's exponents (< 2T) suffice — the |ι|=2T² bound of the original lemma does not.
* vandermonde_class_sums_zero_of_bound / _apply_eq_zero_of_bound: univariate,
bound N ≥ (univ.image x).card.
* multivariate_vandermonde_apply_eq_zero_of_bound / _class_sums_zero_of_bound:
uniform bound M ≥ (univ.image (b · j)).card for every coordinate j.
Mirror the existing |ι|-bounded proofs verbatim with the distinct-value bound
threaded through. Axiom-clean [propext, Classical.choice, Quot.sound].
…uivSimple (axiom-clean)
The pair analogue of the column bridge, via edgeTestGraph (Gλτ):
* prod_biUnion_const (private helper): product over ⋃ⱼ Kf j of a function
constant = c j on each block equals ∏ⱼ (c j)^(Kf j).card.
* aligned_edge_moments_of_tupleEquivSimple_super: for exponent vectors k, l
bounded by 2T,
∑ₓ∑ᵧ W x·W y·B x y·(∏ⱼ(B j x)^{k j})·(∏ⱼ(B j y)^{l j})
= ∑ₓ∑ᵧ W x·W y·B x y·(∏ⱼ(B(superMap j)x)^{k j})·(∏ⱼ(B(superMap j)y)^{l j}),
from h 2 (edgeTestGraph (⋃Kl)(⋃Kt)) + the closed form, regrouping over two
selected label sets (ξ≡j, ξ'≡superMap j per fibre).
Axiom-clean [propext, Classical.choice, Quot.sound]. This is the pair-moment input
for the bounded-Vandermonde edge extraction (superMap_preserves_B), next.
…om-clean) aligned_moments_class_balance_of_bound: the bounded-exponent analogue of the column aligned_moments_class_balance. For profile families x, y with weights a, b, if the moment sums agree for every exponent vector bounded by 2N (where each profile coordinate has ≤ N distinct values on each side), then the a-mass and b-mass over each profile level set agree. Via the combined index ι ⊕ ι reduced to CaiGovorov.multivariate_vandermonde_class_sums_zero_of_bound (bound 2N, side condition (univ.image (bb·c)).card ≤ 2N from card_union_le). This is the pair-capable extraction engine: the edge moments only reach exponent 2T (super-surjectivity limit) but the pair index is 2T², so the |ι|-bounded Vandermonde does not apply — this per-coordinate-bounded version does (each pair profile coordinate takes ≤ 2T distinct values). Axiom-clean [propext, Classical.choice, Quot.sound].
aligned_edge_moments_pair_balance: specializes the bounded extraction engine to
pairs. For profiles col_x = (B · x) and superMap-shifted col, with weight
W p.1·W p.2·B p.1 p.2, the W·B-mass over each pair-profile level set agrees:
∑_p [col_{p.1}=z₁ ∧ col_{p.2}=z₂] W p.1 W p.2 B p.1 p.2
= ∑_p [B(s·)p.1=z₁ ∧ B(s·)p.2=z₂] W p.1 W p.2 B p.1 p.2.
Pair profile encoded over Fin (T+T) via Fin.append (split by Fin.prod_univ_add +
append_left/right), N=T (each coordinate ≤ T distinct values), hmom = the edge
bridge. Axiom-clean [propext, Classical.choice, Quot.sound].
…omorphism
Steps 2-7 of 3A.5. The support-witness map superInv (r) is the automorphism:
* superInv + superInv_spec + superInv_unique (the unique support witness).
* superInv_injective / _bijective (twin-free).
* superInv_preserves_W: support fibre = {superInv t}, weight balance ⟹ W(r t)=W t.
* superInv_preserves_B: pair balance at z=(B·a,B·b) has left fibre {(a,b)} and
right fibre {(r a, r b)} (superInv_unique); positivity cancels weights ⟹
B(r a)(r b)=B a b.
* superInv_eq_superMap: support B a b=B(superMap a)(r b) + B a b=B(r a)(r b)
+ superInv surjective + twin-free ⟹ r=superMap.
* exports superMap_preserves_B / _W, and
superMap_isWeightedAutomorphism : IsWeightedAutomorphism B W (superPerm …).
This resolves the apparent edge/weight circularity (r is the automorphism, then
r=superMap). Axiom-clean [propext, Classical.choice, Quot.sound]. 3A.6 (full-fibre
label reconciliation ξ' i = superMap (ξ i)) is the only remaining super-case piece
before assembling tupleEquivSimple_implies_orbit_super.
…s_orbit_super (axiom-clean)
Completes the super-surjective Cai–Govorov orbit separation (chunk 3A).
* one_extra_label_moment: the one-extra-label moment identity. starTestGraph on
S = {i₀} ∪ ⋃ⱼ Kⱼ (Kⱼ ⊆ superFiberSubset j \ {i₀}) gives, after change of variables
t ↦ superMap t (using superMap's automorphism property),
∑ₜ W t·B(ξ i₀)t·∏ⱼ(B j t)^{kⱼ} = ∑ₜ W t·B(ξ' i₀)(superMap t)·∏ⱼ(B j t)^{kⱼ}.
* superMap_agrees_on_all_labels: ∀ i, ξ' i = superMap (ξ i). Vandermonde class-sum
over Fin T (bound T — single-sided after the change of variables, no 2T needed)
+ twin-free singleton fibres + positivity ⟹ B(ξ i₀)t = B(ξ' i₀)(superMap t) ∀t;
the automorphism property then identifies ξ' i₀ = superMap (ξ i₀).
* tupleEquivSimple_implies_orbit_super : tupleOrbitRel B W ξ ξ' :=
⟨superPerm, superMap_isWeightedAutomorphism, superMap_agrees_on_all_labels⟩.
Axiom-clean [propext, Classical.choice, Quot.sound]. Chunk 3A (super-surjective case)
DONE. Remaining: 3B (amplification → arbitrary ξ), 3C (upstream wrapper).
The Cai–Govorov amplification scaffold (toward removing super-surjectivity):
* ExtLabel K T := Fin K ⊕ (Fin T × Fin (2*T²)) — original labels plus 2*T²
copies per host vertex; Fintype/DecidableEq instances.
* extTuple ξ (inl i = ξ i, inr (v,_) = v); extCard, card_extLabel,
extLabelEquivFin, extTupleFin (the Fin-indexed transport).
* extTuple_superSurjective: every host vertex has its 2*T² copies in the
preimage, so SuperSurjective (extTupleFin ξ) (fibre card ≥ 2*T² = 2*T*T).
* Extends ξ μ := agrees with ξ on the original labels; extensionWeight
(∏ W over the extra-label values, the weight factor in eq. 10).
Axiom-clean [propext, Classical.choice, Quot.sound]. Next: 3B.1b = eq.10 via
trace-induction (iterating multiLabeledEvalK_sum_last_label), per the de-risking
analysis — not raw Fin reindexing.
…he linchpin
The make-or-break identity of the Cai–Govorov super-surjectivity removal: unpinning
all extra labels = a single traced evaluation.
* MultiLabeledGraph.castUnlabeled (hab : a = b) + multiLabeledEvalK_castUnlabeled
(eval-invariance under the val-preserving unlabeled-count cast).
* traceIterExtraLabels m M : fold the last m labels into unlabeled vertices
(recursion on m; m+1 ↦ (traceIterExtraLabels m M.trace).castUnlabeled).
* multiLabeledEvalK_sum_extra_labels:
∑_{ρ : Fin m → Fin T} (∏ⱼ W(ρ j)) · multiLabeledEvalK (K+m) n M B W (Fin.append φ ρ)
= multiLabeledEvalK K (n+m) (traceIterExtraLabels m M) B W φ,
by induction on m, peeling the last label via multiLabeledEvalK_sum_last_label.
Trace-API probe findings (the point of this chunk): castUnlabeled invariance needs
subst (congr 1 won't peel MultiLabeledGraph.mk); induction must generalize n (M auto);
the K+(m+1) vs (K+m)+1 friction needs explicit @Fin.append length args + binding the
sum-last-label instance to a have with explicit HAdd-form type (raw Nat.add vs HAdd
print mismatch). All resolved. Axiom-clean [propext, Classical.choice, Quot.sound].
Next: 3B.1c = read off eq.10 for ξ/ξ' (promote simple G to multi, sum over extension
family) — then the tensor/Vandermonde/counting wrapper (3B.2).
…tity (axiom-clean)
The Cai–Govorov proof gate. Bridges the multigraph trace core back to genuine
simple graphs, then reads off eq.10 for ξ and ξ'.
Step 2 (trace-to-simple bridge, the decisive part):
* simpleEvalAt_eq_multi' (local reproof; Lovász's is private, engine
multiLabeledEvalK_ofSimple is public).
* unlabelExtras G := comap (val-preserving Fin.cast) G (turn the last m labels
into unlabeled vertices, still a SIMPLE graph).
* traceIterExtraLabels_mult: the iterated trace/castUnlabeled reindexing
collapses to a single val-cast (induction on m).
* traceIterExtraLabels_ofSimple_eq / _eval: traceIterᵐ (ofSimple G) =
ofSimple (unlabelExtras G), hence the multi-eval of the traced simple graph
equals simpleEvalAt (unlabelExtras G).
Steps 3-5 (extension family, extras-last Fin encoding):
* ExtendsFin, extensionWeightFin; appendExtensionEquiv ((Fin m → Fin T) ≃
{µ // ExtendsFin ξ µ}, µ = Fin.append ξ ρ); sum_extensions_eq_sum_rho.
* extension_sum_identity (EQUATION 10): tupleEquivSimple B W ξ ξ' ⟹
∑_{µ//ExtendsFin ξ} extensionWeightFin W µ · simpleEvalAt B W G µ
= ∑_{ν//ExtendsFin ξ'} extensionWeightFin W ν · simpleEvalAt B W G ν,
both sides = simpleEvalAt (unlabelExtras G) applied to ξ/ξ', where h closes it.
Axiom-clean [propext, Classical.choice, Quot.sound]. Gate passed: the extension-
family sum identity holds. Next: 3B.2 (separating family + tensor multiplicativity
+ Vandermonde over extension-profiles + char-0 ⟹ J≠∅ ⟹ tupleEquivSimple_implies_orbit).
…tra_labels) Light cleanup before 3B.2: the three 3B.1 proof-gate pillars now all carry docstrings (traceIterExtraLabels_ofSimple_eq and extension_sum_identity already had them; add one to multiLabeledEvalK_sum_extra_labels). CaiGovorovOrbit.lean stays as staging; no relocation and no 3A churn.
…iom-clean)
Toward the Cai–Govorov super-surjectivity-removal wrapper:
* coverExtra T : Fin (T*(2*T²)) → Fin T — the extra-value tuple mapping 2*T²
labels to each host vertex (via finProdFinEquiv: label j ↦ its vertex component).
* superExt ξ := Fin.append ξ (coverExtra T) : Fin (K + T*(2*T²)) → Fin T — the
canonical super-surjective extension (keeps ξ on the first K labels).
* superExt_extends : ExtendsFin ξ (superExt ξ).
* coverExtra_fiber_card : each vertex has exactly 2*T² preimages under coverExtra.
* superExt_superSurjective : SuperSurjective (superExt ξ) (inject the 2*T² copies
via Fin.natAdd K into the fibre).
Axiom-clean [propext, Classical.choice, Quot.sound]. This is η, the fixed
super-surjective reference extension for the orbit families I/J. Next: 3B.2b
(separation via the super-case contrapositive).
… (axiom-clean) not_tupleEquivSimple_of_not_orbit (Cai–Govorov Lemma 10): since superExt ξ is super-surjective, any extension μ not in its weighted-automorphism orbit is not simple-equivalent to superExt ξ (so some simple graph separates them). This is the contrapositive of tupleEquivSimple_implies_orbit_super applied to η = superExt ξ, and is the oracle that builds the finite separating family. Axiom-clean [propext, Classical.choice, Quot.sound]. Next: 3B.2c (iterate multiLabeledEvalK_glue for tensor multiplicativity) + 3B.2d (Vandermonde over extension-profiles + char-0 counting ⟹ J≠∅ ⟹ tupleEquivSimple_implies_orbit).
…cstrings - CaiGovorovOrbit: remove the superseded Sum-type extension family (ExtLabel, extTuple, extCard, extLabelEquivFin, extTupleFin, Extends, extensionWeight, extTuple_superSurjective) — zero references; live path is ExtendsFin/ extensionWeightFin/superExt. - Lovasz: multiEval_separates_orbits docstring said SORRY on a fully proved theorem (fixed); tupleEquivSimple_implies_orbit sorry comment relabeled #62→#70 with the live Cai–Govorov strategy recorded (stale downstream list dropped — #62/#73 roots verify axiom-clean independently); orbit_separation_by_simple_graph comment updated likewise; stale L3018 pointer for connection_matrix_rank_theorem replaced by name reference. - MatrixDetermination: stale '8 sorries' census corrected to the current 6 with breakdown (labeledEvalK_glue is PROVED; star1_tri1 delegates). - SimpleRank: closedWalkProfile_sub_eq_wInner docstring called the proved rootedProfile_rootedCycleGraph_eq_closedWalkProfile a 'focused sorry' (fixed). - Graphon.lean: add the missing CaiGovorovOrbit module bullet. lake build green (2962 jobs); sorry count unchanged at 21.
… chunk 3A (axiom-clean) The 3A engine consumed its tupleEquivSimple hypothesis at exactly three sites (star bridge, edge bridge, one-extra-label moment). New structure TestEvalEq records just those star/edge test-graph equalities; the whole chain (superMap/superPerm/automorphism/reconciliation) now runs from it. Core renamed testEvalEq_implies_orbit_super; tupleEquivSimple_implies_ orbit_super kept as a wrapper via TestEvalEq.of_tupleEquivSimple, so not_tupleEquivSimple_of_not_orbit is unchanged. Why: the eq.(10) descent (chunk 4F) matches extensions only on the star/edge moment profile — full tupleEquivSimple is not available there. lean_verify testEvalEq_implies_orbit_super: [propext, Classical.choice, Quot.sound].
…xiom-clean) MultiLabeledGraph.SimpleMult (all mults ≤ 1) and NoLabelPairs (no label-label edges); toSimple (fromEdgeSet of the mult-1 pairs) with mem_toSimple_edgeFinset, ofSimple_toSimple (section of ofSimple on mult≤1 multigraphs) and simpleEvalAt_toSimple (evaluation transport). Invariant suppliers for ofSimple/empty and the star/edge test graphs (every test edge touches an unlabeled vertex). glueCast some/none characterizations; glue_simpleMult (label-label is the only place glue ADDS multiplicities — NoLabelPairs on the right factor keeps it ≤ 1) and glue_noLabelPairs. This converts glued ofSimple test multigraphs back to honest simple graphs, so eq. (10) can consume products of test moments (chunk 4D).
… (axiom-clean) glueSigma/glueList (foldr over sigma-packaged multigraphs, empty base); multiLabeledEvalK_glueList = map-prod by iterating multiLabeledEvalK_glue; glueList_simpleMult/glueList_noLabelPairs inherit the chunk-4B invariants.
…om-clean)
TestCoord (star ⊕ edge coordinates), testMoment closed forms, coordGraph
(ofSimple test graphs) with coordGraph_eval and the 4B invariants;
expGraph k = glueList of k(c) replicated coordGraphs with
expGraph_eval = ∏_c moment_c^{k c} (via a self-contained
prod_map_flatMap_replicate + Finset.prod_map_toList); expTestGraph =
toSimple with simpleEvalAt_expTestGraph — the moment-power realization
as a SINGLE simple graph, ready for eq. (10). testEvalEq_iff_moments
bridges the chunk-4A interface to moment matching.
…r_moments (axiom-clean) Pure refactor: the hbridge inside extension_sum_identity becomes the public sum_extensions_eval (extension-family sum collapses to one simpleEvalAt of unlabelExtras G) — also the engine for the chunk-5B annihilator. New extension_power_moments = eq. (10) at G := expTestGraph k: the weighted test-moment powers of the extension families of ξ and ξ' agree for EVERY exponent vector — the hmom feed for the 4F Vandermonde.
…e_implies_orbit_general (axiom-clean) The Cai–Govorov descent, completing the simple-graph orbit theorem with NO surjectivity hypothesis: - testProfile (Fin-indexed test-moment vector via Fintype.equivFin) + testProfile_eq_iff. - exists_matching_extension: two-family bounded Vandermonde (aligned_moments_class_balance_of_bound over ι = Fin m → Fin T, N = card ι — exponents realized by GRAPH COPIES, so any bound works) fed by extension_power_moments; positivity of the ξ-side class at the profile of superExt ξ (contains coverExtra T definitionally, W > 0) forces a matching extension of ξ'. - tupleEquivSimple_implies_orbit_general: match extension → moment-form super-case (testEvalEq_implies_orbit_super) at level K + T·2T² → restrict the automorphism to the first K labels via Fin.append_left/superExt_extends. lean_verify: [propext, Classical.choice, Quot.sound]. This proves the statement of the Lovasz.lean:7598 sorry (tupleEquivSimple_implies_orbit) downstream; the rank-residue wiring (chunks 5A-5C) comes next.
…OrbitRank.lean CycleKrylov sits upstream of CaiGovorovOrbit, so the rank residue could not consume the Cai-Govorov machinery at its old home. Moved verbatim (instFintypeOrbitClass, orbitInvariantToClassFun, orbitInvariantEquiv, finrank_orbitInvariantSubmodule, the sorry'd residue, Phase D collapse, hard inclusion) into Graphon/SimpleOrbitRank.lean importing CaiGovorovOrbit; pointer comment left in CycleKrylov; registered in the root module. Sorry count unchanged (the residue sorry moved files). NB Spectral.lean (unimported leaf) declares its own same-named instFintypeOrbitClass; no clash on any current import chain.
…de annihilator (axiom-clean)
Any c : OrbitClass → ℝ annihilating every simple evaluation at orbit
representatives is zero — strictly stronger than point separation, and
exactly what the rank lower bound needs. Signed single-family Vandermonde
over OrbitClass × (Fin m → Fin T) with the test-moment profile of
Fin.append (out q) ρ as classifier: hmom collapses per-q via
sum_extensions_eval + simpleEvalAt_expTestGraph to the hc hypothesis at
unlabelExtras (expTestGraph k); the class of the superExt (out q₀)
profile is exactly {q₀} ×ˢ P (chunk 4A at level K+m forces q = q₀ via
Quotient.sound/out_eq); positive W-mass of P (coverExtra T member)
kills c q₀.
lean_verify eval_rep_annihilator_zero: [propext, Classical.choice,
Quot.sound].
…_orbitClass PROVED (axiom-clean, −1 sorry) evalRepPairing (representative pairing ⟨c,f⟩ = ∑ q, c q · f (out q), a bilinear mk₂ mirroring orbitInnerBil) + the dual-pairing argument transcribed from connectionMatrix_full_rank_of_orthogonal (hle1 half): Ψ := subtype.dualMap ∘ evalRepPairing is injective by eval_rep_annihilator_zero (instantiated at the span generators), so #OrbitClass = finrank (OrbitClass → ℝ) ≤ finrank (Dual simpleEvalSubmodule) = finrank simpleEvalSubmodule. With the residue gone, simpleEvalSubmodule_eq_orbitInvariantSubmodule and orbitInvariantSubmodule_le_simpleEvalSubmodule are now sorry-free: THE #70 RANK THEOREM (simple-eval span = orbit-invariant functions) IS FULLY PROVED. lean_verify on both: [propext, Classical.choice, Quot.sound]. lake build green; project sorry count 21 → 20; CycleKrylov.lean is now sorry-free.
…vOrbit header) Lovasz sorry comments at tupleEquivSimple_implies_orbit and orbit_separation_by_simple_graph now state the theorem is PROVED downstream (tupleEquivSimple_implies_orbit_general) and that the former Option B rank argument is REALIZED in SimpleOrbitRank.lean; the CaiGovorovOrbit module header is rewritten from 'staging file' to the full architecture map (3A/3B/4A–4G + pointer to the rank endgame). lake build green; sorry count 20.
…rmonde dedup) Review (PR #2, high effort): no proof/statement defects; 10 confirmed documentation & cleanup findings, all fixed: 1. Lovasz 7567-comment falsely claimed nothing proved depends on the tupleEquivSimple_implies_orbit sorry — corrected: the simple-side chain (k1_orbit_sep_aux → of_const_on_orbit → label_unlabeled_square_moment_descends) IS still tainted; only the multigraph #62/#73 chain is independent. 2. orbit_separation_by_simple_graph docstring: stale BLOCKED-on-#62 status replaced with the proved-downstream status. 3. tupleEquivSimple_implies_orbit docstring: 'not derivable from simple-graph evaluations alone' marked superseded — the Cai–Govorov route refutes it (scoped the claim to the original induction plan). 4. SimpleOrbitRank Phase-D docstring: dropped stale 'modulo the lower bound' caveat (now unconditional). 5. CycleKrylov MOVED note: accurate about which four declarations were self-contained; documents the lost Fintype (OrbitClass) instance for CycleKrylov-only importers. 6. not_tupleEquivSimple_of_not_orbit: docstring no longer claims a live 'oracle' role (descent routes through exists_matching_extension); dropped the unexplained 'Lemma 10' numbering; module docstring bullet likewise. 7. tupleEquivSimple_starTestGraph_mult: docstring no longer claims to be the live Vandermonde bridge (that is aligned_moments_of_testEvalEq_super). 8. CaiGovorov: 80-line unbounded multivariate apply_eq_zero (and its class-sums form) deduplicated into one-line corollaries of the bounded engine at M := card ι, relocated after it. 9. CaiGovorov header: proper copyright/Authors attribution. 10. superMap_support: removed conversational artifact from docstring. lake build green; sorry count unchanged (20).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes the mathematical core of #70 (simple-graph orbit separation, Lovász §3): 31 commits building the complete Cai–Govorov route (ITCS 2020, arXiv:1909.03693), ending with two fully proved, axiom-clean headline theorems.
Headline results
tupleEquivSimple_implies_orbit_general(Graphon/CaiGovorovOrbit.lean): if all simple-graph evaluations at two K-tuples agree, the tuples are related by a weighted automorphism — no surjectivity hypothesis. This is the statement of the long-standingtupleEquivSimple_implies_orbitsorry (Lovász Lemma 2.4, simple form).Graphon/SimpleOrbitRank.lean, new file):simpleEvalSubmodule = orbitInvariantSubmodule— the former sole named residuesimpleEvalSubmodule_finrank_ge_orbitClassis filled via a signed-Vandermonde annihilator argument + dual-pairing injectivity.Architecture
Graphon/CaiGovorov.lean).TestEvalEqinterface.toSimplebridge +glueListproduct law realize test-moment powers as single simple graphs (the test graphs have no label-label edges, sidestepping the Hadamard-square obstruction); a two-family Vandermonde matches an extension of ξ′ againstsuperExt ξ; the super-case runs at level K + T·2T² and restricts.CycleKrylov.lean(now sorry-free);eval_rep_annihilator_zero+evalRepPairingtranscribe the proven multigraph dual-pairing argument.Verification
lake buildgreen (2963 jobs), warning-clean on the touched files.#print axioms-equivalent (lean_verify):[propext, Classical.choice, Quot.sound]only.Not in scope
The legacy
Lovasz.lean§3.10 sorries (tupleEquivSimple_implies_orbitat its original home and its neighbors) remain, documented as proved-downstream: filling them in place requires relocating the Cai–Govorov stack above Lovász §3.10 — a follow-up refactor.